From 9380f458ee4409acfcf580eaf8b06ff5815ba4e0 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 10:15:52 +0000 Subject: [PATCH] feat(research): classify shared A2 rank-six equality supports --- research/e8-a2-shared-equality/PROOF.md | 189 ++++++++++++++++ research/e8-a2-shared-equality/README.md | 119 ++++++++++ research/e8-a2-shared-equality/SOURCES.json | 30 +++ research/e8-a2-shared-equality/TASK.json | 104 +++++++++ research/e8-a2-shared-equality/VERIFY.json | 35 +++ research/e8-a2-shared-equality/independent.py | 105 +++++++++ research/e8-a2-shared-equality/verify.py | 214 ++++++++++++++++++ 7 files changed, 796 insertions(+) create mode 100644 research/e8-a2-shared-equality/PROOF.md create mode 100644 research/e8-a2-shared-equality/README.md create mode 100644 research/e8-a2-shared-equality/SOURCES.json create mode 100644 research/e8-a2-shared-equality/TASK.json create mode 100644 research/e8-a2-shared-equality/VERIFY.json create mode 100644 research/e8-a2-shared-equality/independent.py create mode 100644 research/e8-a2-shared-equality/verify.py diff --git a/research/e8-a2-shared-equality/PROOF.md b/research/e8-a2-shared-equality/PROOF.md new file mode 100644 index 0000000000..459df21220 --- /dev/null +++ b/research/e8-a2-shared-equality/PROOF.md @@ -0,0 +1,189 @@ +# Exactly three A2 fibers share each rank-six equality support + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement and inherited premises + +Use the full E8 root-line labels R in F2^9 from PR3288, with leading +coordinate one. For a 27-root projective A2 fiber F and a binary space V +of dimension at most six, write + +``` +J_F(V) = |R intersect V| + |F intersect V|. +``` + +PR3262 and PR3288 supply the individual bound J_F(V)<=32. PR3288 also +supplies its equality characterization and the count of 27 equality +six-spaces for each of the 3,360 distinct fibers. These are cited premises. +This package does not independently audit their proofs or model census. + +**Theorem.** If J_F(V)=32 for at least one fiber, then exactly three +distinct A2 fibers satisfy J_F(V)=32 for this same V. Two distinct fibers +share at most one equality six-space. Consequently there are exactly +30,240 equality six-spaces in total, and every fiber shares equality with +exactly 54 other fibers. A fourth distinct fiber cannot saturate the +individual bound on that same support. + +The theorem concerns this finite full-E8 configuration. It does not say that +pairwise compatibility of several fibers forces a common equality space. + +## A2 fibers in the quadratic model + +Write E=F2^8, with the nondegenerate plus quadratic form q and polar form +B(x,y)=q(x+y)+q(x)+q(y). Root lines correspond to q(x)=1, with label +(1,x). An A2 root plane gives an anisotropic binary two-space N. Its three +nonzero vectors all have q=1. For p in N minus {0}, put + +``` +K = N-perp, +H(N,p) = p+K, +F(N,p) = {x in H(N,p):q(x)=1} minus {p}. +``` + +These are the 27-root fibers in the inherited model. To see the parity +identification, choose two roots of an A2 plane. The mod-two evaluation +against them has one zero class and three nonzero classes. Each nonzero +class contains its unique A2 root p and the corresponding large +projective evaluation fiber. The original real fibers have sizes +36,27,27,27,1,1,1, as recorded in the pinned predecessor. Distinct pairs +(N,p) give distinct affine sections and fibers. + +The Gauss sum on N is -2. Its orthogonal complement K has Gauss sum -8, +since the ambient sum is +16. Translation by the orthogonal root p gives +sum_(x in H(N,p)) (-1)^q(x)=+8. Thus H contains 28 roots, including p. +The predecessor's seven-dimensional binary span is the homogenization of +H. Its equality six-spaces have affine sections A=a+L of dimension five, +contain 16 roots, and avoid p. + +## The singular radical of an equality section + +Fix one equality section A=a+L inside H(N,p). The hyperplane L in the +nondegenerate six-space K has a one-dimensional radical . Equivalently, +L is the kernel of B(-,r) on K, for a unique nonzero r in K. Since the +form is alternating, r belongs to L. + +The affine hyperplane A avoids p, so B(a-p,r)=1. As p is orthogonal to K, + +``` +B(a,r)=1. +``` + +The root count 16 says that the signed quadratic sum on A is zero. The +quadratic restriction identity from PR3288, or its direct squared-sum +calculation, gives + +``` +(sum_(x in A) (-1)^q(x))^2 + = 32 [1+(-1)^(q(r)+B(a,r))]. +``` + +It follows that q(r)=0. Hence + +``` +U = L-perp = N direct-sum +``` + +has dimension three, radical , and q(r)=0. Its quotient by the radical +is the anisotropic plane N. + +## Four complementary planes, three admissible projections + +Every other fiber F(N',p') containing all 16 roots of this equality +six-space has A contained in H(N',p'), by the inherited equality +characterization. Therefore N' is contained in U. An anisotropic two-space +in U is a complement to . Conversely every complement is anisotropic, +because q descends to the anisotropic quotient U/. + +There are exactly four complements. Relative to U=N direct-sum , they +are the graphs + +``` +N_f = {u+f(u)r:u in N}, f in Hom(N,F2). +``` + +For each complement let p_f be the unique orthogonal projection of a +onto N_f. The condition p_f=0 is that B(a,-) vanish on N_f. On a graph, + +``` +B(a,u+f(u)r) = B(a,u)+f(u), +``` + +because B(a,r)=1. Exactly one f makes this functional zero. For that +complement p_f=0, which is not an A2 root and does not define a large +fiber. For each of the remaining three complements, p_f is nonzero and +q(p_f)=1. + +Each of those three affine sections H(N_f,p_f) contains A. Also p_f is +not in A, since B(p_f,r)=0 whereas B(x,r)=1 for every x in A. Thus every +root of A lies in F(N_f,p_f), giving joint score 32. Conversely the +previous paragraph exhausts every possible fiber. This proves exactly +three, including the initially chosen fiber. + +The 16 roots determine their affine five-space A. Otherwise they would +fill an affine four-space on which q is constant one. Its direction would +be a four-dimensional totally isotropic subspace of L. But L has radical +dimension one and nondegenerate quotient dimension four, so its largest +totally isotropic subspace has dimension three. This is impossible. +Homogenizing shows that the roots determine V as well. + +## Pairwise uniqueness and the counts + +Distinct fibers have distinct seven-dimensional binary spans W_F. +Indeed the leading-one section determines N-perp and then N, and its +orthogonal projection determines p. If two distinct fibers share an +equality V, then V is contained in the intersection of their two spans. +That intersection has dimension at most six, so it is exactly V. Hence +the shared equality space is unique. + +Double-counting the inherited 3,360 times 27 incidences now gives + +``` +number of equality spaces = 3360*27/3 = 30240. +neighbors of each fiber = 27*(3-1) = 54. +compatible unordered fiber pairs = 3360*54/2 = 90720. +``` + +Pairwise uniqueness is needed in the second count, to prevent counting a +neighbor twice. These counts do not enumerate arbitrary cliques in the +pairwise compatibility graph. + +## Explicit witness and verification boundary + +In the pinned simple-root encoding, one common equality support is + +``` +[3,11,27,31,39,47,59,63,71,79,83,87,103,111,123,127]. +``` + +The three anisotropic normal planes, listed by their nonzero eight-bit +vectors before homogenization, and their omitted singleton points are + +``` +N={84,128,212}, p=128; +N={84,134,210}, p=210; +N={82,134,212}, p=82. +``` + +The verifier uses q0(x)=x0*x1+x2*x3+x4*x5+x6*x7. The columns +`[3,6,18,34,76,78,130,208]` give an explicit invertible transport to the +pinned simple-root quadratic polynomial. All 256 values are compared. +No P112 membership or caller compatibility is asserted for this witness. + +The primal enumeration visits the hyperplanes of each inherited fiber +span and constructs the new cross-fiber incidence. The separate dual +enumeration visits every U=N+ above, its four complementary planes and +the four cosets of U-perp with B(a,r)=1. They agree on every support and +every incident (N,p), not only totals. All 30,240 zero-projection exclusions +are checked. The code does not import or run predecessor executable code. + +The new written proof and finite certificate are author-checked evidence. +Independent human and formal proof-kernel review are unclaimed. The +predecessor's individual bounds and E8 binding remain cited dependencies. +No shortening threshold, physical circuit, paid moment, kappa or complete +multiplication theorem is derived. + +Credit Nick Petalas / PR3288, PR3280 and PR3262, David Arias's quadratic +model, DreamingOfClouds / PR3154, joaqcoo and the retained E8/P112 lineage. +Quadratic-form restriction identities and binary symplectic linear algebra +are classical. The new step is the simultaneous three-fiber classification +and its incidence consequences. diff --git a/research/e8-a2-shared-equality/README.md b/research/e8-a2-shared-equality/README.md new file mode 100644 index 0000000000..1705b6d76a --- /dev/null +++ b/research/e8-a2-shared-equality/README.md @@ -0,0 +1,119 @@ +# Exactly three A2 fibers share each rank-six equality support + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped written mathematical proof with an exact finite +certificate. For the full E8 leading-one root labels, every binary +rank-six support attaining the individual joint bound 32 for one 27-root +A2 fiber attains it for exactly three distinct fibers. A fourth distinct +fiber cannot attain 32 on that same support. Two distinct fibers share +at most one equality six-space. + +There are 30,240 equality supports, each with three incidences. Every one +of the 3,360 fibers has exactly 54 compatible neighbors. The individual +bound, its 27 equality spaces per fiber and the E8 model remain credited +premises from PR3288 and its predecessors. This contribution answers the +separate simultaneous-equality opening, with a new three-projection proof +and complete cross-fiber incidence. + +[PROOF.md](PROOF.md) gives the theorem, the exact hypotheses and a literal +16-root attainer. The primal enumeration constructs equality hyperplanes +inside fiber spans. The separate dual enumeration constructs singular +radical three-spaces and their affine cosets. They compare every support +and every incident fiber. They share the specified quadratic model, but +neither imports predecessor executable code. This is separate +combinatorial checking, not independent human review. + +## Reproduce + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/research_package.py --package research/e8-a2-shared-equality +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/e8-a2-shared-equality/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/e8-a2-shared-equality/verify.py +``` + +The registered replay runs both direct commands. Expected status is +`PASS_A2_SHARED_EQUALITY`, with 30,240 supports, multiplicity three and +54 neighbors per fiber. The complete canonical incidence SHA256 is +`be65d72f039eaf568a318133a63a07166d6cf29e1d1d0ee5254f57741f393b62`. +The optional `--receipt /absolute/path/outside/checkout.json` writes a +generated receipt bound to package and input hashes. Receipt files and +other run outputs belong outside the checkout. + +The dual enumeration covers 7,560 radical three-spaces, 30,240 affine +cosets and every zero-projection exclusion. The primary checker also +checks the explicit simple-root transport at all 256 points, the witness +rank, a genuine balanced hyperplane containing its omitted singleton +whose joint score is 31, and four invalid binary domains. Explicit +exceptions preserve these checks under optimized Python. + +## Scope and source status + +The individual-fiber results are cited dependencies, not this deliverable's +audit targets. [SOURCES.json](SOURCES.json) pins their proof and the exact +simple-root convention. These inputs are authenticated as bytes, without +executing their verifiers. Historical catalogue and selected-result pins +are provenance. No unmerged source commit or network is needed at replay. + +This full-E8 theorem supplies no new P112 threshold, pairwise-clique +classification, actual decoder or physical caller, native program, +restoration implementation, paid moment, kappa or selected-frontier change. +The five selected framework assumptions remain. Predecessor scientific +replays, selected cold replay, Lean and Docker were not run. Independent +human and formal proof-kernel review are unclaimed. + +This is a changed `complex-rank-shape-decoder` card and a scoped +support-geometry side result. A real caller must specify its fibers and +show that they require saturation on one common support before this +obstruction can affect its budget. A finite compatibility improvement +does not authorize a further construction campaign. + +## Implementation bounds + +All mathematical domains are fixed subsets of F2^8 or F2^9. The primal +loops through 3,360 fibers and at most 127 hyperplanes of each. It retains +30,240 support keys, 90,720 incidences and at most 90,720 compatibility +pairs. The dual loops through at most 255 radical candidates and 1,120 +normal planes, then eight cosets for each of 7,560 three-spaces. Every +point scan has 256 iterations. Basis construction has at most 512 input +vectors and nine pivots. There is no recursion, subprocess, network, +dynamic code evaluation or unbounded input search. + +Power of Ten rule 3 deviation: CPython allocates integers, tuples and +dictionaries during these bounded finite enumerations. The fixed domains +bound collection sizes; this is not a fixed-allocation implementation or +a certified Python allocator bound. All functions are below sixty lines. +Warning-strict normal and optimized execution are the available local +diagnostics. No separately installed linter or formal proof checker is +claimed. + +## Open next questions + +- Which pairwise-compatible triples actually share an equality space? + Start with the explicit compatibility graph and the support triples. + No clique classification is provided here. +- Does a named current decoder or caller require four distinct fibers to + attain their individual maxima on the same rank-six support? First bind + its literal support and complete paid invoice. No such caller is supplied. + +Discovery stopped at the first verified simultaneous-compatibility result. + +## Credit and coordination + +Credit Nick Petalas / PR3288, PR3280 and PR3262, David Arias's quadratic +model, DreamingOfClouds / PR3154, joaqcoo and the retained E8/P112 lineage. +Quadratic restriction and binary symplectic linear algebra are classical. +No global literature-priority claim is made. PR3302 concerns outside-span +capacity 30 and supplies no simultaneous equality result used here. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19371205) +states the delivered question. Base main is +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision eight, +selected PR6030. The overlap snapshot covered 522 open PRs, 6,536 +Discussion records and all 8,917 tracked local notes. Main/merged object +and general-form searches, account history and current reservations were +also checked. Arbitrary historical diffs and unpublished work remain +coverage limits. Metadata and archive retention do not imply scientific +acceptance or a selected-frontier update. diff --git a/research/e8-a2-shared-equality/SOURCES.json b/research/e8-a2-shared-equality/SOURCES.json new file mode 100644 index 0000000000..8e612bcd76 --- /dev/null +++ b/research/e8-a2-shared-equality/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/e8-a2-analytic-rank6/PROOF.md", + "usage": "input", + "git_blob": "8a7cc2e989101322f289bb98102ff40097841779", + "sha256": "4347eeee7c0986ffa1ae51d02ae67b4ed4554fc389a89c4423aff994a753546a" + }, + { + "path": "research/p112-root-simplex-exclusion/geometry.py", + "usage": "input", + "git_blob": "222ea556faf2b275f73815c4e7d0d5f1e3294f2f", + "sha256": "b8ac379e41f5ad83bdb6c7f7c55129fc3d9c07801ea61591478f25d72ff0b021" + } + ] +} diff --git a/research/e8-a2-shared-equality/TASK.json b/research/e8-a2-shared-equality/TASK.json new file mode 100644 index 0000000000..13402e76de --- /dev/null +++ b/research/e8-a2-shared-equality/TASK.json @@ -0,0 +1,104 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exactly three distinct A2 fibers share every rank-six equality support in full E8; pairwise uniqueness, 30240 supports and degree 54.", + "scope_change_reason": "Take PR3288’s expressly open simultaneous-equality question, rather than replay its individual-fiber bound. This is a scoped support-geometry side result, not a complete supplier.", + "bottleneck_link": "Simultaneous equality is required before individual support capacities can be treated as jointly attainable in a decoder or caller. Four distinct fibers cannot all saturate on the same rank-six support.", + "budget_minutes": 60, + "stop_rule": "Stop discovery at the first verified compatibility result. Package the theorem, one literal witness and complete cross-incidence certificate; leave changed ranks, cliques and physical callers open.", + "outcome": "completed", + "evidence": "PROOF.md gives the four-complement/three-projection proof. Primal hyperplane and dual radical-coset enumerations compare every support and every incident fiber.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which pairwise-compatible triples share a common equality space?", + "why_it_matters": "The theorem classifies simultaneous incidence, but pairwise compatibility is a weaker condition.", + "first_step": "Compare the three neighbors attached to a common support with triangles in the explicit 3360-vertex compatibility graph.", + "blocked_by": "No clique classification or caller-specific compatibility constraints are supplied." + }, + { + "question": "Does a named current decoder or caller require four distinct A2 fibers to saturate on one rank-six support?", + "why_it_matters": "Such a contract would be excluded by the new theorem; separate individual capacities are insufficient.", + "first_step": "Bind its literal fibers, support, ranks and complete paid invoice before applying this obstruction.", + "blocked_by": "No actual physical caller or changed paid profile is constructed here." + } + ], + "source_question": { + "pr": 3288, + "author": "petalas", + "head": "c375ed42aabf1b8cdcaae0cc565540d0eda9fa0e", + "scope": "simultaneous compatibility of equality supports" + }, + "upstream_checkpoint": { + "canonical_main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "checked_at_utc": "2026-11-03T10:05:00Z", + "priority_revision": 8, + "selected_pr": 6030 + }, + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19371205", + "coverage": { + "open_prs": 522, + "discussion_records": 6536, + "local_notes": 8917, + "complete_pagination": true + }, + "limits": "Main and merged object/general-form searches plus live handoffs and reservations were checked. Arbitrary historical diffs and unpublished work are outside coverage." + }, + "claim_type": "scoped written proof with exact finite certificate" +} diff --git a/research/e8-a2-shared-equality/VERIFY.json b/research/e8-a2-shared-equality/VERIFY.json new file mode 100644 index 0000000000..f07ef0fe2e --- /dev/null +++ b/research/e8-a2-shared-equality/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/e8-a2-analytic-rank6/PROOF.md", + "research/p112-root-simplex-exclusion/geometry.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Complete primal/dual equality incidence, source transport, literal attainer and hypothesis/domain controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "The same complete certificate and rejection controls with assertions disabled." + } + ] +} diff --git a/research/e8-a2-shared-equality/independent.py b/research/e8-a2-shared-equality/independent.py new file mode 100644 index 0000000000..e704ee6eda --- /dev/null +++ b/research/e8-a2-shared-equality/independent.py @@ -0,0 +1,105 @@ +"""Dual three-space enumeration; no imports from the primal enumerator. + +Produced by Nick Petalas. Apache-2.0. +""" + +from itertools import combinations +import json + + +def check(condition, message): + if not condition: + raise ValueError(message) + + +def qform(x): + return sum((x >> (2 * i) & 1) * (x >> (2 * i + 1) & 1) + for i in range(4)) % 2 + + +def pairing(x, y): + return sum(((x >> (2 * i) & 1) * (y >> (2 * i + 1) & 1) + + (y >> (2 * i) & 1) * (x >> (2 * i + 1) & 1)) + for i in range(4)) % 2 + + +def dual_spaces(): + """U=N+, with r nonzero singular, N an anisotropic plane in r-perp.""" + roots = tuple(x for x in range(256) if qform(x)) + planes = {tuple(sorted((x, y, x ^ y))) + for x, y in combinations(roots, 2) if pairing(x, y)} + spaces = {} + for radical in range(1, 256): + if qform(radical): + continue + for plane in planes: + if all(not pairing(radical, x) for x in plane): + vectors = tuple(sorted((0, radical, *plane, + *(x ^ radical for x in plane)))) + spaces[vectors] = radical + check(len(spaces) == 7560, "complete dual three-space inventory") + return spaces + + +def complement_planes(vectors, radical): + candidates = set() + for x, y in combinations(vectors[1:], 2): + if pairing(x, y): + plane = tuple(sorted((x, y, x ^ y))) + check(radical not in plane and all(qform(z) for z in plane), + "four anisotropic complements") + candidates.add(plane) + check(len(candidates) == 4, "complement plane count") + return tuple(sorted(candidates)) + + +def affine_cosets(vectors, radical): + # Canonical cosets use syndrome values against every member of U. + cosets = {} + for x in range(256): + syndrome = tuple(pairing(x, y) for y in vectors[1:]) + cosets.setdefault(syndrome, []).append(x) + check(len(cosets) == 8 and all(len(c) == 32 for c in cosets.values()), + "complete affine five-space cosets") + selected = tuple(tuple(c) for c in cosets.values() if pairing(c[0], radical)) + check(len(selected) == 4, "nonzero radical character") + return selected + + +def incident_fibers(coset, planes): + a = coset[0] + entries, zero_points = [], 0 + for plane in planes: + projection = tuple(p for p in (0, *plane) + if all(pairing(a ^ p, x) == 0 for x in plane)) + check(len(projection) == 1, "unique orthogonal projection") + point = projection[0] + if point: + check(point not in coset, "singleton excluded from the equality support") + entries.append((plane, point)) + else: + zero_points += 1 + check(len(entries) == 3 and zero_points == 1, "three valid and one zero projection") + return tuple(sorted(entries)) + + +def independent_incidence(): + incidence = {} + coset_count = 0 + for vectors, radical in dual_spaces().items(): + planes = complement_planes(vectors, radical) + for coset in affine_cosets(vectors, radical): + support = tuple(x for x in coset if qform(x)) + check(len(support) == 16, "balanced sixteen-root support") + mask = sum(1 << x for x in support) + check(mask not in incidence, "distinct affine supports") + incidence[mask] = incident_fibers(coset, planes) + coset_count += 1 + check(coset_count == 30240, "complete dual support inventory") + return incidence, {"dual_three_spaces": 7560, "affine_cosets": coset_count, + "zero_projection_exclusions": coset_count} + + +if __name__ == "__main__": + incidence, counts = independent_incidence() + print(json.dumps({"supports": len(incidence), "dual_checks": counts}, sort_keys=True)) diff --git a/research/e8-a2-shared-equality/verify.py b/research/e8-a2-shared-equality/verify.py new file mode 100644 index 0000000000..52a0fc54e4 --- /dev/null +++ b/research/e8-a2-shared-equality/verify.py @@ -0,0 +1,214 @@ +"""Exact cross-fiber A2 equality incidence. Produced by Nick Petalas. + +Apache-2.0. Individual-fiber results are premises from PR3288. +""" + +import argparse +from collections import Counter +from hashlib import sha256 +from itertools import combinations +import json +from pathlib import Path + +from independent import independent_incidence + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +HYPERBOLIC_COLUMNS = (3, 6, 18, 34, 76, 78, 130, 208) +SIMPLE_EDGES = ((0, 2), (1, 3), (2, 3), (3, 4), (4, 5), (5, 6), (6, 7)) +SIMPLE_WITNESS = (3, 11, 27, 31, 39, 47, 59, 63, 71, 79, 83, 87, 103, 111, 123, 127) +SOURCE_MANIFEST_SHA256 = "cbd2e3530c026ff5f5e5303f1f705e70c47d5b2175e76d0f2ffc5cb5d7dfeb08" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def quadratic(x): + return ((x & (x >> 1) & 0x55).bit_count()) % 2 + + +def source_quadratic(x): + return (x.bit_count() + sum((x >> i & 1) * (x >> j & 1) + for i, j in SIMPLE_EDGES)) % 2 + + +def transform(x): + result = 0 + for i, column in enumerate(HYPERBOLIC_COLUMNS): + if x >> i & 1: + result ^= column + return result + + +def basis(values): + require(len(values) <= 512, "binary inventory bound") + rows = [] + for value in values: + require(type(value) is int and 0 <= value < 512, "binary vector domain") + for row in rows: + value = min(value, value ^ row) + if value: + rows = sorted([min(row, row ^ value) for row in rows] + [value], + reverse=True) + return tuple(rows) + + +def authenticate(): + raw_sources = (PACKAGE / "SOURCES.json").read_bytes() + require(sha256(raw_sources).hexdigest() == SOURCE_MANIFEST_SHA256, + "exact source manifest") + sources = json.loads(raw_sources) + require(len(sources["files"]) == 4, "source inventory") + paths = [] + for row in sources["files"]: + if row["usage"] == "input": + path = ROOT / row["path"] + require(path.is_file() and not path.is_symlink(), "regular source") + raw = path.read_bytes() + require(len(raw) <= 100_000, "source byte bound") + require(sha256(raw).hexdigest() == row["sha256"], "source hash") + paths.append(row["path"]) + require(sorted(paths) == ["research/e8-a2-analytic-rank6/PROOF.md", + "research/p112-root-simplex-exclusion/geometry.py"], + "exact live inputs") + require(len({transform(x) for x in range(256)}) == 256, "invertible transport") + require(all(source_quadratic(transform(x)) == quadratic(x) for x in range(256)), + "transport to the pinned simple-root polynomial") + + +def fiber_inventory(q, polar): + roots = tuple(x for x in range(256) if q[x]) + planes = sorted({tuple(sorted((a, b, a ^ b))) + for a, b in combinations(roots, 2) if polar[a][b]}) + fibers = [] + for plane in planes: + a, b = plane[:2] + for point in plane: + roots_in_section = tuple(x for x in roots + if polar[x][a] == polar[point][a] + and polar[x][b] == polar[point][b]) + fiber = tuple(x for x in roots_in_section if x != point) + fibers.append((plane, point, roots_in_section, fiber)) + require(len(fibers) == 3360, "complete normal-plane inventory") + return fibers + + +def primal_incidence(fibers): + incidence = {} + for plane, point, section, fiber in fibers: + rows = basis(tuple(1 | (x << 1) for x in fiber)) + require(len(rows) == 7, "inherited fiber-span contract") + coordinates = {0: 0} + for i, row in enumerate(rows): + coordinates.update({x ^ row: c | (1 << i) + for x, c in tuple(coordinates.items())}) + for normal in range(1, 128): + support = tuple(x for x in section + if not (coordinates[1 | (x << 1)] & normal).bit_count() % 2) + if len(support) == 16 and point not in support: + mask = sum(1 << x for x in support) + if mask not in incidence: + require(len(basis(tuple(1 | (x << 1) for x in support))) == 6, + "root support determines its six-space") + incidence[mask] = [] + incidence[mask].append((plane, point)) + return {mask: tuple(sorted(entries)) for mask, entries in incidence.items()} + + +def missing_point_control(fiber_record): + _, point, section, fiber = fiber_record + rows = basis(tuple(1 | (x << 1) for x in fiber)) + coordinates = {0: 0} + for i, row in enumerate(rows): + coordinates.update({x ^ row: c | (1 << i) + for x, c in tuple(coordinates.items())}) + found = False + for normal in range(1, 128): + support = {x for x in section + if not (coordinates[1 | (x << 1)] & normal).bit_count() % 2} + if len(support) == 16 and point in support: + require(len(support) + len(support.intersection(fiber)) == 31, + "balanced section containing the singleton has score 31") + found = True + break + require(found, "genuine missing-point countercontrol") + + +def summarize(incidence): + require(Counter(map(len, incidence.values())) == {3: 30240}, "sharp multiplicity") + degrees, pairs = Counter(), set() + digest = sha256() + for mask, entries in sorted(incidence.items()): + require(len(set(entries)) == 3, "three distinct fibers") + digest.update((json.dumps([hex(mask), entries], separators=(",", ":")) + + "\n").encode()) + for pair in combinations(entries, 2): + require(pair not in pairs, "two fibers share at most one equality space") + pairs.add(pair) + degrees.update(pair) + require(len(pairs) == 90720 and Counter(degrees.values()) == {54: 3360}, + "complete compatibility graph") + witness = min(tuple(x for x in range(256) if mask >> x & 1) for mask in incidence) + mask = sum(1 << x for x in witness) + source_labels = sorted(1 | (transform(x) << 1) for x in witness) + require(tuple(source_labels) == SIMPLE_WITNESS, "literal simple-root witness") + return {"supports": len(incidence), "incidences": 3 * len(incidence), + "fibers_per_support": 3, "neighbors_per_fiber": 54, + "compatible_unordered_fiber_pairs": len(pairs), + "incidence_sha256": digest.hexdigest(), + "simple_root_witness": source_labels, + "canonical_witness_fibers": incidence[mask]} + + +def controls(incidence, q, polar): + mask = next(iter(incidence)) + plane, point = incidence[mask][0] + support = tuple(x for x in range(256) if mask >> x & 1) + require(point not in support and all(q[x] for x in support), "valid witness") + require(all(q[x] and q[y] and q[x ^ y] and polar[x][y] + for x, y in combinations(plane, 2)), "anisotropic normal plane") + for invalid in ((True,), (-1,), (512,), tuple(range(513))): + rejected = False + try: + basis(invalid) + except ValueError: + rejected = True + require(rejected, "invalid binary input rejected") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path) + args = parser.parse_args() + authenticate() + q = tuple(quadratic(x) for x in range(256)) + polar = tuple(tuple(q[x ^ y] ^ q[x] ^ q[y] for y in range(256)) + for x in range(256)) + fibers = fiber_inventory(q, polar) + incidence = primal_incidence(fibers) + independent, dual_checks = independent_incidence() + require(incidence == independent, "complete primal/dual incidence agreement") + controls(incidence, q, polar) + missing_point_control(fibers[0]) + result = summarize(incidence) + result["dual_checks"] = dual_checks + result["status"] = "PASS_A2_SHARED_EQUALITY" + if args.receipt is not None: + require(not args.receipt.resolve().is_relative_to(ROOT.resolve()), + "receipt destination must be outside the checkout") + files = sorted(p for p in PACKAGE.iterdir() if p.is_file()) + require(len(files) <= 12, "package receipt inventory bound") + hashes = {p.name: sha256(p.read_bytes()).hexdigest() for p in files} + receipt = {"result": result, "package_sha256": hashes, + "input_sha256": {r["path"]: r["sha256"] for r in + json.loads((PACKAGE / "SOURCES.json").read_text())["files"] + if r["usage"] == "input"}} + args.receipt.write_text(json.dumps(receipt, sort_keys=True, indent=2) + "\n") + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()