Spaces:
Sleeping
Sleeping
Update app.py
Browse files
app.py
CHANGED
|
@@ -1,21 +1,43 @@
|
|
| 1 |
#!/usr/bin/env python3
|
| 2 |
"""
|
| 3 |
-
PRACTICALITY SYSTEM
|
| 4 |
═══════════════════════════════════════════════════════════════════
|
| 5 |
-
|
| 6 |
-
|
| 7 |
-
|
| 8 |
-
|
| 9 |
-
|
| 10 |
-
|
| 11 |
-
|
| 12 |
-
|
| 13 |
-
|
| 14 |
-
|
| 15 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 16 |
"""
|
| 17 |
|
| 18 |
-
import time, random, math, threading, asyncio, warnings
|
| 19 |
from functools import reduce
|
| 20 |
from typing import Optional, Callable, List, Dict, Tuple, Any, Set
|
| 21 |
from dataclasses import dataclass, field
|
|
@@ -34,7 +56,7 @@ import uvicorn
|
|
| 34 |
warnings.filterwarnings("ignore")
|
| 35 |
USE_GPU = torch.cuda.is_available()
|
| 36 |
DEVICE = torch.device("cuda" if USE_GPU else "cpu")
|
| 37 |
-
print(f"[SYSTEM
|
| 38 |
|
| 39 |
# ══════════════════════════════════════════════════════════════════════
|
| 40 |
# SECTION 1: CONSTANTS
|
|
@@ -47,12 +69,12 @@ L9_CONTRIB_THRESHOLD = 1e-8
|
|
| 47 |
HUB_RESIDUAL_MULT = 2.0
|
| 48 |
HUB_DEGREE_RATIO = 0.6
|
| 49 |
MAX_HYPS_PER_AXIOM = 4
|
| 50 |
-
BRANCH_DEPTH = 3
|
| 51 |
MANIFOLD_STEPS = [0.05, 0.2, -0.05, -0.2, 0.5, -0.5]
|
| 52 |
N_MPRT_EXPLORE = 20000 if USE_GPU else 3000
|
| 53 |
POLISH_STEPS = 40
|
| 54 |
ADAM_STEPS = 30
|
| 55 |
PROJECTION_CACHE: Dict = {}
|
|
|
|
| 56 |
|
| 57 |
# ══════════════════════════════════════════════════════════════════════
|
| 58 |
# SECTION 2: INTERVAL ARITHMETIC
|
|
@@ -217,22 +239,21 @@ def expand_psl(prog:PSLProgram) -> ExpandedProblem:
|
|
| 217 |
if name not in bounds: variables.append(name); bounds[name]=(lo,hi)
|
| 218 |
if scope!="root" and name not in scope_vars[scope]: scope_vars[scope].append(name)
|
| 219 |
def add_con(kind,expr,direction,scope="root",weight=1.0,branches=None):
|
| 220 |
-
idx=len(constraints)
|
| 221 |
constraints.append(Constraint(kind,expr,direction,weight,scope,branches or []))
|
| 222 |
-
scope_groups[scope].append(
|
| 223 |
try:
|
| 224 |
syms={v:sp.Symbol(v) for v in variables}
|
| 225 |
-
if kind=
|
| 226 |
-
|
| 227 |
-
parsed=parse_expr(b_str,local_dict=syms)
|
| 228 |
-
for v in variables:
|
| 229 |
-
if sp.Symbol(v) in parsed.free_symbols and scope!="root" and v not in scope_vars[scope]:
|
| 230 |
-
scope_vars[scope].append(v)
|
| 231 |
-
else:
|
| 232 |
-
parsed=parse_expr(expr,local_dict=syms)
|
| 233 |
for v in variables:
|
| 234 |
if sp.Symbol(v) in parsed.free_symbols and scope!="root" and v not in scope_vars[scope]:
|
| 235 |
scope_vars[scope].append(v)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 236 |
except: pass
|
| 237 |
for v in prog.vars: add_var(v.name,v.lo,v.hi)
|
| 238 |
for c in prog.constraints:
|
|
@@ -252,8 +273,7 @@ def expand_psl(prog:PSLProgram) -> ExpandedProblem:
|
|
| 252 |
# ══════════════════════════════════════════════════════════════════════
|
| 253 |
@dataclass
|
| 254 |
class AXLInvariant:
|
| 255 |
-
name:str; expr:str; tolerance:float=VERIFY_G2_TOLERANCE
|
| 256 |
-
mode:str="eq" # "eq": |expr|<tol | "geq": expr>=-tol | "leq": expr<=tol
|
| 257 |
|
| 258 |
@dataclass
|
| 259 |
class AXLProblemDef:
|
|
@@ -398,7 +418,7 @@ class Problem:
|
|
| 398 |
val=float(mc.fast_pt(*[b.get(v,0.0) for v in mc.syms_used]))
|
| 399 |
if mc.kind=="equality": total+=abs(val)*mc.weight
|
| 400 |
elif mc.direction=="geq": total+=max(0.0,-val)*mc.weight
|
| 401 |
-
else: total+=max(0.0,
|
| 402 |
except: total+=1.0
|
| 403 |
for v,(lo,hi) in self.bounds.items():
|
| 404 |
bv=b.get(v,0.0); total+=max(0.0,lo-bv)+max(0.0,bv-hi)
|
|
@@ -466,7 +486,7 @@ class Problem:
|
|
| 466 |
if not isinstance(val,np.ndarray): val=np.full(N,float(val),dtype=np.float32)
|
| 467 |
if mc.kind=="equality": total+=np.abs(val)*mc.weight
|
| 468 |
elif mc.direction=="geq": total+=np.maximum(0.0,-val)*mc.weight
|
| 469 |
-
else: total+=np.maximum(0.0,
|
| 470 |
except: total+=1.0
|
| 471 |
for i,v in enumerate(var_order):
|
| 472 |
lo,hi=self.bounds[v]; col=b_matrix[:,i]
|
|
@@ -474,7 +494,7 @@ class Problem:
|
|
| 474 |
return total
|
| 475 |
|
| 476 |
# ══════════════════════════════════════════════════════════════════════
|
| 477 |
-
# SECTION 6: VERIFY LAYER
|
| 478 |
# ══════════════════════════════════════════════════════════════════════
|
| 479 |
@dataclass
|
| 480 |
class VerifyResult:
|
|
@@ -484,7 +504,7 @@ class VerifyResult:
|
|
| 484 |
failed_gates:List[str]=field(default_factory=list)
|
| 485 |
|
| 486 |
class VerifyLayer:
|
| 487 |
-
def run(self,binding
|
| 488 |
g1_ce=base_problem.constraint_energy(binding)
|
| 489 |
g1_pass=g1_ce<VERIFY_G1_THRESHOLD
|
| 490 |
g2={}
|
|
@@ -494,11 +514,10 @@ class VerifyLayer:
|
|
| 494 |
expr=parse_expr(inv.expr,local_dict=syms)
|
| 495 |
func=sp.lambdify(list(expr.free_symbols),expr,modules="math")
|
| 496 |
args=[binding.get(str(s),0.0) for s in expr.free_symbols]
|
| 497 |
-
val=float(func(*args))
|
| 498 |
-
err=abs(val)
|
| 499 |
if inv.mode=="eq": passed=err<inv.tolerance
|
| 500 |
-
elif inv.mode=="geq": passed=val>=-inv.tolerance
|
| 501 |
-
elif inv.mode=="leq": passed=val<=inv.tolerance
|
| 502 |
else: passed=err<inv.tolerance
|
| 503 |
g2[inv.name]=(round(val,6),passed)
|
| 504 |
except: g2[inv.name]=(999.0,False)
|
|
@@ -542,7 +561,7 @@ AXIOM_ABBR={
|
|
| 542 |
Axiom.IMPLICATION:"IMP",Axiom.NEGATION:"NEG",Axiom.COMPOSITE:"CMP",
|
| 543 |
Axiom.HOLISM:"HOL",Axiom.PARSIMONY:"PAR",Axiom.DUALITY:"DUA",
|
| 544 |
}
|
| 545 |
-
ADJACENT_CONTRADICTIONS=[
|
| 546 |
(Axiom.DISCRETE,Axiom.CONTINUOUS),(Axiom.INJECTIVE,Axiom.SURJECTIVE),
|
| 547 |
(Axiom.ORDERED,Axiom.SYMMETRIC),(Axiom.ATOMIC,Axiom.COMPOSITE),
|
| 548 |
(Axiom.CONSERVED,Axiom.MUTABLE),(Axiom.PARSIMONY,Axiom.ENTROPY),
|
|
@@ -551,7 +570,7 @@ ADJACENT_CONTRADICTIONS=[
|
|
| 551 |
]
|
| 552 |
_CONTRA_SET={frozenset(p) for p in ADJACENT_CONTRADICTIONS}
|
| 553 |
|
| 554 |
-
def sequence_valid(seq:List[str]) -> bool:
|
| 555 |
for i in range(len(seq)-1):
|
| 556 |
if frozenset([seq[i],seq[i+1]]) in _CONTRA_SET: return False
|
| 557 |
return True
|
|
@@ -559,6 +578,19 @@ def sequence_valid(seq:List[str]) -> bool:
|
|
| 559 |
# ══════════════════════════════════════════════════════════════════════
|
| 560 |
# SECTION 8: SHARED DATACLASSES
|
| 561 |
# ══════════════════════════════════════════════════════════════════════
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 562 |
@dataclass
|
| 563 |
class Hypothesis:
|
| 564 |
hid:str; binding:Dict[str,float]; h_type:str; claim:str
|
|
@@ -567,36 +599,56 @@ class Hypothesis:
|
|
| 567 |
|
| 568 |
@dataclass
|
| 569 |
class Baton:
|
|
|
|
| 570 |
binding:Dict[str,float]; ce:float
|
| 571 |
ray_id:str=""; depth:int=0
|
| 572 |
l7:Optional[Any]=None; l9:Optional[Any]=None
|
| 573 |
|
| 574 |
@dataclass
|
| 575 |
class AxiomRay:
|
| 576 |
-
|
| 577 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 578 |
@property
|
| 579 |
def name(self) -> str:
|
| 580 |
return "→".join(AXIOM_ABBR.get(a,a[:3]) for a in self.sequence)
|
| 581 |
-
|
| 582 |
-
|
|
|
|
| 583 |
if sequence_valid(new_seq):
|
| 584 |
-
return AxiomRay(
|
| 585 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 586 |
return None
|
| 587 |
|
| 588 |
@dataclass
|
| 589 |
class HypothesisTrace:
|
| 590 |
-
hid:str; round_idx:int; ray_name:str; action:str
|
| 591 |
ce_before:float; ce_after:float
|
| 592 |
verify:Optional[VerifyResult]; survived:bool; elapsed_ms:float
|
| 593 |
depth:int=0; parent_id:str=""
|
| 594 |
|
| 595 |
@dataclass
|
| 596 |
class StructuralModel:
|
| 597 |
-
best_binding:Dict[str,float]
|
| 598 |
-
|
| 599 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
| 600 |
|
| 601 |
# ══════════════════════════════════════════════════════════════════════
|
| 602 |
# SECTION 9: ORACLES
|
|
@@ -787,7 +839,7 @@ def _test_hypothesis(problem,hyp):
|
|
| 787 |
return best_b,best_ce
|
| 788 |
|
| 789 |
# ══════════════════════════════════════════════════════════════════════
|
| 790 |
-
# SECTION 11: HYPOTHESIS CONSTRUCTORS (27 axioms
|
| 791 |
# ══════════════════════════════════════════════════════════════════════
|
| 792 |
def _proj_val(mc,v,b):
|
| 793 |
if v not in mc.projections: return None
|
|
@@ -867,8 +919,7 @@ def _hyp_quadratic(problem,baton,all_batons,model):
|
|
| 867 |
def _hyp_bilinear(problem,baton,all_batons,model):
|
| 868 |
hyps=[]; b=dict(baton.binding)
|
| 869 |
for mc in problem.compiled_constraints:
|
| 870 |
-
if not mc.parsed: continue
|
| 871 |
-
if not mc.parsed.is_Add: continue
|
| 872 |
for term in mc.parsed.args:
|
| 873 |
if not term.is_Mul: continue
|
| 874 |
syms_in=[str(s) for s in term.free_symbols if str(s) in problem.variables]
|
|
@@ -887,8 +938,7 @@ def _hyp_bilinear(problem,baton,all_batons,model):
|
|
| 887 |
def _hyp_metric(problem,baton,all_batons,model):
|
| 888 |
hyps=[]; b=dict(baton.binding)
|
| 889 |
for mc in problem.compiled_constraints:
|
| 890 |
-
if mc.kind!="equality" or not mc.parsed: continue
|
| 891 |
-
if not mc.parsed.is_Add: continue
|
| 892 |
sq_terms=[t for t in mc.parsed.args if t.is_Pow and t.args[1]==2]
|
| 893 |
if len(sq_terms)<2: continue
|
| 894 |
vars_in=[str(s) for s in mc.parsed.free_symbols if str(s) in problem.variables]
|
|
@@ -924,9 +974,8 @@ def _hyp_ordered(problem,baton,all_batons,model):
|
|
| 924 |
b=dict(baton.binding); nb=dict(b)
|
| 925 |
ord_mcs=[mc for mc in problem.compiled_constraints if mc.kind=="inequality" and len(mc.syms_used)==2]
|
| 926 |
for mc in ord_mcs:
|
| 927 |
-
if len(mc.syms_used)<2: continue
|
| 928 |
vi,vj=mc.syms_used[0],mc.syms_used[1]
|
| 929 |
-
lo_i,
|
| 930 |
if mc.direction=="geq" and nb.get(vi,0)<nb.get(vj,0):
|
| 931 |
mid=(nb[vi]+nb[vj])/2; nb[vi]=max(lo_i,mid); nb[vj]=min(hi_j,mid)
|
| 932 |
return [_make_hyp(f"ord_{hash(str(nb))%9999}",nb,"ordered","OrderBal",["ordered"],{},list(problem.variables),0.67)]
|
|
@@ -1083,7 +1132,7 @@ def _hyp_transitive(problem,baton,all_batons,model):
|
|
| 1083 |
changed=False; iters+=1
|
| 1084 |
for mc in problem.compiled_constraints:
|
| 1085 |
if mc.kind!="equality" or not mc.projections: continue
|
| 1086 |
-
for v
|
| 1087 |
val=_proj_val(mc,v,nb)
|
| 1088 |
if val is None: continue
|
| 1089 |
lo,hi=problem.bounds.get(v,(-1e18,1e18))
|
|
@@ -1205,56 +1254,219 @@ def _hyp_duality(problem,baton,all_batons,model):
|
|
| 1205 |
return hyps
|
| 1206 |
|
| 1207 |
AXIOM_CONSTRUCTORS:Dict[str,Callable]={
|
| 1208 |
-
Axiom.CONTINUOUS:_hyp_continuous,Axiom.DISCRETE:_hyp_discrete,
|
| 1209 |
-
Axiom.QUADRATIC:_hyp_quadratic,Axiom.BILINEAR:_hyp_bilinear,
|
| 1210 |
-
Axiom.METRIC:_hyp_metric,Axiom.SYMMETRIC:_hyp_symmetric,
|
| 1211 |
-
Axiom.ORDERED:_hyp_ordered,Axiom.MONOTONE:_hyp_monotone,
|
| 1212 |
-
Axiom.
|
|
|
|
| 1213 |
Axiom.EQUILIBRIUM:_hyp_equilibrium,Axiom.SUPERPOSITION:_hyp_superposition,
|
| 1214 |
-
Axiom.LOCALITY:_hyp_locality,Axiom.EXTREMAL:_hyp_extremal,
|
| 1215 |
-
Axiom.
|
| 1216 |
-
Axiom.
|
| 1217 |
-
Axiom.
|
| 1218 |
-
Axiom.
|
| 1219 |
-
Axiom.
|
|
|
|
| 1220 |
}
|
| 1221 |
|
| 1222 |
# ══════════════════════════════════════════════════════════════════════
|
| 1223 |
-
# SECTION 12: SEQUENCE HYPOTHESIS GENERATOR
|
|
|
|
|
|
|
| 1224 |
# ══════════════════════════════════════════════════════════════════════
|
| 1225 |
class SequenceHypothesisGenerator:
|
| 1226 |
-
def generate(self,sequence:List[str],problem:Problem,
|
| 1227 |
-
baton:Baton,all_batons:List[Baton],
|
|
|
|
| 1228 |
accumulated:List[Hypothesis]=[]; current=baton
|
|
|
|
|
|
|
| 1229 |
for i,axiom in enumerate(sequence):
|
| 1230 |
constructor=AXIOM_CONSTRUCTORS.get(axiom)
|
| 1231 |
if not constructor: continue
|
|
|
|
| 1232 |
if current.l7 is None:
|
| 1233 |
active=[s for s in problem.scope_order if s!="root" and problem.scope_vars.get(s)]
|
| 1234 |
current.l7=TOPOLOGY_ORACLE.evaluate(problem,active)
|
| 1235 |
if current.l9 is None:
|
| 1236 |
hubs=current.l7.hub_vars if current.l7 else []
|
| 1237 |
current.l9=RESIDUAL_ORACLE.evaluate(current.binding,problem,hubs)
|
|
|
|
| 1238 |
new_hyps=constructor(problem,current,all_batons,model)
|
| 1239 |
accumulated.extend(new_hyps)
|
|
|
|
| 1240 |
best_ce=current.ce; best_b=current.binding
|
| 1241 |
for hyp in sorted(new_hyps,key=lambda h:-h.confidence)[:MAX_HYPS_PER_AXIOM]:
|
| 1242 |
if hyp.hid in model.failure_patterns: continue
|
| 1243 |
tb,tce=_test_hypothesis(problem,hyp)
|
| 1244 |
if tce<best_ce: best_ce=tce; best_b=tb
|
|
|
|
| 1245 |
if best_ce<current.ce:
|
| 1246 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1247 |
return accumulated,current
|
| 1248 |
|
| 1249 |
-
|
| 1250 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1251 |
|
| 1252 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1253 |
all_traces:List[HypothesisTrace]=[]; generator=SequenceHypothesisGenerator()
|
| 1254 |
-
|
| 1255 |
-
|
| 1256 |
-
|
| 1257 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1258 |
|
| 1259 |
init_b={v:(lo+hi)/2 for v,(lo,hi) in base_problem.bounds.items()}
|
| 1260 |
init_ce=base_problem.constraint_energy(init_b)
|
|
@@ -1264,49 +1476,124 @@ class SequenceRayTracer:
|
|
| 1264 |
{v:IV(*base_problem.bounds[v]) for v in base_problem.variables},N_MPRT_EXPLORE//5)
|
| 1265 |
if mprt_ce<init_ce: init_b=mprt_b; init_ce=mprt_ce
|
| 1266 |
seed_baton=Baton(binding=init_b,ce=init_ce,ray_id="SEED")
|
|
|
|
|
|
|
|
|
|
| 1267 |
self._last_traces=all_traces
|
| 1268 |
|
|
|
|
|
|
|
| 1269 |
while active and total_fired<self.MAX_TOTAL_RAYS:
|
| 1270 |
ray=active.pop(0); total_fired+=1
|
| 1271 |
parent_baton=ray.baton or seed_baton
|
| 1272 |
-
|
| 1273 |
-
|
| 1274 |
-
|
|
|
|
|
|
|
| 1275 |
t0=time.time()
|
| 1276 |
-
hyps,output_baton=generator.generate(
|
|
|
|
| 1277 |
elapsed=round((time.time()-t0)*1000,1)
|
| 1278 |
output_baton.ray_id=ray.ray_id; all_batons.append(output_baton)
|
| 1279 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1280 |
verify=VERIFY_LAYER.run(output_baton.binding,base_problem,axl_def.anchors)
|
| 1281 |
trace=HypothesisTrace(
|
| 1282 |
-
hid=ray.ray_id,round_idx=total_fired,ray_name=ray.name,
|
|
|
|
| 1283 |
ce_before=parent_baton.ce if parent_baton.ce<float('inf') else 99.0,
|
| 1284 |
ce_after=output_baton.ce,verify=verify,survived=verify.overall_pass,
|
| 1285 |
elapsed_ms=elapsed,depth=ray.depth,parent_id=ray.parent_id or "")
|
| 1286 |
all_traces.append(trace)
|
| 1287 |
-
|
| 1288 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1289 |
"ce_out":round(output_baton.ce,5),"survived":verify.overall_pass,"ms":elapsed})
|
| 1290 |
-
if verify.overall_pass: break
|
| 1291 |
-
parent_ce=parent_baton.ce if parent_baton.ce<float('inf') else init_ce
|
| 1292 |
-
earned=(output_baton.ce<parent_ce*self.CE_EARN_RATIO or ray.depth<self.MIN_DEPTH)
|
| 1293 |
-
if earned:
|
| 1294 |
-
remaining=[a for a in ALL_AXIOMS if a not in ray.sequence]
|
| 1295 |
-
random.shuffle(remaining); children=[]
|
| 1296 |
-
for axiom in remaining:
|
| 1297 |
-
child=ray.extend(axiom)
|
| 1298 |
-
if child: child.baton=output_baton; children.append(child)
|
| 1299 |
-
if len(children)>=self.BRANCH_WIDTH*2: break
|
| 1300 |
-
active=children+active
|
| 1301 |
|
| 1302 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1303 |
return best_binding,best_ce,history
|
| 1304 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1305 |
# ══════════════════════════════════════════════════════════════════════
|
| 1306 |
-
# SECTION
|
| 1307 |
# ══════════════════════════════════════════════════════════════════════
|
| 1308 |
-
|
| 1309 |
-
# Domain metadata
|
| 1310 |
PROBLEM_META={
|
| 1311 |
"EllipticCurvePoint": {"domain":"Cryptography", "icon":"🔐","difficulty":"Medium"},
|
| 1312 |
"MarkowitzPortfolio": {"domain":"Finance", "icon":"📈","difficulty":"Hard"},
|
|
@@ -1325,247 +1612,185 @@ PROBLEM_META={
|
|
| 1325 |
}
|
| 1326 |
|
| 1327 |
AXL_PROBLEMS=[
|
| 1328 |
-
|
| 1329 |
-
# ── CRYPTOGRAPHY ──────────────────────────────────────────────────────
|
| 1330 |
AXLProblemDef(
|
| 1331 |
name="EllipticCurvePoint",
|
| 1332 |
-
description="Find point on E: y²=x³-x+1
|
| 1333 |
axioms={Axiom.CONTINUOUS,Axiom.QUADRATIC,Axiom.METRIC,Axiom.SYMMETRIC},
|
| 1334 |
variables=[{"name":"ex","lo":-2.0,"hi":2.0},{"name":"ey","lo":-2.0,"hi":2.0}],
|
| 1335 |
-
constraints=[
|
| 1336 |
-
# y² - x³ + x - 1 = 0 → ey**2 - ex**3 + ex - 1 = 0
|
| 1337 |
-
{"kind":"EQ","expr":"ey**2 - ex**3 + ex - 1","weight":5.0},
|
| 1338 |
-
],
|
| 1339 |
scopes=[{"name":"curve","order":0,"vars":["ex","ey"],
|
| 1340 |
"constraints":[{"kind":"EQ","expr":"ey**2 - ex**3 + ex - 1","weight":8.0}]}],
|
| 1341 |
anchors=[AXLInvariant("on_curve","ey**2 - ex**3 + ex - 1",1e-3)],
|
| 1342 |
-
observations={"ex":0.0},
|
| 1343 |
),
|
| 1344 |
-
|
| 1345 |
-
# ── FINANCE ───────────────────────────────────────────────────────────
|
| 1346 |
AXLProblemDef(
|
| 1347 |
name="MarkowitzPortfolio",
|
| 1348 |
-
description="4-asset portfolio: budget=1, return=11%,
|
| 1349 |
-
"μ=[10,12,8,15]%, σ²=[4,9,1,16]%.",
|
| 1350 |
axioms={Axiom.CONSERVED,Axiom.ORDERED,Axiom.METRIC,Axiom.HOLISM},
|
| 1351 |
-
variables=[
|
| 1352 |
-
|
| 1353 |
-
{"name":"w3","lo":0.0,"hi":1.0},{"name":"w4","lo":0.0,"hi":1.0},
|
| 1354 |
-
],
|
| 1355 |
constraints=[
|
| 1356 |
-
{"kind":"CONSERVE","expr":"w1
|
| 1357 |
-
{"kind":"EQ","expr":"0.10*w1
|
| 1358 |
{"kind":"GEQ","expr":"w1","weight":1.0},{"kind":"GEQ","expr":"w2","weight":1.0},
|
| 1359 |
{"kind":"GEQ","expr":"w3","weight":1.0},{"kind":"GEQ","expr":"w4","weight":1.0},
|
| 1360 |
],
|
| 1361 |
scopes=[{"name":"portfolio","order":0,"vars":["w1","w2","w3","w4"],
|
| 1362 |
"constraints":[
|
| 1363 |
-
|
| 1364 |
-
{"kind":"EQ","expr":"w1
|
| 1365 |
-
{"kind":"EQ","expr":"0.10*w1 + 0.12*w2 + 0.08*w3 + 0.15*w4 - 0.11","weight":3.0},
|
| 1366 |
]}],
|
| 1367 |
anchors=[
|
| 1368 |
AXLInvariant("budget","w1+w2+w3+w4-1.0",1e-3),
|
| 1369 |
AXLInvariant("return_target","0.10*w1+0.12*w2+0.08*w3+0.15*w4-0.11",5e-3),
|
| 1370 |
-
AXLInvariant("
|
| 1371 |
-
AXLInvariant("
|
| 1372 |
-
AXLInvariant("w3_positive","w3",1e-3,"geq"),
|
| 1373 |
-
AXLInvariant("w4_positive","w4",1e-3,"geq"),
|
| 1374 |
],
|
| 1375 |
-
# Many valid solutions: e.g. w1=w2=w3≈0.267, w4≈0.200
|
| 1376 |
),
|
| 1377 |
-
|
| 1378 |
-
# ── ENERGY SYSTEMS ────────────────────────────────────────────────────
|
| 1379 |
AXLProblemDef(
|
| 1380 |
name="PowerFlowDC3Bus",
|
| 1381 |
-
description="DC power flow
|
| 1382 |
-
"θ1=0 (ref), Pg1=0.5. Find θ2≈-0.318, θ3≈0.046.",
|
| 1383 |
axioms={Axiom.CONSERVED,Axiom.NETWORK,Axiom.EQUILIBRIUM,Axiom.ORDERED},
|
| 1384 |
-
variables=[
|
| 1385 |
-
{"name":"pt2","lo":-1.0,"hi":0.5},
|
| 1386 |
-
{"name":"pt3","lo":-0.5,"hi":0.5},
|
| 1387 |
-
],
|
| 1388 |
constraints=[
|
| 1389 |
-
|
| 1390 |
-
{"kind":"EQ","expr":"
|
| 1391 |
-
# Bus 2: 3*θ2 - θ3 = -1.0 (Pd2=1.0)
|
| 1392 |
-
{"kind":"EQ","expr":"3*pt2 - pt3 + 1.0","weight":5.0},
|
| 1393 |
],
|
| 1394 |
scopes=[{"name":"power","order":0,"vars":["pt2","pt3"],
|
| 1395 |
"constraints":[
|
| 1396 |
-
{"kind":"EQ","expr":"-2*pt2
|
| 1397 |
-
{"kind":"EQ","expr":"3*pt2
|
| 1398 |
]}],
|
| 1399 |
anchors=[
|
| 1400 |
-
AXLInvariant("
|
| 1401 |
-
AXLInvariant("
|
| 1402 |
],
|
| 1403 |
-
# Known: pt2 = -7/22 ≈ -0.3182, pt3 = 1/22 ≈ 0.0455
|
| 1404 |
),
|
| 1405 |
-
|
| 1406 |
-
# ── CHEMISTRY ────────────────────────────────────────────────────────
|
| 1407 |
AXLProblemDef(
|
| 1408 |
name="ChemEquilibrium",
|
| 1409 |
-
description="A+B↔C
|
| 1410 |
-
"Initial [A]=[B]=1, [C]=0. Solve: ca=cb≈0.390, cc≈0.610.",
|
| 1411 |
axioms={Axiom.CONSERVED,Axiom.BILINEAR,Axiom.CONTINUOUS,Axiom.MONOTONE},
|
| 1412 |
-
variables=[
|
| 1413 |
-
|
| 1414 |
-
{"name":"cb","lo":0.0,"hi":1.0},
|
| 1415 |
-
{"name":"cc","lo":0.0,"hi":1.0},
|
| 1416 |
-
],
|
| 1417 |
constraints=[
|
| 1418 |
-
{"kind":"CONSERVE","expr":"ca
|
| 1419 |
-
{"kind":"CONSERVE","expr":"cb
|
| 1420 |
-
{"kind":"EQ","expr":"4*ca*cb
|
| 1421 |
],
|
| 1422 |
-
scopes=[{"name":"
|
| 1423 |
"constraints":[
|
| 1424 |
-
{"kind":"EQ","expr":"ca
|
| 1425 |
-
{"kind":"EQ","expr":"4*ca*cb
|
| 1426 |
]}],
|
| 1427 |
anchors=[
|
| 1428 |
AXLInvariant("balance_A","ca+cc-1.0",1e-3),
|
| 1429 |
AXLInvariant("balance_B","cb+cc-1.0",1e-3),
|
| 1430 |
-
AXLInvariant("equilibrium","4*ca*cb
|
| 1431 |
],
|
| 1432 |
-
# Known: ca=cb=(-1+√17)/8≈0.3904, cc≈0.6096
|
| 1433 |
),
|
| 1434 |
-
|
| 1435 |
-
# ── CHAOS THEORY ─────────────────────────────────────────────────────
|
| 1436 |
AXLProblemDef(
|
| 1437 |
name="LorenzFixedPoint",
|
| 1438 |
-
description="Lorenz σ=10,ρ=28,β=8/3.
|
| 1439 |
-
"x=y, z=27, x²=72. Solution: (±8.485, ±8.485, 27).",
|
| 1440 |
axioms={Axiom.CONTINUOUS,Axiom.QUADRATIC,Axiom.SYMMETRIC,Axiom.CONSERVED},
|
| 1441 |
-
variables=[
|
| 1442 |
-
|
| 1443 |
-
{"name":"ly","lo":-12.0,"hi":12.0},
|
| 1444 |
-
{"name":"lz","lo":20.0,"hi":35.0},
|
| 1445 |
-
],
|
| 1446 |
constraints=[
|
| 1447 |
-
{"kind":"EQ","expr":"lx
|
| 1448 |
-
{"kind":"EQ","expr":"lz
|
| 1449 |
-
{"kind":"EQ","expr":"lx**2
|
| 1450 |
],
|
| 1451 |
scopes=[{"name":"lorenz","order":0,"vars":["lx","ly","lz"],
|
| 1452 |
"constraints":[
|
| 1453 |
-
{"kind":"EQ","expr":"lx
|
| 1454 |
-
{"kind":"EQ","expr":"lz
|
| 1455 |
-
{"kind":"EQ","expr":"lx**2
|
| 1456 |
]}],
|
| 1457 |
anchors=[
|
| 1458 |
-
AXLInvariant("
|
| 1459 |
-
AXLInvariant("
|
| 1460 |
-
AXLInvariant("
|
| 1461 |
],
|
| 1462 |
),
|
| 1463 |
-
|
| 1464 |
-
# ── GAME THEORY ──────────────────────────────────────────────────────
|
| 1465 |
AXLProblemDef(
|
| 1466 |
name="NashBattleSexes",
|
| 1467 |
-
description="Battle of Sexes
|
| 1468 |
axioms={Axiom.CONTINUOUS,Axiom.SYMMETRIC,Axiom.CONSERVED,Axiom.ORDERED},
|
| 1469 |
-
variables=[
|
| 1470 |
-
{"name":"np","lo":0.0,"hi":1.0}, # P1 prob choosing Opera
|
| 1471 |
-
{"name":"nq","lo":0.0,"hi":1.0}, # P2 prob choosing Opera
|
| 1472 |
-
],
|
| 1473 |
constraints=[
|
| 1474 |
-
{"kind":"EQ","expr":"3*nq
|
| 1475 |
-
{"kind":"EQ","expr":"3*np
|
| 1476 |
],
|
| 1477 |
scopes=[{"name":"nash","order":0,"vars":["np","nq"],
|
| 1478 |
"constraints":[
|
| 1479 |
-
{"kind":"EQ","expr":"3*nq
|
| 1480 |
-
{"kind":"EQ","expr":"3*np
|
| 1481 |
]}],
|
| 1482 |
anchors=[
|
| 1483 |
AXLInvariant("p1_indiff","3*nq-1.0",1e-3),
|
| 1484 |
AXLInvariant("p2_indiff","3*np-2.0",1e-3),
|
| 1485 |
],
|
| 1486 |
-
# Known: np=2/3≈0.6667, nq=1/3≈0.3333
|
| 1487 |
),
|
| 1488 |
-
|
| 1489 |
-
# ── ASTRONOMY ─────────────────────────────────────────────────────────
|
| 1490 |
AXLProblemDef(
|
| 1491 |
name="KeplerPeriapsis",
|
| 1492 |
-
description="Orbital mechanics at periapsis.
|
| 1493 |
-
"Find rp=0.5, vp=√3≈1.732, h≈0.866.",
|
| 1494 |
axioms={Axiom.CONTINUOUS,Axiom.QUADRATIC,Axiom.CONSERVED,Axiom.METRIC},
|
| 1495 |
variables=[
|
| 1496 |
-
{"name":"ka","lo":0.5,"hi":2.0},
|
| 1497 |
-
{"name":"
|
| 1498 |
-
{"name":"
|
| 1499 |
-
{"name":"kvp","lo":0.5,"hi":5.0}, # periapsis speed
|
| 1500 |
-
{"name":"kh","lo":0.1,"hi":3.0}, # specific angular momentum
|
| 1501 |
],
|
| 1502 |
constraints=[
|
| 1503 |
-
{"kind":"EQ","expr":"krp
|
| 1504 |
-
{"kind":"EQ","expr":"kvp**2*krp
|
| 1505 |
-
{"kind":"EQ","expr":"kh
|
| 1506 |
],
|
| 1507 |
scopes=[{"name":"orbit","order":0,"vars":["ka","ke","krp","kvp","kh"],
|
| 1508 |
"constraints":[
|
| 1509 |
-
{"kind":"EQ","expr":"krp
|
| 1510 |
-
{"kind":"EQ","expr":"kvp**2*krp
|
| 1511 |
-
{"kind":"EQ","expr":"kh
|
| 1512 |
]}],
|
| 1513 |
anchors=[
|
| 1514 |
-
AXLInvariant("
|
| 1515 |
-
AXLInvariant("vis_viva","kvp**2*krp
|
| 1516 |
-
AXLInvariant("
|
| 1517 |
],
|
| 1518 |
-
observations={"ka":1.0,"ke":0.5},
|
| 1519 |
),
|
| 1520 |
-
|
| 1521 |
-
# ── STRUCTURAL ENGINEERING ────────────────────────────────────────────
|
| 1522 |
AXLProblemDef(
|
| 1523 |
name="VibratingString3",
|
| 1524 |
-
description="3-node string
|
| 1525 |
-
"FD equations. Known: s1=s3=1.5, s2=2.0.",
|
| 1526 |
axioms={Axiom.ORDERED,Axiom.SYMMETRIC,Axiom.CONSERVED,Axiom.METRIC},
|
| 1527 |
-
variables=[
|
| 1528 |
-
|
| 1529 |
-
{"name":"s2","lo":0.0,"hi":5.0},
|
| 1530 |
-
{"name":"s3","lo":0.0,"hi":5.0},
|
| 1531 |
-
],
|
| 1532 |
constraints=[
|
| 1533 |
-
{"kind":"EQ","expr":"-2*s1
|
| 1534 |
-
{"kind":"EQ","expr":"s1
|
| 1535 |
-
{"kind":"EQ","expr":"s2
|
| 1536 |
],
|
| 1537 |
scopes=[{"name":"string","order":0,"vars":["s1","s2","s3"],
|
| 1538 |
"constraints":[
|
| 1539 |
-
{"kind":"EQ","expr":"-2*s1
|
| 1540 |
-
{"kind":"EQ","expr":"s1
|
| 1541 |
-
{"kind":"EQ","expr":"s2
|
| 1542 |
]}],
|
| 1543 |
anchors=[
|
| 1544 |
AXLInvariant("node1","-2*s1+s2+1.0",1e-3),
|
| 1545 |
AXLInvariant("node2","s1-2*s2+s3+1.0",1e-3),
|
| 1546 |
AXLInvariant("node3","s2-2*s3+1.0",1e-3),
|
| 1547 |
-
AXLInvariant("symmetry","s1-s3",1e-3),
|
| 1548 |
],
|
| 1549 |
-
# Known: s1=s3=1.5, s2=2.0
|
| 1550 |
),
|
| 1551 |
-
|
| 1552 |
-
# ── SIGNAL PROCESSING ─────────────────────────────────────────────────
|
| 1553 |
AXLProblemDef(
|
| 1554 |
name="SignalRecovery4",
|
| 1555 |
-
description="Compressed sensing:
|
| 1556 |
-
"A=[[1,1,0,0],[1,0,1,0],[0,1,0,1]], b=[3,1,4]. "
|
| 1557 |
-
"Sparse solution: x=[1,2,0,2] (3-sparse, r3=0).",
|
| 1558 |
axioms={Axiom.CONSERVED,Axiom.PARSIMONY,Axiom.METRIC,Axiom.INJECTIVE},
|
| 1559 |
-
variables=[
|
| 1560 |
-
|
| 1561 |
-
{"name":"r2","lo":0.0,"hi":5.0},
|
| 1562 |
-
{"name":"r3","lo":0.0,"hi":5.0},
|
| 1563 |
-
{"name":"r4","lo":0.0,"hi":5.0},
|
| 1564 |
-
],
|
| 1565 |
constraints=[
|
| 1566 |
-
{"kind":"EQ","expr":"r1
|
| 1567 |
-
{"kind":"EQ","expr":"r1
|
| 1568 |
-
{"kind":"EQ","expr":"r2
|
| 1569 |
],
|
| 1570 |
scopes=[{"name":"signal","order":0,"vars":["r1","r2","r3","r4"],
|
| 1571 |
"constraints":[
|
|
@@ -1578,24 +1803,15 @@ AXLProblemDef(
|
|
| 1578 |
AXLInvariant("meas2","r1+r3-1.0",1e-3),
|
| 1579 |
AXLInvariant("meas3","r2+r4-4.0",1e-3),
|
| 1580 |
],
|
| 1581 |
-
# Known sparse: r1=1, r2=2, r3=0, r4=2
|
| 1582 |
),
|
| 1583 |
-
|
| 1584 |
-
# ── ROBOTICS ──────────────────────────────────────────────────��──────
|
| 1585 |
AXLProblemDef(
|
| 1586 |
name="RobotArm2D",
|
| 1587 |
-
description="2-link
|
| 1588 |
-
"Find angles: t1≈-0.177rad, t2≈1.531rad. (Trig constraints.)",
|
| 1589 |
axioms={Axiom.CONTINUOUS,Axiom.METRIC,Axiom.SYMMETRIC,Axiom.QUADRATIC},
|
| 1590 |
-
variables=[
|
| 1591 |
-
{"name":"t1","lo":-3.15,"hi":3.15}, # joint 1 angle
|
| 1592 |
-
{"name":"t2","lo":-3.15,"hi":3.15}, # joint 2 angle
|
| 1593 |
-
],
|
| 1594 |
constraints=[
|
| 1595 |
-
|
| 1596 |
-
{"kind":"EQ","expr":"
|
| 1597 |
-
# End-effector y = sin(t1) + sin(t1+t2) = 0.8
|
| 1598 |
-
{"kind":"EQ","expr":"sin(t1) + sin(t1+t2) - 0.8","weight":5.0},
|
| 1599 |
],
|
| 1600 |
scopes=[{"name":"kinematics","order":0,"vars":["t1","t2"],
|
| 1601 |
"constraints":[
|
|
@@ -1605,25 +1821,18 @@ AXLProblemDef(
|
|
| 1605 |
anchors=[
|
| 1606 |
AXLInvariant("reach_x","cos(t1)+cos(t1+t2)-1.2",1e-2),
|
| 1607 |
AXLInvariant("reach_y","sin(t1)+sin(t1+t2)-0.8",1e-2),
|
| 1608 |
-
|
| 1609 |
-
AXLInvariant("elbow_check","cos(t2) - 0.04",0.05),
|
| 1610 |
],
|
| 1611 |
-
# Known: t2=arccos(0.04)≈1.531, t1≈-0.177 (elbow-up config)
|
| 1612 |
),
|
| 1613 |
-
|
| 1614 |
-
# ── MATHEMATICS (from v13.0) ─────────────────────────────────────────
|
| 1615 |
AXLProblemDef(
|
| 1616 |
name="NormManifold4D",
|
| 1617 |
-
description="4 vars on unit sphere, zero sum, x1 observed at 0.5.
|
| 1618 |
-
"Multiple solutions exist on the great circle.",
|
| 1619 |
axioms={Axiom.CONTINUOUS,Axiom.QUADRATIC,Axiom.CONSERVED,Axiom.METRIC,Axiom.SYMMETRIC},
|
| 1620 |
-
variables=[
|
| 1621 |
-
|
| 1622 |
-
{"name":"x3","lo":-1.0,"hi":1.0},{"name":"x4","lo":-1.0,"hi":1.0},
|
| 1623 |
-
],
|
| 1624 |
constraints=[
|
| 1625 |
-
{"kind":"CONSERVE","expr":"x1**2
|
| 1626 |
-
{"kind":"EQ","expr":"x1
|
| 1627 |
],
|
| 1628 |
scopes=[{"name":"sphere","order":0,"vars":["x1","x2","x3","x4"],
|
| 1629 |
"constraints":[{"kind":"EQ","expr":"x1**2+x2**2+x3**2+x4**2-1.0","weight":5.0}]}],
|
|
@@ -1636,8 +1845,7 @@ AXLProblemDef(
|
|
| 1636 |
),
|
| 1637 |
AXLProblemDef(
|
| 1638 |
name="BilinearChain6",
|
| 1639 |
-
description="6-var ordered chain.
|
| 1640 |
-
"Known: (0.5,1.0,1.0,2.0,1.5,3.0).",
|
| 1641 |
axioms={Axiom.DISCRETE,Axiom.ORDERED,Axiom.BILINEAR,Axiom.CONSERVED,Axiom.NETWORK},
|
| 1642 |
variables=[{"name":f"t{i}","lo":0.0,"hi":3.0} for i in range(1,7)],
|
| 1643 |
constraints=[
|
|
@@ -1662,21 +1870,17 @@ AXLProblemDef(
|
|
| 1662 |
),
|
| 1663 |
AXLProblemDef(
|
| 1664 |
name="PhaseCollider",
|
| 1665 |
-
description="2-particle
|
| 1666 |
-
"p1 at r=0.5 or r=1.0.",
|
| 1667 |
axioms={Axiom.DISCRETE,Axiom.MUTABLE,Axiom.SYMMETRIC,Axiom.NETWORK,Axiom.CONSERVED},
|
| 1668 |
-
variables=[
|
| 1669 |
-
|
| 1670 |
-
{"name":"p1y","lo":-2.0,"hi":2.0},{"name":"p2y","lo":-2.0,"hi":2.0},
|
| 1671 |
-
],
|
| 1672 |
constraints=[
|
| 1673 |
{"kind":"CONSERVE","expr":"p1x+p2x"},{"kind":"CONSERVE","expr":"p1y+p2y"},
|
| 1674 |
],
|
| 1675 |
scopes=[{"name":"phase","order":0,"vars":["p1x","p2x","p1y","p2y"],
|
| 1676 |
"constraints":[
|
| 1677 |
{"kind":"BRANCH","name":"phase_select","options":[
|
| 1678 |
-
"p1x**2+p1y**2-0.25","p1x**2+p1y**2-1.0",
|
| 1679 |
-
]},
|
| 1680 |
{"kind":"EQ","expr":"p1x+p2x","weight":3.0},
|
| 1681 |
{"kind":"EQ","expr":"p1y+p2y","weight":3.0},
|
| 1682 |
]}],
|
|
@@ -1688,14 +1892,10 @@ AXLProblemDef(
|
|
| 1688 |
),
|
| 1689 |
AXLProblemDef(
|
| 1690 |
name="MetricPacking3D",
|
| 1691 |
-
description="3 vars
|
| 1692 |
-
"Known: a=-√3, b=0, c=√3.",
|
| 1693 |
axioms={Axiom.CONTINUOUS,Axiom.METRIC,Axiom.INJECTIVE,Axiom.CONSERVED,Axiom.SYMMETRIC},
|
| 1694 |
-
variables=[
|
| 1695 |
-
|
| 1696 |
-
{"name":"b","lo":-3.0,"hi":3.0},
|
| 1697 |
-
{"name":"c","lo":-3.0,"hi":3.0},
|
| 1698 |
-
],
|
| 1699 |
constraints=[
|
| 1700 |
{"kind":"CONSERVE","expr":"a+b+c"},
|
| 1701 |
{"kind":"GEQ","expr":"(a-b)**2-1.0","weight":2.0},
|
|
@@ -1707,12 +1907,11 @@ AXLProblemDef(
|
|
| 1707 |
anchors=[
|
| 1708 |
AXLInvariant("centred","a+b+c",1e-3),
|
| 1709 |
AXLInvariant("norm_6","a**2+b**2+c**2-6.0",0.05),
|
| 1710 |
-
AXLInvariant("sep_ab","(a-b)**2-1.0",0.0,"geq"),
|
| 1711 |
-
AXLInvariant("sep_bc","(b-c)**2-1.0",0.0,"geq"),
|
| 1712 |
],
|
| 1713 |
),
|
| 1714 |
-
|
| 1715 |
-
] # end AXL_PROBLEMS
|
| 1716 |
|
| 1717 |
def build_base_problem(axl_def:AXLProblemDef) -> Problem:
|
| 1718 |
psl_text=AXL_COMPILER.compile(axl_def)
|
|
@@ -1723,16 +1922,18 @@ def build_base_problem(axl_def:AXLProblemDef) -> Problem:
|
|
| 1723 |
scope_order=ep.scope_order,annotations=ep.annotations)
|
| 1724 |
|
| 1725 |
# ══════════════════════════════════════════════════════════════════════
|
| 1726 |
-
# SECTION
|
| 1727 |
# ══════════════════════════════════════════════════════════════════════
|
| 1728 |
STATE_LOCK = threading.Lock()
|
| 1729 |
RUN_LOG: List[Dict] = []
|
| 1730 |
PROBLEM_STATS: Dict[str,Dict] = {p.name: {
|
| 1731 |
"runs":0,"solved":0,"total_ce":0.0,"total_rays":0,
|
| 1732 |
-
"best_ce":float('inf'),"best_ray":"—","
|
|
|
|
|
|
|
| 1733 |
} for p in AXL_PROBLEMS}
|
| 1734 |
-
POOL
|
| 1735 |
-
|
| 1736 |
|
| 1737 |
def _run_problem(axl_def:AXLProblemDef):
|
| 1738 |
try:
|
|
@@ -1743,6 +1944,17 @@ def _run_problem(axl_def:AXLProblemDef):
|
|
| 1743 |
survived=[t for t in traces if t.survived]
|
| 1744 |
failed =[t for t in traces if not t.survived]
|
| 1745 |
best_t =min(survived,key=lambda t:t.ce_after,default=None)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1746 |
record={
|
| 1747 |
"problem":axl_def.name,
|
| 1748 |
"description":axl_def.description[:60],
|
|
@@ -1754,7 +1966,8 @@ def _run_problem(axl_def:AXLProblemDef):
|
|
| 1754 |
"binding":{k:round(v,5) for k,v in binding.items()},
|
| 1755 |
"observations":axl_def.observations,
|
| 1756 |
"traces":[{
|
| 1757 |
-
"round":t.round_idx,"ray":t.ray_name,"
|
|
|
|
| 1758 |
"ce_before":round(t.ce_before,5),"ce":round(t.ce_after,5),
|
| 1759 |
"g1_ce":round(t.verify.gate1_ce,5) if t.verify else None,
|
| 1760 |
"g1":t.verify.gate1_pass if t.verify else False,
|
|
@@ -1762,9 +1975,11 @@ def _run_problem(axl_def:AXLProblemDef):
|
|
| 1762 |
"g2_detail":{k:(round(v,6),ok) for k,(v,ok) in t.verify.gate2_results.items()} if t.verify else {},
|
| 1763 |
"survived":t.survived,"ms":t.elapsed_ms,
|
| 1764 |
} for t in traces],
|
|
|
|
| 1765 |
"survived_count":len(survived),
|
| 1766 |
"failed_count":len(failed),
|
| 1767 |
"best_ray":best_t.ray_name if best_t else "—",
|
|
|
|
| 1768 |
"total_fired":len(traces),
|
| 1769 |
}
|
| 1770 |
with STATE_LOCK:
|
|
@@ -1772,22 +1987,23 @@ def _run_problem(axl_def:AXLProblemDef):
|
|
| 1772 |
if len(RUN_LOG)>60: RUN_LOG.pop(0)
|
| 1773 |
ps=PROBLEM_STATS[axl_def.name]
|
| 1774 |
ps["runs"]+=1; ps["total_rays"]+=len(traces); ps["total_ce"]+=ce
|
| 1775 |
-
if len(survived)>0 and ce<SOLVE_THRESHOLD:
|
| 1776 |
-
ps["solved"]+=1
|
| 1777 |
if ce<ps["best_ce"]:
|
| 1778 |
ps["best_ce"]=ce
|
| 1779 |
ps["best_ray"]=best_t.ray_name if best_t else "—"
|
| 1780 |
-
ps["
|
|
|
|
|
|
|
|
|
|
| 1781 |
except Exception as e:
|
| 1782 |
import traceback; traceback.print_exc()
|
| 1783 |
print(f"[RUN ERROR] {axl_def.name}: {e}")
|
| 1784 |
|
| 1785 |
async def run_loop():
|
| 1786 |
-
global
|
| 1787 |
loop=asyncio.get_event_loop()
|
| 1788 |
while True:
|
| 1789 |
-
prob=AXL_PROBLEMS[
|
| 1790 |
-
_PROBLEM_IDX+=1
|
| 1791 |
await loop.run_in_executor(POOL,_run_problem,prob)
|
| 1792 |
await asyncio.sleep(0.2)
|
| 1793 |
|
|
@@ -1798,60 +2014,49 @@ async def lifespan(app):
|
|
| 1798 |
POOL.shutdown(wait=False)
|
| 1799 |
|
| 1800 |
# ══════════════════════════════════════════════════════════════════════
|
| 1801 |
-
# SECTION
|
| 1802 |
# ══════════════════════════════════════════════════════════════════════
|
| 1803 |
-
app=FastAPI(title="Practicality
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1804 |
|
| 1805 |
def _perf_table() -> str:
|
| 1806 |
rows=""
|
| 1807 |
for prob in AXL_PROBLEMS:
|
| 1808 |
ps=PROBLEM_STATS[prob.name]
|
| 1809 |
if ps["runs"]==0:
|
| 1810 |
-
rows+=f"<tr><td
|
| 1811 |
continue
|
| 1812 |
runs=ps["runs"]; rate=round(ps["solved"]/runs*100)
|
| 1813 |
avg_ce=round(ps["total_ce"]/runs,5)
|
| 1814 |
-
|
| 1815 |
-
|
|
|
|
|
|
|
|
|
|
| 1816 |
dom=PROBLEM_META.get(prob.name,{})
|
| 1817 |
-
|
| 1818 |
-
|
| 1819 |
-
best_ce_str=f"{ps['best_ce']:.5f}" if ps["best_ce"]<float('inf') else "—"
|
| 1820 |
rows+=(f"<tr>"
|
| 1821 |
f"<td style='color:#aaa'>{dom.get('icon','·')}</td>"
|
| 1822 |
-
f"<td style='color:#5C6BC0;font-size:0.8em'>{dom.get('domain','')}</td>"
|
| 1823 |
f"<td style='color:#FF9800'>{prob.name}</td>"
|
|
|
|
| 1824 |
f"<td style='color:#555;font-size:0.75em'>{dom.get('difficulty','')}</td>"
|
| 1825 |
-
f"<td style='color:#888;font-size:0.75em'>{axiom_str}</td>"
|
| 1826 |
f"<td style='color:#aaa'>{runs}</td>"
|
| 1827 |
f"<td style='color:{rate_col};font-weight:700'>{rate}%</td>"
|
| 1828 |
f"<td style='color:#26C6DA'>{avg_ce}</td>"
|
| 1829 |
-
f"<td style='color:#26C6DA;font-size:0.8em'>{
|
| 1830 |
-
f"
|
| 1831 |
-
f"<td style='color:#4CAF50;font-size:0.75em'>{best_ray}</td>"
|
| 1832 |
f"</tr>")
|
| 1833 |
return rows
|
| 1834 |
|
| 1835 |
-
def _axiom_table(log) -> str:
|
| 1836 |
-
axiom_stats=defaultdict(lambda:{"tried":0,"survived":0,"total_ce":0.0,"as_seed":0})
|
| 1837 |
-
for r in log:
|
| 1838 |
-
for t in r.get("traces",[]):
|
| 1839 |
-
parts=t["ray"].split("→")
|
| 1840 |
-
for pos,ax in enumerate(parts):
|
| 1841 |
-
if not ax: continue
|
| 1842 |
-
axiom_stats[ax]["tried"]+=1; axiom_stats[ax]["total_ce"]+=t["ce"]
|
| 1843 |
-
if t["survived"]: axiom_stats[ax]["survived"]+=1
|
| 1844 |
-
if pos==0: axiom_stats[ax]["as_seed"]+=1
|
| 1845 |
-
return "".join(
|
| 1846 |
-
f"<tr><td style='color:#FF9800'>{ax}</td>"
|
| 1847 |
-
f"<td style='color:#aaa'>{s['tried']}</td>"
|
| 1848 |
-
f"<td style='color:#26C6DA'>{s['as_seed']}</td>"
|
| 1849 |
-
f"<td style='color:#4CAF50'>{s['survived']}</td>"
|
| 1850 |
-
f"<td style='color:#26C6DA'>{round(s['total_ce']/s['tried'],5) if s['tried'] else 0}</td>"
|
| 1851 |
-
f"<td style='color:{'#4CAF50' if s['survived']>0 else '#333'}'>{round(s['survived']/s['tried']*100):.0f}%</td></tr>"
|
| 1852 |
-
for ax,s in sorted(axiom_stats.items(),key=lambda x:-x[1]["survived"])
|
| 1853 |
-
) or "<tr><td colspan='6' style='color:#222'>—</td></tr>"
|
| 1854 |
-
|
| 1855 |
def _render_collapse(record:Dict) -> str:
|
| 1856 |
b=record["binding"]; traces=record["traces"]
|
| 1857 |
survived=[t for t in traces if t["survived"]]
|
|
@@ -1861,11 +2066,13 @@ def _render_collapse(record:Dict) -> str:
|
|
| 1861 |
ce=record["ce"]; solved=record["solved"]
|
| 1862 |
ce_color="#4CAF50" if solved else ("#FF9800" if ce<0.5 else "#EF5350")
|
| 1863 |
status="✓ SOLVED" if solved else ("~ PARTIAL" if ce<0.5 else "✗ UNSOLVED")
|
|
|
|
| 1864 |
binding_rows="".join(
|
| 1865 |
f"<tr><td style='color:#888'>{v}</td>"
|
| 1866 |
f"<td style='color:#26C6DA;font-weight:700'>{val:+.5f}</td>"
|
| 1867 |
f"<td style='color:#4CAF50;font-size:0.7em'>{'[OBS]' if v in obs_vars else ''}</td></tr>"
|
| 1868 |
for v,val in b.items())
|
|
|
|
| 1869 |
inv_rows=""
|
| 1870 |
if best and best.get("g2_detail"):
|
| 1871 |
for inv,(val,ok) in best["g2_detail"].items():
|
|
@@ -1873,32 +2080,41 @@ def _render_collapse(record:Dict) -> str:
|
|
| 1873 |
inv_rows+=(f"<tr><td style='color:{c}'>{'✓' if ok else '✗'}</td>"
|
| 1874 |
f"<td style='color:#888;font-size:0.8em'>{inv}</td>"
|
| 1875 |
f"<td style='color:{c};font-size:0.8em'>{val:.5f}</td></tr>")
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1876 |
def span(t):
|
|
|
|
| 1877 |
depth_indent="·"*min(t.get("depth",0),5)
|
| 1878 |
c="#4CAF50" if t["survived"] else ("#555" if t.get("depth",0)>0 else "#333")
|
| 1879 |
star=" ◀" if t["survived"] else ""
|
| 1880 |
delta=t["ce"]-t.get("ce_before",t["ce"])
|
| 1881 |
-
return (f"<div style='color:{c};font-size:0.
|
| 1882 |
-
f"{depth_indent}[{t['round']}|d{t.get('depth',0)}] "
|
| 1883 |
f"<span style='color:#FF9800'>{t['ray']}</span> "
|
| 1884 |
f"CE={t['ce']:.4f} <span style='color:#444'>{delta:+.4f}</span>"
|
| 1885 |
f"<span style='color:#4CAF50;font-weight:700'>{star}</span></div>")
|
| 1886 |
-
|
|
|
|
| 1887 |
return f"""
|
| 1888 |
-
<div style='border:1px solid #181818;border-radius:6px;margin-bottom:
|
| 1889 |
-
<div style='background:#0d0d0d;padding:7px 12px;border-bottom:1px solid #1a1a1a;display:flex;align-items:center;gap:14px'>
|
| 1890 |
<span style='color:{ce_color};font-weight:700'>{status}</span>
|
| 1891 |
<span style='color:#555;font-size:0.8em'>{record.get("icon","·")} {record["problem"]}</span>
|
| 1892 |
<span style='color:#5C6BC0;font-size:0.75em'>{record.get("domain","")}</span>
|
| 1893 |
<span style='color:#333;font-size:0.75em'>CE={ce:.6f}</span>
|
| 1894 |
<span style='color:#26C6DA;font-size:0.72em'>{record["survived_count"]} survived / {record["total_fired"]} fired</span>
|
|
|
|
| 1895 |
</div>
|
| 1896 |
<div style='display:flex'>
|
| 1897 |
-
<div style='flex:0 0
|
| 1898 |
<div style='color:#333;font-size:0.65em;margin-bottom:4px'>BINDING</div>
|
| 1899 |
<table style='border-collapse:collapse;width:100%'>{binding_rows}</table>
|
| 1900 |
</div>
|
| 1901 |
-
<div style='flex:0 0
|
| 1902 |
<div style='color:#333;font-size:0.65em;margin-bottom:4px'>GATE 2 INVARIANTS</div>
|
| 1903 |
<table style='border-collapse:collapse;width:100%'>
|
| 1904 |
{inv_rows or "<tr><td colspan='3' style='color:#222'>—</td></tr>"}
|
|
@@ -1906,7 +2122,7 @@ def _render_collapse(record:Dict) -> str:
|
|
| 1906 |
</div>
|
| 1907 |
<div style='flex:1;padding:8px 10px;overflow-y:auto;max-height:200px'>
|
| 1908 |
<div style='color:#333;font-size:0.65em;margin-bottom:4px'>
|
| 1909 |
-
RAY TREE — best: <span style='color:#FF9800'>{record["best_ray"]}</span>
|
| 1910 |
</div>
|
| 1911 |
{trail}
|
| 1912 |
</div>
|
|
@@ -1917,21 +2133,43 @@ def _render_collapse(record:Dict) -> str:
|
|
| 1917 |
async def dashboard():
|
| 1918 |
with STATE_LOCK:
|
| 1919 |
log=list(reversed(RUN_LOG[-8:]))
|
| 1920 |
-
|
| 1921 |
-
total_runs=sum(s["runs"] for s in
|
| 1922 |
-
total_solved=sum(s["solved"] for s in
|
| 1923 |
-
|
| 1924 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1925 |
|
| 1926 |
perf_rows=_perf_table()
|
| 1927 |
-
ax_rows=_axiom_table(log)
|
| 1928 |
collapses="".join(_render_collapse(r) for r in log) if log else \
|
| 1929 |
"<div style='color:#222;padding:16px'>Cycling through 14 problems…</div>"
|
| 1930 |
|
| 1931 |
-
return f"""<!DOCTYPE html><html><head><title>Practicality
|
| 1932 |
<meta http-equiv="refresh" content="5">
|
| 1933 |
<style>
|
| 1934 |
-
body{{background:#090909;color:#e0e0e0;font-family:monospace;padding:18px;max-width:
|
| 1935 |
h1{{color:#26C6DA;border-bottom:1px solid #1a1a1a;padding-bottom:5px;font-size:1.1em;margin-bottom:4px}}
|
| 1936 |
h3{{color:#252525;margin-top:18px;font-size:0.82em;letter-spacing:2px;text-transform:uppercase}}
|
| 1937 |
table{{width:100%;border-collapse:collapse;margin-bottom:8px}}
|
|
@@ -1939,10 +2177,10 @@ async def dashboard():
|
|
| 1939 |
th{{color:#252525;font-size:0.70em}}
|
| 1940 |
.badge{{display:inline-block;padding:2px 9px;border-radius:3px;background:#0e0e0e;margin:2px;font-size:0.75em;border:1px solid #1a1a1a}}
|
| 1941 |
</style></head><body>
|
| 1942 |
-
<h1>⚗ Practicality
|
| 1943 |
<div style='color:#2a2a2a;font-size:0.72em;margin-bottom:10px'>
|
| 1944 |
-
|
| 1945 |
-
|
| 1946 |
</div>
|
| 1947 |
<div style='margin-bottom:14px'>
|
| 1948 |
<span class='badge' style='color:#aaa'>Total Runs: {total_runs}</span>
|
|
@@ -1952,20 +2190,21 @@ async def dashboard():
|
|
| 1952 |
<span class='badge' style='color:#5C6BC0'>Axioms: {len(ALL_AXIOMS)}</span>
|
| 1953 |
</div>
|
| 1954 |
|
| 1955 |
-
<h3>
|
| 1956 |
<table>
|
| 1957 |
-
<tr>
|
| 1958 |
-
|
| 1959 |
-
<th>Runs</th><th>Rate%</th><th>Avg CE</th><th>Best CE</th>
|
| 1960 |
-
<th>Avg Rays</th><th>Best Sequence</th>
|
| 1961 |
-
</tr>
|
| 1962 |
-
{perf_rows}
|
| 1963 |
</table>
|
| 1964 |
|
| 1965 |
-
<h3>
|
| 1966 |
<table>
|
| 1967 |
-
<tr>
|
| 1968 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1969 |
</table>
|
| 1970 |
|
| 1971 |
<h3>Recent Runs</h3>
|
|
|
|
| 1 |
#!/usr/bin/env python3
|
| 2 |
"""
|
| 3 |
+
PRACTICALITY SYSTEM 15.0 — CREATIVE SEQUENCE WISDOM
|
| 4 |
═══════════════════════════════════════════════════════════════════
|
| 5 |
+
NEW IN 15.0:
|
| 6 |
+
|
| 7 |
+
· CreativeSeeder — four categories of creative ray generation:
|
| 8 |
+
|
| 9 |
+
1. TENSION RAYS: mediated contradictions. [A→B→C] where A and C
|
| 10 |
+
are in ADJACENT_CONTRADICTIONS but B mediates between them.
|
| 11 |
+
CO₂ molecules of the axiom space — stable structures from
|
| 12 |
+
reactive parts. The system now explicitly *seeks* these.
|
| 13 |
+
|
| 14 |
+
2. SCOUT RAYS: random valid sequences, length 3-8. No earning
|
| 15 |
+
required. Pure cartographers of unexplored territory.
|
| 16 |
+
Retroactively earn branching rights if CE is good.
|
| 17 |
+
|
| 18 |
+
3. RECOMBINATION RAYS: genetic crossover of two successful rays.
|
| 19 |
+
Front half of one proven sequence + tail of another.
|
| 20 |
+
Novel combinations from parts that independently worked.
|
| 21 |
+
|
| 22 |
+
4. INVERSION RAYS: a successful sequence reversed and re-fired.
|
| 23 |
+
Same axioms, opposite order of application. The problem
|
| 24 |
+
approached from the other end.
|
| 25 |
+
|
| 26 |
+
· Resonant Pair Discovery (in-run, zero cross-run bias):
|
| 27 |
+
When two consecutive axioms in a sequence both reduce CE
|
| 28 |
+
meaningfully, they are stored as a 'resonant pair' in the
|
| 29 |
+
StructuralModel (per-run only). Child branching prioritises
|
| 30 |
+
extensions that continue resonant pairs. The system senses what
|
| 31 |
+
axiomatic connections are potent for THIS problem in THIS run.
|
| 32 |
+
|
| 33 |
+
· Ray Type field on every ray and trace. Dashboard shows breakdown
|
| 34 |
+
by type — see which creative category drives the most solves.
|
| 35 |
+
|
| 36 |
+
· 14-problem real-world suite retained from 14.0.
|
| 37 |
+
· Verification layer and hypothesis constructors unchanged.
|
| 38 |
"""
|
| 39 |
|
| 40 |
+
import time, random, math, threading, asyncio, warnings
|
| 41 |
from functools import reduce
|
| 42 |
from typing import Optional, Callable, List, Dict, Tuple, Any, Set
|
| 43 |
from dataclasses import dataclass, field
|
|
|
|
| 56 |
warnings.filterwarnings("ignore")
|
| 57 |
USE_GPU = torch.cuda.is_available()
|
| 58 |
DEVICE = torch.device("cuda" if USE_GPU else "cpu")
|
| 59 |
+
print(f"[SYSTEM 15.0] Compute: {'GPU' if USE_GPU else 'CPU'}")
|
| 60 |
|
| 61 |
# ══════════════════════════════════════════════════════════════════════
|
| 62 |
# SECTION 1: CONSTANTS
|
|
|
|
| 69 |
HUB_RESIDUAL_MULT = 2.0
|
| 70 |
HUB_DEGREE_RATIO = 0.6
|
| 71 |
MAX_HYPS_PER_AXIOM = 4
|
|
|
|
| 72 |
MANIFOLD_STEPS = [0.05, 0.2, -0.05, -0.2, 0.5, -0.5]
|
| 73 |
N_MPRT_EXPLORE = 20000 if USE_GPU else 3000
|
| 74 |
POLISH_STEPS = 40
|
| 75 |
ADAM_STEPS = 30
|
| 76 |
PROJECTION_CACHE: Dict = {}
|
| 77 |
+
RESONANCE_THRESHOLD = 0.95 # CE must drop to <95% of prior to count as resonant
|
| 78 |
|
| 79 |
# ══════════════════════════════════════════════════════════════════════
|
| 80 |
# SECTION 2: INTERVAL ARITHMETIC
|
|
|
|
| 239 |
if name not in bounds: variables.append(name); bounds[name]=(lo,hi)
|
| 240 |
if scope!="root" and name not in scope_vars[scope]: scope_vars[scope].append(name)
|
| 241 |
def add_con(kind,expr,direction,scope="root",weight=1.0,branches=None):
|
|
|
|
| 242 |
constraints.append(Constraint(kind,expr,direction,weight,scope,branches or []))
|
| 243 |
+
scope_groups[scope].append(len(constraints)-1)
|
| 244 |
try:
|
| 245 |
syms={v:sp.Symbol(v) for v in variables}
|
| 246 |
+
parsed=parse_expr(expr,local_dict=syms) if kind!="or_eq" else None
|
| 247 |
+
if parsed:
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 248 |
for v in variables:
|
| 249 |
if sp.Symbol(v) in parsed.free_symbols and scope!="root" and v not in scope_vars[scope]:
|
| 250 |
scope_vars[scope].append(v)
|
| 251 |
+
elif kind=="or_eq" and branches:
|
| 252 |
+
for b_str in branches:
|
| 253 |
+
p2=parse_expr(b_str,local_dict=syms)
|
| 254 |
+
for v in variables:
|
| 255 |
+
if sp.Symbol(v) in p2.free_symbols and scope!="root" and v not in scope_vars[scope]:
|
| 256 |
+
scope_vars[scope].append(v)
|
| 257 |
except: pass
|
| 258 |
for v in prog.vars: add_var(v.name,v.lo,v.hi)
|
| 259 |
for c in prog.constraints:
|
|
|
|
| 273 |
# ══════════════════════════════════════════════════════════════════════
|
| 274 |
@dataclass
|
| 275 |
class AXLInvariant:
|
| 276 |
+
name:str; expr:str; tolerance:float=VERIFY_G2_TOLERANCE; mode:str="eq"
|
|
|
|
| 277 |
|
| 278 |
@dataclass
|
| 279 |
class AXLProblemDef:
|
|
|
|
| 418 |
val=float(mc.fast_pt(*[b.get(v,0.0) for v in mc.syms_used]))
|
| 419 |
if mc.kind=="equality": total+=abs(val)*mc.weight
|
| 420 |
elif mc.direction=="geq": total+=max(0.0,-val)*mc.weight
|
| 421 |
+
else: total+=max(0.0,val)*mc.weight
|
| 422 |
except: total+=1.0
|
| 423 |
for v,(lo,hi) in self.bounds.items():
|
| 424 |
bv=b.get(v,0.0); total+=max(0.0,lo-bv)+max(0.0,bv-hi)
|
|
|
|
| 486 |
if not isinstance(val,np.ndarray): val=np.full(N,float(val),dtype=np.float32)
|
| 487 |
if mc.kind=="equality": total+=np.abs(val)*mc.weight
|
| 488 |
elif mc.direction=="geq": total+=np.maximum(0.0,-val)*mc.weight
|
| 489 |
+
else: total+=np.maximum(0.0,val)*mc.weight
|
| 490 |
except: total+=1.0
|
| 491 |
for i,v in enumerate(var_order):
|
| 492 |
lo,hi=self.bounds[v]; col=b_matrix[:,i]
|
|
|
|
| 494 |
return total
|
| 495 |
|
| 496 |
# ══════════════════════════════════════════════════════════════════════
|
| 497 |
+
# SECTION 6: VERIFY LAYER
|
| 498 |
# ══════════════════════════════════════════════════════════════════════
|
| 499 |
@dataclass
|
| 500 |
class VerifyResult:
|
|
|
|
| 504 |
failed_gates:List[str]=field(default_factory=list)
|
| 505 |
|
| 506 |
class VerifyLayer:
|
| 507 |
+
def run(self,binding,base_problem,anchors):
|
| 508 |
g1_ce=base_problem.constraint_energy(binding)
|
| 509 |
g1_pass=g1_ce<VERIFY_G1_THRESHOLD
|
| 510 |
g2={}
|
|
|
|
| 514 |
expr=parse_expr(inv.expr,local_dict=syms)
|
| 515 |
func=sp.lambdify(list(expr.free_symbols),expr,modules="math")
|
| 516 |
args=[binding.get(str(s),0.0) for s in expr.free_symbols]
|
| 517 |
+
val=float(func(*args)); err=abs(val)
|
|
|
|
| 518 |
if inv.mode=="eq": passed=err<inv.tolerance
|
| 519 |
+
elif inv.mode=="geq": passed=val>=-inv.tolerance
|
| 520 |
+
elif inv.mode=="leq": passed=val<=inv.tolerance
|
| 521 |
else: passed=err<inv.tolerance
|
| 522 |
g2[inv.name]=(round(val,6),passed)
|
| 523 |
except: g2[inv.name]=(999.0,False)
|
|
|
|
| 561 |
Axiom.IMPLICATION:"IMP",Axiom.NEGATION:"NEG",Axiom.COMPOSITE:"CMP",
|
| 562 |
Axiom.HOLISM:"HOL",Axiom.PARSIMONY:"PAR",Axiom.DUALITY:"DUA",
|
| 563 |
}
|
| 564 |
+
ADJACENT_CONTRADICTIONS: List[Tuple[str,str]] = [
|
| 565 |
(Axiom.DISCRETE,Axiom.CONTINUOUS),(Axiom.INJECTIVE,Axiom.SURJECTIVE),
|
| 566 |
(Axiom.ORDERED,Axiom.SYMMETRIC),(Axiom.ATOMIC,Axiom.COMPOSITE),
|
| 567 |
(Axiom.CONSERVED,Axiom.MUTABLE),(Axiom.PARSIMONY,Axiom.ENTROPY),
|
|
|
|
| 570 |
]
|
| 571 |
_CONTRA_SET={frozenset(p) for p in ADJACENT_CONTRADICTIONS}
|
| 572 |
|
| 573 |
+
def sequence_valid(seq: List[str]) -> bool:
|
| 574 |
for i in range(len(seq)-1):
|
| 575 |
if frozenset([seq[i],seq[i+1]]) in _CONTRA_SET: return False
|
| 576 |
return True
|
|
|
|
| 578 |
# ══════════════════════════════════════════════════════════════════════
|
| 579 |
# SECTION 8: SHARED DATACLASSES
|
| 580 |
# ══════════════════════════════════════════════════════════════════════
|
| 581 |
+
# Ray types — what kind of creative move generated this ray
|
| 582 |
+
RAY_SEED = "seed" # 🌱 single axiom starter
|
| 583 |
+
RAY_BRANCH = "branch" # 🌿 earned child of a tree ray
|
| 584 |
+
RAY_TENSION = "tension" # ⚡ mediated contradiction sequence
|
| 585 |
+
RAY_SCOUT = "scout" # 🔭 random valid sequence
|
| 586 |
+
RAY_RECOMBINE = "recombine" # 🧬 genetic crossover of two rays
|
| 587 |
+
RAY_INVERT = "invert" # 🔄 reversed successful sequence
|
| 588 |
+
|
| 589 |
+
RAY_ICONS = {
|
| 590 |
+
RAY_SEED:"🌱", RAY_BRANCH:"🌿", RAY_TENSION:"⚡",
|
| 591 |
+
RAY_SCOUT:"🔭", RAY_RECOMBINE:"🧬", RAY_INVERT:"🔄",
|
| 592 |
+
}
|
| 593 |
+
|
| 594 |
@dataclass
|
| 595 |
class Hypothesis:
|
| 596 |
hid:str; binding:Dict[str,float]; h_type:str; claim:str
|
|
|
|
| 599 |
|
| 600 |
@dataclass
|
| 601 |
class Baton:
|
| 602 |
+
"""Partial solution passed between rays. A ray never fails — it terminates."""
|
| 603 |
binding:Dict[str,float]; ce:float
|
| 604 |
ray_id:str=""; depth:int=0
|
| 605 |
l7:Optional[Any]=None; l9:Optional[Any]=None
|
| 606 |
|
| 607 |
@dataclass
|
| 608 |
class AxiomRay:
|
| 609 |
+
"""
|
| 610 |
+
An ordered sequence of axioms. [A→B→C] ≠ [C→B→A].
|
| 611 |
+
Now carries ray_type so we can track which creative move generated it.
|
| 612 |
+
"""
|
| 613 |
+
sequence: List[str]
|
| 614 |
+
ray_id: str
|
| 615 |
+
ray_type: str = RAY_SEED
|
| 616 |
+
depth: int = 0
|
| 617 |
+
parent_id: Optional[str] = None
|
| 618 |
+
baton: Optional[Baton] = None
|
| 619 |
+
|
| 620 |
@property
|
| 621 |
def name(self) -> str:
|
| 622 |
return "→".join(AXIOM_ABBR.get(a,a[:3]) for a in self.sequence)
|
| 623 |
+
|
| 624 |
+
def extend(self, axiom:str, rtype:str=RAY_BRANCH) -> Optional['AxiomRay']:
|
| 625 |
+
new_seq = self.sequence + [axiom]
|
| 626 |
if sequence_valid(new_seq):
|
| 627 |
+
return AxiomRay(
|
| 628 |
+
sequence = new_seq,
|
| 629 |
+
ray_id = f"{self.ray_id}+{AXIOM_ABBR.get(axiom,'?')}",
|
| 630 |
+
ray_type = rtype,
|
| 631 |
+
depth = self.depth + 1,
|
| 632 |
+
parent_id = self.ray_id,
|
| 633 |
+
)
|
| 634 |
return None
|
| 635 |
|
| 636 |
@dataclass
|
| 637 |
class HypothesisTrace:
|
| 638 |
+
hid:str; round_idx:int; ray_name:str; ray_type:str; action:str
|
| 639 |
ce_before:float; ce_after:float
|
| 640 |
verify:Optional[VerifyResult]; survived:bool; elapsed_ms:float
|
| 641 |
depth:int=0; parent_id:str=""
|
| 642 |
|
| 643 |
@dataclass
|
| 644 |
class StructuralModel:
|
| 645 |
+
best_binding: Dict[str,float]
|
| 646 |
+
best_ce: float
|
| 647 |
+
failure_patterns: Set[str] = field(default_factory=set)
|
| 648 |
+
scope_witnesses: Dict[str,Dict[str,Tuple]] = field(default_factory=dict)
|
| 649 |
+
# Resonant pairs — discovered in-run, zero cross-run bias
|
| 650 |
+
# (axiom_a, axiom_b) means a→b produced meaningful CE reduction
|
| 651 |
+
resonant_pairs: List[Tuple[str,str]] = field(default_factory=list)
|
| 652 |
|
| 653 |
# ══════════════════════════════════════════════════════════════════════
|
| 654 |
# SECTION 9: ORACLES
|
|
|
|
| 839 |
return best_b,best_ce
|
| 840 |
|
| 841 |
# ══════════════════════════════════════════════════════════════════════
|
| 842 |
+
# SECTION 11: HYPOTHESIS CONSTRUCTORS (27 axioms, unchanged from 14.0)
|
| 843 |
# ══════════════════════════════════════════════════════════════════════
|
| 844 |
def _proj_val(mc,v,b):
|
| 845 |
if v not in mc.projections: return None
|
|
|
|
| 919 |
def _hyp_bilinear(problem,baton,all_batons,model):
|
| 920 |
hyps=[]; b=dict(baton.binding)
|
| 921 |
for mc in problem.compiled_constraints:
|
| 922 |
+
if not mc.parsed or not mc.parsed.is_Add: continue
|
|
|
|
| 923 |
for term in mc.parsed.args:
|
| 924 |
if not term.is_Mul: continue
|
| 925 |
syms_in=[str(s) for s in term.free_symbols if str(s) in problem.variables]
|
|
|
|
| 938 |
def _hyp_metric(problem,baton,all_batons,model):
|
| 939 |
hyps=[]; b=dict(baton.binding)
|
| 940 |
for mc in problem.compiled_constraints:
|
| 941 |
+
if mc.kind!="equality" or not mc.parsed or not mc.parsed.is_Add: continue
|
|
|
|
| 942 |
sq_terms=[t for t in mc.parsed.args if t.is_Pow and t.args[1]==2]
|
| 943 |
if len(sq_terms)<2: continue
|
| 944 |
vars_in=[str(s) for s in mc.parsed.free_symbols if str(s) in problem.variables]
|
|
|
|
| 974 |
b=dict(baton.binding); nb=dict(b)
|
| 975 |
ord_mcs=[mc for mc in problem.compiled_constraints if mc.kind=="inequality" and len(mc.syms_used)==2]
|
| 976 |
for mc in ord_mcs:
|
|
|
|
| 977 |
vi,vj=mc.syms_used[0],mc.syms_used[1]
|
| 978 |
+
lo_i,_=problem.bounds.get(vi,(-1e18,1e18)); _,hi_j=problem.bounds.get(vj,(-1e18,1e18))
|
| 979 |
if mc.direction=="geq" and nb.get(vi,0)<nb.get(vj,0):
|
| 980 |
mid=(nb[vi]+nb[vj])/2; nb[vi]=max(lo_i,mid); nb[vj]=min(hi_j,mid)
|
| 981 |
return [_make_hyp(f"ord_{hash(str(nb))%9999}",nb,"ordered","OrderBal",["ordered"],{},list(problem.variables),0.67)]
|
|
|
|
| 1132 |
changed=False; iters+=1
|
| 1133 |
for mc in problem.compiled_constraints:
|
| 1134 |
if mc.kind!="equality" or not mc.projections: continue
|
| 1135 |
+
for v in mc.projections:
|
| 1136 |
val=_proj_val(mc,v,nb)
|
| 1137 |
if val is None: continue
|
| 1138 |
lo,hi=problem.bounds.get(v,(-1e18,1e18))
|
|
|
|
| 1254 |
return hyps
|
| 1255 |
|
| 1256 |
AXIOM_CONSTRUCTORS:Dict[str,Callable]={
|
| 1257 |
+
Axiom.CONTINUOUS:_hyp_continuous, Axiom.DISCRETE:_hyp_discrete,
|
| 1258 |
+
Axiom.QUADRATIC:_hyp_quadratic, Axiom.BILINEAR:_hyp_bilinear,
|
| 1259 |
+
Axiom.METRIC:_hyp_metric, Axiom.SYMMETRIC:_hyp_symmetric,
|
| 1260 |
+
Axiom.ORDERED:_hyp_ordered, Axiom.MONOTONE:_hyp_monotone,
|
| 1261 |
+
Axiom.CONVEX:_hyp_convex, Axiom.CONSERVED:_hyp_conserved,
|
| 1262 |
+
Axiom.MUTABLE:_hyp_mutable, Axiom.NETWORK:_hyp_network,
|
| 1263 |
Axiom.EQUILIBRIUM:_hyp_equilibrium,Axiom.SUPERPOSITION:_hyp_superposition,
|
| 1264 |
+
Axiom.LOCALITY:_hyp_locality, Axiom.EXTREMAL:_hyp_extremal,
|
| 1265 |
+
Axiom.ENTROPY:_hyp_entropy, Axiom.INJECTIVE:_hyp_injective,
|
| 1266 |
+
Axiom.SURJECTIVE:_hyp_surjective, Axiom.TRANSITIVE:_hyp_transitive,
|
| 1267 |
+
Axiom.ATOMIC:_hyp_atomic, Axiom.IMPLICATION:_hyp_implication,
|
| 1268 |
+
Axiom.NEGATION:_hyp_negation, Axiom.COMPOSITE:_hyp_composite,
|
| 1269 |
+
Axiom.HOLISM:_hyp_holism, Axiom.PARSIMONY:_hyp_parsimony,
|
| 1270 |
+
Axiom.DUALITY:_hyp_duality,
|
| 1271 |
}
|
| 1272 |
|
| 1273 |
# ══════════════════════════════════════════════════════════════════════
|
| 1274 |
+
# SECTION 12: SEQUENCE HYPOTHESIS GENERATOR
|
| 1275 |
+
# Now tracks resonant pairs — consecutive axioms that both produce
|
| 1276 |
+
# meaningful CE reduction are recorded for this run.
|
| 1277 |
# ══════════════════════════════════════════════════════════════════════
|
| 1278 |
class SequenceHypothesisGenerator:
|
| 1279 |
+
def generate(self, sequence:List[str], problem:Problem,
|
| 1280 |
+
baton:Baton, all_batons:List[Baton],
|
| 1281 |
+
model:StructuralModel) -> Tuple[List[Hypothesis],Baton]:
|
| 1282 |
accumulated:List[Hypothesis]=[]; current=baton
|
| 1283 |
+
prev_axiom:Optional[str]=None; prev_ce=baton.ce
|
| 1284 |
+
|
| 1285 |
for i,axiom in enumerate(sequence):
|
| 1286 |
constructor=AXIOM_CONSTRUCTORS.get(axiom)
|
| 1287 |
if not constructor: continue
|
| 1288 |
+
|
| 1289 |
if current.l7 is None:
|
| 1290 |
active=[s for s in problem.scope_order if s!="root" and problem.scope_vars.get(s)]
|
| 1291 |
current.l7=TOPOLOGY_ORACLE.evaluate(problem,active)
|
| 1292 |
if current.l9 is None:
|
| 1293 |
hubs=current.l7.hub_vars if current.l7 else []
|
| 1294 |
current.l9=RESIDUAL_ORACLE.evaluate(current.binding,problem,hubs)
|
| 1295 |
+
|
| 1296 |
new_hyps=constructor(problem,current,all_batons,model)
|
| 1297 |
accumulated.extend(new_hyps)
|
| 1298 |
+
|
| 1299 |
best_ce=current.ce; best_b=current.binding
|
| 1300 |
for hyp in sorted(new_hyps,key=lambda h:-h.confidence)[:MAX_HYPS_PER_AXIOM]:
|
| 1301 |
if hyp.hid in model.failure_patterns: continue
|
| 1302 |
tb,tce=_test_hypothesis(problem,hyp)
|
| 1303 |
if tce<best_ce: best_ce=tce; best_b=tb
|
| 1304 |
+
|
| 1305 |
if best_ce<current.ce:
|
| 1306 |
+
# Resonance detection: both this axiom AND the previous one reduced CE
|
| 1307 |
+
if prev_axiom and best_ce < prev_ce * RESONANCE_THRESHOLD:
|
| 1308 |
+
pair=(prev_axiom, axiom)
|
| 1309 |
+
if pair not in model.resonant_pairs:
|
| 1310 |
+
model.resonant_pairs.append(pair)
|
| 1311 |
+
prev_ce=current.ce
|
| 1312 |
+
current=Baton(binding=best_b,ce=best_ce,
|
| 1313 |
+
ray_id=current.ray_id,depth=i+1,l7=None,l9=None)
|
| 1314 |
+
|
| 1315 |
+
prev_axiom=axiom
|
| 1316 |
+
|
| 1317 |
return accumulated,current
|
| 1318 |
|
| 1319 |
+
# ══════════════════════════════════════════════════════════════════════
|
| 1320 |
+
# SECTION 13: CREATIVE SEEDER
|
| 1321 |
+
# Generates four categories of novel rays beyond the seed tree.
|
| 1322 |
+
# All creativity is structural — derived from axiom space topology
|
| 1323 |
+
# and in-run resonance discovery. Zero cross-run bias.
|
| 1324 |
+
# ══════════════════════════════════════════════════════════════════════
|
| 1325 |
+
class CreativeSeeder:
|
| 1326 |
+
"""
|
| 1327 |
+
The four creative moves:
|
| 1328 |
+
|
| 1329 |
+
1. TENSION: mediated contradictions [A→B→C] where (A,C) are in
|
| 1330 |
+
ADJACENT_CONTRADICTIONS but B mediates. CO₂ molecules.
|
| 1331 |
+
Stable structures from reactive parts.
|
| 1332 |
+
|
| 1333 |
+
2. SCOUT: fully random valid sequences, length 3-8.
|
| 1334 |
+
Pure cartographers. No earning required.
|
| 1335 |
+
|
| 1336 |
+
3. RECOMBINE: single-point crossover of two proven sequences.
|
| 1337 |
+
Front of seq_a + compatible tail of seq_b.
|
| 1338 |
+
|
| 1339 |
+
4. INVERT: reversed sequence. Same axioms, opposite order.
|
| 1340 |
+
The problem approached from the other end.
|
| 1341 |
+
"""
|
| 1342 |
+
|
| 1343 |
+
def tension_seeds(self, max_n:int=60) -> List[AxiomRay]:
|
| 1344 |
+
"""
|
| 1345 |
+
For every contradiction pair (A,C), find all B that mediate.
|
| 1346 |
+
[A→B→C]: A and C contradict directly but B makes both steps valid.
|
| 1347 |
+
These are seeds — they get to run from the beginning, no earning.
|
| 1348 |
+
"""
|
| 1349 |
+
results:List[AxiomRay]=[]
|
| 1350 |
+
for (a,c) in ADJACENT_CONTRADICTIONS:
|
| 1351 |
+
for b in ALL_AXIOMS:
|
| 1352 |
+
if b in (a,c): continue
|
| 1353 |
+
if (frozenset([a,b]) not in _CONTRA_SET and
|
| 1354 |
+
frozenset([b,c]) not in _CONTRA_SET):
|
| 1355 |
+
seq=[a,b,c]
|
| 1356 |
+
ab=AXIOM_ABBR; rid=f"T_{ab.get(a,a[:3])}_{ab.get(b,b[:3])}_{ab.get(c,c[:3])}"
|
| 1357 |
+
results.append(AxiomRay(sequence=seq,ray_id=rid,ray_type=RAY_TENSION,depth=0))
|
| 1358 |
+
# Extend to length 4: any D where C→D is valid
|
| 1359 |
+
for d in ALL_AXIOMS:
|
| 1360 |
+
if d not in seq and frozenset([c,d]) not in _CONTRA_SET:
|
| 1361 |
+
seq4=seq+[d]; rid4=f"{rid}_{ab.get(d,d[:3])}"
|
| 1362 |
+
results.append(AxiomRay(sequence=seq4,ray_id=rid4,ray_type=RAY_TENSION,depth=0))
|
| 1363 |
+
random.shuffle(results)
|
| 1364 |
+
return results[:max_n]
|
| 1365 |
+
|
| 1366 |
+
def random_scouts(self, n:int=25) -> List[AxiomRay]:
|
| 1367 |
+
"""
|
| 1368 |
+
Fully random valid sequences, length 3-8.
|
| 1369 |
+
Pure exploration — no earning required to spawn children.
|
| 1370 |
+
"""
|
| 1371 |
+
scouts:List[AxiomRay]=[]; attempts=0
|
| 1372 |
+
while len(scouts)<n and attempts<n*30:
|
| 1373 |
+
attempts+=1
|
| 1374 |
+
length=random.randint(3,min(8,len(ALL_AXIOMS)))
|
| 1375 |
+
pool=list(ALL_AXIOMS); random.shuffle(pool)
|
| 1376 |
+
seq=[pool[0]]
|
| 1377 |
+
for ax in pool[1:]:
|
| 1378 |
+
if len(seq)>=length: break
|
| 1379 |
+
if frozenset([seq[-1],ax]) not in _CONTRA_SET:
|
| 1380 |
+
seq.append(ax)
|
| 1381 |
+
if len(seq)>=3:
|
| 1382 |
+
rid=f"SC_{''.join(AXIOM_ABBR.get(a,a[:2]) for a in seq)}"
|
| 1383 |
+
scouts.append(AxiomRay(sequence=seq,ray_id=rid,ray_type=RAY_SCOUT,depth=0))
|
| 1384 |
+
return scouts
|
| 1385 |
+
|
| 1386 |
+
def recombine(self, ray_a:AxiomRay, ray_b:AxiomRay, baton:Baton) -> List[AxiomRay]:
|
| 1387 |
+
"""
|
| 1388 |
+
Single-point crossover. For each cut point, take the front of ray_a
|
| 1389 |
+
and graft on the tail of ray_b (filtering axioms already present).
|
| 1390 |
+
"""
|
| 1391 |
+
results:List[AxiomRay]=[]; ab=AXIOM_ABBR
|
| 1392 |
+
seq_a,seq_b=ray_a.sequence,ray_b.sequence
|
| 1393 |
+
for cut in range(1,min(len(seq_a),len(seq_b))):
|
| 1394 |
+
head=seq_a[:cut]
|
| 1395 |
+
tail=[x for x in seq_b[cut:] if x not in head]
|
| 1396 |
+
candidate=head+tail
|
| 1397 |
+
if len(candidate)>=2 and sequence_valid(candidate):
|
| 1398 |
+
rid=f"RC_{ray_a.ray_id[:8]}x{ray_b.ray_id[:8]}_c{cut}"
|
| 1399 |
+
child=AxiomRay(sequence=candidate,ray_id=rid,ray_type=RAY_RECOMBINE,
|
| 1400 |
+
depth=0,parent_id=f"{ray_a.ray_id}+{ray_b.ray_id}",
|
| 1401 |
+
baton=baton)
|
| 1402 |
+
results.append(child)
|
| 1403 |
+
return results
|
| 1404 |
+
|
| 1405 |
+
def invert(self, ray:AxiomRay, baton:Baton) -> Optional[AxiomRay]:
|
| 1406 |
+
"""
|
| 1407 |
+
Reverse the sequence. Same mathematical worldviews, opposite encounter order.
|
| 1408 |
+
"""
|
| 1409 |
+
inv=list(reversed(ray.sequence))
|
| 1410 |
+
if sequence_valid(inv) and inv!=ray.sequence:
|
| 1411 |
+
rid=f"INV_{ray.ray_id}"
|
| 1412 |
+
return AxiomRay(sequence=inv,ray_id=rid,ray_type=RAY_INVERT,
|
| 1413 |
+
depth=0,parent_id=ray.ray_id,baton=baton)
|
| 1414 |
+
return None
|
| 1415 |
+
|
| 1416 |
+
def resonance_extensions(self, ray:AxiomRay, baton:Baton,
|
| 1417 |
+
resonant_pairs:List[Tuple[str,str]]) -> List[AxiomRay]:
|
| 1418 |
+
"""
|
| 1419 |
+
If the ray ends with axiom A, and (A,B) is a discovered resonant pair,
|
| 1420 |
+
generate A→B as a priority branch. These are in-run discoveries — the
|
| 1421 |
+
system follows its own sensed potency for THIS problem.
|
| 1422 |
+
"""
|
| 1423 |
+
if not ray.sequence or not resonant_pairs: return []
|
| 1424 |
+
last=ray.sequence[-1]; results:List[AxiomRay]=[]
|
| 1425 |
+
resonant_nexts=[b for (a,b) in resonant_pairs if a==last and b not in ray.sequence]
|
| 1426 |
+
for b in resonant_nexts:
|
| 1427 |
+
child=ray.extend(b, RAY_BRANCH)
|
| 1428 |
+
if child:
|
| 1429 |
+
child.baton=baton
|
| 1430 |
+
child.ray_id=f"RES_{child.ray_id}"
|
| 1431 |
+
results.append(child)
|
| 1432 |
+
return results
|
| 1433 |
+
|
| 1434 |
+
CREATIVE_SEEDER=CreativeSeeder()
|
| 1435 |
|
| 1436 |
+
# ══════════════════════════════════════════════════════════════════════
|
| 1437 |
+
# SECTION 14: SEQUENCE RAY TRACER (15.0 — Creative Architecture)
|
| 1438 |
+
# ══════════════════════════════════════════════════════════════════════
|
| 1439 |
+
class SequenceRayTracer:
|
| 1440 |
+
MAX_TOTAL_RAYS = 100 # more budget for creative exploration
|
| 1441 |
+
BRANCH_WIDTH = 3 # branches per earned ray
|
| 1442 |
+
MIN_DEPTH = 1 # depth below which branching is always free
|
| 1443 |
+
CE_EARN_RATIO = 0.90 # 10% reduction earns a branch
|
| 1444 |
+
# Scouts bypass earning — they always get to branch if CE < threshold
|
| 1445 |
+
SCOUT_CE_THRESHOLD = 0.5
|
| 1446 |
+
|
| 1447 |
+
def trace(self, axl_def:AXLProblemDef, base_problem:Problem) -> Tuple[Dict,float,List[Dict]]:
|
| 1448 |
all_traces:List[HypothesisTrace]=[]; generator=SequenceHypothesisGenerator()
|
| 1449 |
+
|
| 1450 |
+
# ── Initial queue: seeds + tension seeds + scouts (interleaved) ──
|
| 1451 |
+
seed_rays=[AxiomRay(sequence=[a],ray_id=f"S{i}",ray_type=RAY_SEED,depth=0)
|
| 1452 |
+
for i,a in enumerate(ALL_AXIOMS)]
|
| 1453 |
+
tension_rays=CREATIVE_SEEDER.tension_seeds(max_n=50)
|
| 1454 |
+
scout_rays=CREATIVE_SEEDER.random_scouts(n=20)
|
| 1455 |
+
|
| 1456 |
+
# Interleave: seed, tension, scout, seed, tension, scout ...
|
| 1457 |
+
# This ensures we don't exhaust the budget on one category
|
| 1458 |
+
active:List[AxiomRay]=[]
|
| 1459 |
+
buckets=[seed_rays, tension_rays, scout_rays]
|
| 1460 |
+
random.shuffle(seed_rays); random.shuffle(tension_rays); random.shuffle(scout_rays)
|
| 1461 |
+
max_len=max(len(b) for b in buckets)
|
| 1462 |
+
for i in range(max_len):
|
| 1463 |
+
for bucket in buckets:
|
| 1464 |
+
if i<len(bucket): active.append(bucket[i])
|
| 1465 |
+
|
| 1466 |
+
all_batons:List[Baton]=[]; best_ce=float('inf'); best_binding:Dict={}
|
| 1467 |
+
history:List[Dict]=[]; total_fired=0
|
| 1468 |
+
# Track successful rays for recombination
|
| 1469 |
+
successful_rays:List[AxiomRay]=[]
|
| 1470 |
|
| 1471 |
init_b={v:(lo+hi)/2 for v,(lo,hi) in base_problem.bounds.items()}
|
| 1472 |
init_ce=base_problem.constraint_energy(init_b)
|
|
|
|
| 1476 |
{v:IV(*base_problem.bounds[v]) for v in base_problem.variables},N_MPRT_EXPLORE//5)
|
| 1477 |
if mprt_ce<init_ce: init_b=mprt_b; init_ce=mprt_ce
|
| 1478 |
seed_baton=Baton(binding=init_b,ce=init_ce,ray_id="SEED")
|
| 1479 |
+
|
| 1480 |
+
# Shared structural model (per-run, carries resonant_pairs)
|
| 1481 |
+
shared_model=StructuralModel(best_binding=init_b,best_ce=init_ce)
|
| 1482 |
self._last_traces=all_traces
|
| 1483 |
|
| 1484 |
+
print(f"\n{'═'*65}\nCREATIVE RAY TRACE 15.0: {axl_def.name}\n{'═'*65}")
|
| 1485 |
+
|
| 1486 |
while active and total_fired<self.MAX_TOTAL_RAYS:
|
| 1487 |
ray=active.pop(0); total_fired+=1
|
| 1488 |
parent_baton=ray.baton or seed_baton
|
| 1489 |
+
|
| 1490 |
+
# Update shared model
|
| 1491 |
+
shared_model.best_binding=best_binding if best_binding else parent_baton.binding
|
| 1492 |
+
shared_model.best_ce=best_ce if best_ce<float('inf') else init_ce
|
| 1493 |
+
|
| 1494 |
t0=time.time()
|
| 1495 |
+
hyps,output_baton=generator.generate(
|
| 1496 |
+
ray.sequence,base_problem,parent_baton,all_batons,shared_model)
|
| 1497 |
elapsed=round((time.time()-t0)*1000,1)
|
| 1498 |
output_baton.ray_id=ray.ray_id; all_batons.append(output_baton)
|
| 1499 |
+
|
| 1500 |
+
improved=output_baton.ce<best_ce
|
| 1501 |
+
if improved:
|
| 1502 |
+
best_ce=output_baton.ce; best_binding=dict(output_baton.binding)
|
| 1503 |
+
successful_rays.append(ray)
|
| 1504 |
+
|
| 1505 |
verify=VERIFY_LAYER.run(output_baton.binding,base_problem,axl_def.anchors)
|
| 1506 |
trace=HypothesisTrace(
|
| 1507 |
+
hid=ray.ray_id,round_idx=total_fired,ray_name=ray.name,
|
| 1508 |
+
ray_type=ray.ray_type,action="CreativeRay",
|
| 1509 |
ce_before=parent_baton.ce if parent_baton.ce<float('inf') else 99.0,
|
| 1510 |
ce_after=output_baton.ce,verify=verify,survived=verify.overall_pass,
|
| 1511 |
elapsed_ms=elapsed,depth=ray.depth,parent_id=ray.parent_id or "")
|
| 1512 |
all_traces.append(trace)
|
| 1513 |
+
|
| 1514 |
+
icon=RAY_ICONS.get(ray.ray_type,"·")
|
| 1515 |
+
status="✓" if verify.overall_pass else ""
|
| 1516 |
+
print(f" [{total_fired:3d}]{icon} {ray.name:<38} "
|
| 1517 |
+
f"CE {parent_baton.ce:.4f}→{output_baton.ce:.4f} "
|
| 1518 |
+
f"G1={'✓' if verify.gate1_pass else '✗'} "
|
| 1519 |
+
f"G2={'✓' if verify.gate2_pass else '✗'} {status}")
|
| 1520 |
+
|
| 1521 |
+
history.append({
|
| 1522 |
+
"ray_id":ray.ray_id,"sequence":ray.name,"ray_type":ray.ray_type,
|
| 1523 |
+
"depth":ray.depth,"parent":ray.parent_id,
|
| 1524 |
+
"ce_in":round(parent_baton.ce if parent_baton.ce<float('inf') else 99,5),
|
| 1525 |
"ce_out":round(output_baton.ce,5),"survived":verify.overall_pass,"ms":elapsed})
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1526 |
|
| 1527 |
+
if verify.overall_pass:
|
| 1528 |
+
print(f"\n✓ TRUE UNIVERSE FOUND: {icon} {ray.name}")
|
| 1529 |
+
break
|
| 1530 |
+
|
| 1531 |
+
# ── Branching decisions ───────────────────────────────────
|
| 1532 |
+
parent_ce=parent_baton.ce if parent_baton.ce<float('inf') else init_ce
|
| 1533 |
+
earned=(output_baton.ce<parent_ce*self.CE_EARN_RATIO
|
| 1534 |
+
or ray.depth<self.MIN_DEPTH)
|
| 1535 |
+
scout_earned=(ray.ray_type==RAY_SCOUT
|
| 1536 |
+
and output_baton.ce<self.SCOUT_CE_THRESHOLD)
|
| 1537 |
+
|
| 1538 |
+
new_children:List[AxiomRay]=[]
|
| 1539 |
+
|
| 1540 |
+
if earned or scout_earned:
|
| 1541 |
+
# 1. Standard tree branches (resonance-guided)
|
| 1542 |
+
new_children.extend(
|
| 1543 |
+
self._spawn_tree_children(ray,output_baton,shared_model.resonant_pairs))
|
| 1544 |
+
|
| 1545 |
+
# 2. Inversion of this ray
|
| 1546 |
+
inv=CREATIVE_SEEDER.invert(ray,output_baton)
|
| 1547 |
+
if inv: new_children.append(inv)
|
| 1548 |
+
|
| 1549 |
+
# 3. Recombination with a random successful ray
|
| 1550 |
+
if len(successful_rays)>=2:
|
| 1551 |
+
partner=random.choice([r for r in successful_rays if r.ray_id!=ray.ray_id]
|
| 1552 |
+
or successful_rays)
|
| 1553 |
+
new_children.extend(
|
| 1554 |
+
CREATIVE_SEEDER.recombine(ray,partner,output_baton)[:2])
|
| 1555 |
+
|
| 1556 |
+
# 4. Resonance-guided extensions
|
| 1557 |
+
new_children.extend(
|
| 1558 |
+
CREATIVE_SEEDER.resonance_extensions(
|
| 1559 |
+
ray,output_baton,shared_model.resonant_pairs))
|
| 1560 |
+
|
| 1561 |
+
# Depth-first: branches at front; inversions/recombinations at back
|
| 1562 |
+
branches=[c for c in new_children if c.ray_type==RAY_BRANCH]
|
| 1563 |
+
creative=[c for c in new_children if c.ray_type!=RAY_BRANCH]
|
| 1564 |
+
active=branches+active+creative
|
| 1565 |
+
|
| 1566 |
+
survived=[t for t in all_traces if t.survived]
|
| 1567 |
+
best_t=min(survived,key=lambda t:t.ce_after,default=None)
|
| 1568 |
+
print(f"\n{'─'*65}")
|
| 1569 |
+
print(f"RESULT: CE={best_ce:.5f} | Fired={total_fired} | "
|
| 1570 |
+
f"Survived={len(survived)} | Best={best_t.ray_name if best_t else '—'}")
|
| 1571 |
+
print(f"Resonant pairs discovered: {shared_model.resonant_pairs}")
|
| 1572 |
return best_binding,best_ce,history
|
| 1573 |
|
| 1574 |
+
def _spawn_tree_children(self, ray:AxiomRay, baton:Baton,
|
| 1575 |
+
resonant_pairs:List[Tuple[str,str]]) -> List[AxiomRay]:
|
| 1576 |
+
"""
|
| 1577 |
+
Standard branch children, but prioritised by resonant pairs.
|
| 1578 |
+
If the ray ends with A and (A,B) is resonant, B goes first.
|
| 1579 |
+
"""
|
| 1580 |
+
last=ray.sequence[-1] if ray.sequence else None
|
| 1581 |
+
resonant_nexts=([b for (a,b) in resonant_pairs if a==last and b not in ray.sequence]
|
| 1582 |
+
if last else [])
|
| 1583 |
+
remaining=[a for a in ALL_AXIOMS if a not in ray.sequence]
|
| 1584 |
+
random.shuffle(remaining)
|
| 1585 |
+
# Resonant candidates first, then random
|
| 1586 |
+
priority=resonant_nexts+[a for a in remaining if a not in resonant_nexts]
|
| 1587 |
+
children:List[AxiomRay]=[]; count=0
|
| 1588 |
+
for axiom in priority:
|
| 1589 |
+
if count>=self.BRANCH_WIDTH*2: break
|
| 1590 |
+
child=ray.extend(axiom, RAY_BRANCH)
|
| 1591 |
+
if child: child.baton=baton; children.append(child); count+=1
|
| 1592 |
+
return children
|
| 1593 |
+
|
| 1594 |
# ══════════════════════════════════════════════════════════════════════
|
| 1595 |
+
# SECTION 15: AXL PROBLEMS (14 real-world domains from 14.0)
|
| 1596 |
# ══════════════════════════════════════════════════════════════════════
|
|
|
|
|
|
|
| 1597 |
PROBLEM_META={
|
| 1598 |
"EllipticCurvePoint": {"domain":"Cryptography", "icon":"🔐","difficulty":"Medium"},
|
| 1599 |
"MarkowitzPortfolio": {"domain":"Finance", "icon":"📈","difficulty":"Hard"},
|
|
|
|
| 1612 |
}
|
| 1613 |
|
| 1614 |
AXL_PROBLEMS=[
|
|
|
|
|
|
|
| 1615 |
AXLProblemDef(
|
| 1616 |
name="EllipticCurvePoint",
|
| 1617 |
+
description="Find point on E: y²=x³-x+1. Observe x=0, find y=±1.",
|
| 1618 |
axioms={Axiom.CONTINUOUS,Axiom.QUADRATIC,Axiom.METRIC,Axiom.SYMMETRIC},
|
| 1619 |
variables=[{"name":"ex","lo":-2.0,"hi":2.0},{"name":"ey","lo":-2.0,"hi":2.0}],
|
| 1620 |
+
constraints=[{"kind":"EQ","expr":"ey**2 - ex**3 + ex - 1","weight":5.0}],
|
|
|
|
|
|
|
|
|
|
| 1621 |
scopes=[{"name":"curve","order":0,"vars":["ex","ey"],
|
| 1622 |
"constraints":[{"kind":"EQ","expr":"ey**2 - ex**3 + ex - 1","weight":8.0}]}],
|
| 1623 |
anchors=[AXLInvariant("on_curve","ey**2 - ex**3 + ex - 1",1e-3)],
|
| 1624 |
+
observations={"ex":0.0},
|
| 1625 |
),
|
|
|
|
|
|
|
| 1626 |
AXLProblemDef(
|
| 1627 |
name="MarkowitzPortfolio",
|
| 1628 |
+
description="4-asset portfolio: budget=1, return=11%, min variance.",
|
|
|
|
| 1629 |
axioms={Axiom.CONSERVED,Axiom.ORDERED,Axiom.METRIC,Axiom.HOLISM},
|
| 1630 |
+
variables=[{"name":"w1","lo":0.0,"hi":1.0},{"name":"w2","lo":0.0,"hi":1.0},
|
| 1631 |
+
{"name":"w3","lo":0.0,"hi":1.0},{"name":"w4","lo":0.0,"hi":1.0}],
|
|
|
|
|
|
|
| 1632 |
constraints=[
|
| 1633 |
+
{"kind":"CONSERVE","expr":"w1+w2+w3+w4-1.0"},
|
| 1634 |
+
{"kind":"EQ","expr":"0.10*w1+0.12*w2+0.08*w3+0.15*w4-0.11","weight":3.0},
|
| 1635 |
{"kind":"GEQ","expr":"w1","weight":1.0},{"kind":"GEQ","expr":"w2","weight":1.0},
|
| 1636 |
{"kind":"GEQ","expr":"w3","weight":1.0},{"kind":"GEQ","expr":"w4","weight":1.0},
|
| 1637 |
],
|
| 1638 |
scopes=[{"name":"portfolio","order":0,"vars":["w1","w2","w3","w4"],
|
| 1639 |
"constraints":[
|
| 1640 |
+
{"kind":"EQ","expr":"w1+w2+w3+w4-1.0","weight":5.0},
|
| 1641 |
+
{"kind":"EQ","expr":"0.10*w1+0.12*w2+0.08*w3+0.15*w4-0.11","weight":3.0},
|
|
|
|
| 1642 |
]}],
|
| 1643 |
anchors=[
|
| 1644 |
AXLInvariant("budget","w1+w2+w3+w4-1.0",1e-3),
|
| 1645 |
AXLInvariant("return_target","0.10*w1+0.12*w2+0.08*w3+0.15*w4-0.11",5e-3),
|
| 1646 |
+
AXLInvariant("w1_pos","w1",1e-3,"geq"),AXLInvariant("w2_pos","w2",1e-3,"geq"),
|
| 1647 |
+
AXLInvariant("w3_pos","w3",1e-3,"geq"),AXLInvariant("w4_pos","w4",1e-3,"geq"),
|
|
|
|
|
|
|
| 1648 |
],
|
|
|
|
| 1649 |
),
|
|
|
|
|
|
|
| 1650 |
AXLProblemDef(
|
| 1651 |
name="PowerFlowDC3Bus",
|
| 1652 |
+
description="DC power flow 3-bus. pt2≈-0.318, pt3≈0.046.",
|
|
|
|
| 1653 |
axioms={Axiom.CONSERVED,Axiom.NETWORK,Axiom.EQUILIBRIUM,Axiom.ORDERED},
|
| 1654 |
+
variables=[{"name":"pt2","lo":-1.0,"hi":0.5},{"name":"pt3","lo":-0.5,"hi":0.5}],
|
|
|
|
|
|
|
|
|
|
| 1655 |
constraints=[
|
| 1656 |
+
{"kind":"EQ","expr":"-2*pt2-3*pt3-0.5","weight":5.0},
|
| 1657 |
+
{"kind":"EQ","expr":"3*pt2-pt3+1.0","weight":5.0},
|
|
|
|
|
|
|
| 1658 |
],
|
| 1659 |
scopes=[{"name":"power","order":0,"vars":["pt2","pt3"],
|
| 1660 |
"constraints":[
|
| 1661 |
+
{"kind":"EQ","expr":"-2*pt2-3*pt3-0.5","weight":5.0},
|
| 1662 |
+
{"kind":"EQ","expr":"3*pt2-pt3+1.0","weight":5.0},
|
| 1663 |
]}],
|
| 1664 |
anchors=[
|
| 1665 |
+
AXLInvariant("bus1","-2*pt2-3*pt3-0.5",1e-3),
|
| 1666 |
+
AXLInvariant("bus2","3*pt2-pt3+1.0",1e-3),
|
| 1667 |
],
|
|
|
|
| 1668 |
),
|
|
|
|
|
|
|
| 1669 |
AXLProblemDef(
|
| 1670 |
name="ChemEquilibrium",
|
| 1671 |
+
description="A+B↔C, Kc=4. ca=cb≈0.390, cc≈0.610.",
|
|
|
|
| 1672 |
axioms={Axiom.CONSERVED,Axiom.BILINEAR,Axiom.CONTINUOUS,Axiom.MONOTONE},
|
| 1673 |
+
variables=[{"name":"ca","lo":0.0,"hi":1.0},{"name":"cb","lo":0.0,"hi":1.0},
|
| 1674 |
+
{"name":"cc","lo":0.0,"hi":1.0}],
|
|
|
|
|
|
|
|
|
|
| 1675 |
constraints=[
|
| 1676 |
+
{"kind":"CONSERVE","expr":"ca+cc-1.0"},
|
| 1677 |
+
{"kind":"CONSERVE","expr":"cb+cc-1.0"},
|
| 1678 |
+
{"kind":"EQ","expr":"4*ca*cb-cc","weight":5.0},
|
| 1679 |
],
|
| 1680 |
+
scopes=[{"name":"equil","order":0,"vars":["ca","cb","cc"],
|
| 1681 |
"constraints":[
|
| 1682 |
+
{"kind":"EQ","expr":"ca-cb","weight":3.0},
|
| 1683 |
+
{"kind":"EQ","expr":"4*ca*cb-cc","weight":5.0},
|
| 1684 |
]}],
|
| 1685 |
anchors=[
|
| 1686 |
AXLInvariant("balance_A","ca+cc-1.0",1e-3),
|
| 1687 |
AXLInvariant("balance_B","cb+cc-1.0",1e-3),
|
| 1688 |
+
AXLInvariant("equilibrium","4*ca*cb-cc",1e-3),
|
| 1689 |
],
|
|
|
|
| 1690 |
),
|
|
|
|
|
|
|
| 1691 |
AXLProblemDef(
|
| 1692 |
name="LorenzFixedPoint",
|
| 1693 |
+
description="Lorenz σ=10,ρ=28,β=8/3. Fixed point: x=y=±8.485, z=27.",
|
|
|
|
| 1694 |
axioms={Axiom.CONTINUOUS,Axiom.QUADRATIC,Axiom.SYMMETRIC,Axiom.CONSERVED},
|
| 1695 |
+
variables=[{"name":"lx","lo":-12.0,"hi":12.0},{"name":"ly","lo":-12.0,"hi":12.0},
|
| 1696 |
+
{"name":"lz","lo":20.0,"hi":35.0}],
|
|
|
|
|
|
|
|
|
|
| 1697 |
constraints=[
|
| 1698 |
+
{"kind":"EQ","expr":"lx-ly","weight":5.0},
|
| 1699 |
+
{"kind":"EQ","expr":"lz-27.0","weight":5.0},
|
| 1700 |
+
{"kind":"EQ","expr":"lx**2-72.0","weight":5.0},
|
| 1701 |
],
|
| 1702 |
scopes=[{"name":"lorenz","order":0,"vars":["lx","ly","lz"],
|
| 1703 |
"constraints":[
|
| 1704 |
+
{"kind":"EQ","expr":"lx-ly","weight":5.0},
|
| 1705 |
+
{"kind":"EQ","expr":"lz-27.0","weight":5.0},
|
| 1706 |
+
{"kind":"EQ","expr":"lx**2-72.0","weight":5.0},
|
| 1707 |
]}],
|
| 1708 |
anchors=[
|
| 1709 |
+
AXLInvariant("x_eq_y","lx-ly",1e-3),
|
| 1710 |
+
AXLInvariant("z_27","lz-27.0",1e-3),
|
| 1711 |
+
AXLInvariant("x2_72","lx**2-72.0",0.1),
|
| 1712 |
],
|
| 1713 |
),
|
|
|
|
|
|
|
| 1714 |
AXLProblemDef(
|
| 1715 |
name="NashBattleSexes",
|
| 1716 |
+
description="Battle of Sexes mixed Nash: p=2/3, q=1/3.",
|
| 1717 |
axioms={Axiom.CONTINUOUS,Axiom.SYMMETRIC,Axiom.CONSERVED,Axiom.ORDERED},
|
| 1718 |
+
variables=[{"name":"np","lo":0.0,"hi":1.0},{"name":"nq","lo":0.0,"hi":1.0}],
|
|
|
|
|
|
|
|
|
|
| 1719 |
constraints=[
|
| 1720 |
+
{"kind":"EQ","expr":"3*nq-1.0","weight":5.0},
|
| 1721 |
+
{"kind":"EQ","expr":"3*np-2.0","weight":5.0},
|
| 1722 |
],
|
| 1723 |
scopes=[{"name":"nash","order":0,"vars":["np","nq"],
|
| 1724 |
"constraints":[
|
| 1725 |
+
{"kind":"EQ","expr":"3*nq-1.0","weight":5.0},
|
| 1726 |
+
{"kind":"EQ","expr":"3*np-2.0","weight":5.0},
|
| 1727 |
]}],
|
| 1728 |
anchors=[
|
| 1729 |
AXLInvariant("p1_indiff","3*nq-1.0",1e-3),
|
| 1730 |
AXLInvariant("p2_indiff","3*np-2.0",1e-3),
|
| 1731 |
],
|
|
|
|
| 1732 |
),
|
|
|
|
|
|
|
| 1733 |
AXLProblemDef(
|
| 1734 |
name="KeplerPeriapsis",
|
| 1735 |
+
description="Orbital mechanics at periapsis. a=1, e=0.5 → rp=0.5, vp=√3, h=√3/2.",
|
|
|
|
| 1736 |
axioms={Axiom.CONTINUOUS,Axiom.QUADRATIC,Axiom.CONSERVED,Axiom.METRIC},
|
| 1737 |
variables=[
|
| 1738 |
+
{"name":"ka","lo":0.5,"hi":2.0},{"name":"ke","lo":0.0,"hi":0.99},
|
| 1739 |
+
{"name":"krp","lo":0.1,"hi":2.0},{"name":"kvp","lo":0.5,"hi":5.0},
|
| 1740 |
+
{"name":"kh","lo":0.1,"hi":3.0},
|
|
|
|
|
|
|
| 1741 |
],
|
| 1742 |
constraints=[
|
| 1743 |
+
{"kind":"EQ","expr":"krp-ka*(1-ke)","weight":5.0},
|
| 1744 |
+
{"kind":"EQ","expr":"kvp**2*krp-(1+ke)","weight":5.0},
|
| 1745 |
+
{"kind":"EQ","expr":"kh-krp*kvp","weight":5.0},
|
| 1746 |
],
|
| 1747 |
scopes=[{"name":"orbit","order":0,"vars":["ka","ke","krp","kvp","kh"],
|
| 1748 |
"constraints":[
|
| 1749 |
+
{"kind":"EQ","expr":"krp-ka*(1-ke)","weight":5.0},
|
| 1750 |
+
{"kind":"EQ","expr":"kvp**2*krp-(1+ke)","weight":5.0},
|
| 1751 |
+
{"kind":"EQ","expr":"kh-krp*kvp","weight":5.0},
|
| 1752 |
]}],
|
| 1753 |
anchors=[
|
| 1754 |
+
AXLInvariant("periapsis","krp-ka*(1-ke)",1e-3),
|
| 1755 |
+
AXLInvariant("vis_viva","kvp**2*krp-(1+ke)",1e-3),
|
| 1756 |
+
AXLInvariant("ang_mom","kh-krp*kvp",1e-3),
|
| 1757 |
],
|
| 1758 |
+
observations={"ka":1.0,"ke":0.5},
|
| 1759 |
),
|
|
|
|
|
|
|
| 1760 |
AXLProblemDef(
|
| 1761 |
name="VibratingString3",
|
| 1762 |
+
description="3-node string, unit load, fixed ends. s1=s3=1.5, s2=2.0.",
|
|
|
|
| 1763 |
axioms={Axiom.ORDERED,Axiom.SYMMETRIC,Axiom.CONSERVED,Axiom.METRIC},
|
| 1764 |
+
variables=[{"name":"s1","lo":0.0,"hi":5.0},{"name":"s2","lo":0.0,"hi":5.0},
|
| 1765 |
+
{"name":"s3","lo":0.0,"hi":5.0}],
|
|
|
|
|
|
|
|
|
|
| 1766 |
constraints=[
|
| 1767 |
+
{"kind":"EQ","expr":"-2*s1+s2+1.0","weight":5.0},
|
| 1768 |
+
{"kind":"EQ","expr":"s1-2*s2+s3+1.0","weight":5.0},
|
| 1769 |
+
{"kind":"EQ","expr":"s2-2*s3+1.0","weight":5.0},
|
| 1770 |
],
|
| 1771 |
scopes=[{"name":"string","order":0,"vars":["s1","s2","s3"],
|
| 1772 |
"constraints":[
|
| 1773 |
+
{"kind":"EQ","expr":"-2*s1+s2+1.0","weight":5.0},
|
| 1774 |
+
{"kind":"EQ","expr":"s1-2*s2+s3+1.0","weight":5.0},
|
| 1775 |
+
{"kind":"EQ","expr":"s2-2*s3+1.0","weight":5.0},
|
| 1776 |
]}],
|
| 1777 |
anchors=[
|
| 1778 |
AXLInvariant("node1","-2*s1+s2+1.0",1e-3),
|
| 1779 |
AXLInvariant("node2","s1-2*s2+s3+1.0",1e-3),
|
| 1780 |
AXLInvariant("node3","s2-2*s3+1.0",1e-3),
|
| 1781 |
+
AXLInvariant("symmetry","s1-s3",1e-3),
|
| 1782 |
],
|
|
|
|
| 1783 |
),
|
|
|
|
|
|
|
| 1784 |
AXLProblemDef(
|
| 1785 |
name="SignalRecovery4",
|
| 1786 |
+
description="Compressed sensing: Ax=b, sparse x=[1,2,0,2].",
|
|
|
|
|
|
|
| 1787 |
axioms={Axiom.CONSERVED,Axiom.PARSIMONY,Axiom.METRIC,Axiom.INJECTIVE},
|
| 1788 |
+
variables=[{"name":"r1","lo":0.0,"hi":5.0},{"name":"r2","lo":0.0,"hi":5.0},
|
| 1789 |
+
{"name":"r3","lo":0.0,"hi":5.0},{"name":"r4","lo":0.0,"hi":5.0}],
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1790 |
constraints=[
|
| 1791 |
+
{"kind":"EQ","expr":"r1+r2-3.0","weight":5.0},
|
| 1792 |
+
{"kind":"EQ","expr":"r1+r3-1.0","weight":5.0},
|
| 1793 |
+
{"kind":"EQ","expr":"r2+r4-4.0","weight":5.0},
|
| 1794 |
],
|
| 1795 |
scopes=[{"name":"signal","order":0,"vars":["r1","r2","r3","r4"],
|
| 1796 |
"constraints":[
|
|
|
|
| 1803 |
AXLInvariant("meas2","r1+r3-1.0",1e-3),
|
| 1804 |
AXLInvariant("meas3","r2+r4-4.0",1e-3),
|
| 1805 |
],
|
|
|
|
| 1806 |
),
|
|
|
|
|
|
|
| 1807 |
AXLProblemDef(
|
| 1808 |
name="RobotArm2D",
|
| 1809 |
+
description="2-link arm L1=L2=1, target=(1.2, 0.8). Find joint angles.",
|
|
|
|
| 1810 |
axioms={Axiom.CONTINUOUS,Axiom.METRIC,Axiom.SYMMETRIC,Axiom.QUADRATIC},
|
| 1811 |
+
variables=[{"name":"t1","lo":-3.15,"hi":3.15},{"name":"t2","lo":-3.15,"hi":3.15}],
|
|
|
|
|
|
|
|
|
|
| 1812 |
constraints=[
|
| 1813 |
+
{"kind":"EQ","expr":"cos(t1)+cos(t1+t2)-1.2","weight":5.0},
|
| 1814 |
+
{"kind":"EQ","expr":"sin(t1)+sin(t1+t2)-0.8","weight":5.0},
|
|
|
|
|
|
|
| 1815 |
],
|
| 1816 |
scopes=[{"name":"kinematics","order":0,"vars":["t1","t2"],
|
| 1817 |
"constraints":[
|
|
|
|
| 1821 |
anchors=[
|
| 1822 |
AXLInvariant("reach_x","cos(t1)+cos(t1+t2)-1.2",1e-2),
|
| 1823 |
AXLInvariant("reach_y","sin(t1)+sin(t1+t2)-0.8",1e-2),
|
| 1824 |
+
AXLInvariant("elbow_check","cos(t2)-0.04",0.05),
|
|
|
|
| 1825 |
],
|
|
|
|
| 1826 |
),
|
|
|
|
|
|
|
| 1827 |
AXLProblemDef(
|
| 1828 |
name="NormManifold4D",
|
| 1829 |
+
description="4 vars on unit sphere, zero sum, x1 observed at 0.5.",
|
|
|
|
| 1830 |
axioms={Axiom.CONTINUOUS,Axiom.QUADRATIC,Axiom.CONSERVED,Axiom.METRIC,Axiom.SYMMETRIC},
|
| 1831 |
+
variables=[{"name":"x1","lo":-1.0,"hi":1.0},{"name":"x2","lo":-1.0,"hi":1.0},
|
| 1832 |
+
{"name":"x3","lo":-1.0,"hi":1.0},{"name":"x4","lo":-1.0,"hi":1.0}],
|
|
|
|
|
|
|
| 1833 |
constraints=[
|
| 1834 |
+
{"kind":"CONSERVE","expr":"x1**2+x2**2+x3**2+x4**2-1.0"},
|
| 1835 |
+
{"kind":"EQ","expr":"x1+x2+x3+x4","weight":2.0},
|
| 1836 |
],
|
| 1837 |
scopes=[{"name":"sphere","order":0,"vars":["x1","x2","x3","x4"],
|
| 1838 |
"constraints":[{"kind":"EQ","expr":"x1**2+x2**2+x3**2+x4**2-1.0","weight":5.0}]}],
|
|
|
|
| 1845 |
),
|
| 1846 |
AXLProblemDef(
|
| 1847 |
name="BilinearChain6",
|
| 1848 |
+
description="6-var ordered chain. Products 0.5, 2.0, 4.5. Sum=9.",
|
|
|
|
| 1849 |
axioms={Axiom.DISCRETE,Axiom.ORDERED,Axiom.BILINEAR,Axiom.CONSERVED,Axiom.NETWORK},
|
| 1850 |
variables=[{"name":f"t{i}","lo":0.0,"hi":3.0} for i in range(1,7)],
|
| 1851 |
constraints=[
|
|
|
|
| 1870 |
),
|
| 1871 |
AXLProblemDef(
|
| 1872 |
name="PhaseCollider",
|
| 1873 |
+
description="2-particle collision: conservation + phase branch.",
|
|
|
|
| 1874 |
axioms={Axiom.DISCRETE,Axiom.MUTABLE,Axiom.SYMMETRIC,Axiom.NETWORK,Axiom.CONSERVED},
|
| 1875 |
+
variables=[{"name":"p1x","lo":-2.0,"hi":2.0},{"name":"p2x","lo":-2.0,"hi":2.0},
|
| 1876 |
+
{"name":"p1y","lo":-2.0,"hi":2.0},{"name":"p2y","lo":-2.0,"hi":2.0}],
|
|
|
|
|
|
|
| 1877 |
constraints=[
|
| 1878 |
{"kind":"CONSERVE","expr":"p1x+p2x"},{"kind":"CONSERVE","expr":"p1y+p2y"},
|
| 1879 |
],
|
| 1880 |
scopes=[{"name":"phase","order":0,"vars":["p1x","p2x","p1y","p2y"],
|
| 1881 |
"constraints":[
|
| 1882 |
{"kind":"BRANCH","name":"phase_select","options":[
|
| 1883 |
+
"p1x**2+p1y**2-0.25","p1x**2+p1y**2-1.0"]},
|
|
|
|
| 1884 |
{"kind":"EQ","expr":"p1x+p2x","weight":3.0},
|
| 1885 |
{"kind":"EQ","expr":"p1y+p2y","weight":3.0},
|
| 1886 |
]}],
|
|
|
|
| 1892 |
),
|
| 1893 |
AXLProblemDef(
|
| 1894 |
name="MetricPacking3D",
|
| 1895 |
+
description="3 vars: centred, norm²=6, min separation. a=-√3, b=0, c=√3.",
|
|
|
|
| 1896 |
axioms={Axiom.CONTINUOUS,Axiom.METRIC,Axiom.INJECTIVE,Axiom.CONSERVED,Axiom.SYMMETRIC},
|
| 1897 |
+
variables=[{"name":"a","lo":-3.0,"hi":3.0},{"name":"b","lo":-3.0,"hi":3.0},
|
| 1898 |
+
{"name":"c","lo":-3.0,"hi":3.0}],
|
|
|
|
|
|
|
|
|
|
| 1899 |
constraints=[
|
| 1900 |
{"kind":"CONSERVE","expr":"a+b+c"},
|
| 1901 |
{"kind":"GEQ","expr":"(a-b)**2-1.0","weight":2.0},
|
|
|
|
| 1907 |
anchors=[
|
| 1908 |
AXLInvariant("centred","a+b+c",1e-3),
|
| 1909 |
AXLInvariant("norm_6","a**2+b**2+c**2-6.0",0.05),
|
| 1910 |
+
AXLInvariant("sep_ab","(a-b)**2-1.0",0.0,"geq"),
|
| 1911 |
+
AXLInvariant("sep_bc","(b-c)**2-1.0",0.0,"geq"),
|
| 1912 |
],
|
| 1913 |
),
|
| 1914 |
+
]
|
|
|
|
| 1915 |
|
| 1916 |
def build_base_problem(axl_def:AXLProblemDef) -> Problem:
|
| 1917 |
psl_text=AXL_COMPILER.compile(axl_def)
|
|
|
|
| 1922 |
scope_order=ep.scope_order,annotations=ep.annotations)
|
| 1923 |
|
| 1924 |
# ══════════════════════════════════════════════════════════════════════
|
| 1925 |
+
# SECTION 16: GLOBAL STATE + ROUND-ROBIN RUNNER
|
| 1926 |
# ══════════════════════════════════════════════════════════════════════
|
| 1927 |
STATE_LOCK = threading.Lock()
|
| 1928 |
RUN_LOG: List[Dict] = []
|
| 1929 |
PROBLEM_STATS: Dict[str,Dict] = {p.name: {
|
| 1930 |
"runs":0,"solved":0,"total_ce":0.0,"total_rays":0,
|
| 1931 |
+
"best_ce":float('inf'),"best_ray":"—","best_ray_type":"—",
|
| 1932 |
+
"type_stats": {t:{"tried":0,"survived":0} for t in
|
| 1933 |
+
[RAY_SEED,RAY_BRANCH,RAY_TENSION,RAY_SCOUT,RAY_RECOMBINE,RAY_INVERT]},
|
| 1934 |
} for p in AXL_PROBLEMS}
|
| 1935 |
+
POOL = ThreadPoolExecutor(max_workers=1)
|
| 1936 |
+
_PROB_IDX = 0
|
| 1937 |
|
| 1938 |
def _run_problem(axl_def:AXLProblemDef):
|
| 1939 |
try:
|
|
|
|
| 1944 |
survived=[t for t in traces if t.survived]
|
| 1945 |
failed =[t for t in traces if not t.survived]
|
| 1946 |
best_t =min(survived,key=lambda t:t.ce_after,default=None)
|
| 1947 |
+
|
| 1948 |
+
# Per-type breakdown
|
| 1949 |
+
type_counts:Dict[str,Dict]={t:{"tried":0,"survived":0}
|
| 1950 |
+
for t in [RAY_SEED,RAY_BRANCH,RAY_TENSION,
|
| 1951 |
+
RAY_SCOUT,RAY_RECOMBINE,RAY_INVERT]}
|
| 1952 |
+
for t in traces:
|
| 1953 |
+
rt=t.ray_type
|
| 1954 |
+
if rt in type_counts:
|
| 1955 |
+
type_counts[rt]["tried"]+=1
|
| 1956 |
+
if t.survived: type_counts[rt]["survived"]+=1
|
| 1957 |
+
|
| 1958 |
record={
|
| 1959 |
"problem":axl_def.name,
|
| 1960 |
"description":axl_def.description[:60],
|
|
|
|
| 1966 |
"binding":{k:round(v,5) for k,v in binding.items()},
|
| 1967 |
"observations":axl_def.observations,
|
| 1968 |
"traces":[{
|
| 1969 |
+
"round":t.round_idx,"ray":t.ray_name,"ray_type":t.ray_type,
|
| 1970 |
+
"depth":t.depth,"parent":t.parent_id,
|
| 1971 |
"ce_before":round(t.ce_before,5),"ce":round(t.ce_after,5),
|
| 1972 |
"g1_ce":round(t.verify.gate1_ce,5) if t.verify else None,
|
| 1973 |
"g1":t.verify.gate1_pass if t.verify else False,
|
|
|
|
| 1975 |
"g2_detail":{k:(round(v,6),ok) for k,(v,ok) in t.verify.gate2_results.items()} if t.verify else {},
|
| 1976 |
"survived":t.survived,"ms":t.elapsed_ms,
|
| 1977 |
} for t in traces],
|
| 1978 |
+
"type_counts":type_counts,
|
| 1979 |
"survived_count":len(survived),
|
| 1980 |
"failed_count":len(failed),
|
| 1981 |
"best_ray":best_t.ray_name if best_t else "—",
|
| 1982 |
+
"best_ray_type":best_t.ray_type if best_t else "—",
|
| 1983 |
"total_fired":len(traces),
|
| 1984 |
}
|
| 1985 |
with STATE_LOCK:
|
|
|
|
| 1987 |
if len(RUN_LOG)>60: RUN_LOG.pop(0)
|
| 1988 |
ps=PROBLEM_STATS[axl_def.name]
|
| 1989 |
ps["runs"]+=1; ps["total_rays"]+=len(traces); ps["total_ce"]+=ce
|
| 1990 |
+
if len(survived)>0 and ce<SOLVE_THRESHOLD: ps["solved"]+=1
|
|
|
|
| 1991 |
if ce<ps["best_ce"]:
|
| 1992 |
ps["best_ce"]=ce
|
| 1993 |
ps["best_ray"]=best_t.ray_name if best_t else "—"
|
| 1994 |
+
ps["best_ray_type"]=best_t.ray_type if best_t else "—"
|
| 1995 |
+
for rt,counts in type_counts.items():
|
| 1996 |
+
ps["type_stats"][rt]["tried"]+=counts["tried"]
|
| 1997 |
+
ps["type_stats"][rt]["survived"]+=counts["survived"]
|
| 1998 |
except Exception as e:
|
| 1999 |
import traceback; traceback.print_exc()
|
| 2000 |
print(f"[RUN ERROR] {axl_def.name}: {e}")
|
| 2001 |
|
| 2002 |
async def run_loop():
|
| 2003 |
+
global _PROB_IDX
|
| 2004 |
loop=asyncio.get_event_loop()
|
| 2005 |
while True:
|
| 2006 |
+
prob=AXL_PROBLEMS[_PROB_IDX % len(AXL_PROBLEMS)]; _PROB_IDX+=1
|
|
|
|
| 2007 |
await loop.run_in_executor(POOL,_run_problem,prob)
|
| 2008 |
await asyncio.sleep(0.2)
|
| 2009 |
|
|
|
|
| 2014 |
POOL.shutdown(wait=False)
|
| 2015 |
|
| 2016 |
# ══════════════════════════════════════════════════════════════════════
|
| 2017 |
+
# SECTION 17: FASTAPI + DASHBOARD
|
| 2018 |
# ══════════════════════════════════════════════════════════════════════
|
| 2019 |
+
app=FastAPI(title="Practicality 15.0",lifespan=lifespan)
|
| 2020 |
+
|
| 2021 |
+
def _type_badge(rt:str, count:int, survived:int) -> str:
|
| 2022 |
+
icon=RAY_ICONS.get(rt,"·")
|
| 2023 |
+
rate=f"{round(survived/count*100)}%" if count else "—"
|
| 2024 |
+
c="#4CAF50" if survived>0 else "#333"
|
| 2025 |
+
return (f"<span style='font-size:0.75em;margin-right:8px'>"
|
| 2026 |
+
f"{icon}<span style='color:#555'>{rt[:3]}</span> "
|
| 2027 |
+
f"<span style='color:{c}'>{rate}</span></span>")
|
| 2028 |
|
| 2029 |
def _perf_table() -> str:
|
| 2030 |
rows=""
|
| 2031 |
for prob in AXL_PROBLEMS:
|
| 2032 |
ps=PROBLEM_STATS[prob.name]
|
| 2033 |
if ps["runs"]==0:
|
| 2034 |
+
rows+=f"<tr><td>{PROBLEM_META.get(prob.name,{}).get('icon','·')}</td><td style='color:#444'>{prob.name}</td><td colspan='8' style='color:#222'>—</td></tr>"
|
| 2035 |
continue
|
| 2036 |
runs=ps["runs"]; rate=round(ps["solved"]/runs*100)
|
| 2037 |
avg_ce=round(ps["total_ce"]/runs,5)
|
| 2038 |
+
rc=ps["type_stats"]
|
| 2039 |
+
type_cells="".join(
|
| 2040 |
+
f"<td style='color:{'#4CAF50' if rc[t]['survived']>0 else '#333'};font-size:0.75em'>"
|
| 2041 |
+
f"{RAY_ICONS.get(t,'·')}{round(rc[t]['survived']/rc[t]['tried']*100) if rc[t]['tried'] else 0}%</td>"
|
| 2042 |
+
for t in [RAY_SEED,RAY_TENSION,RAY_SCOUT,RAY_RECOMBINE,RAY_INVERT,RAY_BRANCH])
|
| 2043 |
dom=PROBLEM_META.get(prob.name,{})
|
| 2044 |
+
best_t_icon=RAY_ICONS.get(ps["best_ray_type"],"·")
|
| 2045 |
+
rate_col="#4CAF50" if rate>=50 else ("#FF9800" if rate>=20 else "#EF5350")
|
|
|
|
| 2046 |
rows+=(f"<tr>"
|
| 2047 |
f"<td style='color:#aaa'>{dom.get('icon','·')}</td>"
|
|
|
|
| 2048 |
f"<td style='color:#FF9800'>{prob.name}</td>"
|
| 2049 |
+
f"<td style='color:#5C6BC0;font-size:0.8em'>{dom.get('domain','')}</td>"
|
| 2050 |
f"<td style='color:#555;font-size:0.75em'>{dom.get('difficulty','')}</td>"
|
|
|
|
| 2051 |
f"<td style='color:#aaa'>{runs}</td>"
|
| 2052 |
f"<td style='color:{rate_col};font-weight:700'>{rate}%</td>"
|
| 2053 |
f"<td style='color:#26C6DA'>{avg_ce}</td>"
|
| 2054 |
+
f"<td style='color:#26C6DA;font-size:0.8em'>{ps['best_ce']:.5f}</td>"
|
| 2055 |
+
f"{type_cells}"
|
| 2056 |
+
f"<td style='color:#4CAF50;font-size:0.75em'>{best_t_icon} {ps['best_ray'][:22]}</td>"
|
| 2057 |
f"</tr>")
|
| 2058 |
return rows
|
| 2059 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 2060 |
def _render_collapse(record:Dict) -> str:
|
| 2061 |
b=record["binding"]; traces=record["traces"]
|
| 2062 |
survived=[t for t in traces if t["survived"]]
|
|
|
|
| 2066 |
ce=record["ce"]; solved=record["solved"]
|
| 2067 |
ce_color="#4CAF50" if solved else ("#FF9800" if ce<0.5 else "#EF5350")
|
| 2068 |
status="✓ SOLVED" if solved else ("~ PARTIAL" if ce<0.5 else "✗ UNSOLVED")
|
| 2069 |
+
|
| 2070 |
binding_rows="".join(
|
| 2071 |
f"<tr><td style='color:#888'>{v}</td>"
|
| 2072 |
f"<td style='color:#26C6DA;font-weight:700'>{val:+.5f}</td>"
|
| 2073 |
f"<td style='color:#4CAF50;font-size:0.7em'>{'[OBS]' if v in obs_vars else ''}</td></tr>"
|
| 2074 |
for v,val in b.items())
|
| 2075 |
+
|
| 2076 |
inv_rows=""
|
| 2077 |
if best and best.get("g2_detail"):
|
| 2078 |
for inv,(val,ok) in best["g2_detail"].items():
|
|
|
|
| 2080 |
inv_rows+=(f"<tr><td style='color:{c}'>{'✓' if ok else '✗'}</td>"
|
| 2081 |
f"<td style='color:#888;font-size:0.8em'>{inv}</td>"
|
| 2082 |
f"<td style='color:{c};font-size:0.8em'>{val:.5f}</td></tr>")
|
| 2083 |
+
|
| 2084 |
+
# Type breakdown badges
|
| 2085 |
+
tc=record.get("type_counts",{})
|
| 2086 |
+
type_summary="".join(_type_badge(rt,tc.get(rt,{}).get("tried",0),tc.get(rt,{}).get("survived",0))
|
| 2087 |
+
for rt in [RAY_SEED,RAY_TENSION,RAY_SCOUT,RAY_RECOMBINE,RAY_INVERT,RAY_BRANCH])
|
| 2088 |
+
|
| 2089 |
def span(t):
|
| 2090 |
+
icon=RAY_ICONS.get(t.get("ray_type",RAY_SEED),"·")
|
| 2091 |
depth_indent="·"*min(t.get("depth",0),5)
|
| 2092 |
c="#4CAF50" if t["survived"] else ("#555" if t.get("depth",0)>0 else "#333")
|
| 2093 |
star=" ◀" if t["survived"] else ""
|
| 2094 |
delta=t["ce"]-t.get("ce_before",t["ce"])
|
| 2095 |
+
return (f"<div style='color:{c};font-size:0.71em;margin-bottom:1px'>"
|
| 2096 |
+
f"{icon}{depth_indent}[{t['round']}|d{t.get('depth',0)}] "
|
| 2097 |
f"<span style='color:#FF9800'>{t['ray']}</span> "
|
| 2098 |
f"CE={t['ce']:.4f} <span style='color:#444'>{delta:+.4f}</span>"
|
| 2099 |
f"<span style='color:#4CAF50;font-weight:700'>{star}</span></div>")
|
| 2100 |
+
|
| 2101 |
+
trail="".join(span(t) for t in traces[:28])
|
| 2102 |
return f"""
|
| 2103 |
+
<div style='border:1px solid #181818;border-radius:6px;margin-bottom:12px;overflow:hidden'>
|
| 2104 |
+
<div style='background:#0d0d0d;padding:7px 12px;border-bottom:1px solid #1a1a1a;display:flex;align-items:center;gap:14px;flex-wrap:wrap'>
|
| 2105 |
<span style='color:{ce_color};font-weight:700'>{status}</span>
|
| 2106 |
<span style='color:#555;font-size:0.8em'>{record.get("icon","·")} {record["problem"]}</span>
|
| 2107 |
<span style='color:#5C6BC0;font-size:0.75em'>{record.get("domain","")}</span>
|
| 2108 |
<span style='color:#333;font-size:0.75em'>CE={ce:.6f}</span>
|
| 2109 |
<span style='color:#26C6DA;font-size:0.72em'>{record["survived_count"]} survived / {record["total_fired"]} fired</span>
|
| 2110 |
+
<span style='margin-left:auto'>{type_summary}</span>
|
| 2111 |
</div>
|
| 2112 |
<div style='display:flex'>
|
| 2113 |
+
<div style='flex:0 0 155px;padding:8px 10px;border-right:1px solid #181818'>
|
| 2114 |
<div style='color:#333;font-size:0.65em;margin-bottom:4px'>BINDING</div>
|
| 2115 |
<table style='border-collapse:collapse;width:100%'>{binding_rows}</table>
|
| 2116 |
</div>
|
| 2117 |
+
<div style='flex:0 0 205px;padding:8px 10px;border-right:1px solid #181818'>
|
| 2118 |
<div style='color:#333;font-size:0.65em;margin-bottom:4px'>GATE 2 INVARIANTS</div>
|
| 2119 |
<table style='border-collapse:collapse;width:100%'>
|
| 2120 |
{inv_rows or "<tr><td colspan='3' style='color:#222'>—</td></tr>"}
|
|
|
|
| 2122 |
</div>
|
| 2123 |
<div style='flex:1;padding:8px 10px;overflow-y:auto;max-height:200px'>
|
| 2124 |
<div style='color:#333;font-size:0.65em;margin-bottom:4px'>
|
| 2125 |
+
RAY TREE — best: <span style='color:#FF9800'>{RAY_ICONS.get(record["best_ray_type"],"·")} {record["best_ray"]}</span>
|
| 2126 |
</div>
|
| 2127 |
{trail}
|
| 2128 |
</div>
|
|
|
|
| 2133 |
async def dashboard():
|
| 2134 |
with STATE_LOCK:
|
| 2135 |
log=list(reversed(RUN_LOG[-8:]))
|
| 2136 |
+
stats_snap=dict(PROBLEM_STATS)
|
| 2137 |
+
total_runs=sum(s["runs"] for s in stats_snap.values())
|
| 2138 |
+
total_solved=sum(s["solved"] for s in stats_snap.values())
|
| 2139 |
+
avg_ce=(sum(s["total_ce"] for s in stats_snap.values())/max(1,total_runs))
|
| 2140 |
+
domains_active=len([p for p in AXL_PROBLEMS if stats_snap[p.name]["runs"]>0])
|
| 2141 |
+
|
| 2142 |
+
# Global creative type efficacy
|
| 2143 |
+
global_type_stats:Dict[str,Dict]={t:{"tried":0,"survived":0}
|
| 2144 |
+
for t in [RAY_SEED,RAY_BRANCH,RAY_TENSION,
|
| 2145 |
+
RAY_SCOUT,RAY_RECOMBINE,RAY_INVERT]}
|
| 2146 |
+
for ps in stats_snap.values():
|
| 2147 |
+
for rt,counts in ps["type_stats"].items():
|
| 2148 |
+
global_type_stats[rt]["tried"]+=counts["tried"]
|
| 2149 |
+
global_type_stats[rt]["survived"]+=counts["survived"]
|
| 2150 |
+
|
| 2151 |
+
type_rows="".join(
|
| 2152 |
+
f"<tr>"
|
| 2153 |
+
f"<td>{RAY_ICONS.get(rt,'·')}</td>"
|
| 2154 |
+
f"<td style='color:#FF9800'>{rt}</td>"
|
| 2155 |
+
f"<td style='color:#aaa'>{s['tried']}</td>"
|
| 2156 |
+
f"<td style='color:#4CAF50'>{s['survived']}</td>"
|
| 2157 |
+
f"<td style='color:#EF5350'>{s['tried']-s['survived']}</td>"
|
| 2158 |
+
f"<td style='color:{'#4CAF50' if s['survived']>0 else '#333'};font-weight:700'>"
|
| 2159 |
+
f"{round(s['survived']/s['tried']*100) if s['tried'] else 0}%</td>"
|
| 2160 |
+
f"<td style='color:#555;font-size:0.8em'>"
|
| 2161 |
+
f"{'Greedy depth-first from single axiom' if rt==RAY_SEED else 'Earned child of tree ray' if rt==RAY_BRANCH else 'Mediated contradiction [A→B→C]' if rt==RAY_TENSION else 'Random length 3-8 cartographer' if rt==RAY_SCOUT else 'Genetic crossover of two sequences' if rt==RAY_RECOMBINE else 'Reversed successful sequence'}"
|
| 2162 |
+
f"</td></tr>"
|
| 2163 |
+
for rt,s in global_type_stats.items())
|
| 2164 |
|
| 2165 |
perf_rows=_perf_table()
|
|
|
|
| 2166 |
collapses="".join(_render_collapse(r) for r in log) if log else \
|
| 2167 |
"<div style='color:#222;padding:16px'>Cycling through 14 problems…</div>"
|
| 2168 |
|
| 2169 |
+
return f"""<!DOCTYPE html><html><head><title>Practicality 15.0</title>
|
| 2170 |
<meta http-equiv="refresh" content="5">
|
| 2171 |
<style>
|
| 2172 |
+
body{{background:#090909;color:#e0e0e0;font-family:monospace;padding:18px;max-width:1700px}}
|
| 2173 |
h1{{color:#26C6DA;border-bottom:1px solid #1a1a1a;padding-bottom:5px;font-size:1.1em;margin-bottom:4px}}
|
| 2174 |
h3{{color:#252525;margin-top:18px;font-size:0.82em;letter-spacing:2px;text-transform:uppercase}}
|
| 2175 |
table{{width:100%;border-collapse:collapse;margin-bottom:8px}}
|
|
|
|
| 2177 |
th{{color:#252525;font-size:0.70em}}
|
| 2178 |
.badge{{display:inline-block;padding:2px 9px;border-radius:3px;background:#0e0e0e;margin:2px;font-size:0.75em;border:1px solid #1a1a1a}}
|
| 2179 |
</style></head><body>
|
| 2180 |
+
<h1>⚗ Practicality 15.0 — Creative Sequence Wisdom</h1>
|
| 2181 |
<div style='color:#2a2a2a;font-size:0.72em;margin-bottom:10px'>
|
| 2182 |
+
🌱 Seeds + ⚡ Tension (mediated contradictions) + 🔭 Scouts (random) →
|
| 2183 |
+
🧬 Recombine + 🔄 Invert → 🌿 Branch (resonance-guided) → Verify
|
| 2184 |
</div>
|
| 2185 |
<div style='margin-bottom:14px'>
|
| 2186 |
<span class='badge' style='color:#aaa'>Total Runs: {total_runs}</span>
|
|
|
|
| 2190 |
<span class='badge' style='color:#5C6BC0'>Axioms: {len(ALL_AXIOMS)}</span>
|
| 2191 |
</div>
|
| 2192 |
|
| 2193 |
+
<h3>Creative Ray Type Efficacy</h3>
|
| 2194 |
<table>
|
| 2195 |
+
<tr><th></th><th>Type</th><th>Tried</th><th>Survived</th><th>Failed</th><th>Rate</th><th>Mechanism</th></tr>
|
| 2196 |
+
{type_rows}
|
|
|
|
|
|
|
|
|
|
|
|
|
| 2197 |
</table>
|
| 2198 |
|
| 2199 |
+
<h3>Multi-Domain Performance</h3>
|
| 2200 |
<table>
|
| 2201 |
+
<tr>
|
| 2202 |
+
<th></th><th>Problem</th><th>Domain</th><th>Diff</th><th>Runs</th><th>Rate%</th>
|
| 2203 |
+
<th>Avg CE</th><th>Best CE</th>
|
| 2204 |
+
<th>🌱</th><th>⚡</th><th>🔭</th><th>🧬</th><th>🔄</th><th>🌿</th>
|
| 2205 |
+
<th>Best Sequence</th>
|
| 2206 |
+
</tr>
|
| 2207 |
+
{perf_rows}
|
| 2208 |
</table>
|
| 2209 |
|
| 2210 |
<h3>Recent Runs</h3>
|