diff --git a/research/four-plane-rank-dual/CERT-INDEX.bin.gz b/research/four-plane-rank-dual/CERT-INDEX.bin.gz new file mode 100644 index 000000000..7c525e1ed Binary files /dev/null and b/research/four-plane-rank-dual/CERT-INDEX.bin.gz differ diff --git a/research/four-plane-rank-dual/CERTIFICATES.json.gz b/research/four-plane-rank-dual/CERTIFICATES.json.gz new file mode 100644 index 000000000..486ac4534 Binary files /dev/null and b/research/four-plane-rank-dual/CERTIFICATES.json.gz differ diff --git a/research/four-plane-rank-dual/README.md b/research/four-plane-rank-dual/README.md new file mode 100644 index 000000000..fd831e263 --- /dev/null +++ b/research/four-plane-rank-dual/README.md @@ -0,0 +1,103 @@ +# Four-plane COPY floor: exact certificates for 98.5% of plane quadruples + +**Claim type:** exact lower-bound certificates, checked by a standard-library verifier, plus a +documented open remainder. **No new κ.** This extends CubeJerry's +[#4365](https://github.com/CrocSwap/integer-mult-bounds/pull/4365), which closed two-plane +mixing, and my [#4421](https://github.com/CrocSwap/integer-mult-bounds/pull/4421), which closed +three-plane mixing on all 27,720 triples, to four planes. The contract is #4365's unchanged: + +- whole-plane closures; +- `F₂`-rank tariffs `t(S, T)`; +- additive charges; +- payload in any field. + +## Result + +For **361,706 of the 367,290 plane quadruples (98.48%)**, every decomposition of `I₈` costs at +least **16 = Σ p_i²**, over every field. This is exactly the cost of separate coordinate messages, +so on those quadruples four-plane mixing cannot lower the COPY mass. **5,584 quadruples, in 3,650 +tariff classes, remain open.** + +## Certificates + +The functionals are those of #4421, extended to four planes: + + L(M) = Σ_{(Z, X)} w · rank(Φ_Z(M)_XX). + +- `X` ranges over the 15 plane unions. +- `Φ_Z` zeroes a set `Z` of the 12 off-diagonal plane blocks. `Z = ∅` gives #4365's block-rank + functional. +- **Subadditivity.** `rank` of a linear image is subadditive. +- **Atom bound.** `Φ_Z(u vᵀ)_XX` is a sum over touched row planes of `u_P(Σ_allowed v_Q)ᵀ`. So its + rank is at most the number of distinct allowed column (or row) plane sets, a combinatorial bound + valid over every field. +- **The test.** If `Σ w·bound(S, T, X, Z) ≤ t(S, T)` for all 225 closure pairs, every decomposition + costs at least `L(I₈) = Σ w·2|X|`. This holds because `Φ_Z` never touches the diagonal blocks. + +Coverage: + +| Certificate | Classes | Quadruples | +| --- | --- | --- | +| block-rank (`Z = ∅`) | 195,523 | the bulk | +| zeroed-block and mixed (several `Z`) | 24,732 | | +| **total certified** | **220,255 of 223,905** | **361,706 of 367,290** | + +All certificates have value exactly 16, and there are 9,330 distinct ones. `verify.py` +recomputes all 367,290 quadruples' tariffs from the pinned selected archive and matching +certificate, the same pins as #4365 and #4421. It reads one certificate index per quadruple from +`CERT-INDEX.bin.gz` and checks every certificate exactly, with integer-scaled weights against an +exact bound table that it builds itself. + +## The open remainder + +On the 3,650 open classes, the best LP value over all `4096 × 15` zero-set and union pairs ranges +from 12.571 to just under 16. Most values are 15.33, 15.5, 15.0 or 15.6. These classes typically +combine two kinds of cheap atom: + +- one free plane pair: binary cross rank 0, so messages between the two planes cost 0; +- a cheap full closure: joint Gram rank 5–7 instead of 8, so a message touching all four planes + costs less than 8. + +The LP's fractional covering leans on the free cross atoms. As in the three-plane case, a real +decomposition must cancel them, and these functionals cannot see the cancellation. For the +triples, one more family (mixed `Z`) closed the gap. For quadruples, the families here, including +off-principal blocks `rank(Φ_Z(M)_{X,Y})` tested on three open classes, do not. These quadruples +are **undecided**, not counterexamples. Two direct tests on one of them were also inconclusive: + +- an exact `F₂` ILP over 65,025 binary atoms for mass ≤ 15 hit its 900 s limit; +- a short real-coefficient search found nothing. + +## Not covered + +- The ℚ/ℂ minimum on the 5,584 open quadruples. +- Decoders over five or more planes. +- Native realization, coverage and hosting, which are #4365's caveats. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/four-plane-rank-dual --check-only +python3.12 -B scripts/research_package.py --package research/four-plane-rank-dual +``` + +The verifier prints `PASS_FOUR_PLANE_RANK_DUAL` in about 4.5 minutes, using only the standard +library. `generation/` holds the scipy scripts that produced the certificates; verification does +not need them. + +## Open next questions + +1. **Is the four-plane mass below 16 over ℂ on the open classes?** + - *Why it matters:* a mass below 16 would be the first mixing gain under #4365's contract. + - *First step:* a cancellation-aware functional for a free plane pair combined with a cheap full + closure. Alternatively, an exact `F₃` or `F₂` search on the lowest class (LP 12.571). + - *Blocked by:* nothing. + +## Credit + +- The contract and the two-plane theorem are CubeJerry's (#4365). +- The labels and matching come from PR1825/2126 (Cinna Davis) and the retained matching + certificate. +- Gonzalo Mier's PR3990/3997 are predecessors. + +Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. +Apache-2.0. diff --git a/research/four-plane-rank-dual/SOURCES.json b/research/four-plane-rank-dual/SOURCES.json new file mode 100644 index 000000000..0de64cce8 --- /dev/null +++ b/research/four-plane-rank-dual/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + }, + { + "path": "research/paired-plane-port-matching-seed6c563a/CERTIFICATE.json", + "usage": "input", + "git_blob": "7ca668d7d50c7276e89b0f6f9575e1b9f1ad9ef6", + "sha256": "4fd648f7b5178bff5441bf364d58234b7bc1a43b924bc6da03013c948f1473b1" + } + ] +} diff --git a/research/four-plane-rank-dual/TASK.json b/research/four-plane-rank-dual/TASK.json new file mode 100644 index 000000000..a159becbf --- /dev/null +++ b/research/four-plane-rank-dual/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 7, + "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "refined", + "actual_scope": "Extend #4365/#4421's rank dual to plane quadruples: exact all-field certificates of the four-plane COPY floor 16.", + "scope_change_reason": "#4421 closed three-plane mixing; its open question 1 is four planes.", + "bottleneck_link": "Local decoders that mix planes could only help if they lower COPY mass below separate messages.", + "budget_minutes": 120, + "stop_rule": "Stop at the zero-set certificate families; report the remainder as open.", + "outcome": "completed", + "evidence": "verify.py: 361,706 of 367,290 quadruples (220,255 of 223,905 tariff classes) certified at floor 16 over every field with 9,330 exact certificates; 5,584 quadruples open with LP values 12.571..15.9.", + "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", + "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.", + "open_questions": [ + { + "question": "Is the four-plane COPY mass below 16 over C on the 3,650 open classes?", + "why_it_matters": "It would be the first mixing gain under #4365's contract.", + "first_step": "A cancellation-aware functional for free pairs with cheap full closures, or an exact F3/F2 search on the lowest class.", + "blocked_by": "None." + } + ] +} diff --git a/research/four-plane-rank-dual/VERIFY.json b/research/four-plane-rank-dual/VERIFY.json new file mode 100644 index 000000000..1bac8b1eb --- /dev/null +++ b/research/four-plane-rank-dual/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1094-audit/selected-replay.tar.gz", + "research/paired-plane-port-matching-seed6c563a/CERTIFICATE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Pinned archive and matching; tariffs of all 367,290 plane quadruples recomputed; 9,330 distinct certificates of value 16 checked exactly (integer-scaled weights, self-built zeroed-block bound table) on every referenced class; 361,706 quadruples certified, 5,584 reported open." + } + ] +} diff --git a/research/four-plane-rank-dual/diagnostics/LOWEST-CLASS.md b/research/four-plane-rank-dual/diagnostics/LOWEST-CLASS.md new file mode 100644 index 000000000..ba7d44f04 --- /dev/null +++ b/research/four-plane-rank-dual/diagnostics/LOWEST-CLASS.md @@ -0,0 +1,50 @@ +# Diagnostic: the lowest open quadruple class (LP 12.571) + +This is local, exploratory evidence. It is not part of the registered verifier and is not a theorem. + +## The class + +The example quadruple is planes `(7, 8, 15, 52)`. Its single-plane cross tariffs are + +- `A–B` and `C–D`: 0, so messages between those planes are free; +- every other cross pair: 2, with each such plane pair's joint Gram of rank 2 ("aligned"). + +The full closure costs 8. The best zeroed-block LP value is 88/7 = 12.571. + +## Why the zeroed-block family stops short here + +Take `Z = {AB, BA, CD, DC}`. The candidate `L(M) = 2·rank(Φ_Z(M))` has `L(I) = 16` and satisfies 221 of +the 225 atom inequalities. It fails only on `(ABC, ABD)`, `(ABD, ABC)`, `(ACD, BCD)` and +`(BCD, ACD)`, which each cost 4. On `(ABC, ABD)` the image `Φ_Z(u vᵀ)` has row vectors + + w_A = (v_A, 0, v_D), w_B = (0, v_B, v_D), w_C = (v_A, v_B, 0), + +with `w_A + w_B − w_C = (0, 0, 2v_D)`. This is rank 2 in characteristic 2, where the functional +would give `L ≤ 4`, but generically rank 3 in characteristic 0, where `L = 6 > 4`. So the obstruction +to certifying 16 is characteristic-dependent. The combinatorial atom bound cannot see that +difference. + +## A border decomposition at mass 14 over ℝ + +The LP's fractional covering suggested the patterns. `lowreal.py` searches small multisets of those +patterns plus free atoms with alternating least squares. The best mass-14 multiset is +`AC×AC, AD×AD, 2·BD×BD, BCD×ACD, AB×CD` plus two of each free atom. `border.py` tracks it: + +| ALS iteration | `‖Σ u vᵀ − I‖` | `max ‖u‖‖v‖` | +| --- | --- | --- | +| 100 | 2.44e-1 | 2.5e3 | +| 1,000 | 7.41e-2 | 2.9e5 | +| 3,000 | 4.26e-2 | 2.7e6 | +| 10,000 | 2.33e-2 | 3.0e7 | +| 20,000 | 1.65e-2 | 1.2e8 | + +The residual tends to 0 only as the coefficients diverge. That is the signature of a border +decomposition (border rank), not an exact one. No exact decomposition below 16 was found. An exact +`F₂` ILP, over 65,025 atoms with mass at most 15, timed out at 1,500 s. + +## Reading + +Over ℝ and ℂ, mass 14 is approached but apparently not attained. A finite-precision decoder cannot +use diverging coefficients, so this is consistent with the open floor being 16, and it explains why +the zeroed-block LP falls below 16. Proving 16 needs a characteristic-0 argument that uses +cancellation, for example the closedness of the set of exact mass-14 decompositions. diff --git a/research/four-plane-rank-dual/diagnostics/border.py b/research/four-plane-rank-dual/diagnostics/border.py new file mode 100644 index 000000000..676a226ee --- /dev/null +++ b/research/four-plane-rank-dual/diagnostics/border.py @@ -0,0 +1,26 @@ +import numpy as np +exec(open('lowreal.py').read().split("cap=int(sys.argv[1])")[0]) +mult=(1, 0, 1, 2, 0, 0, 1, 1, 0, 0) +pats=[p for p,k in zip(paid,mult) for _ in range(k)]+[f for f in free for _ in range(2)] +n=len(pats); I=np.eye(8); rng=np.random.default_rng(11) +bestrun=None +for rs in range(60): + Uv=[np.zeros(8) for _ in pats]; Vv=[np.zeros(8) for _ in pats] + for j,(S,Tt) in enumerate(pats): + Uv[j][coords(S)]=rng.standard_normal(len(coords(S))); Vv[j][coords(Tt)]=rng.standard_normal(len(coords(Tt))) + hist=[] + for it in range(20000): + for side in (0,1): + src=Vv if side==0 else Uv; dst=Uv if side==0 else Vv + for r in range(8): + js=[j for j,(S,Tt) in enumerate(pats) if r in coords(S if side==0 else Tt)] + M=np.array([src[j] for j in js]).T + x,*_=np.linalg.lstsq(M, I[r,:] if side==0 else I[:,r], rcond=None) + for j,xx in zip(js,x): dst[j][r]=xx + if it in (100,1000,3000,10000,19999): + res=np.linalg.norm(sum(np.outer(Uv[j],Vv[j]) for j in range(n))-I) + mx=max(np.linalg.norm(Uv[j])*np.linalg.norm(Vv[j]) for j in range(n)) + hist.append((it,res,mx)) + if bestrun is None or hist[-1][1]>k&1 for i in range(2)] +rng=np.random.default_rng(3) +def als(pats,restarts=30,iters=600): + n=len(pats); I=np.eye(8); best=9 + for _ in range(restarts): + Uv=[np.zeros(8) for _ in pats]; Vv=[np.zeros(8) for _ in pats] + for j,(S,Tt) in enumerate(pats): + Uv[j][coords(S)]=rng.standard_normal(len(coords(S))); Vv[j][coords(Tt)]=rng.standard_normal(len(coords(Tt))) + for it in range(iters): + for side in (0,1): + src=Vv if side==0 else Uv; dst=Uv if side==0 else Vv + for r in range(8): + js=[j for j,(S,Tt) in enumerate(pats) if r in coords(S if side==0 else Tt)] + if not js: continue + M=np.array([src[j] for j in js]).T + x,*_=np.linalg.lstsq(M, I[r,:] if side==0 else I[:,r], rcond=None) + for j,xx in zip(js,x): dst[j][r]=xx + if it%50==49: + res=np.linalg.norm(sum(np.outer(Uv[j],Vv[j]) for j in range(n))-I) + if res<1e-10: return res,(Uv,Vv) + res=np.linalg.norm(sum(np.outer(Uv[j],Vv[j]) for j in range(n))-I); best=min(best,res) + return best,None +cap=int(sys.argv[1]); t=time.time(); tried=0; best=9 +for mult in itertools.product(range(3),repeat=len(paid)): + m=sum(c*k for c,k in zip(cost,mult)) + if m>cap or sum(mult)<4: continue + pats=[p for p,k in zip(paid,mult) for _ in range(k)]+[f for f in free for _ in range(2)] + # necessary: every diagonal plane block reachable by >=2 paid terms (free atoms never touch diagonal blocks) + if any(sum(1 for S,Tt in pats[:sum(mult)] if S&P and Tt&P)<2 for P in (A,B,C,D)): continue + tried+=1 + r,sol=als(pats,restarts=6,iters=300) + if r 12` solves the zeroed-block and mixed LPs for the weak classes, first over + subsets of the cheap cross pairs and then over all 4096 zero sets. +4. `fastcheck.py` holds the exact checker shared with `verify.py`. +5. `gen_quad.py` rationalizes every certificate, checks it exactly, deduplicates, and writes the + two artifacts. + +`verify.py` re-derives the tariffs and the bound table itself, and trusts nothing produced here +beyond the certificate data, which it checks exactly. diff --git a/research/four-plane-rank-dual/generation/fastcheck.py b/research/four-plane-rank-dual/generation/fastcheck.py new file mode 100644 index 000000000..93218699c --- /dev/null +++ b/research/four-plane-rank-dual/generation/fastcheck.py @@ -0,0 +1,32 @@ + +def build_table(): + """bound(S, T, X, Z) for every zero mask Z (12 off-diagonal pairs), as a flat bytearray""" + tab = bytearray(4096 * 15 * 15 * 15) + for S in UNIONS: + for T in UNIONS: + for X in UNIONS: + rows = [P for P in SINGLES if P & S & X] + cols = [Q2 for Q2 in SINGLES if Q2 & T & X] + if not rows or not cols: + continue + rel = [i for i, (P, Q2) in enumerate(OFF) if P in rows and Q2 in cols] + base = ((S - 1) * 15 + T - 1) * 15 + X - 1 + for m in range(4096): + Z = {OFF[i] for i in rel if m >> i & 1} + br = {frozenset(Q2 for Q2 in cols if (P, Q2) not in Z) for P in rows} - {frozenset()} + bc = {frozenset(P for P in rows if (P, Q2) not in Z) for Q2 in cols} - {frozenset()} + tab[m * 3375 + base] = min(len(br), len(bc)) + return tab + + +def cert_ok(tt, cert, tab): + """exact: integer-scaled weights; tt is the 225 tariffs in KEYS order""" + den = 1 + for _, _, w in cert: + den = den * w.denominator // __import__("math").gcd(den, w.denominator) + iw = [(m * 3375, X - 1, int(w * den)) for m, X, w in cert] + for k, (S, T) in enumerate(KEYS): + base = ((S - 1) * 15 + T - 1) * 15 + if sum(w * tab[m + base + x] for m, x, w in iw) > tt[k] * den: + return False + return True diff --git a/research/four-plane-rank-dual/generation/gen_quad.py b/research/four-plane-rank-dual/generation/gen_quad.py new file mode 100644 index 000000000..d24139e7e --- /dev/null +++ b/research/four-plane-rank-dual/generation/gen_quad.py @@ -0,0 +1,56 @@ +"""build CERTIFICATES.json.gz and CERT-INDEX.bin.gz for the four-plane package""" +import pickle, gzip, json, itertools, sys +from fractions import Fraction as Q +from multiprocessing import Pool +import numpy as np +from scipy.optimize import linprog +U=list(range(1,16)); KEYS=[(S,T) for S in U for T in U]; SINGLES=[1,2,4,8] +OFF=[(P,Q2) for P in SINGLES for Q2 in SINGLES if P!=Q2] +pop=lambda x: bin(x).count('1') +def bound(S,T,X,Z): + rows=[P for P in SINGLES if P&S&X]; cols=[Q2 for Q2 in SINGLES if Q2&T&X] + br={frozenset(Q2 for Q2 in cols if (P,Q2) not in Z) for P in rows}-{frozenset()} + bc={frozenset(P for P in rows if (P,Q2) not in Z) for Q2 in cols}-{frozenset()} + return min(len(br),len(bc)) +A0=np.array([[1.0 if (S&X and T&X) else 0.0 for X in U] for S,T in KEYS]); c0=-np.array([2*pop(X) for X in U],float) +UNIONS=U +exec(open('fastcheck.py').read()) +TAB=open('phitab4.bin','rb').read() +def exact_ok(tt,cert): + if sum(2*pop(X)*w for m,X,w in cert)!=16: return False + return cert_ok(tt,cert,TAB) +def block(tt): + r=linprog(c0,A_ub=A0,b_ub=np.array(tt,float),bounds=(0,None),method='highs') + for den in (6,12,60,420): + cert=tuple((0,X,Q(x).limit_denominator(den)) for X,x in zip(U,r.x) if Q(x).limit_denominator(den)>0) + if exact_ok(tt,cert): return tt,cert + return tt,None +if __name__=='__main__': + classes=pickle.load(open('quad_classes.pkl','rb')); weak=set(pickle.load(open('quad_weak.pkl','rb'))) + strong=[k for k in classes if k not in weak] + with Pool(12) as pool: + res=dict(pool.map(block,strong,chunksize=500)) + print('strong',len(strong),'exact certified',sum(1 for v in res.values() if v),flush=True) + for i in range(12): + for tt,(val,nz) in pickle.load(open(f'quad_cert_{i}.pkl','rb')).items(): + if val<16-1e-6: res[tt]=None; continue + cert=None + for den in (6,12,60,420): + cand=tuple(sorted((m,X,Q(w).limit_denominator(den)) for m,X,w in nz if Q(w).limit_denominator(den)>0)) + if exact_ok(tt,cand): cert=cand; break + res[tt]=cert + certs={}; + for tt,cert in res.items(): + if cert is not None and cert not in certs: certs[cert]=len(certs)+1 + print('distinct certificates',len(certs),'certified classes',sum(1 for v in res.values() if v),'of',len(classes),flush=True) + order=list(itertools.combinations(range(56),4)); quad2cls={} + for tt,qs in classes.items(): + for q in qs: quad2cls[q]=tt + idx=bytearray() + for q in order: + c=res.get(quad2cls[q]); ci=certs[c] if c is not None else 0 + idx+=bytes((ci&255,ci>>8)) + out=[[[m,X,str(w)] for m,X,w in cert] for cert,_ in sorted(certs.items(),key=lambda kv:kv[1])] + open('CERTIFICATES.json.gz','wb').write(gzip.compress(json.dumps({"schema":"four-plane-rank-dual/1","certificates":out}).encode(),9)) + open('CERT-INDEX.bin.gz','wb').write(gzip.compress(bytes(idx),9)) + print('quadruples certified', sum(1 for i in range(0,len(idx),2) if idx[i] or idx[i+1]), 'of', len(order)) diff --git a/research/four-plane-rank-dual/generation/phitable.py b/research/four-plane-rank-dual/generation/phitable.py new file mode 100644 index 000000000..7ee02a892 --- /dev/null +++ b/research/four-plane-rank-dual/generation/phitable.py @@ -0,0 +1,18 @@ +import numpy as np, itertools, time +K=4; U=list(range(1,16)); SINGLES=[1,2,4,8] +OFF=[(P,Q) for P in SINGLES for Q in SINGLES if P!=Q] +t=time.time() +tab=np.zeros((4096,15,15,15),dtype=np.uint8) # [Z, S-1, T-1, X-1] +for S in U: + for T in U: + for X in U: + rows=[P for P in SINGLES if P&S&X]; cols=[Q for Q in SINGLES if Q&T&X] + if not rows or not cols: continue + # pairs relevant: (P,Q) with P in rows, Q in cols, P!=Q + rel=[i for i,(P,Q) in enumerate(OFF) if P in rows and Q in cols] + for m in range(4096): + Z={OFF[i] for i in rel if m>>i&1} + br={frozenset(Q for Q in cols if (P,Q) not in Z) for P in rows}-{frozenset()} + bc={frozenset(P for P in rows if (P,Q) not in Z) for Q in cols}-{frozenset()} + tab[m,S-1,T-1,X-1]=min(len(br),len(bc)) +np.save('phitab4.npy',tab); print('built',round(time.time()-t)) diff --git a/research/four-plane-rank-dual/generation/quad.py b/research/four-plane-rank-dual/generation/quad.py new file mode 100644 index 000000000..d22c3f658 --- /dev/null +++ b/research/four-plane-rank-dual/generation/quad.py @@ -0,0 +1,53 @@ +import io, json, tarfile, itertools, pickle, sys, time +import numpy as np +from scipy.optimize import linprog +ROOT='imb/' +arch=open(ROOT+'research/community-frontier1094-audit/selected-replay.tar.gz','rb').read() +with tarfile.open(fileobj=io.BytesIO(arch),mode='r:gz') as tf: + data=json.loads(tf.extractfile('candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json').read()) +rec=sorted(data['recipes'],key=lambda r:r['port']); labels=[r['q'] for r in rec] +planes=json.load(open(ROOT+'research/paired-plane-port-matching-seed6c563a/CERTIFICATE.json'))['matching'] +dot=lambda a,b: bin(a&b).count('1')&1 +def rank2(rows): + rank=0; rows=list(rows) + while rows: + p=rows.pop() + if not p: continue + rank+=1; low=p&-p; rows=[r^p if r&low else r for r in rows] + return rank +K=4; U=list(range(1,1<>k&1] + for T in U: + colsQ=[quad[k] for k in range(K) if T>>k&1] + rows=[] + for p in rowsP: + for r in range(2): + v=0 + for jj,q in enumerate(colsQ): v|=G[p,q][r]<<(2*jj) + rows.append(v) + out.append(rank2(rows)) + return tuple(out) +t=time.time(); classes={} +for n,quad in enumerate(itertools.combinations(range(56),4)): + classes.setdefault(tariffs(quad),[]).append(quad) + if n%50000==0: print('done',n,len(classes),round(time.time()-t),flush=True) +pickle.dump(classes,open('quad_classes.pkl','wb')) +print('quadruples',sum(len(v) for v in classes.values()),'classes',len(classes),round(time.time()-t),flush=True) +pop=lambda x: bin(x).count('1') +weak=0; weakcls=[] +for tt,v in classes.items(): + T=dict(zip(KEYS,tt)) + c=[-2*pop(X) for X in U] + A=[[1.0 if (S&X and Tt&X) else 0.0 for X in U] for S,Tt in KEYS] + val=-linprog(c,A_ub=A,b_ub=[T[k] for k in KEYS],bounds=[(0,None)]*len(U),method='highs').fun + if val<16-1e-6: weak+=len(v); weakcls.append(tt) +pickle.dump(weakcls,open('quad_weak.pkl','wb')) +print('block-rank weak quadruples',weak,'classes',len(weakcls),round(time.time()-t),flush=True) diff --git a/research/four-plane-rank-dual/generation/quad3.py b/research/four-plane-rank-dual/generation/quad3.py new file mode 100644 index 000000000..d0ce9e691 --- /dev/null +++ b/research/four-plane-rank-dual/generation/quad3.py @@ -0,0 +1,30 @@ +import pickle, itertools, time, sys +import numpy as np +from scipy.optimize import linprog +tab=np.load('phitab4.npy') # [Z, S-1, T-1, X-1] +U=list(range(1,16)); KEYS=[(S,T) for S in U for T in U]; SINGLES=[1,2,4,8] +OFF=[(P,Q) for P in SINGLES for Q in SINGLES if P!=Q] +obj=np.array([2*bin(X).count('1') for X in U],float) +def solve(tt, masks): + b=np.array(tt,float) + A=tab[masks][:, :, :, :].transpose(1,2,0,3).reshape(225, len(masks)*15).astype(float) + c=-np.tile(obj,len(masks)) + r=linprog(c,A_ub=A,b_ub=b,bounds=(0,None),method='highs') + return -r.fun, r.x +weak=pickle.load(open('quad_weak.pkl','rb')) +CH=int(sys.argv[1]); NCH=int(sys.argv[2]); weak=weak[CH::NCH] +res={}; t=time.time(); fails=[]; full=0 +for n,tt in enumerate(weak): + T=dict(zip(KEYS,tt)) + cheap=[i for i,(P,Q) in enumerate(OFF) if T[P,Q]<=1] + masks=sorted({sum(1<1e-9] + res[tt]=(val,nz) + if val<16-1e-6: fails.append(tt) + if n%200==0: print(n,len(weak),round(time.time()-t),'full',full,'fails',len(fails),flush=True) +pickle.dump(res,open(f'quad_cert_{CH}.pkl','wb')) +print('done',len(weak),'full',full,'fails',len(fails),round(time.time()-t),flush=True) diff --git a/research/four-plane-rank-dual/verify.py b/research/four-plane-rank-dual/verify.py new file mode 100644 index 000000000..cfc1f06db --- /dev/null +++ b/research/four-plane-rank-dual/verify.py @@ -0,0 +1,171 @@ +#!/usr/bin/env python3 +"""Four-plane COPY floor under #4365's contract: exact certificates for plane quadruples. Standard library only. + +For a plane quadruple and functionals L(M) = sum_{(Z, X)} w rank(Phi_Z(M)_XX) (Phi_Z zeroes the off-diagonal plane +blocks in Z; Z empty gives the plain block-rank functional), subadditivity and the combinatorial atom bound + rank(Phi_Z(u v^T)_XX) <= min(#distinct allowed column-plane sets, #distinct allowed row-plane sets) +show that every decomposition of I_8, over any field, costs at least L(I_8) = sum w 2|X| whenever +sum w bound(S, T, X, Z) <= t(S, T) for all 225 closure pairs. Separate coordinate messages cost 16. + +The verifier recomputes the tariffs of all 367,290 quadruples from the pinned selected archive and matching, +reads one certificate index per quadruple from CERT-INDEX (0 = no certificate), and checks every referenced +certificate exactly on its class. It reports the certified count; quadruples with index 0 are open. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from fractions import Fraction as Q +import gzip +import hashlib +import io +import itertools +import json +from pathlib import Path +import sys +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +ARCHIVE = ROOT / "research/community-frontier1094-audit/selected-replay.tar.gz" +MATCHING = ROOT / "research/paired-plane-port-matching-seed6c563a/CERTIFICATE.json" +MEMBER = "candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json" +HASHES = {"archive": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6", + "matching": "4fd648f7b5178bff5441bf364d58234b7bc1a43b924bc6da03013c948f1473b1"} +K = 4 +UNIONS = list(range(1, 1 << K)) +KEYS = [(S, T) for S in UNIONS for T in UNIONS] +SINGLES = [1 << k for k in range(K)] +OFF = [(P, Q2) for P in SINGLES for Q2 in SINGLES if P != Q2] + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def pop(x): + return bin(x).count("1") + + +def dot(a, b): + return pop(a & b) & 1 + + +def rank2(rows): + rank = 0 + rows = list(rows) + while rows: + p = rows.pop() + if not p: + continue + rank += 1 + low = p & -p + rows = [r ^ p if r & low else r for r in rows] + return rank + + +def load(): + raw = ARCHIVE.read_bytes() + need(hashlib.sha256(raw).hexdigest() == HASHES["archive"], "archive hash") + with tarfile.open(fileobj=io.BytesIO(raw), mode="r:gz") as tf: + data = json.loads(tf.extractfile(MEMBER).read()) + cert = MATCHING.read_bytes() + need(hashlib.sha256(cert).hexdigest() == HASHES["matching"], "matching hash") + labels = [r["q"] for r in sorted(data["recipes"], key=lambda r: r["port"])] + planes = json.loads(cert)["matching"] + need(len(labels) == 112 and len(planes) == 56, "112 labels, 56 planes") + return labels, planes + + +def tariffs_all(labels, planes): + G = {} + for p in range(56): + for q in range(56): + G[p, q] = [sum(dot(labels[a], labels[b]) << j for j, b in enumerate(planes[q])) for a in planes[p]] + for quad in itertools.combinations(range(56), K): + out = [] + for S in UNIONS: + rp = [quad[k] for k in range(K) if S >> k & 1] + for T in UNIONS: + cq = [quad[k] for k in range(K) if T >> k & 1] + rows = [] + for p in rp: + for r in range(2): + v = 0 + for jj, q in enumerate(cq): + v |= G[p, q][r] << (2 * jj) + rows.append(v) + out.append(rank2(rows)) + yield quad, tuple(out) + + +def bound(S, T, X, Z): + rows = [P for P in SINGLES if P & S & X] + cols = [Q2 for Q2 in SINGLES if Q2 & T & X] + br = {frozenset(Q2 for Q2 in cols if (P, Q2) not in Z) for P in rows} - {frozenset()} + bc = {frozenset(P for P in rows if (P, Q2) not in Z) for Q2 in cols} - {frozenset()} + return min(len(br), len(bc)) + + + +def build_table(): + """bound(S, T, X, Z) for every zero mask Z (12 off-diagonal pairs), as a flat bytearray""" + tab = bytearray(4096 * 15 * 15 * 15) + for S in UNIONS: + for T in UNIONS: + for X in UNIONS: + rows = [P for P in SINGLES if P & S & X] + cols = [Q2 for Q2 in SINGLES if Q2 & T & X] + if not rows or not cols: + continue + rel = [i for i, (P, Q2) in enumerate(OFF) if P in rows and Q2 in cols] + base = ((S - 1) * 15 + T - 1) * 15 + X - 1 + for m in range(4096): + Z = {OFF[i] for i in rel if m >> i & 1} + br = {frozenset(Q2 for Q2 in cols if (P, Q2) not in Z) for P in rows} - {frozenset()} + bc = {frozenset(P for P in rows if (P, Q2) not in Z) for Q2 in cols} - {frozenset()} + tab[m * 3375 + base] = min(len(br), len(bc)) + return tab + + +def cert_ok(tt, cert, tab): + """exact: integer-scaled weights; tt is the 225 tariffs in KEYS order""" + den = 1 + for _, _, w in cert: + den = den * w.denominator // __import__("math").gcd(den, w.denominator) + iw = [(m * 3375, X - 1, int(w * den)) for m, X, w in cert] + for k, (S, T) in enumerate(KEYS): + base = ((S - 1) * 15 + T - 1) * 15 + if sum(w * tab[m + base + x] for m, x, w in iw) > tt[k] * den: + return False + return True + + +def main(): + certs_raw = json.loads(gzip.decompress((HERE / "CERTIFICATES.json.gz").read_bytes())) + certs = [None] + [[(mask, X, Q(w)) for mask, X, w in c] for c in certs_raw["certificates"]] + for c in certs[1:]: + need(sum(2 * pop(X) * w for m, X, w in c) == 16 and all(w > 0 and 0 <= m < 4096 for m, X, w in c), + "certificate value 16") + tab = build_table() + index = gzip.decompress((HERE / "CERT-INDEX.bin.gz").read_bytes()) + need(len(index) == 2 * 367290, "one index per quadruple") + labels, planes = load() + checked = {} + certified = open_ = 0 + for n, (quad, tt) in enumerate(tariffs_all(labels, planes)): + ci = index[2 * n] | index[2 * n + 1] << 8 + need(ci < len(certs), "index range") + if ci == 0: + open_ += 1 + continue + key = (tt, ci) + if key not in checked: + need(cert_ok(tt, certs[ci], tab), f"atom inequalities, quad {quad}") + checked[key] = True + certified += 1 + need(certified + open_ == 367290, "all quadruples") + print(json.dumps({"status": "PASS_FOUR_PLANE_RANK_DUAL", "quadruples": 367290, "certified_floor_16": certified, + "open": open_, "distinct_certificates": len(certs) - 1, "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())