Update app.py

app.py

@@ -1,4 +1,4 @@
-
+#!/usr/bin/env python3
 """
 PRACTICALITY SYSTEM 24.1 — STRUCTURAL SKETCH, QUANTUM ENGINE & HOMOTOPY CONTINUATION
 ══════════════════════════════════════════════════════════════════════════════════
@@ -9,11 +9,10 @@ ARCHITECTURE:
             → [WISDOM LAYER]      → Sketch-weighted rays + Masked Deduction (with Homotopy)
             → [GEMINI COLLAPSER]  → Domain-language explanation
 
-UPDATES:
-  1. Homotopy Continuation (Morphing Ray): PyTorch gradients now dynamically soften 
-     transcendental constraints and expand bounds early in the search, allowing Adam
-     to map the linear skeleton before sinking into non-convex traps.
-  2. Quantum Anchor Fix: Correctly verifies correlators to prevent infinite 0.0 CE loops.
+CRITICAL STABILITY FIXES:
+  1. Thread Crash Safety: Entire solver loop wrapped in try/finally to prevent UI lockups.
+  2. UI Responsive Layout: Unminified HTML generators and removed nested f-strings.
+  3. Expanded Axiom Logic: Restored full readability of structural heuristics.
 """
 
 import os, time, random, math, threading, warnings, json, textwrap
@@ -43,13 +42,13 @@ except ImportError:
 # ══════════════════════════════════════════════════════════════════════
 # AI CONFIGURATION
 # ══════════════════════════════════════════════════════════════════════
-DEFAULT_GEMINI_API_KEY = os.environ.get("AI_Key", "")
-GEMINI_MODEL = "gemini-3-flash-preview" # "gemma-4-26b-a4b-it"  #
+DEFAULT_GEMINI_API_KEY = os.environ.get("GEMINI_API_KEY", "")
+GEMINI_MODEL = "gemini-2.5-pro-preview-06-05"
 
 warnings.filterwarnings("ignore")
 USE_GPU = torch.cuda.is_available()
 DEVICE  = torch.device("cuda" if USE_GPU else "cpu")
-print(f"[SYSTEM 24.1] Compute: {DEVICE.type.upper()} | Homotopy Continuation Active")
+print(f"[SYSTEM 24.1] Compute: {DEVICE.type.upper()} | Homotopy Continuation + Thread Safety")
 
 # ══════════════════════════════════════════════════════════════════════
 # SECTION 1: CONSTANTS
@@ -80,18 +79,28 @@ SYMPY_TIMEOUT_SECS       = 4.0
 STATE_LOCK = threading.Lock()
 
 GLOBAL_SOLVE_STATE = {
-    "is_running": False, "phase": "IDLE", "best_ce": float('inf'), "total_fired": 0,
-    "best_ray": "—", "recent_traces": deque(maxlen=25), "high_level_logs": [],
-    "answer": "", "sketch_summary": "", "template_count": 0,
-    "template_best_ce": float('inf'), "sympy_derivation": [],
+    "is_running": False,
+    "phase": "IDLE",
+    "best_ce": float('inf'),
+    "total_fired": 0,
+    "best_ray": "—",
+    "recent_traces": deque(maxlen=25),
+    "high_level_logs": [],
+    "answer": "",
+    "sketch_summary": "",
+    "template_count": 0,
+    "template_best_ce": float('inf'),
+    "sympy_derivation": [],
 }
 
 def _update_state(**kwargs):
     with STATE_LOCK:
-        for k, v in kwargs.items(): GLOBAL_SOLVE_STATE[k] = v
+        for k, v in kwargs.items():
+            GLOBAL_SOLVE_STATE[k] = v
 
 def _add_log(line: str):
-    with STATE_LOCK: GLOBAL_SOLVE_STATE["high_level_logs"].append(line)
+    with STATE_LOCK:
+        GLOBAL_SOLVE_STATE["high_level_logs"].append(line)
 
 # ══════════════════════════════════════════════════════════════════════
 # SECTION 3: INTERVAL ARITHMETIC (HC4)
@@ -307,7 +316,8 @@ AXL_COMPILER=AXLtoPSLCompiler()
 # ══════════════════════════════════════════════════════════════════════
 @dataclass
 class Constraint:
-    kind:str; expr:str; direction:str; weight:float=1.0; scope:str="root"; branches:List[str]=field(default_factory=list)
+    kind:str; expr:str; direction:str; weight:float=1.0; scope:str="root"
+    branches:List[str]=field(default_factory=list)
 
 @dataclass
 class MathConstraint:
@@ -489,59 +499,80 @@ def build_base_problem(axl_def:AXLProblemDef) -> Problem:
 # ══════════════════════════════════════════════════════════════════════
 @dataclass
 class StructuralSketch:
-    axiom_affinities:     Dict[str, float]; solvable_by_sympy:    bool
-    exact_solutions:      List[Dict[str, float]]; sympy_derivation:     List[str]
-    n_free_dof:           int; has_conservation:     bool
-    has_bilinear:         bool; has_ordering:         bool
-    has_transcendental:   bool; dominant_type:        str; sketch_notes:         List[str]
+    axiom_affinities:     Dict[str, float]
+    solvable_by_sympy:    bool
+    exact_solutions:      List[Dict[str, float]]
+    sympy_derivation:     List[str]
+    n_free_dof:           int
+    has_conservation:     bool
+    has_bilinear:         bool
+    has_ordering:         bool
+    has_transcendental:   bool
+    dominant_type:        str
+    sketch_notes:         List[str]
 
 @dataclass
 class HypothesisTemplate:
-    template_id:  str; pinned_vars:  Dict[str,float]; free_vars:    List[str]
-    source:       str; confidence:   float; derivation:   str
+    template_id:  str
+    pinned_vars:  Dict[str,float]
+    free_vars:    List[str]
+    source:       str
+    confidence:   float
+    derivation:   str
 
 def _try_sympy_solve(problem: Problem) -> Tuple[List[Dict[str, float]], bool, List[str]]:
     has_transcendental = any(
         mc.parsed is not None and (mc.parsed.has(sp.sin) or mc.parsed.has(sp.cos) or mc.parsed.has(sp.exp) or mc.parsed.has(sp.log))
         for mc in problem.compiled_constraints)
     if has_transcendental: return [], False, []
+    
     eq_mcs = [mc for mc in problem.compiled_constraints if mc.kind == "equality" and mc.parsed is not None and mc.syms_used]
     if len(eq_mcs) < len(problem.variables): return [], False, []
+    
     syms = [sp.Symbol(v) for v in problem.variables]
     equations = [mc.parsed for mc in eq_mcs]
 
-    def _solve(): return sp.solve(equations, syms, dict=True)
+    def _solve(): 
+        return sp.solve(equations, syms, dict=True)
 
     try:
         with concurrent.futures.ThreadPoolExecutor(max_workers=1) as ex:
             future = ex.submit(_solve)
             raw = future.result(timeout=SYMPY_TIMEOUT_SECS)
     except Exception: return [], False, []
+    
     if not raw: return [], False, []
 
     derivation = ["SYSTEM HANDED TO SYMPY:"]
     for mc in eq_mcs: derivation.append(f"  {mc.expr_str} = 0")
+    
     for sol_idx, sol in enumerate(raw[:2]):
         derivation.append(f"\nSYMBOLIC SOLUTION #{sol_idx + 1}:")
         sorted_sol = sorted(sol.items(), key=lambda kv: len(kv[1].free_symbols))
         for sym, val in sorted_sol:
             simplified = sp.simplify(val); free_s = sorted(simplified.free_symbols, key=str)
             if not free_s:
-                try: num = float(simplified.evalf()); derivation.append(f"  {sym} = {simplified} = {num:.8g}  [constant root]")
-                except: derivation.append(f"  {sym} = {simplified}  [symbolic constant]")
-            else: derivation.append(f"  {sym} = {simplified}  [eliminates {sym}, depends on {', '.join(str(s) for s in free_s)}]")
+                try: 
+                    num = float(simplified.evalf())
+                    derivation.append(f"  {sym} = {simplified} = {num:.8g}  [constant root]")
+                except: 
+                    derivation.append(f"  {sym} = {simplified}  [symbolic constant]")
+            else: 
+                derivation.append(f"  {sym} = {simplified}  [eliminates {sym}, depends on {', '.join(str(s) for s in free_s)}]")
+        
         if len(sorted_sol) == 1:
             sym, val = sorted_sol[0]
             try:
                 poly = sp.Poly(equations[0], sp.Symbol(str(sym)))
-                b_str = f"[{problem.bounds.get(str(sym), ('?','?'))[0]:.4g}, {problem.bounds.get(str(sym), ('?','?'))[1]:.4g}]"
-                derivation.append(f"  Univariate polynomial: degree {poly.degree()}, roots selected by bound check {b_str}")
+                b_lo, b_hi = problem.bounds.get(str(sym), ('?', '?'))
+                derivation.append(f"  Univariate polynomial: degree {poly.degree()}, roots selected by bounds")
             except: pass
 
     valid = []
     b_mid = {v: (problem.bounds[v][0] + problem.bounds[v][1]) / 2 for v in problem.variables}
     for sol in raw:
-        binding = dict(b_mid); ok = True
+        binding = dict(b_mid)
+        ok = True
         for sym, val in sol.items():
             try:
                 num = float(val.evalf()); vn = str(sym)
@@ -553,18 +584,23 @@ def _try_sympy_solve(problem: Problem) -> Tuple[List[Dict[str, float]], bool, Li
         if ok:
             ce = problem.scalar_energy(binding)
             if ce < 1.0: valid.append((binding, ce))
+            
     valid.sort(key=lambda x: x[1])
     if valid: derivation.append(f"\nBOUND-FILTERED: {len(valid)} of {len(raw)} symbolic solutions fall within domains.")
     else: derivation.append(f"\nBOUND CHECK: all {len(raw)} symbolic solutions lie outside variable domains.")
+    
     return [v[0] for v in valid], len(valid) > 0, derivation
 
 def compute_sketch(problem: Problem) -> StructuralSketch:
-    affinities = {a: 1.0 for a in _ALL_AXIOMS_PLACEHOLDER}; notes = []
-    n_vars = len(problem.variables); n_eq = sum(1 for mc in problem.compiled_constraints if mc.kind == "equality")
+    affinities = {a: 1.0 for a in _ALL_AXIOMS_PLACEHOLDER}
+    notes = []
+    n_vars = len(problem.variables)
+    n_eq = sum(1 for mc in problem.compiled_constraints if mc.kind == "equality")
 
     has_conservation = any(mc.weight >= 5.0 for mc in problem.compiled_constraints if mc.kind == "equality")
     if has_conservation:
-        affinities["CONSERVED"] += 3.0; affinities["COMPOSITE"] += 1.5
+        affinities["CONSERVED"] += 3.0
+        affinities["COMPOSITE"] += 1.5
         notes.append("Conservation laws → CONSERVED/COMPOSITE boosted")
 
     if problem.bilinear_pairs:
@@ -572,38 +608,55 @@ def compute_sketch(problem: Problem) -> StructuralSketch:
         notes.append(f"{len(problem.bilinear_pairs)} bilinear pairs → BILINEAR boosted")
 
     if problem.monotone_targets:
-        affinities["MONOTONE_PRODUCT"] += 5.0; affinities["ORDERED"] += 2.5
+        affinities["MONOTONE_PRODUCT"] += 5.0
+        affinities["ORDERED"] += 2.5
         notes.append(f"{len(problem.monotone_targets)} monotone targets → MPR strongly boosted")
 
     if problem.ordering_pairs:
-        affinities["ORDERED"] += 2.0; affinities["DISCRETE"] += 1.0
+        affinities["ORDERED"] += 2.0
+        affinities["DISCRETE"] += 1.0
         notes.append(f"{len(problem.ordering_pairs)} ordering constraints → ORDERED boosted")
 
     if any(problem.scope_vars.values()):
-        affinities["DISCRETE"] += 2.0; affinities["LOCALITY"] += 1.0
+        affinities["DISCRETE"] += 2.0
+        affinities["LOCALITY"] += 1.0
         notes.append("Scope structure detected → DISCRETE boosted")
 
     n_proj = sum(1 for mc in problem.compiled_constraints if mc.projections)
     if n_proj > 0:
-        affinities["ATOMIC"] += 2.0 + n_proj * 0.3; affinities["IMPLICATION"] += 1.5; affinities["TRANSITIVE"] += 1.5
+        affinities["ATOMIC"] += 2.0 + n_proj * 0.3
+        affinities["IMPLICATION"] += 1.5
+        affinities["TRANSITIVE"] += 1.5
         notes.append(f"{n_proj} projectable constraints → ATOMIC/IMPLICATION boosted")
 
     has_sos = any(mc.parsed is not None and mc.parsed.is_Add and any(t.is_Pow and t.args[1] == 2 for t in mc.parsed.args) for mc in problem.compiled_constraints if mc.kind == "equality")
     if has_sos:
-        affinities["METRIC"] += 2.5; affinities["QUADRATIC"] += 2.0; affinities["CONTINUOUS"] += 1.5
+        affinities["METRIC"] += 2.5
+        affinities["QUADRATIC"] += 2.0
+        affinities["CONTINUOUS"] += 1.5
         notes.append("Sum-of-squares → METRIC/QUADRATIC/CONTINUOUS boosted")
 
     tight = sum(1 for v in problem.variables if abs(problem.bounds[v][1] - problem.bounds[v][0]) < 10)
-    if tight > n_vars // 2: affinities["PARSIMONY"] += 2.0; notes.append("Tight bounds → PARSIMONY boosted")
+    if tight > n_vars // 2: 
+        affinities["PARSIMONY"] += 2.0
+        notes.append("Tight bounds → PARSIMONY boosted")
 
-    if n_vars >= 6: affinities["HOLISM"] += 1.5; affinities["NETWORK"] += 1.5; notes.append(f"High-D ({n_vars} vars) → HOLISM/NETWORK boosted")
+    if n_vars >= 6: 
+        affinities["HOLISM"] += 1.5
+        affinities["NETWORK"] += 1.5
+        notes.append(f"High-D ({n_vars} vars) → HOLISM/NETWORK boosted")
 
     bound_groups = defaultdict(list)
     for v in problem.variables: bound_groups[problem.bounds[v]].append(v)
-    if any(len(g) >= 2 for g in bound_groups.values()): affinities["SYMMETRIC"] += 1.5; notes.append("Symmetric bounds → SYMMETRIC boosted")
+    if any(len(g) >= 2 for g in bound_groups.values()): 
+        affinities["SYMMETRIC"] += 1.5
+        notes.append("Symmetric bounds → SYMMETRIC boosted")
 
     has_transcendental = any(mc.parsed is not None and (mc.parsed.has(sp.sin) or mc.parsed.has(sp.cos) or mc.parsed.has(sp.exp)) for mc in problem.compiled_constraints)
-    if has_transcendental: affinities["CONTINUOUS"] += 2.0; affinities["EQUILIBRIUM"] += 1.5; notes.append("Transcendental constraints → CONTINUOUS/EQUILIBRIUM boosted")
+    if has_transcendental: 
+        affinities["CONTINUOUS"] += 2.0
+        affinities["EQUILIBRIUM"] += 1.5
+        notes.append("Transcendental constraints → CONTINUOUS/EQUILIBRIUM boosted")
 
     max_deg = 1
     for mc in problem.compiled_constraints:
@@ -622,19 +675,32 @@ def compute_sketch(problem: Problem) -> StructuralSketch:
     n_obs = sum(1 for v in problem.variables if problem.bounds[v][0] == problem.bounds[v][1])
     n_free_dof = max(0, n_vars - n_obs - n_eq)
 
-    exact_solutions = []; solvable = False; sympy_derivation = []
+    exact_solutions = []
+    solvable = False
+    sympy_derivation = []
     if n_vars <= SYMPY_MAX_VARS and dom_type in ("linear", "quadratic") and not has_transcendental:
         exact_solutions, solvable, sympy_derivation = _try_sympy_solve(problem)
-        if solvable: notes.append(f"✓ SymPy found {len(exact_solutions)} exact solution(s) via {len(sympy_derivation)} steps")
-        else: notes.append("SymPy attempted (no closed form) — proceeding to ray search")
-
-    return StructuralSketch(axiom_affinities=affinities, solvable_by_sympy=solvable, exact_solutions=exact_solutions, sympy_derivation=sympy_derivation, n_free_dof=n_free_dof, has_conservation=has_conservation, has_bilinear=bool(problem.bilinear_pairs), has_ordering=bool(problem.ordering_pairs), has_transcendental=has_transcendental, dominant_type=dom_type, sketch_notes=notes)
+        if solvable: 
+            notes.append(f"✓ SymPy found {len(exact_solutions)} exact solution(s) via {len(sympy_derivation)} steps")
+        else: 
+            notes.append("SymPy attempted (no closed form) — proceeding to ray search")
+
+    return StructuralSketch(
+        axiom_affinities=affinities, solvable_by_sympy=solvable, 
+        exact_solutions=exact_solutions, sympy_derivation=sympy_derivation, 
+        n_free_dof=n_free_dof, has_conservation=has_conservation, 
+        has_bilinear=bool(problem.bilinear_pairs), has_ordering=bool(problem.ordering_pairs), 
+        has_transcendental=has_transcendental, dominant_type=dom_type, sketch_notes=notes)
 
 def generate_templates(problem: Problem, sketch: StructuralSketch) -> List[HypothesisTemplate]:
-    templates = []; b_mid = {v: (problem.bounds[v][0] + problem.bounds[v][1]) / 2 for v in problem.variables}
+    templates = []
+    b_mid = {v: (problem.bounds[v][0] + problem.bounds[v][1]) / 2 for v in problem.variables}
 
     for i, sol in enumerate(sketch.exact_solutions):
-        templates.append(HypothesisTemplate(template_id=f"sympy_{i}", pinned_vars=sol, free_vars=[v for v in problem.variables if v not in sol], source="sympy_exact", confidence=0.99, derivation=f"SymPy exact solution #{i+1}"))
+        templates.append(HypothesisTemplate(
+            template_id=f"sympy_{i}", pinned_vars=sol, 
+            free_vars=[v for v in problem.variables if v not in sol], 
+            source="sympy_exact", confidence=0.99, derivation=f"SymPy exact solution #{i+1}"))
 
     for mc in problem.compiled_constraints:
         if mc.kind != "equality" or mc.weight < 5.0 or not mc.projections: continue
@@ -644,27 +710,40 @@ def generate_templates(problem: Problem, sketch: StructuralSketch) -> List[Hypot
                 try:
                     val = float(proj["func"](*[b_mid.get(s, 0.0) for s in proj["syms"]]))
                     if math.isfinite(val) and lo <= val <= hi:
-                        templates.append(HypothesisTemplate(template_id=f"cons_{v}_{hash(mc.expr_str)%9999}", pinned_vars={v: val}, free_vars=[u for u in problem.variables if u != v], source="conservation", confidence=0.75, derivation=f"Conservation {mc.expr_str} → {v}={val:.4f}"))
+                        templates.append(HypothesisTemplate(
+                            template_id=f"cons_{v}_{hash(mc.expr_str)%9999}", pinned_vars={v: val}, 
+                            free_vars=[u for u in problem.variables if u != v], source="conservation", 
+                            confidence=0.75, derivation=f"Conservation {mc.expr_str} → {v}={val:.4f}"))
                 except: pass
 
     tb = _global_hc4_tighten_bounds(problem)
     for v_small, v_large, k in problem.monotone_targets:
-        lo_s, hi_s = problem.bounds.get(v_small, (-1e9, 1e9)); lo_l, hi_l = problem.bounds.get(v_large, (-1e9, 1e9))
+        lo_s, hi_s = problem.bounds.get(v_small, (-1e9, 1e9))
+        lo_l, hi_l = problem.bounds.get(v_large, (-1e9, 1e9))
         for ratio in [0.1, 0.25, 0.5, 0.707, 0.9]:
             vs_sq = k * ratio
             if vs_sq <= 0: continue
             vs = math.sqrt(vs_sq); vl = k / vs
             if not (lo_s <= vs <= hi_s and lo_l <= vl <= hi_l and vs <= vl): continue
-            nb = dict(b_mid); nb[v_small] = vs; nb[v_large] = vl
+            
+            nb = dict(b_mid)
+            nb[v_small] = vs
+            nb[v_large] = vl
             box = {u: IV(*tb.get(u, problem.bounds.get(u, (-10, 10)))) for u in problem.variables}
-            box[v_small] = IV(vs - 1e-6, vs + 1e-6); box[v_large] = IV(vl - 1e-6, vl + 1e-6)
+            box[v_small] = IV(vs - 1e-6, vs + 1e-6)
+            box[v_large] = IV(vl - 1e-6, vl + 1e-6)
             cont = _hc4(box, problem.compiled_constraints)
+            
             pinned = {v_small: vs, v_large: vl}
             if cont:
                 for u, iv in cont.items():
                     if u in problem.bounds: nb[u] = iv.mid()
                 pinned = {u: nb[u] for u in problem.variables if cont[u].width() < 1e-2}
-            templates.append(HypothesisTemplate(template_id=f"mpr_{v_small}_{v_large}_r{int(ratio*100)}", pinned_vars=pinned, free_vars=[u for u in problem.variables if u not in pinned], source="monotone_prod", confidence=0.88, derivation=f"Monotone {v_small}={vs:.4f}≤{v_large}={vl:.4f}"))
+                
+            templates.append(HypothesisTemplate(
+                template_id=f"mpr_{v_small}_{v_large}_r{int(ratio*100)}", pinned_vars=pinned, 
+                free_vars=[u for u in problem.variables if u not in pinned], source="monotone_prod", 
+                confidence=0.88, derivation=f"Monotone {v_small}={vs:.4f}≤{v_large}={vl:.4f}"))
 
     for mc in problem.compiled_constraints:
         if mc.kind != "equality" or not mc.projections: continue
@@ -674,29 +753,42 @@ def generate_templates(problem: Problem, sketch: StructuralSketch) -> List[Hypot
                 try:
                     val = float(proj["func"](*[b_mid.get(s, 0.0) for s in proj["syms"]]))
                     if math.isfinite(val) and lo <= val <= hi:
-                        templates.append(HypothesisTemplate(template_id=f"proj_{v}_{hash(mc.expr_str)%9999}", pinned_vars={v: val}, free_vars=[u for u in problem.variables if u != v], source="projection", confidence=0.72, derivation=f"Root of {mc.expr_str[:30]} → {v}={val:.4f}"))
+                        templates.append(HypothesisTemplate(
+                            template_id=f"proj_{v}_{hash(mc.expr_str)%9999}", pinned_vars={v: val}, 
+                            free_vars=[u for u in problem.variables if u != v], source="projection", 
+                            confidence=0.72, derivation=f"Root of {mc.expr_str[:30]} → {v}={val:.4f}"))
                 except: pass
 
     bound_groups = defaultdict(list)
     for v in problem.variables: bound_groups[problem.bounds[v]].append(v)
     for bnd, grp in bound_groups.items():
         if len(grp) < 2: continue
-        avg = sum(b_mid[v] for v in grp) / len(grp); lo, hi = bnd
+        avg = sum(b_mid[v] for v in grp) / len(grp)
+        lo, hi = bnd
         if lo <= avg <= hi:
             pinned = {v: avg for v in grp}
-            templates.append(HypothesisTemplate(template_id=f"sym_avg_{'_'.join(grp[:3])}", pinned_vars=pinned, free_vars=[u for u in problem.variables if u not in pinned], source="symmetry", confidence=0.55, derivation=f"Symmetry orbit: {grp} averaged to {avg:.4f}"))
+            templates.append(HypothesisTemplate(
+                template_id=f"sym_avg_{'_'.join(grp[:3])}", pinned_vars=pinned, 
+                free_vars=[u for u in problem.variables if u not in pinned], source="symmetry", 
+                confidence=0.55, derivation=f"Symmetry orbit: {grp} averaged to {avg:.4f}"))
 
     seen = set(); unique = []
     for t in sorted(templates, key=lambda t: -t.confidence):
         key = str(sorted(t.pinned_vars.items()))
-        if key not in seen: seen.add(key); unique.append(t)
+        if key not in seen: 
+            seen.add(key)
+            unique.append(t)
+            
     return unique[:TEMPLATE_BATCH_SIZE]
 
 def templates_to_hypotheses(templates, problem, init_binding):
     hyps = []
     for t in templates:
-        binding = dict(init_binding); binding.update(t.pinned_vars)
-        hyps.append(Hypothesis(hid=t.template_id, binding=binding, h_type=t.source, claim=t.derivation, derivation=[t.source], pinned_vars=t.pinned_vars, free_vars=t.free_vars, confidence=t.confidence))
+        binding = dict(init_binding)
+        binding.update(t.pinned_vars)
+        hyps.append(Hypothesis(
+            hid=t.template_id, binding=binding, h_type=t.source, claim=t.derivation, 
+            derivation=[t.source], pinned_vars=t.pinned_vars, free_vars=t.free_vars, confidence=t.confidence))
     return hyps
 
 _ALL_AXIOMS_PLACEHOLDER: List[str] = []
@@ -706,18 +798,36 @@ _ALL_AXIOMS_PLACEHOLDER: List[str] = []
 # ══════════════════════════════════════════════════════════════════════
 @dataclass
 class L9Certificate:
-    residual_ce: float; dominant_vars: List[str]; dominant_exprs: List[str]; tension_class: str = "unknown"
+    residual_ce: float
+    dominant_vars: List[str]
+    dominant_exprs: List[str]
+    tension_class: str = "unknown"
 
 def _batched_deduce_and_evaluate(problem: Problem, hyps: List['Hypothesis']) -> List[Tuple[Dict, float, List[str], str]]:
     if not hyps: return []
-    B = len(hyps); V = len(problem.variables)
-    x_data = []; mask_data = []; target_data = []
+    B = len(hyps)
+    V = len(problem.variables)
+    
+    x_data = []
+    mask_data = []
+    target_data = []
+    
     for hyp in hyps:
         xr, mr, tr = [], [], []
         for v in problem.variables:
-            if v in hyp.pinned_vars: val = hyp.pinned_vars[v]; xr.append(val); mr.append(0.0); tr.append(val)
-            else: val = hyp.binding.get(v, (problem.bounds[v][0] + problem.bounds[v][1]) / 2); xr.append(val); mr.append(1.0); tr.append(0.0)
-        x_data.append(xr); mask_data.append(mr); target_data.append(tr)
+            if v in hyp.pinned_vars: 
+                val = hyp.pinned_vars[v]
+                xr.append(val)
+                mr.append(0.0)
+                tr.append(val)
+            else: 
+                val = hyp.binding.get(v, (problem.bounds[v][0] + problem.bounds[v][1]) / 2)
+                xr.append(val)
+                mr.append(1.0)
+                tr.append(0.0)
+        x_data.append(xr)
+        mask_data.append(mr)
+        target_data.append(tr)
 
     X = torch.tensor(x_data, device=DEVICE, dtype=torch.float32, requires_grad=True)
     mask = torch.tensor(mask_data, device=DEVICE, dtype=torch.float32)
@@ -731,14 +841,18 @@ def _batched_deduce_and_evaluate(problem: Problem, hyps: List['Hypothesis']) ->
         step_ratio = min(1.0, step / (DEDUCE_ADAM_STEPS * 0.8))
         ce = problem.tensor_energy(X, step_ratio)
         
-        if isinstance(ce, torch.Tensor) and (ce < SOLVE_THRESHOLD).all() and step_ratio == 1.0: break
-        loss = ce.sum(); loss.backward()
+        if isinstance(ce, torch.Tensor) and (ce < SOLVE_THRESHOLD).all() and step_ratio == 1.0: 
+            break
+            
+        loss = ce.sum()
+        loss.backward()
         
         with torch.no_grad():
             X.grad.clamp_(-10.0, 10.0)
             X.grad *= mask
             optimizer.step()
             X.data = torch.where(mask == 0.0, target, X.data)
+            
             for j, v in enumerate(problem.variables):
                 lo, hi = problem.bounds[v]
                 margin = (hi - lo) * 0.1 * (1.0 - step_ratio) # Exploratory bounds fade to 0
@@ -750,26 +864,39 @@ def _batched_deduce_and_evaluate(problem: Problem, hyps: List['Hypothesis']) ->
 
     ce_vals = final_ce.detach().cpu().numpy()
     X_vals = X.detach().cpu().numpy()
-    grads_abs = X.grad.abs(); _, topk_idx = torch.topk(grads_abs, k=min(3, V), dim=1)
-    topk_idx_np = topk_idx.cpu().numpy(); grads_np = grads_abs.cpu().numpy()
+    grads_abs = X.grad.abs()
+    _, topk_idx = torch.topk(grads_abs, k=min(3, V), dim=1)
+    
+    topk_idx_np = topk_idx.cpu().numpy()
+    grads_np = grads_abs.cpu().numpy()
 
     results = []
     for i in range(B):
         final_b = {problem.variables[j]: float(X_vals[i, j]) for j in range(V)}
         dom_vars = [problem.variables[idx] for idx in topk_idx_np[i] if float(grads_np[i, idx]) > 1e-4]
-        n_dom = len(dom_vars); tension_class = ("isolated" if n_dom <= 1 else "relational" if n_dom == 2 else "systemic")
+        n_dom = len(dom_vars)
+        tension_class = ("isolated" if n_dom <= 1 else "relational" if n_dom == 2 else "systemic")
         results.append((final_b, float(ce_vals[i]), dom_vars, tension_class))
+        
     return results
 
 def _mprt_sample(problem, work_box, N):
-    var_list = problem.variables; V = len(var_list)
+    var_list = problem.variables
+    V = len(var_list)
+    
     lo_t = torch.tensor([max(problem.bounds.get(v, (-10.0, 10.0))[0], work_box[v].lo if v in work_box else problem.bounds.get(v, (-10, 10))[0]) for v in var_list], device=DEVICE, dtype=torch.float32)
     hi_t = torch.tensor([min(problem.bounds.get(v, (-10.0, 10.0))[1], work_box[v].hi if v in work_box else problem.bounds.get(v, (-10, 10))[1]) for v in var_list], device=DEVICE, dtype=torch.float32)
+    
     for i in range(V):
-        if lo_t[i] >= hi_t[i]: m = (lo_t[i] + hi_t[i]) / 2; lo_t[i] = m - 1e-6; hi_t[i] = m + 1e-6
+        if lo_t[i] >= hi_t[i]: 
+            m = (lo_t[i] + hi_t[i]) / 2
+            lo_t[i] = m - 1e-6
+            hi_t[i] = m + 1e-6
+            
     X = lo_t.unsqueeze(0) + (hi_t - lo_t).unsqueeze(0) * torch.rand((N, V), device=DEVICE)
     ce_batch = problem.tensor_energy(X, 1.0)
     best_idx = torch.argmin(ce_batch).item()
+    
     return {v: float(X[best_idx, i].item()) for i, v in enumerate(var_list)}, ce_batch[best_idx].item()
 
 # ══════════════════════════════════════════════════════════════════════
@@ -788,7 +915,8 @@ class Axiom:
     COMPOSITE="COMPOSITE"; HOLISM="HOLISM"; PARSIMONY="PARSIMONY"; DUALITY="DUALITY"
 
 ALL_AXIOMS = [getattr(Axiom, a) for a in dir(Axiom) if not a.startswith("__")]
-AXIOM_ABBR = {a: a[:3] for a in ALL_AXIOMS}; AXIOM_ABBR[Axiom.MONOTONE_PRODUCT] = "MPR"
+AXIOM_ABBR = {a: a[:3] for a in ALL_AXIOMS}
+AXIOM_ABBR[Axiom.MONOTONE_PRODUCT] = "MPR"
 _ALL_AXIOMS_PLACEHOLDER.extend(ALL_AXIOMS)
 
 ADJACENT_CONTRADICTIONS = [
@@ -813,41 +941,72 @@ RAY_TYPES = ["seed", "branch", "tension", "scout", "recombine", "invert", "targe
 
 @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')
+    hid: str
+    binding: Dict[str, float]
+    h_type: str
+    claim: str
+    derivation: List[str]
+    pinned_vars: Dict[str, float]
+    free_vars: List[str]
+    confidence: float
+    ce: float = float('inf')
 
 @dataclass
 class Baton:
-    binding: Dict[str, float]; ce: float
-    ray_id: str = ""; depth: int = 0; l9: Optional[L9Certificate] = None
+    binding: Dict[str, float]
+    ce: float
+    ray_id: str = ""
+    depth: int = 0
+    l9: Optional[L9Certificate] = None
 
 @dataclass
 class AxiomRay:
-    sequence: List[str]; ray_id: str; ray_type: str = "seed"
-    depth: int = 0; parent_id: Optional[str] = None
-    baton: Optional[Baton] = None; ce_prior: float = float('inf')
+    sequence: List[str]
+    ray_id: str
+    ray_type: str = "seed"
+    depth: int = 0
+    parent_id: Optional[str] = None
+    baton: Optional[Baton] = None
+    ce_prior: float = float('inf')
+    
     @property
-    def name(self) -> str: return "→".join(AXIOM_ABBR.get(a, a[:3]) for a in self.sequence)
+    def name(self) -> str: 
+        return "→".join(AXIOM_ABBR.get(a, a[:3]) for a in self.sequence)
+        
     def extend(self, axiom: str, rtype: str, new_prior: float = float('inf')) -> Optional['AxiomRay']:
         new_seq = self.sequence + [axiom]
         if sequence_valid(new_seq):
-            return AxiomRay(sequence=new_seq, ray_id=f"{self.ray_id}+{AXIOM_ABBR.get(axiom, '?')}",
-                            ray_type=rtype, depth=self.depth + 1, parent_id=self.ray_id, ce_prior=new_prior)
+            return AxiomRay(
+                sequence=new_seq, 
+                ray_id=f"{self.ray_id}+{AXIOM_ABBR.get(axiom, '?')}",
+                ray_type=rtype, 
+                depth=self.depth + 1, 
+                parent_id=self.ray_id, 
+                ce_prior=new_prior
+            )
         return None
 
 @dataclass
 class HypothesisTrace:
-    hid: str; round_idx: int; ray_name: str; ray_type: str
-    ce_before: float; ce_after: float; survived: bool; elapsed_ms: float
-    g1_pass: bool = False; g2_pass: bool = False
+    hid: str
+    round_idx: int
+    ray_name: str
+    ray_type: str
+    ce_before: float
+    ce_after: float
+    survived: bool
+    elapsed_ms: float
+    g1_pass: bool = False
+    g2_pass: bool = False
     binding: Dict[str, float] = field(default_factory=dict)
     invariant_results: Dict[str, Tuple[float, bool]] = field(default_factory=dict)
-    tension_class: str = "unknown"; depth: int = 0
+    tension_class: str = "unknown"
+    depth: int = 0
 
 @dataclass
 class StructuralModel:
-    best_binding: Dict[str, float]; best_ce: float
+    best_binding: Dict[str, float]
+    best_ce: float
     best_ray: str = "—"
     failure_patterns: Set[str] = field(default_factory=set)
     resonant_pairs: List[Tuple[str, str]] = field(default_factory=list)
@@ -859,11 +1018,15 @@ def _make_hyp(hid, binding, h_type, claim, derivation, pinned, free, conf):
     return Hypothesis(hid=hid, binding=binding, h_type=h_type, claim=claim,
                       derivation=derivation, pinned_vars=pinned, free_vars=free, confidence=conf)
 
-def _hyp_continuous(p, bt, a, m): return [_make_hyp("cnt", bt.binding, "continuous", "Manifold", [], {}, p.variables, 0.45)]
+def _hyp_continuous(p, bt, a, m): 
+    return [_make_hyp("cnt", bt.binding, "continuous", "Manifold", [], {}, p.variables, 0.45)]
+
 def _hyp_discrete(p, bt, a, m):
-    b = dict(bt.binding); pinned = {}
+    b = dict(bt.binding)
+    pinned = {}
     for sn in p.scope_order:
-        svars = p.scope_vars.get(sn, []); smcs = [p.compiled_constraints[i] for i in p.scope_groups.get(sn, [])]
+        svars = p.scope_vars.get(sn, [])
+        smcs = [p.compiled_constraints[i] for i in p.scope_groups.get(sn, [])]
         if svars and smcs:
             box = {v: IV(b.get(v, 0) - max(0.05 * (p.bounds[v][1] - p.bounds[v][0]), 1e-4),
                          b.get(v, 0) + max(0.05 * (p.bounds[v][1] - p.bounds[v][0]), 1e-4)) for v in svars if v in p.bounds}
@@ -871,82 +1034,114 @@ def _hyp_discrete(p, bt, a, m):
             if cont:
                 for v, iv in cont.items():
                     b[v] = iv.mid()
-                    if iv.width() < 1e-2: pinned[v] = b[v]
+                    if iv.width() < 1e-2: 
+                        pinned[v] = b[v]
     return [_make_hyp("dis", b, "discrete", "TopoScope", [], pinned, p.variables, 0.80)]
 
 def _hyp_quadratic(p, bt, a, m):
-    hyps = []; b = dict(bt.binding)
+    hyps = []
+    b = dict(bt.binding)
     if bt.l9 and bt.l9.dominant_vars:
-        for v in bt.l9.dominant_vars[:2]: hyps.append(_make_hyp(f"qua_{v}", b, "quadratic", f"Root({v})", [], {v: b[v]}, p.variables, 0.70))
+        for v in bt.l9.dominant_vars[:2]: 
+            hyps.append(_make_hyp(f"qua_{v}", b, "quadratic", f"Root({v})", [], {v: b[v]}, p.variables, 0.70))
     return hyps
 
 def _hyp_bilinear(p, bt, a, m):
-    hyps = []; b = dict(bt.binding)
+    hyps = []
+    b = dict(bt.binding)
     for vi, vj in p.bilinear_pairs:
-        lo_i, hi_i = p.bounds.get(vi, (0, 10)); lo_j, hi_j = p.bounds.get(vj, (0, 10))
+        lo_i, hi_i = p.bounds.get(vi, (0, 10))
+        lo_j, hi_j = p.bounds.get(vj, (0, 10))
         product = abs(b.get(vi, 1) * b.get(vj, 1))
+        
         if product <= 0: continue
         gm = math.sqrt(product)
+        
         if lo_i <= gm <= hi_i and lo_j <= gm <= hi_j:
-            nb = dict(b); nb[vi] = nb[vj] = gm
+            nb = dict(b)
+            nb[vi] = nb[vj] = gm
             hyps.append(_make_hyp(f"bil_eq_{vi}_{vj}", nb, "bilinear", f"GeoMean({vi}={vj}={gm:.3f})", ["bilinear"], {vi: gm, vj: gm}, [v for v in p.variables if v not in [vi, vj]], 0.70))
+            
         for ratio in [0.4, 0.7071, 0.9]:
-            vs = gm * ratio; vl = product / (vs + 1e-9)
+            vs = gm * ratio
+            vl = product / (vs + 1e-9)
             if lo_i <= vs <= hi_i and lo_j <= vl <= hi_j and vs < vl:
-                nb2 = dict(b); nb2[vi] = vs; nb2[vj] = vl
+                nb2 = dict(b)
+                nb2[vi] = vs
+                nb2[vj] = vl
                 hyps.append(_make_hyp(f"bil_asc_{int(ratio*100)}_{vi}_{vj}", nb2, "bilinear", f"BilAsc({vi}={vs:.3f}<{vj}={vl:.3f})", ["bilinear"], {vi: vs, vj: vl}, [v for v in p.variables if v not in [vi, vj]], 0.75))
     return hyps
 
 def _hyp_monotone_product(p, bt, a, m):
-    hyps = []; b = dict(bt.binding)
+    hyps = []
+    b = dict(bt.binding)
     if not p.monotone_targets: return hyps
     tb = _global_hc4_tighten_bounds(p)
+    
     for v_small, v_large, k in p.monotone_targets:
-        lo_s, hi_s = p.bounds.get(v_small, (-1e9, 1e9)); lo_l, hi_l = p.bounds.get(v_large, (-1e9, 1e9))
+        lo_s, hi_s = p.bounds.get(v_small, (-1e9, 1e9))
+        lo_l, hi_l = p.bounds.get(v_large, (-1e9, 1e9))
+        
         for ratio in [0.25, 0.5, 0.707, 0.9]:
             vs_sq = k * ratio
             if vs_sq <= 0: continue
-            vs = math.sqrt(vs_sq); vl = k / vs
+            vs = math.sqrt(vs_sq)
+            vl = k / vs
             if not (lo_s <= vs <= hi_s and lo_l <= vl <= hi_l and vs <= vl): continue
-            nb = dict(b); nb[v_small] = vs; nb[v_large] = vl
+            
+            nb = dict(b)
+            nb[v_small] = vs
+            nb[v_large] = vl
             box = {u: IV(*tb.get(u, p.bounds.get(u, (-10, 10)))) for u in p.variables}
-            box[v_small] = IV(vs - 1e-6, vs + 1e-6); box[v_large] = IV(vl - 1e-6, vl + 1e-6)
+            box[v_small] = IV(vs - 1e-6, vs + 1e-6)
+            box[v_large] = IV(vl - 1e-6, vl + 1e-6)
             cont = _hc4(box, p.compiled_constraints)
+            
             pinned = {v_small: vs, v_large: vl}
             if cont:
                 for u, iv in cont.items():
                     if u in p.bounds: nb[u] = iv.mid()
                 pinned = {u: nb[u] for u in p.variables if cont[u].width() < 1e-2}
+                
             hyps.append(_make_hyp(f"mpr_{v_small}_{v_large}_r{int(ratio*100)}", nb, "monotone_product", f"MonoProd({v_small}={vs:.4f}≤{v_large}={vl:.4f})", ["ordered", "hc4"], pinned, [u for u in p.variables if u not in pinned], 0.88))
     return hyps
 
 def _hyp_metric(p, bt, a, m):
-    hyps = []; b = dict(bt.binding)
+    hyps = []
+    b = dict(bt.binding)
     for mc in p.compiled_constraints:
         if mc.kind != "equality" or not mc.parsed: continue
         if not mc.parsed.is_Add: continue
+        
         sq_terms = [t for t in mc.parsed.args if t.is_Pow and t.args[1] == 2]
         if len(sq_terms) < 1: continue
         vars_in = [str(s) for s in mc.parsed.free_symbols if str(s) in p.variables]
         if not vars_in: continue
+        
         const_terms = [float(t) for t in mc.parsed.args if t.is_Number]
         if not const_terms: continue
+        
         target = -const_terms[0]
         if target <= 0: continue
+        
         curr_val = sum(b.get(v, 0)**2 for v in vars_in)
         if curr_val < 1e-8: continue
+        
         scale = math.sqrt(target / curr_val)
         nb = dict(b)
         for v in vars_in:
             lo, hi = p.bounds.get(v, (-10, 10))
             nb[v] = max(lo, min(hi, b.get(v, 0) * scale))
+            
         hyps.append(_make_hyp(f"met_{hash(mc.expr_str)%9999}", nb, "metric", f"RadialProject(scale={scale:.4f},dim={len(vars_in)})", ["metric", mc.expr_str], {}, list(p.variables), 0.75))
     return hyps
 
 def _hyp_symmetric(p, bt, a, m):
-    hyps = []; b = dict(bt.binding)
+    hyps = []
+    b = dict(bt.binding)
     groups_to_check = list(p.scope_vars.values()) if p.scope_vars else [p.variables]
-    if not any(p.scope_vars.values()): groups_to_check = [p.variables]
+    if not any(p.scope_vars.values()): 
+        groups_to_check = [p.variables]
 
     seen_pairs = set()
     for grp in groups_to_check:
@@ -957,14 +1152,21 @@ def _hyp_symmetric(p, bt, a, m):
                 vi, vj = vl[i], vl[j]
                 if (vi, vj) in seen_pairs: continue
                 seen_pairs.add((vi, vj))
-                lo_i, hi_i = p.bounds.get(vi, (-1e9, 1e9)); lo_j, hi_j = p.bounds.get(vj, (-1e9, 1e9))
+                
+                lo_i, hi_i = p.bounds.get(vi, (-1e9, 1e9))
+                lo_j, hi_j = p.bounds.get(vj, (-1e9, 1e9))
                 bvi, bvj = b.get(vi, 0), b.get(vj, 0)
+                
                 if lo_i <= bvj <= hi_i and lo_j <= bvi <= hi_j:
-                    nb = dict(b); nb[vi], nb[vj] = bvj, bvi
+                    nb = dict(b)
+                    nb[vi], nb[vj] = bvj, bvi
                     hyps.append(_make_hyp(f"sym_{vi}_{vj}", nb, "symmetric", f"Swap({vi}↔{vj})", ["symmetric"], {vi: nb[vi], vj: nb[vj]}, [v for v in p.variables if v not in [vi, vj]], 0.60))
+                
                 avg = (bvi + bvj) / 2
                 if lo_i <= avg <= hi_i and lo_j <= avg <= hi_j:
-                    nb2 = dict(b); nb2[vi] = avg; nb2[vj] = avg
+                    nb2 = dict(b)
+                    nb2[vi] = avg
+                    nb2[vj] = avg
                     hyps.append(_make_hyp(f"sym_avg_{vi}_{vj}", nb2, "symmetric", f"Average({vi}={vj}={avg:.4f})", ["symmetric"], {vi: avg, vj: avg}, [v for v in p.variables if v not in [vi, vj]], 0.55))
     return hyps[:10]
 
@@ -975,24 +1177,29 @@ def _hyp_conserved(p, bt, a, m): return [_make_hyp("csv", bt.binding, "conserved
 def _hyp_mutable(p, bt, a, m):
     b = dict(bt.binding)
     if bt.l9 and bt.l9.dominant_vars:
-        v = bt.l9.dominant_vars[0]; lo, hi = p.bounds.get(v, (-10, 10))
+        v = bt.l9.dominant_vars[0]
+        lo, hi = p.bounds.get(v, (-10, 10))
         b[v] = max(lo, min(hi, b.get(v, 0) + random.gauss(0, (hi - lo) * 0.05)))
     return [_make_hyp("mut", b, "mutable", "Perturb", [], {}, p.variables, 0.40)]
 def _hyp_network(p, bt, a, m): return [_make_hyp("net", bt.binding, "network", "HubProp", [], {}, p.variables, 0.65)]
 def _hyp_equilibrium(p, bt, a, m): return [_make_hyp("eql", bt.binding, "equilibrium", "GradBal", [], {}, p.variables, 0.72)]
 def _hyp_superposition(p, bt, a, m):
     if a and len(a) > 0:
-        other = random.choice(a); lam = 0.5
+        other = random.choice(a)
+        lam = 0.5
         nb = {v: lam * bt.binding.get(v, 0) + (1 - lam) * other.binding.get(v, 0) for v in p.variables}
         return [_make_hyp("sup", nb, "superposition", "Superpose", [], {}, p.variables, 0.58)]
     return []
 def _hyp_locality(p, bt, a, m): return [_make_hyp("loc", bt.binding, "locality", "LocalFirst", [], {}, p.variables, 0.72)]
 def _hyp_extremal(p, bt, a, m):
-    hyps = []; b = dict(bt.binding)
+    hyps = []
+    b = dict(bt.binding)
     if bt.l9 and bt.l9.dominant_vars:
-        v = bt.l9.dominant_vars[0]; lo, hi = p.bounds.get(v, (0, 1))
+        v = bt.l9.dominant_vars[0]
+        lo, hi = p.bounds.get(v, (0, 1))
         for val in [lo, hi, (lo + hi) / 2]:
-            nb = dict(b); nb[v] = val
+            nb = dict(b)
+            nb[v] = val
             hyps.append(_make_hyp(f"ext_{v}_{val:.3f}", nb, "extremal", f"PinBound({v}={val:.3f})", [], {v: val}, p.variables, 0.65))
     return hyps
 def _hyp_entropy(p, bt, a, m): return [_make_hyp("ent", {v: random.uniform(*p.bounds[v]) for v in p.variables}, "entropy", "MaxEnt", [], {}, p.variables, 0.48)]
@@ -1000,7 +1207,8 @@ def _hyp_injective(p, bt, a, m): return [_make_hyp("inj", bt.binding, "injective
 def _hyp_surjective(p, bt, a, m): return [_make_hyp("sur", bt.binding, "surjective", "Sweep", [], {}, p.variables, 0.45)]
 def _hyp_transitive(p, bt, a, m): return [_make_hyp("tra", bt.binding, "transitive", "TransSnap", [], {}, p.variables, 0.77)]
 def _hyp_atomic(p, bt, a, m):
-    hyps = []; b = dict(bt.binding)
+    hyps = []
+    b = dict(bt.binding)
     for mc in p.compiled_constraints:
         if not mc.projections: continue
         for v, projs in mc.projections.items():
@@ -1009,7 +1217,8 @@ def _hyp_atomic(p, bt, a, m):
                     val = float(proj["func"](*[b.get(s, 0.0) for s in proj["syms"]]))
                     lo, hi = p.bounds.get(v, (-1e9, 1e9))
                     if math.isfinite(val) and lo <= val <= hi:
-                        nb = dict(b); nb[v] = val
+                        nb = dict(b)
+                        nb[v] = val
                         hyps.append(_make_hyp(f"ato_{v}", nb, "atomic", f"Solve({v})", [], {v: val}, p.variables, 0.70))
                         break
                 except: pass
@@ -1022,11 +1231,14 @@ def _hyp_negation(p, bt, a, m):
 def _hyp_composite(p, bt, a, m): return [_make_hyp("cmp", bt.binding, "composite", "Enz", [], {}, p.variables, 0.90)]
 def _hyp_holism(p, bt, a, m): return [_make_hyp("hol", bt.binding, "holism", "Global", [], {}, p.variables, 0.73)]
 def _hyp_parsimony(p, bt, a, m):
-    b = dict(bt.binding); nb = {}
+    b = dict(bt.binding)
+    nb = {}
     max_val = max((abs(v) for v in b.values()), default=1.0)
     for v in p.variables:
-        val = b[v]; lo, hi = p.bounds[v]
-        if abs(val) < 0.1 * max_val and lo <= 0.0 <= hi: nb[v] = 0.0
+        val = b[v]
+        lo, hi = p.bounds[v]
+        if abs(val) < 0.1 * max_val and lo <= 0.0 <= hi: 
+            nb[v] = 0.0
         else:
             candidates = [round(val * m) / m for m in [1, 2, 4] if lo <= round(val * m) / m <= hi]
             nb[v] = min(candidates, key=lambda c: abs(c - val)) if candidates else val
@@ -1080,9 +1292,13 @@ class CreativeSeeder:
         scored = []
         for ax in remaining_axioms:
             w_allos = 1.0
-            if n_dom == 1 and ax in isolated:    w_allos += 5.0
-            elif n_dom == 2 and ax in relational: w_allos += 5.0
-            elif n_dom >= 3 and ax in systemic:  w_allos += 5.0
+            if n_dom == 1 and ax in isolated:    
+                w_allos += 5.0
+            elif n_dom == 2 and ax in relational: 
+                w_allos += 5.0
+            elif n_dom >= 3 and ax in systemic:  
+                w_allos += 5.0
+                
             w_sketch = sketch.axiom_affinities.get(ax, 1.0) if sketch else 1.0
             scored.append((w_allos * w_sketch, ax))
 
@@ -1090,7 +1306,9 @@ class CreativeSeeder:
         children = []
         for _, axiom in scored[:effective_width]:
             child = ray.extend(axiom, "branch", new_prior=out_baton.ce)
-            if child: child.baton = out_baton; children.append(child)
+            if child: 
+                child.baton = out_baton
+                children.append(child)
         return children
 
     def sketch_weighted_seeds(self, sketch: StructuralSketch, init_ce: float) -> List[AxiomRay]:
@@ -1109,17 +1327,24 @@ class CreativeSeeder:
                         if b2 in (a, b1, mid, c): continue
                         if frozenset([mid, b2]) not in _CONTRA_SET and frozenset([b2, c]) not in _CONTRA_SET:
                             results.append(AxiomRay([a, b1, mid, b2, c], f"T5_{AXIOM_ABBR.get(a, '?')}_{AXIOM_ABBR.get(c, '?')}", "tension"))
-        random.shuffle(results); return results[:max_n]
+        random.shuffle(results)
+        return results[:max_n]
 
     def random_scouts(self, n: int = 600) -> List[AxiomRay]:
-        scouts = []; attempts = 0
+        scouts = []
+        attempts = 0
         while len(scouts) < n and attempts < n * 30:
-            attempts += 1; length = random.randint(3, 12)
-            pool = list(ALL_AXIOMS); random.shuffle(pool); seq = [pool[0]]
+            attempts += 1
+            length = random.randint(3, 12)
+            pool = list(ALL_AXIOMS)
+            random.shuffle(pool)
+            seq = [pool[0]]
             for ax in pool[1:]:
                 if len(seq) >= length: break
-                if ax != seq[-1] and frozenset([seq[-1], ax]) not in _CONTRA_SET: seq.append(ax)
-            if len(seq) >= 3: scouts.append(AxiomRay(seq, f"SC_{''.join(AXIOM_ABBR.get(a, a[:2]) for a in seq)}", "scout"))
+                if ax != seq[-1] and frozenset([seq[-1], ax]) not in _CONTRA_SET: 
+                    seq.append(ax)
+            if len(seq) >= 3: 
+                scouts.append(AxiomRay(seq, f"SC_{''.join(AXIOM_ABBR.get(a, a[:2]) for a in seq)}", "scout"))
         return scouts
 
     def recombine(self, ray_a, ray_b, ba, bb) -> List[AxiomRay]:
@@ -1131,21 +1356,26 @@ class CreativeSeeder:
             cut = min(len(ray_a.sequence), len(ray_b.sequence)) // 2
             if cut > 0:
                 seq = ray_a.sequence[:cut] + [x for x in ray_b.sequence[cut:] if x not in ray_a.sequence[:cut]]
-                if sequence_valid(seq): results.append(AxiomRay(seq, f"RC_l{int(lam*100)}", "recombine", baton=ib_baton, ce_prior=ib_ce))
+                if sequence_valid(seq): 
+                    results.append(AxiomRay(seq, f"RC_l{int(lam*100)}", "recombine", baton=ib_baton, ce_prior=ib_ce))
         return results
 
     def invert(self, ray, parent_ce) -> Optional[AxiomRay]:
         inv = list(reversed(ray.sequence))
-        if sequence_valid(inv) and inv != ray.sequence: return AxiomRay(inv, f"INV_{ray.ray_id}", "invert", parent_id=ray.ray_id, ce_prior=parent_ce)
+        if sequence_valid(inv) and inv != ray.sequence: 
+            return AxiomRay(inv, f"INV_{ray.ray_id}", "invert", parent_id=ray.ray_id, ce_prior=parent_ce)
         return None
 
     def resonance_extensions(self, ray, parent_ce, resonant_pairs) -> List[AxiomRay]:
         if not ray.sequence or not resonant_pairs: return []
-        last = ray.sequence[-1]; results = []
+        last = ray.sequence[-1]
+        results = []
         nexts = [b for (a, b) in resonant_pairs if a == last and b != last and frozenset([a, b]) not in _CONTRA_SET and b not in ray.sequence]
         for b in nexts:
             child = ray.extend(b, "branch", new_prior=parent_ce)
-            if child: child.ray_id = f"RES_{child.ray_id}"; results.append(child)
+            if child: 
+                child.ray_id = f"RES_{child.ray_id}"
+                results.append(child)
         return results
 
 CREATIVE_SEEDER = CreativeSeeder()
@@ -1159,15 +1389,25 @@ def _verify(binding, base_problem, anchors):
     g2 = {}
     for inv in anchors:
         try:
-            if inv.compiled_func: val = float(inv.compiled_func(*[binding.get(v, 0.0) for v in inv.syms_used]))
-            else: val = 999.0
+            if inv.compiled_func: 
+                val = float(inv.compiled_func(*[binding.get(v, 0.0) for v in inv.syms_used]))
+            else: 
+                val = 999.0
+                
             err = abs(val)
-            if inv.mode == "eq":    passed = err < inv.tolerance
-            elif inv.mode == "geq": passed = val >= -inv.tolerance
-            elif inv.mode == "leq": passed = val <= inv.tolerance
-            else:                 passed = err < inv.tolerance
+            if inv.mode == "eq":    
+                passed = err < inv.tolerance
+            elif inv.mode == "geq": 
+                passed = val >= -inv.tolerance
+            elif inv.mode == "leq": 
+                passed = val <= inv.tolerance
+            else:                 
+                passed = err < inv.tolerance
+                
             g2[inv.name] = (round(val if inv.mode in ("geq", "leq") else err, 6), passed)
-        except: g2[inv.name] = (999.0, False)
+        except: 
+            g2[inv.name] = (999.0, False)
+            
     g2_pass = all(v[1] for v in g2.values()) if g2 else True
     return g1_pass, g2_pass, g2, round(g1_ce, 6)
 
@@ -1178,55 +1418,77 @@ class SequenceRayTracer:
 
     def trace(self, axl_def: AXLProblemDef, base_problem: Problem):
         hero_traces: List[HypothesisTrace] = []
-        baton_registry: Dict[str, Baton] = {}; baton_registry_keys: deque = deque()
-        successful_rays: List[AxiomRay] = []; resonant_pairs: List[Tuple[str, str]] = []
+        baton_registry: Dict[str, Baton] = {}
+        baton_registry_keys: deque = deque()
+        successful_rays: List[AxiomRay] = []
+        resonant_pairs: List[Tuple[str, str]] = []
 
         for inv in axl_def.anchors:
-            if not inv.compiled_func: inv.compile(base_problem.variables)
+            if not inv.compiled_func: 
+                inv.compile(base_problem.variables)
 
-        _update_state(phase="SKETCHING"); _add_log("🗺 Computing structural sketch…")
+        _update_state(phase="SKETCHING")
+        _add_log("🗺 Computing structural sketch…")
         sketch = compute_sketch(base_problem)
         _update_state(sketch_summary="; ".join(sketch.sketch_notes[:4]), sympy_derivation=sketch.sympy_derivation)
         _add_log(f"✓ Sketch: {sketch.dominant_type} system, DOF={sketch.n_free_dof}")
 
-        _update_state(phase="TEMPLATING"); _add_log("🔬 Generating hypothesis templates…")
+        _update_state(phase="TEMPLATING")
+        _add_log("🔬 Generating hypothesis templates…")
         templates = generate_templates(base_problem, sketch)
         _update_state(template_count=len(templates))
 
         init_b, init_ce = _mprt_sample(base_problem, {v: IV(*base_problem.bounds[v]) for v in base_problem.variables}, N_MPRT_EXPLORE)
         seed_baton = Baton(binding=init_b, ce=init_ce, ray_id="SEED", l9=L9Certificate(init_ce, base_problem.variables[:3], [], "systemic"))
 
-        best_ce = init_ce; best_binding = dict(init_b)
+        best_ce = init_ce
+        best_binding = dict(init_b)
+        
         if templates:
             _add_log("⚗ Evaluating templates (Phase 0 batch)…")
             template_hyps = templates_to_hypotheses(templates, base_problem, init_b)
             t_results = _batched_deduce_and_evaluate(base_problem, template_hyps)
+            
             for (th, template), (final_b, final_ce, dom_vars, tc) in zip(zip(template_hyps, templates), t_results):
                 g1p, g2p, inv_res, g1ce = _verify(final_b, base_problem, axl_def.anchors)
                 overall = g1p and g2p
+                
                 if overall or final_ce < best_ce:
                     hero_traces.append(HypothesisTrace(
                         hid=template.template_id, round_idx=0, ray_name=f"template:{template.source}", ray_type="template",
                         ce_before=init_ce, ce_after=final_ce, survived=overall, elapsed_ms=0.0,
                         g1_pass=g1p, g2_pass=g2p, binding={k: round(v, 5) for k, v in final_b.items()},
                         invariant_results=inv_res, tension_class=tc, depth=0))
-                    with STATE_LOCK: GLOBAL_SOLVE_STATE["recent_traces"].append(hero_traces[-1])
+                        
+                    with STATE_LOCK: 
+                        GLOBAL_SOLVE_STATE["recent_traces"].append(hero_traces[-1])
+                        
                 if final_ce < best_ce:
-                    best_ce = final_ce; best_binding = dict(final_b)
+                    best_ce = final_ce
+                    best_binding = dict(final_b)
                     _update_state(best_ce=best_ce)
+                    
                 if overall:
                     _add_log(f"✓ Template solved at Phase 0! Source: {template.source}")
                     _update_state(best_ce=best_ce, template_best_ce=best_ce, best_ray=f"template:{template.source}")
                     return best_binding, best_ce, hero_traces, 0, {"isolated": 0, "relational": 0, "systemic": 0}
+                    
             _update_state(template_best_ce=best_ce)
 
         _update_state(phase="SEARCHING")
         seed_rays = CREATIVE_SEEDER.sketch_weighted_seeds(sketch, best_ce)
 
-        queues = {"core": seed_rays, "explore": CREATIVE_SEEDER.tension_seeds(3000) + CREATIVE_SEEDER.random_scouts(600), "genetic": CREATIVE_SEEDER.target_seeds(axl_def.anchors)}
-        random.shuffle(queues["explore"]); random.shuffle(queues["genetic"])
-
-        queue_order = ["core", "explore", "genetic"]; q_idx = 0; total_fired = 0
+        queues = {
+            "core": seed_rays, 
+            "explore": CREATIVE_SEEDER.tension_seeds(3000) + CREATIVE_SEEDER.random_scouts(600), 
+            "genetic": CREATIVE_SEEDER.target_seeds(axl_def.anchors)
+        }
+        random.shuffle(queues["explore"])
+        random.shuffle(queues["genetic"])
+
+        queue_order = ["core", "explore", "genetic"]
+        q_idx = 0
+        total_fired = 0
         allosteric_counts = {"isolated": 0, "relational": 0, "systemic": 0}
         model = StructuralModel(best_binding, best_ce)
         seed_baton = Baton(binding=best_binding, ce=best_ce, ray_id="SEED", l9=L9Certificate(best_ce, base_problem.variables[:3], [], "systemic"))
@@ -1239,31 +1501,39 @@ class SequenceRayTracer:
                     q_idx = (q_idx + 1) % 3
                     if q_idx == start_idx: break
                 if not any(queues[k] for k in queue_order): break
-                ray = queues[queue_order[q_idx]].pop(0); q_idx = (q_idx + 1) % 3
-                batch_rays.append(ray); total_fired += 1
+                ray = queues[queue_order[q_idx]].pop(0)
+                q_idx = (q_idx + 1) % 3
+                batch_rays.append(ray)
+                total_fired += 1
+                
             if not batch_rays: break
 
             t0 = time.time()
             historical_batons = list(baton_registry.values())
             batch_hyps: List[Tuple[int, Hypothesis]] = []
+            
             for i, ray in enumerate(batch_rays):
                 p_baton = ray.baton or seed_baton
                 constructor = AXIOM_CONSTRUCTORS.get(ray.sequence[-1])
                 hyps = constructor(base_problem, p_baton, historical_batons, model) if constructor else []
-                if not hyps: hyps = [_make_hyp("fb", p_baton.binding, "fallback", "Pass", [], {}, base_problem.variables, 0.1)]
+                if not hyps: 
+                    hyps = [_make_hyp("fb", p_baton.binding, "fallback", "Pass", [], {}, base_problem.variables, 0.1)]
                 batch_hyps.append((i, hyps[0]))
 
             eval_results = _batched_deduce_and_evaluate(base_problem, [h for _, h in batch_hyps])
             elapsed_ms = (time.time() - t0) * 1000 / max(1, len(batch_rays))
 
-            solved = False; batch_heroes = []
+            solved = False
+            batch_heroes = []
+            
             for (ray_idx, hyp), (final_b, final_ce, dom_vars, tension_class) in zip(batch_hyps, eval_results):
                 ray = batch_rays[ray_idx]
                 parent_ce = (ray.baton or seed_baton).ce
                 allosteric_counts[tension_class] = allosteric_counts.get(tension_class, 0) + 1
 
                 g1_pass, g2_pass, inv_results, g1_ce = _verify(final_b, base_problem, axl_def.anchors)
-                overall_pass = g1_pass and g2_pass; improved = final_ce < best_ce
+                overall_pass = g1_pass and g2_pass
+                improved = final_ce < best_ce
 
                 if improved or overall_pass or random.random() < 0.002:
                     trace = HypothesisTrace(
@@ -1277,21 +1547,30 @@ class SequenceRayTracer:
                 out_baton = Baton(binding=final_b, ce=final_ce, ray_id=ray.ray_id, l9=L9Certificate(final_ce, dom_vars, [], tension_class))
 
                 if final_ce < BATON_REGISTRY_THRESHOLD:
-                    if ray.ray_id in baton_registry: baton_registry[ray.ray_id] = out_baton
+                    if ray.ray_id in baton_registry: 
+                        baton_registry[ray.ray_id] = out_baton
                     else:
                         if len(baton_registry) >= BATON_REGISTRY_MAX:
-                            old_key = baton_registry_keys.popleft(); baton_registry.pop(old_key, None)
-                        baton_registry[ray.ray_id] = out_baton; baton_registry_keys.append(ray.ray_id)
+                            old_key = baton_registry_keys.popleft()
+                            baton_registry.pop(old_key, None)
+                        baton_registry[ray.ray_id] = out_baton
+                        baton_registry_keys.append(ray.ray_id)
 
                 if improved:
-                    best_ce = final_ce; best_binding = dict(final_b); successful_rays.append(ray)
-                    model.best_binding = best_binding; model.best_ce = best_ce; model.best_ray = ray.name
+                    best_ce = final_ce
+                    best_binding = dict(final_b)
+                    successful_rays.append(ray)
+                    model.best_binding = best_binding
+                    model.best_ce = best_ce
+                    model.best_ray = ray.name
 
-                if overall_pass: solved = True
+                if overall_pass: 
+                    solved = True
 
                 if improved and len(ray.sequence) >= 2:
                     pair = (ray.sequence[-2], ray.sequence[-1])
-                    if pair not in resonant_pairs: resonant_pairs.append(pair)
+                    if pair not in resonant_pairs: 
+                        resonant_pairs.append(pair)
                     model.resonant_pairs = resonant_pairs
 
                 earned = (final_ce < parent_ce * CE_EARN_RATIO or ray.depth < 1)
@@ -1301,25 +1580,39 @@ class SequenceRayTracer:
                     remaining = [a for a in ALL_AXIOMS if a != ray.sequence[-1] and frozenset([ray.sequence[-1], a]) not in _CONTRA_SET and a not in ray.sequence]
                     new_children = []
                     new_children.extend(CREATIVE_SEEDER.intelligent_branch(ray, out_baton, remaining, BRANCH_WIDTH, sketch=sketch))
+                    
                     inv = CREATIVE_SEEDER.invert(ray, final_ce)
-                    if inv: new_children.append(inv)
+                    if inv: 
+                        new_children.append(inv)
+                        
                     if len(successful_rays) >= 2:
                         candidates = [r for r in successful_rays if r.ray_id != ray.ray_id]
                         if candidates:
-                            partner = random.choice(candidates); ba = baton_registry.get(ray.ray_id, out_baton); bb = baton_registry.get(partner.ray_id)
-                            if bb is not None: new_children.extend(CREATIVE_SEEDER.recombine(ray, partner, ba, bb)[:3])
+                            partner = random.choice(candidates)
+                            ba = baton_registry.get(ray.ray_id, out_baton)
+                            bb = baton_registry.get(partner.ray_id)
+                            if bb is not None: 
+                                new_children.extend(CREATIVE_SEEDER.recombine(ray, partner, ba, bb)[:3])
+                                
                     new_children.extend(CREATIVE_SEEDER.resonance_extensions(ray, final_ce, resonant_pairs))
+                    
                     for child in new_children:
-                        if child.ray_type in ("seed", "branch", "target"):  queues["core"].append(child)
-                        elif child.ray_type in ("scout", "tension"):       queues["explore"].append(child)
-                        elif child.ray_type in ("recombine", "invert"):    queues["genetic"].append(child)
+                        if child.ray_type in ("seed", "branch", "target"):  
+                            queues["core"].append(child)
+                        elif child.ray_type in ("scout", "tension"):       
+                            queues["explore"].append(child)
+                        elif child.ray_type in ("recombine", "invert"):    
+                            queues["genetic"].append(child)
 
             queues["core"].sort(key=lambda r: r.ce_prior + (r.depth * 0.0001))
             queues["genetic"].sort(key=lambda r: r.ce_prior + (r.depth * 0.0001))
 
             with STATE_LOCK:
-                GLOBAL_SOLVE_STATE["best_ce"] = best_ce; GLOBAL_SOLVE_STATE["total_fired"] = total_fired; GLOBAL_SOLVE_STATE["best_ray"] = model.best_ray
-                for t in batch_heroes: GLOBAL_SOLVE_STATE["recent_traces"].append(t)
+                GLOBAL_SOLVE_STATE["best_ce"] = best_ce
+                GLOBAL_SOLVE_STATE["total_fired"] = total_fired
+                GLOBAL_SOLVE_STATE["best_ray"] = model.best_ray
+                for t in batch_heroes: 
+                    GLOBAL_SOLVE_STATE["recent_traces"].append(t)
 
             if solved: break
 
@@ -1363,84 +1656,149 @@ def encode_problem_to_axl(problem_text, api_key) -> AXLProblemDef:
     resp = client.models.generate_content(model=GEMINI_MODEL, contents=[types.Content(role="user", parts=[types.Part.from_text(text=problem_text)])], config=config)
     
     text = resp.text.strip()
-    if text.startswith("```"): text = text.split("```")[1]; (text := text[4:]) if text.startswith("json") else text
+    if text.startswith("```"): 
+        text = text.split("```")[1]
+        if text.startswith("json"):
+            text = text[4:]
+            
     text = text.strip().rstrip("`").strip()
     d = json.loads(text)
     
     anchors = [AXLInvariant(name=a["name"], expr=a["expr"], tolerance=a.get("tolerance", VERIFY_G2_TOLERANCE), mode=a.get("mode", "eq")) for a in d.get("anchors", [])]
     variables = [{"name": v["name"], "lo": float(v.get("lo", -1000.0)), "hi": float(v.get("hi", 1000.0))} for v in d["variables"]]
+    
     return AXLProblemDef(name=d["name"], description=d.get("description", ""), axioms=set(), variables=variables, constraints=d.get("constraints", []), scopes=d.get("scopes", []), anchors=anchors, observations=d.get("observations", {}))
 
 def collapse_solution(problem_text, axl_def, psl_text, binding, g1_pass, g2_pass, inv_results, best_ray, total_fired, sketch_notes, sympy_derivation, api_key) -> str:
     if not api_key: return "ERROR: API Key required."
     client = genai.Client(api_key=api_key)
-    payload = {"original_problem": problem_text, "solved": g1_pass and g2_pass, "binding": {k: round(v, 6) for k, v in binding.items()}, "psl_program_text": psl_text, "isomorphism_hypothesis": best_ray, "structural_sketch_notes": sketch_notes, "sympy_derivation_chain": sympy_derivation, "invariant_results": inv_results}
+    
+    payload = {
+        "original_problem": problem_text, 
+        "solved": g1_pass and g2_pass, 
+        "binding": {k: round(v, 6) for k, v in binding.items()}, 
+        "psl_program_text": psl_text, 
+        "isomorphism_hypothesis": best_ray, 
+        "structural_sketch_notes": sketch_notes, 
+        "sympy_derivation_chain": sympy_derivation, 
+        "invariant_results": inv_results
+    }
+    
     config = types.GenerateContentConfig(thinking_config=types.ThinkingConfig(thinking_level="HIGH"), system_instruction=[types.Part.from_text(text=COLLAPSER_SYSTEM_PROMPT)], temperature=0.2)
     resp = client.models.generate_content(model=GEMINI_MODEL, contents=[types.Content(role="user", parts=[types.Part.from_text(text=json.dumps(payload, indent=2))])], config=config)
     return resp.text
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 15: GLOBAL SOLVE TASK
+# SECTION 15: GLOBAL SOLVE TASK (With Thread Crash Safety)
 # ══════════════════════════════════════════════════════════════════════
 def global_solve_task(original_problem_text, api_key, prebuilt_axl=None):
-    _update_state(is_running=True, phase="ENCODING", high_level_logs=[], answer="", best_ce=float('inf'), total_fired=0, best_ray="—", recent_traces=deque(maxlen=25), sketch_summary="", template_count=0, template_best_ce=float('inf'), sympy_derivation=[])
-    MAX_ATTEMPTS = 3; current_text = original_problem_text; used_key = api_key or DEFAULT_GEMINI_API_KEY; sketch_notes = []
-
-    for attempt in range(1, MAX_ATTEMPTS + 1):
-        if prebuilt_axl is not None:
-            _add_log("⚡ Bypassing Encoder: Using Pre-compiled Quantum AXL")
-            axl_def = prebuilt_axl
-        else:
-            _add_log(f"🔍 Encoding (attempt {attempt}/{MAX_ATTEMPTS})…")
-            try: axl_def = encode_problem_to_axl(current_text, used_key)
-            except Exception as e: _add_log(f"✗ Encode failed: {e}"); _update_state(is_running=False, phase="ERROR"); return
-        
-        _add_log(f"✓ `{axl_def.name}` | vars: {', '.join(v['name'] for v in axl_def.variables)}")
-        _update_state(phase="COMPILING")
-
-        try: psl_text = AXL_COMPILER.compile(axl_def); base_prob = build_base_problem(axl_def)
-        except Exception as e: _add_log(f"✗ Compile failed: {e}"); _update_state(is_running=False, phase="ERROR"); return
-
-        try: tracer = SequenceRayTracer(); binding, ce, traces, total_fired, allosteric = tracer.trace(axl_def, base_prob)
-        except Exception as e: _add_log(f"✗ Solver error: {e}"); _update_state(is_running=False, phase="ERROR"); return
-
-        with STATE_LOCK: sketch_notes = GLOBAL_SOLVE_STATE.get("sketch_summary", "").split("; "); current_sympy_derivation = GLOBAL_SOLVE_STATE.get("sympy_derivation", [])
-
-        survived = [t for t in traces if t.survived]; best_t = min(survived, key=lambda t: t.ce_after, default=None)
-
-        for inv in axl_def.anchors:
-            if not inv.compiled_func: inv.compile(base_prob.variables)
-
-        g1_ce = base_prob.scalar_energy(binding); g1_pass = g1_ce < VERIFY_G1_THRESHOLD; inv_results = {}
-        for inv in axl_def.anchors:
+    _update_state(
+        is_running=True, phase="ENCODING", high_level_logs=[], answer="", 
+        best_ce=float('inf'), total_fired=0, best_ray="—", recent_traces=deque(maxlen=25), 
+        sketch_summary="", template_count=0, template_best_ce=float('inf'), sympy_derivation=[]
+    )
+    
+    try:
+        MAX_ATTEMPTS = 3
+        current_text = original_problem_text
+        used_key = api_key or DEFAULT_GEMINI_API_KEY
+        sketch_notes = []
+
+        for attempt in range(1, MAX_ATTEMPTS + 1):
+            if prebuilt_axl is not None:
+                _add_log("⚡ Bypassing Encoder: Using Pre-compiled Quantum AXL")
+                axl_def = prebuilt_axl
+            else:
+                _add_log(f"🔍 Encoding (attempt {attempt}/{MAX_ATTEMPTS})…")
+                try: 
+                    axl_def = encode_problem_to_axl(current_text, used_key)
+                except Exception as e: 
+                    _add_log(f"✗ Encode failed: {e}")
+                    _update_state(phase="ERROR", answer=f"Encoder API Failed: {str(e)}")
+                    return
+            
+            _add_log(f"✓ `{axl_def.name}` | vars: {', '.join(v['name'] for v in axl_def.variables)}")
+            _update_state(phase="COMPILING")
+
+            try: 
+                psl_text = AXL_COMPILER.compile(axl_def)
+                base_prob = build_base_problem(axl_def)
+            except Exception as e: 
+                _add_log(f"✗ Compile failed: {e}")
+                _update_state(phase="ERROR", answer=f"Compiler Failed: {str(e)}")
+                return
+
+            try: 
+                tracer = SequenceRayTracer()
+                binding, ce, traces, total_fired, allosteric = tracer.trace(axl_def, base_prob)
+            except Exception as e: 
+                _add_log(f"✗ Solver error: {e}")
+                _update_state(phase="ERROR", answer=f"Ray Tracer Crashed: {str(e)}")
+                return
+
+            with STATE_LOCK: 
+                sketch_notes = GLOBAL_SOLVE_STATE.get("sketch_summary", "").split("; ")
+                current_sympy_derivation = GLOBAL_SOLVE_STATE.get("sympy_derivation", [])
+
+            survived = [t for t in traces if t.survived]
+            best_t = min(survived, key=lambda t: t.ce_after, default=None)
+
+            for inv in axl_def.anchors:
+                if not inv.compiled_func: 
+                    inv.compile(base_prob.variables)
+
+            g1_ce = base_prob.scalar_energy(binding)
+            g1_pass = g1_ce < VERIFY_G1_THRESHOLD
+            inv_results = {}
+            
+            for inv in axl_def.anchors:
+                try:
+                    val = float(inv.compiled_func(*[binding.get(v, 0.0) for v in inv.syms_used]))
+                    err = abs(val)
+                    if inv.mode == "eq":
+                        passed = err < inv.tolerance
+                    elif inv.mode == "geq":
+                        passed = val >= -inv.tolerance
+                    else:
+                        passed = val <= inv.tolerance
+                    inv_results[inv.name] = (round(val, 6), passed)
+                except: 
+                    inv_results[inv.name] = (999.0, False)
+                    
+            g2_pass = all(v[1] for v in inv_results.values())
+
+            solved_str = "✓ SOLVED" if (g1_pass and g2_pass) else "~ PARTIAL" if g1_pass else "✗ UNSOLVED"
+            best_ray = best_t.ray_name if best_t else "—"
+            _add_log(f"🏁 {solved_str} (CE: {ce:.5f}) | Ray: {best_ray}")
+
+            if prebuilt_axl is None:
+                if not g1_pass and attempt < MAX_ATTEMPTS:
+                    current_text = (original_problem_text + f"\n\nPREVIOUS ATTEMPT FAILED (Best CE: {ce}):\nGEOMETRIC SOLVER FAILED. Apply ALGEBRAIC REDUCTION: substitute simple equalities to eliminate variables, output simplified AXL.")
+                    _add_log("⚠ Geometric solver failed. Triggering algebraic reduction…")
+                    continue
+                if not g2_pass and attempt < MAX_ATTEMPTS:
+                    failed = {k: v for k, (v, ok) in inv_results.items() if not ok}
+                    current_text = (original_problem_text + f"\n\nPREVIOUS ATTEMPT FAILED:\nGate 2 failed:\n{json.dumps(failed, indent=2)}\nRevise constraint encoding to capture these conditions.")
+                    _add_log("⚠ Gate 2 failed. Retrying with structural feedback…")
+                    continue
+
+            _add_log("🔤 Collapsing isomorphism to domain language…")
+            _update_state(phase="COLLAPSING")
             try:
-                val = float(inv.compiled_func(*[binding.get(v, 0.0) for v in inv.syms_used])); err = abs(val)
-                passed = (err < inv.tolerance if inv.mode == "eq" else val >= -inv.tolerance if inv.mode == "geq" else val <= inv.tolerance)
-                inv_results[inv.name] = (round(val, 6), passed)
-            except: inv_results[inv.name] = (999.0, False)
-        g2_pass = all(v[1] for v in inv_results.values())
-
-        solved_str = "✓ SOLVED" if (g1_pass and g2_pass) else "~ PARTIAL" if g1_pass else "✗ UNSOLVED"
-        best_ray = best_t.ray_name if best_t else "—"
-        _add_log(f"🏁 {solved_str} (CE: {ce:.5f}) | Ray: {best_ray}")
-
-        if prebuilt_axl is None:
-            if not g1_pass and attempt < MAX_ATTEMPTS:
-                current_text = (original_problem_text + f"\n\nPREVIOUS ATTEMPT FAILED (Best CE: {ce}):\nGEOMETRIC SOLVER FAILED. Apply ALGEBRAIC REDUCTION: substitute simple equalities to eliminate variables, output simplified AXL.")
-                _add_log("⚠ Geometric solver failed. Triggering algebraic reduction…"); continue
-            if not g2_pass and attempt < MAX_ATTEMPTS:
-                failed = {k: v for k, (v, ok) in inv_results.items() if not ok}
-                current_text = (original_problem_text + f"\n\nPREVIOUS ATTEMPT FAILED:\nGate 2 failed:\n{json.dumps(failed, indent=2)}\nRevise constraint encoding to capture these conditions.")
-                _add_log("⚠ Gate 2 failed. Retrying with structural feedback…"); continue
-
-        _add_log("🔤 Collapsing isomorphism to domain language…")
-        _update_state(phase="COLLAPSING")
-        try:
-            answer = collapse_solution(original_problem_text, axl_def, psl_text, binding, g1_pass, g2_pass, inv_results, best_ray, total_fired, sketch_notes, current_sympy_derivation, used_key)
-            _update_state(answer=answer, phase="DONE"); _add_log("✓ Done.")
-        except Exception as e: _update_state(answer=f"Collapsing error: {e}", phase="ERROR"); _add_log("✗ Collapse failed.")
-        break
-    _update_state(is_running=False)
+                answer = collapse_solution(original_problem_text, axl_def, psl_text, binding, g1_pass, g2_pass, inv_results, best_ray, total_fired, sketch_notes, current_sympy_derivation, used_key)
+                _update_state(answer=answer, phase="DONE")
+                _add_log("✓ Done.")
+            except Exception as e: 
+                _update_state(answer=f"Collapsing error: {e}", phase="ERROR")
+                _add_log("✗ Collapse failed.")
+            break
+            
+    except Exception as e:
+        _add_log(f"💥 FATAL SYSTEM ERROR: {str(e)}")
+        _update_state(phase="ERROR", answer=f"Fatal System Error: {str(e)}")
+    finally:
+        # ABSOLUTE GUARANTEE: Never lock the UI
+        _update_state(is_running=False)
 
 def trigger_solve(problem_text, api_key):
     if GLOBAL_SOLVE_STATE["is_running"] or not problem_text.strip(): return
@@ -1448,28 +1806,46 @@ def trigger_solve(problem_text, api_key):
 
 def trigger_quantum_solve(example_name, api_key):
     if not HAS_QUANTUM or GLOBAL_SOLVE_STATE["is_running"]: return
-    _update_state(is_running=True)
     
-    if example_name == "Bell State": circ = QuantumCircuits.example_bell_state()
-    elif example_name == "VQE H2": circ = QuantumCircuits.example_vqe_h2()
-    elif example_name == "QAOA MaxCut": circ = QuantumCircuits.example_qaoa_maxcut_p1()
-    else: _update_state(is_running=False); return
-
-    problem_desc = f"Quantum Circuit: {circ.name}\nDescription: {circ.description}\nTarget Observables: {circ.expected_observables}"
-
-    try: axl_def = QuantumCircuits.build_quantum_axl(circ, AXLProblemDef, AXLInvariant)
-    except Exception as e: _add_log(f"✗ Quantum compiler failed: {e}"); _update_state(is_running=False, phase="ERROR"); return
+    # We yield control to the thread immediately so the button click finishes safely
+    def _run_q():
+        if example_name == "Bell State": 
+            circ = QuantumCircuits.example_bell_state()
+        elif example_name == "VQE H2": 
+            circ = QuantumCircuits.example_vqe_h2()
+        elif example_name == "QAOA MaxCut": 
+            circ = QuantumCircuits.example_qaoa_maxcut_p1()
+        else: 
+            return
+
+        problem_desc = f"Quantum Circuit: {circ.name}\nDescription: {circ.description}\nTarget Observables: {circ.expected_observables}"
+
+        try: 
+            axl_def = QuantumCircuits.build_quantum_axl(circ, AXLProblemDef, AXLInvariant)
+        except Exception as e: 
+            _update_state(is_running=False, phase="ERROR", answer=f"Quantum compiler failed: {str(e)}")
+            return
+            
+        global_solve_task(problem_desc, api_key, axl_def)
 
-    threading.Thread(target=global_solve_task, args=(problem_desc, api_key, axl_def), daemon=True).start()
+    threading.Thread(target=_run_q, daemon=True).start()
 
 # ══════════════════════════════════════════════════════════════════════
 # SECTION 16: GRADIO INTERFACE
 # ══════════════════════════════════════════════════════════════════════
-CSS = """body{background:#090909;color:#e0e0e0;font-family:monospace;}
-.solver-log{font-size:0.75em;background:#0d0d0d;border:1px solid #181818;}
-.answer-box{font-size:0.85em;background:#0d0d0d;border:1px solid #222;padding:10px;}"""
+# Layout fixes for mobile sizing and wrapping
+CSS = """
+body { background: #090909; color: #e0e0e0; font-family: monospace; }
+.solver-log { font-size: 0.75em; background: #0d0d0d; border: 1px solid #181818; }
+.answer-box { font-size: 0.85em; background: #0d0d0d; border: 1px solid #222; padding: 10px; }
+.wrap-row { flex-wrap: wrap !important; }
+"""
+
+RAY_ICONS = {
+    "seed": "🌱", "branch": "🌿", "tension": "⚡", "scout": "🔭", 
+    "recombine": "🧬", "invert": "🔄", "target": "🎯", "template": "🗺", "fallback": "·"
+}
 
-RAY_ICONS = {"seed": "🌱", "branch": "🌿", "tension": "⚡", "scout": "🔭", "recombine": "🧬", "invert": "🔄", "target": "🎯", "template": "🗺", "fallback": "·"}
 PLACEHOLDER_HINT = textwrap.dedent("""
     Try any natural language problem. Gemini encodes it, the system finds the structural solution.
     Examples:
@@ -1479,28 +1855,50 @@ PLACEHOLDER_HINT = textwrap.dedent("""
 
 def build_live_html():
     with STATE_LOCK:
-        phase = GLOBAL_SOLVE_STATE["phase"]; ce = GLOBAL_SOLVE_STATE["best_ce"]
-        fired = GLOBAL_SOLVE_STATE["total_fired"]; best_ray = GLOBAL_SOLVE_STATE["best_ray"]
-        traces = list(GLOBAL_SOLVE_STATE["recent_traces"]); logs = GLOBAL_SOLVE_STATE["high_level_logs"]
+        phase = GLOBAL_SOLVE_STATE["phase"]
+        ce = GLOBAL_SOLVE_STATE["best_ce"]
+        fired = GLOBAL_SOLVE_STATE["total_fired"]
+        best_ray = GLOBAL_SOLVE_STATE["best_ray"]
+        traces = list(GLOBAL_SOLVE_STATE["recent_traces"])
+        logs = GLOBAL_SOLVE_STATE["high_level_logs"]
         sketch_summary = GLOBAL_SOLVE_STATE["sketch_summary"]
-        template_count = GLOBAL_SOLVE_STATE["template_count"]; template_best = GLOBAL_SOLVE_STATE["template_best_ce"]
+        template_count = GLOBAL_SOLVE_STATE["template_count"]
+        template_best = GLOBAL_SOLVE_STATE["template_best_ce"]
 
     ce_color = "#4CAF50" if ce < SOLVE_THRESHOLD else "#FF9800"
-    phase_color = "#26C6DA" if phase in ["SEARCHING", "COLLAPSING", "ENCODING", "SKETCHING", "TEMPLATING"] else ("#4CAF50" if phase == "DONE" else "#888")
+    
+    if phase in ["SEARCHING", "COLLAPSING", "ENCODING", "SKETCHING", "TEMPLATING"]:
+        phase_color = "#26C6DA"
+    elif phase == "DONE":
+        phase_color = "#4CAF50"
+    elif phase == "ERROR":
+        phase_color = "#F44336"
+    else:
+        phase_color = "#888"
 
     log_html = "<ul style='margin:0;padding-left:20px;color:#aaa;font-size:0.82em'>"
-    for l in logs[-5:]: log_html += f"<li>{l}</li>"
+    for l in logs[-5:]: 
+        log_html += f"<li>{l}</li>"
     log_html += "</ul>"
 
-    sketch_html = (f"<div style='color:#555;font-size:0.72em;margin:6px 0;padding:4px 8px;border-left:2px solid #26C6DA;background:#0a0a0a'>🗺 <span style='color:#26C6DA'>Sketch</span>: {sketch_summary[:120]}</div>") if sketch_summary else ""
-    template_html = (f"<div style='color:#555;font-size:0.72em;margin:4px 0'>🗺 Templates: {template_count} generated | floor CE: {f'{template_best:.5f}' if template_best < float('inf') else '—'}</div>") if template_count > 0 else ""
+    sketch_html = ""
+    if sketch_summary:
+        sketch_html = f"<div style='color:#555;font-size:0.72em;margin:6px 0;padding:4px 8px;border-left:2px solid #26C6DA;background:#0a0a0a'>🗺 <span style='color:#26C6DA'>Sketch</span>: {sketch_summary[:120]}</div>"
+        
+    template_html = ""
+    if template_count > 0:
+        t_ce_str = f"{template_best:.5f}" if template_best < float('inf') else "—"
+        template_html = f"<div style='color:#555;font-size:0.72em;margin:4px 0'>🗺 Templates: {template_count} generated | floor CE: {t_ce_str}</div>"
 
     ray_trail = ""
     for t in reversed(traces):
-        icon = RAY_ICONS.get(t.ray_type, "·"); c = "#4CAF50" if t.survived else "#555"; star = " ◀" if t.survived else ""
+        icon = RAY_ICONS.get(t.ray_type, "·")
+        c = "#4CAF50" if t.survived else "#555"
+        star = " ◀" if t.survived else ""
         ray_trail += f"<div style='color:{c};font-size:0.78em;margin-bottom:2px'>{icon} [{t.ray_name}] CE={t.ce_after:.4f} <span style='color:#888'>({t.tension_class[:3]})</span><span style='color:#4CAF50;font-weight:700'>{star}</span></div>"
 
-    return f"""<div style='border:1px solid #222;border-radius:6px;padding:12px;background:#0d0d0d;min-height:440px;display:flex;flex-direction:column'>
+    return f"""
+    <div style='border:1px solid #222;border-radius:6px;padding:12px;background:#0d0d0d;min-height:440px;display:flex;flex-direction:column'>
       <div style='color:{phase_color};font-weight:bold;margin-bottom:8px'>● Phase: {phase}</div>
       <div style='margin-bottom:10px;border-bottom:1px solid #222;padding-bottom:8px'>{log_html}</div>
       {sketch_html}{template_html}
@@ -1510,38 +1908,55 @@ def build_live_html():
       </div>
       <div style='color:#aaa;margin-bottom:8px;font-size:0.85em'>Best Iso: <span style='color:#FF9800'>{best_ray}</span></div>
       <div style='flex:1;overflow-y:auto;border-top:1px solid #222;padding-top:8px'>{ray_trail}</div>
-    </div>"""
+    </div>
+    """
 
 with gr.Blocks(css=CSS, title="Practicality 24.1") as demo:
     gr.Markdown("## ⚗ Practicality 24.1 — Structural Sketch, World Model Prior & Quantum Engine\n`[Gemini Encoder] → [Structural Sketch / SymPy] → [Morphing Ray Solver] → [Gemini Collapser]`")
-    with gr.Row():
-        with gr.Column(scale=2):
+    
+    with gr.Row(elem_classes=["wrap-row"]):
+        with gr.Column(scale=2, min_width=300):
             api_key_input = gr.Textbox(label="Gemini API Key", type="password", placeholder="AIza...", value=DEFAULT_GEMINI_API_KEY, elem_classes=["solver-log"])
             with gr.Tabs():
                 with gr.Tab("Natural Language"):
                     problem_input = gr.Textbox(label="Problem Description", placeholder=PLACEHOLDER_HINT, lines=5, elem_classes=["solver-log"])
                     with gr.Row():
-                        solve_btn = gr.Button("⚗ Solve Natural Language", variant="primary"); clear_btn = gr.Button("Clear")
+                        solve_btn = gr.Button("⚗ Solve Natural Language", variant="primary")
+                        clear_btn = gr.Button("Clear")
+                
                 if HAS_QUANTUM:
                     with gr.Tab("Quantum Circuits (Heisenberg Abstraction)"):
                         q_dropdown = gr.Dropdown(choices=["Bell State", "VQE H2", "QAOA MaxCut"], label="Select Circuit Template", value="Bell State")
                         q_solve_btn = gr.Button("⚛ Run Quantum Solver (Bypass Encoder)", variant="primary")
-        with gr.Column(scale=1):
-            gr.Textbox(value=(f"Compute: {DEVICE.type.upper()}\nAxioms: {len(ALL_AXIOMS)}\nNew: SymPy Derivation Chain Capture\nNew: Quantum BBGKY Cumulant Expansion\nNew: Homotopy Continuation (Morphing Ray)\nNew: Anchor Fix (Gate 2 Sync)"), lines=7, interactive=False, elem_classes=["solver-log"])
-
-    with gr.Row():
-        live_html = gr.HTML(value=build_live_html())
-        answer_box = gr.Textbox(label="Isomorphic Collapse", lines=20, interactive=False, elem_classes=["answer-box"])
+                        
+        with gr.Column(scale=1, min_width=250):
+            gr.Textbox(value=(f"Compute: {DEVICE.type.upper()}\n"
+                              f"Axioms: {len(ALL_AXIOMS)}\n"
+                              f"New: Thread Crash Safety & UI Layout Fix\n"
+                              f"New: Quantum BBGKY Cumulant Expansion\n"
+                              f"New: Homotopy Continuation (Morphing Ray)\n"
+                              f"New: Anchor Fix (Gate 2 Sync)"), 
+                       lines=7, interactive=False, elem_classes=["solver-log"])
+
+    with gr.Row(elem_classes=["wrap-row"]):
+        with gr.Column(scale=1, min_width=300):
+            live_html = gr.HTML(value=build_live_html())
+        with gr.Column(scale=1, min_width=300):
+            answer_box = gr.Textbox(label="Isomorphic Collapse", lines=20, interactive=False, elem_classes=["answer-box"])
 
     def fetch_ui():
         while True:
-            time.sleep(1.0); yield build_live_html(), GLOBAL_SOLVE_STATE["answer"]
+            time.sleep(1.0)
+            yield build_live_html(), GLOBAL_SOLVE_STATE["answer"]
 
     solve_btn.click(fn=trigger_solve, inputs=[problem_input, api_key_input], outputs=None)
     clear_btn.click(fn=lambda: ("", "", ""), inputs=[], outputs=[problem_input, live_html, answer_box])
-    if HAS_QUANTUM: q_solve_btn.click(fn=trigger_quantum_solve, inputs=[q_dropdown, api_key_input], outputs=None)
+    
+    if HAS_QUANTUM: 
+        q_solve_btn.click(fn=trigger_quantum_solve, inputs=[q_dropdown, api_key_input], outputs=None)
+        
     demo.load(fetch_ui, inputs=None, outputs=[live_html, answer_box])
 
 if __name__ == "__main__":
     print(f"[SYSTEM 24.1] Compute: {DEVICE.type.upper()} | Feature Flags: Quantum={HAS_QUANTUM}")
-    demo.launch(server_name="0.0.0.0", server_port=7860, share=False)
+    demo.launch(server_name="0.0.0.0", server_port=7860, share=False)