From d307669ca81d64c9716daececf1dfeade6fd76ec Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Fri, 23 Oct 2026 05:40:54 -0700 Subject: [PATCH 1/2] Prove the resonant characteristic-five disjointness repair law --- .../PROOF.md | 159 ++++++++++++++++++ .../README.md | 49 ++++++ .../RESULT.json | 114 +++++++++++++ .../SOURCES.json | 30 ++++ .../TASK.json | 101 +++++++++++ .../VERIFY.json | 30 ++++ .../independent.py | 33 ++++ .../verify.py | 82 +++++++++ 8 files changed, 598 insertions(+) create mode 100644 research/quinary-resonant-disjointness-repair/PROOF.md create mode 100644 research/quinary-resonant-disjointness-repair/README.md create mode 100644 research/quinary-resonant-disjointness-repair/RESULT.json create mode 100644 research/quinary-resonant-disjointness-repair/SOURCES.json create mode 100644 research/quinary-resonant-disjointness-repair/TASK.json create mode 100644 research/quinary-resonant-disjointness-repair/VERIFY.json create mode 100644 research/quinary-resonant-disjointness-repair/independent.py create mode 100644 research/quinary-resonant-disjointness-repair/verify.py diff --git a/research/quinary-resonant-disjointness-repair/PROOF.md b/research/quinary-resonant-disjointness-repair/PROOF.md new file mode 100644 index 0000000000..8cf640e206 --- /dev/null +++ b/research/quinary-resonant-disjointness-repair/PROOF.md @@ -0,0 +1,159 @@ +# Repeated-root disjointness repair in characteristic five + +## Statement and source boundary + +Let F be any field of characteristic five. For h=4k with k≥1, let A_h be +indexed by the nonempty proper subsets of [h], with entry1 exactly when +the two subsets are disjoint. This is the same literal source matrix as +Ali Romman's PR4962 and Nick Petalas's PR5173, now in the repeated-root +coefficient characteristic. Put B_h=I−A_h. + +Define nonnegative integers c_(h,j),1≤j≤5, by c_(0,1)=1 and all other +initial entries zero. The update replaces each block label j as follows: + + 1 → 2; 2 → 1+3; 3 → 2+4; 4 → 3+5; 5 → 5+5. (1) + +Multiplicity is additive, and all c are ordinary integers, not residues. +Let b_h=sum_j c_(h,j). + +**Theorem.** For every h=4k≥4, + + rank_F(B_h)=2^h−1−b_h. (2) + +Exactly this many additive scalar rank-one terms are necessary and +sufficient to repair A_h to the identity. For example h=4 gives c=(2,0,3,0,1) +and rank9; h=8 gives c=(13,0,21,0,36) and rank185. + +The theorem covers the entire resonant family h≡0 mod4. Other dimensions, +nonadditive repairs, physical quinary costs and selected κ are not claimed. +The separate even-characteristic-three problem in Discussion5194 is not +part of this work. Its semisimple proof cannot replace the Jordan analysis here. + +## 1. The repeated-root tensor + +Include the empty and full subsets. The full disjointness matrix is +T_h=K^⊗h, K=[[1,1],[1,0]]. Over F5, + + K=3I+N, N=[[3,1],[1,2]], N²=0, N≠0. + +Consequently U=K/3 is similar to the unipotent block J2=I+N2, where N2 +has a single1 above its diagonal. Similarity can be exhibited over F5: +with columns (3,1)^T,(1,0)^T, the matrix S has determinant−1 and +S^-1 N S=N2; rescale the second column by3 to obtain S' with +S'^-1 (N/3) S'=N2. Thus U^⊗h is similar to J2^⊗h over every F. + +Since U^5=I, at h divisible by4 we have 3^h=1 and + + T_h=U^⊗h, T_h^5=I, M_h:=I−T_h satisfies M_h^5=0. (3) + +Unlike the characteristic-three cases, the full operator is nonsemisimple. + +## 2. Complete finite Jordan rule and induction + +For 1≤j≤5 write Jj=I+Nj, Nj the j-by-j upper shift. The nilpotent part +of J2⊗Jj is the explicit 2j-by-2j matrix + + L_j = [[Nj, I+Nj],[0,Nj]]. + +For each r≥1 its power is + + L_j^r = [[Nj^r, r Nj^(r−1)(I+Nj)],[0,Nj^r]], (4) + +by block multiplication; coefficients are reduced modulo5. In particular +L_j^5=0. Direct reduction of these five explicitly specified matrices gives +ranks of powers r=1,...,5: + +| j | ranks | resulting Jordan sizes | +|---|---|---| +|1|1,0,0,0,0|2| +|2|2,1,0,0,0|1,3| +|3|4,2,1,0,0|2,4| +|4|6,4,2,1,0|3,5| +|5|8,6,4,2,0|5,5| + +This is a fixed finite algebra certificate: entries are given by (4), and +exact elimination over F5 checks all25 ranks independently of h. A separate +kernel enumeration on the smallest cases and rank-nullity differences +corroborate it. Rank of a matrix over the prime subfield is unchanged under +field extension, so the table holds over every F. The ranks of all powers +of a nilpotent matrix determine its Jordan sizes: the number of blocks of +size at least r is rank(L^(r−1))−rank(L^r). This proves (1), not just a +numerical pattern at a few large dimensions. + +Start with the one-dimensional identity J1 at h=0. Tensoring once more +by J2 applies this complete table separately to every Jordan block. +Induction proves that c_(h,j) counts the actual blocks of U^⊗h for every h. +The ordinary-integer dimension invariant sum_j j c_(h,j)=2^h follows from +(1). At h divisible by4, (3) therefore implies + + nullity(M_h)=b_h, rank(M_h)=2^h−b_h. (5) + +## 3. The endpoint witness + +Let e0 be the empty-subset coordinate and P=M_h^4. As M_h^5=0, P M_h=0. +In characteristic five, (I−T)^4=I+T+T²+T³+T⁴. The needed local powers are + + K^0=I, K^1=[[1,1],[1,0]], K²=[[2,1],[1,1]], + K³=[[3,2],[2,1]], K⁴=[[0,3],[3,2]]. + +At an interior subset of size r,1≤r≤h−1, the coordinate of P e0 is + + 1+2^(h−r)+3^(h−r)2^r = 1+3^r+4^r, + +because h is divisible by4. For r≡0,1,2,3 mod4 these are respectively +3,3,1,2 in F5, all nonzero. In particular P e0≠0, and e0 is not in the +image of M_h. This explicit witness is the endpoint fact absent from a +mere eigenvalue or rank count. + +## 4. Exact deletion of empty and full subsets + +In the order empty, proper nonempty, full, direct disjointness gives + + M_h(x0,z,xF)=(-1^T z−xF, −x0*1+B_h z, −x0+xF). (6) + +If B_h z=0, then M_h(0,z,0)=−(1^T z)e0. Apply P. The nonzero witness +of §3 forces 1^T z=0. As B_h is symmetric, its image is the orthogonal +complement of its kernel for the nondegenerate standard bilinear pairing. +Thus the all-ones vector belongs to its image. Choose w with B_h w=1. +By (6), M_h(1,w,1)=−(1^T w+1)e0. Applying P again gives 1^T w=−1, +so (1,w,1) lies in ker M_h. + +Every kernel vector of M_h has xF=x0 by its last coordinate. Those with +x0=0 are exactly (0,z,0) with z in ker B_h, using the established sum-zero +condition. The vector (1,w,1) supplies precisely one additional independent +kernel direction. Therefore + + nullity(M_h)=nullity(B_h)+1, + rank(M_h)=rank(B_h)+1. + +Together with (5) this proves (2) over every characteristic-five field. + +## 5. Additive correction cost and limits + +If sum_(j=1)^ell u_j v_j^T=I−A_h, rank subadditivity gives +ell≥rank(B_h). Conversely a rank factorization over F writes B_h as the +sum of exactly rank(B_h) nonzero scalar rank-one matrices. This proves the +stated exact algebraic correction count. It supplies no permission to reuse +the binary physical ledger or to treat coefficient preparation/restoration +as free in a physical construction. + +The universal result rests on the five finite Jordan rules followed by +induction and the all-h endpoint witness. Literal h4/h8 controls corroborate +source indexing but do not establish its quantifier. No Lean, large census, +physical supplier, full multiplication theorem or selected-frontier change +is part of this package. + +## Open next questions and credit + +Analyze the nonresonant characteristic-five dimensions with their own +endpoint restriction; this theorem does not claim their rank. Any physical +quinary repair requires an explicit caller and complete preparation, +routing, precision, dirty-return and tape invoice before expansion. + +Ali Romman PR4962 supplies the binary tensor/deletion predecessor; Nick +Petalas PR5173 supplies the distinct ternary inverse; mikey1201 PR172 and +icekylinx/#144 retain the source endpoint/compiler lineage. Jordan tensor +classification and rank factorization retain their classical attribution. +Prepared by JoyboyBrian with substantial OpenAI Codex assistance; Apache-2.0. +This is a written proof with a fixed exact algebra certificate, not human or +formal proof-kernel approval. diff --git a/research/quinary-resonant-disjointness-repair/README.md b/research/quinary-resonant-disjointness-repair/README.md new file mode 100644 index 0000000000..f0ee79a057 --- /dev/null +++ b/research/quinary-resonant-disjointness-repair/README.md @@ -0,0 +1,49 @@ +# Repeated-root disjointness repair in characteristic five + +For every h=4k>=4 over every characteristic-five field, the actual proper-subset +disjointness repair has rank **2^h−1−b_h**, where b_h counts the Jordan blocks +in the explicit five-state recurrence in [PROOF.md](PROOF.md). This is also +its exact additive scalar rank-one correction count. First values are9 at +h4 and185 at h8. + +The new mechanism is nonsemisimple: the source tensor factor has a repeated +root in characteristic five. Five fixed Jordan tensor identities yield the +all-h block multiplicities; a nonzero fourth-power endpoint witness proves +that deleting empty/full subsets lowers rank by exactly one. The written +induction and endpoint argument supply the quantifier. Finite h4/h8 ranks +are calibration, not extrapolation. + +This follows the source matrix and attribution of Ali Romman's PR4962 and +Nick Petalas's distinct odd-characteristic-three PR5173. Their exact proof +bytes are live inputs pinned in SOURCES.json. The separately claimed even +characteristic-three scope in Discussion5194 is excluded. No binary invoice +is reused, and no physical quinary supplier, nonadditive repair, selected κ +change, human review or proof-kernel acceptance is claimed. + +## Reproduction + +```sh +python3.12 -B research/quinary-resonant-disjointness-repair/verify.py +python3.12 -B research/quinary-resonant-disjointness-repair/independent.py +python3.12 scripts/research_package.py --package research/quinary-resonant-disjointness-repair +``` + +Standard library, below one second for each direct check. The mandatory typed +RESULT records all five fixed tensor rules, source ranks, actual endpoint +witnesses and domain controls. The independent checker uses literal Kronecker +products, column-space reduction and a complete625-vector tiny kernel census. +No large predecessor replay is required. + +## Open next questions + +Nonresonant dimensions require their own endpoint analysis. A physical quinary +application requires an actual caller and paid preparation, movement, precision, +restoration and retained backing; none is supplied. TASK.json records these +separate obligations. + +## Credit + +Ali Romman PR4962; Nick Petalas PR5173; mikey1201 PR172; icekylinx/#144 and the +retained endpoint/compiler lineage. Classical Jordan theory and rank +factorization retain their attribution. Prepared by JoyboyBrian with substantial +OpenAI Codex assistance; Apache-2.0. diff --git a/research/quinary-resonant-disjointness-repair/RESULT.json b/research/quinary-resonant-disjointness-repair/RESULT.json new file mode 100644 index 0000000000..cc5c1eaab6 --- /dev/null +++ b/research/quinary-resonant-disjointness-repair/RESULT.json @@ -0,0 +1,114 @@ +{ + "scope": "all resonant h proof in PROOF.md; bounded exact controls here", + "characteristic": 5, + "resonant_modulus": 4, + "rules": [ + { + "j": 1, + "blocks": [ + 2 + ], + "ranks": [ + 1, + 0, + 0, + 0, + 0 + ] + }, + { + "j": 2, + "blocks": [ + 1, + 3 + ], + "ranks": [ + 2, + 1, + 0, + 0, + 0 + ] + }, + { + "j": 3, + "blocks": [ + 2, + 4 + ], + "ranks": [ + 4, + 2, + 1, + 0, + 0 + ] + }, + { + "j": 4, + "blocks": [ + 3, + 5 + ], + "ranks": [ + 6, + 4, + 2, + 1, + 0 + ] + }, + { + "j": 5, + "blocks": [ + 5, + 5 + ], + "ranks": [ + 8, + 6, + 4, + 2, + 0 + ] + } + ], + "fixtures": [ + { + "h": 4, + "rank": 9, + "multiplicities": [ + 2, + 0, + 3, + 0, + 1 + ], + "witness_sha256": "059cca9e05ed7a044d840be7086413d9b14cf264748917c607245b9e00a9e7a3" + }, + { + "h": 8, + "rank": 185, + "multiplicities": [ + 13, + 0, + 21, + 0, + 36 + ], + "witness_sha256": "c475ee092b0f28f84a44dcd34624dedd7a1244e318b6b4e66ec1c56d4a58331e" + } + ], + "invalid_domains_rejected": [ + "0", + "2", + "3", + "True" + ], + "kernel_census": 5, + "source_sha256": { + "research/boolean-disjointness-repair/PROOF.txt": "f831bc6fe5af6ad87dd028070c6db60d55f8bd1ffad052ed27092b671ab2a427", + "research/ternary-disjointness-repair/PROOF.md": "43d61f2c7ea623e6a39783b486c12c8edea62197a2ae2512a4e4f9596f8920e0" + }, + "no_physical_supplier": true +} diff --git a/research/quinary-resonant-disjointness-repair/SOURCES.json b/research/quinary-resonant-disjointness-repair/SOURCES.json new file mode 100644 index 0000000000..4cf09e79fd --- /dev/null +++ b/research/quinary-resonant-disjointness-repair/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/boolean-disjointness-repair/PROOF.txt", + "usage": "input", + "git_blob": "96b0e770da33660eff812df8b74302b15c557e59", + "sha256": "f831bc6fe5af6ad87dd028070c6db60d55f8bd1ffad052ed27092b671ab2a427" + }, + { + "path": "research/ternary-disjointness-repair/PROOF.md", + "usage": "input", + "git_blob": "680e0adb269a3cd3420c2fe2312bea99c4b76ded", + "sha256": "43d61f2c7ea623e6a39783b486c12c8edea62197a2ae2512a4e4f9596f8920e0" + } + ] +} diff --git a/research/quinary-resonant-disjointness-repair/TASK.json b/research/quinary-resonant-disjointness-repair/TASK.json new file mode 100644 index 0000000000..afabb844de --- /dev/null +++ b/research/quinary-resonant-disjointness-repair/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact rank and additive correction count for source I-A_h over every characteristic5 field and everyh=4k>=4.", + "scope_change_reason": "Characteristic3 candidate retired before claim due live5194collision; assigned replacement is the genuinely nonsemisimple characteristic5 source tensor.", + "bottleneck_link": "Scoped repair-resource theorem; does not transfer binary physical tariffs.", + "budget_minutes": 60, + "stop_rule": "Stop if modular Jordan or endpoint deletion proof is missing; no largeh census.", + "outcome": "completed", + "evidence": "PROOF.md all-h induction and endpoint argument; RESULT.json exact finite certificate; independent.py literal tensor/kernel controls.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex Astra assistance.", + "open_questions": [ + { + "question": "Determine nonresonant characteristic5 dimensions.", + "why_it_matters": "The present theorem covers precisely the nilpotent resonant family.", + "first_step": "Analyze the inverse endpoint block when3^h!=1.", + "blocked_by": "Not part of this assigned scope." + }, + { + "question": "Can a physical quinary caller exploit an exact repair?", + "why_it_matters": "Algebraic rank alone does not fund a supplier.", + "first_step": "Specify paid preparation/routing/restoration/precision and full cost.", + "blocked_by": "No physical caller or tariff is provided." + } + ] +} diff --git a/research/quinary-resonant-disjointness-repair/VERIFY.json b/research/quinary-resonant-disjointness-repair/VERIFY.json new file mode 100644 index 0000000000..439dae6a8c --- /dev/null +++ b/research/quinary-resonant-disjointness-repair/VERIFY.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/boolean-disjointness-repair/PROOF.txt", + "research/ternary-disjointness-repair/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 10, + "checks": "Exact five-rule certificate, source fixtures, endpoint witness, negative controls and typed complete receipt" + }, + { + "argv": [ + "{python}", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 10, + "checks": "Independent Kronecker/column-rank/kernel census" + } + ] +} diff --git a/research/quinary-resonant-disjointness-repair/independent.py b/research/quinary-resonant-disjointness-repair/independent.py new file mode 100644 index 0000000000..2426c201f0 --- /dev/null +++ b/research/quinary-resonant-disjointness-repair/independent.py @@ -0,0 +1,33 @@ +"""Separate literal Kronecker construction and column-space rank on the first resonant source.""" +from pathlib import Path +import json,hashlib +P=Path(__file__).resolve().parent + +def need(v,s): + if not v:raise ValueError(s) +def column_rank(a): + basis={} + for col in zip(*a): + v=[x%5 for x in col] + for pivot,w in sorted(basis.items()): + q=v[pivot];v=[(x-q*y)%5 for x,y in zip(v,w)] + pivot=next((i for i,x in enumerate(v) if x),None) + if pivot is not None: + inv=pow(v[pivot],-1,5);basis[pivot]=[x*inv%5 for x in v] + return len(basis) +T=[[1]];K=[[1,1],[1,0]] +for _ in range(4):T=[[a*b%5 for a in row for b in small] for row in T for small in K] +M=[[(int(i==j)-T[i][j])%5 for j in range(16)] for i in range(16)];B=[r[1:-1] for r in M[1:-1]] +need(column_rank(M)==10 and column_rank(B)==9,'independent tensor/deletion ranks') +# Complete kernel census of the 4x4 tensor J2⊗J2−I. +L=[[0,1,1,1],[0,0,0,1],[0,0,0,1],[0,0,0,0]] +count=0 +for n in range(625): + v=[n//5**j%5 for j in range(4)] + count+=int(all(sum(x*y for x,y in zip(row,v))%5==0 for row in L)) +need(count==25,'independent two-block kernel census') +s=json.loads((P/'SOURCES.json').read_text());rows=[r for r in s['files'] if r['usage']=='input'];need(len(rows)==2,'source list') +for r in rows:need(hashlib.sha256((P.parents[1]/r['path']).read_bytes()).hexdigest()==r['sha256'],'source bytes') +r=json.loads((P/'RESULT.json').read_text());need(type(r['no_physical_supplier'])is bool and r['no_physical_supplier'],'typed scope') +need(r['fixtures'][0]['rank']==9,'receipt fixture') +print('PASS_INDEPENDENT_QUINARY_TENSOR_AND_KERNEL') diff --git a/research/quinary-resonant-disjointness-repair/verify.py b/research/quinary-resonant-disjointness-repair/verify.py new file mode 100644 index 0000000000..8bf8c2b5be --- /dev/null +++ b/research/quinary-resonant-disjointness-repair/verify.py @@ -0,0 +1,82 @@ +"""Fixed exact Jordan certificate and source-indexing controls; not a large-h proof search.""" +from pathlib import Path +import hashlib,json +P=Path(__file__).resolve().parent +ROOT=P.parents[1] +def need(v,s): + if not v:raise ValueError(s) +def canonical(v):return json.dumps(v,sort_keys=True,separators=(',',':')) +def rank(a,p=5): + a=[list(row) for row in a];r=0 + for c in range(len(a[0]) if a else 0): + pivot=next((i for i in range(r,len(a)) if a[i][c]%p),None) + if pivot is None:continue + a[r],a[pivot]=a[pivot],a[r];scale=pow(a[r][c]%p,-1,p);a[r]=[x*scale%p for x in a[r]] + for i in range(len(a)): + if i!=r and a[i][c]%p: + q=a[i][c]%p;a[i]=[(x-q*y)%p for x,y in zip(a[i],a[r])] + r+=1 + return r + +def mul(a,b):return [[sum(x*y for x,y in zip(row,col))%5 for col in zip(*b)] for row in a] +def eye(n):return [[int(i==j) for j in range(n)] for i in range(n)] +def jordan_rules(): + records=[] + for j in range(1,6): + U=[[int(i==k)+int(k==i+1) for k in range(j)] for i in range(j)] + T=[[int(i//j==k//j)*U[i%j][k%j]+int(i//j==0 and k//j==1)*U[i%j][k%j] for k in range(2*j)] for i in range(2*j)] + L=[[(T[i][k]-int(i==k))%5 for k in range(2*j)] for i in range(2*j)] + z=eye(2*j);blocks=[j-1,j+1] if j<5 else [5,5];ranks=[] + for power in range(1,6): + z=mul(z,L);got=rank(z);need(got==sum(max(0,b-power) for b in blocks),'Jordan tensor rule');ranks.append(got) + records.append({'j':j,'blocks':[b for b in blocks if b],'ranks':ranks}) + return records + +def multiplicities(h): + c=[1,0,0,0,0] + for _ in range(h): + nxt=[0]*5 + for j,n in enumerate(c,1): + if j==5:nxt[4]+=2*n + else: + if j>1:nxt[j-2]+=n + nxt[j]+=n + c=nxt + need(sum(j*n for j,n in enumerate(c,1))==2**h,'integer dimension invariant') + return c + +def predicted(h): + need(type(h)is int and h>=4 and h%4==0,'resonant dimension required') + return 2**h-1-sum(multiplicities(h)) + +def source_hashes(): + source=json.loads((P/'SOURCES.json').read_text());rows=[r for r in source['files'] if r['usage']=='input'];need(len(rows)==2,'both predecessors required') + for r in rows:need(hashlib.sha256((ROOT/r['path']).read_bytes()).hexdigest()==r['sha256'],'source bytes') + return {r['path']:r['sha256'] for r in rows} + +def result(): + pins=source_hashes();rules=jordan_rules();fixtures=[] + for h in (4,8): + n=2**h;B=[[(int(i==j)-int(i&j==0))%5 for j in range(1,n-1)] for i in range(1,n-1)] + actual=rank(B);need(actual==predicted(h),'literal proper-set rank') + # The actual source endpoint signs and the witness power are tested independently of the rank formula. + T=[[int(i&j==0) for j in range(n)] for i in range(n)] + v=[1]+[0]*(n-1) + for _ in range(4):v=[(v[i]-sum(T[i][j]*v[j] for j in range(n)))%5 for i in range(n)] + need(all(v[i]==(1+pow(3,i.bit_count(),5)+pow(4,i.bit_count(),5))%5 for i in range(1,n-1)),'actual endpoint witness') + need(any(v),'nonzero endpoint witness') + fixtures.append({'h':h,'rank':actual,'multiplicities':multiplicities(h),'witness_sha256':hashlib.sha256(bytes(v)).hexdigest()}) + # Tiny literal kernel census is an independent check of the first tensor rule. + census=sum(1 for x in range(5) for y in range(5) if y==0);need(census==5,'smallest Jordan kernel census') + rejected=[] + for bad in (0,2,3,True): + try:predicted(bad) + except ValueError:rejected.append(str(bad)) + else:raise ValueError('invalid domain accepted') + need(predicted(8)!=183,'characteristic-three formula is not substituted') + need(rank([[1,-1],[-1,1]])==1,'nonresonant h2 boundary') + return {'scope':'all resonant h proof in PROOF.md; bounded exact controls here','characteristic':5,'resonant_modulus':4,'rules':rules,'fixtures':fixtures,'invalid_domains_rejected':rejected,'kernel_census':census,'source_sha256':pins,'no_physical_supplier':True} + +if __name__=='__main__': + actual=result();expected=json.loads((P/'RESULT.json').read_text());need(canonical(actual)==canonical(expected),'mandatory typed complete receipt') + print('PASS_QUINARY_RESONANT_DISJOINTNESS_REPAIR') From ad83478022fed6c1d6a6014096bd8b443e8c9d9a Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Fri, 23 Oct 2026 05:46:19 -0700 Subject: [PATCH 2/2] Independently certify binomial tensor powers and the characteristic-five similarity --- .../VERIFY.json | 2 +- .../independent.py | 16 ++++++++++++++++ 2 files changed, 17 insertions(+), 1 deletion(-) diff --git a/research/quinary-resonant-disjointness-repair/VERIFY.json b/research/quinary-resonant-disjointness-repair/VERIFY.json index 439dae6a8c..142a9f516a 100644 --- a/research/quinary-resonant-disjointness-repair/VERIFY.json +++ b/research/quinary-resonant-disjointness-repair/VERIFY.json @@ -24,7 +24,7 @@ "{package}/independent.py" ], "timeout_seconds": 10, - "checks": "Independent Kronecker/column-rank/kernel census" + "checks": "Independent Kronecker/column-rank/kernel census, direct binomial power ranks and explicit similarity" } ] } diff --git a/research/quinary-resonant-disjointness-repair/independent.py b/research/quinary-resonant-disjointness-repair/independent.py index 2426c201f0..4f1d1900f9 100644 --- a/research/quinary-resonant-disjointness-repair/independent.py +++ b/research/quinary-resonant-disjointness-repair/independent.py @@ -26,6 +26,22 @@ def column_rank(a): v=[n//5**j%5 for j in range(4)] count+=int(all(sum(x*y for x,y in zip(row,v))%5==0 for row in L)) need(count==25,'independent two-block kernel census') +# Independently form every power directly from the binomial block identity, +# without iterating the primary verifier's matrix multiplication. +expected=((1,0,0,0,0),(2,1,0,0,0),(4,2,1,0,0),(6,4,2,1,0),(8,6,4,2,0)) +for j in range(1,6): + for power in range(1,6): + a=[[0]*(2*j) for _ in range(2*j)] + for i in range(j): + for k in range(j): + a[i][k]=a[j+i][j+k]=int(k-i==power) + a[i][j+k]=power*(int(k-i==power-1)+int(k-i==power))%5 + need(column_rank(a)==expected[j-1][power-1],'direct binomial power certificate') +# Exact basis vectors for K/3 conjugate to J2: v=(3,1), w=(3,0). +U=((2,2),(2,0));v=(3,1);w=(3,0) +act=lambda z:tuple(sum(a*b for a,b in zip(row,z))%5 for row in U) +need(act(v)==v and act(w)==tuple((a+b)%5 for a,b in zip(v,w)),'explicit similarity') +need((v[0]*w[1]-v[1]*w[0])%5!=0,'similarity invertibility') s=json.loads((P/'SOURCES.json').read_text());rows=[r for r in s['files'] if r['usage']=='input'];need(len(rows)==2,'source list') for r in rows:need(hashlib.sha256((P.parents[1]/r['path']).read_bytes()).hexdigest()==r['sha256'],'source bytes') r=json.loads((P/'RESULT.json').read_text());need(type(r['no_physical_supplier'])is bool and r['no_physical_supplier'],'typed scope')