Update app.py

app.py

@@ -1,19 +1,21 @@
 #!/usr/bin/env python3
 """
-PRACTICALITY UNIFIED SERVER 22.1 — LATEST GEMINI SDK & STRICT BOUNDARY
+PRACTICALITY UNIFIED SERVER 22.2 — GLOBAL STATE + ISOMORPHISM COLLAPSE
 ═══════════════════════════════════════════════════════════════════
 ARCHITECTURE:
   User Text → [GEMINI 3.1 ENCODER] → AXLProblemDef (Strict Math Representation)
-            → [WISDOM LAYER]       → Hypothesis Engine (CreativeSeeder) generates Axiom rays
-                                   → PyTorch Masked Deduction + Oracle solves topology
-                                   → Verification (Gate 1 & Gate 2)
-                                   → [Self-Correcting Feedback Loop if G2 fails]
-            → [GEMINI 3.1 COLLAPSER] → Domain-language explanation
-
-LATEST UPDATES (22.1):
-  - Migrated to the new `google-genai` SDK.
-  - Implemented `gemini-3.1-pro-preview` with `ThinkingConfig` for maximum semantic routing.
-  - Top-level API key configuration for rapid deployment.
+            → Python Compiler        → PSL Mathematical Program
+            → [WISDOM LAYER]         → Hypothesis Engine tests Isomorphic Axiom sequences
+                                     → PyTorch validates via Masked Deduction
+            → [GEMINI 3.1 COLLAPSER] ← Receives: Binding, PSL Program, Winning Axiom Sequence
+                                     → Outputs: Domain-language explanation based on theory
+
+LATEST UPDATES (22.2):
+  - GLOBAL STATE: The solver runs decoupled from the UI. You can close your browser, 
+    return later, refresh the page, and instantly see the live search progress.
+  - BATCH SCALING: CPU/GPU batch size doubled to 24,576.
+  - ISOMORPHISM COLLAPSING: The LLM is explicitly fed the compiled PSL and the 
+    winning structural theory (Axiom ray) to explain *how* the problem was solved.
 """
 
 import os, time, random, math, threading, warnings, queue, json, textwrap
@@ -28,20 +30,20 @@ from sympy.parsing.sympy_parser import parse_expr
 import torch
 import gradio as gr
 
-# ── NEW GOOGLE GENAI SDK ──────────────────────────────────────────
+# Google GenAI SDK
 from google import genai
 from google.genai import types
 
 # ══════════════════════════════════════════════════════════════════
 # AI CONFIGURATION (Set your key here!)
 # ══════════════════════════════════════════════════════════════════
-DEFAULT_GEMINI_API_KEY = os.environ.get("AI_Key", "")
-GEMINI_MODEL = "gemma-4-26b-a4b-it" # "gemini-3-flash-preview" #
+DEFAULT_GEMINI_API_KEY = os.environ.get("GEMINI_API_KEY", "")
+GEMINI_MODEL = "gemini-3.1-pro-preview"
 
 warnings.filterwarnings("ignore")
 USE_GPU = torch.cuda.is_available()
 DEVICE  = torch.device("cuda" if USE_GPU else "cpu")
-print(f"[UNIFIED SERVER] Compute: {DEVICE.type.upper()} | System 22.1 (GenAI SDK + Neuro-Symbolic Boundary)")
+print(f"[UNIFIED SERVER] Compute: {DEVICE.type.upper()} | System 22.2 (Persistent Global State)")
 
 # ══════════════════════════════════════════════════════════════════════
 # SECTION 1: CONSTANTS
@@ -54,7 +56,7 @@ N_MPRT_EXPLORE           = 1000
 PROJECTION_CACHE: Dict   = {}
 
 MAX_TOTAL_RAYS           = 1_500_000
-RAY_BATCH_SIZE           = 12288
+RAY_BATCH_SIZE           = 24576    # DOUBLED: Maximum CPU throughput to feed GPU
 CE_EARN_RATIO            = 0.90
 SCOUT_CE_THRESHOLD       = 0.5
 BRANCH_WIDTH             = 12
@@ -63,7 +65,29 @@ BATON_REGISTRY_THRESHOLD = 2.0
 BATON_REGISTRY_MAX       = 5000
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 2: INTERVAL ARITHMETIC (HC4)
+# SECTION 2: GLOBAL STATE (Persistence Fix)
+# ══════════════════════════════════════════════════════════════════════
+STATE_LOCK = threading.Lock()
+
+# This state persists across browser reloads
+GLOBAL_SOLVE_STATE = {
+    "is_running": False,
+    "logs": [],
+    "answer": "",
+}
+
+def _emit_log(line: str):
+    """Thread-safe log appending."""
+    with STATE_LOCK:
+        GLOBAL_SOLVE_STATE["logs"].append(line)
+
+def _set_answer(text: str):
+    """Thread-safe answer updating."""
+    with STATE_LOCK:
+        GLOBAL_SOLVE_STATE["answer"] = text
+
+# ═══════════════════════��══════════════════════════════════════════════
+# SECTION 3: INTERVAL ARITHMETIC (HC4)
 # ══════════════════════════════════════════════════════════════════════
 class IV:
     __slots__ = ("lo","hi")
@@ -144,7 +168,7 @@ def _global_hc4_tighten_bounds(problem):
             for v in problem.bounds if v in c}
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 3: PSL PARSER & PRE-COMPILATION
+# SECTION 4: PSL PARSER & PRE-COMPILATION
 # ══════════════════════════════════════════════════════════════════════
 @dataclass
 class PSLVar:        name:str; lo:float; hi:float
@@ -273,7 +297,7 @@ class AXLtoPSLCompiler:
 AXL_COMPILER=AXLtoPSLCompiler()
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 4: PROBLEM COMPILATION
+# SECTION 5: PROBLEM COMPILATION
 # ══════════════════════════════════════════════════════════════════════
 @dataclass
 class Constraint:
@@ -460,7 +484,7 @@ def build_base_problem(axl_def:AXLProblemDef) -> Problem:
                    scope_order=ep.scope_order)
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 5: BATCHED MASKED DEDUCTION & ORACLE
+# SECTION 6: BATCHED MASKED DEDUCTION
 # ══════════════════════════════════════════════════════════════════════
 @dataclass
 class L9Certificate:
@@ -545,7 +569,7 @@ def _mprt_sample(problem,work_box,N):
     return {v:float(X[best_idx,i].item()) for i,v in enumerate(var_list)},ce_batch[best_idx].item()
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 6: AXIOMS
+# SECTION 7: AXIOMS
 # ══════════════════════════════════════════════════════════════════════
 class Axiom:
     CONTINUOUS="CONTINUOUS"; DISCRETE="DISCRETE"; QUADRATIC="QUADRATIC"
@@ -578,7 +602,7 @@ def sequence_valid(seq:List[str]) -> bool:
     return True
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 7: SHARED DATACLASSES
+# SECTION 8: SHARED DATACLASSES
 # ══════════════════════════════════════════════════════════════════════
 RAY_TYPES=["seed","branch","tension","scout","recombine","invert","target"]
 
@@ -630,7 +654,7 @@ class StructuralModel:
     resonant_pairs:List[Tuple[str,str]]=field(default_factory=list)
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 8: HYPOTHESIS CONSTRUCTORS
+# SECTION 9: HYPOTHESIS CONSTRUCTORS
 # ══════════════════════════════════════════════════════════════════════
 def _make_hyp(hid,binding,h_type,claim,derivation,pinned,free,conf):
     return Hypothesis(hid=hid,binding=binding,h_type=h_type,claim=claim,
@@ -783,7 +807,7 @@ AXIOM_CONSTRUCTORS={
 }
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 9: CREATIVE SEEDER
+# SECTION 10: CREATIVE SEEDER
 # ══════════════════════════════════════════════════════════════════════
 class CreativeSeeder:
     def target_seeds(self,anchors:List[AXLInvariant]) -> List[AxiomRay]:
@@ -888,7 +912,7 @@ class CreativeSeeder:
 CREATIVE_SEEDER=CreativeSeeder()
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 10: VERIFY LAYER
+# SECTION 11: VERIFY LAYER
 # ══════════════════════════════════════════════════════════════════════
 def _verify(binding:Dict[str,float],base_problem:Problem,
             anchors:List[AXLInvariant]) -> Tuple[bool,bool,Dict[str,Tuple[float,bool]],float]:
@@ -910,7 +934,7 @@ def _verify(binding:Dict[str,float],base_problem:Problem,
     return g1_pass,g2_pass,g2,round(g1_ce,6)
 
 # ══════════════════════════════════════════════════════════════════════
-# SECTION 11: SEQUENCE RAY TRACER
+# SECTION 12: SEQUENCE RAY TRACER
 # ══════════════════════════════════════════════════════════════════════
 class SequenceRayTracer:
     def trace(self,axl_def:AXLProblemDef,base_problem:Problem):
@@ -941,7 +965,7 @@ class SequenceRayTracer:
         model=StructuralModel(best_binding,best_ce)
         allosteric_counts={"isolated":0,"relational":0,"systemic":0}
 
-        while total_fired<MAX_TOTAL_RAYS:
+        while total_fired<MAX_TOTAL_RAYS and GLOBAL_SOLVE_STATE["is_running"]:
             batch_rays:List[AxiomRay]=[]
             for _ in range(RAY_BATCH_SIZE):
                 start_idx=q_idx
@@ -1047,13 +1071,18 @@ class SequenceRayTracer:
 
             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))
+            
+            # Periodically heartbeat logs
+            if total_fired % (RAY_BATCH_SIZE * 5) == 0:
+                _emit_log(f"  · searching ({total_fired:,} rays fired, best CE={best_ce:.4f})…")
+
             if solved: break
 
         return best_binding,best_ce,hero_traces,total_fired,allosteric_counts
 
 
 # ══════════════════════════════════════════════════════════════════
-# SECTION 12: LLM BRIDGE (GOOGLE GENAI 3.1)
+# SECTION 13: LLM BRIDGE (GOOGLE GENAI 3.1)
 # ══════════════════════════════════════════════════════════════════
 
 ENCODER_SYSTEM_PROMPT = """You are the Encoder for the Practicality Wisdom Layer — a neuro-symbolic
@@ -1122,7 +1151,37 @@ CONSTRAINTS & ANCHORS:
   • Anchors are the verification conditions. What MUST be true to accept the solution?
 
 ══════════════════════════════════════════════════════════════════
-PART 3: FAILURE HANDLING
+PART 3: EXAMPLES
+══════════════════════════════════════════════════════════════════
+
+EXAMPLE 1: Chemical Equilibrium (A + B ↔ C, Kc = 4)
+User: "Find equilibrium concentrations for A+B↔C with Kc=4,
+       starting with [A]=[B]=1 mol/L and [C]=0"
+
+Output:
+{
+  "name": "ChemEquilibrium",
+  "description": "A+B↔C equilibrium with Kc=4, initial [A]=[B]=1, [C]=0",
+  "variables": [
+    {"name": "ca", "lo": 0.0},
+    {"name": "cb", "lo": 0.0},
+    {"name": "cc", "lo": 0.0}
+  ],
+  "constraints": [
+    {"kind": "CONSERVE", "expr": "ca + cc - 1.0"},
+    {"kind": "CONSERVE", "expr": "cb + cc - 1.0"},
+    {"kind": "EQ",       "expr": "4*ca*cb - cc", "weight": 5.0}
+  ],
+  "anchors": [
+    {"name": "atom_balance_A",  "expr": "ca + cc - 1.0",  "tolerance": 0.001, "mode": "eq"},
+    {"name": "atom_balance_B",  "expr": "cb + cc - 1.0",  "tolerance": 0.001, "mode": "eq"},
+    {"name": "kc_equilibrium",  "expr": "4*ca*cb - cc",   "tolerance": 0.001, "mode": "eq"}
+  ],
+  "observations": {}
+}
+
+══════════════════════════════════════════════════════════════════
+PART 4: FAILURE HANDLING
 ══════════════════════════════════════════════════════════════════
 
 If a previous solve attempt is included in the user message showing
@@ -1135,44 +1194,37 @@ Common fixes:
 Output ONLY the JSON. No preamble.
 """
 
-COLLAPSER_SYSTEM_PROMPT = """You are the Collapser for the Practicality Wisdom Layer. You receive
-a JSON object containing:
+COLLAPSER_SYSTEM_PROMPT = """You are the Collapser for the Practicality Wisdom Layer. 
+The system has derived a structural isomorphism (an Axiom Sequence) to collapse 
+the problem constraints you encoded into a verified numerical solution.
+
+Your job is to explain the solution using this structural thinking.
+
+You receive a JSON object containing:
   • The original natural language problem
-  • The problem name and description
   • Whether the solver succeeded (solved/partial/unsolved)
   • The verified variable binding (the numerical solution)
-  • Gate 1 result: global constraint energy (mathematical validity)
-  • Gate 2 results: named invariant checks (domain correctness)
-  • The best axiom ray sequence that found the solution
-  • Total rays fired
-
-Your job is to translate this back into clear, domain-appropriate
-natural language that a human expert in the problem domain would
-recognize as correct and useful.
+  • The compiled PSL Program Text (The exact mathematical constraints the engine proved)
+  • The ISOMORPHISM HYPOTHESIS (best_ray_sequence): The geometric theory that unlocked it.
 
 ══════════════════════════════════════════════════════════════════
 TONE AND FORMAT RULES
 ══════════════════════════════════════════════════════════════════
-• Write for a domain expert, not a general audience
-• Use domain-appropriate variable names and units if discernible
+• Write for a domain expert, not a general audience.
 • Lead with the status: SOLVED / PARTIAL / UNSOLVED
-• Report the binding values in the order they appear in the problem
-• For each Gate 2 invariant:
-    - If passed: briefly confirm what physical condition is satisfied
-    - If failed: explain specifically what condition was NOT met
-      and by how much (the numerical value is provided)
-• Keep it under 250 words
-• End with the axiom sequence that found the solution, formatted
-  as a one-line note
+• Provide the final binding values with domain-appropriate context.
+• EXPLAIN THE ISOMORPHISM: Explicitly explain *how* the `isomorphism_hypothesis` 
+  (the Axiom sequence like SYMMETRIC→MONOTONE) structurally describes the 
+  `psl_program_text`. Do not just list the axioms; explain why the problem's 
+  topology fits that geometry.
+• Keep the entire output under 300 words.
 """
 
 def encode_problem_to_axl(problem_text: str, api_key: str) -> AXLProblemDef:
-    """Uses Google GenAI to slot-fill the text into the AXL structural JSON."""
     if not api_key:
-        raise ValueError("Gemini API Key is missing. Please provide it in the UI or set it globally.")
+        raise ValueError("Gemini API Key is missing.")
     
     client = genai.Client(api_key=api_key)
-    
     config = types.GenerateContentConfig(
         system_instruction=[types.Part.from_text(text=ENCODER_SYSTEM_PROMPT)],
         response_mime_type="application/json",
@@ -1181,19 +1233,16 @@ def encode_problem_to_axl(problem_text: str, api_key: str) -> AXLProblemDef:
     
     response = client.models.generate_content(
         model=GEMINI_MODEL,
-        contents=problem_text,
+        contents=[types.Content(role="user", parts=[types.Part.from_text(text=problem_text)])],
         config=config,
     )
-    
     return _parse_axl_json(response.text)
 
 def _parse_axl_json(raw_json: str) -> AXLProblemDef:
-    """Parses Gemini JSON output into the strict AXL structural definition."""
     text = raw_json.strip()
     if text.startswith("```"):
         text = text.split("```")[1]
-        if text.startswith("json"):
-            text = text[4:]
+        if text.startswith("json"): text = text[4:]
     text = text.strip().rstrip("`").strip()
 
     d = json.loads(text)
@@ -1217,7 +1266,7 @@ def _parse_axl_json(raw_json: str) -> AXLProblemDef:
     return AXLProblemDef(
         name=d["name"],
         description=d.get("description", ""),
-        axioms=set(), # Engine owns Axioms, not the LLM
+        axioms=set(), # Engine owns Axioms
         variables=variables,
         constraints=d.get("constraints", []),
         scopes=d.get("scopes", []),
@@ -1228,6 +1277,7 @@ def _parse_axl_json(raw_json: str) -> AXLProblemDef:
 def collapse_solution(
     problem_text: str,
     axl_def: AXLProblemDef,
+    psl_text: str,
     binding: Dict[str, float],
     g1_pass: bool,
     g2_pass: bool,
@@ -1236,22 +1286,17 @@ def collapse_solution(
     total_fired: int,
     api_key: str
 ) -> str:
-    """Uses Google GenAI with high-level thinking to collapse PyTorch findings to Natural Language."""
-    if not api_key:
-        return "ERROR: Gemini API Key required for semantic collapsing."
+    if not api_key: return "ERROR: Gemini API Key required."
         
     client = genai.Client(api_key=api_key)
     
     payload = {
         "original_problem": problem_text,
-        "problem_name":     axl_def.name,
         "solved":           g1_pass and g2_pass,
-        "gate1_pass":       g1_pass,
-        "gate2_pass":       g2_pass,
         "binding":          {k: round(v, 6) for k, v in binding.items()},
+        "psl_program_text": psl_text,
+        "isomorphism_hypothesis": best_ray,
         "invariant_results":invariant_results,
-        "best_ray_sequence":best_ray,
-        "rays_fired":       total_fired,
     }
     
     config = types.GenerateContentConfig(
@@ -1262,44 +1307,41 @@ def collapse_solution(
     
     response = client.models.generate_content(
         model=GEMINI_MODEL,
-        contents=json.dumps(payload, indent=2),
+        contents=[types.Content(role="user", parts=[types.Part.from_text(text=json.dumps(payload, indent=2))])],
         config=config,
     )
-    
     return response.text
 
 # ══════════════════════════════════════════════════════════════════
-# SECTION 13: STREAMING SOLVER RUNNER WITH FEEDBACK LOOP
+# SECTION 14: GLOBAL SOLVE TASK (Background Thread)
 # ══════════════════════════════════════════════════════════════════
 
-def run_solve_streaming(original_problem_text: str, api_key: str):
+def global_solve_task(original_problem_text: str, api_key: str):
     """
-    Generator that wires Encode → Compile → PyTorch Solve → Verify → Collapse.
-    Includes the self-correcting feedback loop if Gate 2 (Invariants) fails.
+    Runs the full neuro-symbolic pipeline in a background thread, 
+    updating the GLOBAL_SOLVE_STATE dictionary for the UI to poll.
     """
-    log_lines: List[str] = []
-    answer_text = ""
-    MAX_ATTEMPTS = 3
-
-    def emit(line: str):
-        log_lines.append(line)
-        return "\n".join(log_lines), answer_text
+    GLOBAL_SOLVE_STATE["is_running"] = True
+    GLOBAL_SOLVE_STATE["logs"] = []
+    GLOBAL_SOLVE_STATE["answer"] = ""
 
+    MAX_ATTEMPTS = 3
     current_text = original_problem_text
     used_key = api_key or DEFAULT_GEMINI_API_KEY
 
     for attempt in range(1, MAX_ATTEMPTS + 1):
-        yield emit(f"🔍 **Encoding problem (Attempt {attempt}/{MAX_ATTEMPTS})…**\n")
+        _emit_log(f"🔍 **Encoding problem (Attempt {attempt}/{MAX_ATTEMPTS})…**\n")
         t0 = time.time()
         
         try:
             axl_def = encode_problem_to_axl(current_text, used_key)
         except Exception as e:
-            yield emit(f"✗ Encoding failed: {e}\n")
+            _emit_log(f"✗ Encoding failed: {e}\n")
+            GLOBAL_SOLVE_STATE["is_running"] = False
             return
 
         enc_ms = round((time.time() - t0) * 1000)
-        yield emit(
+        _emit_log(
             f"✓ **Encoded** as `{axl_def.name}` ({enc_ms} ms)\n"
             f"  Variables: `{', '.join(v['name'] for v in axl_def.variables)}`\n"
             f"  Anchors: {len(axl_def.anchors)}\n\n"
@@ -1307,49 +1349,32 @@ def run_solve_streaming(original_problem_text: str, api_key: str):
         )
 
         try:
+            psl_text = AXL_COMPILER.compile(axl_def)
             base_prob = build_base_problem(axl_def)
         except Exception as e:
-            yield emit(f"✗ Compilation failed: {e}\n")
+            _emit_log(f"✗ Compilation failed: {e}\n")
+            GLOBAL_SOLVE_STATE["is_running"] = False
             return
 
-        yield emit(
+        _emit_log(
             f"✓ **Compiled**: {len(base_prob.variables)} vars, "
             f"{len(base_prob.compiled_constraints)} constraints\n"
-            f"  Bilinear pairs: {len(base_prob.bilinear_pairs)}\n"
-            f"  Monotone targets: {len(base_prob.monotone_targets)}\n\n"
             f"🚀 **Running wisdom layer (PyTorch Search)…**\n"
         )
 
-        result_q: queue.Queue = queue.Queue()
-
-        def _worker():
-            try:
-                tracer = SequenceRayTracer()
-                binding, ce, traces, total_fired, allosteric = tracer.trace(axl_def, base_prob)
-                result_q.put(("ok", binding, ce, traces, total_fired, allosteric))
-            except Exception as e:
-                result_q.put(("err", str(e)))
-
-        worker_thread = threading.Thread(target=_worker, daemon=True)
-        worker_thread.start()
-
-        dots = 0
-        while worker_thread.is_alive():
-            worker_thread.join(timeout=3.0)
-            if worker_thread.is_alive():
-                dots += 1
-                yield emit(f"  ·{'·' * dots} still searching ({dots * 3}s)…\n")
-
-        if result_q.empty():
-            yield emit("✗ Solver returned no result.\n")
+        try:
+            tracer = SequenceRayTracer()
+            binding, ce, traces, total_fired, allosteric = tracer.trace(axl_def, base_prob)
+        except Exception as e:
+            _emit_log(f"✗ Solver error: {e}\n")
+            GLOBAL_SOLVE_STATE["is_running"] = False
             return
 
-        result = result_q.get()
-        if result[0] == "err":
-            yield emit(f"✗ Solver error: {result[1]}\n")
+        if total_fired == 0:
+            _emit_log("✗ Solver returned no result.\n")
+            GLOBAL_SOLVE_STATE["is_running"] = False
             return
 
-        _, binding, ce, traces, total_fired, allosteric = result
         survived = [t for t in traces if t.survived]
         best_t   = min(survived, key=lambda t: t.ce_after, default=None)
 
@@ -1376,38 +1401,48 @@ def run_solve_streaming(original_problem_text: str, api_key: str):
         g2_detail  = " | ".join(f"{'✓' if ok else '✗'} {k}" for k, (_, ok) in inv_results.items())
         best_ray   = best_t.ray_name if best_t else "—"
 
-        yield emit(
+        _emit_log(
             f"\n{solved_str}\n"
             f"  CE = {ce:.6f} | Gate 1: {'✓' if g1_pass else '✗'} | Gate 2: {'✓' if g2_pass else '✗'}\n"
             f"  {g2_detail}\n"
-            f"  Best ray: `{best_ray}`\n"
+            f"  Isomorphism: `{best_ray}`\n"
             f"  Rays fired: {total_fired:,} | Survived: {len(survived)}\n"
             f"  Allosteric: isolated {allosteric.get('isolated',0):,} | relational {allosteric.get('relational',0):,} | systemic {allosteric.get('systemic',0):,}\n\n"
         )
 
-        # ── Self-Correcting Feedback Loop (Gate 2 Failure) ───────────────
         if not g2_pass and attempt < MAX_ATTEMPTS:
             failed_invs = {k: v for k, (v, ok) in inv_results.items() if not ok}
             current_text = original_problem_text + f"\n\nPREVIOUS ATTEMPT FAILED:\nGate 2 invariants that did not pass:\n{json.dumps(failed_invs, indent=2)}\n\nPlease revise the constraint encoding to better capture these conditions."
-            yield emit(f"⚠ **Gate 2 Failed.** Retrying ({len(failed_invs)} invariants failed) with structural feedback...\n\n---\n")
+            _emit_log(f"⚠ **Gate 2 Failed.** Retrying ({len(failed_invs)} invariants failed) with structural feedback...\n\n---\n")
             continue 
             
-        yield emit(f"🔤 **Collapsing to domain language…**\n")
+        _emit_log(f"🔤 **Collapsing Isomorphism to Domain Language…**\n")
         try:
             answer_text = collapse_solution(
-                original_problem_text, axl_def, binding,
+                original_problem_text, axl_def, psl_text, binding,
                 g1_pass, g2_pass, inv_results,
                 best_ray, total_fired, used_key
             )
-            yield emit("✓ Done.\n")
+            _set_answer(answer_text)
+            _emit_log("✓ Done.\n")
         except Exception as e:
-            answer_text = f"Error during collapsing: {e}"
-            yield emit("✗ Collapsing failed.\n")
+            _set_answer(f"Error during collapsing: {e}")
+            _emit_log("✗ Collapsing failed.\n")
             
         break 
 
+    GLOBAL_SOLVE_STATE["is_running"] = False
+
+
+def trigger_solve(problem_text: str, api_key: str):
+    if GLOBAL_SOLVE_STATE["is_running"]:
+        return
+    if not problem_text.strip():
+        return
+    threading.Thread(target=global_solve_task, args=(problem_text, api_key), daemon=True).start()
+
 # ══════════════════════════════════════════════════════════════════
-# SECTION 14: GRADIO INTERFACE
+# SECTION 15: GRADIO INTERFACE (Polling Global State)
 # ══════════════════════════════════════════════════════════════════
 
 CSS = """
@@ -1466,30 +1501,31 @@ with gr.Blocks(css=CSS, title="Practicality Unified Server") as demo:
 
     with gr.Row():
         solver_log = gr.Textbox(
-            label="Solver Log",
+            label="Solver Log (Live State)",
             lines=18,
             interactive=False,
             elem_classes=["solver-log"],
         )
         answer_box = gr.Textbox(
-            label="Answer",
+            label="Isomorphic Collapse",
             lines=18,
             interactive=False,
             elem_classes=["answer-box"],
         )
 
-    def _solve(problem_text: str, api_key: str):
-        if not problem_text.strip():
-            yield "No problem text provided.", ""
-            return
-        for log_chunk, answer_chunk in run_solve_streaming(problem_text, api_key):
-            yield log_chunk, answer_chunk
+    # UI Polling Loop
+    def fetch_ui_state():
+        while True:
+            time.sleep(1.0)
+            with STATE_LOCK:
+                logs = "".join(GLOBAL_SOLVE_STATE["logs"])
+                ans = GLOBAL_SOLVE_STATE["answer"]
+            yield logs, ans
 
     solve_btn.click(
-        fn=_solve,
+        fn=trigger_solve,
         inputs=[problem_input, api_key_input],
-        outputs=[solver_log, answer_box],
-        show_progress=False,
+        outputs=None, # Fire and forget, UI loop handles updates
     )
 
     clear_btn.click(
@@ -1498,14 +1534,14 @@ with gr.Blocks(css=CSS, title="Practicality Unified Server") as demo:
         outputs=[problem_input, solver_log, answer_box],
     )
 
+    demo.load(fetch_ui_state, inputs=None, outputs=[solver_log, answer_box])
+
     gr.Markdown(
-        "Built with Gradio · Practicality 22.1 · Strict Neuro-Symbolic Boundary",
+        "Built with Gradio · Practicality 22.2 · Global State Persistence + Structural Collapsing",
         elem_classes=["status-bar"]
     )
 
-demo.queue()
-
 if __name__ == "__main__":
     print(f"[UNIFIED SERVER] Compute: {DEVICE.type.upper()}")
-    print(f"[UNIFIED SERVER] System 22.1: GenAI SDK wired. Model: {GEMINI_MODEL}")
+    print(f"[UNIFIED SERVER] System 22.2: GenAI SDK wired. Model: {GEMINI_MODEL}")
     demo.launch(server_name="0.0.0.0", server_port=7860, share=False)