Update app.py

app.py

@@ -1,19 +1,16 @@
 #!/usr/bin/env python3
 """
-PRACTICALITY SYSTEM 11.1 — AXL/PSL PIPELINE
+PRACTICALITY SYSTEM 12.0 — SET-BASED AXIOMATIC RAY TRACING
 ═══════════════════════════════════════════════════════════════════
-FIXED IN 11.1:
-  · PSLTranslator now grounds domain PSL in actual base constraints
-    Domain adds SOFT structural hints (weight 0.15), never replaces base
-  · Observations pin variables in domain PSL (zero-width VAR bounds)
-  · DomainStrategy: wisdom layer informs HOW to search, not WHAT to search
-    Each domain maps to hypothesis weights + polish preference + explore trigger
-  · PhaseCollider redesigned to be provably feasible
-  · StructuralModel moved before solve_by_hypothesis (no more _SM hack)
-  · HypothesisOracle accepts DomainStrategy, applies confidence weights
+NEW IN 12.0:
+  · True Theorist Layer: Human-named domains deleted. 
+  · Boolean Hypercube: 4,708 valid axiomatic permutations generated on boot.
+  · Strict Configuration: Axioms dictate Hypothesis weights directly (No soft constraints).
+  · Absolute Verification: Solver searches pure base problem, VerifyLayer arbitrates.
+  · Wavefront Search: Batches of rays are fired to deduce the problem signature.
 """
 
-import time, random, math, threading, asyncio, warnings, itertools, json
+import time, random, math, threading, asyncio, warnings, itertools
 from functools import reduce
 from typing import Optional, Callable, List, Dict, Tuple, Any, Set
 from dataclasses import dataclass, field
@@ -26,13 +23,13 @@ import sympy as sp
 from sympy.parsing.sympy_parser import parse_expr
 import torch
 from fastapi import FastAPI
-from fastapi.responses import HTMLResponse, JSONResponse
+from fastapi.responses import HTMLResponse
 import uvicorn
 
 warnings.filterwarnings("ignore")
 USE_GPU = torch.cuda.is_available()
 DEVICE  = torch.device("cuda" if USE_GPU else "cpu")
-print(f"[SYSTEM 11.1] Compute: {'GPU' if USE_GPU else 'CPU'}")
+print(f"[SYSTEM 12.0] Compute: {'GPU' if USE_GPU else 'CPU'}")
 
 # ══════════════════════════════════════════════════════════════════════
 # SECTION 1: CONSTANTS
@@ -139,12 +136,10 @@ 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 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
+        p=rest.split(); return PSLVar(p[0],float(p[1]),float(p[2])) if len(p)>=3 else None
     def pw(rest):
         if 'WEIGHT' in rest:
             p=rest.split('WEIGHT'); return p[0].strip(), float(p[1].split()[0])
@@ -172,7 +167,7 @@ def parse_psl(text:str) -> PSLProgram:
                 advance()
                 scons.append(PSLConstraint("or_eq","",scope=sname,weight=1.0,branches=opts))
             elif kw=="ANNOTATE":
-                parts=rest.split()
+                parts=rest.split();
                 if len(parts)>=3: prog.annotations[parts[0]]=parts[2]
         return PSLScope(sname,order,depends or [],svars,links,scons)
 
@@ -195,7 +190,7 @@ def parse_psl(text:str) -> PSLProgram:
             advance()
             prog.constraints.append(PSLConstraint("or_eq","",weight=1.0,branches=opts))
         elif kw=="ANNOTATE":
-            parts=rest.split()
+            parts=rest.split();
             if len(parts)>=3: prog.annotations[parts[0]]=parts[2]
         elif kw=="SCOPE":
             parts=rest.split(); sname=parts[0] if parts else f"s{len(prog.scopes)}"
@@ -254,14 +249,11 @@ def expand_psl(prog:PSLProgram) -> ExpandedProblem:
     for sc in prog.scopes:
         for v in sc.vars: add_var(v.name,v.lo,v.hi,sc.name)
         for vname in sc.links:
-            if vname in bounds and vname not in scope_vars[sc.name]:
-                scope_vars[sc.name].append(vname)
+            if vname in bounds and vname not in scope_vars[sc.name]: scope_vars[sc.name].append(vname)
         for c in sc.constraints:
             kind="or_eq" if c.kind=="or_eq" else "equality" if c.kind=="eq" else "inequality"
             add_con(kind,c.expr,c.kind,sc.name,c.weight,c.branches)
-    return ExpandedProblem(variables,bounds,constraints,
-                           dict(scope_groups),dict(scope_vars),
-                           prog.scope_order,prog.annotations)
+    return ExpandedProblem(variables,bounds,constraints,dict(scope_groups),dict(scope_vars),prog.scope_order,prog.annotations)
 
 # ═════════════════════════════════════════════════════���════════════════
 # SECTION 4: AXL LAYER
@@ -279,7 +271,6 @@ class AXLProblemDef:
     def variables_list(self): return [v["name"] for v in self.variables]
 
 class AXLtoPSLCompiler:
-    """Compile AXL directly to PSL — used only for the BASE problem oracle."""
     TEND_WEIGHT=0.3
     def compile(self,prob:AXLProblemDef) -> str:
         lines=[f"SPACE base_{prob.name}"]
@@ -525,70 +516,86 @@ class VerifyLayer:
 VERIFY_LAYER=VerifyLayer()
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 7: DOMAIN STRATEGY  ← NEW
-# Wisdom layer informs HOW to search, not WHAT to search.
+# SECTION 7: HYPERCUBE SET-BASED THEORIST
+# The fundamental engine. No names. No soft weights. Pure Logic.
 # ══════════════════════════════════════════════════════════════════════
+class Axiom:
+    DISCRETE="DISCRETE"; CONTINUOUS="CONTINUOUS"; METRIC="METRIC"; NETWORK="NETWORK"
+    INJECTIVE="INJECTIVE"; SURJECTIVE="SURJECTIVE"; CONSERVED="CONSERVED"; MUTABLE="MUTABLE"
+    QUADRATIC="QUADRATIC"; BILINEAR="BILINEAR"; ORDERED="ORDERED"; SYMMETRIC="SYMMETRIC"
+    TRANSITIVE="TRANSITIVE"; ATOMIC="ATOMIC"; COMPOSITE="COMPOSITE"
+
+ALL_AXIOMS = [
+    Axiom.DISCRETE, Axiom.CONTINUOUS, Axiom.METRIC, Axiom.NETWORK,
+    Axiom.INJECTIVE, Axiom.SURJECTIVE, Axiom.CONSERVED, Axiom.MUTABLE,
+    Axiom.QUADRATIC, Axiom.BILINEAR, Axiom.ORDERED, Axiom.SYMMETRIC,
+    Axiom.TRANSITIVE, Axiom.ATOMIC, Axiom.COMPOSITE
+]
+
+AXIOM_CONTRADICTIONS=[
+    {Axiom.DISCRETE,Axiom.CONTINUOUS},
+    {Axiom.INJECTIVE,Axiom.SURJECTIVE},
+    {Axiom.ORDERED,Axiom.SYMMETRIC},
+    {Axiom.ATOMIC,Axiom.COMPOSITE},
+    {Axiom.CONSERVED,Axiom.MUTABLE}
+]
+
+def build_hypercube() -> List[Set[str]]:
+    """Generates all non-contradictory combinations of axioms up to length 6."""
+    valid = []
+    for r in range(1, 7):
+        for combo in itertools.combinations(ALL_AXIOMS, r):
+            cset = set(combo)
+            if not any(contra.issubset(cset) for contra in AXIOM_CONTRADICTIONS):
+                valid.append(cset)
+    return valid
+
+# Boots instantly. Generates exactly 4,708 valid universal rays.
+AXIOM_HYPERCUBE = build_hypercube()
+print(f"[SYSTEM 12.0] Axiomatic Hypercube Booted: {len(AXIOM_HYPERCUBE)} valid rays.")
+
 @dataclass
 class DomainStrategy:
     name:           str
-    hyp_weights:    Dict[str,float]   # h_type → confidence multiplier
+    hyp_weights:    Dict[str,float]   # 0.0 strictly prunes hypothesis type
     polish:         str               # "adam" | "gradient" | "both"
-    explore_early:  bool              # True → explore_trigger=2, False → 4
-    scope_priority: str               # "ordered" | "hub" | "natural"
-    note:           str=""
-
-DOMAIN_STRATEGIES: Dict[str,DomainStrategy] = {
-    "NormManifold":    DomainStrategy("NormManifold",
-        {"branch":1.3,"manifold":2.0,"chain":0.8,"residual_chain":1.1},
-        "adam", False, "hub",
-        "Quadratic manifolds → manifold tangents most useful; Adam navigates smooth bowl"),
-    "MetricPacking":   DomainStrategy("MetricPacking",
-        {"branch":1.2,"manifold":0.8,"chain":1.5,"residual_chain":1.2},
-        "gradient", True, "hub",
-        "Separation constraints → algebraic branches + early exploration"),
-    "SequentialChain": DomainStrategy("SequentialChain",
-        {"branch":0.9,"manifold":0.5,"chain":2.0,"residual_chain":1.5},
-        "gradient", False, "ordered",
-        "Ordered chains → topology chain hypotheses dominate"),
-    "BilinearCoupling":DomainStrategy("BilinearCoupling",
-        {"branch":1.3,"manifold":1.6,"chain":1.0,"residual_chain":1.0},
-        "adam", False, "natural",
-        "Bilinear products → manifold + branch both useful; Adam for coupling"),
-    "PhaseJump":       DomainStrategy("PhaseJump",
-        {"branch":2.0,"manifold":1.0,"chain":0.7,"residual_chain":0.9},
-        "adam", True, "natural",
-        "OR constraints → branch hypotheses highest priority; explore early"),
-    "GraphSpace":      DomainStrategy("GraphSpace",
-        {"branch":1.0,"manifold":0.7,"chain":1.3,"residual_chain":1.0},
-        "gradient", False, "hub",
-        "Network hubs → chain + gradient works well"),
-    "HierarchicalTree":DomainStrategy("HierarchicalTree",
-        {"branch":0.9,"manifold":0.6,"chain":1.8,"residual_chain":1.2},
-        "gradient", False, "ordered",
-        "Hierarchical ordering → chain hypotheses + ordered scope priority"),
-    "DiscreteSchedule":DomainStrategy("DiscreteSchedule",
-        {"branch":1.0,"manifold":0.5,"chain":2.0,"residual_chain":1.3},
-        "gradient", False, "ordered",
-        "Scheduling → chain + ordering; manifold less useful for discrete"),
-    "FluidContinuum":  DomainStrategy("FluidContinuum",
-        {"branch":1.1,"manifold":1.8,"chain":0.8,"residual_chain":1.0},
-        "adam", True, "natural",
-        "Continuous flow → manifold tangents + Adam; explore broadly"),
-}
-
-DEFAULT_STRATEGY=DomainStrategy("Default",
-    {"branch":1.0,"manifold":1.0,"chain":1.0,"residual_chain":1.0},
-    "both", False, "natural")
-
-def get_strategy(domain_name:str) -> DomainStrategy:
-    # Check exact match, then prefix match for derived domains (unions, duals)
-    if domain_name in DOMAIN_STRATEGIES: return DOMAIN_STRATEGIES[domain_name]
-    for k,v in DOMAIN_STRATEGIES.items():
-        if k in domain_name: return v
-    return DEFAULT_STRATEGY
+    explore_early:  bool              
+
+def compile_strategy(axioms: Set[str]) -> DomainStrategy:
+    """Translates a pure axiom set into strict search constraints."""
+    name = "|".join(a[:3] for a in sorted(axioms)) if axioms else "BASE"
+    weights = {"branch": 0.0, "chain": 0.0, "coherence": 0.0, "residual_chain": 0.0, "manifold": 0.0}
+    polish = "both"
+    explore_early = False
+
+    if Axiom.CONTINUOUS in axioms:
+        weights["manifold"] = 1.5
+        weights["branch"] = 1.0
+        weights["residual_chain"] = 1.0
+        polish = "adam"
+    if Axiom.DISCRETE in axioms:
+        weights["chain"] = 2.0
+        weights["branch"] = 1.5
+        weights["coherence"] = 1.0
+        polish = "gradient"
+        explore_early = True
+
+    if Axiom.QUADRATIC in axioms or Axiom.METRIC in axioms:
+        weights["manifold"] += 1.0
+        weights["branch"] += 0.5
+    if Axiom.ORDERED in axioms or Axiom.NETWORK in axioms:
+        weights["chain"] += 1.0
+    if Axiom.MUTABLE in axioms or Axiom.BILINEAR in axioms:
+        weights["branch"] += 1.0
+        weights["residual_chain"] += 1.0
+
+    if sum(weights.values()) < 0.1:
+        weights = {"branch": 1.0, "chain": 1.0, "coherence": 1.0, "residual_chain": 1.0, "manifold": 1.0}
+
+    return DomainStrategy(name=f"[{name}]", hyp_weights=weights, polish=polish, explore_early=explore_early)
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 8: SHARED TYPES (before solve_by_hypothesis to avoid forward refs)
+# SECTION 8: SHARED DATACLASSES
 # ══════════════════════════════════════════════════════════════════════
 @dataclass
 class Hypothesis:
@@ -598,10 +605,9 @@ class Hypothesis:
 
 @dataclass
 class HypothesisTrace:
-    hid:str; round_idx:int; domain_name:str; action:str
+    hid:str; round_idx:int; ray_name:str; action:str
     ce_before:float; ce_after:float
     verify:Optional[VerifyResult]; survived:bool; elapsed_ms:float
-    strategy_note:str=""
 
 @dataclass
 class StructuralModel:
@@ -793,8 +799,7 @@ def _adam_polish(problem,binding,steps=ADAM_STEPS):
         if nce<best_ce: best_ce=nce; best_b=dict(b)
     return best_b,best_ce
 
-def solve_by_hypothesis(problem:Problem, budget:int=TOTAL_BUDGET,
-                        strategy:Optional[DomainStrategy]=None) -> Dict:
+def solve_by_hypothesis(problem:Problem, budget:int=TOTAL_BUDGET, strategy:Optional[DomainStrategy]=None) -> Dict:
     t0=time.time()
     explore_trigger = 2 if (strategy and strategy.explore_early) else 4
     polish_pref     = strategy.polish if strategy else "both"
@@ -813,8 +818,7 @@ def solve_by_hypothesis(problem:Problem, budget:int=TOTAL_BUDGET,
     if model.best_ce<SOLVE_THRESHOLD:
         l7=TOPOLOGY_ORACLE.evaluate(problem,active_scopes)
         l9=RESIDUAL_ORACLE.evaluate(model.best_binding,problem,l7.hub_vars)
-        return {"binding":model.best_binding,"ce":model.best_ce,"solved":True,
-                "l7":l7,"l9":l9,"time":round(time.time()-t0,3)}
+        return {"binding":model.best_binding,"ce":model.best_ce,"solved":True,"l7":l7,"l9":l9,"time":round(time.time()-t0,3)}
 
     oracle=HypothesisOracle(strategy=strategy); consec=0
     for round_idx in range(HYPOTHESIS_MAX_ROUNDS):
@@ -840,17 +844,13 @@ def solve_by_hypothesis(problem:Problem, budget:int=TOTAL_BUDGET,
                 eb,ece=_mprt_sample(problem,work_box,N_MPRT_EXPLORE)
                 if ece<model.best_ce: model.best_ce=ece; model.best_binding=dict(eb); consec=0
 
-    # Polish — strategy-directed
+    # Strategy-directed polish
     if polish_pref in ("gradient","both") and SOLVE_THRESHOLD<model.best_ce<2.0:
         gb,gce=_gradient_polish(problem,model.best_binding)
         if gce<model.best_ce: model.best_ce=gce; model.best_binding=gb
     if polish_pref in ("adam","both") and SOLVE_THRESHOLD<model.best_ce<1.0:
         ab,ace=_adam_polish(problem,model.best_binding)
         if ace<model.best_ce: model.best_ce=ace; model.best_binding=ab
-    # Always try Adam as last resort if still not solved
-    if SOLVE_THRESHOLD<model.best_ce<0.5 and polish_pref=="gradient":
-        ab,ace=_adam_polish(problem,model.best_binding,steps=60)
-        if ace<model.best_ce: model.best_ce=ace; model.best_binding=ab
 
     final_l7=TOPOLOGY_ORACLE.evaluate(problem,active_scopes)
     final_l9=RESIDUAL_ORACLE.evaluate(model.best_binding,problem,final_l7.hub_vars)
@@ -858,7 +858,7 @@ def solve_by_hypothesis(problem:Problem, budget:int=TOTAL_BUDGET,
             "l7":final_l7,"l9":final_l9,"time":round(time.time()-t0,3)}
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 11: HYPOTHESIS ENGINE
+# SECTION 11: HYPOTHESIS ENGINE (Strict Pruning)
 # ══════════════════════════════════════════════════════════════════════
 class HypothesisOracle:
     def __init__(self, strategy:Optional[DomainStrategy]=None):
@@ -866,16 +866,24 @@ class HypothesisOracle:
 
     def generate(self,problem,model,l7,l8,l9,round_idx):
         hyps=[]
-        hyps.extend(self._branch_hypotheses(problem,model,l9))
-        hyps.extend(self._chain_hypotheses(problem,model,l7))
-        hyps.extend(self._coherence_hypotheses(problem,model,l8))
-        hyps.extend(self._residual_chain_hypotheses(problem,model,l9))
-        if round_idx>=3: hyps.extend(self._manifold_tangent_hypotheses(problem,model,l9))
-        # Apply strategy confidence weights
+        # Strict pruning: If strategy assigns 0 weight, do NOT generate.
+        w_br = self.strategy.hyp_weights.get("branch",1.0) if self.strategy else 1.0
+        w_ch = self.strategy.hyp_weights.get("chain",1.0) if self.strategy else 1.0
+        w_co = self.strategy.hyp_weights.get("coherence",1.0) if self.strategy else 1.0
+        w_rc = self.strategy.hyp_weights.get("residual_chain",1.0) if self.strategy else 1.0
+        w_mf = self.strategy.hyp_weights.get("manifold",1.0) if self.strategy else 1.0
+
+        if w_br > 0.01: hyps.extend(self._branch_hypotheses(problem,model,l9))
+        if w_ch > 0.01: hyps.extend(self._chain_hypotheses(problem,model,l7))
+        if w_co > 0.01: hyps.extend(self._coherence_hypotheses(problem,model,l8))
+        if w_rc > 0.01: hyps.extend(self._residual_chain_hypotheses(problem,model,l9))
+        if w_mf > 0.01 and round_idx>=3: hyps.extend(self._manifold_tangent_hypotheses(problem,model,l9))
+
         if self.strategy:
             for hyp in hyps:
                 w=self.strategy.hyp_weights.get(hyp.h_type,1.0)
                 hyp.confidence=min(0.99,hyp.confidence*w)
+
         hyps=[h for h in hyps if h.hid not in model.failure_patterns]
         return sorted(hyps,key=lambda h:-h.confidence)
 
@@ -1008,305 +1016,94 @@ def _test_hypothesis(problem,hyp):
     return best_b,best_ce
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 12: WISDOM LAYER
-# The PSLTranslator is the core fix:
-#   domain PSL = base constraints (real, full weight) +
-#                soft domain structural hints (weight 0.15)
-#   observations pin variables via zero-width VAR bounds
+# SECTION 12: AXIOMATIC RAY TRACER (THE THEORIST)
+# Fires strict conceptual sets at the base problem. VerifyLayer arbitrates.
 # ══════════════════════════════════════════════════════════════════════
-class Axiom:
-    DISCRETE="DISCRETE"; CONTINUOUS="CONTINUOUS"; METRIC="METRIC"; NETWORK="NETWORK"
-    INJECTIVE="INJECTIVE"; SURJECTIVE="SURJECTIVE"; CONSERVED="CONSERVED"; MUTABLE="MUTABLE"
-    QUADRATIC="QUADRATIC"; BILINEAR="BILINEAR"; ORDERED="ORDERED"; SYMMETRIC="SYMMETRIC"
-    TRANSITIVE="TRANSITIVE"; ATOMIC="ATOMIC"; COMPOSITE="COMPOSITE"
-
-AXIOM_CONTRADICTIONS=[
-    {Axiom.DISCRETE,Axiom.CONTINUOUS},{Axiom.INJECTIVE,Axiom.SURJECTIVE},
-    {Axiom.ORDERED,Axiom.SYMMETRIC},{Axiom.ATOMIC,Axiom.COMPOSITE},
-    {Axiom.CONSERVED,Axiom.MUTABLE}]
-
-@dataclass
-class AbstractDomain:
-    name:str; axioms:Set[str]; derivation:str="Base"; confidence:float=1.0
-    def is_consistent(self): return not any(p.issubset(self.axioms) for p in AXIOM_CONTRADICTIONS)
-
-BASE_LIBRARY=[
-    AbstractDomain("GraphSpace",{Axiom.DISCRETE,Axiom.NETWORK,Axiom.SYMMETRIC,Axiom.ATOMIC}),
-    AbstractDomain("MetricPacking",{Axiom.DISCRETE,Axiom.METRIC,Axiom.INJECTIVE,Axiom.CONSERVED}),
-    AbstractDomain("FluidContinuum",{Axiom.CONTINUOUS,Axiom.METRIC,Axiom.SURJECTIVE,Axiom.CONSERVED,Axiom.MUTABLE}),
-    AbstractDomain("SequentialChain",{Axiom.DISCRETE,Axiom.ORDERED,Axiom.TRANSITIVE,Axiom.BILINEAR,Axiom.ATOMIC}),
-    AbstractDomain("HierarchicalTree",{Axiom.DISCRETE,Axiom.NETWORK,Axiom.ORDERED,Axiom.COMPOSITE}),
-    AbstractDomain("NormManifold",{Axiom.CONTINUOUS,Axiom.QUADRATIC,Axiom.CONSERVED,Axiom.METRIC,Axiom.SYMMETRIC}),
-    AbstractDomain("BilinearCoupling",{Axiom.CONTINUOUS,Axiom.BILINEAR,Axiom.NETWORK,Axiom.CONSERVED,Axiom.MUTABLE}),
-    AbstractDomain("DiscreteSchedule",{Axiom.DISCRETE,Axiom.ORDERED,Axiom.INJECTIVE,Axiom.CONSERVED,Axiom.ATOMIC}),
-    AbstractDomain("PhaseJump",{Axiom.DISCRETE,Axiom.MUTABLE,Axiom.SYMMETRIC,Axiom.NETWORK,Axiom.ATOMIC}),
-]
-
-class WisdomOps:
-    @staticmethod
-    def _fn(n): return n if len(n)<22 else n[:19]+"..."
-    @staticmethod
-    def union(d1,d2):
-        merged=d1.axioms|d2.axioms
-        c=AbstractDomain(WisdomOps._fn(f"{d1.name}U{d2.name}"),merged,"Union",(d1.confidence+d2.confidence)/2)
-        for pair in AXIOM_CONTRADICTIONS:
-            if pair.issubset(c.axioms):
-                counts={ax:sum(ax in d.axioms for d in BASE_LIBRARY) for ax in pair}
-                c.axioms.discard(min(counts,key=counts.get))
-        return c
-    @staticmethod
-    def relax(d,axioms): return AbstractDomain(WisdomOps._fn(f"{d.name}_Rlx"),d.axioms-axioms,"Relax",d.confidence*0.85)
-    @staticmethod
-    def inject(d,axioms):
-        merged=d.axioms|axioms; ax_str="".join(a[:2] for a in axioms)
-        c=AbstractDomain(WisdomOps._fn(f"{d.name}+{ax_str}"),merged,"Inject",d.confidence*0.9)
-        for pair in AXIOM_CONTRADICTIONS:
-            if pair.issubset(c.axioms):
-                to_rm=pair-d.axioms
-                if to_rm: c.axioms-=to_rm
-        return c
-    @staticmethod
-    def dual(d):
-        fm={Axiom.DISCRETE:Axiom.CONTINUOUS,Axiom.CONTINUOUS:Axiom.DISCRETE,
-            Axiom.INJECTIVE:Axiom.SURJECTIVE,Axiom.SURJECTIVE:Axiom.INJECTIVE,
-            Axiom.ORDERED:Axiom.SYMMETRIC,Axiom.SYMMETRIC:Axiom.ORDERED,
-            Axiom.CONSERVED:Axiom.MUTABLE,Axiom.MUTABLE:Axiom.CONSERVED,
-            Axiom.ATOMIC:Axiom.COMPOSITE,Axiom.COMPOSITE:Axiom.ATOMIC}
-        return AbstractDomain(WisdomOps._fn(f"{d.name}*"),{fm.get(ax,ax) for ax in d.axioms},"Dual",d.confidence*0.7)
-
-class PSLTranslator:
-    """
-    THE CORE FIX.
-    Generates domain PSL = base constraints (full weight) + soft domain hints (0.15).
-    Observations are pinned via zero-width VAR bounds.
-    Domain NEVER replaces the base problem — it only adds soft guidance.
-    """
-    SOFT = 0.15
-
-    def compile(self, domain:AbstractDomain, axl_def:AXLProblemDef) -> str:
-        ax=domain.axioms; variables=axl_def.variables_list(); n=len(variables)
-        lines=[f"SPACE domain_{domain.name.replace(' ','_')}"]
-
-        # ── 1. Variables: use actual bounds, pin observations ──────────
-        for v in axl_def.variables:
-            lo,hi=v["lo"],v["hi"]
-            if v["name"] in axl_def.observations:
-                val=axl_def.observations[v["name"]]; lo=hi=val   # PINNED
-            lines.append(f"VAR {v['name']} {lo} {hi}")
-
-        # ── 2. Base global constraints — ALWAYS, full weight ───────────
-        for c in axl_def.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}")
-
-        # ── 3. Base scopes — ALWAYS, at their original ORDER ──────────
-        for sc in axl_def.scopes:
-            order=sc.get("order",0)
-            dep=f" DEPENDS {' '.join(sc.get('depends',[]))}" if sc.get('depends') else ""
-            lines.append(f"SCOPE {sc['name']} ORDER {order}{dep}")
-            if sc.get("vars"): lines.append(f"  LINK {' '.join(sc['vars'])}")
-            for c in sc.get("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}")
-            lines.append("END")
-
-        # ── 4. Soft domain structural hints — ORDER 100+, weight 0.15 ─
-        # These nudge the search without overriding base constraints.
-        si=100
-
-        if Axiom.ORDERED in ax and Axiom.BILINEAR not in ax and n>=2:
-            lines.append(f"SCOPE domain_order ORDER {si}")
-            lines.append(f"  LINK {' '.join(variables)}")
-            for i in range(n-1):
-                lines.append(f"  GEQ {variables[i+1]} - {variables[i]} WEIGHT {self.SOFT}")
-            lines.append("END"); si+=1
-
-        if Axiom.SYMMETRIC in ax and Axiom.NETWORK in ax and n>=2:
-            lines.append(f"SCOPE domain_sym ORDER {si}")
-            lines.append(f"  LINK {' '.join(variables[:min(4,n)])}")
-            for i in range(0,min(4,n)-1,2):
-                lines.append(f"  EQ {variables[i]} + {variables[i+1]} WEIGHT {self.SOFT}")
-            lines.append("END"); si+=1
-
-        if Axiom.METRIC in ax and Axiom.INJECTIVE in ax and n>=2:
-            lines.append(f"SCOPE domain_sep ORDER {si}")
-            lines.append(f"  LINK {' '.join(variables[:min(4,n)])}")
-            for a,b in itertools.combinations(range(min(4,n)),2):
-                lines.append(f"  GEQ ({variables[a]} - {variables[b]})**2 - 0.04 WEIGHT {self.SOFT}")
-            lines.append("END"); si+=1
-
-        if Axiom.BILINEAR in ax and n>=2:
-            lines.append(f"SCOPE domain_bilinear ORDER {si}")
-            grp=variables[:min(3,n)]
-            lines.append(f"  LINK {' '.join(grp)}")
-            for j in range(len(grp)-1):
-                lines.append(f"  EQ {grp[j]}*{grp[j+1]} WEIGHT {self.SOFT}")
-            lines.append("END"); si+=1
-
-        if Axiom.MANIFOLD_HINT(ax) and n>=2:
-            # Soft quadratic regularisation — only if base has no quadratic conserve
-            has_quad=any("**2" in c.get("expr","") and c["kind"]=="CONSERVE" for c in axl_def.constraints)
-            if not has_quad:
-                lines.append(f"SCOPE domain_quad ORDER {si}")
-                lines.append(f"  LINK {' '.join(variables)}")
-                lines.append(f"  EQ {' + '.join(f'{v}**2' for v in variables)} - {float(n)*0.25:.2f} WEIGHT {self.SOFT}")
-                lines.append("END"); si+=1
-
-        return "\n".join(lines)
-
-# Small helper — avoid if-chain sprawl
-def _manifold_hint(ax): return Axiom.QUADRATIC in ax and Axiom.CONSERVED not in ax
-Axiom.MANIFOLD_HINT = staticmethod(_manifold_hint)
-
 @dataclass
-class DebateRound:
-    round_idx:int; domain:AbstractDomain; psl_text:str
-    ce:float; solved:bool; action:str; strategy_name:str=""
-    traces:List[HypothesisTrace]=field(default_factory=list)
-
-class WisdomDebate:
-    MAX_ROUNDS=6
-    def __init__(self,library=None):
-        self.library=library or list(BASE_LIBRARY)
-        self.translator=PSLTranslator()
-        self.history:List[DebateRound]=[]
-        self.best_ce=float('inf'); self.best_binding={}; self.best_domain=None
-        self.all_traces:List[HypothesisTrace]=[]
-
-    def _critic_score(self,problem_axioms,domain):
-        unmapped=problem_axioms-domain.axioms; false_asm=domain.axioms-problem_axioms
-        score=len(unmapped)*2.0+len(false_asm)*1.0
-        if not domain.is_consistent(): score+=10.0
-        return score,unmapped,false_asm
-
-    def _candidates(self,current,round_idx):
-        cands=[(d,"Library") for d in self.library]
-        for d1,d2 in itertools.combinations(self.library[:5],2):
-            cands.append((WisdomOps.union(d1,d2),"Union"))
-        for d in self.library[:4]: cands.append((WisdomOps.dual(d),"Dual"))
-        if round_idx>2:
-            chosen=random.sample([Axiom.BILINEAR,Axiom.QUADRATIC,Axiom.CONSERVED,Axiom.METRIC,Axiom.ORDERED],2)
-            cands.append((WisdomOps.inject(current,set(chosen)),"RandInject"))
-        return cands
-
-    def debate(self,axl_def:AXLProblemDef,base_problem:Problem) -> Tuple[Dict,float,List[DebateRound]]:
-        problem_axioms=axl_def.axioms
-        current=min(self.library,key=lambda d:self._critic_score(problem_axioms,d)[0])
-        self.history=[]; self.best_ce=float('inf'); self.best_binding={}; self.all_traces=[]
-
-        print(f"\n{'═'*60}\nDEBATE: {axl_def.name} | Axioms: {problem_axioms}\n{'═'*60}")
-
-        for round_idx in range(self.MAX_ROUNDS):
-            cands=self._candidates(current,round_idx)
-            scored=[(self._critic_score(problem_axioms,d)[0],d,act) for d,act in cands]
-            scored.sort(key=lambda x:x[0])
-            tried={r.domain.name for r in self.history}
-            score,winner,action=next((s for s in scored if s[1].name not in tried),scored[0])
-            strategy=get_strategy(winner.name)
-
-            print(f"\n[R{round_idx+1}] {winner.name} | {action} | score={score:.1f} | strategy={strategy.name}")
-            print(f"       hint: {strategy.note[:60]}")
-
-            # ── KEY FIX: translate generates base + soft hints ─────────
-            psl_text=self.translator.compile(winner,axl_def)
-            round_traces=[]
-
-            try:
-                prog=parse_psl(psl_text); ep=expand_psl(prog)
-                if not ep.variables:
-                    print("       ✗ No variables"); current=winner; continue
-
-                dom_prob=Problem(pid=f"dom_{winner.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)
-                t_start=time.time()
-                # ── KEY FIX: solver receives domain strategy ───────────
-                result=solve_by_hypothesis(dom_prob,budget=TOTAL_BUDGET,strategy=strategy)
-                elapsed=round((time.time()-t_start)*1000,1)
-                binding=result["binding"]; ce=result["ce"]; solved=result["solved"]
-
-                # Verify against base problem + anchors
-                verify=VERIFY_LAYER.run(binding,base_problem,axl_def.anchors)
-                base_ce=verify.gate1_ce  # this IS the true base CE now
-
-                trace=HypothesisTrace(
-                    hid=f"R{round_idx+1}_{winner.name[:10]}",
-                    round_idx=round_idx+1, domain_name=winner.name,
-                    action=action, ce_before=self.best_ce if self.best_ce<float('inf') else 99.0,
-                    ce_after=base_ce, verify=verify,
-                    survived=verify.overall_pass, elapsed_ms=elapsed,
-                    strategy_note=strategy.polish)
-                round_traces.append(trace); self.all_traces.append(trace)
-
-                status="✓ SURVIVED" if verify.overall_pass else "✗ FAILED"
-                print(f"       DomCE={ce:.5f} BaseCE={base_ce:.5f} | "
-                      f"G1={'✓' if verify.gate1_pass else '✗'} G2={'✓' if verify.gate2_pass else '✗'} | {status}")
-                for inv_name,(err,passed) in verify.gate2_results.items():
-                    print(f"         [{'✓' if passed else '✗'}] {inv_name}: |err|={err:.6f}")
-
-                if base_ce<self.best_ce:
-                    self.best_ce=base_ce; self.best_binding=dict(binding); self.best_domain=winner
-
-                if verify.overall_pass:
-                    self.history.append(DebateRound(round_idx,winner,psl_text,base_ce,
-                                                     verify.overall_pass,action,strategy.name,round_traces))
-                    print(f"\n✓ VERIFIED + SOLVED in round {round_idx+1}"); break
-
-            except Exception as e:
-                import traceback; traceback.print_exc()
-                trace=HypothesisTrace(hid=f"R{round_idx+1}_ERR",round_idx=round_idx+1,
-                    domain_name=winner.name,action=action,ce_before=99.0,ce_after=99.0,
-                    verify=None,survived=False,elapsed_ms=0)
-                round_traces.append(trace); self.all_traces.append(trace)
-
-            self.history.append(DebateRound(round_idx,winner,psl_text,
-                self.best_ce,self.best_ce<SOLVE_THRESHOLD,action,strategy.name,round_traces))
-            current=winner
-
-        print(f"\n{'─'*60}\nRESULT: BaseCE={self.best_ce:.5f} | Domain={self.best_domain.name if self.best_domain else '?'}")
-        return self.best_binding,self.best_ce,self.history
+class RayTraceRound:
+    round_idx:int; ray_axioms:Set[str]; ray_name:str
+    ce:float; solved:bool; traces:List[HypothesisTrace]=field(default_factory=list)
+
+class AxiomRayTracer:
+    WAVEFRONT_SIZE = 6
+
+    def trace(self, axl_def: AXLProblemDef, base_problem: Problem) -> Tuple[Dict, float, List[RayTraceRound]]:
+        self.all_traces = []
+        best_ce = float('inf')
+        best_binding = {}
+        best_ray = None
+        history = []
+
+        # Phase 1: The Wavefront (Sample diverse universal rays)
+        rays_to_test = random.sample(AXIOM_HYPERCUBE, self.WAVEFRONT_SIZE)
+        
+        # Always test the explicitly defined axioms as a baseline ray
+        if axl_def.axioms and axl_def.axioms not in rays_to_test:
+            rays_to_test[0] = axl_def.axioms
+
+        print(f"\n{'═'*65}\nTHEORIST RAY TRACE: {axl_def.name}\n{'═'*65}")
+
+        for round_idx, ray_axioms in enumerate(rays_to_test):
+            strategy = compile_strategy(ray_axioms)
+            print(f"\n[Ray {round_idx+1}/{self.WAVEFRONT_SIZE}] Firing: {strategy.name}")
+            
+            t_start = time.time()
+            # Strict solver search using base problem + axiom strategy limits
+            result = solve_by_hypothesis(base_problem, budget=TOTAL_BUDGET, strategy=strategy)
+            elapsed = round((time.time()-t_start)*1000, 1)
+            
+            binding = result["binding"]
+            
+            # The VerifyLayer is the absolute arbiter.
+            verify = VERIFY_LAYER.run(binding, base_problem, axl_def.anchors)
+            base_ce = verify.gate1_ce 
+            
+            trace = HypothesisTrace(
+                hid=f"R{round_idx+1}", round_idx=round_idx+1,
+                ray_name=strategy.name, action="Wavefront",
+                ce_before=best_ce if best_ce < float('inf') else 99.0,
+                ce_after=base_ce, verify=verify,
+                survived=verify.overall_pass, elapsed_ms=elapsed
+            )
+            self.all_traces.append(trace)
+
+            status = "✓ SURVIVED" if verify.overall_pass else "✗ FAILED"
+            print(f"       BaseCE={base_ce:.5f} | G1={'✓' if verify.gate1_pass else '✗'} "
+                  f"G2={'✓' if verify.gate2_pass else '✗'} | {status}")
+            for inv_name, (err, passed) in verify.gate2_results.items():
+                print(f"         [{'✓' if passed else '✗'}] {inv_name}: |err|={err:.6f}")
+
+            if base_ce < best_ce:
+                best_ce = base_ce
+                best_binding = dict(binding)
+                best_ray = strategy.name
+
+            history.append(RayTraceRound(round_idx, ray_axioms, strategy.name, base_ce, verify.overall_pass, [trace]))
+
+            if verify.overall_pass:
+                print(f"\n✓ TRUE UNIVERSE FOUND in Ray {round_idx+1}"); break
+
+        print(f"\n{'─'*65}\nRESULT: BaseCE={best_ce:.5f} | Best Ray={best_ray}")
+        return best_binding, best_ce, history
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 13: HARDCODED AXL PROBLEMS (all verified feasible)
+# SECTION 13: HARDCODED AXL PROBLEMS
 # ══════════════════════════════════════════════════════════════════════
 AXL_PROBLEMS=[
-
-    # ── PROBLEM 1: NormManifold4D ─────────────────────────────────────
-    # x1 pinned at 0.5. Find x2,x3,x4 on unit sphere summing to -0.5.
-    # Known solution family: x2=-0.809, x3=0.309, x4=0 (and rotations)
     AXLProblemDef(
         name="NormManifold4D",
         description="4 vars on unit sphere, zero sum, x1 observed at 0.5",
         axioms={Axiom.CONTINUOUS,Axiom.QUADRATIC,Axiom.CONSERVED,Axiom.METRIC,Axiom.SYMMETRIC},
         variables=[
-            {"name":"x1","lo":-1.0,"hi":1.0},
-            {"name":"x2","lo":-1.0,"hi":1.0},
-            {"name":"x3","lo":-1.0,"hi":1.0},
-            {"name":"x4","lo":-1.0,"hi":1.0},
+            {"name":"x1","lo":-1.0,"hi":1.0}, {"name":"x2","lo":-1.0,"hi":1.0},
+            {"name":"x3","lo":-1.0,"hi":1.0}, {"name":"x4","lo":-1.0,"hi":1.0},
         ],
         constraints=[
             {"kind":"CONSERVE","expr":"x1**2 + x2**2 + x3**2 + x4**2 - 1.0"},
             {"kind":"EQ",      "expr":"x1 + x2 + x3 + x4","weight":2.0},
         ],
         scopes=[{"name":"sphere","order":0,"vars":["x1","x2","x3","x4"],
-                 "constraints":[
-                    {"kind":"EQ","expr":"x1**2 + x2**2 + x3**2 + x4**2 - 1.0","weight":5.0},
-                 ]}],
+                 "constraints":[{"kind":"EQ","expr":"x1**2 + x2**2 + x3**2 + x4**2 - 1.0","weight":5.0}]}],
         anchors=[
             AXLInvariant("unit_sphere","x1**2 + x2**2 + x3**2 + x4**2 - 1.0",1e-3),
             AXLInvariant("zero_sum","x1 + x2 + x3 + x4",1e-3),
@@ -1314,9 +1111,6 @@ AXL_PROBLEMS=[
         ],
         observations={"x1":0.5},
     ),
-
-    # ── PROBLEM 2: BilinearChain6 ─────────────────────────────────────
-    # Known exact solution: t1=0.5,t2=1.0,t3=1.0,t4=2.0,t5=1.5,t6=3.0
     AXLProblemDef(
         name="BilinearChain6",
         description="6-var ordered chain with bilinear products and sum conservation",
@@ -1324,10 +1118,8 @@ AXL_PROBLEMS=[
         variables=[{"name":f"t{i}","lo":0.0,"hi":3.0} for i in range(1,7)],
         constraints=[
             {"kind":"CONSERVE","expr":"t1 + t2 + t3 + t4 + t5 + t6 - 9.0"},
-            {"kind":"GEQ","expr":"t2 - t1","weight":1.0},
-            {"kind":"GEQ","expr":"t3 - t2","weight":1.0},
-            {"kind":"GEQ","expr":"t4 - t3","weight":1.0},
-            {"kind":"GEQ","expr":"t5 - t4","weight":1.0},
+            {"kind":"GEQ","expr":"t2 - t1","weight":1.0}, {"kind":"GEQ","expr":"t3 - t2","weight":1.0},
+            {"kind":"GEQ","expr":"t4 - t3","weight":1.0}, {"kind":"GEQ","expr":"t5 - t4","weight":1.0},
             {"kind":"GEQ","expr":"t6 - t5","weight":1.0},
         ],
         scopes=[{"name":"chain","order":0,"vars":[f"t{i}" for i in range(1,7)],
@@ -1343,59 +1135,40 @@ AXL_PROBLEMS=[
             AXLInvariant("bilinear_hi","t5*t6 - 4.5",0.05),
         ],
     ),
-
-    # ── PROBLEM 3: PhaseCollider (FIXED — provably feasible) ──────────
-    # Conservation: p2 = -p1 (momentum = 0)
-    # Phase A: |p1|=0.5, separation=1.0. Phase B: |p1|=1.0, separation=4.0
-    # Branch on p1 radius; separation follows from conservation automatically.
     AXLProblemDef(
         name="PhaseCollider",
         description="2-particle symmetric collision: conservation + phase branch",
         axioms={Axiom.DISCRETE,Axiom.MUTABLE,Axiom.SYMMETRIC,Axiom.NETWORK,Axiom.CONSERVED},
         variables=[
-            {"name":"p1x","lo":-2.0,"hi":2.0},
-            {"name":"p2x","lo":-2.0,"hi":2.0},
-            {"name":"p1y","lo":-2.0,"hi":2.0},
-            {"name":"p2y","lo":-2.0,"hi":2.0},
+            {"name":"p1x","lo":-2.0,"hi":2.0}, {"name":"p2x","lo":-2.0,"hi":2.0},
+            {"name":"p1y","lo":-2.0,"hi":2.0}, {"name":"p2y","lo":-2.0,"hi":2.0},
         ],
         constraints=[
-            {"kind":"CONSERVE","expr":"p1x + p2x"},   # total momentum x = 0
-            {"kind":"CONSERVE","expr":"p1y + p2y"},   # total momentum y = 0
+            {"kind":"CONSERVE","expr":"p1x + p2x"}, {"kind":"CONSERVE","expr":"p1y + p2y"},
         ],
         scopes=[{"name":"phase","order":0,"vars":["p1x","p2x","p1y","p2y"],
                  "constraints":[
-                    # Phase branch: p1 at radius 0.5 OR radius 1.0
                     {"kind":"BRANCH","name":"phase_select","options":[
-                        "p1x**2 + p1y**2 - 0.25",   # phase A: r=0.5
-                        "p1x**2 + p1y**2 - 1.0",    # phase B: r=1.0
+                        "p1x**2 + p1y**2 - 0.25", "p1x**2 + p1y**2 - 1.0",
                     ]},
-                    # Symmetry: p2 = -p1 (follows from conservation, reinforced)
                     {"kind":"EQ","expr":"p1x + p2x","weight":3.0},
                     {"kind":"EQ","expr":"p1y + p2y","weight":3.0},
                  ]}],
         anchors=[
             AXLInvariant("momentum_x","p1x + p2x",1e-3),
             AXLInvariant("momentum_y","p1y + p2y",1e-3),
-            # Phase satisfied: product of both phase residuals near 0
-            AXLInvariant("phase_A_or_B",
-                "(p1x**2 + p1y**2 - 0.25)*(p1x**2 + p1y**2 - 1.0)",0.05),
+            AXLInvariant("phase_A_or_B","(p1x**2 + p1y**2 - 0.25)*(p1x**2 + p1y**2 - 1.0)",0.05),
         ],
     ),
-
-    # ── PROBLEM 4: MetricPacking3D ────────────────────────────────────
-    # Known solution: a=-sqrt(3), b=0, c=sqrt(3) ≈ (-1.732, 0, 1.732)
-    # centred: 0 ✓, sep_ab: 3 ≥ 1 ✓, sep_bc: 3 ≥ 1 ✓, sep_ac: 12 ≥ 4 ✓, norm: 6 ✓
     AXLProblemDef(
         name="MetricPacking3D",
         description="3 vars packed with min separation, centred, norm=6",
         axioms={Axiom.CONTINUOUS,Axiom.METRIC,Axiom.INJECTIVE,Axiom.CONSERVED,Axiom.SYMMETRIC},
         variables=[
-            {"name":"a","lo":-3.0,"hi":3.0},
-            {"name":"b","lo":-3.0,"hi":3.0},
-            {"name":"c","lo":-3.0,"hi":3.0},
+            {"name":"a","lo":-3.0,"hi":3.0}, {"name":"b","lo":-3.0,"hi":3.0}, {"name":"c","lo":-3.0,"hi":3.0},
         ],
         constraints=[
-            {"kind":"CONSERVE","expr":"a + b + c"},          # centred at 0
+            {"kind":"CONSERVE","expr":"a + b + c"},
             {"kind":"GEQ","expr":"(a - b)**2 - 1.0","weight":2.0},
             {"kind":"GEQ","expr":"(b - c)**2 - 1.0","weight":2.0},
             {"kind":"GEQ","expr":"(a - c)**2 - 4.0","weight":2.0},
@@ -1406,7 +1179,7 @@ AXL_PROBLEMS=[
                  ]}],
         anchors=[
             AXLInvariant("centred","a + b + c",1e-3),
-            AXLInvariant("sep_ab","(a - b)**2 - 1.0",0.5),   # ≥ 1 (tolerance on residual)
+            AXLInvariant("sep_ab","(a - b)**2 - 1.0",0.5),
             AXLInvariant("sep_bc","(b - c)**2 - 1.0",0.5),
             AXLInvariant("norm_6","a**2 + b**2 + c**2 - 6.0",0.05),
         ],
@@ -1426,46 +1199,41 @@ def build_base_problem(axl_def:AXLProblemDef) -> Problem:
 # ══════════════════════════════════════════════════════════════════════
 STATE_LOCK=threading.Lock()
 RUN_LOG:List[Dict]=[]
-DEBATE_ENGINE=WisdomDebate()
+THEORIST=AxiomRayTracer()
 POOL=ThreadPoolExecutor(max_workers=2)
 
 def _run_problem(axl_def:AXLProblemDef):
-    t0=time.time()
     try:
-        base_prob=build_base_problem(axl_def)
-        binding,ce,rounds=DEBATE_ENGINE.debate(axl_def,base_prob)
-        elapsed=round(time.time()-t0,2)
-        survived=[t for t in DEBATE_ENGINE.all_traces if t.survived]
-        failed=[t for t in DEBATE_ENGINE.all_traces if not t.survived]
-        best_trace=min((t for t in survived),key=lambda t:t.ce_after,default=None)
-        actual_base_ce=base_prob.constraint_energy(binding)
+        base_prob = build_base_problem(axl_def)
+        binding, ce, rounds = THEORIST.trace(axl_def, base_prob)
+        
+        survived = [t for t in THEORIST.all_traces if t.survived]
+        failed = [t for t in THEORIST.all_traces if not t.survived]
+        best_trace = min(survived, key=lambda t: t.ce_after, default=None)
+        
         record={
-            "problem":axl_def.name,
-            "description":axl_def.description,
-            "axioms":sorted(axl_def.axioms),
-            "ce":round(actual_base_ce,6),
-            "solved":len(survived)>0 and actual_base_ce<SOLVE_THRESHOLD,
-            "elapsed":elapsed,
-            "binding":{k:round(v,5) for k,v in binding.items()},
-            "observations":axl_def.observations,
-            "traces":[{
-                "hid":t.hid,"round":t.round_idx,"domain":t.domain_name,
-                "action":t.action,"strategy":t.strategy_note,
-                "ce":round(t.ce_after,5),
-                "g1_ce":round(t.verify.gate1_ce,5) if t.verify else None,
-                "g1":t.verify.gate1_pass if t.verify else False,
-                "g2":t.verify.gate2_pass if t.verify else False,
-                "g2_detail":{k:(round(err,6),ok)
-                              for k,(err,ok) in t.verify.gate2_results.items()} if t.verify else {},
-                "survived":t.survived,"ms":t.elapsed_ms,
-            } for t in DEBATE_ENGINE.all_traces],
-            "survived_count":len(survived),
-            "failed_count":len(failed),
-            "best_domain":best_trace.domain_name if best_trace else "—",
+            "problem": axl_def.name,
+            "description": axl_def.description,
+            "ce": round(ce, 6),
+            "solved": len(survived) > 0 and ce < SOLVE_THRESHOLD,
+            "binding": {k: round(v, 5) for k, v in binding.items()},
+            "observations": axl_def.observations,
+            "traces": [{
+                "round": t.round_idx, "ray": t.ray_name,
+                "ce": round(t.ce_after, 5),
+                "g1_ce": round(t.verify.gate1_ce, 5) if t.verify else None,
+                "g1": t.verify.gate1_pass if t.verify else False,
+                "g2": t.verify.gate2_pass if t.verify else False,
+                "g2_detail": {k: (round(err, 6), ok) for k, (err, ok) in t.verify.gate2_results.items()} if t.verify else {},
+                "survived": t.survived, "ms": t.elapsed_ms,
+            } for t in THEORIST.all_traces],
+            "survived_count": len(survived),
+            "failed_count": len(failed),
+            "best_ray": best_trace.ray_name if best_trace else "—",
         }
         with STATE_LOCK:
             RUN_LOG.append(record)
-            if len(RUN_LOG)>40: RUN_LOG.pop(0)
+            if len(RUN_LOG) > 40: RUN_LOG.pop(0)
     except Exception as e:
         import traceback; traceback.print_exc()
         print(f"[RUN ERROR] {axl_def.name}: {e}")
@@ -1474,7 +1242,7 @@ async def run_loop():
     loop=asyncio.get_event_loop()
     while True:
         prob=random.choice(AXL_PROBLEMS)
-        await loop.run_in_executor(POOL,_run_problem,prob)
+        await loop.run_in_executor(POOL, _run_problem, prob)
         await asyncio.sleep(0.3)
 
 @asynccontextmanager
@@ -1486,7 +1254,7 @@ async def lifespan(app):
 # ══════════════════════════════════════════════════════════════════════
 # SECTION 15: FASTAPI + DASHBOARD
 # ══════════════════════════════════════════════════════════════════════
-app=FastAPI(title="Practicality 11.1",lifespan=lifespan)
+app=FastAPI(title="Practicality 12.0",lifespan=lifespan)
 
 def _render_collapse(record:Dict) -> str:
     b=record["binding"]; traces=record["traces"]
@@ -1516,14 +1284,12 @@ def _render_collapse(record:Dict) -> str:
 
     def trail_span(t):
         c="#4CAF50" if t["survived"] else "#333"
-        star=" ◀ SURVIVED" if t["survived"] else ""
-        strat=f" [{t.get('strategy','')}]" if t.get("strategy") else ""
+        star=" ◀ VERIFIED" if t["survived"] else ""
         return (f"<div style='color:{c};font-size:0.78em;margin-bottom:3px'>"
-                f"[R{t['round']}] <span style='color:#FF9800'>{t['domain'][:14]}</span>"
-                f"  CE={t['ce']:.5f}"
-                f"  G1={'✓' if t['g1'] else '✗'}{t.get('g1_ce',0):.4f}"
-                f"  G2={'✓' if t['g2'] else '✗'}"
-                f"<span style='color:#555'>{strat}</span>"
+                f"[R{t['round']}] <span style='color:#FF9800'>{t['ray']}</span>"
+                f"  CE={t['ce']:.5f} | "
+                f"G1={'✓' if t['g1'] else '✗'}{t.get('g1_ce',0):.4f} "
+                f"G2={'✓' if t['g2'] else '✗'} "
                 f"<span style='color:#4CAF50;font-weight:700'>{star}</span></div>")
 
     trail="".join(trail_span(t) for t in traces)
@@ -1534,7 +1300,6 @@ def _render_collapse(record:Dict) -> str:
     <span style='color:{ce_color};font-weight:700;font-size:1.05em'>{status}</span>
     <span style='color:#444;font-size:0.85em'>{record["problem"]}</span>
     <span style='color:#333;font-size:0.8em'>BaseCE={ce:.6f}</span>
-    <span style='color:#555;font-size:0.75em'>{record["elapsed"]}s</span>
     <span style='color:#26C6DA;font-size:0.75em'>{record["survived_count"]} survived / {record["failed_count"]} failed</span>
   </div>
   <div style='display:flex'>
@@ -1542,7 +1307,7 @@ def _render_collapse(record:Dict) -> str:
       <div style='color:#333;font-size:0.7em;margin-bottom:5px'>BINDING</div>
       <table style='border-collapse:collapse;width:100%'>{binding_rows}</table>
     </div>
-    <div style='flex:0 0 200px;padding:10px 12px;border-right:1px solid #1a1a1a'>
+    <div style='flex:0 0 230px;padding:10px 12px;border-right:1px solid #1a1a1a'>
       <div style='color:#333;font-size:0.7em;margin-bottom:5px'>INVARIANTS (Gate 2)</div>
       <table style='border-collapse:collapse;width:100%'>
         {inv_rows or "<tr><td colspan='3' style='color:#222'>—</td></tr>"}
@@ -1550,7 +1315,7 @@ def _render_collapse(record:Dict) -> str:
     </div>
     <div style='flex:1;padding:10px 12px'>
       <div style='color:#333;font-size:0.7em;margin-bottom:5px'>
-        HYPOTHESIS TRAIL — best domain: <span style='color:#FF9800'>{record["best_domain"]}</span>
+        WAVEFRONT RAYS — best: <span style='color:#FF9800'>{record["best_ray"]}</span>
       </div>
       {trail}
     </div>
@@ -1563,29 +1328,33 @@ async def dashboard():
     runs=len(RUN_LOG); solved=sum(1 for r in RUN_LOG if r.get("solved",False))
     avg_ce=round(sum(r["ce"] for r in RUN_LOG)/max(1,runs),5) if RUN_LOG else 0
 
-    all_traces=[t for r in log for t in r.get("traces",[])]
-    ds=defaultdict(lambda:{"tried":0,"survived":0,"total_ce":0.0,"strategy":""})
-    for t in all_traces:
-        ds[t["domain"]]["tried"]+=1
-        ds[t["domain"]]["total_ce"]+=t["ce"]
-        ds[t["domain"]]["strategy"]=t.get("strategy","")
-        if t["survived"]: ds[t["domain"]]["survived"]+=1
-    domain_rows="".join(
-        f"<tr><td style='color:#FF9800'>{d}</td>"
+    # Calculate efficacy by individual Axiom (very insightful)
+    axiom_stats = defaultdict(lambda: {"tried": 0, "survived": 0, "total_ce": 0.0})
+    for r in log:
+        for t in r.get("traces", []):
+            ray_str = t["ray"].strip("[]")
+            axioms = ray_str.split("|")
+            for ax in axioms:
+                if not ax: continue
+                axiom_stats[ax]["tried"] += 1
+                axiom_stats[ax]["total_ce"] += t["ce"]
+                if t["survived"]: axiom_stats[ax]["survived"] += 1
+
+    axiom_rows="".join(
+        f"<tr><td style='color:#FF9800'>{ax}</td>"
         f"<td style='color:#aaa'>{s['tried']}</td>"
         f"<td style='color:#4CAF50'>{s['survived']}</td>"
         f"<td style='color:#EF5350'>{s['tried']-s['survived']}</td>"
         f"<td style='color:#26C6DA'>{round(s['total_ce']/s['tried'],5) if s['tried'] else 0}</td>"
-        f"<td style='color:#555'>{s['strategy']}</td>"
         f"<td style='color:{'#4CAF50' if s['survived']>0 else '#333'}'>"
         f"{round(s['survived']/s['tried']*100):.0f}%</td></tr>"
-        for d,s in sorted(ds.items(),key=lambda x:-x[1]["survived"])
-    ) or "<tr><td colspan='7' style='color:#222'>Warming up…</td></tr>"
+        for ax,s in sorted(axiom_stats.items(),key=lambda x:-x[1]["survived"])
+    ) or "<tr><td colspan='6' style='color:#222'>Warming up…</td></tr>"
 
     collapses="".join(_render_collapse(r) for r in log) if log else \
         "<div style='color:#222;padding:20px'>Warming up…</div>"
 
-    return f"""<!DOCTYPE html><html><head><title>Practicality 11.1</title>
+    return f"""<!DOCTYPE html><html><head><title>Practicality 12.0</title>
 <meta http-equiv="refresh" content="4">
 <style>
   body{{background:#090909;color:#e0e0e0;font-family:monospace;padding:20px;max-width:1400px}}
@@ -1596,21 +1365,21 @@ async def dashboard():
   th{{color:#2a2a2a;font-size:0.72em}}
   .badge{{display:inline-block;padding:3px 10px;border-radius:3px;background:#0e0e0e;margin:2px;font-size:0.78em;border:1px solid #1a1a1a}}
 </style></head><body>
-<h1>⚗ Practicality 11.1 — AXL/PSL Pipeline (fixed)</h1>
+<h1>⚗ Practicality 12.0 — Axiomatic Ray Tracing</h1>
 <div style='color:#333;font-size:0.75em;margin-bottom:12px'>
-  AXL → PSL (base + soft domain hints) → Solver [strategy-directed] → Gate1 → Gate2 → Collapse
+  Boolean Hypercube → Wavefront Rays → Strict Solver Conf → Absolute Base Verify
 </div>
 <div style='margin-bottom:16px'>
   <span class='badge' style='color:#aaa'>Runs: {runs}</span>
   <span class='badge' style='color:#4CAF50'>Solved: {solved}</span>
   <span class='badge' style='color:#26C6DA'>Avg BaseCE: {avg_ce}</span>
   <span class='badge' style='color:#FF9800'>Problems: {len(AXL_PROBLEMS)}</span>
-  <span class='badge' style='color:#5C6BC0'>Library: {len(DEBATE_ENGINE.library)}</span>
+  <span class='badge' style='color:#5C6BC0'>Valid Universal Rays: {len(AXIOM_HYPERCUBE)}</span>
 </div>
-<h3>Domain Survival + Strategy</h3>
+<h3>Axiom Efficacy Summary (Which properties describe reality best?)</h3>
 <table>
-  <tr><th>Domain</th><th>Tried</th><th>Survived</th><th>Failed</th><th>Avg BaseCE</th><th>Polish</th><th>Rate</th></tr>
-  {domain_rows}
+  <tr><th>Axiom</th><th>Tested</th><th>Survived</th><th>Failed</th><th>Avg BaseCE</th><th>Efficacy</th></tr>
+  {axiom_rows}
 </table>
 <h3>Collapse View — Recent Runs</h3>
 {collapses}