Update app.py

app.py

@@ -1,14 +1,16 @@
 #!/usr/bin/env python3
 """
-PRACTICALITY SYSTEM 11.0 — AXL/PSL PIPELINE
+PRACTICALITY SYSTEM 11.1 — AXL/PSL PIPELINE
 ═══════════════════════════════════════════════════════════════════
-NEW:
-  · PSL 2.0: CONSERVE, WEIGHT, BRANCH, LINK, ORDER, ANNOTATE
-  · AXL layer: hardcoded problem definitions as Python structs
-  · AXL → PSL compiler: deterministic rule table, no LLM
-  · Verify layer: Gate 1 (structural CE) + Gate 2 (invariants)
-  · HypothesisTrace: full survival log per run
-  · Dashboard: collapse view ready for screenshot
+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
 """
 
 import time, random, math, threading, asyncio, warnings, itertools, json
@@ -30,7 +32,7 @@ import uvicorn
 warnings.filterwarnings("ignore")
 USE_GPU = torch.cuda.is_available()
 DEVICE  = torch.device("cuda" if USE_GPU else "cpu")
-print(f"[SYSTEM 11.0] Compute: {'GPU' if USE_GPU else 'CPU'}")
+print(f"[SYSTEM 11.1] Compute: {'GPU' if USE_GPU else 'CPU'}")
 
 # ══════════════════════════════════════════════════════════════════════
 # SECTION 1: CONSTANTS
@@ -127,14 +129,11 @@ def compile_iv(expr,variables):
 @dataclass
 class PSLVar:        name:str; lo:float; hi:float; weight:float=1.0
 @dataclass
-class PSLConstraint: kind:str; expr:str; scope:str="root"; weight:float=1.0; tolerance:float=SOLVE_THRESHOLD; branches:List[str]=field(default_factory=list); annotation:str=""
+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)  # var → axl_field
+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('#')]
@@ -143,18 +142,14 @@ def parse_psl(text:str) -> PSLProgram:
     def advance():
         nonlocal i; l=lines[i]; i+=1; return l
     def peek(): return lines[i] if i<len(lines) else ""
-    def pvar(rest,wt=1.0):
+    def pvar(rest):
         p=rest.split()
-        if len(p)>=3:
-            w=float(p[3]) if len(p)>3 and p[3].replace('.','').replace('-','').isdigit() else wt
-            return PSLVar(p[0],float(p[1]),float(p[2]),w)
-        return None
-    def parse_weight(rest):
-        """Extract WEIGHT value from end of constraint string."""
+        return PSLVar(p[0],float(p[1]),float(p[2])) if len(p)>=3 else None
+    def pw(rest):
         if 'WEIGHT' in rest:
-            parts=rest.split('WEIGHT'); return parts[0].strip(), float(parts[1].split()[0])
+            p=rest.split('WEIGHT'); return p[0].strip(), float(p[1].split()[0])
         return rest.strip(), 1.0
-    def parse_scope_body(sname, order=0, depends=None):
+    def parse_scope_body(sname,order=0,depends=None):
         svars,scons,links=[],[],[]
         while i<len(lines):
             l=peek(); tk=l.split(None,1)
@@ -164,20 +159,17 @@ def parse_psl(text:str) -> PSLProgram:
             if kw=="VAR":
                 v=pvar(rest)
                 if v: svars.append(v)
-            elif kw=="LINK":
-                links.extend(rest.split())
+            elif kw=="LINK": links.extend(rest.split())
             elif kw in ("EQ","GEQ","LEQ"):
-                expr,wt=parse_weight(rest)
-                scons.append(PSLConstraint(kw.lower(),expr,scope=sname,weight=wt))
+                expr,wt=pw(rest); scons.append(PSLConstraint(kw.lower(),expr,scope=sname,weight=wt))
             elif kw=="CONSERVE":
-                expr,_=parse_weight(rest)
-                scons.append(PSLConstraint("eq",expr,scope=sname,weight=10.0))
+                expr,_=pw(rest); scons.append(PSLConstraint("eq",expr,scope=sname,weight=10.0))
             elif kw=="BRANCH":
                 opts=[]
-                while i<len(lines) and not peek().startswith("END"):
+                while i<len(lines) and not peek().upper().startswith("END"):
                     bl=advance()
                     if bl.upper().startswith("OPTION"): opts.append(bl.split(None,1)[1].strip())
-                advance()  # END BRANCH
+                advance()
                 scons.append(PSLConstraint("or_eq","",scope=sname,weight=1.0,branches=opts))
             elif kw=="ANNOTATE":
                 parts=rest.split()
@@ -192,11 +184,9 @@ def parse_psl(text:str) -> PSLProgram:
             v=pvar(rest)
             if v: prog.vars.append(v)
         elif kw in ("EQ","GEQ","LEQ"):
-            expr,wt=parse_weight(rest)
-            prog.constraints.append(PSLConstraint(kw.lower(),expr,weight=wt))
+            expr,wt=pw(rest); prog.constraints.append(PSLConstraint(kw.lower(),expr,weight=wt))
         elif kw=="CONSERVE":
-            expr,_=parse_weight(rest)
-            prog.constraints.append(PSLConstraint("eq",expr,weight=10.0))
+            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"):
@@ -218,9 +208,8 @@ def parse_psl(text:str) -> PSLProgram:
                 idx=rest.upper().index("DEPENDS")
                 depends=rest[idx:].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.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
 
@@ -228,8 +217,8 @@ def parse_psl(text:str) -> PSLProgram:
 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]
-    annotations:Dict[str,str]=field(default_factory=dict)
+    scope_groups:Dict[str,List[int]]; scope_vars:Dict[str,List[str]]
+    scope_order:List[str]; annotations:Dict[str,str]=field(default_factory=dict)
 
 def expand_psl(prog:PSLProgram) -> ExpandedProblem:
     variables=[]; bounds={}; constraints=[]
@@ -275,89 +264,60 @@ def expand_psl(prog:PSLProgram) -> ExpandedProblem:
                            prog.scope_order,prog.annotations)
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 4: AXL LAYER — DATACLASSES + COMPILER
+# SECTION 4: AXL LAYER
 # ══════════════════════════════════════════════════════════════════════
 @dataclass
 class AXLInvariant:
-    name: str
-    expr: str
-    tolerance: float = VERIFY_G2_TOLERANCE
+    name:str; expr:str; tolerance:float=VERIFY_G2_TOLERANCE
 
 @dataclass
 class AXLProblemDef:
-    name:        str
-    description: str
-    axioms:      Set[str]
-    variables:   List[Dict]          # {name, lo, hi, tends, observed}
-    constraints: List[Dict]          # {kind: EQ/GEQ/LEQ/CONSERVE, expr, weight}
-    scopes:      List[Dict]          # {name, order, vars, constraints}
-    anchors:     List[AXLInvariant]  # verification oracles
-    observations: Dict[str,float] = field(default_factory=dict)
-
+    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)
     def variables_list(self): return [v["name"] for v in self.variables]
 
 class AXLtoPSLCompiler:
-    """Deterministic rule-based compiler. No LLM. No judgment calls."""
-
-    TEND_WEIGHT = 0.3
-
-    def compile(self, prob: AXLProblemDef) -> str:
-        lines = [f"SPACE {prob.name}"]
-
-        # Global variables
+    """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}"]
         for v in prob.variables:
-            lo, hi = v["lo"], v["hi"]
-            # Observations → zero-width bound
+            lo,hi=v["lo"],v["hi"]
             if v["name"] in prob.observations:
-                val = prob.observations[v["name"]]
-                lo = hi = val
+                val=prob.observations[v["name"]]; lo=hi=val
             lines.append(f"VAR {v['name']} {lo} {hi}")
-            # ANNOTATE for reverse mapping
             lines.append(f"ANNOTATE {v['name']} FROM_AXL {prob.name}.{v['name']}")
-
-        # Global constraints
         for c in prob.constraints:
-            wt = c.get("weight", 1.0)
-            kw = "CONSERVE" if c["kind"] == "CONSERVE" else c["kind"]
-            if kw == "CONSERVE":
-                lines.append(f"CONSERVE {c['expr']}")
-            else:
-                lines.append(f"{kw} {c['expr']} WEIGHT {wt}")
-
-        # TEND → soft constraints (global vars)
+            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 v in prob.variables:
-            tends = v.get("tends", "")
-            if tends == "MIN":
-                lines.append(f"EQ {v['name']} - {v['lo']} WEIGHT {self.TEND_WEIGHT}")
-            elif tends == "MAX":
-                lines.append(f"EQ {v['name']} - {v['hi']} WEIGHT {self.TEND_WEIGHT}")
-            elif tends.startswith("TOWARD:"):
-                val = tends.split(":")[1]
-                lines.append(f"EQ {v['name']} - {val} WEIGHT {self.TEND_WEIGHT}")
-
-        # Scopes
+            tends=v.get("tends","")
+            if tends=="MIN": lines.append(f"EQ {v['name']} - {v['lo']} WEIGHT {self.TEND_WEIGHT}")
+            elif tends=="MAX": lines.append(f"EQ {v['name']} - {v['hi']} WEIGHT {self.TEND_WEIGHT}")
+            elif tends.startswith("TOWARD:"): lines.append(f"EQ {v['name']} - {tends.split(':')[1]} WEIGHT {self.TEND_WEIGHT}")
         for sc in prob.scopes:
-            dep_str = f" DEPENDS {' '.join(sc.get('depends',[]))}" if sc.get('depends') else ""
-            lines.append(f"SCOPE {sc['name']} ORDER {sc.get('order',0)}{dep_str}")
-            sv = sc.get("vars", [])
-            if sv:
-                lines.append(f"  LINK {' '.join(sv)}")
-            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":
+            dep=f" DEPENDS {' '.join(sc.get('depends',[]))}" if sc.get('depends') else ""
+            lines.append(f"SCOPE {sc['name']} ORDER {sc.get('order',0)}{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}")
+                    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}")
+                else: lines.append(f"  {c['kind']} {c['expr']} WEIGHT {wt}")
             lines.append("END")
-
         return "\n".join(lines)
 
-AXL_COMPILER = AXLtoPSLCompiler()
+AXL_COMPILER=AXLtoPSLCompiler()
 
 # ══════════════════════════════════════════════════════════════════════
 # SECTION 5: PROBLEM & CONSTRAINT COMPILATION
@@ -373,7 +333,6 @@ class MathConstraint:
     fast_iv:Optional[Callable]=field(default=None,repr=False)
     fast_pt:Optional[Callable]=field(default=None,repr=False)
     fast_np:Optional[Callable]=field(default=None,repr=False)
-    fast_torch: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"
@@ -405,10 +364,6 @@ def compile_mc(kind,expr_str,direction,variables,weight=1.0,scope="root",branche
         mc.fast_iv=compile_iv(parsed,variables)
         mc.fast_pt=sp.lambdify([sp.Symbol(v) for v in mc.syms_used],parsed,modules="math")
         mc.fast_np=sp.lambdify([sp.Symbol(v) for v in mc.syms_used],parsed,modules="numpy")
-        if USE_GPU:
-            _tops={"sin":torch.sin,"cos":torch.cos,"exp":torch.exp,"sqrt":torch.sqrt,"log":torch.log,"Abs":torch.abs}
-            try: mc.fast_torch=sp.lambdify([sp.Symbol(v) for v in mc.syms_used],parsed,modules=[_tops,"math"])
-            except: pass
         fast_jac={}
         for v in mc.syms_used:
             try:
@@ -422,8 +377,7 @@ def compile_mc(kind,expr_str,direction,variables,weight=1.0,scope="root",branche
                 for sym in parsed.free_symbols:
                     v_str=str(sym)
                     try:
-                        sols=sp.solve(parsed,sym)
-                        pm[v_str]=[]
+                        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")})
@@ -435,8 +389,7 @@ def compile_mc(kind,expr_str,direction,variables,weight=1.0,scope="root",branche
 
 @dataclass
 class Problem:
-    pid:str; variables:List[str]
-    constraints:List[Constraint]; bounds:Dict[str,Tuple[float,float]]
+    pid:str; variables:List[str]; constraints:List[Constraint]; bounds:Dict[str,Tuple[float,float]]
     tier:str="hard"
     scope_groups:Dict[str,List[int]]=field(default_factory=dict)
     scope_vars:Dict[str,List[str]]=field(default_factory=dict)
@@ -462,9 +415,9 @@ class Problem:
                 if mc.fast_pt is None: total+=1.0; continue
                 try:
                     val=float(mc.fast_pt(*[b.get(v,0.0) for v in mc.syms_used]))
-                    if mc.kind=="equality":       total+=abs(val)*mc.weight
-                    elif mc.direction=="geq":     total+=max(0.0,-val)*mc.weight
-                    else:                         total+=max(0.0,val)*mc.weight
+                    if mc.kind=="equality":     total+=abs(val)*mc.weight
+                    elif mc.direction=="geq":   total+=max(0.0,-val)*mc.weight
+                    else:                       total+=max(0.0,val)*mc.weight
                 except: total+=1.0
         for v,(lo,hi) in self.bounds.items():
             bv=b.get(v,0.0); total+=max(0.0,lo-bv)+max(0.0,bv-hi)
@@ -515,7 +468,8 @@ class Problem:
                 for bmc in mc.branches:
                     if bmc.fast_np:
                         try:
-                            args=[b_matrix[:,vti[v]] for v in bmc.syms_used]
+                            args=[b_matrix[:,vti[v]] for v in bmc.syms_used if v in vti]
+                            if len(args)!=len(bmc.syms_used): continue
                             val=bmc.fast_np(*args)
                             if not isinstance(val,np.ndarray): val=np.full(N,float(val),dtype=np.float32)
                             bv.append(np.abs(val))
@@ -525,7 +479,8 @@ class Problem:
             else:
                 if mc.fast_np is None: total+=1.0; continue
                 try:
-                    args=[b_matrix[:,vti[v]] for v in mc.syms_used]
+                    args=[b_matrix[:,vti[v]] for v in mc.syms_used if v in vti]
+                    if len(args)!=len(mc.syms_used): total+=1.0; continue
                     val=mc.fast_np(*args)
                     if not isinstance(val,np.ndarray): val=np.full(N,float(val),dtype=np.float32)
                     if mc.kind=="equality":     total+=np.abs(val)*mc.weight
@@ -542,46 +497,123 @@ class Problem:
 # ══════════════════════════════════════════════════════════════════════
 @dataclass
 class VerifyResult:
-    gate1_ce:       float
-    gate1_pass:     bool
-    gate2_results:  Dict[str,Tuple[float,bool]]   # name → (error, pass)
-    gate2_pass:     bool
-    overall_pass:   bool
-    failed_gates:   List[str] = field(default_factory=list)
+    gate1_ce:float; gate1_pass:bool
+    gate2_results:Dict[str,Tuple[float,bool]]
+    gate2_pass:bool; overall_pass:bool
+    failed_gates:List[str]=field(default_factory=list)
 
 class VerifyLayer:
-    def run(self, binding:Dict[str,float], base_problem:Problem,
-            anchors:List[AXLInvariant]) -> VerifyResult:
-
-        # Gate 1 — structural CE against base problem
-        g1_ce = base_problem.constraint_energy(binding)
-        g1_pass = g1_ce < VERIFY_G1_THRESHOLD
-
-        # Gate 2 — invariant checks
-        g2 = {}
+    def run(self,binding:Dict[str,float],base_problem:Problem,anchors:List[AXLInvariant]) -> VerifyResult:
+        g1_ce=base_problem.constraint_energy(binding)
+        g1_pass=g1_ce<VERIFY_G1_THRESHOLD
+        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")
-                args = [binding.get(str(s), 0.0) for s in expr.free_symbols]
-                err = abs(float(func(*args)))
-                g2[inv.name] = (round(err, 6), err < inv.tolerance)
-            except Exception as e:
-                g2[inv.name] = (999.0, False)
+                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")
+                args=[binding.get(str(s),0.0) for s in expr.free_symbols]
+                err=abs(float(func(*args)))
+                g2[inv.name]=(round(err,6),err<inv.tolerance)
+            except: g2[inv.name]=(999.0,False)
+        g2_pass=all(v[1] for v in g2.values()) if g2 else True
+        failed=(["Gate1"] if not g1_pass else [])+[k for k,v in g2.items() if not v[1]]
+        return VerifyResult(gate1_ce=round(g1_ce,6),gate1_pass=g1_pass,
+                            gate2_results=g2,gate2_pass=g2_pass,
+                            overall_pass=g1_pass and g2_pass,failed_gates=failed)
+
+VERIFY_LAYER=VerifyLayer()
 
-        g2_pass = all(v[1] for v in g2.values()) if g2 else True
-        failed = (["Gate1"] if not g1_pass else []) + [k for k,v in g2.items() if not v[1]]
+# ══════════════════════════════════════════════════════════════════════
+# SECTION 7: DOMAIN STRATEGY  ← NEW
+# Wisdom layer informs HOW to search, not WHAT to search.
+# ══════════════════════════════════════════════════════════════════════
+@dataclass
+class DomainStrategy:
+    name:           str
+    hyp_weights:    Dict[str,float]   # h_type → confidence multiplier
+    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
 
-        return VerifyResult(
-            gate1_ce=round(g1_ce, 6), gate1_pass=g1_pass,
-            gate2_results=g2, gate2_pass=g2_pass,
-            overall_pass=g1_pass and g2_pass, failed_gates=failed)
+# ══════════════════════════════════════════════════════════════════════
+# SECTION 8: SHARED TYPES (before solve_by_hypothesis to avoid forward refs)
+# ══════════════════════════════════════════════════════════════════════
+@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')
 
-VERIFY_LAYER = VerifyLayer()
+@dataclass
+class HypothesisTrace:
+    hid:str; round_idx:int; domain_name:str; action:str
+    ce_before:float; ce_after:float
+    verify:Optional[VerifyResult]; survived:bool; elapsed_ms:float
+    strategy_note:str=""
+
+@dataclass
+class StructuralModel:
+    best_binding:Dict[str,float]; best_ce:float
+    tested:List[Hypothesis]=field(default_factory=list)
+    failure_patterns:Set[str]=field(default_factory=set)
+    scope_witnesses:Dict[str,Dict[str,Tuple]]=field(default_factory=dict)
+    confirmed_ranges:Dict[str,Tuple[float,float]]=field(default_factory=dict)
+    conflict_vars:Set[str]=field(default_factory=set)
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 7: ORACLES
+# SECTION 9: ORACLES
 # ══════════════════════════════════════════════════════════════════════
 @dataclass
 class L7Certificate: topology_sig:str; hub_vars:List[str]; solve_order:List[str]
@@ -644,10 +676,12 @@ class ResidualOracle:
         re=[e for e,c in sorted(de,key=lambda x:-x[1])[:5]]
         return L9Certificate(round(ce,6),rv,re)
 
-TOPOLOGY_ORACLE=TopologyOracle(); COHERENCE_ORACLE=CoherenceOracle(); RESIDUAL_ORACLE=ResidualOracle()
+TOPOLOGY_ORACLE=TopologyOracle()
+COHERENCE_ORACLE=CoherenceOracle()
+RESIDUAL_ORACLE=ResidualOracle()
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 8: CORE SOLVERS
+# SECTION 10: CORE SOLVERS
 # ══════════════════════════════════════════════════════════════════════
 def _hc4(box,constraints):
     cur=dict(box)
@@ -666,7 +700,8 @@ def _hc4(box,constraints):
             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)))):
+                    (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
@@ -758,8 +793,12 @@ 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, budget=TOTAL_BUDGET):
+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"
+
     init_b={v:max(lo,min(hi,(lo+hi)/2)) for v,(lo,hi) in problem.bounds.items()}
     tb=_global_hc4_tighten(problem)
     full_box={v:IV(tb[v][0],tb[v][1]) for v in problem.variables if v in tb}
@@ -767,26 +806,17 @@ def solve_by_hypothesis(problem, budget=TOTAL_BUDGET):
     if mprt_ce<problem.constraint_energy(init_b): init_b=mprt_b
     snap_b,snap_ce=_algebraic_snap(problem,init_b)
     if snap_ce<problem.constraint_energy(init_b): init_b=snap_b
-    best_b=dict(init_b); best_ce=problem.constraint_energy(init_b)
-
-    from dataclasses import dataclass as _dc
-    @_dc
-    class _SM:
-        best_binding:dict; best_ce:float
-        tested:list=field(default_factory=list)
-        failure_patterns:set=field(default_factory=set)
-        scope_witnesses:dict=field(default_factory=dict)
-        confirmed_ranges:dict=field(default_factory=dict)
-        conflict_vars:set=field(default_factory=set)
-
-    model=_SM(best_binding=init_b,best_ce=problem.constraint_energy(init_b))
+
+    model=StructuralModel(best_binding=dict(init_b),best_ce=problem.constraint_energy(init_b))
     active_scopes=[s for s in problem.scope_order if s!="root" and problem.scope_vars.get(s)]
+
     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(); consec=0; explore_trigger=4
+    oracle=HypothesisOracle(strategy=strategy); consec=0
     for round_idx in range(HYPOTHESIS_MAX_ROUNDS):
         if model.best_ce<SOLVE_THRESHOLD: break
         l7=TOPOLOGY_ORACLE.evaluate(problem,active_scopes)
@@ -810,12 +840,17 @@ def solve_by_hypothesis(problem, budget=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
 
-    if SOLVE_THRESHOLD<model.best_ce<2.0:
+    # Polish — strategy-directed
+    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 SOLVE_THRESHOLD<model.best_ce<1.0:
+    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)
@@ -823,36 +858,12 @@ def solve_by_hypothesis(problem, budget=TOTAL_BUDGET):
             "l7":final_l7,"l9":final_l9,"time":round(time.time()-t0,3)}
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 9: HYPOTHESIS ENGINE + TRACE LOGGING
+# SECTION 11: HYPOTHESIS ENGINE
 # ══════════════════════════════════════════════════════════════════════
-@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 HypothesisTrace:
-    hid:          str
-    round_idx:    int
-    domain_name:  str
-    action:       str
-    ce_before:    float
-    ce_after:     float
-    verify:       Optional[VerifyResult]
-    survived:     bool
-    elapsed_ms:   float
-
-@dataclass
-class StructuralModel:
-    best_binding:Dict[str,float]; best_ce:float
-    tested:List[Hypothesis]=field(default_factory=list)
-    failure_patterns:Set[str]=field(default_factory=set)
-    scope_witnesses:Dict[str,Dict[str,Tuple]]=field(default_factory=dict)
-    confirmed_ranges:Dict[str,Tuple[float,float]]=field(default_factory=dict)
-    conflict_vars:Set[str]=field(default_factory=set)
-
 class HypothesisOracle:
+    def __init__(self, strategy:Optional[DomainStrategy]=None):
+        self.strategy=strategy
+
     def generate(self,problem,model,l7,l8,l9,round_idx):
         hyps=[]
         hyps.extend(self._branch_hypotheses(problem,model,l9))
@@ -860,6 +871,11 @@ class HypothesisOracle:
         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
+        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)
 
@@ -875,9 +891,10 @@ class HypothesisOracle:
                         val=float(proj["func"](*[ref.get(s,0.0) for s in proj["syms"]]))
                         if not math.isfinite(val) or abs(val)>1e6 or not(lo<=val<=hi): continue
                         b=dict(ref); b[v]=val
-                        hyps.append(Hypothesis(hid=f"br_{hash(expr_str)%9999}_{v}_{pi}",binding=b,h_type="branch",
-                            claim=f"AlgBranch:{v}={val:.4f}",derivation=[expr_str],
-                            pinned_vars={v:val},free_vars=[u for u in problem.variables if u!=v],
+                        hyps.append(Hypothesis(hid=f"br_{hash(expr_str)%9999}_{v}_{pi}",
+                            binding=b,h_type="branch",claim=f"AlgBranch:{v}={val:.4f}",
+                            derivation=[expr_str],pinned_vars={v:val},
+                            free_vars=[u for u in problem.variables if u!=v],
                             confidence=0.85 if pi==0 else 0.70))
                     except: pass
         return hyps
@@ -890,16 +907,18 @@ class HypothesisOracle:
             if not svars: continue
             scope_mcs=[problem.compiled_constraints[i] for i in problem.scope_groups.get(sn,[])]
             if not scope_mcs: continue
-            start_box={v:IV(*tb.get(v,problem.bounds[v])) for v in svars if v in problem.bounds}
+            start_box={v:IV(*tb.get(v,problem.bounds.get(v,(-10,10)))) for v in svars if v in problem.bounds}
             cont=_hc4(start_box,scope_mcs)
             if cont:
                 for v,iv in cont.items():
                     b[v]=iv.mid()
                 chain_steps.append(sn)
         if chain_steps:
-            hyps.append(Hypothesis(hid=f"chain_{'_'.join(c[:4] for c in chain_steps)}",
-                binding=b,h_type="chain",claim=f"TopologyChain({' → '.join(chain_steps)})",
-                derivation=chain_steps,pinned_vars={v:b[v] for sn in chain_steps for v in problem.scope_vars.get(sn,[]) if v in b},
+            hyps.append(Hypothesis(
+                hid=f"chain_{'_'.join(c[:4] for c in chain_steps)}",
+                binding=b,h_type="chain",claim=f"TopoChain({' → '.join(chain_steps)})",
+                derivation=chain_steps,
+                pinned_vars={v:b[v] for sn in chain_steps for v in problem.scope_vars.get(sn,[]) if v in b},
                 free_vars=[v for v in problem.variables if not any(v in problem.scope_vars.get(sn,[]) for sn in chain_steps)],
                 confidence=0.80))
         return hyps
@@ -910,10 +929,11 @@ class HypothesisOracle:
         for v,(lo,hi) in l8.tightened_bounds.items():
             if v in problem.bounds: b[v]=(lo+hi)/2.0
         return [Hypothesis(hid=f"coh_{hash(tuple(sorted(l8.incoherent_vars)))%9999}",
-            binding=b,h_type="coherence",claim=f"CoherenceMeet({', '.join(list(l8.incoherent_vars)[:3])})",
+            binding=b,h_type="coherence",claim=f"CoherMeet({', '.join(list(l8.incoherent_vars)[:3])})",
             derivation=list(l8.incoherent_vars),
             pinned_vars={v:b[v] for v in l8.incoherent_vars if v in b},
-            free_vars=[v for v in problem.variables if v not in l8.incoherent_vars],confidence=0.70)]
+            free_vars=[v for v in problem.variables if v not in l8.incoherent_vars],
+            confidence=0.70)]
 
     def _residual_chain_hypotheses(self,problem,model,l9):
         if not l9.dominant_vars: return []
@@ -988,7 +1008,11 @@ def _test_hypothesis(problem,hyp):
     return best_b,best_ce
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 10: WISDOM LAYER + DEBATE (with trace logging)
+# 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
 # ══════════════════════════════════════════════════════════════════════
 class Axiom:
     DISCRETE="DISCRETE"; CONTINUOUS="CONTINUOUS"; METRIC="METRIC"; NETWORK="NETWORK"
@@ -996,15 +1020,15 @@ class Axiom:
     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}]
+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)
-    def __str__(self): return f"[{self.name}|{self.derivation}] {{{', '.join(sorted(self.axioms))}}}"
+    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}),
@@ -1024,19 +1048,18 @@ class WisdomOps:
     @staticmethod
     def union(d1,d2):
         merged=d1.axioms|d2.axioms
-        c=AbstractDomain(WisdomOps._fn(f"{d1.name}∪{d2.name}"),merged,"Union",(d1.confidence+d2.confidence)/2)
+        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,f"Relax",d.confidence*0.85)
+    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,f"Inject",d.confidence*0.9)
+        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
@@ -1052,60 +1075,107 @@ class WisdomOps:
         return AbstractDomain(WisdomOps._fn(f"{d.name}*"),{fm.get(ax,ax) for ax in d.axioms},"Dual",d.confidence*0.7)
 
 class PSLTranslator:
-    def compile(self,domain:AbstractDomain,variables:List[str],description:str="") -> str:
-        ax=domain.axioms; n=len(variables); lines=[f"SPACE wisdom_{domain.name.replace(' ','_').replace('∪','U')}"]
-        if Axiom.CONTINUOUS in ax and Axiom.QUADRATIC in ax:
-            for v in variables: lines.append(f"VAR {v} -2.0 2.0")
-        elif Axiom.CONTINUOUS in ax:
-            for v in variables: lines.append(f"VAR {v} -5.0 5.0")
-        elif Axiom.ORDERED in ax:
-            for v in variables: lines.append(f"VAR {v} -2.0 5.0")
-        else:
-            for v in variables: lines.append(f"VAR {v} 0.0 3.0")
-        si=0
-        if Axiom.CONSERVED in ax and n>=2:
-            lines.append(f"SCOPE conserved_{si} ORDER {si}")
-            lines.append(f"  LINK {' '.join(variables)}")
-            lines.append(f"  CONSERVE {' + '.join(variables)} - {n/2.0:.1f}")
-            lines.append("END"); si+=1
-        if Axiom.QUADRATIC in ax and Axiom.CONSERVED in ax and n>=2:
-            lines.append(f"SCOPE norm_{si} ORDER {si}")
+    """
+    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)}")
-            lines.append(f"  CONSERVE {' + '.join(f'{v}**2' for v in variables)} - {n/2.0:.1f}")
+            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.BILINEAR in ax and n>=2:
-            w=min(3,n)
-            for i in range(0,n-1,max(1,w-1)):
-                grp=variables[i:i+w]
-                if len(grp)<2: continue
-                lines.append(f"SCOPE bilinear_{si} ORDER {si}")
-                lines.append(f"  LINK {' '.join(grp)}")
-                for j in range(len(grp)-1):
-                    lines.append(f"  EQ {grp[j]}**2 + {grp[j+1]}**2 - 1.0")
-                    lines.append(f"  EQ {grp[j]}*{grp[j+1]} - 0.0")
-                lines.append("END"); si+=1
-        if Axiom.ORDERED in ax and Axiom.BILINEAR not in ax:
-            lines.append(f"SCOPE ordered_{si} ORDER {si}")
-            lines.append(f"  LINK {' '.join(variables)}")
-            for i in range(n-1): lines.append(f"  GEQ {variables[i+1]} - {variables[i]}")
+
+        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 separation_{si} ORDER {si}")
-            lines.append(f"  LINK {' '.join(variables[:min(6,n)])}")
-            for i,j in itertools.combinations(range(min(6,n)),2):
-                lines.append(f"  GEQ ({variables[i]} - {variables[j]})**2 - 0.25")
+            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.SYMMETRIC in ax and Axiom.NETWORK in ax and n>=2:
-            lines.append(f"SCOPE symmetric_{si} ORDER {si}")
-            lines.append(f"  LINK {' '.join(variables)}")
-            for i in range(0,n-1,2): lines.append(f"  EQ {variables[i]} + {variables[i+1]} - 1.0")
+
+        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
+    ce:float; solved:bool; action:str; strategy_name:str=""
     traces:List[HypothesisTrace]=field(default_factory=list)
 
 class WisdomDebate:
@@ -1125,19 +1195,20 @@ class WisdomDebate:
 
     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 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)),f"RandInject"))
+            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; variables=axl_def.variables_list()
+        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{'═'*55}\nDEBATE: {axl_def.name}\nAxioms: {problem_axioms}\n{'═'*55}")
+        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)
@@ -1145,99 +1216,110 @@ class WisdomDebate:
             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}] Domain: {winner.name} | Action: {action} | Score: {score:.1f}")
-            psl_text=self.translator.compile(winner,variables,axl_def.description)
+            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(f"       ✗ No variables compiled"); current=winner; continue
+                    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()
-                result=solve_by_hypothesis(dom_prob,budget=TOTAL_BUDGET)
+                # ── 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=ce,
-                    verify=verify,
-                    survived=verify.overall_pass,
-                    elapsed_ms=elapsed)
+                    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"       CE={ce:.5f} | G1={'✓' if verify.gate1_pass else '✗'} CE={verify.gate1_ce:.4f} | G2={'✓' if verify.gate2_pass else '✗'} | {status}")
+                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}")
+                    print(f"         [{'✓' if passed else '✗'}] {inv_name}: |err|={err:.6f}")
 
-                if ce<self.best_ce:
-                    self.best_ce=ce; self.best_binding=dict(binding); self.best_domain=winner
-                if verify.overall_pass and solved:
-                    self.history.append(DebateRound(round_idx,winner,psl_text,ce,solved,action,round_traces))
+                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:
-                print(f"       ERROR: {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,round_traces))
+                self.best_ce,self.best_ce<SOLVE_THRESHOLD,action,strategy.name,round_traces))
             current=winner
 
-        print(f"\n{'─'*55}\nRESULT: CE={self.best_ce:.5f} | Domain={self.best_domain.name if self.best_domain else '?'}")
+        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
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 11: HARDCODED AXL PROBLEMS
+# SECTION 13: HARDCODED AXL PROBLEMS (all verified feasible)
 # ══════════════════════════════════════════════════════════════════════
-@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)
-
-    def variables_list(self): return [v["name"] for v in self.variables]
+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="Four coupled variables on unit sphere with zero-sum constraint",
+        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":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),
+            AXLInvariant("x1_pinned","x1 - 0.5",1e-3),
         ],
         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-variable bilinear chain with conservation and ordering",
+        description="6-var ordered chain with bilinear products and sum conservation",
         axioms={Axiom.DISCRETE,Axiom.ORDERED,Axiom.BILINEAR,Axiom.CONSERVED,Axiom.NETWORK},
         variables=[{"name":f"t{i}","lo":0.0,"hi":3.0} for i in range(1,7)],
         constraints=[
@@ -1248,77 +1330,90 @@ AXL_PROBLEMS = [
             {"kind":"GEQ","expr":"t5 - t4","weight":1.0},
             {"kind":"GEQ","expr":"t6 - t5","weight":1.0},
         ],
-        scopes=[
-            {"name":"chain","order":0,"vars":[f"t{i}" for i in range(1,7)],
-             "constraints":[
-                {"kind":"EQ","expr":"t1*t2 - 0.5","weight":1.0},
-                {"kind":"EQ","expr":"t3*t4 - 2.0","weight":1.0},
-                {"kind":"EQ","expr":"t5*t6 - 4.5","weight":1.0},
-             ]},
-        ],
+        scopes=[{"name":"chain","order":0,"vars":[f"t{i}" for i in range(1,7)],
+                 "constraints":[
+                    {"kind":"EQ","expr":"t1*t2 - 0.5","weight":2.0},
+                    {"kind":"EQ","expr":"t3*t4 - 2.0","weight":2.0},
+                    {"kind":"EQ","expr":"t5*t6 - 4.5","weight":2.0},
+                 ]}],
         anchors=[
             AXLInvariant("conservation","t1 + t2 + t3 + t4 + t5 + t6 - 9.0",1e-3),
-            AXLInvariant("ordering_t1_t2","t1 - t2",1.0),   # t2 >= t1
-            AXLInvariant("bilinear_mid","t3*t4 - 2.0",0.1),
+            AXLInvariant("bilinear_lo","t1*t2 - 0.5",0.05),
+            AXLInvariant("bilinear_mid","t3*t4 - 2.0",0.05),
+            AXLInvariant("bilinear_hi","t5*t6 - 4.5",0.05),
         ],
     ),
+
+    # ── 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="4 variables with phase constraints — must satisfy one of two collision configurations",
+        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"},     # momentum x conserved = 0
-            {"kind":"CONSERVE","expr":"p1y + p2y"},     # momentum y conserved = 0
-        ],
-        scopes=[
-            {"name":"phase","order":0,"vars":["p1x","p2x","p1y","p2y"],
-             "constraints":[
-                {"kind":"BRANCH","name":"collision_mode","options":[
-                    "p1x**2 + p1y**2 - 1.0",   # phase A: unit circle
-                    "p1x**2 + p1y**2 - 2.0",   # phase B: larger circle
-                ]},
-                {"kind":"EQ","expr":"(p1x - p2x)**2 + (p1y - p2y)**2 - 1.0","weight":2.0},
-             ]},
+            {"kind":"CONSERVE","expr":"p1x + p2x"},   # total momentum x = 0
+            {"kind":"CONSERVE","expr":"p1y + p2y"},   # total momentum y = 0
         ],
+        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
+                    ]},
+                    # 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),
-            AXLInvariant("separation","(p1x - p2x)**2 + (p1y - p2y)**2 - 1.0",0.1),
+            # 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),
         ],
     ),
+
+    # ── 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 variables packed in metric space with minimum separation and norm bound",
+        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":"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},
-            {"kind":"CONSERVE","expr":"a + b + c"},   # centred at 0
-        ],
-        scopes=[
-            {"name":"packing","order":0,"vars":["a","b","c"],
-             "constraints":[
-                {"kind":"EQ","expr":"a**2 + b**2 + c**2 - 6.0","weight":1.5},
-             ]},
         ],
+        scopes=[{"name":"packing","order":0,"vars":["a","b","c"],
+                 "constraints":[
+                    {"kind":"EQ","expr":"a**2 + b**2 + c**2 - 6.0","weight":2.0},
+                 ]}],
         anchors=[
             AXLInvariant("centred","a + b + c",1e-3),
-            AXLInvariant("sep_ab","(a - b)**2 - 1.0",0.2),
-            AXLInvariant("sep_bc","(b - c)**2 - 1.0",0.2),
+            AXLInvariant("sep_ab","(a - b)**2 - 1.0",0.5),   # ≥ 1 (tolerance on residual)
+            AXLInvariant("sep_bc","(b - c)**2 - 1.0",0.5),
+            AXLInvariant("norm_6","a**2 + b**2 + c**2 - 6.0",0.05),
         ],
     ),
 ]
 
 def build_base_problem(axl_def:AXLProblemDef) -> Problem:
-    """Compile the AXL definition directly to a Problem for use as verification oracle."""
     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,
@@ -1327,10 +1422,10 @@ def build_base_problem(axl_def:AXLProblemDef) -> Problem:
                    scope_order=ep.scope_order,annotations=ep.annotations)
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 12: GLOBAL STATE + RUNNER
+# SECTION 14: GLOBAL STATE + RUNNER
 # ════════════════════════════════════════════════════════════════���═════
 STATE_LOCK=threading.Lock()
-RUN_LOG:List[Dict]=[]   # full run records for dashboard
+RUN_LOG:List[Dict]=[]
 DEBATE_ENGINE=WisdomDebate()
 POOL=ThreadPoolExecutor(max_workers=2)
 
@@ -1338,33 +1433,30 @@ def _run_problem(axl_def:AXLProblemDef):
     t0=time.time()
     try:
         base_prob=build_base_problem(axl_def)
-        binding, domain_ce, rounds=DEBATE_ENGINE.debate(axl_def,base_prob)
+        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)
-        
-        # FIX: Calculate actual CE against the original base problem
-        actual_base_ce = base_prob.constraint_energy(binding)
-        is_truly_solved = len(survived) > 0
-
+        actual_base_ce=base_prob.constraint_energy(binding)
         record={
             "problem":axl_def.name,
             "description":axl_def.description,
             "axioms":sorted(axl_def.axioms),
-            "ce":round(actual_base_ce, 6),        # Use REAL energy
-            "domain_ce":round(domain_ce, 6),      # Keep domain CE for reference
-            "solved":is_truly_solved,             # ONLY true if verified
+            "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,"ce":round(t.ce_after,5),
+                "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 {},
+                "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),
@@ -1375,6 +1467,7 @@ def _run_problem(axl_def:AXLProblemDef):
             RUN_LOG.append(record)
             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}")
 
 async def run_loop():
@@ -1382,7 +1475,7 @@ async def run_loop():
     while True:
         prob=random.choice(AXL_PROBLEMS)
         await loop.run_in_executor(POOL,_run_problem,prob)
-        await asyncio.sleep(0.5)
+        await asyncio.sleep(0.3)
 
 @asynccontextmanager
 async def lifespan(app):
@@ -1391,167 +1484,135 @@ async def lifespan(app):
     POOL.shutdown(wait=False)
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 13: FASTAPI + DASHBOARD
+# SECTION 15: FASTAPI + DASHBOARD
 # ══════════════════════════════════════════════════════════════════════
-app=FastAPI(title="Practicality 11.0",lifespan=lifespan)
-
-def _render_trace_table(traces:List[Dict]) -> str:
-    rows=""
-    for t in traces:
-        g1c="#4CAF50" if t["g1"] else "#EF5350"
-        g2c="#4CAF50" if t["g2"] else "#EF5350"
-        sc="#4CAF50" if t["survived"] else "#EF5350"
-        star=" ◀" if t["survived"] else ""
-        g2d="  ".join(f"{k}={v[0]:.4f}{'✓' if v[1] else '✗'}" for k,v in t.get("g2_detail",{}).items())
-        rows+=(f"<tr>"
-               f"<td style='color:#888'>{t['round']}</td>"
-               f"<td style='color:#FF9800'>{t['domain']}</td>"
-               f"<td style='color:#555;font-size:0.75em'>{t['action']}</td>"
-               f"<td style='color:#26C6DA'>{t['ce']:.5f}</td>"
-               f"<td style='color:{g1c}'>{t['g1_ce']:.4f}{'✓' if t['g1'] else '✗'}</td>"
-               f"<td style='color:{g2c}'>{'✓' if t['g2'] else '✗'} {g2d}</td>"
-               f"<td style='color:{sc};font-weight:700'>{'SURVIVED'+star if t['survived'] else 'failed'}</td>"
-               f"<td style='color:#444'>{t['ms']}ms</td>"
-               f"</tr>")
-    return rows
+app=FastAPI(title="Practicality 11.1",lifespan=lifespan)
 
 def _render_collapse(record:Dict) -> str:
-    b=record["binding"]
-    traces=record["traces"]
+    b=record["binding"]; traces=record["traces"]
     survived=[t for t in traces if t["survived"]]
-    
-    # FIX: If nothing survived, pick the best attempt to show WHY it failed
     best=min(survived,key=lambda t:t["ce"],default=None)
-    if not best and traces:
-        best=min(traces,key=lambda t:t.get("g1_ce",999.0))
-
-    obs_vars=set()
-    for axl in AXL_PROBLEMS:
-        if axl.name==record["problem"]: obs_vars=set(axl.observations.keys()); break
+    if not best and traces: best=min(traces,key=lambda t:t.get("g1_ce") or 999.0)
+    obs_vars=set(record.get("observations",{}).keys())
 
-    # FIX: Ensure it correctly marks it as UNSOLVED when CE is high or unverified
-    ce_color="#4CAF50" if record["solved"] else ("#FF9800" if record["ce"]<1.0 else "#EF5350")
-    status="✓ SOLVED + VERIFIED" if record["solved"] else ("~ PARTIAL" if record["ce"]<1.0 else "✗ UNSOLVED")
+    solved=record["solved"]
+    ce=record["ce"]
+    ce_color="#4CAF50" if solved else ("#FF9800" if ce<0.5 else "#EF5350")
+    status="✓ SOLVED + VERIFIED" if solved else ("~ PARTIAL" if ce<0.5 else "✗ UNSOLVED")
 
     binding_rows="".join(
-        f"<tr><td style='color:#888;width:80px'>{v}</td>"
+        f"<tr><td style='color:#888;width:70px'>{v}</td>"
         f"<td style='color:#26C6DA;font-weight:700'>{val:+.5f}</td>"
-        f"<td style='color:#555;font-size:0.8em'>{'[OBS]' if v in obs_vars else ''}</td></tr>"
-        for v,val in b.items()
-    )
+        f"<td style='color:#4CAF50;font-size:0.75em'>{'[OBS]' if v in obs_vars else ''}</td></tr>"
+        for v,val in b.items())
 
     inv_rows=""
     if best and best.get("g2_detail"):
         for inv,(err,ok) in best["g2_detail"].items():
             c="#4CAF50" if ok else "#EF5350"
-            inv_rows+=f"<tr><td style='color:{c}'>{'✓' if ok else '✗'}</td><td style='color:#aaa'>{inv}</td><td style='color:{c}'>{err:.6f}</td></tr>"
-
-    trail="".join(
-        f"<span style='color:{'#4CAF50' if t['survived'] else '#444'};margin-right:8px;font-size:0.8em'>"
-        f"[R{t['round']}] {t['domain'][:12]} CE={t['ce']:.4f} {'◀' if t['survived'] else ''}"
-        f"</span>"
-        for t in traces
-    )
-
-    dom_ce_str = f" | DomCE={record.get('domain_ce', 0.0):.6f}" if 'domain_ce' in record else ""
+            inv_rows+=(f"<tr><td style='color:{c}'>{'✓' if ok else '✗'}</td>"
+                       f"<td style='color:#aaa'>{inv}</td>"
+                       f"<td style='color:{c}'>{err:.6f}</td></tr>")
+
+    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 ""
+        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"<span style='color:#4CAF50;font-weight:700'>{star}</span></div>")
+
+    trail="".join(trail_span(t) for t in traces)
 
     return f"""
-<div style='border:1px solid #2a2a2a;border-radius:8px;margin-bottom:20px;overflow:hidden'>
-  <div style='background:#111;padding:10px 14px;border-bottom:1px solid #222'>
-    <span style='color:{ce_color};font-weight:700;font-size:1.1em'>{status}</span>
-    <span style='color:#555;margin-left:16px;font-size:0.85em'>{record['problem']}</span>
-    <span style='color:#333;margin-left:12px;font-size:0.8em'>BaseCE={record['ce']:.6f}{dom_ce_str}</span>
-    <span style='color:#555;margin-left:12px;font-size:0.8em'>{record['elapsed']}s</span>
+<div style='border:1px solid #222;border-radius:8px;margin-bottom:18px;overflow:hidden'>
+  <div style='background:#0e0e0e;padding:9px 14px;border-bottom:1px solid #1a1a1a;display:flex;align-items:center;gap:16px'>
+    <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;gap:0'>
-    <div style='flex:1;padding:12px 14px;border-right:1px solid #1a1a1a'>
-      <div style='color:#333;font-size:0.75em;margin-bottom:6px'>BINDING</div>
-      <table style='width:100%;border-collapse:collapse'>
-        <tr><th style='color:#333;font-size:0.75em;text-align:left'>VAR</th>
-            <th style='color:#333;font-size:0.75em;text-align:left'>VALUE</th>
-            <th></th></tr>
-        {binding_rows}
-      </table>
+  <div style='display:flex'>
+    <div style='flex:0 0 180px;padding:10px 12px;border-right:1px solid #1a1a1a'>
+      <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:1;padding:12px 14px;border-right:1px solid #1a1a1a'>
-      <div style='color:#333;font-size:0.75em;margin-bottom:6px'>INVARIANTS (Gate 2)</div>
-      <table style='width:100%;border-collapse:collapse'>
-        <tr><th style='color:#333;font-size:0.75em;text-align:left'>✓</th>
-            <th style='color:#333;font-size:0.75em;text-align:left'>NAME</th>
-            <th style='color:#333;font-size:0.75em;text-align:left'>|ERR|</th></tr>
+    <div style='flex:0 0 200px;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>"}
       </table>
     </div>
-    <div style='flex:1;padding:12px 14px'>
-      <div style='color:#333;font-size:0.75em;margin-bottom:6px'>
-        HYPOTHESIS TRAIL — {record['survived_count']} survived / {record['failed_count']} failed
-      </div>
-      <div style='line-height:2'>{trail}</div>
-      <div style='color:#555;font-size:0.8em;margin-top:8px'>
-        Best domain: <span style='color:#FF9800'>{record['best_domain']}</span>
+    <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>
       </div>
+      {trail}
     </div>
   </div>
 </div>"""
 
 @app.get("/",response_class=HTMLResponse)
 async def dashboard():
-    with STATE_LOCK: log=list(reversed(RUN_LOG[-12:]))
-
-    runs=len(RUN_LOG) if RUN_LOG else 0
-    solved=sum(1 for r in RUN_LOG if r.get("solved",False))
+    with STATE_LOCK: log=list(reversed(RUN_LOG[-10:]))
+    runs=len(RUN_LOG); solved=sum(1 for r in RUN_LOG if r.get("solved",False))
     avg_ce=round(sum(r["ce"] for r in RUN_LOG)/max(1,runs),5) if RUN_LOG else 0
 
-    collapses="".join(_render_collapse(r) for r in log) if log else \
-        "<div style='color:#222;padding:20px'>Warming up — first run starting…</div>"
-
-    # Hypothesis survival summary table across all recent runs
     all_traces=[t for r in log for t in r.get("traces",[])]
-    domain_stats=defaultdict(lambda:{"tried":0,"survived":0,"total_ce":0.0})
+    ds=defaultdict(lambda:{"tried":0,"survived":0,"total_ce":0.0,"strategy":""})
     for t in all_traces:
-        domain_stats[t["domain"]]["tried"]+=1
-        domain_stats[t["domain"]]["total_ce"]+=t["ce"]
-        if t["survived"]: domain_stats[t["domain"]]["survived"]+=1
+        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>"
         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'],4) if s['tried'] else 0}</td>"
-        f"<td style='color:#555'>{round(s['survived']/s['tried']*100,0):.0f}%</td></tr>"
-        for d,s in sorted(domain_stats.items(),key=lambda x:-x[1]["survived"])
-    ) or "<tr><td colspan='6' style='color:#222'>—</td></tr>"
+        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>"
 
-    return f"""<!DOCTYPE html><html><head><title>Practicality 11.0</title>
+    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>
 <meta http-equiv="refresh" content="4">
 <style>
   body{{background:#090909;color:#e0e0e0;font-family:monospace;padding:20px;max-width:1400px}}
-  h1{{color:#26C6DA;border-bottom:1px solid #1a1a1a;padding-bottom:6px;font-size:1.2em}}
-  h3{{color:#333;margin-top:24px;font-size:0.9em;letter-spacing:1px}}
+  h1{{color:#26C6DA;border-bottom:1px solid #1a1a1a;padding-bottom:6px;font-size:1.15em}}
+  h3{{color:#2a2a2a;margin-top:20px;font-size:0.85em;letter-spacing:2px;text-transform:uppercase}}
   table{{width:100%;border-collapse:collapse;margin-bottom:10px}}
-  th,td{{padding:5px 8px;text-align:left;border-bottom:1px solid #111;font-size:0.85em;overflow:hidden;text-overflow:ellipsis;white-space:nowrap}}
-  th{{color:#333;font-size:0.75em}}
-  .badge{{display:inline-block;padding:3px 10px;border-radius:4px;background:#111;margin:2px;font-size:0.8em}}
+  th,td{{padding:4px 8px;text-align:left;border-bottom:1px solid #0f0f0f;font-size:0.82em}}
+  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 System 11.0 — AXL/PSL Pipeline</h1>
-<div style='color:#444;font-size:0.8em;margin-bottom:14px'>
-  AXL (hardcoded) → PSL 2.0 → Solver → Gate1 (structural CE) → Gate2 (invariants) → Collapse View
+<h1>⚗ Practicality 11.1 — AXL/PSL Pipeline (fixed)</h1>
+<div style='color:#333;font-size:0.75em;margin-bottom:12px'>
+  AXL → PSL (base + soft domain hints) → Solver [strategy-directed] → Gate1 → Gate2 → Collapse
 </div>
-<div style='margin-bottom:18px'>
+<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>
 </div>
-
-<h3>DOMAIN SURVIVAL SUMMARY</h3>
+<h3>Domain Survival + Strategy</h3>
 <table>
-  <tr><th>Domain</th><th>Tried</th><th>Survived</th><th>Failed</th><th>Avg CE</th><th>Survival%</th></tr>
+  <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}
 </table>
-
-<h3>COLLAPSE VIEW — Recent Runs</h3>
+<h3>Collapse View — Recent Runs</h3>
 {collapses}
 </body></html>"""