From f1b590e74c2401c465416403d426597202b136ec Mon Sep 17 00:00:00 2001 From: Thiago Maceno Rocha Goulart Date: Wed, 14 Oct 2026 05:28:08 -0300 Subject: [PATCH 1/3] Prove P112 fitting rank nine over all characteristic-two fields --- .../p112-characteristic-two-minrank/README.md | 184 ++++++++++++++++++ .../SOURCES.json | 24 +++ .../p112-characteristic-two-minrank/TASK.json | 89 +++++++++ .../VERIFIED.json | 178 +++++++++++++++++ .../VERIFY.json | 22 +++ .../p112-characteristic-two-minrank/verify.py | 158 +++++++++++++++ 6 files changed, 655 insertions(+) create mode 100644 research/p112-characteristic-two-minrank/README.md create mode 100644 research/p112-characteristic-two-minrank/SOURCES.json create mode 100644 research/p112-characteristic-two-minrank/TASK.json create mode 100644 research/p112-characteristic-two-minrank/VERIFIED.json create mode 100644 research/p112-characteristic-two-minrank/VERIFY.json create mode 100644 research/p112-characteristic-two-minrank/verify.py diff --git a/research/p112-characteristic-two-minrank/README.md b/research/p112-characteristic-two-minrank/README.md new file mode 100644 index 0000000000..36103adfbe --- /dev/null +++ b/research/p112-characteristic-two-minrank/README.md @@ -0,0 +1,184 @@ +# P112 fitting rank is nine in every characteristic-two field + +For the pinned 112-port graph, **every matrix with nonzero diagonal and zeros +on the required pairs has rank at least nine over every field of characteristic +two**, finite or infinite. Symmetry is not assumed. The existing binary labels +give the matching upper bound. Six eight-cliques on just 17 vertices certify the +lower bound. The same induced 17-vertex graph therefore has minimum rank nine. + +This is a scoped obstruction to a rank-eight label replacement. It supplies no +new circuit, helper inventory, multiplication theorem or improved exponent. + +## Exact object and graph convention + +Use root_lines[8:] and binary_ports[8:] from +[PROTOTYPE.json](../direct-delivery504-global/inputs/hamming/PROTOTYPE.json). +The removed first eight roots are exactly twice the coordinate vectors. The +remaining roots are integer vectors in eight dimensions, of squared norm four; +their distinct-pair dot products are in {-2,0,2}. + +Indices below are zero-based **after** removing the first eight rows. Put an +edge between distinct indices i and j exactly when their integer root dot +product is nonzero. These are the 2,912 unordered **required-zero** pairs. +A fitting matrix here has M_ii nonzero and M_ij = M_ji = 0 on each such pair; +all other off-diagonal entries are free. + +Some Haemers-bound literature instead calls a matrix fitting when its zeros +are on graph nonedges. Our required-zero graph is the complement of the +corresponding induced E8 orthogonality graph. This convention matters. + +The exact source commit is 0b1cccf86e2f5132ed286a26ef0a681a495740ea. +The input SHA256 is +327d2a868043e846381aa58a33053c24425e8cad522ff401b10ec8af1d649a3f. +[SOURCES.json](SOURCES.json) also pins the Git blob and historical catalogue and +selected record. Those provenance files are not changed by this package. + +## Six-clique certificate + +Each row is an eight-clique in the required-zero graph: + +~~~text +C1 = 0, 8, 9, 24, 32, 56, 64, 88 +C2 = 0, 8, 16, 24, 32, 40, 56, 57 +C3 = 1, 8, 9, 24, 33, 56, 65, 88 +C4 = 1, 8, 17, 24, 25, 56, 65, 72 +C5 = 1, 8, 17, 24, 33, 40, 56, 57 +C6 = 0, 8, 16, 24, 25, 56, 64, 72 +~~~ + +Their union has 17 vertices and 106 induced required-zero pairs. In the six +rows, exactly vertices 0 and 1 occur an odd number of times. They are adjacent. +These elementary integer facts are all the finite input needed for the lower +bound. + +## Proof for arbitrary fitting matrices + +Let F be any field of characteristic two and M any fitting matrix. Multiplying +each row by the inverse of its diagonal entry preserves rank and required +zeros, so assume M_ii = 1. Every eight-clique gives an identity principal +submatrix, hence rank(M) is at least eight. + +Suppose rank(M) = 8 and factor M = U V^T, where U and V have eight columns. +Write their i-th rows as u_i and v_i. For each displayed clique C, + +~~~text +U_C V_C^T = I_8, so V_C^T U_C = I_8. +~~~ + +Thus the rank-one matrices P_i = v_i^T u_i sum to I_8 on each clique. +Sum all six equations. Characteristic two cancels their right sides and every +even-incidence P_i, leaving P_0 = P_1. Multiplication on the left by u_0 and +on the right by v_0^T gives + +~~~text +1 = (u_0 v_0^T)^2 = u_0 P_0 v_0^T + = u_0 P_1 v_0^T = (u_0 v_1^T)(u_1 v_0^T) = M_01 M_10 = 0. +~~~ + +This contradiction proves rank(M) at least nine without assuming symmetry, +a Gram representation or a finite field. The argument uses only the displayed +17 vertices. + +For the upper bound, decode each retained binary label as a vector b_i in +F_2^9. The checker verifies odd self-dot product and zero dot product on every +required pair, as well as the complete Gram identity + +~~~text +b_i . b_j = 1 + (root_i . root_j)/2 (mod 2). +~~~ + +Consequently their binary Gram matrix is a fitting matrix of rank at most +nine over every characteristic-two field. The checker also computes rank nine +for that matrix and verifies that the 17 retained labels span nine dimensions. +Together with the lower bound this proves the claimed equality for both graphs. + +## Block-rank corollary and its limit + +For d-by-d blocks, suppose M_ii = I_d and M_ij = M_ji = 0 on all required +pairs. Write r = rank(M) and factor its blocks as M_ij = U_i V_j, with U_i of +size d by r and V_i of size r by d. Each P_i = V_i U_i is a rank-d idempotent. +On an eight-clique the P_i are pairwise mutually annihilating, so their sum +S_C is an idempotent of rank 8d. Therefore E_C = I_r - S_C has rank r - 8d. + +The same six-clique cancellation gives P_0 + P_1 = sum_C E_C. Since P_0 and +P_1 are mutually annihilating rank-d idempotents, their sum has rank 2d. +Rank subadditivity gives + +~~~text +2d <= 6(r - 8d), hence r >= ceil(25d/3). +~~~ + +Invertible diagonal blocks can be normalized first. This is a human proof of +a normalized block-rank lower bound of 25/3; it does **not** prove a fractional +minimum of nine or rule out every block-valued interface. The finite checker +verifies the common clique certificate, not a formalization of the rank lemmas. + +## Reproduce and coverage + +From the repository root, with Python 3.12 and no external dependencies: + +~~~sh +python3.12 scripts/research_package.py --package research/p112-characteristic-two-minrank --check-only +python3.12 scripts/research_package.py --package research/p112-characteristic-two-minrank +~~~ + +The registered replay runs verify.py with -I -B -O. Every acceptance check +uses an explicit exception and remains active with assertions disabled. The +script rewrites the deterministic [VERIFIED.json](VERIFIED.json) receipt. + +The independently written verifier imports no search program or producer. +It checks the exact input hash, source indexing, every clique edge and incidence, +the scalar sandwich reduction, all 2,912 required-zero pairs, all 12,544 binary +Gram entries, and the rank-nine upper construction. Seven negative controls +alter source bytes, a clique vertex, the clique count, the edge convention, +an upper label's diagonal, an upper label while preserving odd norm, and the +label dimension. All seven must be rejected. + +The universal field statements follow from the proof above; a finite solver +search is neither needed nor used in this replay. No full supplier or selected +frontier replay is claimed. This is not a Lean formalization. + +## Overlap, relevance and attribution + +[Discussion 1713](https://github.com/CrocSwap/integer-mult-bounds/discussions/1713) +records the finding and its strengthening from symmetric representations to +arbitrary fitting matrices. The complete remote overlap refresh on +2026-10-14 at 08:19 UTC covered 418 open PRs and 371 Discussions, including +comments and replies. Local overlap coverage was limited by this sparse +checkout. [PR1471](https://github.com/CrocSwap/integer-mult-bounds/pull/1471), +head 3695ad16e7bc4c0f6248a9e5a64fc069fa096733, audits the odd-characteristic +portability of a particular P112 tensor proof. The present theorem instead +bounds every fitting matrix in characteristic two. An overlap search does not +establish novelty, and no priority claim is made here. + +The rank-nine upper construction is known: Debbie Leung, Laura Mancinska, +William Matthews, Maris Ozols and Aidan Roy, +[Entanglement can increase asymptotic rates of zero-error classical communication over classical channels](https://arxiv.org/abs/1009.1195), +Theorem 9 and section 4, explain the binary symplectic upper bound and the E8 +embedding, crediting Peeters for the symplectic-graph result. We credit that +literature rather than treating the inherited labels as a new construction. +The contribution here is the explicit six-clique lower certificate, its +source binding and the independently replayable checks; no literature-wide +novelty claim for the underlying rank obstruction is asserted. + +The concrete input is retained from icekylinx's +[direct-delivery504-global](../direct-delivery504-global/README.md) package, +prepared with OpenAI GPT-6 Astra assistance. Its Hamming/root inputs descend +from the PR523/514/507/425/433 lineage credited in that package's +[NOTICE.md](../direct-delivery504-global/NOTICE.md) and source ancestry. This +package references the existing input without modifying or re-vendoring it. + +Prepared for Thiago with substantial OpenAI GPT-6 Astra and Codex assistance +for exploration, proof review, independent checking and packaging. New work +is Apache-2.0; retained source attribution and licenses remain applicable. + +## Open next questions + +Can a changed graph or a genuinely block-valued interface improve a complete +paid supplier budget? The fixed scalar rank-eight premise is closed, but the +block corollary leaves a gap between 25/3 and nine. A useful first step is to +write the changed constraints and an optimistic complete paid budget before +building a circuit. The missing native word, restoration/phase proof and +global owner invoice are the current blockers. [TASK.json](TASK.json) records +this question and explicitly labels this package as a side result of the +helper-inventory investigation. diff --git a/research/p112-characteristic-two-minrank/SOURCES.json b/research/p112-characteristic-two-minrank/SOURCES.json new file mode 100644 index 0000000000..06ada17171 --- /dev/null +++ b/research/p112-characteristic-two-minrank/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/direct-delivery504-global/inputs/hamming/PROTOTYPE.json", + "usage": "input", + "git_blob": "9efe30ee107b9c67f15f1c726e1a1cb5cef03929", + "sha256": "327d2a868043e846381aa58a33053c24425e8cad522ff401b10ec8af1d649a3f" + } + ] +} diff --git a/research/p112-characteristic-two-minrank/TASK.json b/research/p112-characteristic-two-minrank/TASK.json new file mode 100644 index 0000000000..3db0aaa7ab --- /dev/null +++ b/research/p112-characteristic-two-minrank/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "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": [ + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json" + ], + "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.", + "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." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the minimum rank of arbitrary, possibly asymmetric fitting matrices for the pinned P112 required-zero graph over every characteristic-two field, with an explicit small certificate and independent checker.", + "scope_change_reason": "The constructive helper-inventory investigation raised a necessary rank-eight label premise. This package isolates its exact obstruction as a side result; it does not supply a changed helper inventory.", + "bottleneck_link": "Excludes replacing the fixed P112 nine-coordinate fitting labels by eight coordinates over any characteristic-two extension field, even with different source and target labels. Changed graphs, block interfaces, and complete suppliers require separate work; no kappa improvement follows.", + "budget_minutes": 75, + "stop_rule": "Stop this side-result investigation after a source-pinned finite certificate, an elementary proof over every characteristic-two field, independent replay and explicit scope/attribution checks.", + "outcome": "completed", + "evidence": "Six eight-cliques use 17 vertices and have odd incidence exactly at adjacent vertices 0 and 1. The independent standard-library verifier checks all 2912 required-zero pairs, the complete binary Gram matrix, rank-nine upper bounds, the symbolic scalar contradiction and seven corruption controls. README gives the universal proof and a separately reviewed block-rank corollary.", + "author": "Thiago, with OpenAI GPT-6 Astra and Codex assistance", + "ai_assistance": "Substantial OpenAI GPT-6 Astra and Codex assistance was used for mathematical exploration, independent checking, literature search, implementation and packaging.", + "open_questions": [ + { + "question": "Can a changed port graph or genuinely block-valued label interface improve a complete paid supplier budget?", + "why_it_matters": "The scalar rank-eight premise for this exact graph is closed. The block corollary gives only normalized rank at least 25/3, not nine, and does not price a supplier.", + "first_step": "Write the changed graph or block constraints and derive a complete optimistic paid budget before constructing a circuit.", + "blocked_by": "No compatible native word, restoration/phase proof or global owner invoice for such a changed interface is supplied here." + } + ], + "coordination": { + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1713", + "overlap_checked_at": "2026-10-14T08:19:31.840748+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T08:18:08.249593+00:00", + "complete_pagination": true, + "records": 418 + }, + "discussions": { + "fetched_at": "2026-10-14T08:19:31.759476+00:00", + "complete_pagination": true, + "records": 371 + } + }, + "nearest_overlap": { + "pr": 1471, + "head": "3695ad16e7bc4c0f6248a9e5a64fc069fa096733", + "difference": "PR1471 audits odd-characteristic portability of a pinned P112 tensor argument; this package proves a lower bound for all fitting matrices over every characteristic-two field." + } + }, + "prior_art": [ + { + "url": "https://arxiv.org/abs/1009.1195", + "description": "Leung, Mancinska, Matthews, Ozols and Roy, Theorem 9 and section 4: known rank-nine symplectic upper construction; graph convention explained in README." + } + ] +} diff --git a/research/p112-characteristic-two-minrank/VERIFIED.json b/research/p112-characteristic-two-minrank/VERIFIED.json new file mode 100644 index 0000000000..275d387b9b --- /dev/null +++ b/research/p112-characteristic-two-minrank/VERIFIED.json @@ -0,0 +1,178 @@ +{ + "status": "PASS_INDEPENDENT_GENERAL_CHAR2_MINIMUM_FITTING_RANK_NINE", + "source_sha256": "327d2a868043e846381aa58a33053c24425e8cad522ff401b10ec8af1d649a3f", + "source_vertex_offset": 8, + "vertices": 112, + "required_zero_unordered_edges": 2912, + "symmetric_matrix_assumed": false, + "diagonal_normalization": "left multiply by diag(M_ii^-1); preserves rank and every required zero", + "factor_orientation": "M_ij=u_i*v_j^T; P_i=v_i^T*u_i; U_C*V_C^T=I implies V_C^T*U_C=I", + "certificate_vertices": [ + 0, + 1, + 8, + 9, + 16, + 17, + 24, + 25, + 32, + 33, + 40, + 56, + 57, + 64, + 65, + 72, + 88 + ], + "cliques": [ + [ + 0, + 8, + 9, + 24, + 32, + 56, + 64, + 88 + ], + [ + 0, + 8, + 16, + 24, + 32, + 40, + 56, + 57 + ], + [ + 1, + 8, + 9, + 24, + 33, + 56, + 65, + 88 + ], + [ + 1, + 8, + 17, + 24, + 25, + 56, + 65, + 72 + ], + [ + 1, + 8, + 17, + 24, + 33, + 40, + 56, + 57 + ], + [ + 0, + 8, + 16, + 24, + 25, + 56, + 64, + 72 + ] + ], + "incidence_counts": { + "0": 3, + "1": 3, + "8": 6, + "9": 2, + "16": 2, + "17": 2, + "24": 6, + "25": 2, + "32": 2, + "33": 2, + "40": 2, + "56": 6, + "57": 2, + "64": 2, + "65": 2, + "72": 2, + "88": 2 + }, + "residual_vertices": [ + 0, + 1 + ], + "induced_required_zero_edges": 106, + "symbolic_sandwich_residual": "1=0", + "upper_dimension": 9, + "upper_basis_vertex_indices": [ + 0, + 1, + 2, + 4, + 8, + 9, + 16, + 24, + 56 + ], + "induced_upper_basis_vertex_indices": [ + 0, + 1, + 8, + 9, + 16, + 24, + 25, + 56, + 57 + ], + "field_scope": "Every field of characteristic two, finite or infinite; no symmetry assumption.", + "corruption_controls": [ + { + "control": "source byte changed", + "outcome": "REJECTED", + "reason": "source SHA-256 mismatch" + }, + { + "control": "clique vertex changed", + "outcome": "REJECTED", + "reason": "clique requires zeros on BOTH directed off-diagonal matrix entries" + }, + { + "control": "one clique omitted", + "outcome": "REJECTED", + "reason": "six clique equations" + }, + { + "control": "edge convention reversed", + "outcome": "REJECTED", + "reason": "clique requires zeros on BOTH directed off-diagonal matrix entries" + }, + { + "control": "upper diagonal corrupted", + "outcome": "REJECTED", + "reason": "nonzero diagonal in the binary Gram matrix" + }, + { + "control": "upper label changed with odd norm preserved", + "outcome": "REJECTED", + "reason": "all required directed zeros" + }, + { + "control": "upper labels truncated to eight coordinates", + "outcome": "REJECTED", + "reason": "nonzero diagonal in the binary Gram matrix" + } + ], + "scope": "Exact finite certificate and elementary field-independent proof; no novelty, native circuit, or exponent claim." +} diff --git a/research/p112-characteristic-two-minrank/VERIFY.json b/research/p112-characteristic-two-minrank/VERIFY.json new file mode 100644 index 0000000000..17e69440ab --- /dev/null +++ b/research/p112-characteristic-two-minrank/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/direct-delivery504-global/inputs/hamming/PROTOTYPE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Pinned P112 input, six-clique scalar-rank certificate, all required zeros, full binary Gram matrix and rank-nine upper bounds, seven corruption controls. The general-field and block-rank arguments are human proofs in README." + } + ] +} diff --git a/research/p112-characteristic-two-minrank/verify.py b/research/p112-characteristic-two-minrank/verify.py new file mode 100644 index 0000000000..c12575b62c --- /dev/null +++ b/research/p112-characteristic-two-minrank/verify.py @@ -0,0 +1,158 @@ +"""Prepared for Thiago with OpenAI GPT-6 Astra and Codex assistance. Apache-2.0. + +Independent exact audit of the pinned P112 characteristic-two certificate. + +Only the Python standard library is used. This module imports no producer, +search code, or other verifier. The source supplies integer roots and binary +upper-bound labels; the six displayed clique lists are certificate data. + +Proof over ANY field K of characteristic two: row-normalize a fitting matrix +to M_ii=1. An eight-clique gives rank(M)>=8. If rank(M)=8, factor M=U V^T. +For every eight-clique C, U_C V_C^T=I_8, hence V_C^T U_C=I_8. Thus the +outer products P_i=v_i^T u_i sum to I_8 on C, without assuming symmetry. +The six clique equations have even right-hand side and odd incidence only +at 0 and 1. Consequently P_0=P_1. Sandwiching with u_0 and v_0^T gives +1=M_00^2=M_01 M_10=0. The checker independently verifies that final scalar +polynomial reduction. The nine binary labels embed in every such field. +This proves minrank nine for the specified constraints, not a new exponent. +""" +from collections import Counter +from copy import deepcopy +import hashlib +from itertools import combinations +import json +from pathlib import Path + +PIN='327d2a868043e846381aa58a33053c24425e8cad522ff401b10ec8af1d649a3f' +HERE=Path(__file__).resolve().parent +SOURCE=HERE.parents[1]/'research/direct-delivery504-global/inputs/hamming/PROTOTYPE.json' +BLOCKS=[ + [0,8,9,24,32,56,64,88], [0,8,16,24,32,40,56,57], + [1,8,9,24,33,56,65,88], [1,8,17,24,25,56,65,72], + [1,8,17,24,33,40,56,57], [0,8,16,24,25,56,64,72], +] + + +def require(condition,message): + if not condition: + raise ValueError(message) + + +def pinned(raw): + require(hashlib.sha256(raw).hexdigest()==PIN,'source SHA-256 mismatch') + return json.loads(raw) + + +def graph(roots): + require(len(roots)==112,'P112 vertex count') + require(all(len(r)==8 and all(type(x) is int for x in r) and sum(x*x for x in r)==4 + for r in roots),'eight integer coordinates and squared norm four') + edges=set() + for i,j in combinations(range(112),2): + dot=sum(roots[i][k]*roots[j][k] for k in range(8)) + require(dot in (-2,0,2),'distinct root lines with normalized Gram in {-1,0,1}') + if dot: + edges.add((i,j)) + return edges + + +def lower(edges,blocks): + require(len(blocks)==6,'six clique equations') + for block in blocks: + require(len(block)==8 and len(set(block))==8,'eight distinct clique vertices') + require(all(tuple(sorted((i,j))) in edges for i,j in combinations(block,2)), + 'clique requires zeros on BOTH directed off-diagonal matrix entries') + counts=Counter(v for block in blocks for v in block) + require(sorted(v for v,c in counts.items() if c%2)==[0,1],'odd incidence is precisely 0 and 1') + require((0,1) in edges,'the residual two vertices require off-diagonal zeros') + # Sandwich sum_C sum_i(v_i^T u_i)=6I by u_0 and v_0^T. + # Each surviving term is M_0i*M_i0, with distinct ordered symbols. + polynomial=Counter({():len(blocks)%2}) + for i,count in counts.items(): + if count%2: + if i==0: + polynomial[()]+=1 # M_00*M_00 = 1 + elif tuple(sorted((0,i))) not in edges: + polynomial[((0,i),(i,0))]+=1 # no symmetry assumed + residual={monomial:c%2 for monomial,c in polynomial.items() if c%2} + require(residual=={():1},'the derived scalar equation must reduce to 1=0') + return counts + + +def binary_basis(rows): + pivots={};indices=[] + for index,row in enumerate(rows): + x=row + while x: + p=x.bit_length()-1 + if p in pivots: + x^=pivots[p] + else: + pivots[p]=x;indices.append(index);break + return indices + + +def upper(roots,labels,edges): + require(len(labels)==112 and all(type(x) is int and 0 Date: Wed, 14 Oct 2026 06:32:53 -0300 Subject: [PATCH 2/3] Strengthen P112 certificate to block rank and nonlinear broadcast --- .../PETERSEN-LP-DUAL.json | 775 ++++++++++++++++++ .../PETERSEN-VERIFIED.json | 47 ++ .../p112-characteristic-two-minrank/README.md | 318 ++++--- .../p112-characteristic-two-minrank/TASK.json | 34 +- .../VERIFIED.json | 238 +++--- .../VERIFY.json | 13 +- .../petersen_lp_verify.py | 203 +++++ .../p112-characteristic-two-minrank/verify.py | 93 ++- 8 files changed, 1453 insertions(+), 268 deletions(-) create mode 100644 research/p112-characteristic-two-minrank/PETERSEN-LP-DUAL.json create mode 100644 research/p112-characteristic-two-minrank/PETERSEN-VERIFIED.json create mode 100644 research/p112-characteristic-two-minrank/petersen_lp_verify.py diff --git a/research/p112-characteristic-two-minrank/PETERSEN-LP-DUAL.json b/research/p112-characteristic-two-minrank/PETERSEN-LP-DUAL.json new file mode 100644 index 0000000000..645e6fba2b --- /dev/null +++ b/research/p112-characteristic-two-minrank/PETERSEN-LP-DUAL.json @@ -0,0 +1,775 @@ +{ + "schema": "petersen-shannon-rank-lp-dual-v1", + "prior_art": { + "authors": "Anna Blasiak, Robert Kleinberg, Eyal Lubetzky", + "title": "Index coding via linear programming", + "location": "Fact 5.6 (1)", + "url": "https://www.cs.cornell.edu/~ablasiak/papers/bkl-beta.pdf", + "claim": "Petersen broadcast rate beta = 5; no novelty claimed for this bound" + }, + "vertices": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 0, + 3 + ], + [ + 0, + 4 + ], + [ + 1, + 2 + ], + [ + 1, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 3 + ], + [ + 2, + 4 + ], + [ + 3, + 4 + ] + ], + "adjacency": "disjoint two-element subsets of {0,1,2,3,4}", + "variables": "F(S), for all 1024 subsets S of the ten vertices", + "certified_identity": "F(empty) - 5 = sum(multiplier * listed constraint expression)", + "constraints": [ + { + "kind": "slope", + "S": 0, + "i": 1, + "multiplier": "1/2" + }, + { + "kind": "slope", + "S": 0, + "i": 6, + "multiplier": "1/2" + }, + { + "kind": "slope", + "S": 2, + "i": 7, + "multiplier": "1/2" + }, + { + "kind": "slope", + "S": 64, + "i": 0, + "multiplier": "1/2" + }, + { + "kind": "slope", + "S": 65, + "i": 3, + "multiplier": "1/2" + }, + { + "kind": "submodular", + "S": 109, + "i": 1, + "j": 4, + "multiplier": "1/8" + }, + { + "kind": "slope", + "S": 128, + "i": 5, + "multiplier": "1/4" + }, + { + "kind": "submodular", + "S": 128, + "i": 1, + "j": 3, + "multiplier": "1/4" + }, + { + "kind": "slope", + "S": 130, + "i": 2, + "multiplier": "1/4" + }, + { + "kind": "submodular", + "S": 136, + "i": 4, + "j": 8, + "multiplier": "1/4" + }, + { + "kind": "slope", + "S": 138, + "i": 8, + "multiplier": "1/4" + }, + { + "kind": "slope", + "S": 140, + "i": 9, + "multiplier": "1/4" + }, + { + "kind": "submodular", + "S": 140, + "i": 0, + "j": 5, + "multiplier": "1/8" + }, + { + "kind": "submodular", + "S": 140, + "i": 1, + "j": 4, + "multiplier": "1/8" + }, + { + "kind": "submodular", + "S": 141, + "i": 4, + "j": 6, + "multiplier": "1/8" + }, + { + "kind": "submodular", + "S": 142, + "i": 0, + "j": 4, + "multiplier": "1/8" + }, + { + "kind": "submodular", + "S": 152, + "i": 2, + "j": 5, + "multiplier": "1/4" + }, + { + "kind": "submodular", + "S": 156, + "i": 5, + "j": 6, + "multiplier": "1/8" + }, + { + "kind": "submodular", + "S": 156, + "i": 6, + "j": 9, + "multiplier": "1/4" + }, + { + "kind": "submodular", + "S": 157, + "i": 1, + "j": 8, + "multiplier": "1/8" + }, + { + "kind": "slope", + "S": 160, + "i": 4, + "multiplier": "1/4" + }, + { + "kind": "slope", + "S": 162, + "i": 2, + "multiplier": "1/4" + }, + { + "kind": "submodular", + "S": 162, + "i": 3, + "j": 9, + "multiplier": "1/4" + }, + { + "kind": "submodular", + "S": 170, + "i": 6, + "j": 8, + "multiplier": "1/4" + }, + { + "kind": "submodular", + "S": 172, + "i": 0, + "j": 4, + "multiplier": "1/8" + }, + { + "kind": "slope", + "S": 192, + "i": 9, + "multiplier": "1/4" + }, + { + "kind": "submodular", + "S": 192, + "i": 2, + "j": 3, + "multiplier": "1/4" + }, + { + "kind": "submodular", + "S": 196, + "i": 0, + "j": 1, + "multiplier": "1/8" + }, + { + "kind": "submodular", + "S": 196, + "i": 1, + "j": 8, + "multiplier": "1/8" + }, + { + "kind": "submodular", + "S": 197, + "i": 1, + "j": 3, + "multiplier": "1/8" + }, + { + "kind": "slope", + "S": 200, + "i": 8, + "multiplier": "1/4" + }, + { + "kind": "submodular", + "S": 200, + "i": 0, + "j": 1, + "multiplier": "1/4" + }, + { + "kind": "submodular", + "S": 200, + "i": 0, + "j": 2, + "multiplier": "1/4" + }, + { + "kind": "submodular", + "S": 202, + "i": 0, + "j": 4, + "multiplier": "1/4" + }, + { + "kind": "submodular", + "S": 218, + "i": 8, + "j": 9, + "multiplier": "1/4" + }, + { + "kind": "submodular", + "S": 220, + "i": 0, + "j": 5, + "multiplier": "1/8" + }, + { + "kind": "submodular", + "S": 220, + "i": 8, + "j": 9, + "multiplier": "1/4" + }, + { + "kind": "slope", + "S": 226, + "i": 4, + "multiplier": "1/4" + }, + { + "kind": "submodular", + "S": 226, + "i": 2, + "j": 3, + "multiplier": "1/4" + }, + { + "kind": "submodular", + "S": 234, + "i": 2, + "j": 9, + "multiplier": "1/4" + }, + { + "kind": "submodular", + "S": 234, + "i": 4, + "j": 8, + "multiplier": "1/4" + }, + { + "kind": "submodular", + "S": 392, + "i": 4, + "j": 6, + "multiplier": "1/4" + }, + { + "kind": "submodular", + "S": 413, + "i": 5, + "j": 9, + "multiplier": "1/8" + }, + { + "kind": "submodular", + "S": 452, + "i": 1, + "j": 3, + "multiplier": "1/8" + }, + { + "kind": "submodular", + "S": 460, + "i": 5, + "j": 9, + "multiplier": "1/8" + }, + { + "kind": "submodular", + "S": 492, + "i": 0, + "j": 1, + "multiplier": "1/8" + }, + { + "kind": "submodular", + "S": 674, + "i": 3, + "j": 6, + "multiplier": "1/4" + }, + { + "kind": "slope", + "S": 704, + "i": 5, + "multiplier": "1/4" + }, + { + "kind": "submodular", + "S": 730, + "i": 0, + "j": 5, + "multiplier": "1/4" + }, + { + "kind": "submodular", + "S": 752, + "i": 0, + "j": 2, + "multiplier": "1/4" + }, + { + "kind": "submodular", + "S": 908, + "i": 5, + "j": 6, + "multiplier": "1/8" + }, + { + "kind": "decode", + "S": 73, + "i": 7, + "multiplier": "-1/2" + }, + { + "kind": "decode", + "S": 109, + "i": 7, + "multiplier": "-1/8" + }, + { + "kind": "decode", + "S": 111, + "i": 7, + "multiplier": "1/8" + }, + { + "kind": "decode", + "S": 125, + "i": 7, + "multiplier": "1/8" + }, + { + "kind": "decode", + "S": 127, + "i": 7, + "multiplier": "-5/8" + }, + { + "kind": "decode", + "S": 127, + "i": 8, + "multiplier": "1/4" + }, + { + "kind": "decode", + "S": 127, + "i": 9, + "multiplier": "1/4" + }, + { + "kind": "decode", + "S": 134, + "i": 6, + "multiplier": "-1/4" + }, + { + "kind": "decode", + "S": 143, + "i": 6, + "multiplier": "1/8" + }, + { + "kind": "decode", + "S": 166, + "i": 6, + "multiplier": "-1/4" + }, + { + "kind": "decode", + "S": 176, + "i": 3, + "multiplier": "-1/4" + }, + { + "kind": "decode", + "S": 183, + "i": 3, + "multiplier": "-1/4" + }, + { + "kind": "decode", + "S": 183, + "i": 6, + "multiplier": "1/4" + }, + { + "kind": "decode", + "S": 189, + "i": 8, + "multiplier": "-1/8" + }, + { + "kind": "decode", + "S": 191, + "i": 6, + "multiplier": "-3/8" + }, + { + "kind": "decode", + "S": 191, + "i": 8, + "multiplier": "1/8" + }, + { + "kind": "decode", + "S": 219, + "i": 9, + "multiplier": "-1/4" + }, + { + "kind": "decode", + "S": 237, + "i": 8, + "multiplier": "-1/8" + }, + { + "kind": "decode", + "S": 239, + "i": 8, + "multiplier": "1/8" + }, + { + "kind": "decode", + "S": 242, + "i": 3, + "multiplier": "-1/4" + }, + { + "kind": "decode", + "S": 243, + "i": 3, + "multiplier": "1/4" + }, + { + "kind": "decode", + "S": 243, + "i": 9, + "multiplier": "-1/4" + }, + { + "kind": "decode", + "S": 247, + "i": 9, + "multiplier": "1/4" + }, + { + "kind": "decode", + "S": 251, + "i": 9, + "multiplier": "1/4" + }, + { + "kind": "decode", + "S": 255, + "i": 8, + "multiplier": "-1" + }, + { + "kind": "decode", + "S": 347, + "i": 2, + "multiplier": "-1/4" + }, + { + "kind": "decode", + "S": 347, + "i": 7, + "multiplier": "1/4" + }, + { + "kind": "decode", + "S": 351, + "i": 5, + "multiplier": "-1/4" + }, + { + "kind": "decode", + "S": 394, + "i": 5, + "multiplier": "-1/4" + }, + { + "kind": "decode", + "S": 398, + "i": 5, + "multiplier": "-1/8" + }, + { + "kind": "decode", + "S": 398, + "i": 6, + "multiplier": "1/8" + }, + { + "kind": "decode", + "S": 415, + "i": 5, + "multiplier": "-1/8" + }, + { + "kind": "decode", + "S": 430, + "i": 6, + "multiplier": "-1/8" + }, + { + "kind": "decode", + "S": 472, + "i": 2, + "multiplier": "-1/4" + }, + { + "kind": "decode", + "S": 474, + "i": 5, + "multiplier": "1/4" + }, + { + "kind": "decode", + "S": 475, + "i": 9, + "multiplier": "1/4" + }, + { + "kind": "decode", + "S": 511, + "i": 9, + "multiplier": "-1" + }, + { + "kind": "decode", + "S": 621, + "i": 1, + "multiplier": "-1/4" + }, + { + "kind": "decode", + "S": 621, + "i": 7, + "multiplier": "1/4" + }, + { + "kind": "decode", + "S": 623, + "i": 4, + "multiplier": "-1/4" + }, + { + "kind": "decode", + "S": 652, + "i": 4, + "multiplier": "-1/4" + }, + { + "kind": "decode", + "S": 685, + "i": 4, + "multiplier": "1/8" + }, + { + "kind": "decode", + "S": 685, + "i": 8, + "multiplier": "-1/8" + }, + { + "kind": "decode", + "S": 686, + "i": 4, + "multiplier": "-1/4" + }, + { + "kind": "decode", + "S": 686, + "i": 6, + "multiplier": "1/4" + }, + { + "kind": "decode", + "S": 694, + "i": 3, + "multiplier": "1/4" + }, + { + "kind": "decode", + "S": 694, + "i": 6, + "multiplier": "-1/4" + }, + { + "kind": "decode", + "S": 701, + "i": 8, + "multiplier": "1/8" + }, + { + "kind": "decode", + "S": 736, + "i": 1, + "multiplier": "-1/4" + }, + { + "kind": "decode", + "S": 749, + "i": 8, + "multiplier": "1/4" + }, + { + "kind": "decode", + "S": 752, + "i": 1, + "multiplier": "-1/4" + }, + { + "kind": "decode", + "S": 753, + "i": 1, + "multiplier": "1/4" + }, + { + "kind": "decode", + "S": 754, + "i": 3, + "multiplier": "-1/4" + }, + { + "kind": "decode", + "S": 756, + "i": 1, + "multiplier": "1/4" + }, + { + "kind": "decode", + "S": 757, + "i": 1, + "multiplier": "-1/4" + }, + { + "kind": "decode", + "S": 908, + "i": 0, + "multiplier": "-1/8" + }, + { + "kind": "decode", + "S": 909, + "i": 4, + "multiplier": "-1/8" + }, + { + "kind": "decode", + "S": 940, + "i": 0, + "multiplier": "1/8" + }, + { + "kind": "decode", + "S": 972, + "i": 4, + "multiplier": "1/4" + }, + { + "kind": "decode", + "S": 986, + "i": 0, + "multiplier": "-1/4" + }, + { + "kind": "decode", + "S": 1004, + "i": 0, + "multiplier": "-1/4" + }, + { + "kind": "normalize", + "multiplier": "1" + } + ], + "discovery_only": { + "solver": "scipy.optimize.linprog(method=highs)", + "float_optimum": 5.0, + "total_inequalities": 21760, + "total_equalities": 641 + } +} diff --git a/research/p112-characteristic-two-minrank/PETERSEN-VERIFIED.json b/research/p112-characteristic-two-minrank/PETERSEN-VERIFIED.json new file mode 100644 index 0000000000..b7c4f9ed60 --- /dev/null +++ b/research/p112-characteristic-two-minrank/PETERSEN-VERIFIED.json @@ -0,0 +1,47 @@ +{ + "PASS": true, + "terms": 113, + "kinds": { + "decode": 61, + "normalize": 1, + "slope": 15, + "submodular": 36 + }, + "exact_identity": "F(empty) - 5", + "subset_coefficients_checked": 1024, + "matching_upper_bound": { + "pairs": [ + [ + 0, + 7 + ], + [ + 1, + 6 + ], + [ + 2, + 8 + ], + [ + 3, + 5 + ], + [ + 4, + 9 + ] + ], + "exact_rate": 5, + "all_elementary_inequalities_checked": 21760, + "all_decoding_equalities_checked": 640 + }, + "negative_controls_rejected": [ + "changed_multiplier", + "negative_inequality_multiplier", + "missing_decode_neighbor", + "omitted_normalization", + "changed_graph_numbering" + ], + "certificate_sha256": "beb7ada1d584e5c83325c37caffeb6c6ff6b16add289fa413b8d8066d1ac43fd" +} diff --git a/research/p112-characteristic-two-minrank/README.md b/research/p112-characteristic-two-minrank/README.md index 36103adfbe..11f9d3c1f4 100644 --- a/research/p112-characteristic-two-minrank/README.md +++ b/research/p112-characteristic-two-minrank/README.md @@ -1,117 +1,193 @@ -# P112 fitting rank is nine in every characteristic-two field - -For the pinned 112-port graph, **every matrix with nonzero diagonal and zeros -on the required pairs has rank at least nine over every field of characteristic -two**, finite or infinite. Symmetry is not assumed. The existing binary labels -give the matching upper bound. Six eight-cliques on just 17 vertices certify the -lower bound. The same induced 17-vertex graph therefore has minimum rank nine. - -This is a scoped obstruction to a rank-eight label replacement. It supplies no -new circuit, helper inventory, multiplication theorem or improved exponent. +# P112 block-rank and binary broadcast certificates + +For the pinned 112-port graph, every fitting matrix with invertible d-by-d +diagonal blocks has rank at least **9d over every field**, for every positive +integer d. The existing binary labels attain 9d over every characteristic-two +field. In the corresponding side-information graph, even nonlinear zero-error +codes for d-bit messages require exactly **9d broadcast bits**. + +A source-pinned induced graph on 14 vertices certifies these statements: in the +usual fitting/side-information convention it is four isolated vertices disjoint +from the Petersen graph. Petersen's broadcast rate five is known from +[Blasiak, Kleinberg and Lubetzky, Fact 5.6(1)](https://www.cs.cornell.edu/~ablasiak/papers/bkl-beta.pdf). +This package supplies the explicit embedding, an exact rational certificate for +that known bound, and a separate short characteristic-two proof. It makes no +novelty claim for the Petersen theorem or the inherited binary upper bound. + +This closes scalar, block-linear and binary nonlinear rank/broadcast compression +of this fixed graph below nine. It supplies no new native circuit, helper +inventory, multiplication theorem or improved exponent. An abstract broadcast +code is not a legal reversible supplier word. ## Exact object and graph convention Use root_lines[8:] and binary_ports[8:] from [PROTOTYPE.json](../direct-delivery504-global/inputs/hamming/PROTOTYPE.json). -The removed first eight roots are exactly twice the coordinate vectors. The -remaining roots are integer vectors in eight dimensions, of squared norm four; -their distinct-pair dot products are in {-2,0,2}. +The removed eight roots are twice the coordinate vectors. The remaining 112 +integer roots have squared norm four; distinct root dot products are -2, 0 or 2. +All vertex indices below are zero-based after removing the eight rows. + +Let R be the required-zero graph: distinct i,j are adjacent when their root dot +product is nonzero. It has 2,912 unordered edges. A block matrix fits this +convention if M_ii is invertible and M_ij=M_ji=0 on every edge of R. Symmetry +of M is not assumed. Left multiplication by diag(M_ii inverse) normalizes +all diagonal blocks to I_d without changing rank or required zeros. + +Let G be the complement of R. This is the usual Haemers fitting graph, with +zeros required on nonedges, and the side-information graph in which receiver i +knows x_j precisely for neighbors j in G. Thus G is the induced E8 +orthogonality graph. The two graph conventions must not be interchanged. + +The source commit is 0b1cccf86e2f5132ed286a26ef0a681a495740ea and input SHA256 +is 327d2a868043e846381aa58a33053c24425e8cad522ff401b10ec8af1d649a3f. +[SOURCES.json](SOURCES.json) also pins the Git blob and historical catalogue +and selected record. No predecessor or selected-record file is modified. + +## Four cliques and a 14-vertex embedding + +These are eight-cliques in R: + +~~~text +C1 = 2, 16, 57, 70, 78, 84, 100, 102 +C2 = 10, 16, 57, 70, 78, 84, 108, 110 +C3 = 2, 10, 16, 32, 34, 57, 70, 84 +C4 = 16, 32, 57, 68, 70, 84, 100, 108 +~~~ + +Their union has 14 vertices and 76 induced edges of R. Exactly +T={34,68,102,110} has odd incidence, and T itself is a four-clique in R. -Indices below are zero-based **after** removing the first eight rows. Put an -edge between distinct indices i and j exactly when their integer root dot -product is nonzero. These are the 2,912 unordered **required-zero** pairs. -A fitting matrix here has M_ii nonzero and M_ij = M_ji = 0 on each such pair; -all other off-diagonal entries are free. +Within this union, U={16,57,70,84} is adjacent in R to all other vertices. +Identify the remaining vertices with two-subsets of {0,1,2,3,4}: -Some Haemers-bound literature instead calls a matrix fitting when its zeros -are on graph nonedges. Our required-zero graph is the complement of the -corresponding induced E8 orthogonality graph. This convention matters. +~~~text +2:02 10:12 32:23 34:24 68:34 +78:01 100:03 102:04 108:13 110:14 +~~~ + +The checker verifies every pair: two of these vertices are adjacent in R +exactly when their subsets intersect. Consequently the induced graph in G is +four isolated vertices plus the Petersen graph, whose edges join disjoint +two-subsets. This is an explicit isomorphism, not a degree-sequence inference. -The exact source commit is 0b1cccf86e2f5132ed286a26ef0a681a495740ea. -The input SHA256 is -327d2a868043e846381aa58a33053c24425e8cad522ff401b10ec8af1d649a3f. -[SOURCES.json](SOURCES.json) also pins the Git blob and historical catalogue and -selected record. Those provenance files are not changed by this package. +## Short proof in characteristic two -## Six-clique certificate +Factor a normalized fitting block matrix as M_ij=U_i V_j with rank r, +where U_i is d-by-r and V_i is r-by-d. Then P_i=V_i U_i is a rank-d +idempotent. On a clique of R these idempotents mutually annihilate in both +orders. For each displayed eight-clique C, their sum S_C is therefore an +idempotent of rank 8d, and E_C=I_r-S_C has rank r-8d. -Each row is an eight-clique in the required-zero graph: +In characteristic two, summing the four equations for E_C cancels the four +identity matrices and all even incidences, leaving sum_C E_C=sum_T P_i. +The latter has rank 4d because T is a required-zero clique. Rank subadditivity +now gives ~~~text -C1 = 0, 8, 9, 24, 32, 56, 64, 88 -C2 = 0, 8, 16, 24, 32, 40, 56, 57 -C3 = 1, 8, 9, 24, 33, 56, 65, 88 -C4 = 1, 8, 17, 24, 25, 56, 65, 72 -C5 = 1, 8, 17, 24, 33, 40, 56, 57 -C6 = 0, 8, 16, 24, 25, 56, 64, 72 +4d <= 4(r-8d), so r >= 9d. ~~~ -Their union has 17 vertices and 106 induced required-zero pairs. In the six -rows, exactly vertices 0 and 1 occur an odd number of times. They are adjacent. -These elementary integer facts are all the finite input needed for the lower -bound. +This argument applies to every characteristic-two field, finite or infinite, +and every positive d. It needs neither symmetry nor a Gram representation. +The finite checker verifies its clique/incidence inputs and exact coefficients; +the rank lemmas above are a human-readable proof, not a Lean formalization. -## Proof for arbitrary fitting matrices +## Exact Petersen certificate and the all-field lower bound -Let F be any field of characteristic two and M any fitting matrix. Multiplying -each row by the inverse of its diagonal entry preserves rank and required -zeros, so assume M_ii = 1. Every eight-clique gives an identity principal -submatrix, hence rank(M) is at least eight. +[PETERSEN-LP-DUAL.json](PETERSEN-LP-DUAL.json) contains 113 rational terms in +functions F(S), indexed by all 1,024 subsets of the ten Petersen vertices. +[petersen_lp_verify.py](petersen_lp_verify.py) reconstructs each term from its +kind and vertex/subset indices; it never trusts a stored coefficient row. +It checks the exact identity + +~~~text +F(empty)-5 = sum_t multiplier_t * expression_t(F). +~~~ -Suppose rank(M) = 8 and factor M = U V^T, where U and V have eight columns. -Write their i-th rows as u_i and v_i. For each displayed clique C, +There are 15 slope inequalities, 36 elementary submodular inequalities, +61 decoding equalities and one normalization equality. The allowed expressions +are ~~~text -U_C V_C^T = I_8, so V_C^T U_C = I_8. +monotone: F(S+i)-F(S) >= 0 +slope: F(S)+1-F(S+i) >= 0 +submodular: F(S+i)+F(S+j)-F(S)-F(S+i+j) >= 0 +decode: F(S+i)-F(S) = 0, when every neighbor of i lies in S +normalize: F(V)-10 = 0 ~~~ -Thus the rank-one matrices P_i = v_i^T u_i sum to I_8 on each clique. -Sum all six equations. Characteristic two cancels their right sides and every -even-incidence P_i, leaving P_0 = P_1. Multiplication on the left by u_0 and -on the right by v_0^T gives +Added vertices must be absent from S, and i and j distinct. Inequality +multipliers are positive; equality multipliers may have either sign. Exact +Fraction arithmetic confirms coefficient one at F(empty), zero at the other +1,023 variables, and constant -5. Thus every function satisfying these +constraints has F(empty)>=5. Floating-point LP was used only to propose the +certificate; verification has no optimizer or third-party dependency. + +To apply this over an arbitrary field, let Q be a normalized Petersen-fitting +block matrix and W its row space inside the 10d-dimensional coordinate space. +Write E_i for coordinate block i and set ~~~text -1 = (u_0 v_0^T)^2 = u_0 P_0 v_0^T - = u_0 P_1 v_0^T = (u_0 v_1^T)(u_1 v_0^T) = M_01 M_10 = 0. +F(S) = dim(W + sum_(i in S) E_i) / d. ~~~ -This contradiction proves rank(M) at least nine without assuming symmetry, -a Gram representation or a finite field. The argument uses only the displayed -17 vertices. +Dimension is monotone and submodular and each coordinate block raises it by +at most d. Normalization gives F(V)=10. The d rows belonging to receiver i +have identity in block i and zeros outside i and its neighbors. Hence +E_i is contained in W+sum_(j in N(i)) E_j, proving the decoding equalities. +The certificate gives rank(Q)>=5d, including over infinite fields. + +The principal submatrix on the displayed 14 vertices is block diagonal +I_(4d) plus such a Q. Its rank is at least 9d, so the full matrix also has +rank at least 9d. A perfect matching of Petersen gives five independent +pair-sum rows over every field; adding the four isolated coordinates shows +that the 14-vertex graph has exact minimum block rank 9d over every field. +For the full 112-vertex graph, only the characteristic-two upper bound is +provided here. + +## Nonlinear zero-error binary broadcast -For the upper bound, decode each retained binary label as a vector b_i in -F_2^9. The checker verifies odd self-dot product and zero dot product on every -required pair, as well as the complete Gram identity +Fix the 98 outside messages to arbitrary constants. In the induced 14-vertex +problem the four isolated messages Z have no side information, so Z is a +function of the broadcast B. Take all remaining messages independent and +uniform d-bit strings. Then ~~~text -b_i . b_j = 1 + (root_i . root_j)/2 (mod 2). +H(B) = H(Z)+H(B|Z) = 4d+H(B|Z). ~~~ -Consequently their binary Gram matrix is a fitting matrix of rank at most -nine over every characteristic-two field. The checker also computes rank nine -for that matrix and verifies that the 17 retained labels span nine dimensions. -Together with the lower bound this proves the claimed equality for both graphs. +For each fixed z, set F(S)=H(B,X_S | Z=z)/d on the ten Petersen messages. +Entropy is monotone and submodular, each message adds at most d bits, +deterministic encoding gives F(V)=10, and zero-error decoding gives the listed +equalities. The exact certificate forces H(B|Z=z)>=5d. Thus H(B)>=9d, +and a fixed-length broadcast requires at least 9d bits. Fixing the outside +messages cannot increase the available broadcast length, so this is also a +lower bound for the full graph. -## Block-rank corollary and its limit +The same lower-bound argument works for independent uniform messages in any +finite alphabet, after normalizing entropy by their log cardinality. The +matching upper bound for the full graph asserted here is specifically binary. +No zero-error nonlinear binary block code of any block length beats nine. -For d-by-d blocks, suppose M_ii = I_d and M_ij = M_ji = 0 on all required -pairs. Write r = rank(M) and factor its blocks as M_ij = U_i V_j, with U_i of -size d by r and V_i of size r by d. Each P_i = V_i U_i is a rank-d idempotent. -On an eight-clique the P_i are pairwise mutually annihilating, so their sum -S_C is an idempotent of rank 8d. Therefore E_C = I_r - S_C has rank r - 8d. +## Known upper construction -The same six-clique cancellation gives P_0 + P_1 = sum_C E_C. Since P_0 and -P_1 are mutually annihilating rank-d idempotents, their sum has rank 2d. -Rank subadditivity gives +Let b_i be the retained binary label in F_2^9. The checker verifies all +12,544 entries of ~~~text -2d <= 6(r - 8d), hence r >= ceil(25d/3). +b_i dot b_j = 1 + (root_i dot root_j)/2 (mod 2), ~~~ -Invertible diagonal blocks can be normalized first. This is a human proof of -a normalized block-rank lower bound of 25/3; it does **not** prove a fractional -minimum of nine or rule out every block-valued interface. The finite checker -verifies the common clique certificate, not a formalization of the rank lemmas. +including odd diagonal entries and all required zeros. The resulting fitting +matrix has rank nine, as does its restriction to the 14 vertices. Tensoring +with I_d gives rank 9d over every characteristic-two field. + +For a broadcast code transmit s=sum_j b_j x_j, with nine bitwise coordinates. +Receiver i computes b_i dot s. Its own coefficient is one; every other +nonzero coefficient is on a neighbor in G and can be subtracted using the +known message. This gives 9d broadcast bits for every positive d. Together +with the preceding lower bound it proves exactness at each block length, +not just an asymptotic infimum. ## Reproduce and coverage @@ -122,51 +198,53 @@ python3.12 scripts/research_package.py --package research/p112-characteristic-tw python3.12 scripts/research_package.py --package research/p112-characteristic-two-minrank ~~~ -The registered replay runs verify.py with -I -B -O. Every acceptance check -uses an explicit exception and remains active with assertions disabled. The -script rewrites the deterministic [VERIFIED.json](VERIFIED.json) receipt. +The registered replay runs both verifiers with -I -B -O. Explicit exceptions +keep acceptance checks active with assertions disabled. The deterministic +receipts are [VERIFIED.json](VERIFIED.json) and +[PETERSEN-VERIFIED.json](PETERSEN-VERIFIED.json). -The independently written verifier imports no search program or producer. -It checks the exact input hash, source indexing, every clique edge and incidence, -the scalar sandwich reduction, all 2,912 required-zero pairs, all 12,544 binary -Gram entries, and the rank-nine upper construction. Seven negative controls -alter source bytes, a clique vertex, the clique count, the edge convention, -an upper label's diagonal, an upper label while preserving odd norm, and the -label dimension. All seven must be rejected. +The graph verifier imports no producer, search program or other verifier. +It checks the source hash and indexing, all 2,912 required-zero pairs, all +12,544 Gram entries, the four-clique certificate, the exact graph isomorphism +and rank-nine upper bounds. Ten corruption controls must be rejected. +The separate dual verifier checks all 1,024 rational coefficient sums and +rejects five corruptions, including a negative inequality multiplier and +an invalid decoding condition. Its perfect-matching positive fixture checks +all 21,760 elementary inequalities and all 640 decoding equalities. -The universal field statements follow from the proof above; a finite solver -search is neither needed nor used in this replay. No full supplier or selected -frontier replay is claimed. This is not a Lean formalization. +The reductions from rank and entropy to these finite certificates are the +proofs above. No formal proof assistant, full supplier replay or selected +frontier replay is claimed. ## Overlap, relevance and attribution [Discussion 1713](https://github.com/CrocSwap/integer-mult-bounds/discussions/1713) -records the finding and its strengthening from symmetric representations to -arbitrary fitting matrices. The complete remote overlap refresh on -2026-10-14 at 08:19 UTC covered 418 open PRs and 371 Discussions, including -comments and replies. Local overlap coverage was limited by this sparse -checkout. [PR1471](https://github.com/CrocSwap/integer-mult-bounds/pull/1471), -head 3695ad16e7bc4c0f6248a9e5a64fc069fa096733, audits the odd-characteristic -portability of a particular P112 tensor proof. The present theorem instead -bounds every fitting matrix in characteristic two. An overlap search does not -establish novelty, and no priority claim is made here. - -The rank-nine upper construction is known: Debbie Leung, Laura Mancinska, -William Matthews, Maris Ozols and Aidan Roy, +records the scoped result. The complete remote overlap refresh on +2026-10-14 at 09:32 UTC covered 442 open PRs and 409 Discussions, including +comments and replies. Sparse-checkout local coverage was limited. +[PR1471](https://github.com/CrocSwap/integer-mult-bounds/pull/1471), head +3695ad16e7bc4c0f6248a9e5a64fc069fa096733, audits odd-characteristic portability +of a particular P112 tensor proof. This package bounds every fitting matrix +and the corresponding binary broadcast problem. No priority claim is made. + +Petersen's rate five is established in Anna Blasiak, Robert Kleinberg and +Eyal Lubetzky, [Index coding via linear programming](https://arxiv.org/abs/1004.1379), +Fact 5.6(1), printed page 28. The dual here is an exact replayable certificate +of that known result. The binary upper construction is also known: Debbie +Leung, Laura Mancinska, William Matthews, Maris Ozols and Aidan Roy, [Entanglement can increase asymptotic rates of zero-error classical communication over classical channels](https://arxiv.org/abs/1009.1195), -Theorem 9 and section 4, explain the binary symplectic upper bound and the E8 -embedding, crediting Peeters for the symplectic-graph result. We credit that -literature rather than treating the inherited labels as a new construction. -The contribution here is the explicit six-clique lower certificate, its -source binding and the independently replayable checks; no literature-wide -novelty claim for the underlying rank obstruction is asserted. - -The concrete input is retained from icekylinx's +Theorem 9 and section 4, explain the symplectic construction and E8 embedding, +crediting Peeters for the symplectic-graph result. The contribution here is +the pinned P112 embedding, the four-clique certificate, and independent exact +checks of the resulting scoped obstructions; no literature-wide novelty claim +for the underlying parameters is asserted. + +The input is retained from icekylinx's [direct-delivery504-global](../direct-delivery504-global/README.md) package, prepared with OpenAI GPT-6 Astra assistance. Its Hamming/root inputs descend from the PR523/514/507/425/433 lineage credited in that package's -[NOTICE.md](../direct-delivery504-global/NOTICE.md) and source ancestry. This -package references the existing input without modifying or re-vendoring it. +[NOTICE.md](../direct-delivery504-global/NOTICE.md). Inputs are referenced +without modification or re-vendoring. Prepared for Thiago with substantial OpenAI GPT-6 Astra and Codex assistance for exploration, proof review, independent checking and packaging. New work @@ -174,11 +252,11 @@ is Apache-2.0; retained source attribution and licenses remain applicable. ## Open next questions -Can a changed graph or a genuinely block-valued interface improve a complete -paid supplier budget? The fixed scalar rank-eight premise is closed, but the -block corollary leaves a gap between 25/3 and nine. A useful first step is to -write the changed constraints and an optimistic complete paid budget before -building a circuit. The missing native word, restoration/phase proof and -global owner invoice are the current blockers. [TASK.json](TASK.json) records -this question and explicitly labels this package as a side result of the -helper-inventory investigation. +Can a changed port graph or a native word that changes the fitting/broadcast +constraints improve a complete paid supplier budget? Merely using larger +blocks, asymmetric labels, extension fields, or nonlinear binary encoding +cannot lower this fixed graph's bound below nine. A useful first step is to +state the changed constraints and a complete optimistic paid budget before +building a circuit. Missing native words, restoration/phase proofs and global +owner invoices remain the blockers. [TASK.json](TASK.json) explicitly labels +this package as a side result of the helper-inventory investigation. diff --git a/research/p112-characteristic-two-minrank/TASK.json b/research/p112-characteristic-two-minrank/TASK.json index 3db0aaa7ab..c99100b106 100644 --- a/research/p112-characteristic-two-minrank/TASK.json +++ b/research/p112-characteristic-two-minrank/TASK.json @@ -42,48 +42,52 @@ ] }, "scope_status": "changed", - "actual_scope": "Prove the minimum rank of arbitrary, possibly asymmetric fitting matrices for the pinned P112 required-zero graph over every characteristic-two field, with an explicit small certificate and independent checker.", - "scope_change_reason": "The constructive helper-inventory investigation raised a necessary rank-eight label premise. This package isolates its exact obstruction as a side result; it does not supply a changed helper inventory.", - "bottleneck_link": "Excludes replacing the fixed P112 nine-coordinate fitting labels by eight coordinates over any characteristic-two extension field, even with different source and target labels. Changed graphs, block interfaces, and complete suppliers require separate work; no kappa improvement follows.", + "actual_scope": "Source-pinned induced Petersen-plus-four-isolates certificate: block fitting rank at least 9d over every field, equality in characteristic two, and exact nonlinear zero-error binary broadcast length 9d for every positive block size d.", + "scope_change_reason": "The helper-inventory investigation raised a necessary rank-eight label premise. This side result isolates the obstruction, strengthens it to all block sizes and binary nonlinear coding, and identifies its known Petersen-theorem basis; it supplies no new helper inventory.", + "bottleneck_link": "Closes below-nine fitting compression of this exact graph over every field and binary nonlinear broadcast compression at every block size. A positive supplier must change the graph/constraints or save other paid work; no kappa improvement follows.", "budget_minutes": 75, - "stop_rule": "Stop this side-result investigation after a source-pinned finite certificate, an elementary proof over every characteristic-two field, independent replay and explicit scope/attribution checks.", + "stop_rule": "Finish this side result after source-pinned embedding, exact rational dual, independent characteristic-two proof, registered replays, and explicit prior-art/scope checks.", "outcome": "completed", - "evidence": "Six eight-cliques use 17 vertices and have odd incidence exactly at adjacent vertices 0 and 1. The independent standard-library verifier checks all 2912 required-zero pairs, the complete binary Gram matrix, rank-nine upper bounds, the symbolic scalar contradiction and seven corruption controls. README gives the universal proof and a separately reviewed block-rank corollary.", + "evidence": "Four eight-cliques on 14 vertices have odd incidence at a four-clique, proving 4d<=4(r-8d) in characteristic two. The induced usual fitting graph is four isolates plus Petersen. A 113-term exact rational certificate proves the known Petersen bound five and extends the full lower bound to all fields and nonlinear zero-error codes. Independent standard-library replays check all 2912 required-zero pairs, 12544 binary Gram entries, all 1024 dual coefficients, a matching positive fixture, and 15 corruption controls.", "author": "Thiago, with OpenAI GPT-6 Astra and Codex assistance", "ai_assistance": "Substantial OpenAI GPT-6 Astra and Codex assistance was used for mathematical exploration, independent checking, literature search, implementation and packaging.", "open_questions": [ { - "question": "Can a changed port graph or genuinely block-valued label interface improve a complete paid supplier budget?", - "why_it_matters": "The scalar rank-eight premise for this exact graph is closed. The block corollary gives only normalized rank at least 25/3, not nine, and does not price a supplier.", - "first_step": "Write the changed graph or block constraints and derive a complete optimistic paid budget before constructing a circuit.", - "blocked_by": "No compatible native word, restoration/phase proof or global owner invoice for such a changed interface is supplied here." + "question": "Can a changed graph or changed native interface improve a complete paid supplier budget?", + "why_it_matters": "The fixed graph cannot be compressed below nine using scalar or block-linear fitting matrices over any field, nor nonlinear zero-error binary codes. Savings must change those constraints or remove other paid work.", + "first_step": "Specify the changed graph or native constraints and derive a complete optimistic paid budget before constructing a circuit.", + "blocked_by": "No compatible native word, restoration/phase proof or global owner invoice for a changed interface is supplied here." } ], "coordination": { "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1713", - "overlap_checked_at": "2026-10-14T08:19:31.840748+00:00", + "overlap_checked_at": "2026-10-14T09:32:07.988435+00:00", "coverage": { "open_prs": { - "fetched_at": "2026-10-14T08:18:08.249593+00:00", + "fetched_at": "2026-10-14T09:30:20.286086+00:00", "complete_pagination": true, - "records": 418 + "records": 442 }, "discussions": { - "fetched_at": "2026-10-14T08:19:31.759476+00:00", + "fetched_at": "2026-10-14T09:32:07.925671+00:00", "complete_pagination": true, - "records": 371 + "records": 409 } }, "nearest_overlap": { "pr": 1471, "head": "3695ad16e7bc4c0f6248a9e5a64fc069fa096733", - "difference": "PR1471 audits odd-characteristic portability of a pinned P112 tensor argument; this package proves a lower bound for all fitting matrices over every characteristic-two field." + "difference": "PR1471 audits odd-characteristic portability of a pinned P112 tensor argument; this package gives an all-field lower bound for all fitting block matrices and a nonlinear binary broadcast lower bound through an explicit classical subgraph." } }, "prior_art": [ { "url": "https://arxiv.org/abs/1009.1195", "description": "Leung, Mancinska, Matthews, Ozols and Roy, Theorem 9 and section 4: known rank-nine symplectic upper construction; graph convention explained in README." + }, + { + "url": "https://arxiv.org/abs/1004.1379", + "description": "Blasiak, Kleinberg and Lubetzky, Index coding via linear programming, Fact 5.6(1): known Petersen broadcast rate five. The package gives a source-pinned embedding and exact rational dual, with no novelty claim for this theorem." } ] } diff --git a/research/p112-characteristic-two-minrank/VERIFIED.json b/research/p112-characteristic-two-minrank/VERIFIED.json index 275d387b9b..85f5c089dc 100644 --- a/research/p112-characteristic-two-minrank/VERIFIED.json +++ b/research/p112-characteristic-two-minrank/VERIFIED.json @@ -1,119 +1,150 @@ { - "status": "PASS_INDEPENDENT_GENERAL_CHAR2_MINIMUM_FITTING_RANK_NINE", + "status": "PASS_INDEPENDENT_CHAR2_ALL_BLOCK_SIZES_FITTING_RANK_9D", "source_sha256": "327d2a868043e846381aa58a33053c24425e8cad522ff401b10ec8af1d649a3f", "source_vertex_offset": 8, "vertices": 112, "required_zero_unordered_edges": 2912, "symmetric_matrix_assumed": false, - "diagonal_normalization": "left multiply by diag(M_ii^-1); preserves rank and every required zero", - "factor_orientation": "M_ij=u_i*v_j^T; P_i=v_i^T*u_i; U_C*V_C^T=I implies V_C^T*U_C=I", + "diagonal_normalization": "left multiply by blockdiag(M_ii^-1); preserves rank and every required zero", + "factor_orientation": "M_ij=U_i*V_j; P_i=V_i*U_i; U_C*V_C=I_8d implies V_C*U_C is a rank-8d idempotent", "certificate_vertices": [ - 0, - 1, - 8, - 9, + 2, + 10, 16, - 17, - 24, - 25, 32, - 33, - 40, - 56, + 34, 57, - 64, - 65, - 72, - 88 + 68, + 70, + 78, + 84, + 100, + 102, + 108, + 110 ], "cliques": [ [ - 0, - 8, - 9, - 24, - 32, - 56, - 64, - 88 - ], - [ - 0, - 8, + 2, 16, - 24, - 32, - 40, - 56, - 57 + 57, + 70, + 78, + 84, + 100, + 102 ], [ - 1, - 8, - 9, - 24, - 33, - 56, - 65, - 88 - ], - [ - 1, - 8, - 17, - 24, - 25, - 56, - 65, - 72 + 10, + 16, + 57, + 70, + 78, + 84, + 108, + 110 ], [ - 1, - 8, - 17, - 24, - 33, - 40, - 56, - 57 + 2, + 10, + 16, + 32, + 34, + 57, + 70, + 84 ], [ - 0, - 8, 16, - 24, - 25, - 56, - 64, - 72 + 32, + 57, + 68, + 70, + 84, + 100, + 108 ] ], + "classical_graph_identification": { + "required_zero_graph": "K4 joined with the triangular graph T(5)", + "usual_fitting_graph": "four isolated vertices disjoint union Petersen", + "universal_vertices": [ + 16, + 57, + 70, + 84 + ], + "vertex_to_two_subset": { + "2": [ + 0, + 2 + ], + "10": [ + 1, + 2 + ], + "32": [ + 2, + 3 + ], + "34": [ + 2, + 4 + ], + "68": [ + 3, + 4 + ], + "78": [ + 0, + 1 + ], + "100": [ + 0, + 3 + ], + "102": [ + 0, + 4 + ], + "108": [ + 1, + 3 + ], + "110": [ + 1, + 4 + ] + } + }, "incidence_counts": { - "0": 3, - "1": 3, - "8": 6, - "9": 2, - "16": 2, - "17": 2, - "24": 6, - "25": 2, + "2": 2, + "10": 2, + "16": 4, "32": 2, - "33": 2, - "40": 2, - "56": 6, - "57": 2, - "64": 2, - "65": 2, - "72": 2, - "88": 2 + "34": 1, + "57": 4, + "68": 1, + "70": 4, + "78": 2, + "84": 4, + "100": 2, + "102": 1, + "108": 2, + "110": 1 }, "residual_vertices": [ - 0, - 1 + 34, + 68, + 102, + 110 ], - "induced_required_zero_edges": 106, - "symbolic_sandwich_residual": "1=0", + "induced_required_zero_edges": 76, + "block_rank_inequality": "4*d <= 4*(r-8*d), hence r >= 9*d", + "exact_minimum_block_rank": "9*d for every positive integer d", + "exact_fractional_minimum": 9, "upper_dimension": 9, + "block_upper_construction": "the verified binary fitting matrix tensor I_d", "upper_basis_vertex_indices": [ 0, 1, @@ -126,15 +157,15 @@ 56 ], "induced_upper_basis_vertex_indices": [ - 0, - 1, - 8, - 9, + 2, + 10, 16, - 24, - 25, - 56, - 57 + 32, + 34, + 57, + 68, + 70, + 84 ], "field_scope": "Every field of characteristic two, finite or infinite; no symmetry assumption.", "corruption_controls": [ @@ -151,13 +182,28 @@ { "control": "one clique omitted", "outcome": "REJECTED", - "reason": "six clique equations" + "reason": "four clique equations cancel their identities in characteristic two" }, { "control": "edge convention reversed", "outcome": "REJECTED", "reason": "clique requires zeros on BOTH directed off-diagonal matrix entries" }, + { + "control": "odd-incidence set changed", + "outcome": "REJECTED", + "reason": "odd incidence is precisely the displayed four vertices" + }, + { + "control": "required edge inside residual clique removed", + "outcome": "REJECTED", + "reason": "residual projectors mutually annihilate in BOTH directions" + }, + { + "control": "Petersen embedding changed", + "outcome": "REJECTED", + "reason": "exact K4 join triangular-graph structure" + }, { "control": "upper diagonal corrupted", "outcome": "REJECTED", diff --git a/research/p112-characteristic-two-minrank/VERIFY.json b/research/p112-characteristic-two-minrank/VERIFY.json index 17e69440ab..5459ab5804 100644 --- a/research/p112-characteristic-two-minrank/VERIFY.json +++ b/research/p112-characteristic-two-minrank/VERIFY.json @@ -16,7 +16,18 @@ "{package}/verify.py" ], "timeout_seconds": 30, - "checks": "Pinned P112 input, six-clique scalar-rank certificate, all required zeros, full binary Gram matrix and rank-nine upper bounds, seven corruption controls. The general-field and block-rank arguments are human proofs in README." + "checks": "Pinned P112 input, four-clique block-rank certificate, exact induced Petersen-plus-four-isolates graph, all required zeros, full binary Gram matrix and rank-nine upper bounds; ten corruption controls. Universal rank and entropy reductions are human-readable proofs in README." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-O", + "{package}/petersen_lp_verify.py" + ], + "timeout_seconds": 30, + "checks": "Reconstruct 113 valid Petersen Shannon/rank constraint expressions; verify all 1024 rational coefficient sums equal F(empty)-5, five corruption controls, and a perfect-matching positive fixture against all elementary constraints. No LP solver is used." } ] } diff --git a/research/p112-characteristic-two-minrank/petersen_lp_verify.py b/research/p112-characteristic-two-minrank/petersen_lp_verify.py new file mode 100644 index 0000000000..9f07fa0bc6 --- /dev/null +++ b/research/p112-characteristic-two-minrank/petersen_lp_verify.py @@ -0,0 +1,203 @@ +"""Prepared for Thiago with OpenAI GPT-6 Astra and Codex assistance. Apache-2.0. + +Stdlib-only exact verifier for the known Petersen broadcast/rank bound 5. + +No optimization package, floating-point arithmetic, assert statements, or +import of the discovery program is used. See Blasiak--Kleinberg--Lubetzky, +"Index coding via linear programming", Fact 5.6 (1), for prior art. +""" +from collections import Counter +from copy import deepcopy +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations +from pathlib import Path +import json +import sys + + +def require(condition, reason): + if not condition: + raise ValueError(reason) + + +def graph(): + vertices = [list(e) for e in combinations(range(5), 2)] + adjacency = [] + for a in vertices: + mask = 0 + for j, b in enumerate(vertices): + if len(set(a + b)) == 4: + mask |= 1 << j + adjacency.append(mask) + require(all(m.bit_count() == 3 for m in adjacency), "Petersen degrees") + require(all(((adjacency[i] >> j) & 1) == ((adjacency[j] >> i) & 1) + for i in range(10) for j in range(10)), "graph symmetry") + return vertices, adjacency + + +def expression(entry, adjacency): + """Reconstruct a genuine Shannon/rank constraint, never trust stored rows.""" + require(isinstance(entry, dict), "constraint must be a mapping") + kind = entry.get("kind") + require(kind in ("monotone", "slope", "submodular", "decode", "normalize"), + "unknown constraint kind") + expected_keys = {"kind", "multiplier"} + if kind != "normalize": + expected_keys |= {"S", "i"} + if kind == "submodular": + expected_keys.add("j") + require(set(entry) == expected_keys, "constraint keys") + if kind == "normalize": + return {1023: 1}, -10, False + s, i = entry["S"], entry["i"] + require(type(s) is int and 0 <= s < 1024, "subset outside ten vertices") + require(type(i) is int and 0 <= i < 10 and not s & (1 << i), + "added vertex must be absent") + si = s | (1 << i) + if kind == "monotone": + return {si: 1, s: -1}, 0, True + if kind == "slope": + return {s: 1, si: -1}, 1, True + if kind == "decode": + require(adjacency[i] & s == adjacency[i], "decode missing known neighbor") + return {si: 1, s: -1}, 0, False + j = entry["j"] + require(type(j) is int and i < j < 10 and not s & (1 << j), + "submodular vertices must be distinct and absent") + sj, sij = s | (1 << j), si | (1 << j) + return {si: 1, sj: 1, s: -1, sij: -1}, 0, True + + +def verify(certificate): + vertices, adjacency = graph() + require(certificate.get("schema") == "petersen-shannon-rank-lp-dual-v1", "schema") + require(certificate.get("vertices") == vertices, "vertex numbering changed") + constraints = certificate.get("constraints") + require(isinstance(constraints, list) and constraints, "no certificate terms") + total = [Fraction(0) for _ in range(1024)] + constant = Fraction(0) + kinds = Counter() + seen = set() + for entry in constraints: + coefficients, offset, inequality = expression(entry, adjacency) + require(isinstance(entry["multiplier"], str), "multiplier must be exact text") + multiplier = Fraction(entry["multiplier"]) + require(multiplier != 0, "zero certificate term") + require(not inequality or multiplier > 0, "inequality multiplier must be positive") + signature = tuple(sorted((k, v) for k, v in entry.items() if k != "multiplier")) + require(signature not in seen, "duplicate constraint term") + seen.add(signature) + kinds[entry["kind"]] += 1 + for index, value in coefficients.items(): + total[index] += multiplier * value + constant += multiplier * offset + require(total[0] == 1, "wrong coefficient of F(empty)") + require(all(value == 0 for value in total[1:]), "uncancelled subset coefficient") + require(constant == -5, "wrong constant term") + return {"terms": len(constraints), "kinds": dict(sorted(kinds.items())), + "exact_identity": "F(empty) - 5", "subset_coefficients_checked": len(total)} + + +def matching_witness(certificate): + """A five-pair scalar code attains the lower bound over every field.""" + _, adjacency = graph() + + def search(remaining): + if remaining == 0: + return [] + i = (remaining & -remaining).bit_length() - 1 + for j in range(i + 1, 10): + if remaining & adjacency[i] & (1 << j): + rest = search(remaining ^ (1 << i) ^ (1 << j)) + if rest is not None: + return [(i, j)] + rest + return None + + pairs = search(1023) + require(pairs is not None and len(pairs) == 5, "no perfect matching") + pair_masks = [(1 << i) | (1 << j) for i, j in pairs] + require(sum(pair_masks) == 1023, "matching does not partition vertices") + # Broadcast x_i + x_j on each edge. Adding the coordinates in S to its + # five independent rows increases rank once for every pair touched by S. + f = [5 + sum(bool(s & p) for p in pair_masks) for s in range(1024)] + require(f[0] == 5 and f[1023] == 10, "matching endpoint values") + checked_inequalities = 0 + checked_decodes = 0 + for s in range(1024): + absent = [i for i in range(10) if not s & (1 << i)] + for i in absent: + si = s | (1 << i) + require(0 <= f[si] - f[s] <= 1, "matching monotonicity/slope") + checked_inequalities += 2 + if adjacency[i] & s == adjacency[i]: + require(f[si] == f[s], "matching decoding") + checked_decodes += 1 + for i, j in combinations(absent, 2): + require(f[s | (1 << i)] + f[s | (1 << j)] >= + f[s] + f[s | (1 << i) | (1 << j)], "matching submodularity") + checked_inequalities += 1 + for entry in certificate["constraints"]: + coefficients, offset, _ = expression(entry, adjacency) + value = offset + sum(coefficient * f[s] for s, coefficient in coefficients.items()) + require(value == 0, "non-tight term on matching code") + return {"pairs": pairs, "exact_rate": 5, + "all_elementary_inequalities_checked": checked_inequalities, + "all_decoding_equalities_checked": checked_decodes} + + +def negative_controls(certificate): + passed = [] + + def reject(name, candidate): + try: + verify(candidate) + except (ValueError, TypeError, KeyError, ZeroDivisionError): + passed.append(name) + return + raise ValueError("negative control accepted: " + name) + + changed = deepcopy(certificate) + term = changed["constraints"][0] + term["multiplier"] = str(Fraction(term["multiplier"]) + Fraction(1, 8)) + reject("changed_multiplier", changed) + + changed = deepcopy(certificate) + term = next(t for t in changed["constraints"] + if t["kind"] in ("monotone", "slope", "submodular")) + term["multiplier"] = str(-abs(Fraction(term["multiplier"]))) + reject("negative_inequality_multiplier", changed) + + changed = deepcopy(certificate) + term = next(t for t in changed["constraints"] if t["kind"] == "decode") + _, adjacency = graph() + term["S"] &= ~(adjacency[term["i"]] & -adjacency[term["i"]]) + reject("missing_decode_neighbor", changed) + + changed = deepcopy(certificate) + changed["constraints"] = [t for t in changed["constraints"] if t["kind"] != "normalize"] + reject("omitted_normalization", changed) + + changed = deepcopy(certificate) + changed["vertices"][0] = changed["vertices"][1] + reject("changed_graph_numbering", changed) + return passed + + +def main(): + path = (Path(sys.argv[1]) if len(sys.argv) > 1 else + Path(__file__).with_name("PETERSEN-LP-DUAL.json")) + raw = path.read_bytes() + certificate = json.loads(raw) + result = verify(certificate) + result["matching_upper_bound"] = matching_witness(certificate) + result["negative_controls_rejected"] = negative_controls(certificate) + result["certificate_sha256"] = sha256(raw).hexdigest() + result = dict(PASS=True, **result) + Path(__file__).with_name("PETERSEN-VERIFIED.json").write_text( + json.dumps(result, indent=2) + "\n", encoding="utf-8") + print(json.dumps(result, indent=2)) + + +if __name__ == "__main__": + main() diff --git a/research/p112-characteristic-two-minrank/verify.py b/research/p112-characteristic-two-minrank/verify.py index c12575b62c..ed016be1ff 100644 --- a/research/p112-characteristic-two-minrank/verify.py +++ b/research/p112-characteristic-two-minrank/verify.py @@ -4,20 +4,21 @@ Only the Python standard library is used. This module imports no producer, search code, or other verifier. The source supplies integer roots and binary -upper-bound labels; the six displayed clique lists are certificate data. - -Proof over ANY field K of characteristic two: row-normalize a fitting matrix -to M_ii=1. An eight-clique gives rank(M)>=8. If rank(M)=8, factor M=U V^T. -For every eight-clique C, U_C V_C^T=I_8, hence V_C^T U_C=I_8. Thus the -outer products P_i=v_i^T u_i sum to I_8 on C, without assuming symmetry. -The six clique equations have even right-hand side and odd incidence only -at 0 and 1. Consequently P_0=P_1. Sandwiching with u_0 and v_0^T gives -1=M_00^2=M_01 M_10=0. The checker independently verifies that final scalar -polynomial reduction. The nine binary labels embed in every such field. -This proves minrank nine for the specified constraints, not a new exponent. +upper-bound labels; the four displayed clique lists are certificate data. + +Proof for every positive block size d over ANY characteristic-two field: +normalize the diagonal blocks to I_d and factor M_ij=U_i V_j with rank r. +P_i=V_i U_i are rank-d idempotents and mutually annihilate on required-zero +cliques. For an eight-clique C, E_C=I-sum_C P_i has rank r-8d. The four +cliques have odd incidence precisely at a four-clique T. Consequently +sum_C E_C=sum_T P_i has rank 4d, so 4d<=4(r-8d), or r>=9d. Known binary +labels tensored with I_d give the matching upper bound. The checker verifies +the finite inputs and rank-inequality coefficients, not a formalization of +the universal rank lemmas. No symmetry, new circuit or exponent is claimed. """ from collections import Counter from copy import deepcopy +from fractions import Fraction import hashlib from itertools import combinations import json @@ -27,10 +28,13 @@ HERE=Path(__file__).resolve().parent SOURCE=HERE.parents[1]/'research/direct-delivery504-global/inputs/hamming/PROTOTYPE.json' BLOCKS=[ - [0,8,9,24,32,56,64,88], [0,8,16,24,32,40,56,57], - [1,8,9,24,33,56,65,88], [1,8,17,24,25,56,65,72], - [1,8,17,24,33,40,56,57], [0,8,16,24,25,56,64,72], + [2,16,57,70,78,84,100,102], [10,16,57,70,78,84,108,110], + [2,10,16,32,34,57,70,84], [16,32,57,68,70,84,100,108], ] +ODD=[34,68,102,110] +UNIVERSAL=[16,57,70,84] +PETERSEN_PAIRS={2:(0,2),10:(1,2),32:(2,3),34:(2,4),68:(3,4), + 78:(0,1),100:(0,3),102:(0,4),108:(1,3),110:(1,4)} def require(condition,message): @@ -56,26 +60,21 @@ def graph(roots): return edges -def lower(edges,blocks): - require(len(blocks)==6,'six clique equations') +def lower(edges,blocks,odd=ODD): + require(len(blocks)==4 and len(blocks)%2==0,'four clique equations cancel their identities in characteristic two') for block in blocks: require(len(block)==8 and len(set(block))==8,'eight distinct clique vertices') require(all(tuple(sorted((i,j))) in edges for i,j in combinations(block,2)), 'clique requires zeros on BOTH directed off-diagonal matrix entries') counts=Counter(v for block in blocks for v in block) - require(sorted(v for v,c in counts.items() if c%2)==[0,1],'odd incidence is precisely 0 and 1') - require((0,1) in edges,'the residual two vertices require off-diagonal zeros') - # Sandwich sum_C sum_i(v_i^T u_i)=6I by u_0 and v_0^T. - # Each surviving term is M_0i*M_i0, with distinct ordered symbols. - polynomial=Counter({():len(blocks)%2}) - for i,count in counts.items(): - if count%2: - if i==0: - polynomial[()]+=1 # M_00*M_00 = 1 - elif tuple(sorted((0,i))) not in edges: - polynomial[((0,i),(i,0))]+=1 # no symmetry assumed - residual={monomial:c%2 for monomial,c in polynomial.items() if c%2} - require(residual=={():1},'the derived scalar equation must reduce to 1=0') + require(sorted(v for v,c in counts.items() if c%2)==odd,'odd incidence is precisely the displayed four vertices') + require(len(odd)==4 and len(set(odd))==4,'four distinct residual vertices') + require(all(tuple(sorted((i,j))) in edges for i,j in combinations(odd,2)), + 'residual projectors mutually annihilate in BOTH directions') + # rank(sum_T P_i)=|T|*d <= sum_C rank(E_C)=t*(r-8*d). + # This verifies the finite coefficients; the rank lemmas are in README. + require(Fraction(8*len(blocks)+len(odd),len(blocks))==9, + 'exact normalized block-rank bound is nine') return counts @@ -92,6 +91,18 @@ def binary_basis(rows): return indices +def known_graph(edges,vertices,pairs=PETERSEN_PAIRS): + require(set(vertices)==set(UNIVERSAL)|set(pairs),'the displayed graph partition is exact') + require(sorted(tuple(sorted(p)) for p in pairs.values())==list(combinations(range(5),2)), + 'the ten vertices represent all two-subsets of a five-set') + for i,j in combinations(vertices,2): + required=(i in UNIVERSAL or j in UNIVERSAL or bool(set(pairs[i])&set(pairs[j]))) + require(((i,j) in edges)==required,'exact K4 join triangular-graph structure') + return dict(required_zero_graph='K4 joined with the triangular graph T(5)', + usual_fitting_graph='four isolated vertices disjoint union Petersen', + universal_vertices=UNIVERSAL,vertex_to_two_subset=pairs) + + def upper(roots,labels,edges): require(len(labels)==112 and all(type(x) is int and 0 Date: Wed, 14 Oct 2026 07:18:32 -0300 Subject: [PATCH 3/3] Certify the selected P111 corollary by exact root reflection --- .../P111-VERIFIED.json | 110 ++++++++++++++ .../p112-characteristic-two-minrank/README.md | 54 ++++++- .../SOURCES.json | 6 + .../p112-characteristic-two-minrank/TASK.json | 16 +- .../VERIFY.json | 14 +- .../p111_corollary.py | 139 ++++++++++++++++++ 6 files changed, 324 insertions(+), 15 deletions(-) create mode 100644 research/p112-characteristic-two-minrank/P111-VERIFIED.json create mode 100644 research/p112-characteristic-two-minrank/p111_corollary.py diff --git a/research/p112-characteristic-two-minrank/P111-VERIFIED.json b/research/p112-characteristic-two-minrank/P111-VERIFIED.json new file mode 100644 index 0000000000..8392bb8741 --- /dev/null +++ b/research/p112-characteristic-two-minrank/P111-VERIFIED.json @@ -0,0 +1,110 @@ +{ + "status": "PASS_SELECTED_P111_BLOCK_RANK_AND_BINARY_BROADCAST_9D", + "prototype_sha256": "327d2a868043e846381aa58a33053c24425e8cad522ff401b10ec8af1d649a3f", + "selected_word_sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f", + "vertices": 111, + "required_zero_unordered_edges": 2870, + "binary_gram_entries": 12321, + "reflection": "negate coordinate 1, using zero-based coordinate indices", + "P112_to_P111_witness_map": { + "2": 12, + "10": 16, + "16": 26, + "32": 38, + "34": 40, + "57": 63, + "68": 69, + "70": 71, + "78": 74, + "84": 84, + "100": 99, + "102": 97, + "108": 107, + "110": 109 + }, + "cliques": [ + [ + 12, + 26, + 63, + 71, + 74, + 84, + 99, + 97 + ], + [ + 16, + 26, + 63, + 71, + 74, + 84, + 107, + 109 + ], + [ + 12, + 16, + 26, + 38, + 40, + 63, + 71, + 84 + ], + [ + 26, + 38, + 63, + 69, + 71, + 84, + 99, + 107 + ] + ], + "odd_incidence": [ + 40, + 69, + 97, + 109 + ], + "induced_witness_vertices": 14, + "outside_messages_fixed_for_entropy_argument": 97, + "all_field_block_rank_lower_bound": "9*d for every positive integer d", + "characteristic_two_block_rank_and_binary_broadcast": "exactly 9*d", + "corruption_controls": [ + { + "control": "P111 source bytes changed", + "outcome": "REJECTED", + "reason": "source SHA-256" + }, + { + "control": "reflection map vertex changed", + "outcome": "REJECTED", + "reason": "coordinate-one sign reflection into selected P111" + }, + { + "control": "root norm changed", + "outcome": "REJECTED", + "reason": "integer E8 root coordinates" + }, + { + "control": "induced required-zero edge omitted", + "outcome": "REJECTED", + "reason": "exact induced four-isolates-plus-Petersen fitting graph" + }, + { + "control": "binary diagonal changed", + "outcome": "REJECTED", + "reason": "nine-coordinate binary labels" + }, + { + "control": "binary labels truncated to eight coordinates", + "outcome": "REJECTED", + "reason": "odd binary diagonal" + } + ], + "scope": "Finite embedding and upper-bound checks plus the same written Petersen rank/entropy reduction. No new native word, paid supplier saving or multiplication-exponent improvement." +} diff --git a/research/p112-characteristic-two-minrank/README.md b/research/p112-characteristic-two-minrank/README.md index 11f9d3c1f4..387df8b87d 100644 --- a/research/p112-characteristic-two-minrank/README.md +++ b/research/p112-characteristic-two-minrank/README.md @@ -1,11 +1,16 @@ -# P112 block-rank and binary broadcast certificates +# P111 and P112 block-rank and binary broadcast certificates -For the pinned 112-port graph, every fitting matrix with invertible d-by-d +For both the selected 111-port graph and the pinned 112-port graph, every +fitting matrix with invertible d-by-d diagonal blocks has rank at least **9d over every field**, for every positive integer d. The existing binary labels attain 9d over every characteristic-two field. In the corresponding side-information graph, even nonlinear zero-error codes for d-bit messages require exactly **9d broadcast bits**. +The selected P111 corollary is checked directly against the PR589 native-word +input. It does not assume that P111 is a subset of this particular P112: +a coordinate reflection places the same 14-vertex witness inside P111. + A source-pinned induced graph on 14 vertices certifies these statements: in the usual fitting/side-information convention it is four isolated vertices disjoint from the Petersen graph. Petersen's broadcast rate five is known from @@ -70,6 +75,34 @@ exactly when their subsets intersect. Consequently the induced graph in G is four isolated vertices plus the Petersen graph, whose edges join disjoint two-subsets. This is an explicit isomorphism, not a degree-sequence inference. +## Corollary for the selected P111 supplier + +The current bit supplier uses the 111 labels in +[bitE8mut-p111-tuned.json.gz](../e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz), +SHA256 e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f. +Negate coordinate 1 (zero-based) of each of the fourteen P112 witness roots. +Up to the sign of a root line, the resulting P111 indices are: + +~~~text +P112: 2 10 16 32 34 57 68 70 78 84 100 102 108 110 +P111: 12 16 26 38 40 63 69 71 74 84 99 97 107 109 +~~~ + +[p111_corollary.py](p111_corollary.py) reads both pinned inputs without importing +another verifier. It checks the reflection, every induced pair, the four +eight-cliques and odd-incidence four-clique directly. The same all-field rank +proof and nonlinear entropy proof therefore apply; the latter fixes 97 +outside messages instead of 98. Matching the P111 root lines to the inherited +full 120-label binary construction verifies all 12,321 Gram entries, all +2,870 required-zero pairs, and exact rank nine. Thus both full graphs have +block rank exactly 9d in characteristic two and binary broadcast length +exactly 9d for every positive d. Only their all-field lower bound is asserted. + +Six corruption controls and the finite source-bound receipt are recorded in +[P111-VERIFIED.json](P111-VERIFIED.json). This rules out below-nine fitting or +broadcast compression for the selected label graph, but gives no lower bound +on its complete paid supplier cost and no new native circuit. + ## Short proof in characteristic two Factor a normalized fitting block matrix as M_ij=U_i V_j with rank r, @@ -198,10 +231,11 @@ python3.12 scripts/research_package.py --package research/p112-characteristic-tw python3.12 scripts/research_package.py --package research/p112-characteristic-two-minrank ~~~ -The registered replay runs both verifiers with -I -B -O. Explicit exceptions +The registered replay runs all three verifiers with -I -B -O. Explicit exceptions keep acceptance checks active with assertions disabled. The deterministic receipts are [VERIFIED.json](VERIFIED.json) and -[PETERSEN-VERIFIED.json](PETERSEN-VERIFIED.json). +[PETERSEN-VERIFIED.json](PETERSEN-VERIFIED.json), and +[P111-VERIFIED.json](P111-VERIFIED.json). The graph verifier imports no producer, search program or other verifier. It checks the source hash and indexing, all 2,912 required-zero pairs, all @@ -211,6 +245,8 @@ The separate dual verifier checks all 1,024 rational coefficient sums and rejects five corruptions, including a negative inequality multiplier and an invalid decoding condition. Its perfect-matching positive fixture checks all 21,760 elementary inequalities and all 640 decoding equalities. +The P111 checker independently checks its new input and reflected embedding, +the full binary Gram matrix, and six further corruption controls. The reductions from rank and entropy to these finite certificates are the proofs above. No formal proof assistant, full supplier replay or selected @@ -220,7 +256,7 @@ frontier replay is claimed. [Discussion 1713](https://github.com/CrocSwap/integer-mult-bounds/discussions/1713) records the scoped result. The complete remote overlap refresh on -2026-10-14 at 09:32 UTC covered 442 open PRs and 409 Discussions, including +2026-10-14 at 10:16 UTC covered 460 open PRs and 435 Discussions, including comments and replies. Sparse-checkout local coverage was limited. [PR1471](https://github.com/CrocSwap/integer-mult-bounds/pull/1471), head 3695ad16e7bc4c0f6248a9e5a64fc069fa096733, audits odd-characteristic portability @@ -235,7 +271,7 @@ Leung, Laura Mancinska, William Matthews, Maris Ozols and Aidan Roy, [Entanglement can increase asymptotic rates of zero-error classical communication over classical channels](https://arxiv.org/abs/1009.1195), Theorem 9 and section 4, explain the symplectic construction and E8 embedding, crediting Peeters for the symplectic-graph result. The contribution here is -the pinned P112 embedding, the four-clique certificate, and independent exact +the pinned P112 and selected P111 embeddings, the four-clique certificate, and independent exact checks of the resulting scoped obstructions; no literature-wide novelty claim for the underlying parameters is asserted. @@ -246,6 +282,12 @@ from the PR523/514/507/425/433 lineage credited in that package's [NOTICE.md](../direct-delivery504-global/NOTICE.md). Inputs are referenced without modification or re-vendoring. +The selected P111 input is the unchanged PR589 tuned word, built on eumemic's +PR555 word and the PR543/545 lineage, with substantial Anthropic Claude assistance credited in +[e8-bit-p111-tuned](../e8-bit-p111-tuned/README.md). Its native construction is +used only as a source of the exact live root labels here; its authors retain +credit for the word and its supplier results. + Prepared for Thiago with substantial OpenAI GPT-6 Astra and Codex assistance for exploration, proof review, independent checking and packaging. New work is Apache-2.0; retained source attribution and licenses remain applicable. diff --git a/research/p112-characteristic-two-minrank/SOURCES.json b/research/p112-characteristic-two-minrank/SOURCES.json index 06ada17171..7540fa9f45 100644 --- a/research/p112-characteristic-two-minrank/SOURCES.json +++ b/research/p112-characteristic-two-minrank/SOURCES.json @@ -19,6 +19,12 @@ "usage": "input", "git_blob": "9efe30ee107b9c67f15f1c726e1a1cb5cef03929", "sha256": "327d2a868043e846381aa58a33053c24425e8cad522ff401b10ec8af1d649a3f" + }, + { + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" } ] } diff --git a/research/p112-characteristic-two-minrank/TASK.json b/research/p112-characteristic-two-minrank/TASK.json index c99100b106..f860377eff 100644 --- a/research/p112-characteristic-two-minrank/TASK.json +++ b/research/p112-characteristic-two-minrank/TASK.json @@ -42,13 +42,13 @@ ] }, "scope_status": "changed", - "actual_scope": "Source-pinned induced Petersen-plus-four-isolates certificate: block fitting rank at least 9d over every field, equality in characteristic two, and exact nonlinear zero-error binary broadcast length 9d for every positive block size d.", + "actual_scope": "Source-pinned induced Petersen-plus-four-isolates certificates for both selected P111 and pinned P112: block fitting rank at least 9d over every field, equality in characteristic two, and exact nonlinear zero-error binary broadcast length 9d for every positive block size d.", "scope_change_reason": "The helper-inventory investigation raised a necessary rank-eight label premise. This side result isolates the obstruction, strengthens it to all block sizes and binary nonlinear coding, and identifies its known Petersen-theorem basis; it supplies no new helper inventory.", "bottleneck_link": "Closes below-nine fitting compression of this exact graph over every field and binary nonlinear broadcast compression at every block size. A positive supplier must change the graph/constraints or save other paid work; no kappa improvement follows.", "budget_minutes": 75, - "stop_rule": "Finish this side result after source-pinned embedding, exact rational dual, independent characteristic-two proof, registered replays, and explicit prior-art/scope checks.", + "stop_rule": "Finish this side result after source-pinned embedding, exact rational dual, independent characteristic-two proof, registered replays, and explicit prior-art/scope checks. Include the directly checked selected-P111 reflection corollary.", "outcome": "completed", - "evidence": "Four eight-cliques on 14 vertices have odd incidence at a four-clique, proving 4d<=4(r-8d) in characteristic two. The induced usual fitting graph is four isolates plus Petersen. A 113-term exact rational certificate proves the known Petersen bound five and extends the full lower bound to all fields and nonlinear zero-error codes. Independent standard-library replays check all 2912 required-zero pairs, 12544 binary Gram entries, all 1024 dual coefficients, a matching positive fixture, and 15 corruption controls.", + "evidence": "Four eight-cliques on 14 vertices have odd incidence at a four-clique, proving 4d<=4(r-8d) in characteristic two. The induced usual fitting graph is four isolates plus Petersen. A 113-term exact rational certificate proves the known Petersen bound five and extends the full lower bound to all fields and nonlinear zero-error codes. Independent standard-library replays check all 2912 required-zero pairs, 12544 binary Gram entries, all 1024 dual coefficients, a matching positive fixture, and 15 corruption controls. A separate checker proves the selected P111 corollary by an exact coordinate reflection of the fourteen-vertex witness, verifies all 2,870 required-zero pairs and 12,321 binary Gram entries, and rejects six further corruptions. The nonlinear reduction fixes 97 outside messages for P111.", "author": "Thiago, with OpenAI GPT-6 Astra and Codex assistance", "ai_assistance": "Substantial OpenAI GPT-6 Astra and Codex assistance was used for mathematical exploration, independent checking, literature search, implementation and packaging.", "open_questions": [ @@ -61,17 +61,17 @@ ], "coordination": { "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1713", - "overlap_checked_at": "2026-10-14T09:32:07.988435+00:00", + "overlap_checked_at": "2026-10-14T10:16:32.419039+00:00", "coverage": { "open_prs": { - "fetched_at": "2026-10-14T09:30:20.286086+00:00", + "fetched_at": "2026-10-14T10:14:58.185262+00:00", "complete_pagination": true, - "records": 442 + "records": 460 }, "discussions": { - "fetched_at": "2026-10-14T09:32:07.925671+00:00", + "fetched_at": "2026-10-14T10:16:32.336110+00:00", "complete_pagination": true, - "records": 409 + "records": 435 } }, "nearest_overlap": { diff --git a/research/p112-characteristic-two-minrank/VERIFY.json b/research/p112-characteristic-two-minrank/VERIFY.json index 5459ab5804..8c6ee42249 100644 --- a/research/p112-characteristic-two-minrank/VERIFY.json +++ b/research/p112-characteristic-two-minrank/VERIFY.json @@ -4,7 +4,8 @@ "python": "3.12", "requirements": [], "inputs": [ - "research/direct-delivery504-global/inputs/hamming/PROTOTYPE.json" + "research/direct-delivery504-global/inputs/hamming/PROTOTYPE.json", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz" ], "commands": [ { @@ -28,6 +29,17 @@ ], "timeout_seconds": 30, "checks": "Reconstruct 113 valid Petersen Shannon/rank constraint expressions; verify all 1024 rational coefficient sums equal F(empty)-5, five corruption controls, and a perfect-matching positive fixture against all elementary constraints. No LP solver is used." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-O", + "{package}/p111_corollary.py" + ], + "timeout_seconds": 30, + "checks": "Selected P111 source pin, exact reflected fourteen-vertex embedding and clique certificate, all 2,870 required-zero pairs and 12,321 binary Gram entries, exact rank-nine upper bound and six corruption controls; inherits the documented universal Petersen rank/entropy reduction." } ] } diff --git a/research/p112-characteristic-two-minrank/p111_corollary.py b/research/p112-characteristic-two-minrank/p111_corollary.py new file mode 100644 index 0000000000..e69ea264a1 --- /dev/null +++ b/research/p112-characteristic-two-minrank/p111_corollary.py @@ -0,0 +1,139 @@ +"""Prepared for Thiago with OpenAI GPT-6 Astra and Codex assistance. Apache-2.0. + +Independently check the selected P111 corollary from two pinned raw inputs. +No other verifier or producer is imported. The universal rank/entropy proof +is the same Petersen reduction in README; this checks its new finite inputs. +""" +from collections import Counter +from itertools import combinations +from pathlib import Path +import gzip +import hashlib +import json + +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] +PROTOTYPE=ROOT/'research/direct-delivery504-global/inputs/hamming/PROTOTYPE.json' +WORD=ROOT/'research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz' +PROTOTYPE_PIN='327d2a868043e846381aa58a33053c24425e8cad522ff401b10ec8af1d649a3f' +WORD_PIN='e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f' +MAP={2:12,10:16,16:26,32:38,34:40,57:63,68:69,70:71, + 78:74,84:84,100:99,102:97,108:107,110:109} +CLIQUES=[[2,16,57,70,78,84,100,102],[10,16,57,70,78,84,108,110], + [2,10,16,32,34,57,70,84],[16,32,57,68,70,84,100,108]] +UNIVERSAL=[16,57,70,84] +PAIRS={2:(0,2),10:(1,2),32:(2,3),34:(2,4),68:(3,4), + 78:(0,1),100:(0,3),102:(0,4),108:(1,3),110:(1,4)} + +def need(test,message): + if not test:raise ValueError(message) + +def pinned(raw,pin): + need(hashlib.sha256(raw).hexdigest()==pin,'source SHA-256') + +def canonical(root): + return max(tuple(root),tuple(-x for x in root)) + +def graph(roots): + need(len(roots)==111,'selected P111 vertex count') + need(len({canonical(r) for r in roots})==111,'distinct root lines') + need(all(len(r)==8 and all(type(x) is int for x in r) + and sum(x*x for x in r)==4 for r in roots),'integer E8 root coordinates') + edges=set() + for i,j in combinations(range(111),2): + dot=sum(a*b for a,b in zip(roots[i],roots[j])) + need(dot in (-2,0,2),'normalized integral Gram off diagonal') + if dot:edges.add((i,j)) + return edges + +def embedding(original,roots,edges,mapping): + need(set(mapping)==set(UNIVERSAL)|set(PAIRS),'all fourteen witness vertices') + need(len(set(mapping.values()))==14,'injective witness map') + for old,new in mapping.items(): + reflected=list(original[old+8]);reflected[1]*=-1 + need(0<=new<111 and canonical(reflected)==canonical(roots[new]), + 'coordinate-one sign reflection into selected P111') + for i,j in combinations(sorted(mapping),2): + want=i in UNIVERSAL or j in UNIVERSAL or bool(set(PAIRS[i])&set(PAIRS[j])) + got=tuple(sorted((mapping[i],mapping[j]))) in edges + need(got==want,'exact induced four-isolates-plus-Petersen fitting graph') + mapped=[[mapping[i] for i in c] for c in CLIQUES] + for clique in mapped: + need(len(set(clique))==8 and all(tuple(sorted(p)) in edges + for p in combinations(clique,2)),'four eight-cliques') + incidence=Counter(i for c in mapped for i in c) + odd=sorted(i for i,c in incidence.items() if c%2) + need(odd==sorted(mapping[i] for i in [34,68,102,110]),'four-clique odd incidence') + need(all(tuple(sorted(p)) in edges for p in combinations(odd,2)), + 'residual four-clique') + return mapped,odd + +def rank_binary(rows): + basis={} + for value in rows: + while value: + p=value.bit_length()-1 + if p in basis:value^=basis[p] + else:basis[p]=value;break + return len(basis) + +def upper(roots,labels,edges): + need(len(labels)==111 and all(type(x) is int and 0