Spaces:
Sleeping
Sleeping
Update app.py
Browse files
app.py
CHANGED
|
@@ -1,13 +1,28 @@
|
|
| 1 |
#!/usr/bin/env python3
|
| 2 |
"""
|
| 3 |
-
PRACTICALITY SYSTEM
|
| 4 |
βββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 5 |
-
NEW IN
|
| 6 |
-
Β·
|
| 7 |
-
|
| 8 |
-
|
| 9 |
-
|
| 10 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 11 |
"""
|
| 12 |
|
| 13 |
import time, random, math, threading, asyncio, warnings, itertools
|
|
@@ -29,7 +44,7 @@ import uvicorn
|
|
| 29 |
warnings.filterwarnings("ignore")
|
| 30 |
USE_GPU = torch.cuda.is_available()
|
| 31 |
DEVICE = torch.device("cuda" if USE_GPU else "cpu")
|
| 32 |
-
print(f"[SYSTEM
|
| 33 |
|
| 34 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 35 |
# SECTION 1: CONSTANTS
|
|
@@ -37,13 +52,11 @@ print(f"[SYSTEM 12.1] Compute: {'GPU' if USE_GPU else 'CPU'}")
|
|
| 37 |
SOLVE_THRESHOLD = 0.05
|
| 38 |
VERIFY_G1_THRESHOLD = 0.08
|
| 39 |
VERIFY_G2_TOLERANCE = 1e-3
|
| 40 |
-
TOTAL_BUDGET = 400
|
| 41 |
HC4_VOLUME_FLOOR = 0.20
|
| 42 |
L9_CONTRIB_THRESHOLD = 1e-8
|
| 43 |
HUB_RESIDUAL_MULT = 2.0
|
| 44 |
HUB_DEGREE_RATIO = 0.6
|
| 45 |
-
|
| 46 |
-
MAX_HYPS_PER_ROUND = 8
|
| 47 |
BRANCH_DEPTH = 3
|
| 48 |
MANIFOLD_STEPS = [0.05, 0.2, -0.05, -0.2, 0.5, -0.5]
|
| 49 |
N_MPRT_EXPLORE = 20000 if USE_GPU else 3000
|
|
@@ -121,7 +134,7 @@ def compile_iv(expr,variables):
|
|
| 121 |
return _c(expr)
|
| 122 |
|
| 123 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 124 |
-
# SECTION 3: PSL 2.0 PARSER
|
| 125 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 126 |
@dataclass
|
| 127 |
class PSLVar: name:str; lo:float; hi:float; weight:float=1.0
|
|
@@ -167,10 +180,9 @@ def parse_psl(text:str) -> PSLProgram:
|
|
| 167 |
advance()
|
| 168 |
scons.append(PSLConstraint("or_eq","",scope=sname,weight=1.0,branches=opts))
|
| 169 |
elif kw=="ANNOTATE":
|
| 170 |
-
parts=rest.split()
|
| 171 |
if len(parts)>=3: prog.annotations[parts[0]]=parts[2]
|
| 172 |
return PSLScope(sname,order,depends or [],svars,links,scons)
|
| 173 |
-
|
| 174 |
while i<len(lines):
|
| 175 |
l=advance(); tk=l.split(None,1)
|
| 176 |
kw=tk[0].upper() if tk else ""; rest=tk[1].strip() if len(tk)>1 else ""
|
|
@@ -190,7 +202,7 @@ def parse_psl(text:str) -> PSLProgram:
|
|
| 190 |
advance()
|
| 191 |
prog.constraints.append(PSLConstraint("or_eq","",weight=1.0,branches=opts))
|
| 192 |
elif kw=="ANNOTATE":
|
| 193 |
-
parts=rest.split()
|
| 194 |
if len(parts)>=3: prog.annotations[parts[0]]=parts[2]
|
| 195 |
elif kw=="SCOPE":
|
| 196 |
parts=rest.split(); sname=parts[0] if parts else f"s{len(prog.scopes)}"
|
|
@@ -218,11 +230,9 @@ class ExpandedProblem:
|
|
| 218 |
def expand_psl(prog:PSLProgram) -> ExpandedProblem:
|
| 219 |
variables=[]; bounds={}; constraints=[]
|
| 220 |
scope_groups=defaultdict(list); scope_vars=defaultdict(list)
|
| 221 |
-
|
| 222 |
def add_var(name,lo,hi,scope="root"):
|
| 223 |
if name not in bounds: variables.append(name); bounds[name]=(lo,hi)
|
| 224 |
if scope!="root" and name not in scope_vars[scope]: scope_vars[scope].append(name)
|
| 225 |
-
|
| 226 |
def add_con(kind,expr,direction,scope="root",weight=1.0,branches=None):
|
| 227 |
idx=len(constraints)
|
| 228 |
constraints.append(Constraint(kind,expr,direction,weight,scope,branches or []))
|
|
@@ -241,7 +251,6 @@ def expand_psl(prog:PSLProgram) -> ExpandedProblem:
|
|
| 241 |
if sp.Symbol(v) in parsed.free_symbols and scope!="root" and v not in scope_vars[scope]:
|
| 242 |
scope_vars[scope].append(v)
|
| 243 |
except: pass
|
| 244 |
-
|
| 245 |
for v in prog.vars: add_var(v.name,v.lo,v.hi)
|
| 246 |
for c in prog.constraints:
|
| 247 |
kind="or_eq" if c.kind=="or_eq" else "equality" if c.kind=="eq" else "inequality"
|
|
@@ -256,7 +265,7 @@ def expand_psl(prog:PSLProgram) -> ExpandedProblem:
|
|
| 256 |
return ExpandedProblem(variables,bounds,constraints,dict(scope_groups),dict(scope_vars),prog.scope_order,prog.annotations)
|
| 257 |
|
| 258 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 259 |
-
# SECTION 4: AXL LAYER
|
| 260 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 261 |
@dataclass
|
| 262 |
class AXLInvariant:
|
|
@@ -311,7 +320,7 @@ class AXLtoPSLCompiler:
|
|
| 311 |
AXL_COMPILER=AXLtoPSLCompiler()
|
| 312 |
|
| 313 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 314 |
-
# SECTION 5: PROBLEM & CONSTRAINT COMPILATION
|
| 315 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 316 |
@dataclass
|
| 317 |
class Constraint:
|
|
@@ -484,7 +493,7 @@ class Problem:
|
|
| 484 |
return total
|
| 485 |
|
| 486 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 487 |
-
# SECTION 6: VERIFY LAYER
|
| 488 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 489 |
@dataclass
|
| 490 |
class VerifyResult:
|
|
@@ -494,7 +503,7 @@ class VerifyResult:
|
|
| 494 |
failed_gates:List[str]=field(default_factory=list)
|
| 495 |
|
| 496 |
class VerifyLayer:
|
| 497 |
-
def run(self,binding
|
| 498 |
g1_ce=base_problem.constraint_energy(binding)
|
| 499 |
g1_pass=g1_ce<VERIFY_G1_THRESHOLD
|
| 500 |
g2={}
|
|
@@ -509,85 +518,92 @@ class VerifyLayer:
|
|
| 509 |
except: g2[inv.name]=(999.0,False)
|
| 510 |
g2_pass=all(v[1] for v in g2.values()) if g2 else True
|
| 511 |
failed=(["Gate1"] if not g1_pass else [])+[k for k,v in g2.items() if not v[1]]
|
| 512 |
-
return VerifyResult(
|
| 513 |
-
gate2_results=g2,gate2_pass=g2_pass,
|
| 514 |
-
overall_pass=g1_pass and g2_pass,failed_gates=failed)
|
| 515 |
|
| 516 |
VERIFY_LAYER=VerifyLayer()
|
| 517 |
|
| 518 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 519 |
-
# SECTION 7:
|
|
|
|
|
|
|
| 520 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 521 |
class Axiom:
|
| 522 |
-
|
| 523 |
-
|
| 524 |
-
|
| 525 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 526 |
|
| 527 |
ALL_AXIOMS = [
|
| 528 |
-
Axiom.
|
| 529 |
-
Axiom.
|
| 530 |
-
Axiom.
|
| 531 |
-
Axiom.
|
|
|
|
|
|
|
|
|
|
| 532 |
]
|
| 533 |
|
| 534 |
-
# Explicit short-codes to prevent UI collision (e.g. CNT vs CSV)
|
| 535 |
AXIOM_ABBR = {
|
| 536 |
-
Axiom.
|
| 537 |
-
Axiom.
|
| 538 |
-
Axiom.
|
| 539 |
-
Axiom.
|
| 540 |
-
Axiom.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 541 |
}
|
| 542 |
|
| 543 |
-
|
| 544 |
-
|
| 545 |
-
|
| 546 |
-
|
| 547 |
-
|
| 548 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 549 |
]
|
|
|
|
| 550 |
|
| 551 |
-
def
|
| 552 |
-
|
| 553 |
-
for
|
| 554 |
-
|
| 555 |
-
|
| 556 |
-
|
| 557 |
-
valid.append(cset)
|
| 558 |
-
return valid
|
| 559 |
-
|
| 560 |
-
AXIOM_HYPERCUBE = build_hypercube()
|
| 561 |
-
print(f"[SYSTEM 12.1] Axiomatic Hypercube Booted: {len(AXIOM_HYPERCUBE)} valid rays.")
|
| 562 |
-
|
| 563 |
-
@dataclass
|
| 564 |
-
class DomainStrategy:
|
| 565 |
-
name: str
|
| 566 |
-
hyp_weights: Dict[str,float]
|
| 567 |
-
polish: str
|
| 568 |
-
explore_early: bool
|
| 569 |
-
|
| 570 |
-
def compile_strategy(axioms: Set[str]) -> DomainStrategy:
|
| 571 |
-
name = "|".join(AXIOM_ABBR[a] for a in sorted(axioms)) if axioms else "BASE"
|
| 572 |
-
weights = {"branch": 0.0, "chain": 0.0, "coherence": 0.0, "residual_chain": 0.0, "manifold": 0.0}
|
| 573 |
-
polish = "both"
|
| 574 |
-
explore_early = False
|
| 575 |
-
|
| 576 |
-
if Axiom.CONTINUOUS in axioms:
|
| 577 |
-
weights["manifold"] = 1.5; weights["branch"] = 1.0; weights["residual_chain"] = 1.0; polish = "adam"
|
| 578 |
-
if Axiom.DISCRETE in axioms:
|
| 579 |
-
weights["chain"] = 2.0; weights["branch"] = 1.5; weights["coherence"] = 1.0; polish = "gradient"; explore_early = True
|
| 580 |
-
if Axiom.QUADRATIC in axioms or Axiom.METRIC in axioms:
|
| 581 |
-
weights["manifold"] += 1.0; weights["branch"] += 0.5
|
| 582 |
-
if Axiom.ORDERED in axioms or Axiom.NETWORK in axioms:
|
| 583 |
-
weights["chain"] += 1.0
|
| 584 |
-
if Axiom.MUTABLE in axioms or Axiom.BILINEAR in axioms:
|
| 585 |
-
weights["branch"] += 1.0; weights["residual_chain"] += 1.0
|
| 586 |
-
|
| 587 |
-
if sum(weights.values()) < 0.1:
|
| 588 |
-
weights = {"branch": 1.0, "chain": 1.0, "coherence": 1.0, "residual_chain": 1.0, "manifold": 1.0}
|
| 589 |
-
|
| 590 |
-
return DomainStrategy(name=f"[{name}]", hyp_weights=weights, polish=polish, explore_early=explore_early)
|
| 591 |
|
| 592 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 593 |
# SECTION 8: SHARED DATACLASSES
|
|
@@ -598,29 +614,66 @@ class Hypothesis:
|
|
| 598 |
derivation:List[str]; pinned_vars:Dict[str,float]; free_vars:List[str]
|
| 599 |
confidence:float; ce:float=float('inf')
|
| 600 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 601 |
@dataclass
|
| 602 |
class HypothesisTrace:
|
| 603 |
hid:str; round_idx:int; ray_name:str; action:str
|
| 604 |
ce_before:float; ce_after:float
|
| 605 |
verify:Optional[VerifyResult]; survived:bool; elapsed_ms:float
|
|
|
|
| 606 |
|
| 607 |
@dataclass
|
| 608 |
class StructuralModel:
|
| 609 |
best_binding:Dict[str,float]; best_ce:float
|
| 610 |
-
tested:List[Hypothesis]=field(default_factory=list)
|
| 611 |
failure_patterns:Set[str]=field(default_factory=set)
|
| 612 |
scope_witnesses:Dict[str,Dict[str,Tuple]]=field(default_factory=dict)
|
| 613 |
-
confirmed_ranges:Dict[str,Tuple[float,float]]=field(default_factory=dict)
|
| 614 |
-
conflict_vars:Set[str]=field(default_factory=set)
|
| 615 |
|
| 616 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 617 |
-
# SECTION 9: ORACLES
|
| 618 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 619 |
@dataclass
|
| 620 |
class L7Certificate: topology_sig:str; hub_vars:List[str]; solve_order:List[str]
|
| 621 |
@dataclass
|
| 622 |
-
class L8Certificate: incoherent_vars:List[str]; tightened_bounds:Dict[str,Tuple[float,float]]
|
| 623 |
-
@dataclass
|
| 624 |
class L9Certificate: residual_ce:float; dominant_vars:List[str]; dominant_exprs:List[str]
|
| 625 |
|
| 626 |
class TopologyOracle:
|
|
@@ -633,19 +686,6 @@ class TopologyOracle:
|
|
| 633 |
so=sorted(active_scopes,key=lambda sn:sum(vd.get(v,0) for v in problem.scope_vars.get(sn,[])))
|
| 634 |
return L7Certificate("mesh" if len(hub)>2 else "hub" if hub else "chain",hub,so)
|
| 635 |
|
| 636 |
-
class CoherenceOracle:
|
| 637 |
-
def evaluate(self,wd):
|
| 638 |
-
inc=set(); tight={}; scopes=list(wd.keys())
|
| 639 |
-
for i in range(len(scopes)):
|
| 640 |
-
for j in range(i+1,len(scopes)):
|
| 641 |
-
ba,bb=wd[scopes[i]],wd[scopes[j]]
|
| 642 |
-
for v in set(ba)&set(bb):
|
| 643 |
-
lo_a,hi_a=ba[v]; lo_b,hi_b=bb[v]
|
| 644 |
-
o_lo=max(lo_a,lo_b); o_hi=min(hi_a,hi_b)
|
| 645 |
-
if o_lo>o_hi+1e-8: inc.add(v); tight[v]=(min(lo_a,lo_b),max(hi_a,hi_b))
|
| 646 |
-
elif o_hi>o_lo: tight[v]=(o_lo,o_hi)
|
| 647 |
-
return L8Certificate(list(inc),tight)
|
| 648 |
-
|
| 649 |
class ResidualOracle:
|
| 650 |
def evaluate(self,binding,problem,hub_vars):
|
| 651 |
ce=problem.constraint_energy(binding)
|
|
@@ -677,10 +717,11 @@ class ResidualOracle:
|
|
| 677 |
re=[e for e,c in sorted(de,key=lambda x:-x[1])[:5]]
|
| 678 |
return L9Certificate(round(ce,6),rv,re)
|
| 679 |
|
| 680 |
-
TOPOLOGY_ORACLE=TopologyOracle()
|
|
|
|
| 681 |
|
| 682 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 683 |
-
# SECTION 10: CORE SOLVERS
|
| 684 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 685 |
def _hc4(box,constraints):
|
| 686 |
cur=dict(box)
|
|
@@ -792,239 +833,6 @@ def _adam_polish(problem,binding,steps=ADAM_STEPS):
|
|
| 792 |
if nce<best_ce: best_ce=nce; best_b=dict(b)
|
| 793 |
return best_b,best_ce
|
| 794 |
|
| 795 |
-
def solve_by_hypothesis(problem:Problem, budget:int=TOTAL_BUDGET, strategy:Optional[DomainStrategy]=None) -> Dict:
|
| 796 |
-
t0=time.time()
|
| 797 |
-
explore_trigger = 2 if (strategy and strategy.explore_early) else 4
|
| 798 |
-
polish_pref = strategy.polish if strategy else "both"
|
| 799 |
-
|
| 800 |
-
init_b={v:max(lo,min(hi,(lo+hi)/2)) for v,(lo,hi) in problem.bounds.items()}
|
| 801 |
-
tb=_global_hc4_tighten(problem)
|
| 802 |
-
full_box={v:IV(tb[v][0],tb[v][1]) for v in problem.variables if v in tb}
|
| 803 |
-
mprt_b,mprt_ce=_mprt_sample(problem,full_box,N_MPRT_EXPLORE//5)
|
| 804 |
-
if mprt_ce<problem.constraint_energy(init_b): init_b=mprt_b
|
| 805 |
-
snap_b,snap_ce=_algebraic_snap(problem,init_b)
|
| 806 |
-
if snap_ce<problem.constraint_energy(init_b): init_b=snap_b
|
| 807 |
-
|
| 808 |
-
model=StructuralModel(best_binding=dict(init_b),best_ce=problem.constraint_energy(init_b))
|
| 809 |
-
active_scopes=[s for s in problem.scope_order if s!="root" and problem.scope_vars.get(s)]
|
| 810 |
-
|
| 811 |
-
if model.best_ce<SOLVE_THRESHOLD:
|
| 812 |
-
l7=TOPOLOGY_ORACLE.evaluate(problem,active_scopes)
|
| 813 |
-
l9=RESIDUAL_ORACLE.evaluate(model.best_binding,problem,l7.hub_vars)
|
| 814 |
-
return {"binding":model.best_binding,"ce":model.best_ce,"solved":True,"l7":l7,"l9":l9,"time":round(time.time()-t0,3)}
|
| 815 |
-
|
| 816 |
-
generator=HypothesisGenerator(strategy=strategy); consec=0
|
| 817 |
-
for round_idx in range(HYPOTHESIS_MAX_ROUNDS):
|
| 818 |
-
if model.best_ce<SOLVE_THRESHOLD: break
|
| 819 |
-
l7=TOPOLOGY_ORACLE.evaluate(problem,active_scopes)
|
| 820 |
-
l8=COHERENCE_ORACLE.evaluate(model.scope_witnesses)
|
| 821 |
-
l9=RESIDUAL_ORACLE.evaluate(model.best_binding,problem,l7.hub_vars)
|
| 822 |
-
hypotheses=generator.generate(problem,model,l7,l8,l9,round_idx)
|
| 823 |
-
improved=False
|
| 824 |
-
for hyp in hypotheses[:MAX_HYPS_PER_ROUND]:
|
| 825 |
-
if model.best_ce<SOLVE_THRESHOLD: break
|
| 826 |
-
tb2,tce=_test_hypothesis(problem,hyp)
|
| 827 |
-
if tce<model.best_ce:
|
| 828 |
-
model.best_ce=tce; model.best_binding=dict(tb2); improved=True; consec=0
|
| 829 |
-
for sn in active_scopes:
|
| 830 |
-
sv=problem.scope_vars.get(sn,[]); sb={v:tb2[v] for v in sv if v in tb2}
|
| 831 |
-
if sb: model.scope_witnesses[sn]={v:(val-1e-3,val+1e-3) for v,val in sb.items()}
|
| 832 |
-
else: model.failure_patterns.add(hyp.hid)
|
| 833 |
-
if not improved:
|
| 834 |
-
consec+=1
|
| 835 |
-
if consec>=explore_trigger:
|
| 836 |
-
work_box={v:IV(*problem.bounds[v]) for v in problem.variables}
|
| 837 |
-
eb,ece=_mprt_sample(problem,work_box,N_MPRT_EXPLORE)
|
| 838 |
-
if ece<model.best_ce: model.best_ce=ece; model.best_binding=dict(eb); consec=0
|
| 839 |
-
|
| 840 |
-
# Strategy-directed polish
|
| 841 |
-
if polish_pref in ("gradient","both") and SOLVE_THRESHOLD<model.best_ce<2.0:
|
| 842 |
-
gb,gce=_gradient_polish(problem,model.best_binding)
|
| 843 |
-
if gce<model.best_ce: model.best_ce=gce; model.best_binding=gb
|
| 844 |
-
if polish_pref in ("adam","both") and SOLVE_THRESHOLD<model.best_ce<1.0:
|
| 845 |
-
ab,ace=_adam_polish(problem,model.best_binding)
|
| 846 |
-
if ace<model.best_ce: model.best_ce=ace; model.best_binding=ab
|
| 847 |
-
|
| 848 |
-
final_l7=TOPOLOGY_ORACLE.evaluate(problem,active_scopes)
|
| 849 |
-
final_l9=RESIDUAL_ORACLE.evaluate(model.best_binding,problem,final_l7.hub_vars)
|
| 850 |
-
return {"binding":model.best_binding,"ce":model.best_ce,"solved":model.best_ce<SOLVE_THRESHOLD,
|
| 851 |
-
"l7":final_l7,"l9":final_l9,"time":round(time.time()-t0,3)}
|
| 852 |
-
|
| 853 |
-
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 854 |
-
# SECTION 11: HYPOTHESIS GENERATOR (Enzymes / Permutation Factory)
|
| 855 |
-
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 856 |
-
class HypothesisGenerator:
|
| 857 |
-
def __init__(self, strategy:Optional[DomainStrategy]=None):
|
| 858 |
-
self.strategy=strategy
|
| 859 |
-
|
| 860 |
-
def generate(self,problem,model,l7,l8,l9,round_idx):
|
| 861 |
-
hyps=[]
|
| 862 |
-
w_br = self.strategy.hyp_weights.get("branch",1.0) if self.strategy else 1.0
|
| 863 |
-
w_ch = self.strategy.hyp_weights.get("chain",1.0) if self.strategy else 1.0
|
| 864 |
-
w_co = self.strategy.hyp_weights.get("coherence",1.0) if self.strategy else 1.0
|
| 865 |
-
w_rc = self.strategy.hyp_weights.get("residual_chain",1.0) if self.strategy else 1.0
|
| 866 |
-
w_mf = self.strategy.hyp_weights.get("manifold",1.0) if self.strategy else 1.0
|
| 867 |
-
|
| 868 |
-
# Stacking (Enzyme): Branch + Chain composite
|
| 869 |
-
w_cmp = min(w_br, w_ch)
|
| 870 |
-
|
| 871 |
-
if w_br > 0.01: hyps.extend(self._branch_hypotheses(problem,model,l9))
|
| 872 |
-
if w_ch > 0.01: hyps.extend(self._chain_hypotheses(problem,model,l7))
|
| 873 |
-
if w_co > 0.01: hyps.extend(self._coherence_hypotheses(problem,model,l8))
|
| 874 |
-
if w_rc > 0.01: hyps.extend(self._residual_chain_hypotheses(problem,model,l9))
|
| 875 |
-
if w_mf > 0.01 and round_idx>=3: hyps.extend(self._manifold_tangent_hypotheses(problem,model,l9))
|
| 876 |
-
if w_cmp > 0.01: hyps.extend(self._composite_hypotheses(problem,model,l7,l9))
|
| 877 |
-
|
| 878 |
-
if self.strategy:
|
| 879 |
-
for hyp in hyps:
|
| 880 |
-
w=self.strategy.hyp_weights.get(hyp.h_type,1.0)
|
| 881 |
-
hyp.confidence=min(0.99,hyp.confidence*w)
|
| 882 |
-
|
| 883 |
-
hyps=[h for h in hyps if h.hid not in model.failure_patterns]
|
| 884 |
-
return sorted(hyps,key=lambda h:-h.confidence)
|
| 885 |
-
|
| 886 |
-
def _composite_hypotheses(self,problem,model,l7,l9):
|
| 887 |
-
"""Enzyme: Pins a branch value and instantly cascades a chain reaction through interval arithmetic."""
|
| 888 |
-
hyps=[]
|
| 889 |
-
if not l7.solve_order or not l9.dominant_exprs: return hyps
|
| 890 |
-
ref=model.best_binding
|
| 891 |
-
tb=_global_hc4_tighten(problem)
|
| 892 |
-
for expr_str in l9.dominant_exprs[:3]:
|
| 893 |
-
mc=next((mc for mc in problem.compiled_constraints if mc.expr_str==expr_str),None)
|
| 894 |
-
if not mc or not mc.projections: continue
|
| 895 |
-
for v,proj_list in mc.projections.items():
|
| 896 |
-
lo,hi=problem.bounds.get(v,(-1e18,1e18))
|
| 897 |
-
for pi,proj in enumerate(proj_list):
|
| 898 |
-
try:
|
| 899 |
-
val=float(proj["func"](*[ref.get(s,0.0) for s in proj["syms"]]))
|
| 900 |
-
if not math.isfinite(val) or abs(val)>1e6 or not(lo<=val<=hi): continue
|
| 901 |
-
|
| 902 |
-
# 1. Pin the branch
|
| 903 |
-
start_box={u: IV(*tb.get(u, problem.bounds.get(u, (-10,10)))) for u in problem.variables}
|
| 904 |
-
start_box[v]=IV(val-1e-6, val+1e-6)
|
| 905 |
-
|
| 906 |
-
# 2. Trigger the cascade
|
| 907 |
-
cont=_hc4(start_box, problem.compiled_constraints)
|
| 908 |
-
if cont:
|
| 909 |
-
b=dict(ref)
|
| 910 |
-
for u,iv in cont.items(): b[u]=iv.mid()
|
| 911 |
-
# Anything contracted to near-zero width is solidly pinned by the cascade
|
| 912 |
-
pinned={u:b[u] for u in problem.variables if cont[u].width() < 1e-2}
|
| 913 |
-
hyps.append(Hypothesis(
|
| 914 |
-
hid=f"cmp_{hash(expr_str)%9999}_{v}_{pi}",
|
| 915 |
-
binding=b, h_type="composite",
|
| 916 |
-
claim=f"Enz(Br({v})βChain)",
|
| 917 |
-
derivation=[expr_str, "hc4_chain"],
|
| 918 |
-
pinned_vars=pinned,
|
| 919 |
-
free_vars=[u for u in problem.variables if u not in pinned],
|
| 920 |
-
confidence=0.90 if pi==0 else 0.80))
|
| 921 |
-
except: pass
|
| 922 |
-
return hyps
|
| 923 |
-
|
| 924 |
-
def _branch_hypotheses(self,problem,model,l9):
|
| 925 |
-
hyps=[]; ref=model.best_binding
|
| 926 |
-
for expr_str in l9.dominant_exprs[:4]:
|
| 927 |
-
mc=next((mc for mc in problem.compiled_constraints if mc.expr_str==expr_str),None)
|
| 928 |
-
if not mc or not mc.projections: continue
|
| 929 |
-
for v,proj_list in mc.projections.items():
|
| 930 |
-
lo,hi=problem.bounds.get(v,(-1e18,1e18))
|
| 931 |
-
for pi,proj in enumerate(proj_list):
|
| 932 |
-
try:
|
| 933 |
-
val=float(proj["func"](*[ref.get(s,0.0) for s in proj["syms"]]))
|
| 934 |
-
if not math.isfinite(val) or abs(val)>1e6 or not(lo<=val<=hi): continue
|
| 935 |
-
b=dict(ref); b[v]=val
|
| 936 |
-
hyps.append(Hypothesis(hid=f"br_{hash(expr_str)%9999}_{v}_{pi}",
|
| 937 |
-
binding=b,h_type="branch",claim=f"AlgBranch:{v}={val:.4f}",
|
| 938 |
-
derivation=[expr_str],pinned_vars={v:val},
|
| 939 |
-
free_vars=[u for u in problem.variables if u!=v],
|
| 940 |
-
confidence=0.85 if pi==0 else 0.70))
|
| 941 |
-
except: pass
|
| 942 |
-
return hyps
|
| 943 |
-
|
| 944 |
-
def _chain_hypotheses(self,problem,model,l7):
|
| 945 |
-
if not l7.solve_order: return []
|
| 946 |
-
hyps=[]; tb=_global_hc4_tighten(problem); b=dict(model.best_binding); chain_steps=[]
|
| 947 |
-
for sn in l7.solve_order:
|
| 948 |
-
svars=problem.scope_vars.get(sn,[])
|
| 949 |
-
if not svars: continue
|
| 950 |
-
scope_mcs=[problem.compiled_constraints[i] for i in problem.scope_groups.get(sn,[])]
|
| 951 |
-
if not scope_mcs: continue
|
| 952 |
-
start_box={v:IV(*tb.get(v,problem.bounds.get(v,(-10,10)))) for v in svars if v in problem.bounds}
|
| 953 |
-
cont=_hc4(start_box,scope_mcs)
|
| 954 |
-
if cont:
|
| 955 |
-
for v,iv in cont.items():
|
| 956 |
-
b[v]=iv.mid()
|
| 957 |
-
chain_steps.append(sn)
|
| 958 |
-
if chain_steps:
|
| 959 |
-
hyps.append(Hypothesis(
|
| 960 |
-
hid=f"chain_{'_'.join(c[:4] for c in chain_steps)}",
|
| 961 |
-
binding=b,h_type="chain",claim=f"TopoChain({' β '.join(chain_steps)})",
|
| 962 |
-
derivation=chain_steps,
|
| 963 |
-
pinned_vars={v:b[v] for sn in chain_steps for v in problem.scope_vars.get(sn,[]) if v in b},
|
| 964 |
-
free_vars=[v for v in problem.variables if not any(v in problem.scope_vars.get(sn,[]) for sn in chain_steps)],
|
| 965 |
-
confidence=0.80))
|
| 966 |
-
return hyps
|
| 967 |
-
|
| 968 |
-
def _coherence_hypotheses(self,problem,model,l8):
|
| 969 |
-
if not l8.incoherent_vars: return []
|
| 970 |
-
b=dict(model.best_binding)
|
| 971 |
-
for v,(lo,hi) in l8.tightened_bounds.items():
|
| 972 |
-
if v in problem.bounds: b[v]=(lo+hi)/2.0
|
| 973 |
-
return [Hypothesis(hid=f"coh_{hash(tuple(sorted(l8.incoherent_vars)))%9999}",
|
| 974 |
-
binding=b,h_type="coherence",claim=f"CoherMeet({', '.join(list(l8.incoherent_vars)[:3])})",
|
| 975 |
-
derivation=list(l8.incoherent_vars),
|
| 976 |
-
pinned_vars={v:b[v] for v in l8.incoherent_vars if v in b},
|
| 977 |
-
free_vars=[v for v in problem.variables if v not in l8.incoherent_vars],
|
| 978 |
-
confidence=0.70)]
|
| 979 |
-
|
| 980 |
-
def _residual_chain_hypotheses(self,problem,model,l9):
|
| 981 |
-
if not l9.dominant_vars: return []
|
| 982 |
-
hyps=[]; b=dict(model.best_binding); chain=[]; depth=0
|
| 983 |
-
for tv in l9.dominant_vars[:BRANCH_DEPTH]:
|
| 984 |
-
if depth>=BRANCH_DEPTH: break
|
| 985 |
-
for mc in problem.compiled_constraints:
|
| 986 |
-
if tv not in mc.syms_used or tv not in mc.projections: continue
|
| 987 |
-
for proj in mc.projections[tv]:
|
| 988 |
-
try:
|
| 989 |
-
val=float(proj["func"](*[b.get(s,0.0) for s in proj["syms"]]))
|
| 990 |
-
lo,hi=problem.bounds.get(tv,(-1e18,1e18))
|
| 991 |
-
if not(lo<=val<=hi) or not math.isfinite(val): continue
|
| 992 |
-
b[tv]=val; chain.append(f"{tv}={val:.3f}"); depth+=1; break
|
| 993 |
-
except: pass
|
| 994 |
-
if depth>len(chain)-1: break
|
| 995 |
-
if chain:
|
| 996 |
-
hyps.append(Hypothesis(hid=f"rchain_{hash(str(chain))%9999}",
|
| 997 |
-
binding=b,h_type="residual_chain",claim=f"ResChain({' β '.join(chain)})",
|
| 998 |
-
derivation=l9.dominant_exprs[:len(chain)],
|
| 999 |
-
pinned_vars={v:b[v] for v in l9.dominant_vars[:len(chain)] if v in b},
|
| 1000 |
-
free_vars=[v for v in problem.variables if v not in l9.dominant_vars[:len(chain)]],
|
| 1001 |
-
confidence=0.65))
|
| 1002 |
-
return hyps
|
| 1003 |
-
|
| 1004 |
-
def _manifold_tangent_hypotheses(self,problem,model,l9):
|
| 1005 |
-
hyps=[]; b=model.best_binding
|
| 1006 |
-
eq_mcs=[mc for mc in problem.compiled_constraints if mc.kind=="equality" and mc.fast_jac]
|
| 1007 |
-
if not eq_mcs: return hyps
|
| 1008 |
-
nv=len(problem.variables); J=np.zeros((len(eq_mcs),nv))
|
| 1009 |
-
for i,mc in enumerate(eq_mcs):
|
| 1010 |
-
for j,v in enumerate(problem.variables):
|
| 1011 |
-
if v not in mc.fast_jac: continue
|
| 1012 |
-
jac=mc.fast_jac[v]
|
| 1013 |
-
try: J[i,j]=float(jac["func"](*[b.get(s,0.0) for s in jac["syms"]]))
|
| 1014 |
-
except: pass
|
| 1015 |
-
try:
|
| 1016 |
-
_,sv,Vt=np.linalg.svd(J,full_matrices=True); rank=np.sum(sv>1e-8)
|
| 1017 |
-
if rank>=Vt.shape[0]: return hyps
|
| 1018 |
-
for di,nd in enumerate(Vt[rank:][:2]):
|
| 1019 |
-
for step in MANIFOLD_STEPS:
|
| 1020 |
-
nb={v:max(problem.bounds[v][0],min(problem.bounds[v][1],b.get(v,0.0)+step*nd[j]))
|
| 1021 |
-
for j,v in enumerate(problem.variables)}
|
| 1022 |
-
hyps.append(Hypothesis(hid=f"mfld_d{di}_s{step}",binding=nb,h_type="manifold",
|
| 1023 |
-
claim=f"Manifold(dir={di},step={step:.2f})",derivation=[f"null_dir_{di}"],
|
| 1024 |
-
pinned_vars={},free_vars=problem.variables,confidence=0.45))
|
| 1025 |
-
except: pass
|
| 1026 |
-
return hyps
|
| 1027 |
-
|
| 1028 |
def _test_hypothesis(problem,hyp):
|
| 1029 |
b=dict(hyp.binding)
|
| 1030 |
for v,(lo,hi) in problem.bounds.items():
|
|
@@ -1050,71 +858,700 @@ def _test_hypothesis(problem,hyp):
|
|
| 1050 |
return best_b,best_ce
|
| 1051 |
|
| 1052 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1053 |
-
# SECTION
|
|
|
|
|
|
|
|
|
|
| 1054 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1055 |
-
@dataclass
|
| 1056 |
-
class RayTraceRound:
|
| 1057 |
-
round_idx:int; ray_axioms:Set[str]; ray_name:str
|
| 1058 |
-
ce:float; solved:bool; traces:List[HypothesisTrace]=field(default_factory=list)
|
| 1059 |
|
| 1060 |
-
|
| 1061 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1062 |
|
| 1063 |
-
|
| 1064 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1065 |
best_ce = float('inf')
|
| 1066 |
-
best_binding = {}
|
| 1067 |
-
|
| 1068 |
-
|
| 1069 |
-
|
| 1070 |
-
rays_to_test = random.sample(AXIOM_HYPERCUBE, self.WAVEFRONT_SIZE)
|
| 1071 |
-
if axl_def.axioms and axl_def.axioms not in rays_to_test:
|
| 1072 |
-
rays_to_test[0] = axl_def.axioms
|
| 1073 |
-
|
| 1074 |
-
print(f"\n{'β'*65}\nTHEORIST RAY TRACE: {axl_def.name}\n{'β'*65}")
|
| 1075 |
-
|
| 1076 |
-
for round_idx, ray_axioms in enumerate(rays_to_test):
|
| 1077 |
-
strategy = compile_strategy(ray_axioms)
|
| 1078 |
-
print(f"\n[Ray {round_idx+1}/{self.WAVEFRONT_SIZE}] Firing: {strategy.name}")
|
| 1079 |
-
|
| 1080 |
-
t_start = time.time()
|
| 1081 |
-
result = solve_by_hypothesis(base_problem, budget=TOTAL_BUDGET, strategy=strategy)
|
| 1082 |
-
elapsed = round((time.time()-t_start)*1000, 1)
|
| 1083 |
-
|
| 1084 |
-
binding = result["binding"]
|
| 1085 |
-
verify = VERIFY_LAYER.run(binding, base_problem, axl_def.anchors)
|
| 1086 |
-
base_ce = verify.gate1_ce
|
| 1087 |
-
|
| 1088 |
-
trace = HypothesisTrace(
|
| 1089 |
-
hid=f"R{round_idx+1}", round_idx=round_idx+1,
|
| 1090 |
-
ray_name=strategy.name, action="Wavefront",
|
| 1091 |
-
ce_before=best_ce if best_ce < float('inf') else 99.0,
|
| 1092 |
-
ce_after=base_ce, verify=verify,
|
| 1093 |
-
survived=verify.overall_pass, elapsed_ms=elapsed
|
| 1094 |
-
)
|
| 1095 |
-
self.all_traces.append(trace)
|
| 1096 |
|
| 1097 |
-
|
| 1098 |
-
|
| 1099 |
-
f"G2={'β' if verify.gate2_pass else 'β'} | {status}")
|
| 1100 |
-
for inv_name, (err, passed) in verify.gate2_results.items():
|
| 1101 |
-
print(f" [{'β' if passed else 'β'}] {inv_name}: |err|={err:.6f}")
|
| 1102 |
|
| 1103 |
-
|
| 1104 |
-
|
| 1105 |
-
|
| 1106 |
-
|
|
|
|
|
|
|
|
|
|
| 1107 |
|
| 1108 |
-
|
| 1109 |
|
| 1110 |
-
|
| 1111 |
-
|
|
|
|
|
|
|
|
|
|
| 1112 |
|
| 1113 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1114 |
return best_binding, best_ce, history
|
| 1115 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1116 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1117 |
-
# SECTION
|
| 1118 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1119 |
AXL_PROBLEMS=[
|
| 1120 |
AXLProblemDef(
|
|
@@ -1127,7 +1564,7 @@ AXL_PROBLEMS=[
|
|
| 1127 |
],
|
| 1128 |
constraints=[
|
| 1129 |
{"kind":"CONSERVE","expr":"x1**2 + x2**2 + x3**2 + x4**2 - 1.0"},
|
| 1130 |
-
{"kind":"EQ",
|
| 1131 |
],
|
| 1132 |
scopes=[{"name":"sphere","order":0,"vars":["x1","x2","x3","x4"],
|
| 1133 |
"constraints":[{"kind":"EQ","expr":"x1**2 + x2**2 + x3**2 + x4**2 - 1.0","weight":5.0}]}],
|
|
@@ -1192,7 +1629,8 @@ AXL_PROBLEMS=[
|
|
| 1192 |
description="3 vars packed with min separation, centred, norm=6",
|
| 1193 |
axioms={Axiom.CONTINUOUS,Axiom.METRIC,Axiom.INJECTIVE,Axiom.CONSERVED,Axiom.SYMMETRIC},
|
| 1194 |
variables=[
|
| 1195 |
-
{"name":"a","lo":-3.0,"hi":3.0}, {"name":"b","lo":-3.0,"hi":3.0},
|
|
|
|
| 1196 |
],
|
| 1197 |
constraints=[
|
| 1198 |
{"kind":"CONSERVE","expr":"a + b + c"},
|
|
@@ -1201,9 +1639,7 @@ AXL_PROBLEMS=[
|
|
| 1201 |
{"kind":"GEQ","expr":"(a - c)**2 - 4.0","weight":2.0},
|
| 1202 |
],
|
| 1203 |
scopes=[{"name":"packing","order":0,"vars":["a","b","c"],
|
| 1204 |
-
"constraints":[
|
| 1205 |
-
{"kind":"EQ","expr":"a**2 + b**2 + c**2 - 6.0","weight":2.0},
|
| 1206 |
-
]}],
|
| 1207 |
anchors=[
|
| 1208 |
AXLInvariant("centred","a + b + c",1e-3),
|
| 1209 |
AXLInvariant("sep_ab","(a - b)**2 - 1.0",0.5),
|
|
@@ -1213,50 +1649,57 @@ AXL_PROBLEMS=[
|
|
| 1213 |
),
|
| 1214 |
]
|
| 1215 |
|
| 1216 |
-
def build_base_problem(axl_def:AXLProblemDef) -> Problem:
|
| 1217 |
-
psl_text=AXL_COMPILER.compile(axl_def)
|
| 1218 |
-
prog=parse_psl(psl_text); ep=expand_psl(prog)
|
| 1219 |
-
return Problem(pid=f"base_{axl_def.name}",variables=ep.variables,
|
| 1220 |
-
constraints=ep.constraints,bounds=ep.bounds,
|
| 1221 |
-
scope_groups=ep.scope_groups,scope_vars=ep.scope_vars,
|
| 1222 |
-
scope_order=ep.scope_order,annotations=ep.annotations)
|
| 1223 |
|
| 1224 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1225 |
-
# SECTION
|
| 1226 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1227 |
-
STATE_LOCK=threading.Lock()
|
| 1228 |
-
RUN_LOG:List[Dict]=[]
|
| 1229 |
-
THEORIST=
|
| 1230 |
-
POOL=ThreadPoolExecutor(max_workers=2)
|
| 1231 |
|
| 1232 |
-
def _run_problem(axl_def:AXLProblemDef):
|
| 1233 |
try:
|
| 1234 |
base_prob = build_base_problem(axl_def)
|
| 1235 |
-
binding, ce,
|
| 1236 |
-
|
| 1237 |
survived = [t for t in THEORIST.all_traces if t.survived]
|
| 1238 |
-
failed
|
| 1239 |
-
|
| 1240 |
-
|
| 1241 |
-
record={
|
| 1242 |
-
"problem":
|
| 1243 |
"description": axl_def.description,
|
| 1244 |
-
"ce":
|
| 1245 |
-
"solved":
|
| 1246 |
-
"binding":
|
| 1247 |
-
"observations":
|
| 1248 |
"traces": [{
|
| 1249 |
-
"round":
|
| 1250 |
-
"
|
| 1251 |
-
"
|
| 1252 |
-
"
|
| 1253 |
-
"
|
| 1254 |
-
"
|
| 1255 |
-
"
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1256 |
} for t in THEORIST.all_traces],
|
|
|
|
| 1257 |
"survived_count": len(survived),
|
| 1258 |
-
"failed_count":
|
| 1259 |
-
"best_ray":
|
|
|
|
| 1260 |
}
|
| 1261 |
with STATE_LOCK:
|
| 1262 |
RUN_LOG.append(record)
|
|
@@ -1266,9 +1709,9 @@ def _run_problem(axl_def:AXLProblemDef):
|
|
| 1266 |
print(f"[RUN ERROR] {axl_def.name}: {e}")
|
| 1267 |
|
| 1268 |
async def run_loop():
|
| 1269 |
-
loop=asyncio.get_event_loop()
|
| 1270 |
while True:
|
| 1271 |
-
prob=random.choice(AXL_PROBLEMS)
|
| 1272 |
await loop.run_in_executor(POOL, _run_problem, prob)
|
| 1273 |
await asyncio.sleep(0.3)
|
| 1274 |
|
|
@@ -1279,55 +1722,58 @@ async def lifespan(app):
|
|
| 1279 |
POOL.shutdown(wait=False)
|
| 1280 |
|
| 1281 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1282 |
-
# SECTION
|
| 1283 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1284 |
-
app=FastAPI(title="Practicality
|
| 1285 |
|
| 1286 |
-
def _render_collapse(record:Dict) -> str:
|
| 1287 |
-
b=record["binding"]; traces=record["traces"]
|
| 1288 |
-
survived=[t for t in traces if t["survived"]]
|
| 1289 |
-
best=min(survived,key=lambda t:t["ce"],default=None)
|
| 1290 |
-
if not best and traces:
|
| 1291 |
-
|
|
|
|
| 1292 |
|
| 1293 |
-
solved=record["solved"]
|
| 1294 |
-
|
| 1295 |
-
|
| 1296 |
-
status="β SOLVED + VERIFIED" if solved else ("~ PARTIAL" if ce<0.5 else "β UNSOLVED")
|
| 1297 |
|
| 1298 |
-
binding_rows="".join(
|
| 1299 |
f"<tr><td style='color:#888;width:70px'>{v}</td>"
|
| 1300 |
f"<td style='color:#26C6DA;font-weight:700'>{val:+.5f}</td>"
|
| 1301 |
f"<td style='color:#4CAF50;font-size:0.75em'>{'[OBS]' if v in obs_vars else ''}</td></tr>"
|
| 1302 |
for v,val in b.items())
|
| 1303 |
|
| 1304 |
-
inv_rows=""
|
| 1305 |
if best and best.get("g2_detail"):
|
| 1306 |
for inv,(err,ok) in best["g2_detail"].items():
|
| 1307 |
-
c="#4CAF50" if ok else "#EF5350"
|
| 1308 |
-
inv_rows+=(f"<tr><td style='color:{c}'>{'β' if ok else 'β'}</td>"
|
| 1309 |
-
|
| 1310 |
-
|
| 1311 |
|
| 1312 |
def trail_span(t):
|
| 1313 |
-
|
| 1314 |
-
|
| 1315 |
-
|
| 1316 |
-
|
| 1317 |
-
|
| 1318 |
-
|
| 1319 |
-
f"
|
|
|
|
|
|
|
|
|
|
| 1320 |
f"<span style='color:#4CAF50;font-weight:700'>{star}</span></div>")
|
| 1321 |
|
| 1322 |
-
trail="".join(trail_span(t) for t in traces)
|
| 1323 |
|
| 1324 |
return f"""
|
| 1325 |
-
<div style='border:1px solid #
|
| 1326 |
<div style='background:#0e0e0e;padding:9px 14px;border-bottom:1px solid #1a1a1a;display:flex;align-items:center;gap:16px'>
|
| 1327 |
<span style='color:{ce_color};font-weight:700;font-size:1.05em'>{status}</span>
|
| 1328 |
<span style='color:#444;font-size:0.85em'>{record["problem"]}</span>
|
| 1329 |
-
<span style='color:#333;font-size:0.8em'>
|
| 1330 |
-
<span style='color:#26C6DA;font-size:0.75em'>{record["survived_count"]} survived / {record["
|
| 1331 |
</div>
|
| 1332 |
<div style='display:flex'>
|
| 1333 |
<div style='flex:0 0 180px;padding:10px 12px;border-right:1px solid #1a1a1a'>
|
|
@@ -1340,50 +1786,54 @@ def _render_collapse(record:Dict) -> str:
|
|
| 1340 |
{inv_rows or "<tr><td colspan='3' style='color:#222'>β</td></tr>"}
|
| 1341 |
</table>
|
| 1342 |
</div>
|
| 1343 |
-
<div style='flex:1;padding:10px 12px'>
|
| 1344 |
<div style='color:#333;font-size:0.7em;margin-bottom:5px'>
|
| 1345 |
-
|
| 1346 |
</div>
|
| 1347 |
{trail}
|
| 1348 |
</div>
|
| 1349 |
</div>
|
| 1350 |
</div>"""
|
| 1351 |
|
| 1352 |
-
@app.get("/",response_class=HTMLResponse)
|
| 1353 |
async def dashboard():
|
| 1354 |
-
with STATE_LOCK: log=list(reversed(RUN_LOG[-10:]))
|
| 1355 |
-
runs=len(RUN_LOG)
|
| 1356 |
-
|
|
|
|
| 1357 |
|
| 1358 |
-
|
|
|
|
| 1359 |
for r in log:
|
| 1360 |
-
for t in r.get("traces",
|
| 1361 |
-
ray_str = t["ray"]
|
| 1362 |
-
|
| 1363 |
-
for
|
| 1364 |
-
if not
|
| 1365 |
-
axiom_stats[
|
| 1366 |
-
axiom_stats[
|
| 1367 |
-
if t["survived"]:
|
| 1368 |
-
|
| 1369 |
-
|
|
|
|
| 1370 |
f"<tr><td style='color:#FF9800'>{ax}</td>"
|
| 1371 |
f"<td style='color:#aaa'>{s['tried']}</td>"
|
|
|
|
| 1372 |
f"<td style='color:#4CAF50'>{s['survived']}</td>"
|
| 1373 |
f"<td style='color:#EF5350'>{s['tried']-s['survived']}</td>"
|
| 1374 |
f"<td style='color:#26C6DA'>{round(s['total_ce']/s['tried'],5) if s['tried'] else 0}</td>"
|
| 1375 |
f"<td style='color:{'#4CAF50' if s['survived']>0 else '#333'}'>"
|
| 1376 |
f"{round(s['survived']/s['tried']*100):.0f}%</td></tr>"
|
| 1377 |
-
for ax,s in sorted(axiom_stats.items(),key=lambda x:-x[1]["survived"])
|
| 1378 |
-
) or "<tr><td colspan='
|
| 1379 |
|
| 1380 |
-
collapses="".join(_render_collapse(r) for r in log) if log else \
|
| 1381 |
"<div style='color:#222;padding:20px'>Warming upβ¦</div>"
|
| 1382 |
|
| 1383 |
-
return f"""<!DOCTYPE html><html><head><title>Practicality
|
| 1384 |
<meta http-equiv="refresh" content="4">
|
| 1385 |
<style>
|
| 1386 |
-
body{{background:#090909;color:#e0e0e0;font-family:monospace;padding:20px;max-width:
|
| 1387 |
h1{{color:#26C6DA;border-bottom:1px solid #1a1a1a;padding-bottom:6px;font-size:1.15em}}
|
| 1388 |
h3{{color:#2a2a2a;margin-top:20px;font-size:0.85em;letter-spacing:2px;text-transform:uppercase}}
|
| 1389 |
table{{width:100%;border-collapse:collapse;margin-bottom:10px}}
|
|
@@ -1391,25 +1841,27 @@ async def dashboard():
|
|
| 1391 |
th{{color:#2a2a2a;font-size:0.72em}}
|
| 1392 |
.badge{{display:inline-block;padding:3px 10px;border-radius:3px;background:#0e0e0e;margin:2px;font-size:0.78em;border:1px solid #1a1a1a}}
|
| 1393 |
</style></head><body>
|
| 1394 |
-
<h1>β Practicality
|
| 1395 |
<div style='color:#333;font-size:0.75em;margin-bottom:12px'>
|
| 1396 |
-
|
|
|
|
|
|
|
| 1397 |
</div>
|
| 1398 |
<div style='margin-bottom:16px'>
|
| 1399 |
<span class='badge' style='color:#aaa'>Runs: {runs}</span>
|
| 1400 |
<span class='badge' style='color:#4CAF50'>Solved: {solved}</span>
|
| 1401 |
-
<span class='badge' style='color:#26C6DA'>Avg
|
| 1402 |
<span class='badge' style='color:#FF9800'>Problems: {len(AXL_PROBLEMS)}</span>
|
| 1403 |
-
<span class='badge' style='color:#5C6BC0'>
|
| 1404 |
</div>
|
| 1405 |
-
<h3>Axiom Efficacy
|
| 1406 |
<table>
|
| 1407 |
-
<tr><th>Axiom</th><th>
|
| 1408 |
{axiom_rows}
|
| 1409 |
</table>
|
| 1410 |
<h3>Collapse View β Recent Runs</h3>
|
| 1411 |
{collapses}
|
| 1412 |
</body></html>"""
|
| 1413 |
|
| 1414 |
-
if __name__=="__main__":
|
| 1415 |
-
uvicorn.run(app,host="0.0.0.0",port=7860,log_level="warning")
|
|
|
|
| 1 |
#!/usr/bin/env python3
|
| 2 |
"""
|
| 3 |
+
PRACTICALITY SYSTEM 13.0 β SEQUENCE RAYS
|
| 4 |
βββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 5 |
+
NEW IN 13.0:
|
| 6 |
+
Β· 27 Axioms: expanded from 15 to include physics (EQUILIBRIUM,
|
| 7 |
+
SUPERPOSITION, LOCALITY, EXTREMAL, ENTROPY), mathematics
|
| 8 |
+
(MONOTONE, CONVEX, PARSIMONY), logic/philosophy (DUALITY,
|
| 9 |
+
HOLISM, IMPLICATION, NEGATION).
|
| 10 |
+
Β· Rays as Ordered Sequences: [AβBβC] β [CβBβA]. Sequence order
|
| 11 |
+
is structural. Each axiom constructor is called in order with
|
| 12 |
+
the partial binding produced by all prior axioms as its context.
|
| 13 |
+
Β· Contradiction at Distance: contradicting axioms forbidden only
|
| 14 |
+
when ADJACENT in the sequence. Non-adjacent contradictions are
|
| 15 |
+
allowed β the chain earns its own coherence through mediating
|
| 16 |
+
axioms between them.
|
| 17 |
+
Β· Baton Protocol: rays do not fail, they terminate with a partial
|
| 18 |
+
binding (the baton). Child rays inherit it and continue.
|
| 19 |
+
Branching occurs from both stalling AND productive rays.
|
| 20 |
+
Β· Earned Extension: a ray earns the right to branch by achieving
|
| 21 |
+
a CE reduction ratio. Below MIN_DEPTH all rays branch freely.
|
| 22 |
+
Β· Each axiom owns its own hypothesis constructor derived from its
|
| 23 |
+
mathematical/physical meaning β not a weight scalar on shared types.
|
| 24 |
+
Β· Wisdom lives in the combinatorial sequence space itself.
|
| 25 |
+
No learning. No signatures. No bias.
|
| 26 |
"""
|
| 27 |
|
| 28 |
import time, random, math, threading, asyncio, warnings, itertools
|
|
|
|
| 44 |
warnings.filterwarnings("ignore")
|
| 45 |
USE_GPU = torch.cuda.is_available()
|
| 46 |
DEVICE = torch.device("cuda" if USE_GPU else "cpu")
|
| 47 |
+
print(f"[SYSTEM 13.0] Compute: {'GPU' if USE_GPU else 'CPU'}")
|
| 48 |
|
| 49 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 50 |
# SECTION 1: CONSTANTS
|
|
|
|
| 52 |
SOLVE_THRESHOLD = 0.05
|
| 53 |
VERIFY_G1_THRESHOLD = 0.08
|
| 54 |
VERIFY_G2_TOLERANCE = 1e-3
|
|
|
|
| 55 |
HC4_VOLUME_FLOOR = 0.20
|
| 56 |
L9_CONTRIB_THRESHOLD = 1e-8
|
| 57 |
HUB_RESIDUAL_MULT = 2.0
|
| 58 |
HUB_DEGREE_RATIO = 0.6
|
| 59 |
+
MAX_HYPS_PER_AXIOM = 4
|
|
|
|
| 60 |
BRANCH_DEPTH = 3
|
| 61 |
MANIFOLD_STEPS = [0.05, 0.2, -0.05, -0.2, 0.5, -0.5]
|
| 62 |
N_MPRT_EXPLORE = 20000 if USE_GPU else 3000
|
|
|
|
| 134 |
return _c(expr)
|
| 135 |
|
| 136 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 137 |
+
# SECTION 3: PSL 2.0 PARSER (unchanged from 12.1)
|
| 138 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 139 |
@dataclass
|
| 140 |
class PSLVar: name:str; lo:float; hi:float; weight:float=1.0
|
|
|
|
| 180 |
advance()
|
| 181 |
scons.append(PSLConstraint("or_eq","",scope=sname,weight=1.0,branches=opts))
|
| 182 |
elif kw=="ANNOTATE":
|
| 183 |
+
parts=rest.split()
|
| 184 |
if len(parts)>=3: prog.annotations[parts[0]]=parts[2]
|
| 185 |
return PSLScope(sname,order,depends or [],svars,links,scons)
|
|
|
|
| 186 |
while i<len(lines):
|
| 187 |
l=advance(); tk=l.split(None,1)
|
| 188 |
kw=tk[0].upper() if tk else ""; rest=tk[1].strip() if len(tk)>1 else ""
|
|
|
|
| 202 |
advance()
|
| 203 |
prog.constraints.append(PSLConstraint("or_eq","",weight=1.0,branches=opts))
|
| 204 |
elif kw=="ANNOTATE":
|
| 205 |
+
parts=rest.split()
|
| 206 |
if len(parts)>=3: prog.annotations[parts[0]]=parts[2]
|
| 207 |
elif kw=="SCOPE":
|
| 208 |
parts=rest.split(); sname=parts[0] if parts else f"s{len(prog.scopes)}"
|
|
|
|
| 230 |
def expand_psl(prog:PSLProgram) -> ExpandedProblem:
|
| 231 |
variables=[]; bounds={}; constraints=[]
|
| 232 |
scope_groups=defaultdict(list); scope_vars=defaultdict(list)
|
|
|
|
| 233 |
def add_var(name,lo,hi,scope="root"):
|
| 234 |
if name not in bounds: variables.append(name); bounds[name]=(lo,hi)
|
| 235 |
if scope!="root" and name not in scope_vars[scope]: scope_vars[scope].append(name)
|
|
|
|
| 236 |
def add_con(kind,expr,direction,scope="root",weight=1.0,branches=None):
|
| 237 |
idx=len(constraints)
|
| 238 |
constraints.append(Constraint(kind,expr,direction,weight,scope,branches or []))
|
|
|
|
| 251 |
if sp.Symbol(v) in parsed.free_symbols and scope!="root" and v not in scope_vars[scope]:
|
| 252 |
scope_vars[scope].append(v)
|
| 253 |
except: pass
|
|
|
|
| 254 |
for v in prog.vars: add_var(v.name,v.lo,v.hi)
|
| 255 |
for c in prog.constraints:
|
| 256 |
kind="or_eq" if c.kind=="or_eq" else "equality" if c.kind=="eq" else "inequality"
|
|
|
|
| 265 |
return ExpandedProblem(variables,bounds,constraints,dict(scope_groups),dict(scope_vars),prog.scope_order,prog.annotations)
|
| 266 |
|
| 267 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 268 |
+
# SECTION 4: AXL LAYER (unchanged from 12.1)
|
| 269 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 270 |
@dataclass
|
| 271 |
class AXLInvariant:
|
|
|
|
| 320 |
AXL_COMPILER=AXLtoPSLCompiler()
|
| 321 |
|
| 322 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 323 |
+
# SECTION 5: PROBLEM & CONSTRAINT COMPILATION (unchanged from 12.1)
|
| 324 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 325 |
@dataclass
|
| 326 |
class Constraint:
|
|
|
|
| 493 |
return total
|
| 494 |
|
| 495 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 496 |
+
# SECTION 6: VERIFY LAYER (unchanged from 12.1)
|
| 497 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 498 |
@dataclass
|
| 499 |
class VerifyResult:
|
|
|
|
| 503 |
failed_gates:List[str]=field(default_factory=list)
|
| 504 |
|
| 505 |
class VerifyLayer:
|
| 506 |
+
def run(self,binding,base_problem,anchors):
|
| 507 |
g1_ce=base_problem.constraint_energy(binding)
|
| 508 |
g1_pass=g1_ce<VERIFY_G1_THRESHOLD
|
| 509 |
g2={}
|
|
|
|
| 518 |
except: g2[inv.name]=(999.0,False)
|
| 519 |
g2_pass=all(v[1] for v in g2.values()) if g2 else True
|
| 520 |
failed=(["Gate1"] if not g1_pass else [])+[k for k,v in g2.items() if not v[1]]
|
| 521 |
+
return VerifyResult(round(g1_ce,6),g1_pass,g2,g2_pass,g1_pass and g2_pass,failed)
|
|
|
|
|
|
|
| 522 |
|
| 523 |
VERIFY_LAYER=VerifyLayer()
|
| 524 |
|
| 525 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 526 |
+
# SECTION 7: EXPANDED AXIOM SPACE β 27 Axioms
|
| 527 |
+
# Sources: Mathematics, Physics, Logic, Philosophy
|
| 528 |
+
# Each axiom is a lens. The sequence of lenses is the ray.
|
| 529 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 530 |
class Axiom:
|
| 531 |
+
# ββ Mathematics ββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 532 |
+
CONTINUOUS = "CONTINUOUS" # smooth, differentiable structure
|
| 533 |
+
DISCRETE = "DISCRETE" # integer/graph/combinatorial structure
|
| 534 |
+
QUADRATIC = "QUADRATIC" # second-degree relationships
|
| 535 |
+
BILINEAR = "BILINEAR" # products of variable pairs
|
| 536 |
+
METRIC = "METRIC" # norm/distance structure
|
| 537 |
+
SYMMETRIC = "SYMMETRIC" # invariance under permutation
|
| 538 |
+
ORDERED = "ORDERED" # total/partial ordering
|
| 539 |
+
MONOTONE = "MONOTONE" # monotone function relationships
|
| 540 |
+
CONVEX = "CONVEX" # convex structure, convex relaxation
|
| 541 |
+
# ββ Physics ββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 542 |
+
CONSERVED = "CONSERVED" # conservation law (zero divergence)
|
| 543 |
+
MUTABLE = "MUTABLE" # state changes, perturbation
|
| 544 |
+
NETWORK = "NETWORK" # graph/flow/connectivity
|
| 545 |
+
EQUILIBRIUM = "EQUILIBRIUM" # force balance, opposing terms cancel
|
| 546 |
+
SUPERPOSITION="SUPERPOSITION"# linear combination of valid states
|
| 547 |
+
LOCALITY = "LOCALITY" # local-to-global propagation
|
| 548 |
+
EXTREMAL = "EXTREMAL" # least action / saddle point
|
| 549 |
+
ENTROPY = "ENTROPY" # maximum spread / disorder
|
| 550 |
+
# ββ Logic ββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 551 |
+
INJECTIVE = "INJECTIVE" # one-to-one (distinct values)
|
| 552 |
+
SURJECTIVE = "SURJECTIVE" # onto (full range coverage)
|
| 553 |
+
TRANSITIVE = "TRANSITIVE" # chain: AβB, BβC implies AβC
|
| 554 |
+
ATOMIC = "ATOMIC" # solve one constraint at a time
|
| 555 |
+
IMPLICATION = "IMPLICATION" # if-then: pin one, propagate others
|
| 556 |
+
NEGATION = "NEGATION" # complement / mirror exploration
|
| 557 |
+
# ββ Philosophy βββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 558 |
+
COMPOSITE = "COMPOSITE" # whole from parts (enzyme stacking)
|
| 559 |
+
HOLISM = "HOLISM" # global view, all constraints at once
|
| 560 |
+
PARSIMONY = "PARSIMONY" # simplest (Occam): integer/rational vals
|
| 561 |
+
DUALITY = "DUALITY" # dual: make inequalities exactly tight
|
| 562 |
|
| 563 |
ALL_AXIOMS = [
|
| 564 |
+
Axiom.CONTINUOUS, Axiom.DISCRETE, Axiom.QUADRATIC, Axiom.BILINEAR,
|
| 565 |
+
Axiom.METRIC, Axiom.SYMMETRIC, Axiom.ORDERED, Axiom.MONOTONE, Axiom.CONVEX,
|
| 566 |
+
Axiom.CONSERVED, Axiom.MUTABLE, Axiom.NETWORK, Axiom.EQUILIBRIUM,
|
| 567 |
+
Axiom.SUPERPOSITION, Axiom.LOCALITY, Axiom.EXTREMAL, Axiom.ENTROPY,
|
| 568 |
+
Axiom.INJECTIVE, Axiom.SURJECTIVE, Axiom.TRANSITIVE, Axiom.ATOMIC,
|
| 569 |
+
Axiom.IMPLICATION, Axiom.NEGATION,
|
| 570 |
+
Axiom.COMPOSITE, Axiom.HOLISM, Axiom.PARSIMONY, Axiom.DUALITY,
|
| 571 |
]
|
| 572 |
|
|
|
|
| 573 |
AXIOM_ABBR = {
|
| 574 |
+
Axiom.CONTINUOUS:"CNT", Axiom.DISCRETE:"DIS", Axiom.QUADRATIC:"QUA",
|
| 575 |
+
Axiom.BILINEAR:"BIL", Axiom.METRIC:"MET", Axiom.SYMMETRIC:"SYM",
|
| 576 |
+
Axiom.ORDERED:"ORD", Axiom.MONOTONE:"MON", Axiom.CONVEX:"CVX",
|
| 577 |
+
Axiom.CONSERVED:"CSV", Axiom.MUTABLE:"MUT", Axiom.NETWORK:"NET",
|
| 578 |
+
Axiom.EQUILIBRIUM:"EQL",Axiom.SUPERPOSITION:"SUP",Axiom.LOCALITY:"LOC",
|
| 579 |
+
Axiom.EXTREMAL:"EXT", Axiom.ENTROPY:"ENT",
|
| 580 |
+
Axiom.INJECTIVE:"INJ", Axiom.SURJECTIVE:"SUR",Axiom.TRANSITIVE:"TRA",
|
| 581 |
+
Axiom.ATOMIC:"ATO", Axiom.IMPLICATION:"IMP",Axiom.NEGATION:"NEG",
|
| 582 |
+
Axiom.COMPOSITE:"CMP", Axiom.HOLISM:"HOL", Axiom.PARSIMONY:"PAR",
|
| 583 |
+
Axiom.DUALITY:"DUA",
|
| 584 |
}
|
| 585 |
|
| 586 |
+
# Contradictions forbidden only when ADJACENT in a sequence.
|
| 587 |
+
# At distance β₯ 2, both can exist β the chain earns its coherence.
|
| 588 |
+
ADJACENT_CONTRADICTIONS: List[Tuple[str,str]] = [
|
| 589 |
+
(Axiom.DISCRETE, Axiom.CONTINUOUS),
|
| 590 |
+
(Axiom.INJECTIVE, Axiom.SURJECTIVE),
|
| 591 |
+
(Axiom.ORDERED, Axiom.SYMMETRIC),
|
| 592 |
+
(Axiom.ATOMIC, Axiom.COMPOSITE),
|
| 593 |
+
(Axiom.CONSERVED, Axiom.MUTABLE),
|
| 594 |
+
(Axiom.PARSIMONY, Axiom.ENTROPY), # simplest vs most-spread
|
| 595 |
+
(Axiom.HOLISM, Axiom.LOCALITY), # global vs local-first
|
| 596 |
+
(Axiom.EXTREMAL, Axiom.ENTROPY), # minimize vs maximize disorder
|
| 597 |
+
(Axiom.NEGATION, Axiom.IMPLICATION), # deny vs affirm-and-propagate
|
| 598 |
]
|
| 599 |
+
_CONTRA_SET = {frozenset(p) for p in ADJACENT_CONTRADICTIONS}
|
| 600 |
|
| 601 |
+
def sequence_valid(seq: List[str]) -> bool:
|
| 602 |
+
"""Only adjacent pairs checked. Distance β₯ 2 contradiction = allowed."""
|
| 603 |
+
for i in range(len(seq)-1):
|
| 604 |
+
if frozenset([seq[i], seq[i+1]]) in _CONTRA_SET:
|
| 605 |
+
return False
|
| 606 |
+
return True
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 607 |
|
| 608 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 609 |
# SECTION 8: SHARED DATACLASSES
|
|
|
|
| 614 |
derivation:List[str]; pinned_vars:Dict[str,float]; free_vars:List[str]
|
| 615 |
confidence:float; ce:float=float('inf')
|
| 616 |
|
| 617 |
+
@dataclass
|
| 618 |
+
class Baton:
|
| 619 |
+
"""
|
| 620 |
+
The partial solution passed between rays like a relay baton.
|
| 621 |
+
A ray does not fail β it terminates and hands this to its children.
|
| 622 |
+
"""
|
| 623 |
+
binding: Dict[str,float]
|
| 624 |
+
ce: float
|
| 625 |
+
ray_id: str = ""
|
| 626 |
+
depth: int = 0
|
| 627 |
+
l7: Optional[Any] = None # TopologyCert β lazily computed
|
| 628 |
+
l9: Optional[Any] = None # ResidualCert β lazily computed
|
| 629 |
+
|
| 630 |
+
@dataclass
|
| 631 |
+
class AxiomRay:
|
| 632 |
+
"""
|
| 633 |
+
A ray is an ordered sequence of axioms, not an unordered set.
|
| 634 |
+
[AβBβC] is structurally different from [CβBβA].
|
| 635 |
+
"""
|
| 636 |
+
sequence: List[str]
|
| 637 |
+
ray_id: str
|
| 638 |
+
depth: int = 0
|
| 639 |
+
parent_id: Optional[str] = None
|
| 640 |
+
baton: Optional[Baton] = None
|
| 641 |
+
|
| 642 |
+
@property
|
| 643 |
+
def name(self) -> str:
|
| 644 |
+
return "β".join(AXIOM_ABBR.get(a,a[:3]) for a in self.sequence)
|
| 645 |
+
|
| 646 |
+
def extend(self, axiom: str) -> Optional['AxiomRay']:
|
| 647 |
+
new_seq = self.sequence + [axiom]
|
| 648 |
+
if sequence_valid(new_seq):
|
| 649 |
+
return AxiomRay(
|
| 650 |
+
sequence = new_seq,
|
| 651 |
+
ray_id = f"{self.ray_id}+{AXIOM_ABBR.get(axiom,'?')}",
|
| 652 |
+
depth = self.depth + 1,
|
| 653 |
+
parent_id = self.ray_id,
|
| 654 |
+
baton = None # caller sets baton
|
| 655 |
+
)
|
| 656 |
+
return None
|
| 657 |
+
|
| 658 |
@dataclass
|
| 659 |
class HypothesisTrace:
|
| 660 |
hid:str; round_idx:int; ray_name:str; action:str
|
| 661 |
ce_before:float; ce_after:float
|
| 662 |
verify:Optional[VerifyResult]; survived:bool; elapsed_ms:float
|
| 663 |
+
depth:int=0; parent_id:str=""
|
| 664 |
|
| 665 |
@dataclass
|
| 666 |
class StructuralModel:
|
| 667 |
best_binding:Dict[str,float]; best_ce:float
|
|
|
|
| 668 |
failure_patterns:Set[str]=field(default_factory=set)
|
| 669 |
scope_witnesses:Dict[str,Dict[str,Tuple]]=field(default_factory=dict)
|
|
|
|
|
|
|
| 670 |
|
| 671 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 672 |
+
# SECTION 9: ORACLES (unchanged from 12.1)
|
| 673 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 674 |
@dataclass
|
| 675 |
class L7Certificate: topology_sig:str; hub_vars:List[str]; solve_order:List[str]
|
| 676 |
@dataclass
|
|
|
|
|
|
|
| 677 |
class L9Certificate: residual_ce:float; dominant_vars:List[str]; dominant_exprs:List[str]
|
| 678 |
|
| 679 |
class TopologyOracle:
|
|
|
|
| 686 |
so=sorted(active_scopes,key=lambda sn:sum(vd.get(v,0) for v in problem.scope_vars.get(sn,[])))
|
| 687 |
return L7Certificate("mesh" if len(hub)>2 else "hub" if hub else "chain",hub,so)
|
| 688 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 689 |
class ResidualOracle:
|
| 690 |
def evaluate(self,binding,problem,hub_vars):
|
| 691 |
ce=problem.constraint_energy(binding)
|
|
|
|
| 717 |
re=[e for e,c in sorted(de,key=lambda x:-x[1])[:5]]
|
| 718 |
return L9Certificate(round(ce,6),rv,re)
|
| 719 |
|
| 720 |
+
TOPOLOGY_ORACLE=TopologyOracle()
|
| 721 |
+
RESIDUAL_ORACLE=ResidualOracle()
|
| 722 |
|
| 723 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 724 |
+
# SECTION 10: CORE SOLVERS (unchanged from 12.1)
|
| 725 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 726 |
def _hc4(box,constraints):
|
| 727 |
cur=dict(box)
|
|
|
|
| 833 |
if nce<best_ce: best_ce=nce; best_b=dict(b)
|
| 834 |
return best_b,best_ce
|
| 835 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 836 |
def _test_hypothesis(problem,hyp):
|
| 837 |
b=dict(hyp.binding)
|
| 838 |
for v,(lo,hi) in problem.bounds.items():
|
|
|
|
| 858 |
return best_b,best_ce
|
| 859 |
|
| 860 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 861 |
+
# SECTION 11: HYPOTHESIS CONSTRUCTORS
|
| 862 |
+
# One constructor per axiom. Each derives its behavior from what that
|
| 863 |
+
# axiom MEANS mathematically/physically, not from a weight scalar.
|
| 864 |
+
# Signature: (problem, baton, all_batons, model) -> List[Hypothesis]
|
| 865 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
|
|
|
|
|
|
|
|
|
|
|
|
| 866 |
|
| 867 |
+
def _proj_val(mc, v, b):
|
| 868 |
+
"""Utility: attempt projection of variable v from constraint mc."""
|
| 869 |
+
if v not in mc.projections: return None
|
| 870 |
+
for proj in mc.projections[v]:
|
| 871 |
+
try:
|
| 872 |
+
val = float(proj["func"](*[b.get(s,0.0) for s in proj["syms"]]))
|
| 873 |
+
if math.isfinite(val) and abs(val) < 1e6: return val
|
| 874 |
+
except: pass
|
| 875 |
+
return None
|
| 876 |
+
|
| 877 |
+
def _make_hyp(hid, binding, h_type, claim, derivation, pinned, free, conf):
|
| 878 |
+
return Hypothesis(hid=hid, binding=binding, h_type=h_type, claim=claim,
|
| 879 |
+
derivation=derivation, pinned_vars=pinned, free_vars=free, confidence=conf)
|
| 880 |
+
|
| 881 |
+
# ββ Mathematics ββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 882 |
+
|
| 883 |
+
def _hyp_continuous(problem, baton, all_batons, model):
|
| 884 |
+
"""Null-space tangent step on the equality manifold."""
|
| 885 |
+
hyps = []; b = baton.binding
|
| 886 |
+
eq_mcs = [mc for mc in problem.compiled_constraints if mc.kind=="equality" and mc.fast_jac]
|
| 887 |
+
if not eq_mcs: return hyps
|
| 888 |
+
nv = len(problem.variables)
|
| 889 |
+
J = np.zeros((len(eq_mcs), nv))
|
| 890 |
+
for i,mc in enumerate(eq_mcs):
|
| 891 |
+
for j,v in enumerate(problem.variables):
|
| 892 |
+
if v not in mc.fast_jac: continue
|
| 893 |
+
jac = mc.fast_jac[v]
|
| 894 |
+
try: J[i,j] = float(jac["func"](*[b.get(s,0.0) for s in jac["syms"]]))
|
| 895 |
+
except: pass
|
| 896 |
+
try:
|
| 897 |
+
_,sv,Vt = np.linalg.svd(J,full_matrices=True); rank = np.sum(sv>1e-8)
|
| 898 |
+
if rank >= Vt.shape[0]: return hyps
|
| 899 |
+
for di,nd in enumerate(Vt[rank:][:2]):
|
| 900 |
+
for step in MANIFOLD_STEPS:
|
| 901 |
+
nb = {v:max(problem.bounds[v][0],min(problem.bounds[v][1],b.get(v,0.0)+step*nd[j]))
|
| 902 |
+
for j,v in enumerate(problem.variables)}
|
| 903 |
+
hyps.append(_make_hyp(f"cnt_d{di}_s{step}",nb,"continuous",
|
| 904 |
+
f"Manifold(dir={di},step={step:.2f})",[f"null_{di}"],{},problem.variables,0.45))
|
| 905 |
+
except: pass
|
| 906 |
+
return hyps
|
| 907 |
+
|
| 908 |
+
def _hyp_discrete(problem, baton, all_batons, model):
|
| 909 |
+
"""Topological chain: propagate HC4 through scope ordering."""
|
| 910 |
+
tb = _global_hc4_tighten(problem); b = dict(baton.binding); steps = []
|
| 911 |
+
l7 = baton.l7
|
| 912 |
+
if not l7 or not l7.solve_order: return []
|
| 913 |
+
for sn in l7.solve_order:
|
| 914 |
+
svars = problem.scope_vars.get(sn,[])
|
| 915 |
+
if not svars: continue
|
| 916 |
+
smcs = [problem.compiled_constraints[i] for i in problem.scope_groups.get(sn,[])]
|
| 917 |
+
if not smcs: continue
|
| 918 |
+
box = {v:IV(*tb.get(v,problem.bounds.get(v,(-10,10)))) for v in svars if v in problem.bounds}
|
| 919 |
+
cont = _hc4(box, smcs)
|
| 920 |
+
if cont:
|
| 921 |
+
for v,iv in cont.items(): b[v]=iv.mid()
|
| 922 |
+
steps.append(sn)
|
| 923 |
+
if not steps: return []
|
| 924 |
+
pinned = {v:b[v] for sn in steps for v in problem.scope_vars.get(sn,[]) if v in b}
|
| 925 |
+
return [_make_hyp(f"dis_{'_'.join(s[:4] for s in steps)}",b,"discrete",
|
| 926 |
+
f"TopoChain({' β '.join(steps)})",steps,pinned,
|
| 927 |
+
[v for v in problem.variables if v not in pinned],0.80)]
|
| 928 |
+
|
| 929 |
+
def _hyp_quadratic(problem, baton, all_batons, model):
|
| 930 |
+
"""Algebraic root projection on quadratic constraints."""
|
| 931 |
+
hyps = []; b = dict(baton.binding); l9 = baton.l9
|
| 932 |
+
if not l9: return hyps
|
| 933 |
+
for expr_str in l9.dominant_exprs[:3]:
|
| 934 |
+
mc = next((mc for mc in problem.compiled_constraints if mc.expr_str==expr_str),None)
|
| 935 |
+
if not mc or not mc.projections: continue
|
| 936 |
+
for v,projs in mc.projections.items():
|
| 937 |
+
lo,hi = problem.bounds.get(v,(-1e18,1e18))
|
| 938 |
+
for pi,proj in enumerate(projs):
|
| 939 |
+
try:
|
| 940 |
+
val = float(proj["func"](*[b.get(s,0.0) for s in proj["syms"]]))
|
| 941 |
+
if not(lo<=val<=hi) or not math.isfinite(val): continue
|
| 942 |
+
nb = dict(b); nb[v]=val
|
| 943 |
+
hyps.append(_make_hyp(f"qua_{hash(expr_str)%9999}_{v}_{pi}",nb,"quadratic",
|
| 944 |
+
f"QuadRoot({v}={val:.4f})",[expr_str],{v:val},
|
| 945 |
+
[u for u in problem.variables if u!=v],0.80 if pi==0 else 0.65))
|
| 946 |
+
except: pass
|
| 947 |
+
return hyps
|
| 948 |
+
|
| 949 |
+
def _hyp_bilinear(problem, baton, all_batons, model):
|
| 950 |
+
"""Geometric mean split for bilinear product constraints."""
|
| 951 |
+
hyps = []; b = dict(baton.binding)
|
| 952 |
+
for mc in problem.compiled_constraints:
|
| 953 |
+
if not mc.parsed: continue
|
| 954 |
+
expr = mc.parsed
|
| 955 |
+
if not expr.is_Add: continue
|
| 956 |
+
for term in expr.args:
|
| 957 |
+
if not term.is_Mul: continue
|
| 958 |
+
syms_in = [str(s) for s in term.free_symbols if str(s) in problem.variables]
|
| 959 |
+
if len(syms_in) != 2: continue
|
| 960 |
+
vi,vj = syms_in
|
| 961 |
+
lo_i,hi_i = problem.bounds.get(vi,(0,10))
|
| 962 |
+
lo_j,hi_j = problem.bounds.get(vj,(0,10))
|
| 963 |
+
product = abs(b.get(vi,1)*b.get(vj,1))
|
| 964 |
+
gm = math.sqrt(product) if product >= 0 else 0
|
| 965 |
+
if lo_i<=gm<=hi_i and lo_j<=gm<=hi_j:
|
| 966 |
+
nb = dict(b); nb[vi]=gm; nb[vj]=gm
|
| 967 |
+
hyps.append(_make_hyp(f"bil_{vi}_{vj}",nb,"bilinear",
|
| 968 |
+
f"GeoMean({vi}={vj}={gm:.4f})",["bilinear"],{vi:gm,vj:gm},
|
| 969 |
+
[v for v in problem.variables if v not in [vi,vj]],0.70))
|
| 970 |
+
return hyps
|
| 971 |
+
|
| 972 |
+
def _hyp_metric(problem, baton, all_batons, model):
|
| 973 |
+
"""Radial projection onto norm sphere constraints."""
|
| 974 |
+
hyps = []; b = dict(baton.binding)
|
| 975 |
+
for mc in problem.compiled_constraints:
|
| 976 |
+
if mc.kind!="equality" or not mc.parsed: continue
|
| 977 |
+
expr = mc.parsed
|
| 978 |
+
if not expr.is_Add: continue
|
| 979 |
+
sq_terms = [t for t in expr.args if t.is_Pow and t.args[1]==2]
|
| 980 |
+
if len(sq_terms) < 2: continue
|
| 981 |
+
vars_in = [str(s) for s in expr.free_symbols if str(s) in problem.variables]
|
| 982 |
+
curr_val = sum(b.get(v,0)**2 for v in vars_in)
|
| 983 |
+
if curr_val < 1e-8: continue
|
| 984 |
+
const_terms = [t for t in expr.args if t.is_Number]
|
| 985 |
+
if not const_terms: continue
|
| 986 |
+
target = -float(const_terms[0])
|
| 987 |
+
if target <= 0: continue
|
| 988 |
+
scale = math.sqrt(target/curr_val)
|
| 989 |
+
nb = dict(b)
|
| 990 |
+
for v in vars_in:
|
| 991 |
+
lo,hi = problem.bounds.get(v,(-10,10))
|
| 992 |
+
nb[v] = max(lo,min(hi,b.get(v,0)*scale))
|
| 993 |
+
hyps.append(_make_hyp(f"met_{hash(mc.expr_str)%9999}",nb,"metric",
|
| 994 |
+
f"RadialProject(scale={scale:.4f})",["metric",mc.expr_str],{},list(problem.variables),0.75))
|
| 995 |
+
return hyps
|
| 996 |
+
|
| 997 |
+
def _hyp_symmetric(problem, baton, all_batons, model):
|
| 998 |
+
"""Pairwise variable swaps β symmetry group exploration."""
|
| 999 |
+
hyps = []; b = dict(baton.binding); vl = problem.variables
|
| 1000 |
+
for i in range(min(len(vl),5)):
|
| 1001 |
+
for j in range(i+1,min(len(vl),5)):
|
| 1002 |
+
vi,vj = vl[i],vl[j]
|
| 1003 |
+
lo_i,hi_i = problem.bounds[vi]; lo_j,hi_j = problem.bounds[vj]
|
| 1004 |
+
if lo_i<=b.get(vj,0)<=hi_i and lo_j<=b.get(vi,0)<=hi_j:
|
| 1005 |
+
nb = dict(b); nb[vi],nb[vj] = b.get(vj,0),b.get(vi,0)
|
| 1006 |
+
hyps.append(_make_hyp(f"sym_{vi}_{vj}",nb,"symmetric",f"Swap({vi}β{vj})",
|
| 1007 |
+
["symmetric"],{vi:nb[vi],vj:nb[vj]},
|
| 1008 |
+
[v for v in vl if v not in [vi,vj]],0.60))
|
| 1009 |
+
return hyps
|
| 1010 |
+
|
| 1011 |
+
def _hyp_ordered(problem, baton, all_batons, model):
|
| 1012 |
+
"""Enforce variable ordering by midpoint balancing."""
|
| 1013 |
+
b = dict(baton.binding); nb = dict(b)
|
| 1014 |
+
ord_mcs = [mc for mc in problem.compiled_constraints
|
| 1015 |
+
if mc.kind=="inequality" and len(mc.syms_used)==2]
|
| 1016 |
+
for mc in ord_mcs:
|
| 1017 |
+
vi,vj = mc.syms_used
|
| 1018 |
+
lo_i,hi_i = problem.bounds.get(vi,(-1e18,1e18))
|
| 1019 |
+
lo_j,hi_j = problem.bounds.get(vj,(-1e18,1e18))
|
| 1020 |
+
if mc.direction=="geq" and nb.get(vi,0)<nb.get(vj,0):
|
| 1021 |
+
mid = (nb[vi]+nb[vj])/2
|
| 1022 |
+
nb[vi]=max(lo_i,mid); nb[vj]=min(hi_j,mid)
|
| 1023 |
+
return [_make_hyp(f"ord_{hash(str(nb))%9999}",nb,"ordered","OrderBalance",
|
| 1024 |
+
["ordered"],{},list(problem.variables),0.67)]
|
| 1025 |
+
|
| 1026 |
+
def _hyp_monotone(problem, baton, all_batons, model):
|
| 1027 |
+
"""Step variables in order of gradient magnitude β monotone path."""
|
| 1028 |
+
b = dict(baton.binding); grad = problem.evaluate_gradient(b)
|
| 1029 |
+
ordered = sorted(problem.variables,key=lambda v:-abs(grad.get(v,0)))
|
| 1030 |
+
nb = dict(b)
|
| 1031 |
+
for v in ordered:
|
| 1032 |
+
lo,hi = problem.bounds[v]; g = grad.get(v,0)
|
| 1033 |
+
if abs(g)>1e-10: nb[v]=max(lo,min(hi,nb[v]-0.05*g))
|
| 1034 |
+
return [_make_hyp(f"mon_{hash(str(nb))%9999}",nb,"monotone","MonotonePath",
|
| 1035 |
+
["monotone"],{},list(problem.variables),0.67)]
|
| 1036 |
+
|
| 1037 |
+
def _hyp_convex(problem, baton, all_batons, model):
|
| 1038 |
+
"""Convex combination of current binding and constraint projection."""
|
| 1039 |
+
hyps = []; b = dict(baton.binding)
|
| 1040 |
+
for mc in problem.compiled_constraints:
|
| 1041 |
+
if mc.kind!="equality" or not mc.projections: continue
|
| 1042 |
+
for v,projs in mc.projections.items():
|
| 1043 |
+
lo,hi = problem.bounds.get(v,(-1e18,1e18))
|
| 1044 |
+
for proj in projs:
|
| 1045 |
+
try:
|
| 1046 |
+
val = float(proj["func"](*[b.get(s,0.0) for s in proj["syms"]]))
|
| 1047 |
+
if not(lo<=val<=hi) or not math.isfinite(val): continue
|
| 1048 |
+
nb = dict(b); nb[v] = 0.5*b[v]+0.5*val
|
| 1049 |
+
hyps.append(_make_hyp(f"cvx_{hash(mc.expr_str)%9999}_{v}",nb,"convex",
|
| 1050 |
+
f"ConvexMix({v}β{val:.3f})",["convex",mc.expr_str],{v:nb[v]},
|
| 1051 |
+
[u for u in problem.variables if u!=v],0.63))
|
| 1052 |
+
except: pass
|
| 1053 |
+
return hyps
|
| 1054 |
+
|
| 1055 |
+
# ββ Physics ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1056 |
+
|
| 1057 |
+
def _hyp_conserved(problem, baton, all_batons, model):
|
| 1058 |
+
"""Enforce conservation laws directly via projection."""
|
| 1059 |
+
hyps = []; b = dict(baton.binding)
|
| 1060 |
+
cons_mcs = [mc for mc in problem.compiled_constraints if mc.kind=="equality" and mc.weight>=5.0]
|
| 1061 |
+
for mc in cons_mcs:
|
| 1062 |
+
for v,projs in mc.projections.items():
|
| 1063 |
+
lo,hi = problem.bounds.get(v,(-1e18,1e18))
|
| 1064 |
+
for proj in projs:
|
| 1065 |
+
try:
|
| 1066 |
+
val = float(proj["func"](*[b.get(s,0.0) for s in proj["syms"]]))
|
| 1067 |
+
if not(lo<=val<=hi) or not math.isfinite(val): continue
|
| 1068 |
+
nb = dict(b); nb[v]=val
|
| 1069 |
+
hyps.append(_make_hyp(f"csv_{hash(mc.expr_str)%9999}_{v}",nb,"conserved",
|
| 1070 |
+
f"Conserve({v}={val:.4f})",[mc.expr_str],{v:val},
|
| 1071 |
+
[u for u in problem.variables if u!=v],0.82))
|
| 1072 |
+
except: pass
|
| 1073 |
+
return hyps
|
| 1074 |
+
|
| 1075 |
+
def _hyp_mutable(problem, baton, all_batons, model):
|
| 1076 |
+
"""Gaussian perturbation of dominant residual variables."""
|
| 1077 |
+
hyps = []; l9 = baton.l9; b = dict(baton.binding)
|
| 1078 |
+
if not l9 or not l9.dominant_vars: return hyps
|
| 1079 |
+
for v in l9.dominant_vars[:3]:
|
| 1080 |
+
lo,hi = problem.bounds.get(v,(-10,10))
|
| 1081 |
+
for _ in range(3):
|
| 1082 |
+
noise = random.gauss(0,(hi-lo)*0.05)
|
| 1083 |
+
val = max(lo,min(hi,b[v]+noise))
|
| 1084 |
+
nb = dict(b); nb[v]=val
|
| 1085 |
+
hyps.append(_make_hyp(f"mut_{v}_{random.randint(0,9999)}",nb,"mutable",
|
| 1086 |
+
f"Perturb({v}Β±{noise:.4f})",["mutable",v],{},list(problem.variables),0.40))
|
| 1087 |
+
return hyps
|
| 1088 |
+
|
| 1089 |
+
def _hyp_network(problem, baton, all_batons, model):
|
| 1090 |
+
"""Hub-and-spoke: propagate from most-connected variable."""
|
| 1091 |
+
vd = defaultdict(int)
|
| 1092 |
+
for mc in problem.compiled_constraints:
|
| 1093 |
+
for v in mc.syms_used: vd[v]+=1
|
| 1094 |
+
if not vd: return []
|
| 1095 |
+
hub = max(vd,key=vd.get); b = dict(baton.binding)
|
| 1096 |
+
for mc in problem.compiled_constraints:
|
| 1097 |
+
if hub not in mc.syms_used or hub not in mc.projections: continue
|
| 1098 |
+
val = _proj_val(mc,hub,b)
|
| 1099 |
+
if val is None: continue
|
| 1100 |
+
lo,hi = problem.bounds.get(hub,(-1e18,1e18))
|
| 1101 |
+
if lo<=val<=hi: b[hub]=val; break
|
| 1102 |
+
return [_make_hyp(f"net_{hub}_{hash(str(b))%9999}",b,"network",
|
| 1103 |
+
f"HubProp({hub},deg={vd[hub]})",["network",hub],{hub:b[hub]},
|
| 1104 |
+
[v for v in problem.variables if v!=hub],0.65)]
|
| 1105 |
+
|
| 1106 |
+
def _hyp_equilibrium(problem, baton, all_batons, model):
|
| 1107 |
+
"""Find gradient balance point β opposing forces cancel."""
|
| 1108 |
+
b = dict(baton.binding); grad = problem.evaluate_gradient(b)
|
| 1109 |
+
gms = sum(g**2 for g in grad.values())
|
| 1110 |
+
if gms < 1e-12: return []
|
| 1111 |
+
lr = min(0.15, baton.ce/(gms+1e-8))
|
| 1112 |
+
nb = {v:max(problem.bounds[v][0],min(problem.bounds[v][1],b[v]-lr*grad[v]))
|
| 1113 |
+
for v in problem.variables}
|
| 1114 |
+
return [_make_hyp(f"eql_{hash(str(nb))%9999}",nb,"equilibrium",
|
| 1115 |
+
f"GradBalance(lr={lr:.4f})",["equilibrium"],{},list(problem.variables),0.72)]
|
| 1116 |
+
|
| 1117 |
+
def _hyp_superposition(problem, baton, all_batons, model):
|
| 1118 |
+
"""Linear combinations of inherited batons from parent rays."""
|
| 1119 |
+
hyps = []; recent = [bt for bt in all_batons[-8:] if bt.ce < float('inf') and bt.binding]
|
| 1120 |
+
if not recent: return hyps
|
| 1121 |
+
for lam in [0.25, 0.5, 0.75]:
|
| 1122 |
+
other = random.choice(recent)
|
| 1123 |
+
nb = {}
|
| 1124 |
+
for v in problem.variables:
|
| 1125 |
+
lo,hi = problem.bounds[v]
|
| 1126 |
+
val = lam*baton.binding.get(v,0)+(1-lam)*other.binding.get(v,0)
|
| 1127 |
+
nb[v] = max(lo,min(hi,val))
|
| 1128 |
+
hyps.append(_make_hyp(f"sup_{int(lam*10)}_{random.randint(0,999)}",nb,"superposition",
|
| 1129 |
+
f"Superpose(Ξ»={lam:.2f},ray={other.ray_id})",["superposition",other.ray_id],
|
| 1130 |
+
{},list(problem.variables),0.58))
|
| 1131 |
+
return hyps
|
| 1132 |
+
|
| 1133 |
+
def _hyp_locality(problem, baton, all_batons, model):
|
| 1134 |
+
"""Solve densest-constraint variable first, propagate outward."""
|
| 1135 |
+
vd = defaultdict(float)
|
| 1136 |
+
for mc in problem.compiled_constraints:
|
| 1137 |
+
for v in mc.syms_used: vd[v]+=mc.weight
|
| 1138 |
+
ordered = sorted(problem.variables,key=lambda v:-vd[v])
|
| 1139 |
+
b = dict(baton.binding)
|
| 1140 |
+
for v in ordered[:4]:
|
| 1141 |
+
for mc in problem.compiled_constraints:
|
| 1142 |
+
if v not in mc.syms_used or v not in mc.projections: continue
|
| 1143 |
+
val = _proj_val(mc,v,b)
|
| 1144 |
+
if val is None: continue
|
| 1145 |
+
lo,hi = problem.bounds.get(v,(-1e18,1e18))
|
| 1146 |
+
if lo<=val<=hi: b[v]=val; break
|
| 1147 |
+
return [_make_hyp(f"loc_{hash(str(b))%9999}",b,"locality",
|
| 1148 |
+
f"LocalFirst({ordered[0] if ordered else '?'})",["locality"],
|
| 1149 |
+
{v:b[v] for v in ordered[:4] if v in b},ordered[4:],0.72)]
|
| 1150 |
+
|
| 1151 |
+
def _hyp_extremal(problem, baton, all_batons, model):
|
| 1152 |
+
"""Extremal principle: test boundary values of dominant variables."""
|
| 1153 |
+
hyps = []; l9 = baton.l9; b = dict(baton.binding)
|
| 1154 |
+
if not l9 or not l9.dominant_vars: return hyps
|
| 1155 |
+
for v in l9.dominant_vars[:3]:
|
| 1156 |
+
lo,hi = problem.bounds.get(v,(0,1))
|
| 1157 |
+
for val in [lo,hi,(lo+hi)/2]:
|
| 1158 |
+
nb = dict(b); nb[v]=val
|
| 1159 |
+
hyps.append(_make_hyp(f"ext_{v}_{val:.4f}",nb,"extremal",
|
| 1160 |
+
f"Extremal({v}={val:.4f})",["extremal"],{v:val},
|
| 1161 |
+
[u for u in problem.variables if u!=v],0.65))
|
| 1162 |
+
return hyps
|
| 1163 |
+
|
| 1164 |
+
def _hyp_entropy(problem, baton, all_batons, model):
|
| 1165 |
+
"""Maximum disorder: spread variables across their bounds."""
|
| 1166 |
+
nb_mid = {v:(lo+hi)/2 for v,(lo,hi) in problem.bounds.items()}
|
| 1167 |
+
nb_rand = {v:random.uniform(lo,hi) for v,(lo,hi) in problem.bounds.items()}
|
| 1168 |
+
return [
|
| 1169 |
+
_make_hyp("ent_mid",nb_mid,"entropy","MaxEntropy(mid)",["entropy"],{},list(problem.variables),0.48),
|
| 1170 |
+
_make_hyp(f"ent_rnd_{random.randint(0,999)}",nb_rand,"entropy","MaxEntropy(random)",["entropy"],{},list(problem.variables),0.42),
|
| 1171 |
+
]
|
| 1172 |
+
|
| 1173 |
+
# ββ Logic ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1174 |
+
|
| 1175 |
+
def _hyp_injective(problem, baton, all_batons, model):
|
| 1176 |
+
"""Ensure distinct values β nudge duplicates apart."""
|
| 1177 |
+
b = dict(baton.binding); nb = dict(b); seen = {}
|
| 1178 |
+
for v in problem.variables:
|
| 1179 |
+
val = nb[v]
|
| 1180 |
+
rval = round(val,4)
|
| 1181 |
+
if rval in seen:
|
| 1182 |
+
lo,hi = problem.bounds[v]
|
| 1183 |
+
nb[v] = max(lo,min(hi,val+(hi-lo)*0.01*(len(seen)+1)))
|
| 1184 |
+
seen[rval]=v
|
| 1185 |
+
return [_make_hyp(f"inj_{hash(str(nb))%9999}",nb,"injective","EnsureDistinct",
|
| 1186 |
+
["injective"],{},list(problem.variables),0.50)]
|
| 1187 |
+
|
| 1188 |
+
def _hyp_surjective(problem, baton, all_batons, model):
|
| 1189 |
+
"""Range sweep: test fractional positions along each variable's span."""
|
| 1190 |
+
hyps = []
|
| 1191 |
+
for v in problem.variables[:5]:
|
| 1192 |
+
lo,hi = problem.bounds[v]
|
| 1193 |
+
for frac in [0.1,0.9]:
|
| 1194 |
+
nb = dict(baton.binding); nb[v]=lo+frac*(hi-lo)
|
| 1195 |
+
hyps.append(_make_hyp(f"sur_{v}_{int(frac*100)}",nb,"surjective",
|
| 1196 |
+
f"RangeSweep({v}@{frac:.0%})",["surjective"],{v:nb[v]},
|
| 1197 |
+
[u for u in problem.variables if u!=v],0.45))
|
| 1198 |
+
return hyps
|
| 1199 |
+
|
| 1200 |
+
def _hyp_transitive(problem, baton, all_batons, model):
|
| 1201 |
+
"""Transitively snap projections until convergence."""
|
| 1202 |
+
b = dict(baton.binding); nb = dict(b); changed=True; iters=0
|
| 1203 |
+
while changed and iters<6:
|
| 1204 |
+
changed=False; iters+=1
|
| 1205 |
+
for mc in problem.compiled_constraints:
|
| 1206 |
+
if mc.kind!="equality" or not mc.projections: continue
|
| 1207 |
+
for v,projs in mc.projections.items():
|
| 1208 |
+
val = _proj_val(mc,v,nb)
|
| 1209 |
+
if val is None: continue
|
| 1210 |
+
lo,hi = problem.bounds.get(v,(-1e18,1e18))
|
| 1211 |
+
if lo<=val<=hi and abs(val-nb.get(v,0))>1e-6:
|
| 1212 |
+
nb[v]=val; changed=True
|
| 1213 |
+
if nb==b: return []
|
| 1214 |
+
pinned = {v:nb[v] for v in nb if abs(nb[v]-b.get(v,0))>1e-4}
|
| 1215 |
+
return [_make_hyp(f"tra_{hash(str(nb))%9999}",nb,"transitive",
|
| 1216 |
+
f"TransitiveSnap({iters}iters)",["transitive"],pinned,
|
| 1217 |
+
[v for v in problem.variables if v not in pinned],0.77)]
|
| 1218 |
+
|
| 1219 |
+
def _hyp_atomic(problem, baton, all_batons, model):
|
| 1220 |
+
"""Solve a single most-violated constraint; ignore the rest."""
|
| 1221 |
+
b = dict(baton.binding); worst_mc=None; worst_val=0.0
|
| 1222 |
+
for mc in problem.compiled_constraints:
|
| 1223 |
+
if mc.fast_pt is None: continue
|
| 1224 |
+
try:
|
| 1225 |
+
val = abs(float(mc.fast_pt(*[b.get(v,0.0) for v in mc.syms_used])))
|
| 1226 |
+
if val>worst_val: worst_val=val; worst_mc=mc
|
| 1227 |
+
except: pass
|
| 1228 |
+
if not worst_mc or not worst_mc.projections: return []
|
| 1229 |
+
hyps = []
|
| 1230 |
+
for v,projs in worst_mc.projections.items():
|
| 1231 |
+
lo,hi = problem.bounds.get(v,(-1e18,1e18))
|
| 1232 |
+
for proj in projs:
|
| 1233 |
+
try:
|
| 1234 |
+
val = float(proj["func"](*[b.get(s,0.0) for s in proj["syms"]]))
|
| 1235 |
+
if not(lo<=val<=hi) or not math.isfinite(val): continue
|
| 1236 |
+
nb = dict(b); nb[v]=val
|
| 1237 |
+
hyps.append(_make_hyp(f"ato_{hash(worst_mc.expr_str)%9999}_{v}",nb,"atomic",
|
| 1238 |
+
f"SolveOne({worst_mc.expr_str[:20]}β{v}={val:.4f})",[worst_mc.expr_str],
|
| 1239 |
+
{v:val},[u for u in problem.variables if u!=v],0.70))
|
| 1240 |
+
except: pass
|
| 1241 |
+
return hyps
|
| 1242 |
+
|
| 1243 |
+
def _hyp_implication(problem, baton, all_batons, model):
|
| 1244 |
+
"""Pin a dominant variable, propagate implications through HC4."""
|
| 1245 |
+
hyps = []; l9 = baton.l9; b = dict(baton.binding)
|
| 1246 |
+
if not l9 or not l9.dominant_vars: return hyps
|
| 1247 |
+
tb = _global_hc4_tighten(problem)
|
| 1248 |
+
for v in l9.dominant_vars[:2]:
|
| 1249 |
+
val = b.get(v,(problem.bounds[v][0]+problem.bounds[v][1])/2)
|
| 1250 |
+
box = {u:IV(*tb.get(u,problem.bounds.get(u,(-10,10)))) for u in problem.variables}
|
| 1251 |
+
box[v] = IV(val-1e-4,val+1e-4)
|
| 1252 |
+
contracted = _hc4(box,problem.compiled_constraints)
|
| 1253 |
+
if not contracted: continue
|
| 1254 |
+
nb = {u:contracted[u].mid() for u in problem.variables}
|
| 1255 |
+
pinned = {u:nb[u] for u in problem.variables if contracted[u].width()<1e-2}
|
| 1256 |
+
hyps.append(_make_hyp(f"imp_{v}_{hash(str(nb))%9999}",nb,"implication",
|
| 1257 |
+
f"Imply({v}={val:.3f}βHC4)",["implication",v],pinned,
|
| 1258 |
+
[u for u in problem.variables if u not in pinned],0.78))
|
| 1259 |
+
return hyps
|
| 1260 |
+
|
| 1261 |
+
def _hyp_negation(problem, baton, all_batons, model):
|
| 1262 |
+
"""Mirror current binding through the centre of variable bounds."""
|
| 1263 |
+
nb = {}
|
| 1264 |
+
for v in problem.variables:
|
| 1265 |
+
lo,hi = problem.bounds[v]; mid=(lo+hi)/2
|
| 1266 |
+
nb[v] = max(lo,min(hi,2*mid-baton.binding.get(v,mid)))
|
| 1267 |
+
return [_make_hyp(f"neg_{hash(str(nb))%9999}",nb,"negation","MirrorBounds",
|
| 1268 |
+
["negation"],{},list(problem.variables),0.42)]
|
| 1269 |
+
|
| 1270 |
+
# ββ Philosophy βββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1271 |
+
|
| 1272 |
+
def _hyp_composite(problem, baton, all_batons, model):
|
| 1273 |
+
"""Enzyme: pin branch value, cascade HC4 (Practicality 12.1 enzyme)."""
|
| 1274 |
+
hyps = []; l9 = baton.l9
|
| 1275 |
+
if not l9: return hyps
|
| 1276 |
+
ref = baton.binding; tb = _global_hc4_tighten(problem)
|
| 1277 |
+
for expr_str in l9.dominant_exprs[:3]:
|
| 1278 |
+
mc = next((mc for mc in problem.compiled_constraints if mc.expr_str==expr_str),None)
|
| 1279 |
+
if not mc or not mc.projections: continue
|
| 1280 |
+
for v,proj_list in mc.projections.items():
|
| 1281 |
+
lo,hi = problem.bounds.get(v,(-1e18,1e18))
|
| 1282 |
+
for pi,proj in enumerate(proj_list):
|
| 1283 |
+
try:
|
| 1284 |
+
val = float(proj["func"](*[ref.get(s,0.0) for s in proj["syms"]]))
|
| 1285 |
+
if not math.isfinite(val) or abs(val)>1e6 or not(lo<=val<=hi): continue
|
| 1286 |
+
box = {u:IV(*tb.get(u,problem.bounds.get(u,(-10,10)))) for u in problem.variables}
|
| 1287 |
+
box[v] = IV(val-1e-6,val+1e-6)
|
| 1288 |
+
cont = _hc4(box,problem.compiled_constraints)
|
| 1289 |
+
if not cont: continue
|
| 1290 |
+
b = dict(ref)
|
| 1291 |
+
for u,iv in cont.items(): b[u]=iv.mid()
|
| 1292 |
+
pinned = {u:b[u] for u in problem.variables if cont[u].width()<1e-2}
|
| 1293 |
+
hyps.append(_make_hyp(f"cmp_{hash(expr_str)%9999}_{v}_{pi}",b,"composite",
|
| 1294 |
+
f"Enz(Br({v})βChain)",[expr_str,"hc4_chain"],pinned,
|
| 1295 |
+
[u for u in problem.variables if u not in pinned],0.90 if pi==0 else 0.80))
|
| 1296 |
+
except: pass
|
| 1297 |
+
return hyps
|
| 1298 |
+
|
| 1299 |
+
def _hyp_holism(problem, baton, all_batons, model):
|
| 1300 |
+
"""Single global gradient step treating all constraints simultaneously."""
|
| 1301 |
+
b = dict(baton.binding); grad = problem.evaluate_gradient(b)
|
| 1302 |
+
gms = sum(g**2 for g in grad.values())
|
| 1303 |
+
if gms < 1e-12: return []
|
| 1304 |
+
lr = min(0.5,baton.ce/(gms+1e-8))
|
| 1305 |
+
nb = {v:max(problem.bounds[v][0],min(problem.bounds[v][1],b[v]-lr*grad[v]))
|
| 1306 |
+
for v in problem.variables}
|
| 1307 |
+
return [_make_hyp(f"hol_{hash(str(nb))%9999}",nb,"holism",
|
| 1308 |
+
f"GlobalStep(lr={lr:.4f})",["holism"],{},list(problem.variables),0.73)]
|
| 1309 |
+
|
| 1310 |
+
def _hyp_parsimony(problem, baton, all_batons, model):
|
| 1311 |
+
"""Occam: simplest (integer / half-integer) values."""
|
| 1312 |
+
b = dict(baton.binding); nb = {}
|
| 1313 |
+
for v in problem.variables:
|
| 1314 |
+
lo,hi = problem.bounds[v]; candidates = []
|
| 1315 |
+
for mult in [1,2,4]:
|
| 1316 |
+
r = round(b[v]*mult)/mult
|
| 1317 |
+
if lo<=r<=hi: candidates.append(r)
|
| 1318 |
+
nb[v] = min(candidates,key=lambda c:abs(c-b[v])) if candidates else b[v]
|
| 1319 |
+
return [_make_hyp(f"par_{hash(str(nb))%9999}",nb,"parsimony","Occam(round)",
|
| 1320 |
+
["parsimony"],{},list(problem.variables),0.58)]
|
| 1321 |
+
|
| 1322 |
+
def _hyp_duality(problem, baton, all_batons, model):
|
| 1323 |
+
"""Dual: make each inequality constraint exactly tight."""
|
| 1324 |
+
hyps = []; b = dict(baton.binding)
|
| 1325 |
+
for mc in problem.compiled_constraints:
|
| 1326 |
+
if mc.kind!="inequality" or not mc.projections: continue
|
| 1327 |
+
for v,projs in mc.projections.items():
|
| 1328 |
+
lo,hi = problem.bounds.get(v,(-1e18,1e18))
|
| 1329 |
+
for proj in projs:
|
| 1330 |
+
try:
|
| 1331 |
+
val = float(proj["func"](*[b.get(s,0.0) for s in proj["syms"]]))
|
| 1332 |
+
if not(lo<=val<=hi) or not math.isfinite(val): continue
|
| 1333 |
+
nb = dict(b); nb[v]=val
|
| 1334 |
+
hyps.append(_make_hyp(f"dua_{hash(mc.expr_str)%9999}_{v}",nb,"duality",
|
| 1335 |
+
f"DualTight({v}β{mc.expr_str[:18]})",["duality",mc.expr_str],{v:val},
|
| 1336 |
+
[u for u in problem.variables if u!=v],0.68))
|
| 1337 |
+
break
|
| 1338 |
+
except: pass
|
| 1339 |
+
return hyps
|
| 1340 |
+
|
| 1341 |
+
# Registry: axiom string β constructor function
|
| 1342 |
+
AXIOM_CONSTRUCTORS: Dict[str, Callable] = {
|
| 1343 |
+
Axiom.CONTINUOUS: _hyp_continuous,
|
| 1344 |
+
Axiom.DISCRETE: _hyp_discrete,
|
| 1345 |
+
Axiom.QUADRATIC: _hyp_quadratic,
|
| 1346 |
+
Axiom.BILINEAR: _hyp_bilinear,
|
| 1347 |
+
Axiom.METRIC: _hyp_metric,
|
| 1348 |
+
Axiom.SYMMETRIC: _hyp_symmetric,
|
| 1349 |
+
Axiom.ORDERED: _hyp_ordered,
|
| 1350 |
+
Axiom.MONOTONE: _hyp_monotone,
|
| 1351 |
+
Axiom.CONVEX: _hyp_convex,
|
| 1352 |
+
Axiom.CONSERVED: _hyp_conserved,
|
| 1353 |
+
Axiom.MUTABLE: _hyp_mutable,
|
| 1354 |
+
Axiom.NETWORK: _hyp_network,
|
| 1355 |
+
Axiom.EQUILIBRIUM: _hyp_equilibrium,
|
| 1356 |
+
Axiom.SUPERPOSITION: _hyp_superposition,
|
| 1357 |
+
Axiom.LOCALITY: _hyp_locality,
|
| 1358 |
+
Axiom.EXTREMAL: _hyp_extremal,
|
| 1359 |
+
Axiom.ENTROPY: _hyp_entropy,
|
| 1360 |
+
Axiom.INJECTIVE: _hyp_injective,
|
| 1361 |
+
Axiom.SURJECTIVE: _hyp_surjective,
|
| 1362 |
+
Axiom.TRANSITIVE: _hyp_transitive,
|
| 1363 |
+
Axiom.ATOMIC: _hyp_atomic,
|
| 1364 |
+
Axiom.IMPLICATION: _hyp_implication,
|
| 1365 |
+
Axiom.NEGATION: _hyp_negation,
|
| 1366 |
+
Axiom.COMPOSITE: _hyp_composite,
|
| 1367 |
+
Axiom.HOLISM: _hyp_holism,
|
| 1368 |
+
Axiom.PARSIMONY: _hyp_parsimony,
|
| 1369 |
+
Axiom.DUALITY: _hyp_duality,
|
| 1370 |
+
}
|
| 1371 |
+
|
| 1372 |
+
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1373 |
+
# SECTION 12: SEQUENCE HYPOTHESIS GENERATOR
|
| 1374 |
+
# Processes the axiom sequence of a ray in order.
|
| 1375 |
+
# Each axiom adds hypotheses; the best result updates the baton for
|
| 1376 |
+
# the next axiom in the sequence. The chain earns its own direction.
|
| 1377 |
+
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1378 |
+
class SequenceHypothesisGenerator:
|
| 1379 |
+
def generate(self, sequence: List[str], problem: Problem,
|
| 1380 |
+
baton: Baton, all_batons: List[Baton],
|
| 1381 |
+
model: StructuralModel) -> Tuple[List[Hypothesis], Baton]:
|
| 1382 |
+
accumulated: List[Hypothesis] = []
|
| 1383 |
+
current = baton
|
| 1384 |
+
|
| 1385 |
+
for i, axiom in enumerate(sequence):
|
| 1386 |
+
constructor = AXIOM_CONSTRUCTORS.get(axiom)
|
| 1387 |
+
if not constructor:
|
| 1388 |
+
continue
|
| 1389 |
+
|
| 1390 |
+
# Lazily enrich baton with oracle context
|
| 1391 |
+
if current.l7 is None:
|
| 1392 |
+
active = [s for s in problem.scope_order if s!="root" and problem.scope_vars.get(s)]
|
| 1393 |
+
current.l7 = TOPOLOGY_ORACLE.evaluate(problem, active)
|
| 1394 |
+
if current.l9 is None:
|
| 1395 |
+
hubs = current.l7.hub_vars if current.l7 else []
|
| 1396 |
+
current.l9 = RESIDUAL_ORACLE.evaluate(current.binding, problem, hubs)
|
| 1397 |
+
|
| 1398 |
+
new_hyps = constructor(problem, current, all_batons, model)
|
| 1399 |
+
accumulated.extend(new_hyps)
|
| 1400 |
+
|
| 1401 |
+
# Test top hypotheses; best result becomes context for next axiom
|
| 1402 |
+
best_ce = current.ce
|
| 1403 |
+
best_b = current.binding
|
| 1404 |
+
for hyp in sorted(new_hyps, key=lambda h: -h.confidence)[:MAX_HYPS_PER_AXIOM]:
|
| 1405 |
+
if hyp.hid in model.failure_patterns: continue
|
| 1406 |
+
tb, tce = _test_hypothesis(problem, hyp)
|
| 1407 |
+
if tce < best_ce:
|
| 1408 |
+
best_ce = tce; best_b = tb
|
| 1409 |
+
|
| 1410 |
+
if best_ce < current.ce:
|
| 1411 |
+
current = Baton(binding=best_b, ce=best_ce,
|
| 1412 |
+
ray_id=current.ray_id, depth=i+1,
|
| 1413 |
+
l7=None, l9=None) # recomputed next iteration
|
| 1414 |
+
|
| 1415 |
+
return accumulated, current
|
| 1416 |
|
| 1417 |
+
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1418 |
+
# SECTION 13: SEQUENCE RAY TRACER
|
| 1419 |
+
# Manages a tree of AxiomRays. Rays terminate with a Baton.
|
| 1420 |
+
# Children inherit the Baton and extend the sequence.
|
| 1421 |
+
# Branching from both stalling and productive rays.
|
| 1422 |
+
# Earned Extension: must reduce CE by CE_EARN_RATIO to branch,
|
| 1423 |
+
# except when depth < MIN_DEPTH where branching is always allowed.
|
| 1424 |
+
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1425 |
+
class SequenceRayTracer:
|
| 1426 |
+
MAX_TOTAL_RAYS = 80
|
| 1427 |
+
BRANCH_WIDTH = 4
|
| 1428 |
+
MIN_DEPTH = 1
|
| 1429 |
+
CE_EARN_RATIO = 0.90 # 10% CE reduction earns a branch
|
| 1430 |
+
|
| 1431 |
+
def trace(self, axl_def: AXLProblemDef, base_problem: Problem):
|
| 1432 |
+
self.all_traces: List[HypothesisTrace] = []
|
| 1433 |
+
generator = SequenceHypothesisGenerator()
|
| 1434 |
+
|
| 1435 |
+
# Seed: one length-1 ray per axiom, shuffled (no ordering bias)
|
| 1436 |
+
active: List[AxiomRay] = [
|
| 1437 |
+
AxiomRay(sequence=[a], ray_id=f"S{i}", depth=0)
|
| 1438 |
+
for i,a in enumerate(ALL_AXIOMS)
|
| 1439 |
+
]
|
| 1440 |
+
random.shuffle(active)
|
| 1441 |
+
|
| 1442 |
+
all_batons: List[Baton] = []
|
| 1443 |
best_ce = float('inf')
|
| 1444 |
+
best_binding: Dict = {}
|
| 1445 |
+
history: List[Dict] = []
|
| 1446 |
+
total_fired = 0
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1447 |
|
| 1448 |
+
init_b = {v:(lo+hi)/2 for v,(lo,hi) in base_problem.bounds.items()}
|
| 1449 |
+
init_ce = base_problem.constraint_energy(init_b)
|
|
|
|
|
|
|
|
|
|
| 1450 |
|
| 1451 |
+
# Try algebraic snap + MPRT on initial binding
|
| 1452 |
+
snap_b, snap_ce = _algebraic_snap(base_problem, init_b)
|
| 1453 |
+
if snap_ce < init_ce: init_b = snap_b; init_ce = snap_ce
|
| 1454 |
+
mprt_b, mprt_ce = _mprt_sample(base_problem,
|
| 1455 |
+
{v:IV(*base_problem.bounds[v]) for v in base_problem.variables},
|
| 1456 |
+
N_MPRT_EXPLORE//5)
|
| 1457 |
+
if mprt_ce < init_ce: init_b = mprt_b; init_ce = mprt_ce
|
| 1458 |
|
| 1459 |
+
seed_baton = Baton(binding=init_b, ce=init_ce, ray_id="SEED")
|
| 1460 |
|
| 1461 |
+
print(f"\n{'β'*65}\nSEQUENCE RAY TRACE: {axl_def.name}\n{'β'*65}")
|
| 1462 |
+
|
| 1463 |
+
while active and total_fired < self.MAX_TOTAL_RAYS:
|
| 1464 |
+
ray = active.pop(0)
|
| 1465 |
+
total_fired += 1
|
| 1466 |
|
| 1467 |
+
parent_baton = ray.baton or seed_baton
|
| 1468 |
+
model = StructuralModel(
|
| 1469 |
+
best_binding = best_binding if best_binding else parent_baton.binding,
|
| 1470 |
+
best_ce = best_ce if best_ce < float('inf') else init_ce
|
| 1471 |
+
)
|
| 1472 |
+
|
| 1473 |
+
t0 = time.time()
|
| 1474 |
+
hyps, output_baton = generator.generate(
|
| 1475 |
+
ray.sequence, base_problem, parent_baton, all_batons, model)
|
| 1476 |
+
elapsed = round((time.time()-t0)*1000, 1)
|
| 1477 |
+
|
| 1478 |
+
output_baton.ray_id = ray.ray_id
|
| 1479 |
+
all_batons.append(output_baton)
|
| 1480 |
+
|
| 1481 |
+
if output_baton.ce < best_ce:
|
| 1482 |
+
best_ce = output_baton.ce
|
| 1483 |
+
best_binding = dict(output_baton.binding)
|
| 1484 |
+
|
| 1485 |
+
verify = VERIFY_LAYER.run(output_baton.binding, base_problem, axl_def.anchors)
|
| 1486 |
+
trace = HypothesisTrace(
|
| 1487 |
+
hid = ray.ray_id,
|
| 1488 |
+
round_idx = total_fired,
|
| 1489 |
+
ray_name = ray.name,
|
| 1490 |
+
action = "SequenceRay",
|
| 1491 |
+
ce_before = parent_baton.ce if parent_baton.ce < float('inf') else 99.0,
|
| 1492 |
+
ce_after = output_baton.ce,
|
| 1493 |
+
verify = verify,
|
| 1494 |
+
survived = verify.overall_pass,
|
| 1495 |
+
elapsed_ms= elapsed,
|
| 1496 |
+
depth = ray.depth,
|
| 1497 |
+
parent_id = ray.parent_id or "",
|
| 1498 |
+
)
|
| 1499 |
+
self.all_traces.append(trace)
|
| 1500 |
+
|
| 1501 |
+
status = "β SURVIVED" if verify.overall_pass else ""
|
| 1502 |
+
print(f" [{total_fired:3d}] {ray.name:<40} "
|
| 1503 |
+
f"CE {parent_baton.ce:.4f}β{output_baton.ce:.4f} "
|
| 1504 |
+
f"G1={'β' if verify.gate1_pass else 'β'} "
|
| 1505 |
+
f"G2={'β' if verify.gate2_pass else 'β'} "
|
| 1506 |
+
f"{status}")
|
| 1507 |
+
|
| 1508 |
+
history.append({
|
| 1509 |
+
"ray_id": ray.ray_id,
|
| 1510 |
+
"sequence": ray.name,
|
| 1511 |
+
"depth": ray.depth,
|
| 1512 |
+
"parent": ray.parent_id,
|
| 1513 |
+
"ce_in": round(parent_baton.ce,5) if parent_baton.ce < float('inf') else 99.0,
|
| 1514 |
+
"ce_out": round(output_baton.ce,5),
|
| 1515 |
+
"survived": verify.overall_pass,
|
| 1516 |
+
"ms": elapsed,
|
| 1517 |
+
})
|
| 1518 |
+
|
| 1519 |
+
if verify.overall_pass:
|
| 1520 |
+
print(f"\nβ TRUE UNIVERSE FOUND: {ray.name}")
|
| 1521 |
+
break
|
| 1522 |
+
|
| 1523 |
+
# Branching decision
|
| 1524 |
+
parent_ce = parent_baton.ce if parent_baton.ce < float('inf') else init_ce
|
| 1525 |
+
earned = (output_baton.ce < parent_ce * self.CE_EARN_RATIO
|
| 1526 |
+
or ray.depth < self.MIN_DEPTH)
|
| 1527 |
+
if earned:
|
| 1528 |
+
children = self._spawn_children(ray, output_baton)
|
| 1529 |
+
# Depth-first: children at front
|
| 1530 |
+
active = children + active
|
| 1531 |
+
|
| 1532 |
+
survived = [t for t in self.all_traces if t.survived]
|
| 1533 |
+
failed = [t for t in self.all_traces if not t.survived]
|
| 1534 |
+
best_t = min(survived, key=lambda t: t.ce_after, default=None)
|
| 1535 |
+
print(f"\n{'β'*65}")
|
| 1536 |
+
print(f"RESULT: CE={best_ce:.5f} | Fired={total_fired} | "
|
| 1537 |
+
f"Survived={len(survived)} | Best={best_t.ray_name if best_t else 'β'}")
|
| 1538 |
return best_binding, best_ce, history
|
| 1539 |
|
| 1540 |
+
def _spawn_children(self, ray: AxiomRay, baton: Baton) -> List[AxiomRay]:
|
| 1541 |
+
remaining = [a for a in ALL_AXIOMS if a not in ray.sequence]
|
| 1542 |
+
random.shuffle(remaining) # no ordering bias in child selection
|
| 1543 |
+
children: List[AxiomRay] = []
|
| 1544 |
+
for axiom in remaining:
|
| 1545 |
+
child = ray.extend(axiom)
|
| 1546 |
+
if child:
|
| 1547 |
+
child.baton = baton
|
| 1548 |
+
children.append(child)
|
| 1549 |
+
if len(children) >= self.BRANCH_WIDTH * 2:
|
| 1550 |
+
break
|
| 1551 |
+
return children
|
| 1552 |
+
|
| 1553 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1554 |
+
# SECTION 14: HARDCODED AXL PROBLEMS (unchanged from 12.1)
|
| 1555 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1556 |
AXL_PROBLEMS=[
|
| 1557 |
AXLProblemDef(
|
|
|
|
| 1564 |
],
|
| 1565 |
constraints=[
|
| 1566 |
{"kind":"CONSERVE","expr":"x1**2 + x2**2 + x3**2 + x4**2 - 1.0"},
|
| 1567 |
+
{"kind":"EQ","expr":"x1 + x2 + x3 + x4","weight":2.0},
|
| 1568 |
],
|
| 1569 |
scopes=[{"name":"sphere","order":0,"vars":["x1","x2","x3","x4"],
|
| 1570 |
"constraints":[{"kind":"EQ","expr":"x1**2 + x2**2 + x3**2 + x4**2 - 1.0","weight":5.0}]}],
|
|
|
|
| 1629 |
description="3 vars packed with min separation, centred, norm=6",
|
| 1630 |
axioms={Axiom.CONTINUOUS,Axiom.METRIC,Axiom.INJECTIVE,Axiom.CONSERVED,Axiom.SYMMETRIC},
|
| 1631 |
variables=[
|
| 1632 |
+
{"name":"a","lo":-3.0,"hi":3.0}, {"name":"b","lo":-3.0,"hi":3.0},
|
| 1633 |
+
{"name":"c","lo":-3.0,"hi":3.0},
|
| 1634 |
],
|
| 1635 |
constraints=[
|
| 1636 |
{"kind":"CONSERVE","expr":"a + b + c"},
|
|
|
|
| 1639 |
{"kind":"GEQ","expr":"(a - c)**2 - 4.0","weight":2.0},
|
| 1640 |
],
|
| 1641 |
scopes=[{"name":"packing","order":0,"vars":["a","b","c"],
|
| 1642 |
+
"constraints":[{"kind":"EQ","expr":"a**2 + b**2 + c**2 - 6.0","weight":2.0}]}],
|
|
|
|
|
|
|
| 1643 |
anchors=[
|
| 1644 |
AXLInvariant("centred","a + b + c",1e-3),
|
| 1645 |
AXLInvariant("sep_ab","(a - b)**2 - 1.0",0.5),
|
|
|
|
| 1649 |
),
|
| 1650 |
]
|
| 1651 |
|
| 1652 |
+
def build_base_problem(axl_def: AXLProblemDef) -> Problem:
|
| 1653 |
+
psl_text = AXL_COMPILER.compile(axl_def)
|
| 1654 |
+
prog = parse_psl(psl_text); ep = expand_psl(prog)
|
| 1655 |
+
return Problem(pid=f"base_{axl_def.name}", variables=ep.variables,
|
| 1656 |
+
constraints=ep.constraints, bounds=ep.bounds,
|
| 1657 |
+
scope_groups=ep.scope_groups, scope_vars=ep.scope_vars,
|
| 1658 |
+
scope_order=ep.scope_order, annotations=ep.annotations)
|
| 1659 |
|
| 1660 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1661 |
+
# SECTION 15: GLOBAL STATE + RUNNER
|
| 1662 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1663 |
+
STATE_LOCK = threading.Lock()
|
| 1664 |
+
RUN_LOG: List[Dict] = []
|
| 1665 |
+
THEORIST = SequenceRayTracer()
|
| 1666 |
+
POOL = ThreadPoolExecutor(max_workers=2)
|
| 1667 |
|
| 1668 |
+
def _run_problem(axl_def: AXLProblemDef):
|
| 1669 |
try:
|
| 1670 |
base_prob = build_base_problem(axl_def)
|
| 1671 |
+
binding, ce, history = THEORIST.trace(axl_def, base_prob)
|
| 1672 |
+
|
| 1673 |
survived = [t for t in THEORIST.all_traces if t.survived]
|
| 1674 |
+
failed = [t for t in THEORIST.all_traces if not t.survived]
|
| 1675 |
+
best_t = min(survived, key=lambda t: t.ce_after, default=None)
|
| 1676 |
+
|
| 1677 |
+
record = {
|
| 1678 |
+
"problem": axl_def.name,
|
| 1679 |
"description": axl_def.description,
|
| 1680 |
+
"ce": round(ce, 6),
|
| 1681 |
+
"solved": len(survived) > 0 and ce < SOLVE_THRESHOLD,
|
| 1682 |
+
"binding": {k: round(v,5) for k,v in binding.items()},
|
| 1683 |
+
"observations":axl_def.observations,
|
| 1684 |
"traces": [{
|
| 1685 |
+
"round": t.round_idx,
|
| 1686 |
+
"ray": t.ray_name,
|
| 1687 |
+
"depth": t.depth,
|
| 1688 |
+
"parent": t.parent_id,
|
| 1689 |
+
"ce_before":round(t.ce_before,5),
|
| 1690 |
+
"ce": round(t.ce_after,5),
|
| 1691 |
+
"g1_ce": round(t.verify.gate1_ce,5) if t.verify else None,
|
| 1692 |
+
"g1": t.verify.gate1_pass if t.verify else False,
|
| 1693 |
+
"g2": t.verify.gate2_pass if t.verify else False,
|
| 1694 |
+
"g2_detail":{k:(round(err,6),ok) for k,(err,ok) in t.verify.gate2_results.items()} if t.verify else {},
|
| 1695 |
+
"survived": t.survived,
|
| 1696 |
+
"ms": t.elapsed_ms,
|
| 1697 |
} for t in THEORIST.all_traces],
|
| 1698 |
+
"ray_tree": history,
|
| 1699 |
"survived_count": len(survived),
|
| 1700 |
+
"failed_count": len(failed),
|
| 1701 |
+
"best_ray": best_t.ray_name if best_t else "β",
|
| 1702 |
+
"total_fired": len(THEORIST.all_traces),
|
| 1703 |
}
|
| 1704 |
with STATE_LOCK:
|
| 1705 |
RUN_LOG.append(record)
|
|
|
|
| 1709 |
print(f"[RUN ERROR] {axl_def.name}: {e}")
|
| 1710 |
|
| 1711 |
async def run_loop():
|
| 1712 |
+
loop = asyncio.get_event_loop()
|
| 1713 |
while True:
|
| 1714 |
+
prob = random.choice(AXL_PROBLEMS)
|
| 1715 |
await loop.run_in_executor(POOL, _run_problem, prob)
|
| 1716 |
await asyncio.sleep(0.3)
|
| 1717 |
|
|
|
|
| 1722 |
POOL.shutdown(wait=False)
|
| 1723 |
|
| 1724 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1725 |
+
# SECTION 16: FASTAPI + DASHBOARD
|
| 1726 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1727 |
+
app = FastAPI(title="Practicality 13.0", lifespan=lifespan)
|
| 1728 |
|
| 1729 |
+
def _render_collapse(record: Dict) -> str:
|
| 1730 |
+
b = record["binding"]; traces = record["traces"]
|
| 1731 |
+
survived = [t for t in traces if t["survived"]]
|
| 1732 |
+
best = min(survived, key=lambda t: t["ce"], default=None)
|
| 1733 |
+
if not best and traces:
|
| 1734 |
+
best = min(traces, key=lambda t: t.get("g1_ce") or 999.0)
|
| 1735 |
+
obs_vars = set(record.get("observations",{}).keys())
|
| 1736 |
|
| 1737 |
+
ce = record["ce"]; solved = record["solved"]
|
| 1738 |
+
ce_color = "#4CAF50" if solved else ("#FF9800" if ce < 0.5 else "#EF5350")
|
| 1739 |
+
status = "β SOLVED + VERIFIED" if solved else ("~ PARTIAL" if ce < 0.5 else "β UNSOLVED")
|
|
|
|
| 1740 |
|
| 1741 |
+
binding_rows = "".join(
|
| 1742 |
f"<tr><td style='color:#888;width:70px'>{v}</td>"
|
| 1743 |
f"<td style='color:#26C6DA;font-weight:700'>{val:+.5f}</td>"
|
| 1744 |
f"<td style='color:#4CAF50;font-size:0.75em'>{'[OBS]' if v in obs_vars else ''}</td></tr>"
|
| 1745 |
for v,val in b.items())
|
| 1746 |
|
| 1747 |
+
inv_rows = ""
|
| 1748 |
if best and best.get("g2_detail"):
|
| 1749 |
for inv,(err,ok) in best["g2_detail"].items():
|
| 1750 |
+
c = "#4CAF50" if ok else "#EF5350"
|
| 1751 |
+
inv_rows += (f"<tr><td style='color:{c}'>{'β' if ok else 'β'}</td>"
|
| 1752 |
+
f"<td style='color:#aaa'>{inv}</td>"
|
| 1753 |
+
f"<td style='color:{c}'>{err:.6f}</td></tr>")
|
| 1754 |
|
| 1755 |
def trail_span(t):
|
| 1756 |
+
depth_pad = " " * min(t.get("depth",0), 6)
|
| 1757 |
+
c = "#4CAF50" if t["survived"] else ("#555" if t.get("depth",0) > 0 else "#333")
|
| 1758 |
+
ce_delta = t["ce"] - t.get("ce_before", t["ce"])
|
| 1759 |
+
delta_str = f"Ξ{ce_delta:+.4f}" if abs(ce_delta) > 1e-6 else ""
|
| 1760 |
+
star = " β VERIFIED" if t["survived"] else ""
|
| 1761 |
+
return (f"<div style='color:{c};font-size:0.75em;margin-bottom:2px'>"
|
| 1762 |
+
f"{depth_pad}[R{t['round']}|d{t.get('depth',0)}] "
|
| 1763 |
+
f"<span style='color:#FF9800'>{t['ray']}</span> "
|
| 1764 |
+
f"CE={t['ce']:.5f} <span style='color:#555'>{delta_str}</span> "
|
| 1765 |
+
f"G1={'β' if t['g1'] else 'β'} G2={'β' if t['g2'] else 'β'}"
|
| 1766 |
f"<span style='color:#4CAF50;font-weight:700'>{star}</span></div>")
|
| 1767 |
|
| 1768 |
+
trail = "".join(trail_span(t) for t in traces[:30])
|
| 1769 |
|
| 1770 |
return f"""
|
| 1771 |
+
<div style='border:1px solid #1a1a1a;border-radius:8px;margin-bottom:18px;overflow:hidden'>
|
| 1772 |
<div style='background:#0e0e0e;padding:9px 14px;border-bottom:1px solid #1a1a1a;display:flex;align-items:center;gap:16px'>
|
| 1773 |
<span style='color:{ce_color};font-weight:700;font-size:1.05em'>{status}</span>
|
| 1774 |
<span style='color:#444;font-size:0.85em'>{record["problem"]}</span>
|
| 1775 |
+
<span style='color:#333;font-size:0.8em'>CE={ce:.6f}</span>
|
| 1776 |
+
<span style='color:#26C6DA;font-size:0.75em'>{record["survived_count"]} survived / {record["total_fired"]} fired</span>
|
| 1777 |
</div>
|
| 1778 |
<div style='display:flex'>
|
| 1779 |
<div style='flex:0 0 180px;padding:10px 12px;border-right:1px solid #1a1a1a'>
|
|
|
|
| 1786 |
{inv_rows or "<tr><td colspan='3' style='color:#222'>β</td></tr>"}
|
| 1787 |
</table>
|
| 1788 |
</div>
|
| 1789 |
+
<div style='flex:1;padding:10px 12px;overflow-y:auto;max-height:260px'>
|
| 1790 |
<div style='color:#333;font-size:0.7em;margin-bottom:5px'>
|
| 1791 |
+
SEQUENCE RAY TREE β best: <span style='color:#FF9800'>{record["best_ray"]}</span>
|
| 1792 |
</div>
|
| 1793 |
{trail}
|
| 1794 |
</div>
|
| 1795 |
</div>
|
| 1796 |
</div>"""
|
| 1797 |
|
| 1798 |
+
@app.get("/", response_class=HTMLResponse)
|
| 1799 |
async def dashboard():
|
| 1800 |
+
with STATE_LOCK: log = list(reversed(RUN_LOG[-10:]))
|
| 1801 |
+
runs = len(RUN_LOG)
|
| 1802 |
+
solved = sum(1 for r in RUN_LOG if r.get("solved",False))
|
| 1803 |
+
avg_ce = round(sum(r["ce"] for r in RUN_LOG)/max(1,runs),5) if RUN_LOG else 0
|
| 1804 |
|
| 1805 |
+
# Axiom efficacy across all sequence positions
|
| 1806 |
+
axiom_stats = defaultdict(lambda: {"tried":0,"survived":0,"total_ce":0.0,"as_seed":0})
|
| 1807 |
for r in log:
|
| 1808 |
+
for t in r.get("traces",[]):
|
| 1809 |
+
ray_str = t["ray"]
|
| 1810 |
+
parts = ray_str.split("β")
|
| 1811 |
+
for pos, ax_abbr in enumerate(parts):
|
| 1812 |
+
if not ax_abbr: continue
|
| 1813 |
+
axiom_stats[ax_abbr]["tried"] += 1
|
| 1814 |
+
axiom_stats[ax_abbr]["total_ce"] += t["ce"]
|
| 1815 |
+
if t["survived"]: axiom_stats[ax_abbr]["survived"] += 1
|
| 1816 |
+
if pos == 0: axiom_stats[ax_abbr]["as_seed"] += 1
|
| 1817 |
+
|
| 1818 |
+
axiom_rows = "".join(
|
| 1819 |
f"<tr><td style='color:#FF9800'>{ax}</td>"
|
| 1820 |
f"<td style='color:#aaa'>{s['tried']}</td>"
|
| 1821 |
+
f"<td style='color:#26C6DA'>{s['as_seed']}</td>"
|
| 1822 |
f"<td style='color:#4CAF50'>{s['survived']}</td>"
|
| 1823 |
f"<td style='color:#EF5350'>{s['tried']-s['survived']}</td>"
|
| 1824 |
f"<td style='color:#26C6DA'>{round(s['total_ce']/s['tried'],5) if s['tried'] else 0}</td>"
|
| 1825 |
f"<td style='color:{'#4CAF50' if s['survived']>0 else '#333'}'>"
|
| 1826 |
f"{round(s['survived']/s['tried']*100):.0f}%</td></tr>"
|
| 1827 |
+
for ax,s in sorted(axiom_stats.items(), key=lambda x:-x[1]["survived"])
|
| 1828 |
+
) or "<tr><td colspan='7' style='color:#222'>Warming upβ¦</td></tr>"
|
| 1829 |
|
| 1830 |
+
collapses = "".join(_render_collapse(r) for r in log) if log else \
|
| 1831 |
"<div style='color:#222;padding:20px'>Warming upβ¦</div>"
|
| 1832 |
|
| 1833 |
+
return f"""<!DOCTYPE html><html><head><title>Practicality 13.0</title>
|
| 1834 |
<meta http-equiv="refresh" content="4">
|
| 1835 |
<style>
|
| 1836 |
+
body{{background:#090909;color:#e0e0e0;font-family:monospace;padding:20px;max-width:1500px}}
|
| 1837 |
h1{{color:#26C6DA;border-bottom:1px solid #1a1a1a;padding-bottom:6px;font-size:1.15em}}
|
| 1838 |
h3{{color:#2a2a2a;margin-top:20px;font-size:0.85em;letter-spacing:2px;text-transform:uppercase}}
|
| 1839 |
table{{width:100%;border-collapse:collapse;margin-bottom:10px}}
|
|
|
|
| 1841 |
th{{color:#2a2a2a;font-size:0.72em}}
|
| 1842 |
.badge{{display:inline-block;padding:3px 10px;border-radius:3px;background:#0e0e0e;margin:2px;font-size:0.78em;border:1px solid #1a1a1a}}
|
| 1843 |
</style></head><body>
|
| 1844 |
+
<h1>β Practicality 13.0 β Sequence Rays (Ordered Axiom Chains)</h1>
|
| 1845 |
<div style='color:#333;font-size:0.75em;margin-bottom:12px'>
|
| 1846 |
+
27 Axioms (Math Β· Physics Β· Logic Β· Philosophy) β Ordered Sequences β
|
| 1847 |
+
Baton Protocol (child inherits partial) β Earn Extension by CE reduction β
|
| 1848 |
+
Contradiction at Distance allowed
|
| 1849 |
</div>
|
| 1850 |
<div style='margin-bottom:16px'>
|
| 1851 |
<span class='badge' style='color:#aaa'>Runs: {runs}</span>
|
| 1852 |
<span class='badge' style='color:#4CAF50'>Solved: {solved}</span>
|
| 1853 |
+
<span class='badge' style='color:#26C6DA'>Avg CE: {avg_ce}</span>
|
| 1854 |
<span class='badge' style='color:#FF9800'>Problems: {len(AXL_PROBLEMS)}</span>
|
| 1855 |
+
<span class='badge' style='color:#5C6BC0'>Axioms: {len(ALL_AXIOMS)}</span>
|
| 1856 |
</div>
|
| 1857 |
+
<h3>Axiom Efficacy β All Sequence Positions</h3>
|
| 1858 |
<table>
|
| 1859 |
+
<tr><th>Axiom</th><th>In-Seq</th><th>As Seed</th><th>Survived</th><th>Failed</th><th>Avg CE</th><th>Efficacy</th></tr>
|
| 1860 |
{axiom_rows}
|
| 1861 |
</table>
|
| 1862 |
<h3>Collapse View β Recent Runs</h3>
|
| 1863 |
{collapses}
|
| 1864 |
</body></html>"""
|
| 1865 |
|
| 1866 |
+
if __name__ == "__main__":
|
| 1867 |
+
uvicorn.run(app, host="0.0.0.0", port=7860, log_level="warning")
|