diff --git "a/app.py" "b/app.py" --- "a/app.py" +++ "b/app.py" @@ -1,28 +1,18 @@ #!/usr/bin/env python3 """ -PRACTICALITY SYSTEM 13.0 — SEQUENCE RAYS +PRACTICALITY SYSTEM 14.0 — REAL-WORLD DOMAIN SUITE ═══════════════════════════════════════════════════════════════════ -NEW IN 13.0: - · 27 Axioms: expanded from 15 to include physics (EQUILIBRIUM, - SUPERPOSITION, LOCALITY, EXTREMAL, ENTROPY), mathematics - (MONOTONE, CONVEX, PARSIMONY), logic/philosophy (DUALITY, - HOLISM, IMPLICATION, NEGATION). - · Rays as Ordered Sequences: [A→B→C] ≠ [C→B→A]. Sequence order - is structural. Each axiom constructor is called in order with - the partial binding produced by all prior axioms as its context. - · Contradiction at Distance: contradicting axioms forbidden only - when ADJACENT in the sequence. Non-adjacent contradictions are - allowed — the chain earns its own coherence through mediating - axioms between them. - · Baton Protocol: rays do not fail, they terminate with a partial - binding (the baton). Child rays inherit it and continue. - Branching occurs from both stalling AND productive rays. - · Earned Extension: a ray earns the right to branch by achieving - a CE reduction ratio. Below MIN_DEPTH all rays branch freely. - · Each axiom owns its own hypothesis constructor derived from its - mathematical/physical meaning — not a weight scalar on shared types. - · Wisdom lives in the combinatorial sequence space itself. - No learning. No signatures. No bias. +14 Problems across 11 domains: + Cryptography · Finance · Energy · Chemistry · Physics · Chaos + Game Theory · Astronomy · Engineering · Signal Processing · Mathematics + +New in 14.0: + · 10 real-world AXL problems (hardcoded, no LLM) + · AXLInvariant mode: "eq" | "geq" (fixes GEQ semantic) + · PROBLEM_META: domain / category tagging + · PROBLEM_STATS: per-problem live performance tracking + · Round-robin cycling: every problem gets tested evenly + · Multi-domain performance table in dashboard """ import time, random, math, threading, asyncio, warnings, itertools @@ -44,24 +34,24 @@ import uvicorn warnings.filterwarnings("ignore") USE_GPU = torch.cuda.is_available() DEVICE = torch.device("cuda" if USE_GPU else "cpu") -print(f"[SYSTEM 13.0] Compute: {'GPU' if USE_GPU else 'CPU'}") +print(f"[SYSTEM 14.0] Compute: {'GPU' if USE_GPU else 'CPU'}") # ══════════════════════════════════════════════════════════════════════ # SECTION 1: CONSTANTS # ══════════════════════════════════════════════════════════════════════ -SOLVE_THRESHOLD = 0.05 -VERIFY_G1_THRESHOLD = 0.08 -VERIFY_G2_TOLERANCE = 1e-3 -HC4_VOLUME_FLOOR = 0.20 -L9_CONTRIB_THRESHOLD = 1e-8 -HUB_RESIDUAL_MULT = 2.0 -HUB_DEGREE_RATIO = 0.6 -MAX_HYPS_PER_AXIOM = 4 -BRANCH_DEPTH = 3 -MANIFOLD_STEPS = [0.05, 0.2, -0.05, -0.2, 0.5, -0.5] -N_MPRT_EXPLORE = 20000 if USE_GPU else 3000 -POLISH_STEPS = 40 -ADAM_STEPS = 30 +SOLVE_THRESHOLD = 0.05 +VERIFY_G1_THRESHOLD = 0.08 +VERIFY_G2_TOLERANCE = 1e-3 +HC4_VOLUME_FLOOR = 0.20 +L9_CONTRIB_THRESHOLD = 1e-8 +HUB_RESIDUAL_MULT = 2.0 +HUB_DEGREE_RATIO = 0.6 +MAX_HYPS_PER_AXIOM = 4 +BRANCH_DEPTH = 3 +MANIFOLD_STEPS = [0.05, 0.2, -0.05, -0.2, 0.5, -0.5] +N_MPRT_EXPLORE = 20000 if USE_GPU else 3000 +POLISH_STEPS = 40 +ADAM_STEPS = 30 PROJECTION_CACHE: Dict = {} # ══════════════════════════════════════════════════════════════════════ @@ -134,10 +124,10 @@ def compile_iv(expr,variables): return _c(expr) # ══════════════════════════════════════════════════════════════════════ -# SECTION 3: PSL 2.0 PARSER (unchanged from 12.1) +# SECTION 3: PSL 2.0 PARSER # ══════════════════════════════════════════════════════════════════════ @dataclass -class PSLVar: name:str; lo:float; hi:float; weight:float=1.0 +class PSLVar: name:str; lo:float; hi:float @dataclass class PSLConstraint: kind:str; expr:str; scope:str="root"; weight:float=1.0; branches:List[str]=field(default_factory=list) @dataclass @@ -154,9 +144,8 @@ def parse_psl(text:str) -> PSLProgram: def pvar(rest): p=rest.split(); return PSLVar(p[0],float(p[1]),float(p[2])) if len(p)>=3 else None def pw(rest): - if 'WEIGHT' in rest: - p=rest.split('WEIGHT'); return p[0].strip(), float(p[1].split()[0]) - return rest.strip(), 1.0 + if 'WEIGHT' in rest: p=rest.split('WEIGHT'); return p[0].strip(),float(p[1].split()[0]) + return rest.strip(),1.0 def parse_scope_body(sname,order=0,depends=None): svars,scons,links=[],[],[] while i PSLProgram: if bl.upper().startswith("OPTION"): opts.append(bl.split(None,1)[1].strip()) advance() scons.append(PSLConstraint("or_eq","",scope=sname,weight=1.0,branches=opts)) - elif kw=="ANNOTATE": - parts=rest.split() - if len(parts)>=3: prog.annotations[parts[0]]=parts[2] return PSLScope(sname,order,depends or [],svars,links,scons) while i PSLProgram: if bl.upper().startswith("OPTION"): opts.append(bl.split(None,1)[1].strip()) advance() prog.constraints.append(PSLConstraint("or_eq","",weight=1.0,branches=opts)) - elif kw=="ANNOTATE": - parts=rest.split() - if len(parts)>=3: prog.annotations[parts[0]]=parts[2] elif kw=="SCOPE": parts=rest.split(); sname=parts[0] if parts else f"s{len(prog.scopes)}" order=0; depends=[] @@ -265,11 +248,12 @@ def expand_psl(prog:PSLProgram) -> ExpandedProblem: return ExpandedProblem(variables,bounds,constraints,dict(scope_groups),dict(scope_vars),prog.scope_order,prog.annotations) # ══════════════════════════════════════════════════════════════════════ -# SECTION 4: AXL LAYER (unchanged from 12.1) +# SECTION 4: AXL LAYER # ══════════════════════════════════════════════════════════════════════ @dataclass class AXLInvariant: name:str; expr:str; tolerance:float=VERIFY_G2_TOLERANCE + mode:str="eq" # "eq": |expr|=-tol | "leq": expr<=tol @dataclass class AXLProblemDef: @@ -285,10 +269,8 @@ class AXLtoPSLCompiler: lines=[f"SPACE base_{prob.name}"] for v in prob.variables: lo,hi=v["lo"],v["hi"] - if v["name"] in prob.observations: - val=prob.observations[v["name"]]; lo=hi=val + if v["name"] in prob.observations: val=prob.observations[v["name"]]; lo=hi=val lines.append(f"VAR {v['name']} {lo} {hi}") - lines.append(f"ANNOTATE {v['name']} FROM_AXL {prob.name}.{v['name']}") for c in prob.constraints: wt=c.get("weight",1.0) if c["kind"]=="CONSERVE": lines.append(f"CONSERVE {c['expr']}") @@ -320,7 +302,7 @@ class AXLtoPSLCompiler: AXL_COMPILER=AXLtoPSLCompiler() # ══════════════════════════════════════════════════════════════════════ -# SECTION 5: PROBLEM & CONSTRAINT COMPILATION (unchanged from 12.1) +# SECTION 5: PROBLEM COMPILATION # ══════════════════════════════════════════════════════════════════════ @dataclass class Constraint: @@ -355,8 +337,7 @@ def compile_mc(kind,expr_str,direction,variables,weight=1.0,scope="root",branche except: pass if not rivs: return IV(-1e18,1e18) return IV(min(r.lo for r in rivs),max(r.hi for r in rivs)) - mc.fast_iv=_or_iv - return mc + mc.fast_iv=_or_iv; return mc syms={v:sp.Symbol(v) for v in variables} try: parsed=parse_expr(expr_str,local_dict=syms); mc.parsed=parsed @@ -415,9 +396,9 @@ class Problem: if mc.fast_pt is None: total+=1.0; continue try: val=float(mc.fast_pt(*[b.get(v,0.0) for v in mc.syms_used])) - if mc.kind=="equality": total+=abs(val)*mc.weight - elif mc.direction=="geq": total+=max(0.0,-val)*mc.weight - else: total+=max(0.0,val)*mc.weight + if mc.kind=="equality": total+=abs(val)*mc.weight + elif mc.direction=="geq": total+=max(0.0,-val)*mc.weight + else: total+=max(0.0, val)*mc.weight except: total+=1.0 for v,(lo,hi) in self.bounds.items(): bv=b.get(v,0.0); total+=max(0.0,lo-bv)+max(0.0,bv-hi) @@ -483,9 +464,9 @@ class Problem: if len(args)!=len(mc.syms_used): total+=1.0; continue val=mc.fast_np(*args) if not isinstance(val,np.ndarray): val=np.full(N,float(val),dtype=np.float32) - if mc.kind=="equality": total+=np.abs(val)*mc.weight - elif mc.direction=="geq": total+=np.maximum(0.0,-val)*mc.weight - else: total+=np.maximum(0.0,val)*mc.weight + if mc.kind=="equality": total+=np.abs(val)*mc.weight + elif mc.direction=="geq": total+=np.maximum(0.0,-val)*mc.weight + else: total+=np.maximum(0.0, val)*mc.weight except: total+=1.0 for i,v in enumerate(var_order): lo,hi=self.bounds[v]; col=b_matrix[:,i] @@ -493,7 +474,7 @@ class Problem: return total # ══════════════════════════════════════════════════════════════════════ -# SECTION 6: VERIFY LAYER (unchanged from 12.1) +# SECTION 6: VERIFY LAYER (mode-aware) # ══════════════════════════════════════════════════════════════════════ @dataclass class VerifyResult: @@ -503,7 +484,7 @@ class VerifyResult: failed_gates:List[str]=field(default_factory=list) class VerifyLayer: - def run(self,binding,base_problem,anchors): + def run(self,binding:Dict[str,float],base_problem:Problem,anchors:List[AXLInvariant]) -> VerifyResult: g1_ce=base_problem.constraint_energy(binding) g1_pass=g1_ce=-inv.tolerance # constraint satisfied + elif inv.mode=="leq": passed=val<=inv.tolerance # constraint satisfied + else: passed=err bool: - """Only adjacent pairs checked. Distance ≥ 2 contradiction = allowed.""" +def sequence_valid(seq:List[str]) -> bool: for i in range(len(seq)-1): - if frozenset([seq[i], seq[i+1]]) in _CONTRA_SET: - return False + if frozenset([seq[i],seq[i+1]]) in _CONTRA_SET: return False return True # ══════════════════════════════════════════════════════════════════════ @@ -616,43 +567,22 @@ class Hypothesis: @dataclass class Baton: - """ - The partial solution passed between rays like a relay baton. - A ray does not fail — it terminates and hands this to its children. - """ - binding: Dict[str,float] - ce: float - ray_id: str = "" - depth: int = 0 - l7: Optional[Any] = None # TopologyCert — lazily computed - l9: Optional[Any] = None # ResidualCert — lazily computed + binding:Dict[str,float]; ce:float + ray_id:str=""; depth:int=0 + l7:Optional[Any]=None; l9:Optional[Any]=None @dataclass class AxiomRay: - """ - A ray is an ordered sequence of axioms, not an unordered set. - [A→B→C] is structurally different from [C→B→A]. - """ - sequence: List[str] - ray_id: str - depth: int = 0 - parent_id: Optional[str] = None - baton: Optional[Baton] = None - + sequence:List[str]; ray_id:str; depth:int=0 + parent_id:Optional[str]=None; baton:Optional[Baton]=None @property def name(self) -> str: return "→".join(AXIOM_ABBR.get(a,a[:3]) for a in self.sequence) - - def extend(self, axiom: str) -> Optional['AxiomRay']: - new_seq = self.sequence + [axiom] + def extend(self,axiom:str) -> Optional['AxiomRay']: + new_seq=self.sequence+[axiom] if sequence_valid(new_seq): - return AxiomRay( - sequence = new_seq, - ray_id = f"{self.ray_id}+{AXIOM_ABBR.get(axiom,'?')}", - depth = self.depth + 1, - parent_id = self.ray_id, - baton = None # caller sets baton - ) + return AxiomRay(sequence=new_seq,ray_id=f"{self.ray_id}+{AXIOM_ABBR.get(axiom,'?')}", + depth=self.depth+1,parent_id=self.ray_id) return None @dataclass @@ -669,7 +599,7 @@ class StructuralModel: scope_witnesses:Dict[str,Dict[str,Tuple]]=field(default_factory=dict) # ══════════════════════════════════════════════════════════════════════ -# SECTION 9: ORACLES (unchanged from 12.1) +# SECTION 9: ORACLES # ══════════════════════════════════════════════════════════════════════ @dataclass class L7Certificate: topology_sig:str; hub_vars:List[str]; solve_order:List[str] @@ -717,11 +647,10 @@ class ResidualOracle: re=[e for e,c in sorted(de,key=lambda x:-x[1])[:5]] return L9Certificate(round(ce,6),rv,re) -TOPOLOGY_ORACLE=TopologyOracle() -RESIDUAL_ORACLE=ResidualOracle() +TOPOLOGY_ORACLE=TopologyOracle(); RESIDUAL_ORACLE=ResidualOracle() # ══════════════════════════════════════════════════════════════════════ -# SECTION 10: CORE SOLVERS (unchanged from 12.1) +# SECTION 10: CORE SOLVERS # ══════════════════════════════════════════════════════════════════════ def _hc4(box,constraints): cur=dict(box) @@ -858,862 +787,1009 @@ def _test_hypothesis(problem,hyp): return best_b,best_ce # ══════════════════════════════════════════════════════════════════════ -# SECTION 11: HYPOTHESIS CONSTRUCTORS -# One constructor per axiom. Each derives its behavior from what that -# axiom MEANS mathematically/physically, not from a weight scalar. -# Signature: (problem, baton, all_batons, model) -> List[Hypothesis] +# SECTION 11: HYPOTHESIS CONSTRUCTORS (27 axioms — same as v13.0) # ══════════════════════════════════════════════════════════════════════ - -def _proj_val(mc, v, b): - """Utility: attempt projection of variable v from constraint mc.""" +def _proj_val(mc,v,b): if v not in mc.projections: return None for proj in mc.projections[v]: try: - val = float(proj["func"](*[b.get(s,0.0) for s in proj["syms"]])) - if math.isfinite(val) and abs(val) < 1e6: return val + val=float(proj["func"](*[b.get(s,0.0) for s in proj["syms"]])) + if math.isfinite(val) and abs(val)<1e6: return val except: pass return None -def _make_hyp(hid, binding, h_type, claim, derivation, pinned, free, conf): - return Hypothesis(hid=hid, binding=binding, h_type=h_type, claim=claim, - derivation=derivation, pinned_vars=pinned, free_vars=free, confidence=conf) - -# ── Mathematics ──────────────────────────────────────────────────────── +def _make_hyp(hid,binding,h_type,claim,derivation,pinned,free,conf): + return Hypothesis(hid=hid,binding=binding,h_type=h_type,claim=claim, + derivation=derivation,pinned_vars=pinned,free_vars=free,confidence=conf) -def _hyp_continuous(problem, baton, all_batons, model): - """Null-space tangent step on the equality manifold.""" - hyps = []; b = baton.binding - eq_mcs = [mc for mc in problem.compiled_constraints if mc.kind=="equality" and mc.fast_jac] +def _hyp_continuous(problem,baton,all_batons,model): + hyps=[]; b=baton.binding + eq_mcs=[mc for mc in problem.compiled_constraints if mc.kind=="equality" and mc.fast_jac] if not eq_mcs: return hyps - nv = len(problem.variables) - J = np.zeros((len(eq_mcs), nv)) + nv=len(problem.variables); J=np.zeros((len(eq_mcs),nv)) for i,mc in enumerate(eq_mcs): for j,v in enumerate(problem.variables): if v not in mc.fast_jac: continue - jac = mc.fast_jac[v] - try: J[i,j] = float(jac["func"](*[b.get(s,0.0) for s in jac["syms"]])) + jac=mc.fast_jac[v] + try: J[i,j]=float(jac["func"](*[b.get(s,0.0) for s in jac["syms"]])) except: pass try: - _,sv,Vt = np.linalg.svd(J,full_matrices=True); rank = np.sum(sv>1e-8) - if rank >= Vt.shape[0]: return hyps + _,sv,Vt=np.linalg.svd(J,full_matrices=True); rank=np.sum(sv>1e-8) + if rank>=Vt.shape[0]: return hyps for di,nd in enumerate(Vt[rank:][:2]): for step in MANIFOLD_STEPS: - nb = {v:max(problem.bounds[v][0],min(problem.bounds[v][1],b.get(v,0.0)+step*nd[j])) - for j,v in enumerate(problem.variables)} + nb={v:max(problem.bounds[v][0],min(problem.bounds[v][1],b.get(v,0.0)+step*nd[j])) + for j,v in enumerate(problem.variables)} hyps.append(_make_hyp(f"cnt_d{di}_s{step}",nb,"continuous", - f"Manifold(dir={di},step={step:.2f})",[f"null_{di}"],{},problem.variables,0.45)) + f"Manifold(d={di},s={step:.2f})",[f"null_{di}"],{},problem.variables,0.45)) except: pass return hyps -def _hyp_discrete(problem, baton, all_batons, model): - """Topological chain: propagate HC4 through scope ordering.""" - tb = _global_hc4_tighten(problem); b = dict(baton.binding); steps = [] - l7 = baton.l7 +def _hyp_discrete(problem,baton,all_batons,model): + tb=_global_hc4_tighten(problem); b=dict(baton.binding); steps=[] + l7=baton.l7 if not l7 or not l7.solve_order: return [] for sn in l7.solve_order: - svars = problem.scope_vars.get(sn,[]) + svars=problem.scope_vars.get(sn,[]) if not svars: continue - smcs = [problem.compiled_constraints[i] for i in problem.scope_groups.get(sn,[])] + smcs=[problem.compiled_constraints[i] for i in problem.scope_groups.get(sn,[])] if not smcs: continue - box = {v:IV(*tb.get(v,problem.bounds.get(v,(-10,10)))) for v in svars if v in problem.bounds} - cont = _hc4(box, smcs) + box={v:IV(*tb.get(v,problem.bounds.get(v,(-10,10)))) for v in svars if v in problem.bounds} + cont=_hc4(box,smcs) if cont: for v,iv in cont.items(): b[v]=iv.mid() steps.append(sn) if not steps: return [] - pinned = {v:b[v] for sn in steps for v in problem.scope_vars.get(sn,[]) if v in b} + pinned={v:b[v] for sn in steps for v in problem.scope_vars.get(sn,[]) if v in b} return [_make_hyp(f"dis_{'_'.join(s[:4] for s in steps)}",b,"discrete", f"TopoChain({' → '.join(steps)})",steps,pinned, [v for v in problem.variables if v not in pinned],0.80)] -def _hyp_quadratic(problem, baton, all_batons, model): - """Algebraic root projection on quadratic constraints.""" - hyps = []; b = dict(baton.binding); l9 = baton.l9 +def _hyp_quadratic(problem,baton,all_batons,model): + hyps=[]; b=dict(baton.binding); l9=baton.l9 if not l9: return hyps for expr_str in l9.dominant_exprs[:3]: - mc = next((mc for mc in problem.compiled_constraints if mc.expr_str==expr_str),None) + mc=next((mc for mc in problem.compiled_constraints if mc.expr_str==expr_str),None) if not mc or not mc.projections: continue for v,projs in mc.projections.items(): - lo,hi = problem.bounds.get(v,(-1e18,1e18)) + lo,hi=problem.bounds.get(v,(-1e18,1e18)) for pi,proj in enumerate(projs): try: - val = float(proj["func"](*[b.get(s,0.0) for s in proj["syms"]])) + val=float(proj["func"](*[b.get(s,0.0) for s in proj["syms"]])) if not(lo<=val<=hi) or not math.isfinite(val): continue - nb = dict(b); nb[v]=val + nb=dict(b); nb[v]=val hyps.append(_make_hyp(f"qua_{hash(expr_str)%9999}_{v}_{pi}",nb,"quadratic", - f"QuadRoot({v}={val:.4f})",[expr_str],{v:val}, + f"Root({v}={val:.4f})",[expr_str],{v:val}, [u for u in problem.variables if u!=v],0.80 if pi==0 else 0.65)) except: pass return hyps -def _hyp_bilinear(problem, baton, all_batons, model): - """Geometric mean split for bilinear product constraints.""" - hyps = []; b = dict(baton.binding) +def _hyp_bilinear(problem,baton,all_batons,model): + hyps=[]; b=dict(baton.binding) for mc in problem.compiled_constraints: if not mc.parsed: continue - expr = mc.parsed - if not expr.is_Add: continue - for term in expr.args: + if not mc.parsed.is_Add: continue + for term in mc.parsed.args: if not term.is_Mul: continue - syms_in = [str(s) for s in term.free_symbols if str(s) in problem.variables] - if len(syms_in) != 2: continue - vi,vj = syms_in - lo_i,hi_i = problem.bounds.get(vi,(0,10)) - lo_j,hi_j = problem.bounds.get(vj,(0,10)) - product = abs(b.get(vi,1)*b.get(vj,1)) - gm = math.sqrt(product) if product >= 0 else 0 + syms_in=[str(s) for s in term.free_symbols if str(s) in problem.variables] + if len(syms_in)!=2: continue + vi,vj=syms_in + lo_i,hi_i=problem.bounds.get(vi,(0,10)); lo_j,hi_j=problem.bounds.get(vj,(0,10)) + product=abs(b.get(vi,1)*b.get(vj,1)) + gm=math.sqrt(product) if product>=0 else 0 if lo_i<=gm<=hi_i and lo_j<=gm<=hi_j: - nb = dict(b); nb[vi]=gm; nb[vj]=gm + nb=dict(b); nb[vi]=gm; nb[vj]=gm hyps.append(_make_hyp(f"bil_{vi}_{vj}",nb,"bilinear", f"GeoMean({vi}={vj}={gm:.4f})",["bilinear"],{vi:gm,vj:gm}, [v for v in problem.variables if v not in [vi,vj]],0.70)) return hyps -def _hyp_metric(problem, baton, all_batons, model): - """Radial projection onto norm sphere constraints.""" - hyps = []; b = dict(baton.binding) +def _hyp_metric(problem,baton,all_batons,model): + hyps=[]; b=dict(baton.binding) for mc in problem.compiled_constraints: if mc.kind!="equality" or not mc.parsed: continue - expr = mc.parsed - if not expr.is_Add: continue - sq_terms = [t for t in expr.args if t.is_Pow and t.args[1]==2] - if len(sq_terms) < 2: continue - vars_in = [str(s) for s in expr.free_symbols if str(s) in problem.variables] - curr_val = sum(b.get(v,0)**2 for v in vars_in) - if curr_val < 1e-8: continue - const_terms = [t for t in expr.args if t.is_Number] + if not mc.parsed.is_Add: continue + sq_terms=[t for t in mc.parsed.args if t.is_Pow and t.args[1]==2] + if len(sq_terms)<2: continue + vars_in=[str(s) for s in mc.parsed.free_symbols if str(s) in problem.variables] + curr_val=sum(b.get(v,0)**2 for v in vars_in) + if curr_val<1e-8: continue + const_terms=[t for t in mc.parsed.args if t.is_Number] if not const_terms: continue - target = -float(const_terms[0]) - if target <= 0: continue - scale = math.sqrt(target/curr_val) - nb = dict(b) + target=-float(const_terms[0]) + if target<=0: continue + scale=math.sqrt(target/curr_val) + nb=dict(b) for v in vars_in: - lo,hi = problem.bounds.get(v,(-10,10)) - nb[v] = max(lo,min(hi,b.get(v,0)*scale)) + lo,hi=problem.bounds.get(v,(-10,10)) + nb[v]=max(lo,min(hi,b.get(v,0)*scale)) hyps.append(_make_hyp(f"met_{hash(mc.expr_str)%9999}",nb,"metric", - f"RadialProject(scale={scale:.4f})",["metric",mc.expr_str],{},list(problem.variables),0.75)) + f"RadialProject(s={scale:.4f})",["metric",mc.expr_str],{},list(problem.variables),0.75)) return hyps -def _hyp_symmetric(problem, baton, all_batons, model): - """Pairwise variable swaps — symmetry group exploration.""" - hyps = []; b = dict(baton.binding); vl = problem.variables +def _hyp_symmetric(problem,baton,all_batons,model): + hyps=[]; b=dict(baton.binding); vl=problem.variables for i in range(min(len(vl),5)): for j in range(i+1,min(len(vl),5)): - vi,vj = vl[i],vl[j] - lo_i,hi_i = problem.bounds[vi]; lo_j,hi_j = problem.bounds[vj] + vi,vj=vl[i],vl[j] + lo_i,hi_i=problem.bounds[vi]; lo_j,hi_j=problem.bounds[vj] if lo_i<=b.get(vj,0)<=hi_i and lo_j<=b.get(vi,0)<=hi_j: - nb = dict(b); nb[vi],nb[vj] = b.get(vj,0),b.get(vi,0) + nb=dict(b); nb[vi],nb[vj]=b.get(vj,0),b.get(vi,0) hyps.append(_make_hyp(f"sym_{vi}_{vj}",nb,"symmetric",f"Swap({vi}↔{vj})", ["symmetric"],{vi:nb[vi],vj:nb[vj]}, [v for v in vl if v not in [vi,vj]],0.60)) return hyps -def _hyp_ordered(problem, baton, all_batons, model): - """Enforce variable ordering by midpoint balancing.""" - b = dict(baton.binding); nb = dict(b) - ord_mcs = [mc for mc in problem.compiled_constraints - if mc.kind=="inequality" and len(mc.syms_used)==2] +def _hyp_ordered(problem,baton,all_batons,model): + b=dict(baton.binding); nb=dict(b) + ord_mcs=[mc for mc in problem.compiled_constraints if mc.kind=="inequality" and len(mc.syms_used)==2] for mc in ord_mcs: - vi,vj = mc.syms_used - lo_i,hi_i = problem.bounds.get(vi,(-1e18,1e18)) - lo_j,hi_j = problem.bounds.get(vj,(-1e18,1e18)) + if len(mc.syms_used)<2: continue + vi,vj=mc.syms_used[0],mc.syms_used[1] + lo_i,hi_i=problem.bounds.get(vi,(-1e18,1e18)); lo_j,hi_j=problem.bounds.get(vj,(-1e18,1e18)) if mc.direction=="geq" and nb.get(vi,0)1e-10: nb[v]=max(lo,min(hi,nb[v]-0.05*g)) - return [_make_hyp(f"mon_{hash(str(nb))%9999}",nb,"monotone","MonotonePath", - ["monotone"],{},list(problem.variables),0.67)] + return [_make_hyp(f"mon_{hash(str(nb))%9999}",nb,"monotone","MonoPath",["monotone"],{},list(problem.variables),0.67)] -def _hyp_convex(problem, baton, all_batons, model): - """Convex combination of current binding and constraint projection.""" - hyps = []; b = dict(baton.binding) +def _hyp_convex(problem,baton,all_batons,model): + hyps=[]; b=dict(baton.binding) for mc in problem.compiled_constraints: if mc.kind!="equality" or not mc.projections: continue for v,projs in mc.projections.items(): - lo,hi = problem.bounds.get(v,(-1e18,1e18)) + lo,hi=problem.bounds.get(v,(-1e18,1e18)) for proj in projs: try: - val = float(proj["func"](*[b.get(s,0.0) for s in proj["syms"]])) + val=float(proj["func"](*[b.get(s,0.0) for s in proj["syms"]])) if not(lo<=val<=hi) or not math.isfinite(val): continue - nb = dict(b); nb[v] = 0.5*b[v]+0.5*val + nb=dict(b); nb[v]=0.5*b[v]+0.5*val hyps.append(_make_hyp(f"cvx_{hash(mc.expr_str)%9999}_{v}",nb,"convex", - f"ConvexMix({v}→{val:.3f})",["convex",mc.expr_str],{v:nb[v]}, + f"ConvMix({v}→{val:.3f})",["convex",mc.expr_str],{v:nb[v]}, [u for u in problem.variables if u!=v],0.63)) except: pass return hyps -# ── Physics ──────────────────────────────────────────────────────────── - -def _hyp_conserved(problem, baton, all_batons, model): - """Enforce conservation laws directly via projection.""" - hyps = []; b = dict(baton.binding) - cons_mcs = [mc for mc in problem.compiled_constraints if mc.kind=="equality" and mc.weight>=5.0] +def _hyp_conserved(problem,baton,all_batons,model): + hyps=[]; b=dict(baton.binding) + cons_mcs=[mc for mc in problem.compiled_constraints if mc.kind=="equality" and mc.weight>=5.0] for mc in cons_mcs: for v,projs in mc.projections.items(): - lo,hi = problem.bounds.get(v,(-1e18,1e18)) + lo,hi=problem.bounds.get(v,(-1e18,1e18)) for proj in projs: try: - val = float(proj["func"](*[b.get(s,0.0) for s in proj["syms"]])) + val=float(proj["func"](*[b.get(s,0.0) for s in proj["syms"]])) if not(lo<=val<=hi) or not math.isfinite(val): continue - nb = dict(b); nb[v]=val + nb=dict(b); nb[v]=val hyps.append(_make_hyp(f"csv_{hash(mc.expr_str)%9999}_{v}",nb,"conserved", f"Conserve({v}={val:.4f})",[mc.expr_str],{v:val}, [u for u in problem.variables if u!=v],0.82)) except: pass return hyps -def _hyp_mutable(problem, baton, all_batons, model): - """Gaussian perturbation of dominant residual variables.""" - hyps = []; l9 = baton.l9; b = dict(baton.binding) +def _hyp_mutable(problem,baton,all_batons,model): + hyps=[]; l9=baton.l9; b=dict(baton.binding) if not l9 or not l9.dominant_vars: return hyps for v in l9.dominant_vars[:3]: - lo,hi = problem.bounds.get(v,(-10,10)) + lo,hi=problem.bounds.get(v,(-10,10)) for _ in range(3): - noise = random.gauss(0,(hi-lo)*0.05) - val = max(lo,min(hi,b[v]+noise)) - nb = dict(b); nb[v]=val + noise=random.gauss(0,(hi-lo)*0.05); val=max(lo,min(hi,b[v]+noise)) + nb=dict(b); nb[v]=val hyps.append(_make_hyp(f"mut_{v}_{random.randint(0,9999)}",nb,"mutable", f"Perturb({v}±{noise:.4f})",["mutable",v],{},list(problem.variables),0.40)) return hyps -def _hyp_network(problem, baton, all_batons, model): - """Hub-and-spoke: propagate from most-connected variable.""" - vd = defaultdict(int) +def _hyp_network(problem,baton,all_batons,model): + vd=defaultdict(int) for mc in problem.compiled_constraints: for v in mc.syms_used: vd[v]+=1 if not vd: return [] - hub = max(vd,key=vd.get); b = dict(baton.binding) + hub=max(vd,key=vd.get); b=dict(baton.binding) for mc in problem.compiled_constraints: if hub not in mc.syms_used or hub not in mc.projections: continue - val = _proj_val(mc,hub,b) + val=_proj_val(mc,hub,b) if val is None: continue - lo,hi = problem.bounds.get(hub,(-1e18,1e18)) + lo,hi=problem.bounds.get(hub,(-1e18,1e18)) if lo<=val<=hi: b[hub]=val; break return [_make_hyp(f"net_{hub}_{hash(str(b))%9999}",b,"network", - f"HubProp({hub},deg={vd[hub]})",["network",hub],{hub:b[hub]}, - [v for v in problem.variables if v!=hub],0.65)] - -def _hyp_equilibrium(problem, baton, all_batons, model): - """Find gradient balance point — opposing forces cancel.""" - b = dict(baton.binding); grad = problem.evaluate_gradient(b) - gms = sum(g**2 for g in grad.values()) - if gms < 1e-12: return [] - lr = min(0.15, baton.ce/(gms+1e-8)) - nb = {v:max(problem.bounds[v][0],min(problem.bounds[v][1],b[v]-lr*grad[v])) - for v in problem.variables} + f"HubProp({hub})",["network",hub],{hub:b[hub]},[v for v in problem.variables if v!=hub],0.65)] + +def _hyp_equilibrium(problem,baton,all_batons,model): + b=dict(baton.binding); grad=problem.evaluate_gradient(b) + gms=sum(g**2 for g in grad.values()) + if gms<1e-12: return [] + lr=min(0.15,baton.ce/(gms+1e-8)) + nb={v:max(problem.bounds[v][0],min(problem.bounds[v][1],b[v]-lr*grad[v])) for v in problem.variables} return [_make_hyp(f"eql_{hash(str(nb))%9999}",nb,"equilibrium", - f"GradBalance(lr={lr:.4f})",["equilibrium"],{},list(problem.variables),0.72)] + f"GradBal(lr={lr:.4f})",["equilibrium"],{},list(problem.variables),0.72)] -def _hyp_superposition(problem, baton, all_batons, model): - """Linear combinations of inherited batons from parent rays.""" - hyps = []; recent = [bt for bt in all_batons[-8:] if bt.ce < float('inf') and bt.binding] +def _hyp_superposition(problem,baton,all_batons,model): + hyps=[]; recent=[bt for bt in all_batons[-8:] if bt.ce1e-6: - nb[v]=val; changed=True + lo,hi=problem.bounds.get(v,(-1e18,1e18)) + if lo<=val<=hi and abs(val-nb.get(v,0))>1e-6: nb[v]=val; changed=True if nb==b: return [] - pinned = {v:nb[v] for v in nb if abs(nb[v]-b.get(v,0))>1e-4} + pinned={v:nb[v] for v in nb if abs(nb[v]-b.get(v,0))>1e-4} return [_make_hyp(f"tra_{hash(str(nb))%9999}",nb,"transitive", - f"TransitiveSnap({iters}iters)",["transitive"],pinned, + f"TransSnap({iters})",["transitive"],pinned, [v for v in problem.variables if v not in pinned],0.77)] -def _hyp_atomic(problem, baton, all_batons, model): - """Solve a single most-violated constraint; ignore the rest.""" - b = dict(baton.binding); worst_mc=None; worst_val=0.0 +def _hyp_atomic(problem,baton,all_batons,model): + b=dict(baton.binding); worst_mc=None; worst_val=0.0 for mc in problem.compiled_constraints: if mc.fast_pt is None: continue try: - val = abs(float(mc.fast_pt(*[b.get(v,0.0) for v in mc.syms_used]))) + val=abs(float(mc.fast_pt(*[b.get(v,0.0) for v in mc.syms_used]))) if val>worst_val: worst_val=val; worst_mc=mc except: pass if not worst_mc or not worst_mc.projections: return [] - hyps = [] + hyps=[] for v,projs in worst_mc.projections.items(): - lo,hi = problem.bounds.get(v,(-1e18,1e18)) + lo,hi=problem.bounds.get(v,(-1e18,1e18)) for proj in projs: try: - val = float(proj["func"](*[b.get(s,0.0) for s in proj["syms"]])) + val=float(proj["func"](*[b.get(s,0.0) for s in proj["syms"]])) if not(lo<=val<=hi) or not math.isfinite(val): continue - nb = dict(b); nb[v]=val + nb=dict(b); nb[v]=val hyps.append(_make_hyp(f"ato_{hash(worst_mc.expr_str)%9999}_{v}",nb,"atomic", - f"SolveOne({worst_mc.expr_str[:20]}→{v}={val:.4f})",[worst_mc.expr_str], - {v:val},[u for u in problem.variables if u!=v],0.70)) + f"SolveOne({v}={val:.4f})",[worst_mc.expr_str],{v:val}, + [u for u in problem.variables if u!=v],0.70)) except: pass return hyps -def _hyp_implication(problem, baton, all_batons, model): - """Pin a dominant variable, propagate implications through HC4.""" - hyps = []; l9 = baton.l9; b = dict(baton.binding) +def _hyp_implication(problem,baton,all_batons,model): + hyps=[]; l9=baton.l9; b=dict(baton.binding) if not l9 or not l9.dominant_vars: return hyps - tb = _global_hc4_tighten(problem) + tb=_global_hc4_tighten(problem) for v in l9.dominant_vars[:2]: - val = b.get(v,(problem.bounds[v][0]+problem.bounds[v][1])/2) - box = {u:IV(*tb.get(u,problem.bounds.get(u,(-10,10)))) for u in problem.variables} - box[v] = IV(val-1e-4,val+1e-4) - contracted = _hc4(box,problem.compiled_constraints) + val=b.get(v,(problem.bounds[v][0]+problem.bounds[v][1])/2) + box={u:IV(*tb.get(u,problem.bounds.get(u,(-10,10)))) for u in problem.variables} + box[v]=IV(val-1e-4,val+1e-4) + contracted=_hc4(box,problem.compiled_constraints) if not contracted: continue - nb = {u:contracted[u].mid() for u in problem.variables} - pinned = {u:nb[u] for u in problem.variables if contracted[u].width()<1e-2} + nb={u:contracted[u].mid() for u in problem.variables} + pinned={u:nb[u] for u in problem.variables if contracted[u].width()<1e-2} hyps.append(_make_hyp(f"imp_{v}_{hash(str(nb))%9999}",nb,"implication", - f"Imply({v}={val:.3f}→HC4)",["implication",v],pinned, + f"Imply({v}→HC4)",["implication",v],pinned, [u for u in problem.variables if u not in pinned],0.78)) return hyps -def _hyp_negation(problem, baton, all_batons, model): - """Mirror current binding through the centre of variable bounds.""" - nb = {} +def _hyp_negation(problem,baton,all_batons,model): + nb={} for v in problem.variables: - lo,hi = problem.bounds[v]; mid=(lo+hi)/2 - nb[v] = max(lo,min(hi,2*mid-baton.binding.get(v,mid))) - return [_make_hyp(f"neg_{hash(str(nb))%9999}",nb,"negation","MirrorBounds", - ["negation"],{},list(problem.variables),0.42)] - -# ── Philosophy ───────────────────────────────────────────────────────── + lo,hi=problem.bounds[v]; mid=(lo+hi)/2 + nb[v]=max(lo,min(hi,2*mid-baton.binding.get(v,mid))) + return [_make_hyp(f"neg_{hash(str(nb))%9999}",nb,"negation","Mirror",["negation"],{},list(problem.variables),0.42)] -def _hyp_composite(problem, baton, all_batons, model): - """Enzyme: pin branch value, cascade HC4 (Practicality 12.1 enzyme).""" - hyps = []; l9 = baton.l9 +def _hyp_composite(problem,baton,all_batons,model): + hyps=[]; l9=baton.l9 if not l9: return hyps - ref = baton.binding; tb = _global_hc4_tighten(problem) + ref=baton.binding; tb=_global_hc4_tighten(problem) for expr_str in l9.dominant_exprs[:3]: - mc = next((mc for mc in problem.compiled_constraints if mc.expr_str==expr_str),None) + mc=next((mc for mc in problem.compiled_constraints if mc.expr_str==expr_str),None) if not mc or not mc.projections: continue for v,proj_list in mc.projections.items(): - lo,hi = problem.bounds.get(v,(-1e18,1e18)) + lo,hi=problem.bounds.get(v,(-1e18,1e18)) for pi,proj in enumerate(proj_list): try: - val = float(proj["func"](*[ref.get(s,0.0) for s in proj["syms"]])) + val=float(proj["func"](*[ref.get(s,0.0) for s in proj["syms"]])) if not math.isfinite(val) or abs(val)>1e6 or not(lo<=val<=hi): continue - box = {u:IV(*tb.get(u,problem.bounds.get(u,(-10,10)))) for u in problem.variables} - box[v] = IV(val-1e-6,val+1e-6) - cont = _hc4(box,problem.compiled_constraints) + box={u:IV(*tb.get(u,problem.bounds.get(u,(-10,10)))) for u in problem.variables} + box[v]=IV(val-1e-6,val+1e-6) + cont=_hc4(box,problem.compiled_constraints) if not cont: continue - b = dict(ref) + b=dict(ref) for u,iv in cont.items(): b[u]=iv.mid() - pinned = {u:b[u] for u in problem.variables if cont[u].width()<1e-2} + pinned={u:b[u] for u in problem.variables if cont[u].width()<1e-2} hyps.append(_make_hyp(f"cmp_{hash(expr_str)%9999}_{v}_{pi}",b,"composite", - f"Enz(Br({v})→Chain)",[expr_str,"hc4_chain"],pinned, + f"Enz({v}→Chain)",[expr_str,"hc4"],pinned, [u for u in problem.variables if u not in pinned],0.90 if pi==0 else 0.80)) except: pass return hyps -def _hyp_holism(problem, baton, all_batons, model): - """Single global gradient step treating all constraints simultaneously.""" - b = dict(baton.binding); grad = problem.evaluate_gradient(b) - gms = sum(g**2 for g in grad.values()) - if gms < 1e-12: return [] - lr = min(0.5,baton.ce/(gms+1e-8)) - nb = {v:max(problem.bounds[v][0],min(problem.bounds[v][1],b[v]-lr*grad[v])) - for v in problem.variables} +def _hyp_holism(problem,baton,all_batons,model): + b=dict(baton.binding); grad=problem.evaluate_gradient(b) + gms=sum(g**2 for g in grad.values()) + if gms<1e-12: return [] + lr=min(0.5,baton.ce/(gms+1e-8)) + nb={v:max(problem.bounds[v][0],min(problem.bounds[v][1],b[v]-lr*grad[v])) for v in problem.variables} return [_make_hyp(f"hol_{hash(str(nb))%9999}",nb,"holism", - f"GlobalStep(lr={lr:.4f})",["holism"],{},list(problem.variables),0.73)] + f"Global(lr={lr:.4f})",["holism"],{},list(problem.variables),0.73)] -def _hyp_parsimony(problem, baton, all_batons, model): - """Occam: simplest (integer / half-integer) values.""" - b = dict(baton.binding); nb = {} +def _hyp_parsimony(problem,baton,all_batons,model): + b=dict(baton.binding); nb={} for v in problem.variables: - lo,hi = problem.bounds[v]; candidates = [] + lo,hi=problem.bounds[v]; candidates=[] for mult in [1,2,4]: - r = round(b[v]*mult)/mult + r=round(b[v]*mult)/mult if lo<=r<=hi: candidates.append(r) - nb[v] = min(candidates,key=lambda c:abs(c-b[v])) if candidates else b[v] - return [_make_hyp(f"par_{hash(str(nb))%9999}",nb,"parsimony","Occam(round)", - ["parsimony"],{},list(problem.variables),0.58)] + nb[v]=min(candidates,key=lambda c:abs(c-b[v])) if candidates else b[v] + return [_make_hyp(f"par_{hash(str(nb))%9999}",nb,"parsimony","Occam",["parsimony"],{},list(problem.variables),0.58)] -def _hyp_duality(problem, baton, all_batons, model): - """Dual: make each inequality constraint exactly tight.""" - hyps = []; b = dict(baton.binding) +def _hyp_duality(problem,baton,all_batons,model): + hyps=[]; b=dict(baton.binding) for mc in problem.compiled_constraints: if mc.kind!="inequality" or not mc.projections: continue for v,projs in mc.projections.items(): - lo,hi = problem.bounds.get(v,(-1e18,1e18)) + lo,hi=problem.bounds.get(v,(-1e18,1e18)) for proj in projs: try: - val = float(proj["func"](*[b.get(s,0.0) for s in proj["syms"]])) + val=float(proj["func"](*[b.get(s,0.0) for s in proj["syms"]])) if not(lo<=val<=hi) or not math.isfinite(val): continue - nb = dict(b); nb[v]=val + nb=dict(b); nb[v]=val hyps.append(_make_hyp(f"dua_{hash(mc.expr_str)%9999}_{v}",nb,"duality", - f"DualTight({v}∈{mc.expr_str[:18]})",["duality",mc.expr_str],{v:val}, + f"Tight({v})",["duality",mc.expr_str],{v:val}, [u for u in problem.variables if u!=v],0.68)) break except: pass return hyps -# Registry: axiom string → constructor function -AXIOM_CONSTRUCTORS: Dict[str, Callable] = { - Axiom.CONTINUOUS: _hyp_continuous, - Axiom.DISCRETE: _hyp_discrete, - Axiom.QUADRATIC: _hyp_quadratic, - Axiom.BILINEAR: _hyp_bilinear, - Axiom.METRIC: _hyp_metric, - Axiom.SYMMETRIC: _hyp_symmetric, - Axiom.ORDERED: _hyp_ordered, - Axiom.MONOTONE: _hyp_monotone, - Axiom.CONVEX: _hyp_convex, - Axiom.CONSERVED: _hyp_conserved, - Axiom.MUTABLE: _hyp_mutable, - Axiom.NETWORK: _hyp_network, - Axiom.EQUILIBRIUM: _hyp_equilibrium, - Axiom.SUPERPOSITION: _hyp_superposition, - Axiom.LOCALITY: _hyp_locality, - Axiom.EXTREMAL: _hyp_extremal, - Axiom.ENTROPY: _hyp_entropy, - Axiom.INJECTIVE: _hyp_injective, - Axiom.SURJECTIVE: _hyp_surjective, - Axiom.TRANSITIVE: _hyp_transitive, - Axiom.ATOMIC: _hyp_atomic, - Axiom.IMPLICATION: _hyp_implication, - Axiom.NEGATION: _hyp_negation, - Axiom.COMPOSITE: _hyp_composite, - Axiom.HOLISM: _hyp_holism, - Axiom.PARSIMONY: _hyp_parsimony, - Axiom.DUALITY: _hyp_duality, +AXIOM_CONSTRUCTORS:Dict[str,Callable]={ + Axiom.CONTINUOUS:_hyp_continuous,Axiom.DISCRETE:_hyp_discrete, + Axiom.QUADRATIC:_hyp_quadratic,Axiom.BILINEAR:_hyp_bilinear, + Axiom.METRIC:_hyp_metric,Axiom.SYMMETRIC:_hyp_symmetric, + Axiom.ORDERED:_hyp_ordered,Axiom.MONOTONE:_hyp_monotone,Axiom.CONVEX:_hyp_convex, + Axiom.CONSERVED:_hyp_conserved,Axiom.MUTABLE:_hyp_mutable,Axiom.NETWORK:_hyp_network, + Axiom.EQUILIBRIUM:_hyp_equilibrium,Axiom.SUPERPOSITION:_hyp_superposition, + Axiom.LOCALITY:_hyp_locality,Axiom.EXTREMAL:_hyp_extremal,Axiom.ENTROPY:_hyp_entropy, + Axiom.INJECTIVE:_hyp_injective,Axiom.SURJECTIVE:_hyp_surjective, + Axiom.TRANSITIVE:_hyp_transitive,Axiom.ATOMIC:_hyp_atomic, + Axiom.IMPLICATION:_hyp_implication,Axiom.NEGATION:_hyp_negation, + Axiom.COMPOSITE:_hyp_composite,Axiom.HOLISM:_hyp_holism, + Axiom.PARSIMONY:_hyp_parsimony,Axiom.DUALITY:_hyp_duality, } # ══════════════════════════════════════════════════════════════════════ -# SECTION 12: SEQUENCE HYPOTHESIS GENERATOR -# Processes the axiom sequence of a ray in order. -# Each axiom adds hypotheses; the best result updates the baton for -# the next axiom in the sequence. The chain earns its own direction. +# SECTION 12: SEQUENCE HYPOTHESIS GENERATOR + RAY TRACER # ══════════════════════════════════════════════════════════════════════ class SequenceHypothesisGenerator: - def generate(self, sequence: List[str], problem: Problem, - baton: Baton, all_batons: List[Baton], - model: StructuralModel) -> Tuple[List[Hypothesis], Baton]: - accumulated: List[Hypothesis] = [] - current = baton - - for i, axiom in enumerate(sequence): - constructor = AXIOM_CONSTRUCTORS.get(axiom) - if not constructor: - continue - - # Lazily enrich baton with oracle context + def generate(self,sequence:List[str],problem:Problem, + baton:Baton,all_batons:List[Baton],model:StructuralModel) -> Tuple[List[Hypothesis],Baton]: + accumulated:List[Hypothesis]=[]; current=baton + for i,axiom in enumerate(sequence): + constructor=AXIOM_CONSTRUCTORS.get(axiom) + if not constructor: continue if current.l7 is None: - active = [s for s in problem.scope_order if s!="root" and problem.scope_vars.get(s)] - current.l7 = TOPOLOGY_ORACLE.evaluate(problem, active) + active=[s for s in problem.scope_order if s!="root" and problem.scope_vars.get(s)] + current.l7=TOPOLOGY_ORACLE.evaluate(problem,active) if current.l9 is None: - hubs = current.l7.hub_vars if current.l7 else [] - current.l9 = RESIDUAL_ORACLE.evaluate(current.binding, problem, hubs) - - new_hyps = constructor(problem, current, all_batons, model) + hubs=current.l7.hub_vars if current.l7 else [] + current.l9=RESIDUAL_ORACLE.evaluate(current.binding,problem,hubs) + new_hyps=constructor(problem,current,all_batons,model) accumulated.extend(new_hyps) - - # Test top hypotheses; best result becomes context for next axiom - best_ce = current.ce - best_b = current.binding - for hyp in sorted(new_hyps, key=lambda h: -h.confidence)[:MAX_HYPS_PER_AXIOM]: + best_ce=current.ce; best_b=current.binding + for hyp in sorted(new_hyps,key=lambda h:-h.confidence)[:MAX_HYPS_PER_AXIOM]: if hyp.hid in model.failure_patterns: continue - tb, tce = _test_hypothesis(problem, hyp) - if tce < best_ce: - best_ce = tce; best_b = tb - - if best_ce < current.ce: - current = Baton(binding=best_b, ce=best_ce, - ray_id=current.ray_id, depth=i+1, - l7=None, l9=None) # recomputed next iteration + tb,tce=_test_hypothesis(problem,hyp) + if tce Tuple[Dict,float,List[Dict]]: + all_traces:List[HypothesisTrace]=[]; generator=SequenceHypothesisGenerator() + active=[AxiomRay(sequence=[a],ray_id=f"S{i}",depth=0) for i,a in enumerate(ALL_AXIOMS)] + random.shuffle(active) + all_batons:List[Baton]=[]; best_ce=float('inf'); best_binding:Dict={}; history:List[Dict]=[] + total_fired=0 + + init_b={v:(lo+hi)/2 for v,(lo,hi) in base_problem.bounds.items()} + init_ce=base_problem.constraint_energy(init_b) + snap_b,snap_ce=_algebraic_snap(base_problem,init_b) + if snap_ce List[AxiomRay]: - remaining = [a for a in ALL_AXIOMS if a not in ray.sequence] - random.shuffle(remaining) # no ordering bias in child selection - children: List[AxiomRay] = [] - for axiom in remaining: - child = ray.extend(axiom) - if child: - child.baton = baton - children.append(child) - if len(children) >= self.BRANCH_WIDTH * 2: - break - return children + remaining=[a for a in ALL_AXIOMS if a not in ray.sequence] + random.shuffle(remaining); children=[] + for axiom in remaining: + child=ray.extend(axiom) + if child: child.baton=output_baton; children.append(child) + if len(children)>=self.BRANCH_WIDTH*2: break + active=children+active + + self._last_traces=all_traces + return best_binding,best_ce,history # ══════════════════════════════════════════════════════════════════════ -# SECTION 14: HARDCODED AXL PROBLEMS (unchanged from 12.1) +# SECTION 13: REAL-WORLD AXL PROBLEMS (14 across 11 domains) # ══════════════════════════════════════════════════════════════════════ + +# Domain metadata +PROBLEM_META={ + "EllipticCurvePoint": {"domain":"Cryptography", "icon":"🔐","difficulty":"Medium"}, + "MarkowitzPortfolio": {"domain":"Finance", "icon":"📈","difficulty":"Hard"}, + "PowerFlowDC3Bus": {"domain":"Energy Systems", "icon":"⚡","difficulty":"Medium"}, + "ChemEquilibrium": {"domain":"Chemistry", "icon":"⚗","difficulty":"Medium"}, + "LorenzFixedPoint": {"domain":"Chaos Theory", "icon":"🌀","difficulty":"Easy"}, + "NashBattleSexes": {"domain":"Game Theory", "icon":"🎲","difficulty":"Easy"}, + "KeplerPeriapsis": {"domain":"Astronomy", "icon":"🪐","difficulty":"Medium"}, + "VibratingString3": {"domain":"Structural Eng", "icon":"🏗","difficulty":"Easy"}, + "SignalRecovery4": {"domain":"Signal Proc", "icon":"📡","difficulty":"Medium"}, + "RobotArm2D": {"domain":"Robotics", "icon":"🦾","difficulty":"Hard"}, + "NormManifold4D": {"domain":"Mathematics", "icon":"📐","difficulty":"Medium"}, + "BilinearChain6": {"domain":"Mathematics", "icon":"📐","difficulty":"Hard"}, + "PhaseCollider": {"domain":"Physics", "icon":"⚛","difficulty":"Medium"}, + "MetricPacking3D": {"domain":"Combinatorics", "icon":"🎯","difficulty":"Hard"}, +} + AXL_PROBLEMS=[ - AXLProblemDef( - name="NormManifold4D", - description="4 vars on unit sphere, zero sum, x1 observed at 0.5", - axioms={Axiom.CONTINUOUS,Axiom.QUADRATIC,Axiom.CONSERVED,Axiom.METRIC,Axiom.SYMMETRIC}, - variables=[ - {"name":"x1","lo":-1.0,"hi":1.0}, {"name":"x2","lo":-1.0,"hi":1.0}, - {"name":"x3","lo":-1.0,"hi":1.0}, {"name":"x4","lo":-1.0,"hi":1.0}, - ], - constraints=[ - {"kind":"CONSERVE","expr":"x1**2 + x2**2 + x3**2 + x4**2 - 1.0"}, - {"kind":"EQ","expr":"x1 + x2 + x3 + x4","weight":2.0}, - ], - scopes=[{"name":"sphere","order":0,"vars":["x1","x2","x3","x4"], - "constraints":[{"kind":"EQ","expr":"x1**2 + x2**2 + x3**2 + x4**2 - 1.0","weight":5.0}]}], - anchors=[ - AXLInvariant("unit_sphere","x1**2 + x2**2 + x3**2 + x4**2 - 1.0",1e-3), - AXLInvariant("zero_sum","x1 + x2 + x3 + x4",1e-3), - AXLInvariant("x1_pinned","x1 - 0.5",1e-3), - ], - observations={"x1":0.5}, - ), - AXLProblemDef( - name="BilinearChain6", - description="6-var ordered chain with bilinear products and sum conservation", - axioms={Axiom.DISCRETE,Axiom.ORDERED,Axiom.BILINEAR,Axiom.CONSERVED,Axiom.NETWORK}, - variables=[{"name":f"t{i}","lo":0.0,"hi":3.0} for i in range(1,7)], - constraints=[ - {"kind":"CONSERVE","expr":"t1 + t2 + t3 + t4 + t5 + t6 - 9.0"}, - {"kind":"GEQ","expr":"t2 - t1","weight":1.0}, {"kind":"GEQ","expr":"t3 - t2","weight":1.0}, - {"kind":"GEQ","expr":"t4 - t3","weight":1.0}, {"kind":"GEQ","expr":"t5 - t4","weight":1.0}, - {"kind":"GEQ","expr":"t6 - t5","weight":1.0}, - ], - scopes=[{"name":"chain","order":0,"vars":[f"t{i}" for i in range(1,7)], - "constraints":[ - {"kind":"EQ","expr":"t1*t2 - 0.5","weight":2.0}, - {"kind":"EQ","expr":"t3*t4 - 2.0","weight":2.0}, - {"kind":"EQ","expr":"t5*t6 - 4.5","weight":2.0}, - ]}], - anchors=[ - AXLInvariant("conservation","t1 + t2 + t3 + t4 + t5 + t6 - 9.0",1e-3), - AXLInvariant("bilinear_lo","t1*t2 - 0.5",0.05), - AXLInvariant("bilinear_mid","t3*t4 - 2.0",0.05), - AXLInvariant("bilinear_hi","t5*t6 - 4.5",0.05), - ], - ), - AXLProblemDef( - name="PhaseCollider", - description="2-particle symmetric collision: conservation + phase branch", - axioms={Axiom.DISCRETE,Axiom.MUTABLE,Axiom.SYMMETRIC,Axiom.NETWORK,Axiom.CONSERVED}, - variables=[ - {"name":"p1x","lo":-2.0,"hi":2.0}, {"name":"p2x","lo":-2.0,"hi":2.0}, - {"name":"p1y","lo":-2.0,"hi":2.0}, {"name":"p2y","lo":-2.0,"hi":2.0}, - ], - constraints=[ - {"kind":"CONSERVE","expr":"p1x + p2x"}, {"kind":"CONSERVE","expr":"p1y + p2y"}, - ], - scopes=[{"name":"phase","order":0,"vars":["p1x","p2x","p1y","p2y"], - "constraints":[ - {"kind":"BRANCH","name":"phase_select","options":[ - "p1x**2 + p1y**2 - 0.25", "p1x**2 + p1y**2 - 1.0", - ]}, - {"kind":"EQ","expr":"p1x + p2x","weight":3.0}, - {"kind":"EQ","expr":"p1y + p2y","weight":3.0}, - ]}], - anchors=[ - AXLInvariant("momentum_x","p1x + p2x",1e-3), - AXLInvariant("momentum_y","p1y + p2y",1e-3), - AXLInvariant("phase_A_or_B","(p1x**2 + p1y**2 - 0.25)*(p1x**2 + p1y**2 - 1.0)",0.05), - ], - ), - AXLProblemDef( - name="MetricPacking3D", - description="3 vars packed with min separation, centred, norm=6", - axioms={Axiom.CONTINUOUS,Axiom.METRIC,Axiom.INJECTIVE,Axiom.CONSERVED,Axiom.SYMMETRIC}, - variables=[ - {"name":"a","lo":-3.0,"hi":3.0}, {"name":"b","lo":-3.0,"hi":3.0}, - {"name":"c","lo":-3.0,"hi":3.0}, - ], - constraints=[ - {"kind":"CONSERVE","expr":"a + b + c"}, - {"kind":"GEQ","expr":"(a - b)**2 - 1.0","weight":2.0}, - {"kind":"GEQ","expr":"(b - c)**2 - 1.0","weight":2.0}, - {"kind":"GEQ","expr":"(a - c)**2 - 4.0","weight":2.0}, - ], - scopes=[{"name":"packing","order":0,"vars":["a","b","c"], - "constraints":[{"kind":"EQ","expr":"a**2 + b**2 + c**2 - 6.0","weight":2.0}]}], - anchors=[ - AXLInvariant("centred","a + b + c",1e-3), - AXLInvariant("sep_ab","(a - b)**2 - 1.0",0.5), - AXLInvariant("sep_bc","(b - c)**2 - 1.0",0.5), - AXLInvariant("norm_6","a**2 + b**2 + c**2 - 6.0",0.05), - ], - ), -] -def build_base_problem(axl_def: AXLProblemDef) -> Problem: - psl_text = AXL_COMPILER.compile(axl_def) - prog = parse_psl(psl_text); ep = expand_psl(prog) - return Problem(pid=f"base_{axl_def.name}", variables=ep.variables, - constraints=ep.constraints, bounds=ep.bounds, - scope_groups=ep.scope_groups, scope_vars=ep.scope_vars, - scope_order=ep.scope_order, annotations=ep.annotations) +# ── CRYPTOGRAPHY ────────────────────────────────────────────────────── +AXLProblemDef( + name="EllipticCurvePoint", + description="Find point on E: y²=x³-x+1 (Weierstrass). Observe x=0, find y=±1.", + axioms={Axiom.CONTINUOUS,Axiom.QUADRATIC,Axiom.METRIC,Axiom.SYMMETRIC}, + variables=[{"name":"ex","lo":-2.0,"hi":2.0},{"name":"ey","lo":-2.0,"hi":2.0}], + constraints=[ + # y² - x³ + x - 1 = 0 → ey**2 - ex**3 + ex - 1 = 0 + {"kind":"EQ","expr":"ey**2 - ex**3 + ex - 1","weight":5.0}, + ], + scopes=[{"name":"curve","order":0,"vars":["ex","ey"], + "constraints":[{"kind":"EQ","expr":"ey**2 - ex**3 + ex - 1","weight":8.0}]}], + anchors=[AXLInvariant("on_curve","ey**2 - ex**3 + ex - 1",1e-3)], + observations={"ex":0.0}, # x=0 → y=±1 +), + +# ── FINANCE ─────────────────────────────────────────────────────────── +AXLProblemDef( + name="MarkowitzPortfolio", + description="4-asset portfolio: budget=1, return=11%, minimize variance. " + "μ=[10,12,8,15]%, σ²=[4,9,1,16]%.", + axioms={Axiom.CONSERVED,Axiom.ORDERED,Axiom.METRIC,Axiom.HOLISM}, + variables=[ + {"name":"w1","lo":0.0,"hi":1.0},{"name":"w2","lo":0.0,"hi":1.0}, + {"name":"w3","lo":0.0,"hi":1.0},{"name":"w4","lo":0.0,"hi":1.0}, + ], + constraints=[ + {"kind":"CONSERVE","expr":"w1 + w2 + w3 + w4 - 1.0"}, + {"kind":"EQ","expr":"0.10*w1 + 0.12*w2 + 0.08*w3 + 0.15*w4 - 0.11","weight":3.0}, + {"kind":"GEQ","expr":"w1","weight":1.0},{"kind":"GEQ","expr":"w2","weight":1.0}, + {"kind":"GEQ","expr":"w3","weight":1.0},{"kind":"GEQ","expr":"w4","weight":1.0}, + ], + scopes=[{"name":"portfolio","order":0,"vars":["w1","w2","w3","w4"], + "constraints":[ + # Minimize variance (soft TEND toward low-variance asset 3) + {"kind":"EQ","expr":"w1 + w2 + w3 + w4 - 1.0","weight":5.0}, + {"kind":"EQ","expr":"0.10*w1 + 0.12*w2 + 0.08*w3 + 0.15*w4 - 0.11","weight":3.0}, + ]}], + anchors=[ + AXLInvariant("budget","w1+w2+w3+w4-1.0",1e-3), + AXLInvariant("return_target","0.10*w1+0.12*w2+0.08*w3+0.15*w4-0.11",5e-3), + AXLInvariant("w1_positive","w1",1e-3,"geq"), + AXLInvariant("w2_positive","w2",1e-3,"geq"), + AXLInvariant("w3_positive","w3",1e-3,"geq"), + AXLInvariant("w4_positive","w4",1e-3,"geq"), + ], + # Many valid solutions: e.g. w1=w2=w3≈0.267, w4≈0.200 +), + +# ── ENERGY SYSTEMS ──────────────────────────────────────────────────── +AXLProblemDef( + name="PowerFlowDC3Bus", + description="DC power flow: 3-bus network, B12=2, B13=3, B23=1. " + "θ1=0 (ref), Pg1=0.5. Find θ2≈-0.318, θ3≈0.046.", + axioms={Axiom.CONSERVED,Axiom.NETWORK,Axiom.EQUILIBRIUM,Axiom.ORDERED}, + variables=[ + {"name":"pt2","lo":-1.0,"hi":0.5}, + {"name":"pt3","lo":-0.5,"hi":0.5}, + ], + constraints=[ + # Bus 1: -2*θ2 - 3*θ3 = 0.5 (Pg1=0.5) + {"kind":"EQ","expr":"-2*pt2 - 3*pt3 - 0.5","weight":5.0}, + # Bus 2: 3*θ2 - θ3 = -1.0 (Pd2=1.0) + {"kind":"EQ","expr":"3*pt2 - pt3 + 1.0","weight":5.0}, + ], + scopes=[{"name":"power","order":0,"vars":["pt2","pt3"], + "constraints":[ + {"kind":"EQ","expr":"-2*pt2 - 3*pt3 - 0.5","weight":5.0}, + {"kind":"EQ","expr":"3*pt2 - pt3 + 1.0","weight":5.0}, + ]}], + anchors=[ + AXLInvariant("bus1_balance","-2*pt2 - 3*pt3 - 0.5",1e-3), + AXLInvariant("bus2_balance","3*pt2 - pt3 + 1.0",1e-3), + ], + # Known: pt2 = -7/22 ≈ -0.3182, pt3 = 1/22 ≈ 0.0455 +), + +# ── CHEMISTRY ──────────────────────────────────────────────────────── +AXLProblemDef( + name="ChemEquilibrium", + description="A+B↔C equilibrium, Kc=4. " + "Initial [A]=[B]=1, [C]=0. Solve: ca=cb≈0.390, cc≈0.610.", + axioms={Axiom.CONSERVED,Axiom.BILINEAR,Axiom.CONTINUOUS,Axiom.MONOTONE}, + variables=[ + {"name":"ca","lo":0.0,"hi":1.0}, + {"name":"cb","lo":0.0,"hi":1.0}, + {"name":"cc","lo":0.0,"hi":1.0}, + ], + constraints=[ + {"kind":"CONSERVE","expr":"ca + cc - 1.0"}, # A atom balance + {"kind":"CONSERVE","expr":"cb + cc - 1.0"}, # B atom balance + {"kind":"EQ","expr":"4*ca*cb - cc","weight":5.0}, # Kc=4: cc=Kc*ca*cb + ], + scopes=[{"name":"equilibrium","order":0,"vars":["ca","cb","cc"], + "constraints":[ + {"kind":"EQ","expr":"ca - cb","weight":3.0}, # stoichiometry: ca=cb + {"kind":"EQ","expr":"4*ca*cb - cc","weight":5.0}, + ]}], + anchors=[ + AXLInvariant("balance_A","ca+cc-1.0",1e-3), + AXLInvariant("balance_B","cb+cc-1.0",1e-3), + AXLInvariant("equilibrium","4*ca*cb - cc",1e-3), + ], + # Known: ca=cb=(-1+√17)/8≈0.3904, cc≈0.6096 +), + +# ── CHAOS THEORY ───────────────────────────────────────────────────── +AXLProblemDef( + name="LorenzFixedPoint", + description="Lorenz σ=10,ρ=28,β=8/3. Non-origin fixed point: " + "x=y, z=27, x²=72. Solution: (±8.485, ±8.485, 27).", + axioms={Axiom.CONTINUOUS,Axiom.QUADRATIC,Axiom.SYMMETRIC,Axiom.CONSERVED}, + variables=[ + {"name":"lx","lo":-12.0,"hi":12.0}, + {"name":"ly","lo":-12.0,"hi":12.0}, + {"name":"lz","lo":20.0,"hi":35.0}, + ], + constraints=[ + {"kind":"EQ","expr":"lx - ly","weight":5.0}, # x=y (from σ(y-x)=0) + {"kind":"EQ","expr":"lz - 27.0","weight":5.0}, # z=ρ-1=27 + {"kind":"EQ","expr":"lx**2 - 72.0","weight":5.0}, # x²=β(ρ-1)=8/3*27=72 + ], + scopes=[{"name":"lorenz","order":0,"vars":["lx","ly","lz"], + "constraints":[ + {"kind":"EQ","expr":"lx - ly","weight":5.0}, + {"kind":"EQ","expr":"lz - 27.0","weight":5.0}, + {"kind":"EQ","expr":"lx**2 - 72.0","weight":5.0}, + ]}], + anchors=[ + AXLInvariant("x_equals_y","lx-ly",1e-3), + AXLInvariant("z_is_27","lz-27.0",1e-3), + AXLInvariant("x_squared_72","lx**2-72.0",0.1), + ], +), + +# ── GAME THEORY ────────────────────────────────────────────────────── +AXLProblemDef( + name="NashBattleSexes", + description="Battle of Sexes 2x2 game. Mixed Nash: p=2/3 (P1 Opera), q=1/3 (P2 Opera).", + axioms={Axiom.CONTINUOUS,Axiom.SYMMETRIC,Axiom.CONSERVED,Axiom.ORDERED}, + variables=[ + {"name":"np","lo":0.0,"hi":1.0}, # P1 prob choosing Opera + {"name":"nq","lo":0.0,"hi":1.0}, # P2 prob choosing Opera + ], + constraints=[ + {"kind":"EQ","expr":"3*nq - 1.0","weight":5.0}, # P1 indifference: q=1/3 + {"kind":"EQ","expr":"3*np - 2.0","weight":5.0}, # P2 indifference: p=2/3 + ], + scopes=[{"name":"nash","order":0,"vars":["np","nq"], + "constraints":[ + {"kind":"EQ","expr":"3*nq - 1.0","weight":5.0}, + {"kind":"EQ","expr":"3*np - 2.0","weight":5.0}, + ]}], + anchors=[ + AXLInvariant("p1_indiff","3*nq-1.0",1e-3), + AXLInvariant("p2_indiff","3*np-2.0",1e-3), + ], + # Known: np=2/3≈0.6667, nq=1/3≈0.3333 +), + +# ── ASTRONOMY ──────────────────────────────────────────���────────────── +AXLProblemDef( + name="KeplerPeriapsis", + description="Orbital mechanics at periapsis. GM=1 units. a=1, e=0.5 observed. " + "Find rp=0.5, vp=√3≈1.732, h≈0.866.", + axioms={Axiom.CONTINUOUS,Axiom.QUADRATIC,Axiom.CONSERVED,Axiom.METRIC}, + variables=[ + {"name":"ka","lo":0.5,"hi":2.0}, # semi-major axis + {"name":"ke","lo":0.0,"hi":0.99}, # eccentricity + {"name":"krp","lo":0.1,"hi":2.0}, # periapsis radius + {"name":"kvp","lo":0.5,"hi":5.0}, # periapsis speed + {"name":"kh","lo":0.1,"hi":3.0}, # specific angular momentum + ], + constraints=[ + {"kind":"EQ","expr":"krp - ka*(1 - ke)","weight":5.0}, # rp = a(1-e) + {"kind":"EQ","expr":"kvp**2*krp - (1 + ke)","weight":5.0}, # vis-viva (GM=1) + {"kind":"EQ","expr":"kh - krp*kvp","weight":5.0}, # L = r×v + ], + scopes=[{"name":"orbit","order":0,"vars":["ka","ke","krp","kvp","kh"], + "constraints":[ + {"kind":"EQ","expr":"krp - ka*(1 - ke)","weight":5.0}, + {"kind":"EQ","expr":"kvp**2*krp - (1 + ke)","weight":5.0}, + {"kind":"EQ","expr":"kh - krp*kvp","weight":5.0}, + ]}], + anchors=[ + AXLInvariant("periapsis_radius","krp - ka*(1-ke)",1e-3), + AXLInvariant("vis_viva","kvp**2*krp - (1+ke)",1e-3), + AXLInvariant("ang_momentum","kh - krp*kvp",1e-3), + ], + observations={"ka":1.0,"ke":0.5}, # fix a=1, e=0.5 → rp=0.5, vp=√3, h=√3/2 +), + +# ── STRUCTURAL ENGINEERING ──────────────────────────────────────────── +AXLProblemDef( + name="VibratingString3", + description="3-node string under uniform unit load, fixed endpoints. " + "FD equations. Known: s1=s3=1.5, s2=2.0.", + axioms={Axiom.ORDERED,Axiom.SYMMETRIC,Axiom.CONSERVED,Axiom.METRIC}, + variables=[ + {"name":"s1","lo":0.0,"hi":5.0}, + {"name":"s2","lo":0.0,"hi":5.0}, + {"name":"s3","lo":0.0,"hi":5.0}, + ], + constraints=[ + {"kind":"EQ","expr":"-2*s1 + s2 + 1.0","weight":5.0}, # -2s1+s2=-1 + {"kind":"EQ","expr":"s1 - 2*s2 + s3 + 1.0","weight":5.0}, # s1-2s2+s3=-1 + {"kind":"EQ","expr":"s2 - 2*s3 + 1.0","weight":5.0}, # s2-2s3=-1 + ], + scopes=[{"name":"string","order":0,"vars":["s1","s2","s3"], + "constraints":[ + {"kind":"EQ","expr":"-2*s1 + s2 + 1.0","weight":5.0}, + {"kind":"EQ","expr":"s1 - 2*s2 + s3 + 1.0","weight":5.0}, + {"kind":"EQ","expr":"s2 - 2*s3 + 1.0","weight":5.0}, + ]}], + anchors=[ + AXLInvariant("node1","-2*s1+s2+1.0",1e-3), + AXLInvariant("node2","s1-2*s2+s3+1.0",1e-3), + AXLInvariant("node3","s2-2*s3+1.0",1e-3), + AXLInvariant("symmetry","s1-s3",1e-3), # s1=s3 by symmetry + ], + # Known: s1=s3=1.5, s2=2.0 +), + +# ── SIGNAL PROCESSING ───────────────────────────────────────────────── +AXLProblemDef( + name="SignalRecovery4", + description="Compressed sensing: A*x=b, find sparse x. " + "A=[[1,1,0,0],[1,0,1,0],[0,1,0,1]], b=[3,1,4]. " + "Sparse solution: x=[1,2,0,2] (3-sparse, r3=0).", + axioms={Axiom.CONSERVED,Axiom.PARSIMONY,Axiom.METRIC,Axiom.INJECTIVE}, + variables=[ + {"name":"r1","lo":0.0,"hi":5.0}, + {"name":"r2","lo":0.0,"hi":5.0}, + {"name":"r3","lo":0.0,"hi":5.0}, + {"name":"r4","lo":0.0,"hi":5.0}, + ], + constraints=[ + {"kind":"EQ","expr":"r1 + r2 - 3.0","weight":5.0}, + {"kind":"EQ","expr":"r1 + r3 - 1.0","weight":5.0}, + {"kind":"EQ","expr":"r2 + r4 - 4.0","weight":5.0}, + ], + scopes=[{"name":"signal","order":0,"vars":["r1","r2","r3","r4"], + "constraints":[ + {"kind":"EQ","expr":"r1+r2-3.0","weight":5.0}, + {"kind":"EQ","expr":"r1+r3-1.0","weight":5.0}, + {"kind":"EQ","expr":"r2+r4-4.0","weight":5.0}, + ]}], + anchors=[ + AXLInvariant("meas1","r1+r2-3.0",1e-3), + AXLInvariant("meas2","r1+r3-1.0",1e-3), + AXLInvariant("meas3","r2+r4-4.0",1e-3), + ], + # Known sparse: r1=1, r2=2, r3=0, r4=2 +), + +# ── ROBOTICS ───────────────────────────────────────────────────────── +AXLProblemDef( + name="RobotArm2D", + description="2-link planar arm, L1=L2=1, target=(1.2, 0.8). " + "Find angles: t1≈-0.177rad, t2≈1.531rad. (Trig constraints.)", + axioms={Axiom.CONTINUOUS,Axiom.METRIC,Axiom.SYMMETRIC,Axiom.QUADRATIC}, + variables=[ + {"name":"t1","lo":-3.15,"hi":3.15}, # joint 1 angle + {"name":"t2","lo":-3.15,"hi":3.15}, # joint 2 angle + ], + constraints=[ + # End-effector x = cos(t1) + cos(t1+t2) = 1.2 + {"kind":"EQ","expr":"cos(t1) + cos(t1+t2) - 1.2","weight":5.0}, + # End-effector y = sin(t1) + sin(t1+t2) = 0.8 + {"kind":"EQ","expr":"sin(t1) + sin(t1+t2) - 0.8","weight":5.0}, + ], + scopes=[{"name":"kinematics","order":0,"vars":["t1","t2"], + "constraints":[ + {"kind":"EQ","expr":"cos(t1)+cos(t1+t2)-1.2","weight":5.0}, + {"kind":"EQ","expr":"sin(t1)+sin(t1+t2)-0.8","weight":5.0}, + ]}], + anchors=[ + AXLInvariant("reach_x","cos(t1)+cos(t1+t2)-1.2",1e-2), + AXLInvariant("reach_y","sin(t1)+sin(t1+t2)-0.8",1e-2), + # Reachability: r²=1.44+0.64=2.08 ≤ (L1+L2)²=4 ✓ → cos(t2)≈0.04 + AXLInvariant("elbow_check","cos(t2) - 0.04",0.05), + ], + # Known: t2=arccos(0.04)≈1.531, t1≈-0.177 (elbow-up config) +), + +# ── MATHEMATICS (from v13.0) ───────────────────────────────────────── +AXLProblemDef( + name="NormManifold4D", + description="4 vars on unit sphere, zero sum, x1 observed at 0.5. " + "Multiple solutions exist on the great circle.", + axioms={Axiom.CONTINUOUS,Axiom.QUADRATIC,Axiom.CONSERVED,Axiom.METRIC,Axiom.SYMMETRIC}, + variables=[ + {"name":"x1","lo":-1.0,"hi":1.0},{"name":"x2","lo":-1.0,"hi":1.0}, + {"name":"x3","lo":-1.0,"hi":1.0},{"name":"x4","lo":-1.0,"hi":1.0}, + ], + constraints=[ + {"kind":"CONSERVE","expr":"x1**2 + x2**2 + x3**2 + x4**2 - 1.0"}, + {"kind":"EQ","expr":"x1 + x2 + x3 + x4","weight":2.0}, + ], + scopes=[{"name":"sphere","order":0,"vars":["x1","x2","x3","x4"], + "constraints":[{"kind":"EQ","expr":"x1**2+x2**2+x3**2+x4**2-1.0","weight":5.0}]}], + anchors=[ + AXLInvariant("unit_sphere","x1**2+x2**2+x3**2+x4**2-1.0",1e-3), + AXLInvariant("zero_sum","x1+x2+x3+x4",1e-3), + AXLInvariant("x1_pinned","x1-0.5",1e-3), + ], + observations={"x1":0.5}, +), +AXLProblemDef( + name="BilinearChain6", + description="6-var ordered chain. t1*t2=0.5, t3*t4=2.0, t5*t6=4.5, sum=9. " + "Known: (0.5,1.0,1.0,2.0,1.5,3.0).", + axioms={Axiom.DISCRETE,Axiom.ORDERED,Axiom.BILINEAR,Axiom.CONSERVED,Axiom.NETWORK}, + variables=[{"name":f"t{i}","lo":0.0,"hi":3.0} for i in range(1,7)], + constraints=[ + {"kind":"CONSERVE","expr":"t1+t2+t3+t4+t5+t6-9.0"}, + {"kind":"GEQ","expr":"t2-t1","weight":1.0},{"kind":"GEQ","expr":"t3-t2","weight":1.0}, + {"kind":"GEQ","expr":"t4-t3","weight":1.0},{"kind":"GEQ","expr":"t5-t4","weight":1.0}, + {"kind":"GEQ","expr":"t6-t5","weight":1.0}, + ], + scopes=[{"name":"chain","order":0,"vars":[f"t{i}" for i in range(1,7)], + "constraints":[ + {"kind":"EQ","expr":"t1*t2-0.5","weight":2.0}, + {"kind":"EQ","expr":"t3*t4-2.0","weight":2.0}, + {"kind":"EQ","expr":"t5*t6-4.5","weight":2.0}, + ]}], + anchors=[ + AXLInvariant("conservation","t1+t2+t3+t4+t5+t6-9.0",1e-3), + AXLInvariant("bilinear_lo","t1*t2-0.5",0.05), + AXLInvariant("bilinear_mid","t3*t4-2.0",0.05), + AXLInvariant("bilinear_hi","t5*t6-4.5",0.05), + AXLInvariant("ordering","t2-t1",0.5,"geq"), + ], +), +AXLProblemDef( + name="PhaseCollider", + description="2-particle symmetric collision: conservation + phase branch. " + "p1 at r=0.5 or r=1.0.", + axioms={Axiom.DISCRETE,Axiom.MUTABLE,Axiom.SYMMETRIC,Axiom.NETWORK,Axiom.CONSERVED}, + variables=[ + {"name":"p1x","lo":-2.0,"hi":2.0},{"name":"p2x","lo":-2.0,"hi":2.0}, + {"name":"p1y","lo":-2.0,"hi":2.0},{"name":"p2y","lo":-2.0,"hi":2.0}, + ], + constraints=[ + {"kind":"CONSERVE","expr":"p1x+p2x"},{"kind":"CONSERVE","expr":"p1y+p2y"}, + ], + scopes=[{"name":"phase","order":0,"vars":["p1x","p2x","p1y","p2y"], + "constraints":[ + {"kind":"BRANCH","name":"phase_select","options":[ + "p1x**2+p1y**2-0.25","p1x**2+p1y**2-1.0", + ]}, + {"kind":"EQ","expr":"p1x+p2x","weight":3.0}, + {"kind":"EQ","expr":"p1y+p2y","weight":3.0}, + ]}], + anchors=[ + AXLInvariant("momentum_x","p1x+p2x",1e-3), + AXLInvariant("momentum_y","p1y+p2y",1e-3), + AXLInvariant("phase_A_or_B","(p1x**2+p1y**2-0.25)*(p1x**2+p1y**2-1.0)",0.05), + ], +), +AXLProblemDef( + name="MetricPacking3D", + description="3 vars packed with min separation, centred at 0, norm²=6. " + "Known: a=-√3, b=0, c=√3.", + axioms={Axiom.CONTINUOUS,Axiom.METRIC,Axiom.INJECTIVE,Axiom.CONSERVED,Axiom.SYMMETRIC}, + variables=[ + {"name":"a","lo":-3.0,"hi":3.0}, + {"name":"b","lo":-3.0,"hi":3.0}, + {"name":"c","lo":-3.0,"hi":3.0}, + ], + constraints=[ + {"kind":"CONSERVE","expr":"a+b+c"}, + {"kind":"GEQ","expr":"(a-b)**2-1.0","weight":2.0}, + {"kind":"GEQ","expr":"(b-c)**2-1.0","weight":2.0}, + {"kind":"GEQ","expr":"(a-c)**2-4.0","weight":2.0}, + ], + scopes=[{"name":"packing","order":0,"vars":["a","b","c"], + "constraints":[{"kind":"EQ","expr":"a**2+b**2+c**2-6.0","weight":2.0}]}], + anchors=[ + AXLInvariant("centred","a+b+c",1e-3), + AXLInvariant("norm_6","a**2+b**2+c**2-6.0",0.05), + AXLInvariant("sep_ab","(a-b)**2-1.0",0.0,"geq"), # (a-b)²≥1 + AXLInvariant("sep_bc","(b-c)**2-1.0",0.0,"geq"), # (b-c)²≥1 + ], +), + +] # end AXL_PROBLEMS + +def build_base_problem(axl_def:AXLProblemDef) -> Problem: + psl_text=AXL_COMPILER.compile(axl_def) + prog=parse_psl(psl_text); ep=expand_psl(prog) + return Problem(pid=f"base_{axl_def.name}",variables=ep.variables, + constraints=ep.constraints,bounds=ep.bounds, + scope_groups=ep.scope_groups,scope_vars=ep.scope_vars, + scope_order=ep.scope_order,annotations=ep.annotations) # ══════════════════════════════════════════════════════════════════════ -# SECTION 15: GLOBAL STATE + RUNNER +# SECTION 14: GLOBAL STATE + ROUND-ROBIN RUNNER # ══════════════════════════════════════════════════════════════════════ -STATE_LOCK = threading.Lock() -RUN_LOG: List[Dict] = [] -THEORIST = SequenceRayTracer() -POOL = ThreadPoolExecutor(max_workers=2) - -def _run_problem(axl_def: AXLProblemDef): +STATE_LOCK = threading.Lock() +RUN_LOG: List[Dict] = [] +PROBLEM_STATS: Dict[str,Dict] = {p.name: { + "runs":0,"solved":0,"total_ce":0.0,"total_rays":0, + "best_ce":float('inf'),"best_ray":"—","last_binding":{} +} for p in AXL_PROBLEMS} +POOL = ThreadPoolExecutor(max_workers=1) # sequential: one tracer at a time +_PROBLEM_IDX = 0 + +def _run_problem(axl_def:AXLProblemDef): try: - base_prob = build_base_problem(axl_def) - binding, ce, history = THEORIST.trace(axl_def, base_prob) - - survived = [t for t in THEORIST.all_traces if t.survived] - failed = [t for t in THEORIST.all_traces if not t.survived] - best_t = min(survived, key=lambda t: t.ce_after, default=None) - - record = { - "problem": axl_def.name, - "description": axl_def.description, - "ce": round(ce, 6), - "solved": len(survived) > 0 and ce < SOLVE_THRESHOLD, - "binding": {k: round(v,5) for k,v in binding.items()}, + base_prob=build_base_problem(axl_def) + tracer=SequenceRayTracer() + binding,ce,history=tracer.trace(axl_def,base_prob) + traces=tracer._last_traces + survived=[t for t in traces if t.survived] + failed =[t for t in traces if not t.survived] + best_t =min(survived,key=lambda t:t.ce_after,default=None) + record={ + "problem":axl_def.name, + "description":axl_def.description[:60], + "domain":PROBLEM_META.get(axl_def.name,{}).get("domain","Unknown"), + "icon":PROBLEM_META.get(axl_def.name,{}).get("icon","·"), + "difficulty":PROBLEM_META.get(axl_def.name,{}).get("difficulty","?"), + "ce":round(ce,6), + "solved":len(survived)>0 and ce 40: RUN_LOG.pop(0) + if len(RUN_LOG)>60: RUN_LOG.pop(0) + ps=PROBLEM_STATS[axl_def.name] + ps["runs"]+=1; ps["total_rays"]+=len(traces); ps["total_ce"]+=ce + if len(survived)>0 and ce str: - b = record["binding"]; traces = record["traces"] - survived = [t for t in traces if t["survived"]] - best = min(survived, key=lambda t: t["ce"], default=None) - if not best and traces: - best = min(traces, key=lambda t: t.get("g1_ce") or 999.0) - obs_vars = set(record.get("observations",{}).keys()) - - ce = record["ce"]; solved = record["solved"] - ce_color = "#4CAF50" if solved else ("#FF9800" if ce < 0.5 else "#EF5350") - status = "✓ SOLVED + VERIFIED" if solved else ("~ PARTIAL" if ce < 0.5 else "✗ UNSOLVED") - - binding_rows = "".join( - f"{v}" +app=FastAPI(title="Practicality 14.0",lifespan=lifespan) + +def _perf_table() -> str: + rows="" + for prob in AXL_PROBLEMS: + ps=PROBLEM_STATS[prob.name] + if ps["runs"]==0: + rows+=f"{PROBLEM_META.get(prob.name,{}).get('icon','·')}{PROBLEM_META.get(prob.name,{}).get('domain','')}{prob.name}{PROBLEM_META.get(prob.name,{}).get('difficulty','')}warming up…" + continue + runs=ps["runs"]; rate=round(ps["solved"]/runs*100) + avg_ce=round(ps["total_ce"]/runs,5) + avg_rays=round(ps["total_rays"]/runs,1) + rate_col="#4CAF50" if rate>=50 else ("#FF9800" if rate>=20 else "#EF5350") + dom=PROBLEM_META.get(prob.name,{}) + axiom_str=", ".join(sorted(AXIOM_ABBR.get(a,a[:3]) for a in prob.axioms)[:4]) + best_ray=ps["best_ray"][:25] if ps["best_ray"]!="—" else "—" + best_ce_str=f"{ps['best_ce']:.5f}" if ps["best_ce"]" + f"{dom.get('icon','·')}" + f"{dom.get('domain','')}" + f"{prob.name}" + f"{dom.get('difficulty','')}" + f"{axiom_str}" + f"{runs}" + f"{rate}%" + f"{avg_ce}" + f"{best_ce_str}" + f"{avg_rays:.0f}" + f"{best_ray}" + f"") + return rows + +def _axiom_table(log) -> str: + axiom_stats=defaultdict(lambda:{"tried":0,"survived":0,"total_ce":0.0,"as_seed":0}) + for r in log: + for t in r.get("traces",[]): + parts=t["ray"].split("→") + for pos,ax in enumerate(parts): + if not ax: continue + axiom_stats[ax]["tried"]+=1; axiom_stats[ax]["total_ce"]+=t["ce"] + if t["survived"]: axiom_stats[ax]["survived"]+=1 + if pos==0: axiom_stats[ax]["as_seed"]+=1 + return "".join( + f"{ax}" + f"{s['tried']}" + f"{s['as_seed']}" + f"{s['survived']}" + f"{round(s['total_ce']/s['tried'],5) if s['tried'] else 0}" + f"0 else '#333'}'>{round(s['survived']/s['tried']*100):.0f}%" + for ax,s in sorted(axiom_stats.items(),key=lambda x:-x[1]["survived"]) + ) or "—" + +def _render_collapse(record:Dict) -> str: + b=record["binding"]; traces=record["traces"] + survived=[t for t in traces if t["survived"]] + best=min(survived,key=lambda t:t["ce"],default=None) + if not best and traces: best=min(traces,key=lambda t:t.get("g1_ce") or 999.0) + obs_vars=set(record.get("observations",{}).keys()) + ce=record["ce"]; solved=record["solved"] + ce_color="#4CAF50" if solved else ("#FF9800" if ce<0.5 else "#EF5350") + status="✓ SOLVED" if solved else ("~ PARTIAL" if ce<0.5 else "✗ UNSOLVED") + binding_rows="".join( + f"{v}" f"{val:+.5f}" - f"{'[OBS]' if v in obs_vars else ''}" + f"{'[OBS]' if v in obs_vars else ''}" for v,val in b.items()) - - inv_rows = "" + inv_rows="" if best and best.get("g2_detail"): - for inv,(err,ok) in best["g2_detail"].items(): - c = "#4CAF50" if ok else "#EF5350" - inv_rows += (f"{'✓' if ok else '✗'}" - f"{inv}" - f"{err:.6f}") - - def trail_span(t): - depth_pad = " " * min(t.get("depth",0), 6) - c = "#4CAF50" if t["survived"] else ("#555" if t.get("depth",0) > 0 else "#333") - ce_delta = t["ce"] - t.get("ce_before", t["ce"]) - delta_str = f"Δ{ce_delta:+.4f}" if abs(ce_delta) > 1e-6 else "" - star = " ◀ VERIFIED" if t["survived"] else "" - return (f"
" - f"{depth_pad}[R{t['round']}|d{t.get('depth',0)}] " + for inv,(val,ok) in best["g2_detail"].items(): + c="#4CAF50" if ok else "#EF5350" + inv_rows+=(f"{'✓' if ok else '✗'}" + f"{inv}" + f"{val:.5f}") + def span(t): + depth_indent="·"*min(t.get("depth",0),5) + c="#4CAF50" if t["survived"] else ("#555" if t.get("depth",0)>0 else "#333") + star=" ◀" if t["survived"] else "" + delta=t["ce"]-t.get("ce_before",t["ce"]) + return (f"
" + f"{depth_indent}[{t['round']}|d{t.get('depth',0)}] " f"{t['ray']} " - f"CE={t['ce']:.5f} {delta_str} " - f"G1={'✓' if t['g1'] else '✗'} G2={'✓' if t['g2'] else '✗'}" + f"CE={t['ce']:.4f} {delta:+.4f}" f"{star}
") - - trail = "".join(trail_span(t) for t in traces[:30]) - + trail="".join(span(t) for t in traces[:25]) return f""" -
-
- {status} - {record["problem"]} - CE={ce:.6f} - {record["survived_count"]} survived / {record["total_fired"]} fired +
+
+ {status} + {record.get("icon","·")} {record["problem"]} + {record.get("domain","")} + CE={ce:.6f} + {record["survived_count"]} survived / {record["total_fired"]} fired
-
-
BINDING
+
+
BINDING
{binding_rows}
-
-
INVARIANTS (Gate 2)
+
+
GATE 2 INVARIANTS
{inv_rows or ""}
—
-
-
- SEQUENCE RAY TREE — best: {record["best_ray"]} +
+
+ RAY TREE — best: {record["best_ray"]}
{trail}
""" -@app.get("/", response_class=HTMLResponse) +@app.get("/",response_class=HTMLResponse) async def dashboard(): - with STATE_LOCK: log = list(reversed(RUN_LOG[-10:])) - runs = len(RUN_LOG) - solved = sum(1 for r in RUN_LOG if r.get("solved",False)) - avg_ce = round(sum(r["ce"] for r in RUN_LOG)/max(1,runs),5) if RUN_LOG else 0 - - # Axiom efficacy across all sequence positions - axiom_stats = defaultdict(lambda: {"tried":0,"survived":0,"total_ce":0.0,"as_seed":0}) - for r in log: - for t in r.get("traces",[]): - ray_str = t["ray"] - parts = ray_str.split("→") - for pos, ax_abbr in enumerate(parts): - if not ax_abbr: continue - axiom_stats[ax_abbr]["tried"] += 1 - axiom_stats[ax_abbr]["total_ce"] += t["ce"] - if t["survived"]: axiom_stats[ax_abbr]["survived"] += 1 - if pos == 0: axiom_stats[ax_abbr]["as_seed"] += 1 - - axiom_rows = "".join( - f"{ax}" - f"{s['tried']}" - f"{s['as_seed']}" - f"{s['survived']}" - f"{s['tried']-s['survived']}" - f"{round(s['total_ce']/s['tried'],5) if s['tried'] else 0}" - f"0 else '#333'}'>" - f"{round(s['survived']/s['tried']*100):.0f}%" - for ax,s in sorted(axiom_stats.items(), key=lambda x:-x[1]["survived"]) - ) or "Warming up…" - - collapses = "".join(_render_collapse(r) for r in log) if log else \ - "
Warming up…
" - - return f"""Practicality 13.0 - + with STATE_LOCK: + log=list(reversed(RUN_LOG[-8:])) + stats_snapshot=dict(PROBLEM_STATS) + total_runs=sum(s["runs"] for s in stats_snapshot.values()) + total_solved=sum(s["solved"] for s in stats_snapshot.values()) + domains_active=len([p for p in AXL_PROBLEMS if stats_snapshot[p.name]["runs"]>0]) + avg_ce=(sum(s["total_ce"] for s in stats_snapshot.values())/max(1,total_runs)) + + perf_rows=_perf_table() + ax_rows=_axiom_table(log) + collapses="".join(_render_collapse(r) for r in log) if log else \ + "
Cycling through 14 problems…
" + + return f"""Practicality 14.0 + -

⚗ Practicality 13.0 — Sequence Rays (Ordered Axiom Chains)

-
- 27 Axioms (Math · Physics · Logic · Philosophy) → Ordered Sequences → - Baton Protocol (child inherits partial) → Earn Extension by CE reduction → - Contradiction at Distance allowed +

⚗ Practicality 14.0 — 14 Domains · 27 Axioms · Sequence Rays

+
+ Real-world AXL problems → PSL base → Sequence rays (ordered axiom chains) → + Baton protocol → Earn extension by CE reduction → Contradiction at distance
-
- Runs: {runs} - Solved: {solved} - Avg CE: {avg_ce} - Problems: {len(AXL_PROBLEMS)} +
+ Total Runs: {total_runs} + Solved: {total_solved} + Avg CE: {avg_ce:.5f} + Active Domains: {domains_active}/14 Axioms: {len(ALL_AXIOMS)}
-

Axiom Efficacy — All Sequence Positions

+ +

Multi-Domain Performance Table

+ + + + + + + {perf_rows} +
DomainProblemDifficultyAxiom TagsRunsRate%Avg CEBest CEAvg RaysBest Sequence
+ +

Axiom Efficacy — Cross-Domain

- - {axiom_rows} + + {ax_rows}
AxiomIn-SeqAs SeedSurvivedFailedAvg CEEfficacy
AxiomIn-SeqAs SeedSurvivedAvg CERate
-

Collapse View — Recent Runs

+ +

Recent Runs

{collapses} """ -if __name__ == "__main__": - uvicorn.run(app, host="0.0.0.0", port=7860, log_level="warning") \ No newline at end of file +if __name__=="__main__": + uvicorn.run(app,host="0.0.0.0",port=7860,log_level="warning") \ No newline at end of file