Update app.py

app.py

@@ -1 +1,1511 @@
-h
+#!/usr/bin/env python3
+"""
+PRACTICALITY UNIFIED SERVER 22.1 — LATEST GEMINI SDK & STRICT BOUNDARY
+═══════════════════════════════════════════════════════════════════
+ARCHITECTURE:
+  User Text → [GEMINI 3.1 ENCODER] → AXLProblemDef (Strict Math Representation)
+            → [WISDOM LAYER]       → Hypothesis Engine (CreativeSeeder) generates Axiom rays
+                                   → PyTorch Masked Deduction + Oracle solves topology
+                                   → Verification (Gate 1 & Gate 2)
+                                   → [Self-Correcting Feedback Loop if G2 fails]
+            → [GEMINI 3.1 COLLAPSER] → Domain-language explanation
+
+LATEST UPDATES (22.1):
+  - Migrated to the new `google-genai` SDK.
+  - Implemented `gemini-3.1-pro-preview` with `ThinkingConfig` for maximum semantic routing.
+  - Top-level API key configuration for rapid deployment.
+"""
+
+import os, time, random, math, threading, warnings, queue, json, textwrap
+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
+
+# ── NEW GOOGLE GENAI SDK ──────────────────────────────────────────
+from google import genai
+from google.genai import types
+
+# ══════════════════════════════════════════════════════════════════
+# AI CONFIGURATION (Set your key here!)
+# ══════════════════════════════════════════════════════════════════
+DEFAULT_GEMINI_API_KEY = os.environ.get("GEMINI_API_KEY", "")
+GEMINI_MODEL = "gemini-3.1-pro-preview"
+
+warnings.filterwarnings("ignore")
+USE_GPU = torch.cuda.is_available()
+DEVICE  = torch.device("cuda" if USE_GPU else "cpu")
+print(f"[UNIFIED SERVER] Compute: {DEVICE.type.upper()} | System 22.1 (GenAI SDK + Neuro-Symbolic Boundary)")
+
+# ══════════════════════════════════════════════════════════════════════
+# 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
+BRANCH_WIDTH_SYSTEMIC    = 16
+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<len(lines) else ""
+    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): 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 i<len(lines):
+            l=peek(); tk=l.split(None,1); kw=tk[0].upper() if tk else ""; rest=tk[1].strip() if len(tk)>1 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 i<len(lines) and not peek().upper().startswith("END"):
+                    bl=advance(); opts.append(bl.split(None,1)[1].strip()) if bl.upper().startswith("OPTION") else None
+                advance(); scons.append(PSLConstraint("or_eq","",scope=sname,weight=1.0,branches=opts))
+        return PSLScope(sname,order,depends or [],svars,links,scons)
+    while i<len(lines):
+        l=advance(); tk=l.split(None,1); kw=tk[0].upper() if tk else ""; rest=tk[1].strip() if len(tk)>1 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<len(lines) and not peek().upper().startswith("END"):
+                bl=advance(); opts.append(bl.split(None,1)[1].strip()) if bl.upper().startswith("OPTION") else None
+            advance(); prog.constraints.append(PSLConstraint("or_eq","",weight=1.0,branches=opts))
+        elif kw=="SCOPE":
+            parts=rest.split(); sname=parts[0] if parts else f"s{len(prog.scopes)}"; order=0; depends=[]
+            if "ORDER" in rest.upper():
+                try: order=int(rest[rest.upper().index("ORDER"):].split()[1])
+                except: pass
+            if "DEPENDS" in rest.upper(): depends=rest[rest.upper().index("DEPENDS"):].split()[1:]
+            sc=parse_scope_body(sname,order,depends); prog.scopes.append(sc); prog.scope_order.append(sname)
+    prog.scopes.sort(key=lambda s:s.order); prog.scope_order=[s.name for s in prog.scopes]
+    return prog
+
+@dataclass
+class ExpandedProblem:
+    variables:List[str]; bounds:Dict[str,Tuple[float,float]]; constraints:List['Constraint']
+    scope_groups:Dict[str,List[int]]; scope_vars:Dict[str,List[str]]; scope_order:List[str]
+
+def expand_psl(prog:PSLProgram) -> 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]]:
+    if mc.kind != "inequality" or mc.direction != "geq": return None
+    if mc.parsed is None: return None
+    parsed = mc.parsed
+    free = [str(s) for s in parsed.free_symbols if str(s) in variables]
+    if len(free) != 2: return None
+    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
+    if c0 > 0 and c1 < 0: return (v1, v0)
+    elif c1 > 0 and c0 < 0: return (v0, v1)
+    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) 
+
+    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)}
+
+        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)
+
+        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))
+
+        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:
+                            k_expr = -(mc.parsed - sa*sb)
+                            k = float(k_expr.evalf())
+                            if k > 0:
+                                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
+
+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 5: BATCHED MASKED DEDUCTION & ORACLE
+# ══════════════════════════════════════════════════════════════════════
+@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<SOLVE_THRESHOLD).all(): break
+        loss=ce.sum(); loss.backward()
+        with torch.no_grad():
+            X.grad*=mask
+            optimizer.step()
+            X.data=torch.where(mask==0.0,target,X.data)
+            for j,v in enumerate(problem.variables):
+                lo,hi=problem.bounds[v]
+                X.data[:,j]=torch.clamp(X.data[:,j],lo,hi)
+
+    optimizer.zero_grad()
+    final_ce=problem.tensor_energy(X)
+    final_ce.sum().backward()
+
+    ce_vals = final_ce.detach().cpu().numpy()
+    X_vals  = X.detach().cpu().numpy()
+
+    grads_abs = X.grad.abs()
+    _, topk_idx = torch.topk(grads_abs, k=min(3, V), dim=1)
+    topk_idx_np = topk_idx.cpu().numpy()
+    grads_np = grads_abs.cpu().numpy()
+
+    results=[]
+    for i in range(B):
+        final_b={problem.variables[j]:float(X_vals[i,j]) for j in range(V)}
+        dom_vars = [problem.variables[idx] for idx in topk_idx_np[i] if float(grads_np[i, idx]) > 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 vs<vl:
+                nb2=dict(b); nb2[vi]=vs; nb2[vj]=vl
+                hyps.append(_make_hyp(f"bil_asc_{int(ratio*100)}_{vi}_{vj}",nb2,"bilinear",f"BilAsc({vi}={vs:.3f}<{vj}={vl:.3f})",["bilinear"],{vi:vs,vj:vl},[v for v in p.variables if v not in [vi,vj]],0.75))
+            if lo_i<=vl<=hi_i and lo_j<=vs<=hi_j and vl>vs:
+                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):
+    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)
+        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)<n and attempts<n*30:
+            attempts+=1; length=random.randint(3,12)
+            pool=list(ALL_AXIOMS); random.shuffle(pool); seq=[pool[0]]
+            for ax in pool[1:]:
+                if len(seq)>=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<VERIFY_G1_THRESHOLD
+    g2={}
+    for inv in anchors:
+        try:
+            if inv.compiled_func: val = float(inv.compiled_func(*[binding.get(v, 0.0) for v in inv.syms_used]))
+            else: val = 999.0
+            err=abs(val)
+            if inv.mode=="eq":    passed=err<inv.tolerance
+            elif inv.mode=="geq": passed=val>=-inv.tolerance
+            elif inv.mode=="leq": passed=val<=inv.tolerance
+            else:                 passed=err<inv.tolerance
+            g2[inv.name]=(round(val if inv.mode in ("geq","leq") else err,6),passed)
+        except: g2[inv.name]=(999.0,False)
+    g2_pass=all(v[1] for v in g2.values()) if g2 else True
+    return g1_pass,g2_pass,g2,round(g1_ce,6)
+
+# ══════════════════════════════════════════════════════════════════════
+# SECTION 11: SEQUENCE RAY TRACER
+# ══════════════════════════════════════════════════════════════════════
+class SequenceRayTracer:
+    def trace(self,axl_def:AXLProblemDef,base_problem:Problem):
+        hero_traces:List[HypothesisTrace]=[]
+        baton_registry:Dict[str,Baton]={}
+        baton_registry_keys:deque=deque()
+        successful_rays:List[AxiomRay]=[]
+        resonant_pairs:List[Tuple[str,str]]=[]
+
+        for inv in axl_def.anchors:
+            if not inv.compiled_func:
+                inv.compile(base_problem.variables)
+
+        init_b,init_ce=_mprt_sample(base_problem,
+            {v:IV(*base_problem.bounds[v]) for v in base_problem.variables},N_MPRT_EXPLORE)
+        seed_baton=Baton(binding=init_b,ce=init_ce,ray_id="SEED",
+                         l9=L9Certificate(init_ce,base_problem.variables[:3],[],"systemic"))
+
+        queues={
+            "core":[AxiomRay([a],f"S{i}","seed",ce_prior=init_ce) for i,a in enumerate(ALL_AXIOMS)],
+            "explore":CREATIVE_SEEDER.tension_seeds(3000)+CREATIVE_SEEDER.random_scouts(600),
+            "genetic":CREATIVE_SEEDER.target_seeds(axl_def.anchors),
+        }
+        for q in queues.values(): random.shuffle(q)
+
+        queue_order=["core","explore","genetic"]; q_idx=0
+        best_ce=init_ce; best_binding=dict(init_b); total_fired=0
+        model=StructuralModel(best_binding,best_ce)
+        allosteric_counts={"isolated":0,"relational":0,"systemic":0}
+
+        while total_fired<MAX_TOTAL_RAYS:
+            batch_rays:List[AxiomRay]=[]
+            for _ in range(RAY_BATCH_SIZE):
+                start_idx=q_idx
+                while not queues[queue_order[q_idx]]:
+                    q_idx=(q_idx+1)%3
+                    if q_idx==start_idx: break
+                if not any(queues[k] for k in queue_order): break
+                ray=queues[queue_order[q_idx]].pop(0); q_idx=(q_idx+1)%3
+                batch_rays.append(ray); total_fired+=1
+            if not batch_rays: break
+
+            t0=time.time()
+            historical_batons=list(baton_registry.values())
+
+            batch_hyps:List[Tuple[int,Hypothesis]]=[]
+            for i,ray in enumerate(batch_rays):
+                p_baton=ray.baton or seed_baton
+                constructor=AXIOM_CONSTRUCTORS.get(ray.sequence[-1])
+                hyps=constructor(base_problem,p_baton,historical_batons,model) if constructor else []
+                if not hyps: hyps=[_make_hyp("fb",p_baton.binding,"fallback","Pass",[],{},base_problem.variables,0.1)]
+                batch_hyps.append((i,hyps[0]))
+
+            eval_results=_batched_deduce_and_evaluate(base_problem,[h for _,h in batch_hyps])
+            elapsed_ms=(time.time()-t0)*1000/max(1,len(batch_rays))
+
+            solved=False
+            for (ray_idx,hyp),(final_b,final_ce,dom_vars,tension_class) in zip(batch_hyps,eval_results):
+                ray=batch_rays[ray_idx]
+                parent_ce=(ray.baton or seed_baton).ce
+                allosteric_counts[tension_class]=allosteric_counts.get(tension_class,0)+1
+
+                g1_pass,g2_pass,inv_results,g1_ce=_verify(final_b,base_problem,axl_def.anchors)
+                overall_pass=g1_pass and g2_pass
+
+                improved=final_ce<best_ce
+                if improved or overall_pass or random.random()<0.002:
+                    hero_traces.append(HypothesisTrace(
+                        hid=ray.ray_id,round_idx=total_fired-len(batch_rays)+ray_idx,
+                        ray_name=ray.name,ray_type=ray.ray_type,
+                        ce_before=parent_ce,ce_after=final_ce,
+                        survived=overall_pass,elapsed_ms=elapsed_ms,
+                        g1_pass=g1_pass,g2_pass=g2_pass,
+                        binding={k:round(v,5) for k,v in final_b.items()},
+                        invariant_results=inv_results,
+                        tension_class=tension_class,depth=ray.depth))
+
+                out_baton=Baton(binding=final_b,ce=final_ce,ray_id=ray.ray_id,
+                                l9=L9Certificate(final_ce,dom_vars,[],tension_class))
+
+                if final_ce<BATON_REGISTRY_THRESHOLD:
+                    if ray.ray_id in baton_registry:
+                        baton_registry[ray.ray_id]=out_baton
+                    else:
+                        if len(baton_registry)>=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<parent_ce*CE_EARN_RATIO or ray.depth<1)
+                scout_earned=(ray.ray_type=="scout" and final_ce<SCOUT_CE_THRESHOLD)
+
+                if earned or scout_earned:
+                    remaining=[a for a in ALL_AXIOMS
+                                if a!=ray.sequence[-1]
+                                and frozenset([ray.sequence[-1],a]) not in _CONTRA_SET
+                                and a not in ray.sequence]
+
+                    new_children:List[AxiomRay]=[]
+                    new_children.extend(
+                        CREATIVE_SEEDER.intelligent_branch(ray,out_baton,remaining,BRANCH_WIDTH))
+                    inv=CREATIVE_SEEDER.invert(ray,final_ce)
+                    if inv: new_children.append(inv)
+
+                    if len(successful_rays)>=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: LLM BRIDGE (GOOGLE GENAI 3.1)
+# ══════════════════════════════════════════════════════════════════
+
+ENCODER_SYSTEM_PROMPT = """You are the Encoder for the Practicality Wisdom Layer — a neuro-symbolic
+constraint satisfaction engine. Your job is STRICT SLOT-FILLING, not reasoning.
+You read a natural language problem description and produce a structured
+JSON object that represents its mathematical constraints.
+
+You do NOT solve the problem. You do NOT guess the structural topology. You only translate.
+
+══════════════════════════════════════════════════════════════════
+PART 1: THE AXL STRUCTURE
+══════════════════════════════════════════════════════════════════
+
+You must output a single JSON object matching this schema exactly:
+
+{
+  "name":        string,          // CamelCase, no spaces
+  "description": string,          // one sentence
+  "variables": [
+    {
+      "name": string,   // short lowercase identifier (x, v1, theta, etc.)
+      "lo":   number,   // OPTIONAL: ONLY provide if the problem explicitly limits this (e.g., > 0)
+      "hi":   number    // OPTIONAL: ONLY provide if the problem explicitly limits this
+    }
+  ],
+  "constraints": [
+    {
+      "kind":   "EQ" | "GEQ" | "LEQ" | "CONSERVE",
+      "expr":   string,   // valid Python/sympy expression using variable names
+      "weight": number    // 1.0 default; 5.0 for hard constraints; 10.0 for conservation laws
+    }
+  ],
+  "anchors": [
+    {
+      "name":      string,   // snake_case identifier for this condition
+      "expr":      string,   // sympy expression that equals 0 when satisfied
+      "tolerance": number,   // how close to 0 counts as solved (default 0.001)
+      "mode":      "eq" | "geq" | "leq"
+    }
+  ],
+  "observations": {
+    "variable_name": number   // variables whose values are STRICTLY KNOWN/FIXED in the prompt
+  }
+}
+
+CRITICAL: Output ONLY the JSON object. No preamble, no markdown fences.
+
+══════════════════════════════════════════════════════════════════
+PART 2: ENCODING RULES
+══════════════════════════════════════════════════════════════════
+
+VARIABLES & BOUNDS:
+  • Use short names: x, y, v, w1, cb
+  • DO NOT INVENT BOUNDS. If the text says "probabilities", set lo=0.0, hi=1.0. 
+    If the text says nothing, omit "lo" and "hi" entirely.
+  • Fixed values go in "observations", not as tight bounds.
+  • DO include observed variables in the variables list. The engine handles pinning.
+
+CONSTRAINTS & ANCHORS:
+  • EQ: expr = 0 (e.g., "x**2 + y**2 - 1.0")
+  • GEQ: expr ≥ 0
+  • LEQ: expr ≤ 0
+  • CONSERVE: inviolable laws (weight 10.0 automatically)
+  • Expressions must be valid Python/sympy: use **, *, +, -, /
+  • Do NOT use =, >=, <= in expressions — only the expression that evaluates against 0.
+  • Anchors are the verification conditions. What MUST be true to accept the solution?
+
+══════════════════════════════════════════════════════════════════
+PART 3: FAILURE HANDLING
+══════════════════════════════════════════════════════════════════
+
+If a previous solve attempt is included in the user message showing
+failed invariants, revise the encoding to better capture those conditions. 
+Common fixes:
+  • Invariant fails with large value → increase constraint weight
+  • Wrong sign → swap GEQ to LEQ or negate expr
+  • Missing constraint → add missing physical law as EQ or CONSERVE
+
+Output ONLY the JSON. No preamble.
+"""
+
+COLLAPSER_SYSTEM_PROMPT = """You are the Collapser for the Practicality Wisdom Layer. You receive
+a JSON object containing:
+  • The original natural language problem
+  • The problem name and description
+  • Whether the solver succeeded (solved/partial/unsolved)
+  • The verified variable binding (the numerical solution)
+  • Gate 1 result: global constraint energy (mathematical validity)
+  • Gate 2 results: named invariant checks (domain correctness)
+  • The best axiom ray sequence that found the solution
+  • Total rays fired
+
+Your job is to translate this back into clear, domain-appropriate
+natural language that a human expert in the problem domain would
+recognize as correct and useful.
+
+══════════════════════════════════════════════════════════════════
+TONE AND FORMAT RULES
+══════════════════════════════════════════════════════════════════
+• Write for a domain expert, not a general audience
+• Use domain-appropriate variable names and units if discernible
+• Lead with the status: SOLVED / PARTIAL / UNSOLVED
+• Report the binding values in the order they appear in the problem
+• For each Gate 2 invariant:
+    - If passed: briefly confirm what physical condition is satisfied
+    - If failed: explain specifically what condition was NOT met
+      and by how much (the numerical value is provided)
+• Keep it under 250 words
+• End with the axiom sequence that found the solution, formatted
+  as a one-line note
+"""
+
+def encode_problem_to_axl(problem_text: str, api_key: str) -> AXLProblemDef:
+    """Uses Google GenAI to slot-fill the text into the AXL structural JSON."""
+    if not api_key:
+        raise ValueError("Gemini API Key is missing. Please provide it in the UI or set it globally.")
+    
+    client = genai.Client(api_key=api_key)
+    
+    config = types.GenerateContentConfig(
+        system_instruction=[types.Part.from_text(text=ENCODER_SYSTEM_PROMPT)],
+        response_mime_type="application/json",
+        temperature=0.1,
+    )
+    
+    response = client.models.generate_content(
+        model=GEMINI_MODEL,
+        contents=problem_text,
+        config=config,
+    )
+    
+    return _parse_axl_json(response.text)
+
+def _parse_axl_json(raw_json: str) -> AXLProblemDef:
+    """Parses Gemini JSON output into the strict AXL structural definition."""
+    text = raw_json.strip()
+    if text.startswith("```"):
+        text = text.split("```")[1]
+        if text.startswith("json"):
+            text = text[4:]
+    text = text.strip().rstrip("`").strip()
+
+    d = json.loads(text)
+    anchors = [
+        AXLInvariant(
+            name=a["name"], expr=a["expr"],
+            tolerance=a.get("tolerance", VERIFY_G2_TOLERANCE),
+            mode=a.get("mode", "eq")
+        )
+        for a in d.get("anchors", [])
+    ]
+    
+    variables = []
+    for v in d["variables"]:
+        variables.append({
+            "name": v["name"],
+            "lo": float(v.get("lo", -1e18)), 
+            "hi": float(v.get("hi", 1e18))
+        })
+
+    return AXLProblemDef(
+        name=d["name"],
+        description=d.get("description", ""),
+        axioms=set(), # Engine owns Axioms, not the LLM
+        variables=variables,
+        constraints=d.get("constraints", []),
+        scopes=d.get("scopes", []),
+        anchors=anchors,
+        observations=d.get("observations", {}),
+    )
+
+def collapse_solution(
+    problem_text: str,
+    axl_def: AXLProblemDef,
+    binding: Dict[str, float],
+    g1_pass: bool,
+    g2_pass: bool,
+    invariant_results: Dict[str, Tuple[float, bool]],
+    best_ray: str,
+    total_fired: int,
+    api_key: str
+) -> str:
+    """Uses Google GenAI with high-level thinking to collapse PyTorch findings to Natural Language."""
+    if not api_key:
+        return "ERROR: Gemini API Key required for semantic collapsing."
+        
+    client = genai.Client(api_key=api_key)
+    
+    payload = {
+        "original_problem": problem_text,
+        "problem_name":     axl_def.name,
+        "solved":           g1_pass and g2_pass,
+        "gate1_pass":       g1_pass,
+        "gate2_pass":       g2_pass,
+        "binding":          {k: round(v, 6) for k, v in binding.items()},
+        "invariant_results":invariant_results,
+        "best_ray_sequence":best_ray,
+        "rays_fired":       total_fired,
+    }
+    
+    config = types.GenerateContentConfig(
+        thinking_config=types.ThinkingConfig(thinking_level="HIGH"),
+        system_instruction=[types.Part.from_text(text=COLLAPSER_SYSTEM_PROMPT)],
+        temperature=0.2,
+    )
+    
+    response = client.models.generate_content(
+        model=GEMINI_MODEL,
+        contents=json.dumps(payload, indent=2),
+        config=config,
+    )
+    
+    return response.text
+
+# ══════════════════════════════════════════════════════════════════
+# SECTION 13: STREAMING SOLVER RUNNER WITH FEEDBACK LOOP
+# ══════════════════════════════════════════════════════════════════
+
+def run_solve_streaming(original_problem_text: str, api_key: str):
+    """
+    Generator that wires Encode → Compile → PyTorch Solve → Verify → Collapse.
+    Includes the self-correcting feedback loop if Gate 2 (Invariants) fails.
+    """
+    log_lines: List[str] = []
+    answer_text = ""
+    MAX_ATTEMPTS = 3
+
+    def emit(line: str):
+        log_lines.append(line)
+        return "\n".join(log_lines), answer_text
+
+    current_text = original_problem_text
+    used_key = api_key or DEFAULT_GEMINI_API_KEY
+
+    for attempt in range(1, MAX_ATTEMPTS + 1):
+        yield emit(f"🔍 **Encoding problem (Attempt {attempt}/{MAX_ATTEMPTS})…**\n")
+        t0 = time.time()
+        
+        try:
+            axl_def = encode_problem_to_axl(current_text, used_key)
+        except Exception as e:
+            yield emit(f"✗ Encoding failed: {e}\n")
+            return
+
+        enc_ms = round((time.time() - t0) * 1000)
+        yield emit(
+            f"✓ **Encoded** as `{axl_def.name}` ({enc_ms} ms)\n"
+            f"  Variables: `{', '.join(v['name'] for v in axl_def.variables)}`\n"
+            f"  Anchors: {len(axl_def.anchors)}\n\n"
+            f"⚙ **Compiling AXL → PSL…**\n"
+        )
+
+        try:
+            base_prob = build_base_problem(axl_def)
+        except Exception as e:
+            yield emit(f"✗ Compilation failed: {e}\n")
+            return
+
+        yield emit(
+            f"✓ **Compiled**: {len(base_prob.variables)} vars, "
+            f"{len(base_prob.compiled_constraints)} constraints\n"
+            f"  Bilinear pairs: {len(base_prob.bilinear_pairs)}\n"
+            f"  Monotone targets: {len(base_prob.monotone_targets)}\n\n"
+            f"🚀 **Running wisdom layer (PyTorch Search)…**\n"
+        )
+
+        result_q: queue.Queue = queue.Queue()
+
+        def _worker():
+            try:
+                tracer = SequenceRayTracer()
+                binding, ce, traces, total_fired, allosteric = tracer.trace(axl_def, base_prob)
+                result_q.put(("ok", binding, ce, traces, total_fired, allosteric))
+            except Exception as e:
+                result_q.put(("err", str(e)))
+
+        worker_thread = threading.Thread(target=_worker, daemon=True)
+        worker_thread.start()
+
+        dots = 0
+        while worker_thread.is_alive():
+            worker_thread.join(timeout=3.0)
+            if worker_thread.is_alive():
+                dots += 1
+                yield emit(f"  ·{'·' * dots} still searching ({dots * 3}s)…\n")
+
+        if result_q.empty():
+            yield emit("✗ Solver returned no result.\n")
+            return
+
+        result = result_q.get()
+        if result[0] == "err":
+            yield emit(f"✗ Solver error: {result[1]}\n")
+            return
+
+        _, binding, ce, traces, total_fired, allosteric = result
+        survived = [t for t in traces if t.survived]
+        best_t   = min(survived, key=lambda t: t.ce_after, default=None)
+
+        for inv in axl_def.anchors:
+            if not inv.compiled_func:
+                inv.compile(base_prob.variables)
+
+        g1_ce   = base_prob.scalar_energy(binding)
+        g1_pass = g1_ce < VERIFY_G1_THRESHOLD
+        inv_results: Dict[str, Tuple[float, bool]] = {}
+        for inv in axl_def.anchors:
+            try:
+                val = float(inv.compiled_func(*[binding.get(v, 0.0) for v in inv.syms_used]))
+                err = abs(val)
+                if inv.mode == "eq":    passed = err < inv.tolerance
+                elif inv.mode == "geq": passed = val >= -inv.tolerance
+                else:                   passed = val <= inv.tolerance
+                inv_results[inv.name] = (round(val, 6), passed)
+            except:
+                inv_results[inv.name] = (999.0, False)
+        g2_pass = all(v[1] for v in inv_results.values())
+
+        solved_str = "✓ SOLVED" if (g1_pass and g2_pass) else "~ PARTIAL" if g1_pass else "✗ UNSOLVED"
+        g2_detail  = " | ".join(f"{'✓' if ok else '✗'} {k}" for k, (_, ok) in inv_results.items())
+        best_ray   = best_t.ray_name if best_t else "—"
+
+        yield emit(
+            f"\n{solved_str}\n"
+            f"  CE = {ce:.6f} | Gate 1: {'✓' if g1_pass else '✗'} | Gate 2: {'✓' if g2_pass else '✗'}\n"
+            f"  {g2_detail}\n"
+            f"  Best ray: `{best_ray}`\n"
+            f"  Rays fired: {total_fired:,} | Survived: {len(survived)}\n"
+            f"  Allosteric: isolated {allosteric.get('isolated',0):,} | relational {allosteric.get('relational',0):,} | systemic {allosteric.get('systemic',0):,}\n\n"
+        )
+
+        # ── Self-Correcting Feedback Loop (Gate 2 Failure) ───────────────
+        if not g2_pass and attempt < MAX_ATTEMPTS:
+            failed_invs = {k: v for k, (v, ok) in inv_results.items() if not ok}
+            current_text = original_problem_text + f"\n\nPREVIOUS ATTEMPT FAILED:\nGate 2 invariants that did not pass:\n{json.dumps(failed_invs, indent=2)}\n\nPlease revise the constraint encoding to better capture these conditions."
+            yield emit(f"⚠ **Gate 2 Failed.** Retrying ({len(failed_invs)} invariants failed) with structural feedback...\n\n---\n")
+            continue 
+            
+        yield emit(f"🔤 **Collapsing to domain language…**\n")
+        try:
+            answer_text = collapse_solution(
+                original_problem_text, axl_def, binding,
+                g1_pass, g2_pass, inv_results,
+                best_ray, total_fired, used_key
+            )
+            yield emit("✓ Done.\n")
+        except Exception as e:
+            answer_text = f"Error during collapsing: {e}"
+            yield emit("✗ Collapsing failed.\n")
+            
+        break 
+
+# ══════════════════════════════════════════════════════════════════
+# SECTION 14: GRADIO INTERFACE
+# ══════════════════════════════════════════════════════════════════
+
+CSS = """
+body { background: #090909; color: #e0e0e0; font-family: monospace; }
+.solver-log { font-size: 0.75em; background: #0d0d0d; border: 1px solid #181818; }
+.answer-box { font-size: 0.85em; background: #0d0d0d; border: 1px solid #222; }
+.status-bar { font-size: 0.70em; color: #555; padding: 4px 0; }
+"""
+
+PLACEHOLDER_HINT = textwrap.dedent("""
+    Try any problem description. Gemini will extract the mathematical structure.
+
+    Example inputs:
+      • "Find points on the elliptic curve y²=x³-x+1 where x=0"
+      • "Solve a DC power flow problem with 3 buses where p1+p2+p3=1"
+      • "Markowitz portfolio with 4 assets, returns [10%, 12%, 8%, 15%], target return 11%"
+""").strip()
+
+with gr.Blocks(css=CSS, title="Practicality Unified Server") as demo:
+
+    gr.Markdown(
+        "## ⚗ Practicality Unified Server\n"
+        "`[Gemini 3.1 Encoder] → AXL/PSL → [PyTorch Ray Solver] → [Gemini 3.1 Collapser]`"
+    )
+
+    with gr.Row():
+        with gr.Column(scale=2):
+            api_key_input = gr.Textbox(
+                label="Gemini API Key", 
+                type="password", 
+                placeholder="AIza...", 
+                value=DEFAULT_GEMINI_API_KEY,
+                elem_classes=["solver-log"]
+            )
+            problem_input = gr.Textbox(
+                label="Problem Description",
+                placeholder=PLACEHOLDER_HINT,
+                lines=5,
+                elem_classes=["solver-log"],
+            )
+            with gr.Row():
+                solve_btn = gr.Button("⚗ Solve", variant="primary")
+                clear_btn = gr.Button("Clear")
+
+        with gr.Column(scale=1):
+            gr.Markdown("**Device & Mode**")
+            gr.Textbox(
+                value=f"Compute: {DEVICE.type.upper()}\n"
+                      f"Axioms: {len(ALL_AXIOMS)}\n"
+                      f"Max rays: {MAX_TOTAL_RAYS:,}\n"
+                      f"Batch: {RAY_BATCH_SIZE:,}\n"
+                      f"LLM: {GEMINI_MODEL}",
+                lines=5, interactive=False,
+                elem_classes=["solver-log"],
+            )
+
+    with gr.Row():
+        solver_log = gr.Textbox(
+            label="Solver Log",
+            lines=18,
+            interactive=False,
+            elem_classes=["solver-log"],
+        )
+        answer_box = gr.Textbox(
+            label="Answer",
+            lines=18,
+            interactive=False,
+            elem_classes=["answer-box"],
+        )
+
+    def _solve(problem_text: str, api_key: str):
+        if not problem_text.strip():
+            yield "No problem text provided.", ""
+            return
+        for log_chunk, answer_chunk in run_solve_streaming(problem_text, api_key):
+            yield log_chunk, answer_chunk
+
+    solve_btn.click(
+        fn=_solve,
+        inputs=[problem_input, api_key_input],
+        outputs=[solver_log, answer_box],
+        show_progress=False,
+    )
+
+    clear_btn.click(
+        fn=lambda: ("", "", ""),
+        inputs=[],
+        outputs=[problem_input, solver_log, answer_box],
+    )
+
+    gr.Markdown(
+        "Built with Gradio · Practicality 22.1 · Strict Neuro-Symbolic Boundary",
+        elem_classes=["status-bar"]
+    )
+
+demo.queue()
+
+if __name__ == "__main__":
+    print(f"[UNIFIED SERVER] Compute: {DEVICE.type.upper()}")
+    print(f"[UNIFIED SERVER] System 22.1: GenAI SDK wired. Model: {GEMINI_MODEL}")
+    demo.launch(server_name="0.0.0.0", server_port=7860, share=False)