#!/usr/bin/env python3 """ PRACTICALITY SYSTEM 21.0 — MPR ORDERING FIX + BRANCH WIDTH 12 ═══════════════════════════════════════════════════════════════════ CHANGES FROM 20.0: 1. BRANCH_WIDTH: 4 → 12 (more exploration per earned ray) 2. MPR ORDERING BUG FIX: The v_small/v_large detection now reads expression sign correctly instead of relying on sympy's alphabetical symbol ordering. For GEQ expr like "t2-t1", we parse which symbol has a positive coefficient (v_large) and which has a negative coefficient (v_small). 3. SYSTEMIC BRANCH BOOST: When tension_class=="systemic" and ce>0.1, branch width scales to 16 to handle high-condition- number constraint Jacobians (BilinearChain6 class problems). 4. GPU UTILIZATION FIX: Tensor operations moved to stay on device throughout batch; eliminated CPU round-trips in energy loop. """ import time, random, math, threading, warnings from functools import reduce from typing import Optional, Callable, List, Dict, Tuple, Any, Set from dataclasses import dataclass, field from collections import defaultdict, deque import numpy as np import sympy as sp from sympy.parsing.sympy_parser import parse_expr import torch import gradio as gr warnings.filterwarnings("ignore") USE_GPU = torch.cuda.is_available() DEVICE = torch.device("cuda" if USE_GPU else "cpu") print(f"[SYSTEM 21.0] Compute: {DEVICE.type.upper()} | MPR Fix + Branch-12") # ══════════════════════════════════════════════════════════════════════ # SECTION 1: CONSTANTS # ══════════════════════════════════════════════════════════════════════ SOLVE_THRESHOLD = 0.05 VERIFY_G1_THRESHOLD = 0.08 VERIFY_G2_TOLERANCE = 1e-3 DEDUCE_ADAM_STEPS = 25 N_MPRT_EXPLORE = 1000 PROJECTION_CACHE: Dict = {} MAX_TOTAL_RAYS = 1_500_000 RAY_BATCH_SIZE = 12288 CE_EARN_RATIO = 0.90 SCOUT_CE_THRESHOLD = 0.5 BRANCH_WIDTH = 12 # 20.0 was 4 BRANCH_WIDTH_SYSTEMIC = 16 # extra width for systemic tension BATON_REGISTRY_THRESHOLD = 2.0 BATON_REGISTRY_MAX = 5000 # ══════════════════════════════════════════════════════════════════════ # SECTION 2: INTERVAL ARITHMETIC (HC4) # ══════════════════════════════════════════════════════════════════════ class IV: __slots__ = ("lo","hi") def __init__(self,lo,hi): self.lo=float(lo); self.hi=float(hi) def __add__(self,o): return IV(self.lo+o,self.hi+o) if isinstance(o,(int,float)) else IV(self.lo+o.lo,self.hi+o.hi) __radd__=__add__ def __sub__(self,o): return IV(self.lo-o,self.hi-o) if isinstance(o,(int,float)) else IV(self.lo-o.hi,self.hi-o.lo) def __rsub__(self,o): return IV(o-self.hi,o-self.lo) if isinstance(o,(int,float)) else o.__sub__(self) def __mul__(self,o): if isinstance(o,(int,float)): a,b=self.lo*o,self.hi*o; return IV(min(a,b),max(a,b)) p=(self.lo*o.lo,self.lo*o.hi,self.hi*o.lo,self.hi*o.hi); return IV(min(p),max(p)) __rmul__=__mul__ def __truediv__(self,o): if isinstance(o,(int,float)): if abs(o)<1e-15: return IV(-1e18,1e18) a,b=self.lo/o,self.hi/o; return IV(min(a,b),max(a,b)) if o.lo<=0<=o.hi: return IV(-1e18,1e18) return self*IV(1.0/o.hi,1.0/o.lo) def __rtruediv__(self,o): if self.lo<=0<=self.hi: return IV(-1e18,1e18) return IV(o/self.hi,o/self.lo) if o>=0 else IV(o/self.lo,o/self.hi) def __neg__(self): return IV(-self.hi,-self.lo) def __pow__(self,n): if isinstance(n,int): if n==0: return IV(1.0,1.0) if n%2==0: if self.lo>=0: return IV(self.lo**n,self.hi**n) if self.hi<=0: return IV(self.hi**n,self.lo**n) return IV(0.0,max(abs(self.lo)**n,abs(self.hi)**n)) return IV(self.lo**n if self.lo>=0 else -((-self.lo)**n), self.hi**n if self.hi>=0 else -((-self.hi)**n)) if self.lo<0: return IV(0.0,max(abs(self.lo)**n,self.hi**n)) return IV(self.lo**n,self.hi**n) def contains_zero(self): return self.lo<=0.0<=self.hi def width(self): return max(0.0,self.hi-self.lo) def mid(self): return (self.lo+self.hi)*0.5 def compile_iv(expr,variables): def _c(e): if e.is_Number: v=float(e); return lambda box,_v=v: IV(_v,_v) if e.is_Symbol: n=str(e); return lambda box,_n=n: box.get(_n,IV(-1e18,1e18)) if e.is_Add: fs=[_c(a) for a in e.args]; return lambda box,_fs=fs: reduce(lambda a,b:a+b,(_f(box) for _f in _fs)) if e.is_Mul: fs=[_c(a) for a in e.args]; return lambda box,_fs=fs: reduce(lambda a,b:a*b,(_f(box) for _f in _fs)) if e.is_Pow: bc=_c(e.args[0]); ex=e.args[1] if ex.is_Number: return lambda box,_bc=bc,_ex=float(ex): _bc(box)**_ex exc=_c(ex); return lambda box,_bc=bc,_exc=exc: _bc(box)**_exc(box).mid() return lambda box: IV(-1e18,1e18) return _c(expr) def _hc4(box,constraints): cur=dict(box) for mc in constraints: if getattr(mc,'weight',1.0)==0.0: continue if mc.kind=="or_eq": valid=False for bmc in mc.branches: if bmc.fast_iv is None: valid=True; break try: if bmc.fast_iv(cur).contains_zero(): valid=True; break except: valid=True; break if not valid: return None else: if mc.fast_iv is None: continue try: riv=mc.fast_iv(cur) if ((mc.kind=="equality" and not riv.contains_zero()) or (mc.kind=="inequality" and ((mc.direction=="geq" and riv.hi<-1e-10) or (mc.direction=="leq" and riv.lo>1e-10)))): return None except: pass return cur def _global_hc4_tighten_bounds(problem): gb={v:IV(lo,hi) for v,(lo,hi) in problem.bounds.items()} c=_hc4(gb,problem.compiled_constraints) if c is None: return dict(problem.bounds) return {v:(max(problem.bounds[v][0],c[v].lo),min(problem.bounds[v][1],c[v].hi)) for v in problem.bounds if v in c} # ══════════════════════════════════════════════════════════════════════ # SECTION 3: PSL PARSER & PRE-COMPILATION # ══════════════════════════════════════════════════════════════════════ @dataclass 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 class PSLScope: name:str; order:int=0; depends:List[str]=field(default_factory=list); vars:List[PSLVar]=field(default_factory=list); links:List[str]=field(default_factory=list); constraints:List[PSLConstraint]=field(default_factory=list) @dataclass class PSLProgram: name:str; vars:List[PSLVar]; constraints:List[PSLConstraint]; scopes:List[PSLScope]; scope_order:List[str]; annotations:Dict[str,str]=field(default_factory=dict) def parse_psl(text:str) -> PSLProgram: lines=[l.strip() for l in text.strip().split('\n') if l.strip() and not l.strip().startswith('#')] prog=PSLProgram("unnamed",[],[],[],[]); i=0 def advance(): nonlocal i; l=lines[i]; i+=1; return l def peek(): return lines[i] if i=3 else None def pw(rest): return (rest.split('WEIGHT')[0].strip(),float(rest.split('WEIGHT')[1].split()[0])) if 'WEIGHT' in rest else (rest.strip(),1.0) def parse_scope_body(sname,order=0,depends=None): svars,scons,links=[],[],[] while i1 else "" if kw in ("END","END SCOPE"): advance(); break advance() if kw=="VAR": v=pvar(rest); svars.append(v) if v else None elif kw=="LINK": links.extend(rest.split()) elif kw in ("EQ","GEQ","LEQ"): expr,wt=pw(rest); scons.append(PSLConstraint(kw.lower(),expr,scope=sname,weight=wt)) elif kw=="CONSERVE": expr,_=pw(rest); scons.append(PSLConstraint("eq",expr,scope=sname,weight=10.0)) elif kw=="BRANCH": opts=[] while i1 else "" if kw=="SPACE": prog.name=rest.split()[0] if rest else "unnamed" elif kw=="VAR": v=pvar(rest); prog.vars.append(v) if v else None elif kw in ("EQ","GEQ","LEQ"): expr,wt=pw(rest); prog.constraints.append(PSLConstraint(kw.lower(),expr,weight=wt)) elif kw=="CONSERVE": expr,_=pw(rest); prog.constraints.append(PSLConstraint("eq",expr,weight=10.0)) elif kw=="BRANCH": opts=[] while i ExpandedProblem: variables=[]; bounds={}; constraints=[]; scope_groups=defaultdict(list); scope_vars=defaultdict(list) def add_var(name,lo,hi,scope="root"): if name not in bounds: variables.append(name); bounds[name]=(lo,hi) if scope!="root" and name not in scope_vars[scope]: scope_vars[scope].append(name) def add_con(kind,expr,direction,scope="root",weight=1.0,branches=None): constraints.append(Constraint(kind,expr,direction,weight,scope,branches or [])) scope_groups[scope].append(len(constraints)-1) try: syms={v:sp.Symbol(v) for v in variables} parsed=parse_expr(expr,local_dict=syms) if kind!="or_eq" else None if parsed: for v in variables: if sp.Symbol(v) in parsed.free_symbols and scope!="root" and v not in scope_vars[scope]: scope_vars[scope].append(v) except: pass for v in prog.vars: add_var(v.name,v.lo,v.hi) for c in prog.constraints: add_con("or_eq" if c.kind=="or_eq" else "equality" if c.kind=="eq" else "inequality", c.expr,c.kind,"root",c.weight,c.branches) for sc in prog.scopes: for v in sc.vars: add_var(v.name,v.lo,v.hi,sc.name) for c in sc.constraints: add_con("or_eq" if c.kind=="or_eq" else "equality" if c.kind=="eq" else "inequality", c.expr,c.kind,sc.name,c.weight,c.branches) return ExpandedProblem(variables,bounds,constraints,dict(scope_groups),dict(scope_vars),prog.scope_order) @dataclass class AXLInvariant: name:str; expr:str; tolerance:float=VERIFY_G2_TOLERANCE; mode:str="eq" compiled_func: Optional[Callable] = field(default=None, repr=False) syms_used: List[str] = field(default_factory=list) def compile(self, variables: List[str]): syms = {v: sp.Symbol(v) for v in variables} parsed = parse_expr(self.expr, local_dict=syms) self.syms_used = [str(s) for s in parsed.free_symbols if str(s) in variables] self.compiled_func = sp.lambdify([sp.Symbol(v) for v in self.syms_used], parsed, modules="math") @dataclass class AXLProblemDef: name:str; description:str; axioms:Set[str]; variables:List[Dict]; constraints:List[Dict] scopes:List[Dict]; anchors:List[AXLInvariant]; observations:Dict[str,float]=field(default_factory=dict) class AXLtoPSLCompiler: def compile(self,prob:AXLProblemDef) -> str: 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 lines.append(f"VAR {v['name']} {lo} {hi}") for c in prob.constraints: wt=c.get("weight",1.0) if c["kind"]=="CONSERVE": lines.append(f"CONSERVE {c['expr']}") elif c["kind"]=="BRANCH": lines.append(f"BRANCH {c.get('name','br')}") for opt in c.get("options",[]): lines.append(f" OPTION {opt}") lines.append("END BRANCH") else: lines.append(f"{c['kind']} {c['expr']} WEIGHT {wt}") for sc in prob.scopes: lines.append(f"SCOPE {sc['name']} ORDER {sc.get('order',0)}") for c in sc.get("constraints",[]): lines.append(f" {c['kind']} {c['expr']} WEIGHT {c.get('weight',1.0)}") lines.append("END") return "\n".join(lines) AXL_COMPILER=AXLtoPSLCompiler() # ══════════════════════════════════════════════════════════════════════ # SECTION 4: PROBLEM COMPILATION # ══════════════════════════════════════════════════════════════════════ @dataclass class Constraint: kind:str; expr:str; direction:str; weight:float=1.0; scope:str="root" branches:List[str]=field(default_factory=list) @dataclass class MathConstraint: kind:str; expr_str:str; direction:str; weight:float=1.0 fast_iv:Optional[Callable]=field(default=None,repr=False) fast_pt:Optional[Callable]=field(default=None,repr=False) torch_func:Optional[Callable]=field(default=None,repr=False) syms_used:List[str]=field(default_factory=list) parsed:Optional[sp.Expr]=field(default=None,repr=False) scope:str="root" branches:List['MathConstraint']=field(default_factory=list) projections:Dict[str,List[Dict]]=field(default_factory=dict) def compile_mc(kind,expr_str,direction,variables,weight=1.0,scope="root",branches=None): mc=MathConstraint(kind=kind,expr_str=expr_str,direction=direction,weight=weight,scope=scope) if kind=="or_eq" and branches: for b_str in branches: b_mc=compile_mc("equality",b_str,"eq",variables,weight,scope) mc.branches.append(b_mc); mc.syms_used.extend(b_mc.syms_used) mc.syms_used=list(dict.fromkeys(mc.syms_used)) def _or_iv(box,_mcs=mc.branches): rivs=[] for b in _mcs: if b.fast_iv: try: rivs.append(b.fast_iv(box)) 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 syms={v:sp.Symbol(v) for v in variables} try: parsed=parse_expr(expr_str,local_dict=syms); mc.parsed=parsed mc.syms_used=[v for v in variables if sp.Symbol(v) in parsed.free_symbols] mc.fast_iv=compile_iv(parsed,variables) mc.fast_pt=sp.lambdify([sp.Symbol(v) for v in mc.syms_used],parsed,modules="math") pt_map={'sin':torch.sin,'cos':torch.cos,'exp':torch.exp,'sqrt':torch.sqrt,'Abs':torch.abs} t_func_raw=sp.lambdify([sp.Symbol(v) for v in mc.syms_used],parsed,modules=[pt_map,"math"]) def _t_wrapper(*args): val=t_func_raw(*args) return torch.tensor(val,device=DEVICE,dtype=torch.float32) if isinstance(val,(int,float)) else val mc.torch_func=_t_wrapper if kind=="equality": if expr_str not in PROJECTION_CACHE: pm={} for sym in parsed.free_symbols: v_str=str(sym) try: sols=sp.solve(parsed,sym); pm[v_str]=[] for sol in sols: fs=list(sol.free_symbols) pm[v_str].append({"syms":[str(s) for s in fs], "func":sp.lambdify(fs,sol,modules="math")}) except: pass PROJECTION_CACHE[expr_str]=pm mc.projections=PROJECTION_CACHE.get(expr_str,{}) except: pass return mc def _extract_ordering_pair(mc: MathConstraint, variables: List[str]) -> Optional[Tuple[str,str]]: """ SYSTEM 21.0 FIX: Correctly extract (v_small, v_large) from a GEQ constraint by reading coefficient signs rather than relying on sympy symbol ordering. For expr "t2-t1 >= 0": t2 has coeff +1 (v_large), t1 has coeff -1 (v_small) For expr "t1-t2 >= 0": t1 has coeff +1 (v_large), t2 has coeff -1 (v_small) Returns (v_small, v_large) or None if not a simple difference constraint. """ if mc.kind != "inequality" or mc.direction != "geq": return None if mc.parsed is None: return None parsed = mc.parsed sym_vars = {v: sp.Symbol(v) for v in variables} # Must involve exactly 2 variables free = [str(s) for s in parsed.free_symbols if str(s) in variables] if len(free) != 2: return None # Extract linear coefficients: parsed = c0 + c1*v1 + c2*v2 # For the ordering to be v_large >= v_small, we need: # parsed = v_large - v_small >= 0 # so v_large has positive coeff, v_small has negative coeff v0, v1 = free[0], free[1] try: c0 = float(parsed.coeff(sp.Symbol(v0))) c1 = float(parsed.coeff(sp.Symbol(v1))) except Exception: return None # Need one positive and one negative coefficient for a pure ordering constraint if c0 > 0 and c1 < 0: return (v1, v0) # v1 is small (negative coeff), v0 is large (positive coeff) elif c1 > 0 and c0 < 0: return (v0, v1) # v0 is small (negative coeff), v1 is large (positive coeff) return None @dataclass class Problem: pid:str; variables:List[str]; constraints:List[Constraint] bounds:Dict[str,Tuple[float,float]] scope_groups:Dict[str,List[int]]=field(default_factory=dict) scope_vars:Dict[str,List[str]]=field(default_factory=dict) scope_order:List[str]=field(default_factory=list) bilinear_pairs: List[Tuple[str,str]] = field(default_factory=list) monotone_targets: List[Tuple[str,str,float]] = field(default_factory=list) ordering_pairs: List[Tuple[str,str]] = field(default_factory=list) # NEW 21.0 def __post_init__(self): self.compiled_constraints=[ compile_mc(c.kind,c.expr,c.direction,self.variables,c.weight,c.scope,c.branches) for c in self.constraints] self.var_idx={v:i for i,v in enumerate(self.variables)} # SYSTEM 21.0: Extract ordering pairs with correct sign detection for mc in self.compiled_constraints: pair = _extract_ordering_pair(mc, self.variables) if pair and pair not in self.ordering_pairs: self.ordering_pairs.append(pair) # Bilinear pairs from equality constraints for mc in self.compiled_constraints: if mc.parsed and mc.parsed.is_Add: for term in mc.parsed.args: if term.is_Mul: syms_in = [str(s) for s in term.free_symbols if str(s) in self.variables] if len(syms_in) == 2: va, vb = syms_in if (va, vb) not in self.bilinear_pairs and (vb, va) not in self.bilinear_pairs: self.bilinear_pairs.append((va, vb)) # Monotone targets: bilinear products that also appear in ordering for mc in self.compiled_constraints: if mc.kind == "equality" and mc.parsed is not None: for va, vb in self.bilinear_pairs: sa, sb = sp.Symbol(va), sp.Symbol(vb) if sa in mc.parsed.free_symbols and sb in mc.parsed.free_symbols: try: # Extract constant k from: va*vb = k (i.e. va*vb - k = 0) k_expr = -(mc.parsed - sa*sb) k = float(k_expr.evalf()) if k > 0: # Check which ordering applies (21.0 fix: use ordering_pairs) for vs, vl in self.ordering_pairs: if set([va, vb]) == set([vs, vl]): target = (vs, vl, k) if target not in self.monotone_targets: self.monotone_targets.append(target) except Exception: pass def tensor_energy(self,X:torch.Tensor) -> torch.Tensor: is_batched=(X.dim()==2) total=torch.zeros(X.shape[0] if is_batched else 1,device=DEVICE,dtype=torch.float32) for mc in self.compiled_constraints: if getattr(mc,'weight',1.0)==0.0: continue if mc.kind=="or_eq": b_vals=[] for bmc in mc.branches: if bmc.torch_func: args=[X[:,self.var_idx[v]] if is_batched else X[self.var_idx[v]] for v in bmc.syms_used] b_vals.append(torch.abs(bmc.torch_func(*args))) if b_vals: total+=torch.stack(b_vals,dim=0).min(dim=0)[0]*mc.weight else: if mc.torch_func is None: continue args=[X[:,self.var_idx[v]] if is_batched else X[self.var_idx[v]] for v in mc.syms_used] val=mc.torch_func(*args) if mc.kind=="equality": total+=torch.abs(val)*mc.weight elif mc.direction=="geq": total+=torch.relu(-val)*mc.weight else: total+=torch.relu(val)*mc.weight for i,v in enumerate(self.variables): lo,hi=self.bounds[v] col=X[:,i] if is_batched else X[i] total+=torch.relu(lo-col)+torch.relu(col-hi) return total.squeeze() def scalar_energy(self,b:Dict[str,float]) -> float: total=0.0 for mc in self.compiled_constraints: if getattr(mc,'weight',1.0)==0.0: continue if mc.kind=="or_eq": vals=[] for bmc in mc.branches: if bmc.fast_pt: try: vals.append(abs(float(bmc.fast_pt(*[b.get(v,0.0) for v in bmc.syms_used])))) except: pass total+=(min(vals)*mc.weight) if vals else 1.0 else: 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 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) return total # ══════════════════════════════════════════════════════════════════════ # SECTION 5: BATCHED MASKED DEDUCTION # ══════════════════════════════════════════════════════════════════════ @dataclass class L9Certificate: residual_ce:float; dominant_vars:List[str]; dominant_exprs:List[str] tension_class:str="unknown" def _batched_deduce_and_evaluate( problem:Problem, hyps:List['Hypothesis']) -> List[Tuple[Dict,float,List[str],str]]: if not hyps: return [] B=len(hyps); V=len(problem.variables) x_data = [] mask_data = [] target_data = [] for hyp in hyps: xr, mr, tr = [], [], [] for v in problem.variables: if v in hyp.pinned_vars: val = hyp.pinned_vars[v] xr.append(val); mr.append(0.0); tr.append(val) else: val = hyp.binding.get(v, (problem.bounds[v][0]+problem.bounds[v][1])/2) xr.append(val); mr.append(1.0); tr.append(0.0) x_data.append(xr); mask_data.append(mr); target_data.append(tr) X = torch.tensor(x_data, device=DEVICE, dtype=torch.float32, requires_grad=True) mask = torch.tensor(mask_data, device=DEVICE, dtype=torch.float32) target = torch.tensor(target_data, device=DEVICE, dtype=torch.float32) optimizer=torch.optim.Adam([X],lr=0.05) for _ in range(DEDUCE_ADAM_STEPS): optimizer.zero_grad() ce=problem.tensor_energy(X) if isinstance(ce,torch.Tensor) and (ce 1e-4] n_dom = len(dom_vars) if n_dom<=1: tension_class="isolated" elif n_dom==2: tension_class="relational" else: tension_class="systemic" results.append((final_b,float(ce_vals[i]),dom_vars,tension_class)) return results def _mprt_sample(problem,work_box,N): var_list=problem.variables; V=len(var_list) lo_t=torch.tensor([max(problem.bounds.get(v,(-10.0,10.0))[0], work_box[v].lo if v in work_box else problem.bounds.get(v,(-10,10))[0]) for v in var_list],device=DEVICE,dtype=torch.float32) hi_t=torch.tensor([min(problem.bounds.get(v,(-10.0,10.0))[1], work_box[v].hi if v in work_box else problem.bounds.get(v,(-10,10))[1]) for v in var_list],device=DEVICE,dtype=torch.float32) for i in range(V): if lo_t[i]>=hi_t[i]: m=(lo_t[i]+hi_t[i])/2; lo_t[i]=m-1e-6; hi_t[i]=m+1e-6 X=lo_t.unsqueeze(0)+(hi_t-lo_t).unsqueeze(0)*torch.rand((N,V),device=DEVICE) ce_batch=problem.tensor_energy(X) best_idx=torch.argmin(ce_batch).item() return {v:float(X[best_idx,i].item()) for i,v in enumerate(var_list)},ce_batch[best_idx].item() # ══════════════════════════════════════════════════════════════════════ # SECTION 6: AXIOMS # ══════════════════════════════════════════════════════════════════════ class Axiom: CONTINUOUS="CONTINUOUS"; DISCRETE="DISCRETE"; QUADRATIC="QUADRATIC" BILINEAR="BILINEAR"; METRIC="METRIC"; SYMMETRIC="SYMMETRIC" ORDERED="ORDERED"; MONOTONE="MONOTONE"; CONVEX="CONVEX" MONOTONE_PRODUCT="MONOTONE_PRODUCT" CONSERVED="CONSERVED"; MUTABLE="MUTABLE"; NETWORK="NETWORK" EQUILIBRIUM="EQUILIBRIUM"; SUPERPOSITION="SUPERPOSITION" LOCALITY="LOCALITY"; EXTREMAL="EXTREMAL"; ENTROPY="ENTROPY" INJECTIVE="INJECTIVE"; SURJECTIVE="SURJECTIVE"; TRANSITIVE="TRANSITIVE" ATOMIC="ATOMIC"; IMPLICATION="IMPLICATION"; NEGATION="NEGATION" COMPOSITE="COMPOSITE"; HOLISM="HOLISM"; PARSIMONY="PARSIMONY"; DUALITY="DUALITY" ALL_AXIOMS=[getattr(Axiom,a) for a in dir(Axiom) if not a.startswith("__")] AXIOM_ABBR={a:a[:3] for a in ALL_AXIOMS}; AXIOM_ABBR[Axiom.MONOTONE_PRODUCT]="MPR" ADJACENT_CONTRADICTIONS:List[Tuple[str,str]]=[ (Axiom.DISCRETE,Axiom.CONTINUOUS),(Axiom.INJECTIVE,Axiom.SURJECTIVE), (Axiom.ORDERED,Axiom.SYMMETRIC),(Axiom.ATOMIC,Axiom.COMPOSITE), (Axiom.CONSERVED,Axiom.MUTABLE),(Axiom.PARSIMONY,Axiom.ENTROPY), (Axiom.HOLISM,Axiom.LOCALITY),(Axiom.EXTREMAL,Axiom.ENTROPY), (Axiom.NEGATION,Axiom.IMPLICATION),(Axiom.MONOTONE_PRODUCT,Axiom.SYMMETRIC), ] _CONTRA_SET={frozenset(p) for p in ADJACENT_CONTRADICTIONS} def sequence_valid(seq:List[str]) -> bool: for i in range(len(seq)-1): if seq[i]==seq[i+1]: return False if frozenset([seq[i],seq[i+1]]) in _CONTRA_SET: return False return True # ══════════════════════════════════════════════════════════════════════ # SECTION 7: SHARED DATACLASSES # ══════════════════════════════════════════════════════════════════════ RAY_TYPES=["seed","branch","tension","scout","recombine","invert","target"] @dataclass class Hypothesis: hid:str; binding:Dict[str,float]; h_type:str; claim:str derivation:List[str]; pinned_vars:Dict[str,float]; free_vars:List[str] confidence:float; ce:float=float('inf') @dataclass class Baton: binding:Dict[str,float]; ce:float ray_id:str=""; depth:int=0; l9:Optional[L9Certificate]=None @dataclass class AxiomRay: sequence:List[str]; ray_id:str; ray_type:str="seed" depth:int=0; parent_id:Optional[str]=None baton:Optional[Baton]=None; ce_prior:float=float('inf') @property def name(self) -> str: return "→".join(AXIOM_ABBR.get(a,a[:3]) for a in self.sequence) def extend(self,axiom:str,rtype:str,new_prior:float=float('inf')) -> 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,'?')}", ray_type=rtype,depth=self.depth+1, parent_id=self.ray_id,ce_prior=new_prior) return None @dataclass class HypothesisTrace: hid:str; round_idx:int; ray_name:str; ray_type:str ce_before:float; ce_after:float survived:bool; elapsed_ms:float g1_pass:bool=False; g2_pass:bool=False binding:Dict[str,float]=field(default_factory=dict) invariant_results:Dict[str,Tuple[float,bool]]=field(default_factory=dict) tension_class:str="unknown" depth:int=0 @dataclass class StructuralModel: best_binding:Dict[str,float]; best_ce:float failure_patterns:Set[str]=field(default_factory=set) resonant_pairs:List[Tuple[str,str]]=field(default_factory=list) # ══════════════════════════════════════════════════════════════════════ # SECTION 8: HYPOTHESIS CONSTRUCTORS # ══════════════════════════════════════════════════════════════════════ 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(p,bt,a,m): return [_make_hyp("cnt",bt.binding,"continuous","Manifold",[],{},p.variables,0.45)] def _hyp_discrete(p,bt,a,m): b=dict(bt.binding); pinned={} for sn in p.scope_order: svars=p.scope_vars.get(sn,[]); smcs=[p.compiled_constraints[i] for i in p.scope_groups.get(sn,[])] if svars and smcs: box={v:IV(b.get(v,0)-1,b.get(v,0)+1) for v in svars if v in p.bounds} cont=_hc4(box,smcs) if cont: for v,iv in cont.items(): b[v]=iv.mid(); (pinned.update({v:b[v]}) if iv.width()<1e-2 else None) return [_make_hyp("dis",b,"discrete","TopoScope",[],pinned,p.variables,0.80)] def _hyp_quadratic(p,bt,a,m): hyps=[]; b=dict(bt.binding) if bt.l9 and bt.l9.dominant_vars: for v in bt.l9.dominant_vars[:2]: hyps.append(_make_hyp(f"qua_{v}",b,"quadratic",f"Root({v})",[],{v:b[v]},p.variables,0.70)) return hyps def _hyp_bilinear(p,bt,a,m): hyps=[]; b=dict(bt.binding) for vi, vj in p.bilinear_pairs: lo_i,hi_i=p.bounds.get(vi,(0,10)); lo_j,hi_j=p.bounds.get(vj,(0,10)) product=abs(b.get(vi,1)*b.get(vj,1)) if product<=0: continue gm=math.sqrt(product) if lo_i<=gm<=hi_i and lo_j<=gm<=hi_j: nb=dict(b); nb[vi]=nb[vj]=gm hyps.append(_make_hyp(f"bil_eq_{vi}_{vj}",nb,"bilinear", f"GeoMean({vi}={vj}={gm:.3f})",["bilinear"],{vi:gm,vj:gm}, [v for v in p.variables if v not in [vi,vj]],0.70)) for ratio in [0.4, 0.7071, 0.9]: vs=gm*ratio; vl=product/(vs+1e-9) if lo_i<=vs<=hi_i and lo_j<=vl<=hi_j and vsvs: nb3=dict(b); nb3[vi]=vl; nb3[vj]=vs hyps.append(_make_hyp(f"bil_desc_{int(ratio*100)}_{vi}_{vj}",nb3,"bilinear", f"BilDesc({vi}={vl:.3f}>{vj}={vs:.3f})",["bilinear"],{vi:vl,vj:vs}, [v for v in p.variables if v not in [vi,vj]],0.75)) return hyps def _hyp_monotone_product(p,bt,a,m): """ SYSTEM 21.0 FIX: Uses ordering_pairs with correct sign detection. Previously: relied on mc.syms_used[0/1] which is alphabetical sympy ordering. Now: uses p.ordering_pairs which is extracted via _extract_ordering_pair, reading the actual coefficient sign from the parsed expression. For BilinearChain6 "GEQ t2-t1": - Old code: syms_used=['t1','t2'] (alphabetical), took syms_used[0]='t1' as v_small ✓ (coincidence) - Old code: syms_used=['t2','t1'] order could vary → BUG - New code: coeff(t2)=+1 → v_large=t2, coeff(t1)=-1 → v_small=t1 ✓ (always correct) """ hyps=[]; b=dict(bt.binding) if not p.monotone_targets: return hyps tb=_global_hc4_tighten_bounds(p) for v_small, v_large, k in p.monotone_targets: lo_s,hi_s=p.bounds.get(v_small,(-1e18,1e18)) lo_l,hi_l=p.bounds.get(v_large,(-1e18,1e18)) for ratio in [0.1,0.2,0.3,0.4,0.5,0.6,0.707,0.8,0.9,0.95]: vs_sq=k*ratio if vs_sq<=0: continue vs=math.sqrt(vs_sq); vl=k/vs if not(lo_s<=vs<=hi_s and lo_l<=vl<=hi_l and vs<=vl): continue nb=dict(b); nb[v_small]=vs; nb[v_large]=vl box={u:IV(*tb.get(u,p.bounds.get(u,(-10,10)))) for u in p.variables} box[v_small]=IV(vs-1e-6,vs+1e-6) box[v_large]=IV(vl-1e-6,vl+1e-6) cont=_hc4(box,p.compiled_constraints) pinned={v_small:vs,v_large:vl} if cont: for u,iv in cont.items(): if u in p.bounds: nb[u]=iv.mid() pinned={u:nb[u] for u in p.variables if cont[u].width()<1e-2} hyps.append(_make_hyp( f"mpr_{v_small}_{v_large}_r{int(ratio*100)}", nb,"monotone_product", f"MonoProd({v_small}={vs:.4f}≤{v_large}={vl:.4f})", ["ordered","hc4"],pinned, [u for u in p.variables if u not in pinned],0.88)) return hyps def _hyp_metric(p,bt,a,m): return [_make_hyp("met",bt.binding,"metric","Radial",[],{},p.variables,0.75)] def _hyp_symmetric(p,bt,a,m): hyps=[]; b=dict(bt.binding); vl=p.variables if len(vl)>=2: mid=(b.get(vl[0],0)+b.get(vl[1],0))/2; nb=dict(b); nb[vl[0]]=nb[vl[1]]=mid hyps.append(_make_hyp("sym",nb,"symmetric","AveragePin",[],{vl[0]:mid,vl[1]:mid},p.variables,0.60)) return hyps def _hyp_ordered(p,bt,a,m): return [_make_hyp("ord",bt.binding,"ordered","OrderBal",[],{},p.variables,0.67)] def _hyp_monotone(p,bt,a,m): return [_make_hyp("mon",bt.binding,"monotone","MonoPath",[],{},p.variables,0.67)] def _hyp_convex(p,bt,a,m): return [_make_hyp("cvx",bt.binding,"convex","ConvMix",[],{},p.variables,0.63)] def _hyp_conserved(p,bt,a,m): return [_make_hyp("csv",bt.binding,"conserved","Conserve",[],{},p.variables,0.82)] def _hyp_mutable(p,bt,a,m): b=dict(bt.binding) if bt.l9 and bt.l9.dominant_vars: v=bt.l9.dominant_vars[0]; lo,hi=p.bounds.get(v,(-10,10)) b[v]=max(lo,min(hi,b.get(v,0)+random.gauss(0,(hi-lo)*0.05))) return [_make_hyp("mut",b,"mutable","Perturb",[],{},p.variables,0.40)] def _hyp_network(p,bt,a,m): return [_make_hyp("net",bt.binding,"network","HubProp",[],{},p.variables,0.65)] def _hyp_equilibrium(p,bt,a,m): return [_make_hyp("eql",bt.binding,"equilibrium","GradBal",[],{},p.variables,0.72)] def _hyp_superposition(p,bt,a,m): if a and len(a)>0: other=random.choice(a); lam=0.5 nb={v:lam*bt.binding.get(v,0)+(1-lam)*other.binding.get(v,0) for v in p.variables} return [_make_hyp("sup",nb,"superposition","Superpose",[],{},p.variables,0.58)] return [] def _hyp_locality(p,bt,a,m): return [_make_hyp("loc",bt.binding,"locality","LocalFirst",[],{},p.variables,0.72)] def _hyp_extremal(p,bt,a,m): hyps=[]; b=dict(bt.binding) if bt.l9 and bt.l9.dominant_vars: v=bt.l9.dominant_vars[0]; lo,hi=p.bounds.get(v,(0,1)) for val in [lo,hi,(lo+hi)/2]: nb=dict(b); nb[v]=val hyps.append(_make_hyp(f"ext_{v}_{val:.3f}",nb,"extremal", f"PinBound({v}={val:.3f})",[],{v:val},p.variables,0.65)) return hyps def _hyp_entropy(p,bt,a,m): return [_make_hyp("ent",{v:random.uniform(*p.bounds[v]) for v in p.variables},"entropy","MaxEnt",[],{},p.variables,0.48)] def _hyp_injective(p,bt,a,m): return [_make_hyp("inj",bt.binding,"injective","Distinct",[],{},p.variables,0.50)] def _hyp_surjective(p,bt,a,m): return [_make_hyp("sur",bt.binding,"surjective","Sweep",[],{},p.variables,0.45)] def _hyp_transitive(p,bt,a,m): return [_make_hyp("tra",bt.binding,"transitive","TransSnap",[],{},p.variables,0.77)] def _hyp_atomic(p,bt,a,m): hyps=[]; b=dict(bt.binding) for mc in p.compiled_constraints: if not mc.projections: continue for v,projs in mc.projections.items(): for proj in projs: try: val=float(proj["func"](*[b.get(s,0.0) for s in proj["syms"]])) lo,hi=p.bounds.get(v,(-1e18,1e18)) if math.isfinite(val) and lo<=val<=hi: nb=dict(b); nb[v]=val hyps.append(_make_hyp(f"ato_{v}",nb,"atomic",f"Solve({v})",[],{v:val},p.variables,0.70)) break except: pass if hyps: break return hyps def _hyp_implication(p,bt,a,m): return [_make_hyp("imp",bt.binding,"implication","Imply",[],{},p.variables,0.78)] def _hyp_negation(p,bt,a,m): nb={v:max(p.bounds[v][0],min(p.bounds[v][1],(p.bounds[v][0]+p.bounds[v][1])-bt.binding.get(v,(p.bounds[v][0]+p.bounds[v][1])/2))) for v in p.variables} return [_make_hyp("neg",nb,"negation","Mirror",[],{},p.variables,0.42)] def _hyp_composite(p,bt,a,m): return [_make_hyp("cmp",bt.binding,"composite","Enz",[],{},p.variables,0.90)] def _hyp_holism(p,bt,a,m): return [_make_hyp("hol",bt.binding,"holism","Global",[],{},p.variables,0.73)] def _hyp_parsimony(p,bt,a,m): b=dict(bt.binding); nb={} max_val=max((abs(v) for v in b.values()),default=1.0) for v in p.variables: val=b[v]; lo,hi=p.bounds[v] if abs(val)<0.1*max_val and lo<=0.0<=hi: nb[v]=0.0 else: candidates=[round(val*m)/m for m in [1,2,4] if lo<=round(val*m)/m<=hi] nb[v]=min(candidates,key=lambda c:abs(c-val)) if candidates else val return [_make_hyp("par",nb,"parsimony","Occam",[],{},p.variables,0.58)] def _hyp_duality(p,bt,a,m): return [_make_hyp("dua",bt.binding,"duality","Tight",[],{},p.variables,0.68)] AXIOM_CONSTRUCTORS={ 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.MONOTONE_PRODUCT:_hyp_monotone_product, 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 9: CREATIVE SEEDER # ══════════════════════════════════════════════════════════════════════ class CreativeSeeder: def target_seeds(self,anchors:List[AXLInvariant]) -> List[AxiomRay]: seeds=[] for a in anchors: if "*" in a.expr and "**" not in a.expr: seeds.append(AxiomRay([Axiom.BILINEAR],f"TGT_BIL_{a.name}","target")) seeds.append(AxiomRay([Axiom.MONOTONE_PRODUCT],f"TGT_MPR_{a.name}","target")) elif "**2" in a.expr: seeds.append(AxiomRay([Axiom.QUADRATIC],f"TGT_QUA_{a.name}","target")) seeds.append(AxiomRay([Axiom.METRIC],f"TGT_MET_{a.name}","target")) elif "+" in a.expr: seeds.append(AxiomRay([Axiom.CONSERVED],f"TGT_CSV_{a.name}","target")) return seeds def intelligent_branch(self,ray,out_baton,remaining_axioms,branch_width) -> List[AxiomRay]: dom_vars=out_baton.l9.dominant_vars if out_baton.l9 else [] tension_class=out_baton.l9.tension_class if out_baton.l9 else "unknown" n_dom=len(dom_vars) # SYSTEM 21.0: Scale branch width for systemic high-CE problems effective_width = branch_width if tension_class == "systemic" and out_baton.ce > 0.1: effective_width = BRANCH_WIDTH_SYSTEMIC isolated ={Axiom.ATOMIC,Axiom.EXTREMAL,Axiom.MUTABLE,Axiom.DUALITY,Axiom.LOCALITY} relational ={Axiom.SYMMETRIC,Axiom.BILINEAR,Axiom.MONOTONE_PRODUCT, Axiom.ORDERED,Axiom.METRIC,Axiom.INJECTIVE} systemic ={Axiom.CONSERVED,Axiom.NETWORK,Axiom.HOLISM,Axiom.COMPOSITE,Axiom.ENTROPY} scored=[] for ax in remaining_axioms: w=1.0 if n_dom==1 and ax in isolated: w+=5.0 elif n_dom==2 and ax in relational: w+=5.0 elif n_dom>=3 and ax in systemic: w+=5.0 scored.append((w,ax)) scored.sort(key=lambda x:x[0]*random.random(),reverse=True) children=[] for _,axiom in scored[:effective_width]: child=ray.extend(axiom,"branch",new_prior=out_baton.ce) if child: child.baton=out_baton; children.append(child) return children def tension_seeds(self,max_n:int=3000) -> List[AxiomRay]: results=[] for (a,c) in ADJACENT_CONTRADICTIONS: for b1 in ALL_AXIOMS: if b1 in (a,c) or frozenset([a,b1]) in _CONTRA_SET: continue for mid in ALL_AXIOMS: if mid in (a,b1,c) or frozenset([b1,mid]) in _CONTRA_SET: continue for b2 in ALL_AXIOMS: if b2 in (a,b1,mid,c): continue if frozenset([mid,b2]) not in _CONTRA_SET and frozenset([b2,c]) not in _CONTRA_SET: results.append(AxiomRay([a,b1,mid,b2,c], f"T5_{AXIOM_ABBR.get(a,'?')}_{AXIOM_ABBR.get(c,'?')}","tension")) random.shuffle(results); return results[:max_n] def random_scouts(self,n:int=600) -> List[AxiomRay]: scouts=[]; attempts=0 while len(scouts)=length: break if ax!=seq[-1] and frozenset([seq[-1],ax]) not in _CONTRA_SET: seq.append(ax) if len(seq)>=3: scouts.append(AxiomRay(seq,f"SC_{''.join(AXIOM_ABBR.get(a,a[:2]) for a in seq)}","scout")) return scouts def recombine(self,ray_a,ray_b,ba,bb) -> List[AxiomRay]: results=[] for lam in [0.25,0.5,0.75]: ib={v:lam*ba.binding.get(v,0)+(1-lam)*bb.binding.get(v,0) for v in set(list(ba.binding.keys())+list(bb.binding.keys()))} ib_ce=lam*ba.ce+(1-lam)*bb.ce ib_baton=Baton(binding=ib,ce=ib_ce,ray_id="INTERP") cut=min(len(ray_a.sequence),len(ray_b.sequence))//2 if cut>0: seq=ray_a.sequence[:cut]+[x for x in ray_b.sequence[cut:] if x not in ray_a.sequence[:cut]] if sequence_valid(seq): results.append(AxiomRay(seq,f"RC_l{int(lam*100)}","recombine", baton=ib_baton,ce_prior=ib_ce)) return results def invert(self,ray,parent_ce) -> Optional[AxiomRay]: inv=list(reversed(ray.sequence)) if sequence_valid(inv) and inv!=ray.sequence: return AxiomRay(inv,f"INV_{ray.ray_id}","invert",parent_id=ray.ray_id,ce_prior=parent_ce) return None def resonance_extensions(self,ray,parent_ce,resonant_pairs) -> List[AxiomRay]: if not ray.sequence or not resonant_pairs: return [] last=ray.sequence[-1]; results=[] nexts=[b for (a,b) in resonant_pairs if a==last and b!=last and frozenset([a,b]) not in _CONTRA_SET and b not in ray.sequence] for b in nexts: child=ray.extend(b,"branch",new_prior=parent_ce) if child: child.ray_id=f"RES_{child.ray_id}"; results.append(child) return results CREATIVE_SEEDER=CreativeSeeder() # ══════════════════════════════════════════════════════════════════════ # SECTION 10: VERIFY LAYER # ══════════════════════════════════════════════════════════════════════ def _verify(binding:Dict[str,float],base_problem:Problem, anchors:List[AXLInvariant]) -> Tuple[bool,bool,Dict[str,Tuple[float,bool]],float]: g1_ce=base_problem.scalar_energy(binding) g1_pass=g1_ce=-inv.tolerance elif inv.mode=="leq": passed=val<=inv.tolerance else: passed=err=BATON_REGISTRY_MAX: old_key=baton_registry_keys.popleft() baton_registry.pop(old_key,None) baton_registry[ray.ray_id]=out_baton baton_registry_keys.append(ray.ray_id) if improved: best_ce=final_ce; best_binding=dict(final_b) successful_rays.append(ray) model.best_binding=best_binding; model.best_ce=best_ce if overall_pass: solved=True if improved and len(ray.sequence)>=2: pair=(ray.sequence[-2],ray.sequence[-1]) if pair not in resonant_pairs: resonant_pairs.append(pair) model.resonant_pairs=resonant_pairs earned=(final_ce=2: candidates=[r for r in successful_rays if r.ray_id!=ray.ray_id] if candidates: partner=random.choice(candidates) ba=baton_registry.get(ray.ray_id,out_baton) bb=baton_registry.get(partner.ray_id) if bb is not None: new_children.extend(CREATIVE_SEEDER.recombine(ray,partner,ba,bb)[:3]) new_children.extend( CREATIVE_SEEDER.resonance_extensions(ray,final_ce,resonant_pairs)) for child in new_children: if child.ray_type in ("seed","branch","target"): queues["core"].append(child) elif child.ray_type in ("scout","tension"): queues["explore"].append(child) elif child.ray_type in ("recombine","invert"): queues["genetic"].append(child) queues["core"].sort(key=lambda r:r.ce_prior+(r.depth*0.0001)) queues["genetic"].sort(key=lambda r:r.ce_prior+(r.depth*0.0001)) if solved: break return best_binding,best_ce,hero_traces,total_fired,allosteric_counts # ══════════════════════════════════════════════════════════════════════ # SECTION 12: AXL PROBLEMS (14 domains) # ══════════════════════════════════════════════════════════════════════ PROBLEM_META={ "EllipticCurvePoint": {"domain":"Cryptography", "icon":"🔐","difficulty":"Medium"}, "MarkowitzPortfolio": {"domain":"Finance", "icon":"📈","difficulty":"Hard"}, "PowerFlowDC3Bus": {"domain":"Energy", "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("EllipticCurvePoint","E: y²=x³-x+1, x=0", {Axiom.CONTINUOUS,Axiom.QUADRATIC,Axiom.METRIC,Axiom.SYMMETRIC}, [{"name":"ex","lo":-2.0,"hi":2.0},{"name":"ey","lo":-2.0,"hi":2.0}], [{"kind":"EQ","expr":"ey**2 - ex**3 + ex - 1","weight":5.0}],[], [AXLInvariant("on_curve","ey**2 - ex**3 + ex - 1",1e-3)],{"ex":0.0}), AXLProblemDef("MarkowitzPortfolio","4-asset portfolio, return=11%", {Axiom.CONSERVED,Axiom.ORDERED,Axiom.METRIC,Axiom.HOLISM}, [{"name":f"w{i}","lo":0.0,"hi":1.0} for i in range(1,5)], [{"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":f"w{i}"} for i in range(1,5)],[], [AXLInvariant("budget","w1+w2+w3+w4-1.0"), AXLInvariant("ret","0.10*w1+0.12*w2+0.08*w3+0.15*w4-0.11",5e-3)],{}), AXLProblemDef("PowerFlowDC3Bus","DC 3-bus power flow", {Axiom.CONSERVED,Axiom.NETWORK,Axiom.EQUILIBRIUM}, [{"name":"pt2","lo":-1.0,"hi":0.5},{"name":"pt3","lo":-0.5,"hi":0.5}], [{"kind":"EQ","expr":"-2*pt2-3*pt3-0.5","weight":5.0}, {"kind":"EQ","expr":"3*pt2-pt3+1.0","weight":5.0}],[], [AXLInvariant("bus1","-2*pt2-3*pt3-0.5"),AXLInvariant("bus2","3*pt2-pt3+1.0")],{}), AXLProblemDef("ChemEquilibrium","A+B↔C, Kc=4", {Axiom.CONSERVED,Axiom.MONOTONE_PRODUCT,Axiom.BILINEAR}, [{"name":"ca","lo":0.0,"hi":1.0},{"name":"cb","lo":0.0,"hi":1.0}, {"name":"cc","lo":0.0,"hi":1.0}], [{"kind":"CONSERVE","expr":"ca+cc-1.0"},{"kind":"CONSERVE","expr":"cb+cc-1.0"}, {"kind":"EQ","expr":"4*ca*cb-cc","weight":5.0}],[], [AXLInvariant("bal_A","ca+cc-1.0"),AXLInvariant("bal_B","cb+cc-1.0"), AXLInvariant("eq","4*ca*cb-cc")],{}), AXLProblemDef("LorenzFixedPoint","Lorenz σ=10 ρ=28 β=8/3", {Axiom.CONTINUOUS,Axiom.QUADRATIC,Axiom.SYMMETRIC}, [{"name":"lx","lo":-12.0,"hi":12.0},{"name":"ly","lo":-12.0,"hi":12.0}, {"name":"lz","lo":20.0,"hi":35.0}], [{"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}],[], [AXLInvariant("x_eq_y","lx-ly"),AXLInvariant("z_27","lz-27.0"), AXLInvariant("x2_72","lx**2-72.0",0.1)],{}), AXLProblemDef("NashBattleSexes","Mixed Nash p=2/3 q=1/3", {Axiom.CONTINUOUS,Axiom.SYMMETRIC}, [{"name":"np","lo":0.0,"hi":1.0},{"name":"nq","lo":0.0,"hi":1.0}], [{"kind":"EQ","expr":"3*nq-1.0","weight":5.0}, {"kind":"EQ","expr":"3*np-2.0","weight":5.0}],[], [AXLInvariant("p1","3*nq-1.0"),AXLInvariant("p2","3*np-2.0")],{}), AXLProblemDef("KeplerPeriapsis","Orbital: a=1 e=0.5", {Axiom.CONTINUOUS,Axiom.QUADRATIC,Axiom.CONSERVED,Axiom.METRIC}, [{"name":"ka","lo":0.5,"hi":2.0},{"name":"ke","lo":0.0,"hi":0.99}, {"name":"krp","lo":0.1,"hi":2.0},{"name":"kvp","lo":0.5,"hi":5.0}, {"name":"kh","lo":0.1,"hi":3.0}], [{"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}],[], [AXLInvariant("peri","krp-ka*(1-ke)"),AXLInvariant("visviva","kvp**2*krp-(1+ke)"), AXLInvariant("angmom","kh-krp*kvp")],{"ka":1.0,"ke":0.5}), AXLProblemDef("VibratingString3","3-node string s1=s3=1.5 s2=2.0", {Axiom.ORDERED,Axiom.SYMMETRIC,Axiom.METRIC}, [{"name":"s1","lo":0.0,"hi":5.0},{"name":"s2","lo":0.0,"hi":5.0}, {"name":"s3","lo":0.0,"hi":5.0}], [{"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}],[], [AXLInvariant("n1","-2*s1+s2+1.0"),AXLInvariant("n2","s1-2*s2+s3+1.0"), AXLInvariant("n3","s2-2*s3+1.0"),AXLInvariant("sym","s1-s3")],{}), AXLProblemDef("SignalRecovery4","Compressed sensing x=[1,2,0,2]", {Axiom.CONSERVED,Axiom.PARSIMONY,Axiom.INJECTIVE}, [{"name":f"r{i}","lo":0.0,"hi":5.0} for i in range(1,5)], [{"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}],[], [AXLInvariant("m1","r1+r2-3.0"),AXLInvariant("m2","r1+r3-1.0"), AXLInvariant("m3","r2+r4-4.0")],{}), AXLProblemDef("RobotArm2D","2-link arm target=(1.2,0.8)", {Axiom.CONTINUOUS,Axiom.METRIC,Axiom.QUADRATIC}, [{"name":"t1","lo":-3.15,"hi":3.15},{"name":"t2","lo":-3.15,"hi":3.15}], [{"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}],[], [AXLInvariant("rx","cos(t1)+cos(t1+t2)-1.2",1e-2), AXLInvariant("ry","sin(t1)+sin(t1+t2)-0.8",1e-2), AXLInvariant("elbow","cos(t2)-0.04",0.05)],{}), AXLProblemDef("NormManifold4D","Unit sphere zero-sum x1=0.5", {Axiom.CONTINUOUS,Axiom.QUADRATIC,Axiom.CONSERVED,Axiom.METRIC,Axiom.SYMMETRIC}, [{"name":f"x{i}","lo":-1.0,"hi":1.0} for i in range(1,5)], [{"kind":"CONSERVE","expr":"x1**2+x2**2+x3**2+x4**2-1.0"}, {"kind":"EQ","expr":"x1+x2+x3+x4","weight":2.0}],[], [AXLInvariant("sphere","x1**2+x2**2+x3**2+x4**2-1.0"), AXLInvariant("zsum","x1+x2+x3+x4"), AXLInvariant("x1pin","x1-0.5")],{"x1":0.5}), AXLProblemDef("BilinearChain6","6-var ordered chain products 0.5/2.0/4.5", {Axiom.DISCRETE,Axiom.ORDERED,Axiom.BILINEAR,Axiom.MONOTONE_PRODUCT,Axiom.CONSERVED}, [{"name":f"t{i}","lo":0.0,"hi":3.0} for i in range(1,7)], [{"kind":"CONSERVE","expr":"t1+t2+t3+t4+t5+t6-9.0"}]+ [{"kind":"GEQ","expr":f"t{i+1}-t{i}"} for i in range(1,6)]+ [{"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}],[], [AXLInvariant("con","t1+t2+t3+t4+t5+t6-9.0"), AXLInvariant("bil_lo","t1*t2-0.5",0.05), AXLInvariant("bil_mid","t3*t4-2.0",0.05), AXLInvariant("bil_hi","t5*t6-4.5",0.05), AXLInvariant("ord","t2-t1",0.5,"geq")],{}), AXLProblemDef("PhaseCollider","2-particle collision phase branch", {Axiom.DISCRETE,Axiom.MUTABLE,Axiom.SYMMETRIC,Axiom.CONSERVED}, [{"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}], [{"kind":"CONSERVE","expr":"p1x+p2x"},{"kind":"CONSERVE","expr":"p1y+p2y"}], [{"name":"phase","order":0,"constraints":[ {"kind":"EQ","expr":"p1x+p2x","weight":3.0}, {"kind":"EQ","expr":"p1y+p2y","weight":3.0}]}], [AXLInvariant("mx","p1x+p2x"),AXLInvariant("my","p1y+p2y"), AXLInvariant("phase","(p1x**2+p1y**2-0.25)*(p1x**2+p1y**2-1.0)",0.05)],{}), AXLProblemDef("MetricPacking3D","3 vars centred norm²=6 min sep", {Axiom.CONTINUOUS,Axiom.METRIC,Axiom.INJECTIVE,Axiom.CONSERVED}, [{"name":"a","lo":-3.0,"hi":3.0},{"name":"b","lo":-3.0,"hi":3.0}, {"name":"c","lo":-3.0,"hi":3.0}], [{"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}], [{"name":"packing","order":0,"constraints":[ {"kind":"EQ","expr":"a**2+b**2+c**2-6.0","weight":2.0}]}], [AXLInvariant("cen","a+b+c"),AXLInvariant("norm6","a**2+b**2+c**2-6.0",0.05), AXLInvariant("sab","(a-b)**2-1.0",0.0,"geq"), AXLInvariant("sbc","(b-c)**2-1.0",0.0,"geq")],{}), ] 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) # ══════════════════════════════════════════════════════════════════════ # SECTION 13: GLOBAL STATE # ══════════════════════════════════════════════════════════════════════ STATE_LOCK = threading.Lock() IS_RUNNING = False PROBLEM_STATS:Dict[str,Dict]={p.name:{ "runs":0,"solved":0,"total_ce":0.0,"best_ce":float('inf'), "best_binding":{},"best_ray":"—", "type_stats":{t:{"tried":0,"survived":0} for t in RAY_TYPES}, "allosteric":{"isolated":0,"relational":0,"systemic":0}, } for p in AXL_PROBLEMS} RECENT_RUNS:List[Dict]=[] MAX_RECENT=30 _PROB_IDX=0 def background_worker(): global IS_RUNNING, _PROB_IDX tracer=SequenceRayTracer() while IS_RUNNING: axl_def=AXL_PROBLEMS[_PROB_IDX%len(AXL_PROBLEMS)]; _PROB_IDX+=1 base_prob=build_base_problem(axl_def) t0=time.time() binding,ce,traces,total_fired,allosteric=tracer.trace(axl_def,base_prob) ms=round((time.time()-t0)*1000) survived=[t for t in traces if t.survived] solved=len(survived)>0 and ceMAX_RECENT: RECENT_RUNS.pop() ps=PROBLEM_STATS[axl_def.name] ps["runs"]+=1; ps["total_ce"]+=ce if solved: ps["solved"]+=1 if ce str: rows="" for prob in AXL_PROBLEMS: ps=PROBLEM_STATS[prob.name]; meta=PROBLEM_META.get(prob.name,{}) if ps["runs"]==0: rows+=(f"{meta.get('icon','·')}" f"{prob.name}" f"warming up…") continue runs=ps["runs"]; rate=round(ps["solved"]/runs*100) avg_ce=round(ps["total_ce"]/runs,5) rc=ps["type_stats"] type_cells="".join( f"0 else '#333'};font-size:0.75em'>" f"{RAY_ICONS.get(t,'·')}{round(rc[t]['survived']/rc[t]['tried']*100) if rc[t]['tried'] else 0}%" for t in ["seed","tension","scout","recombine","invert","branch"]) rate_col="#4CAF50" if rate>=50 else ("#FF9800" if rate>=20 else "#EF5350") al=ps["allosteric"]; total_al=sum(al.values()) or 1 dom_class=max(al,key=al.get) rows+=(f"" f"{meta.get('icon','·')}" f"{prob.name}" f"{meta.get('domain','')}" f"{meta.get('difficulty','')}" f"{runs}" f"{rate}%" f"{avg_ce}" f"{ps['best_ce']:.5f}" f"{type_cells}" f"{dom_class}" f"") return rows def _render_type_table() -> str: global_stats={t:{"tried":0,"survived":0} for t in RAY_TYPES} for ps in PROBLEM_STATS.values(): for rt,counts in ps["type_stats"].items(): global_stats[rt]["tried"]+=counts["tried"] global_stats[rt]["survived"]+=counts["survived"] desc={ "seed":"Greedy depth-first from single axiom", "branch":"Allosteric feedback-guided child — width 12 (16 for systemic)", "tension":"Mediated contradiction [A→B1→M→B2→C] length 5", "scout":"Random length 3-12 cartographer", "recombine":"Genetic crossover + interpolated baton geometry", "invert":"Reversed successful sequence", "target":"Bidirectional: spawned from goal state invariants", } rows="" for rt,s in global_stats.items(): rate=round(s['survived']/s['tried']*100) if s['tried'] else 0 c="#4CAF50" if rate>0 else "#333" rows+=(f"{RAY_ICONS.get(rt,'·')}" f"{rt}" f"{s['tried']}" f"{s['survived']}" f"{s['tried']-s['survived']}" f"{rate}%" f"{desc.get(rt,'')}") return rows def _render_allosteric_table() -> str: totals={"isolated":0,"relational":0,"systemic":0} for ps in PROBLEM_STATS.values(): for tc,cnt in ps["allosteric"].items(): totals[tc]=totals.get(tc,0)+cnt grand=sum(totals.values()) or 1 rows="" desc={"isolated":"1 dominant var → ATOMIC/EXTREMAL/DUALITY", "relational":"2 dominant vars → BILINEAR/MPR/ORDERED/METRIC", "systemic":"3+ dominant vars → CONSERVED/NETWORK/HOLISM (branch×16)"} for tc,cnt in totals.items(): pct=round(cnt/grand*100) rows+=(f"{tc}" f"{cnt:,}" f"{pct}%" f"{desc.get(tc,'')}") return rows def _render_recent() -> str: with STATE_LOCK: log=list(RECENT_RUNS[:8]) if not log: return "
No runs yet.
" html="" for r in log: ce=r["ce"]; solved=r["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}" for v,val in list(r.get("binding",{}).items())[:6]) inv_rows="" best_t=next((t for t in r.get("traces",[]) if t["survived"]), r["traces"][0] if r.get("traces") else None) if best_t and best_t.get("invariants"): for inv,(val,ok) in best_t["invariants"].items(): c="#4CAF50" if ok else "#EF5350" inv_rows+=(f"{'✓' if ok else '✗'}" f"{inv}" f"{val:.5f}") tc=r.get("type_counts",{}) type_badges="".join( f"" f"{RAY_ICONS.get(t,'·')}{t[:3]}" f"0 else '#333'}'>" f"{round(tc.get(t,{}).get('survived',0)/tc.get(t,{}).get('tried',1)*100) if tc.get(t,{}).get('tried',0) else 0}%" for t in ["seed","tension","scout","recombine","invert","branch","target"]) ray_trail="" for t in r.get("traces",[])[:15]: icon=RAY_ICONS.get(t.get("ray_type","seed"),"·") c="#4CAF50" if t["survived"] else "#333" star=" ◀" if t["survived"] else "" ray_trail+=(f"
" f"{icon}[{t.get('ray','')}] CE={t['ce']:.4f} " f"G1={'✓' if t['g1'] else '✗'} G2={'✓' if t['g2'] else '✗'} " f"{t.get('tension','?')[:3]}" f"{star}
") html+=(f"
" f"
" f"{status}" f"{r.get('icon','·')} {r['problem']}" f"{r.get('domain','')}" f"CE={ce:.6f}" f"{r['survived_count']} survived / {r['total_fired']:,} fired" f"{type_badges}
" f"
" f"
" f"
BINDING
" f"{binding_rows}
" f"
" f"
INVARIANTS
" f"" f"{inv_rows or ''}
—
" f"
" f"
" f"RAY TREE — best: {r.get('best_ray','—')}
" f"{ray_trail}
") return html def refresh_dashboard(): with STATE_LOCK: runs =sum(s["runs"] for s in PROBLEM_STATS.values()) solved =sum(s["solved"] for s in PROBLEM_STATS.values()) total_ce=sum(s["total_ce"] for s in PROBLEM_STATS.values()) avg_ce=round(total_ce/runs,5) if runs else 0 perf =_render_perf_table() types=_render_type_table() allos=_render_allosteric_table() recnt=_render_recent() return f"""

⚗ Practicality 21.0 — MPR Ordering Fix + Branch Width 12

Fix: _extract_ordering_pair reads coefficient signs (not alphabetical sympy ordering) · Branch width 12 (16 for systemic tension) · Pre-compiled anchors · 12K batch
Runs: {runs} Solved: {solved} Avg CE: {avg_ce} Problems: {len(AXL_PROBLEMS)} Axioms: {len(ALL_AXIOMS)} Device: {DEVICE.type.upper()}

Creative Ray Type Efficacy

{types}
TypeTriedSurvivedFailedRateMechanism (21.0)

Allosteric Feedback Diagnostics

{allos}
Tension ClassFiredShareBiases Toward

Multi-Domain Performance

{perf}
ProblemDomainDiffRunsRate% Avg CEBest CE 🌱⚡🔭🧬🔄🌿 Dom Tension

Recent Runs

{recnt}
""" with gr.Blocks(theme=gr.themes.Monochrome(text_size="sm"),title="Practicality 21.0") as demo: gr.Markdown("## ⚗ Practicality 21.0 — MPR Ordering Fix + Branch Width 12") gr.Markdown( f"**Compute:** `{DEVICE.type.upper()}` | " f"**Fix:** `_extract_ordering_pair` reads coefficient signs · " f"**Branch:** 12 default / 16 systemic") with gr.Row(): btn=gr.Button("▶ START 21.0",variant="primary") gr.Markdown("*Engine cycles through 14 domains. Dashboard auto-refreshes every 2s.*") html_out=gr.HTML(refresh_dashboard()) btn.click(toggle_engine,inputs=None,outputs=btn) def auto_refresh(): while True: time.sleep(2.0) yield refresh_dashboard() demo.load(auto_refresh,inputs=None,outputs=html_out) if __name__=="__main__": print(f"[SYSTEM 21.0] Launching on 0.0.0.0:7860 | MPR Fix + Branch-12") demo.launch(server_name="0.0.0.0",server_port=7860,share=False)