Update app.py

app.py

@@ -1,36 +1,20 @@
 #!/usr/bin/env python3
 """
-PRACTICALITY SYSTEM 19.3 — NEURO-SYMBOLIC ENZYME (RESTORED WISDOM)
+PRACTICALITY SYSTEM 20.0 — TRUE GPU SATURATION & PRECOMPILATION
 ═══════════════════════════════════════════════════════════════════
-FIXES FROM 19.2:
-
-  1. RESTORED HYPOTHESIS DEPTH:
-     _hyp_bilinear: Full asymmetric split logic restored — geometric mean
-     PLUS ascending/descending pairs at ratios [0.4, 0.7071, 0.9].
-     Without this BilinearChain6 only gets the equal-split case.
-
-     _hyp_monotone_product: Full ratio sweep restored [0.1, 0.2, 0.3,
-     0.4, 0.5, 0.6, 0.707, 0.8, 0.9, 0.95] with HC4 cascade propagation.
-     19.2 only tested ratio=0.4. The correct BilinearChain6 solution
-     requires ratios like 0.5/2.0, 1.0/2.0, 1.5/3.0 which only emerge
-     from the full sweep.
-
-  2. FIXED BATON REGISTRY:
-     19.2 only stored batons for rays that improved best_ce globally.
-     Silent failure: recombination would fall back to self-recombination
-     when ray_a had never topped the global best.
-
-     19.3 stores any baton with CE < BATON_REGISTRY_THRESHOLD (=2.0).
-     Recombination now actually combines two different solution geometries.
-     Cap at 5000 entries (FIFO) to prevent memory growth.
-
-  3. FULL OBSERVABILITY DASHBOARD:
-     Restored the scientific instruments lost in the Gradio rewrite:
-     - Per-problem performance table (runs, solve rate, avg CE, best CE)
-     - Ray type efficacy table (tried, survived, rate per type)
-     - Allosteric feedback diagnostics (which tension class fired most)
-     - Recent run collapse view with binding and invariant details
-     All auto-refreshing every 2 seconds.
+AIM: 
+  To extract a true, LLM-readable structural isomorphism of a mathematical problem. 
+
+THE BOTTLENECK FIX (20.0):
+  In 19.3, large batch sizes starved the GPU because Python was doing heavy lifting 
+  (SymPy parsing, string evaluation, dict sorting) inside the 12k loop. 
+  
+  System 20.0 implements True Parallelism:
+  1. Pre-compilation: Anchors and Axiom properties (Bilinear/Monotone constants) 
+     are parsed exactly ONCE at initialization.
+  2. GPU Top-K Gradients: Python dict sorting is replaced by `torch.topk()` to 
+     calculate allosteric tension vectors for all 12,288 rays simultaneously on GPU.
+  3. Fast Tensor Build: CPU array generation is streamlined to feed PyTorch instantly.
 """
 
 import time, random, math, threading, warnings
@@ -48,7 +32,7 @@ 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 19.3] Compute: {DEVICE.type.upper()} | Engine: Neuro-Symbolic Enzyme (Restored Wisdom)")
+print(f"[SYSTEM 20.0] Compute: {DEVICE.type.upper()} | Engine: True GPU Saturation")
 
 # ══════════════════════════════════════════════════════════════════════
 # SECTION 1: CONSTANTS
@@ -65,10 +49,8 @@ RAY_BATCH_SIZE           = 12288
 CE_EARN_RATIO            = 0.90
 SCOUT_CE_THRESHOLD       = 0.5
 BRANCH_WIDTH             = 4
-
-# FIX 2: Registry threshold — store any baton that shows meaningful progress
 BATON_REGISTRY_THRESHOLD = 2.0
-BATON_REGISTRY_MAX       = 5000  # FIFO cap to prevent memory growth
+BATON_REGISTRY_MAX       = 5000
 
 # ══════════════════════════════════════════════════════════════════════
 # SECTION 2: INTERVAL ARITHMETIC (HC4)
@@ -145,7 +127,6 @@ def _hc4(box,constraints):
     return cur
 
 def _global_hc4_tighten_bounds(problem):
-    """Tighten bounds using HC4 before hypothesis testing."""
     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)
@@ -153,7 +134,7 @@ def _global_hc4_tighten_bounds(problem):
             for v in problem.bounds if v in c}
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 3: PSL PARSER & AXL LAYER
+# SECTION 3: PSL PARSER & PRE-COMPILATION
 # ══════════════════════════════════════════════════════════════════════
 @dataclass
 class PSLVar:        name:str; lo:float; hi:float
@@ -241,7 +222,17 @@ def expand_psl(prog:PSLProgram) -> ExpandedProblem:
     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"
+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]):
+        """SYSTEM 20.0 FIX: Pre-compile anchors to avoid parsing inside the 12k batch loop"""
+        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:
@@ -344,12 +335,42 @@ class Problem:
     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)
+    
+    # SYSTEM 20.0 PRECOMPILATION ARRAYS
+    bilinear_pairs: List[Tuple[str,str]] = field(default_factory=list)
+    monotone_targets: List[Tuple[str,str,float]] = 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)}
+        
+        # SYSTEM 20.0: Pre-extract structural signatures to avoid AST parsing in batch loops
+        ordered_pairs = []
+        for mc in self.compiled_constraints:
+            if mc.kind == "inequality" and mc.direction == "geq" and len(mc.syms_used) == 2:
+                ordered_pairs.append((mc.syms_used[0], mc.syms_used[1]))
+                
+        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))
+                            if mc.kind == "equality":
+                                try:
+                                    const_part = mc.parsed - sp.Symbol(va)*sp.Symbol(vb)
+                                    k = float(-const_part.evalf())
+                                    if k > 0:
+                                        for vs, vl in ordered_pairs:
+                                            if set([va, vb]) == set([vs, vl]):
+                                                if (vs, vl, k) not in self.monotone_targets:
+                                                    self.monotone_targets.append((vs, vl, k))
+                                except: pass
 
     def tensor_energy(self,X:torch.Tensor) -> torch.Tensor:
         is_batched=(X.dim()==2)
@@ -405,34 +426,38 @@ class Problem:
 @dataclass
 class L9Certificate:
     residual_ce:float; dominant_vars:List[str]; dominant_exprs:List[str]
-    # NEW: track tension class for allosteric diagnostics
-    tension_class:str="unknown"  # "isolated" | "relational" | "systemic"
+    tension_class:str="unknown"
 
 def _batched_deduce_and_evaluate(
         problem:Problem,
         hyps:List['Hypothesis']) -> List[Tuple[Dict,float,List[str],str]]:
     """
     Naked Evaluation with Masked Adam.
-    Returns (binding, ce, dominant_vars, tension_class) per hypothesis.
-    tension_class feeds the allosteric feedback diagnostics.
+    SYSTEM 20.0 FIX: Optimized array building & PyTorch Top-K extraction 
+    to bypass Python CPU loops over large batches.
     """
     if not hyps: return []
     B=len(hyps); V=len(problem.variables)
 
-    X_init=torch.zeros((B,V),device=DEVICE,dtype=torch.float32)
-    mask   =torch.ones( (B,V),device=DEVICE,dtype=torch.float32)
-    target =torch.zeros((B,V),device=DEVICE,dtype=torch.float32)
-
-    for i,hyp in enumerate(hyps):
-        for j,v in enumerate(problem.variables):
-            val=hyp.binding.get(v,(problem.bounds[v][0]+problem.bounds[v][1])/2)
-            X_init[i,j]=val
+    # Fast Python list building to avoid element-by-element tensor operations
+    x_data = []
+    mask_data = []
+    target_data = []
+    for hyp in hyps:
+        xr, mr, tr = [], [], []
+        for v in problem.variables:
             if v in hyp.pinned_vars:
-                mask[i,j]  =0.0
-                target[i,j]=hyp.pinned_vars[v]
-                X_init[i,j]=hyp.pinned_vars[v]
+                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)
 
-    X=X_init.clone().detach().requires_grad_(True)
     optimizer=torch.optim.Adam([X],lr=0.05)
 
     for _ in range(DEDUCE_ADAM_STEPS):
@@ -453,20 +478,28 @@ def _batched_deduce_and_evaluate(
     final_ce=problem.tensor_energy(X)
     final_ce.sum().backward()
 
-    ce_vals =final_ce.detach().cpu().numpy()
-    grads   =X.grad.abs().cpu().numpy()
-    X_vals  =X.detach().cpu().numpy()
+    ce_vals = final_ce.detach().cpu().numpy()
+    X_vals  = X.detach().cpu().numpy()
+
+    # SYSTEM 20.0 FIX: GPU Top-K completely removes Python dictionary sorting overhead
+    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)}
-        var_tensions={problem.variables[j]:float(grads[i,j]) for j in range(V)}
-        dom_vars=sorted(var_tensions.keys(),key=lambda v:-var_tensions[v])[:3]
-        n_dom=sum(1 for v in dom_vars if var_tensions[v]>1e-4)
+        
+        # O(1) top-K gradient extraction per element
+        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):
@@ -570,7 +603,7 @@ class StructuralModel:
     resonant_pairs:List[Tuple[str,str]]=field(default_factory=list)
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 8: HYPOTHESIS CONSTRUCTORS (RESTORED FULL DEPTH)
+# SECTION 8: HYPOTHESIS CONSTRUCTORS (Pre-Compiled)
 # ══════════════════════════════════════════════════════════════════════
 def _make_hyp(hid,binding,h_type,claim,derivation,pinned,free,conf):
     return Hypothesis(hid=hid,binding=binding,h_type=h_type,claim=claim,
@@ -598,111 +631,69 @@ def _hyp_quadratic(p,bt,a,m):
     return hyps
 
 def _hyp_bilinear(p,bt,a,m):
-    """
-    FIX 19.3: Restored full asymmetric split logic.
-    Geometric mean + ascending/descending pairs at multiple ratios.
-    Without this BilinearChain6 only sees the equal-split case.
-    """
+    """SYSTEM 20.0 FIX: Uses pre-extracted bilinear pairs."""
     hyps=[]; b=dict(bt.binding)
-    for mc in p.compiled_constraints:
-        if not mc.parsed or not mc.parsed.is_Add: continue
-        for term in mc.parsed.args:
-            if not term.is_Mul: continue
-            syms_in=[str(s) for s in term.free_symbols if str(s) in p.variables]
-            if len(syms_in)!=2: continue
-            vi,vj=syms_in
-            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)
-
-            # Geometric mean (equal split)
-            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))
-
-            # RESTORED: Asymmetric splits
-            for ratio in [0.4, 0.7071, 0.9]:
-                vs=gm*ratio; vl=product/(vs+1e-9)
-                # Ascending: vi < vj
-                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))
-                # Descending: vi > vj
-                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))
+    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):
-    """
-    FIX 19.3: Full ratio sweep restored [0.1 → 0.95] with HC4 cascade.
-    19.2 only tested ratio=0.4. The correct BilinearChain6 solutions
-    require ratios like 0.25 (t1=0.5, t2=1.0) which need this sweep.
-    """
+    """SYSTEM 20.0 FIX: Uses pre-extracted monotone targets."""
     hyps=[]; b=dict(bt.binding)
 
-    # Build ordered pairs from inequality constraints
-    ordered_pairs:List[Tuple[str,str]]=[]
-    for mc in p.compiled_constraints:
-        if mc.kind=="inequality" and mc.direction=="geq" and len(mc.syms_used)==2:
-            ordered_pairs.append((mc.syms_used[0],mc.syms_used[1]))
+    if not p.monotone_targets: return hyps
+    tb=_global_hc4_tighten_bounds(p)
 
-    if not ordered_pairs: return hyps
+    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))
 
-    # Tighten bounds via HC4 before pinning
-    tb=_global_hc4_tighten_bounds(p)
+        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
 
-    for mc in p.compiled_constraints:
-        if mc.kind!="equality" or not mc.parsed or not mc.parsed.is_Add: continue
-        for term in mc.parsed.args:
-            if not term.is_Mul: continue
-            syms_in=[str(s) for s in term.free_symbols if str(s) in p.variables]
-            if len(syms_in)!=2: continue
-            va,vb=syms_in
-            try:
-                const_part=mc.parsed-sp.Symbol(va)*sp.Symbol(vb)
-                k=float(-const_part.evalf())
-            except: continue
-            if k<=0: continue
-
-            for (v_small,v_large) in ordered_pairs:
-                if set([va,vb])!=set([v_small,v_large]): continue
-                lo_s,hi_s=p.bounds.get(v_small,(-1e18,1e18))
-                lo_l,hi_l=p.bounds.get(v_large,(-1e18,1e18))
-
-                # RESTORED: Full ratio sweep
-                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
-
-                    # HC4 cascade to propagate implications
-                    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})",
-                        [mc.expr_str,"ordered","hc4"],pinned,
-                        [u for u in p.variables if u not in pinned],0.88))
+            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)]
@@ -800,7 +791,6 @@ AXIOM_CONSTRUCTORS={
 # ══════════════════════════════════════════════════════════════════════
 class CreativeSeeder:
     def target_seeds(self,anchors:List[AXLInvariant]) -> List[AxiomRay]:
-        """Bidirectional search: spawn from goal state structure."""
         seeds=[]
         for a in anchors:
             if "*" in a.expr and "**" not in a.expr:
@@ -814,10 +804,6 @@ class CreativeSeeder:
         return seeds
 
     def intelligent_branch(self,ray,out_baton,remaining_axioms,branch_width) -> List[AxiomRay]:
-        """
-        Allosteric feedback: gradient topology biases next axiom selection.
-        Returns children sorted by weighted stochastic score.
-        """
         dom_vars=out_baton.l9.dominant_vars if out_baton.l9 else []
         n_dom=len([v for v in dom_vars])
         isolated  ={Axiom.ATOMIC,Axiom.EXTREMAL,Axiom.MUTABLE,Axiom.DUALITY,Axiom.LOCALITY}
@@ -902,7 +888,7 @@ class CreativeSeeder:
 CREATIVE_SEEDER=CreativeSeeder()
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 10: VERIFY LAYER
+# SECTION 10: VERIFY LAYER (SYSTEM 20.0 FIX: Pre-compiled lambda evaluation)
 # ══════════════════════════════════════════════════════════════════════
 def _verify(binding:Dict[str,float],base_problem:Problem,
             anchors:List[AXLInvariant]) -> Tuple[bool,bool,Dict[str,Tuple[float,bool]],float]:
@@ -911,10 +897,11 @@ def _verify(binding:Dict[str,float],base_problem:Problem,
     g2={}
     for inv in anchors:
         try:
-            syms={v:sp.Symbol(v) for v in binding}
-            expr=parse_expr(inv.expr,local_dict=syms)
-            func=sp.lambdify(list(expr.free_symbols),expr,modules="math")
-            val=float(func(*[binding.get(str(s),0.0) for s in expr.free_symbols])); err=abs(val)
+            if inv.compiled_func:
+                val = float(inv.compiled_func(*[binding.get(v, 0.0) for v in inv.syms_used]))
+            else:
+                val = 999.0 # Failsafe
+            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
@@ -925,19 +912,23 @@ def _verify(binding:Dict[str,float],base_problem:Problem,
     return g1_pass,g2_pass,g2,round(g1_ce,6)
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 11: SEQUENCE RAY TRACER (Fixed Baton Registry)
+# SECTION 11: SEQUENCE RAY TRACER
 # ══════════════════════════════════════════════════════════════════════
 class SequenceRayTracer:
     def trace(self,axl_def:AXLProblemDef,base_problem:Problem):
         hero_traces:List[HypothesisTrace]=[]
 
-        # FIX 2: Registry stores ANY baton below threshold, not just global bests
         baton_registry:Dict[str,Baton]={}
-        baton_registry_keys:deque=deque()   # FIFO for memory cap
+        baton_registry_keys:deque=deque()
 
         successful_rays:List[AxiomRay]=[]
         resonant_pairs:List[Tuple[str,str]]=[]
 
+        # SYSTEM 20.0 FIX: Precompile anchors before 12k loop starts
+        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",
@@ -954,11 +945,9 @@ class SequenceRayTracer:
         best_ce=init_ce; best_binding=dict(init_b); total_fired=0
         model=StructuralModel(best_binding,best_ce)
 
-        # Allosteric diagnostics counters
         allosteric_counts={"isolated":0,"relational":0,"systemic":0}
 
         while total_fired<MAX_TOTAL_RAYS:
-            # Build batch
             batch_rays:List[AxiomRay]=[]
             for _ in range(RAY_BATCH_SIZE):
                 start_idx=q_idx
@@ -973,7 +962,6 @@ class SequenceRayTracer:
             t0=time.time()
             historical_batons=list(baton_registry.values())
 
-            # Generate one hypothesis per ray
             batch_hyps:List[Tuple[int,Hypothesis]]=[]
             for i,ray in enumerate(batch_rays):
                 p_baton=ray.baton or seed_baton
@@ -982,7 +970,6 @@ class SequenceRayTracer:
                 if not hyps: hyps=[_make_hyp("fb",p_baton.binding,"fallback","Pass",[],{},base_problem.variables,0.1)]
                 batch_hyps.append((i,hyps[0]))
 
-            # Batched masked deduction + gradient oracle
             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))
 
@@ -996,7 +983,6 @@ class SequenceRayTracer:
                 overall_pass=g1_pass and g2_pass
 
                 improved=final_ce<best_ce
-                # Save traces for heroes + random sample for observability
                 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,
@@ -1011,7 +997,6 @@ class SequenceRayTracer:
                 out_baton=Baton(binding=final_b,ce=final_ce,ray_id=ray.ray_id,
                                 l9=L9Certificate(final_ce,dom_vars,[],tension_class))
 
-                # FIX 2: Register baton if below threshold — not just global bests
                 if final_ce<BATON_REGISTRY_THRESHOLD:
                     if ray.ray_id in baton_registry:
                         baton_registry[ray.ray_id]=out_baton
@@ -1029,7 +1014,6 @@ class SequenceRayTracer:
 
                 if overall_pass: solved=True
 
-                # Resonance detection
                 if improved and len(ray.sequence)>=2:
                     pair=(ray.sequence[-2],ray.sequence[-1])
                     if pair not in resonant_pairs: resonant_pairs.append(pair)
@@ -1045,21 +1029,18 @@ class SequenceRayTracer:
                                 and a not in ray.sequence]
 
                     new_children:List[AxiomRay]=[]
-                    # Allosteric feedback branching
                     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)
 
-                    # FIX 2: Recombination now gets real registered batons from both parents
                     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)
-                            # Look up actual registered batons — fall back to current only if missing
                             ba=baton_registry.get(ray.ray_id,out_baton)
                             bb=baton_registry.get(partner.ray_id)
-                            if bb is not None:  # Only recombine if partner has a registered baton
+                            if bb is not None:
                                 new_children.extend(CREATIVE_SEEDER.recombine(ray,partner,ba,bb)[:3])
 
                     new_children.extend(
@@ -1233,7 +1214,6 @@ def build_base_problem(axl_def:AXLProblemDef) -> Problem:
 STATE_LOCK = threading.Lock()
 IS_RUNNING = False
 
-# FIX 3: Full observability state
 PROBLEM_STATS:Dict[str,Dict]={p.name:{
     "runs":0,"solved":0,"total_ce":0.0,"best_ce":float('inf'),
     "best_binding":{},"best_ray":"—",
@@ -1241,7 +1221,7 @@ PROBLEM_STATS:Dict[str,Dict]={p.name:{
     "allosteric":{"isolated":0,"relational":0,"systemic":0},
 } for p in AXL_PROBLEMS}
 
-RECENT_RUNS:List[Dict]=[]      # Last 30 full run records
+RECENT_RUNS:List[Dict]=[]
 MAX_RECENT=30
 _PROB_IDX=0
 
@@ -1308,10 +1288,10 @@ def toggle_engine():
     global IS_RUNNING
     IS_RUNNING=not IS_RUNNING
     if IS_RUNNING: threading.Thread(target=background_worker,daemon=True).start()
-    return "⏹ STOP 19.3" if IS_RUNNING else "▶ START 19.3"
+    return "⏹ STOP 20.0" if IS_RUNNING else "▶ START 20.0"
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 14: GRADIO DASHBOARD (Full Observability Restored)
+# SECTION 14: GRADIO DASHBOARD 
 # ══════════════════════════════════════════════════════════════════════
 RAY_ICONS={"seed":"🌱","branch":"🌿","tension":"⚡","scout":"🔭",
            "recombine":"🧬","invert":"🔄","target":"🎯"}
@@ -1476,11 +1456,11 @@ def refresh_dashboard():
     return f"""
 <div style='background:#090909;color:#e0e0e0;font-family:monospace;padding:16px;max-width:1700px'>
 <h2 style='color:#26C6DA;border-bottom:1px solid #1a1a1a;padding-bottom:5px;font-size:1.05em;margin:0 0 8px 0'>
-  ⚗ Practicality 19.3 — Neuro-Symbolic Enzyme (Restored Wisdom)
+  ⚗ Practicality 20.0 — True GPU Saturation
 </h2>
 <div style='color:#2a2a2a;font-size:0.70em;margin-bottom:10px'>
-  Masked Adam (structural pins) · Gradient Oracle → Allosteric Feedback ·
-  Full Bilinear Splits · Full MPR Ratio Sweep · Fixed Baton Registry · 12K Batch
+  Masked Adam (structural pins) · GPU Top-K Oracle → Allosteric Feedback ·
+  Pre-Compiled Axioms & Anchors · 12K Batch Scale
 </div>
 <div style='margin-bottom:12px'>
   <span style='display:inline-block;padding:2px 8px;border-radius:3px;background:#0e0e0e;margin:2px;font-size:0.72em;border:1px solid #1a1a1a;color:#aaa'>Runs: {runs}</span>
@@ -1493,7 +1473,7 @@ def refresh_dashboard():
 
 <h4 style='color:#252525;font-size:0.78em;letter-spacing:2px;text-transform:uppercase;margin:16px 0 4px 0'>Creative Ray Type Efficacy</h4>
 <table style='width:100%;border-collapse:collapse;margin-bottom:10px'>
-<tr style='color:#252525;font-size:0.68em'><th></th><th>Type</th><th>Tried</th><th>Survived</th><th>Failed</th><th>Rate</th><th>Mechanism (19.3)</th></tr>
+<tr style='color:#252525;font-size:0.68em'><th></th><th>Type</th><th>Tried</th><th>Survived</th><th>Failed</th><th>Rate</th><th>Mechanism (20.0)</th></tr>
 {types}
 </table>
 
@@ -1518,14 +1498,14 @@ def refresh_dashboard():
 {recnt}
 </div>"""
 
-with gr.Blocks(theme=gr.themes.Monochrome(text_size="sm"),title="Practicality 19.3") as demo:
-    gr.Markdown("## ⚗ Practicality 19.3 — Neuro-Symbolic Enzyme")
+with gr.Blocks(theme=gr.themes.Monochrome(text_size="sm"),title="Practicality 20.0") as demo:
+    gr.Markdown("## ⚗ Practicality 20.0 — True GPU Saturation")
     gr.Markdown(
         f"**Compute:** `{DEVICE.type.upper()}` | "
-        f"**Fixes:** Full bilinear splits · Full MPR sweep · Fixed baton registry · Full observability")
+        f"**Fixes:** Pre-compiled Axiom ASTs · Pre-compiled Anchor Lambdas · GPU Top-K Gradients")
 
     with gr.Row():
-        btn=gr.Button("▶ START 19.3",variant="primary",scale=1)
+        btn=gr.Button("▶ START 20.0",variant="primary")
         gr.Markdown("*Engine cycles through 14 domains. Dashboard auto-refreshes every 2s.*")
 
     html_out=gr.HTML(refresh_dashboard())
@@ -1539,5 +1519,5 @@ with gr.Blocks(theme=gr.themes.Monochrome(text_size="sm"),title="Practicality 19
     demo.load(auto_refresh,inputs=None,outputs=html_out)
 
 if __name__=="__main__":
-    print(f"[SYSTEM 19.3] Launching on 0.0.0.0:7860 | Compute: {DEVICE.type.upper()}")
+    print(f"[SYSTEM 20.0] Launching on 0.0.0.0:7860 | Compute: {DEVICE.type.upper()}")
     demo.launch(server_name="0.0.0.0",server_port=7860,share=False)