From c5d95a3544dafbb31f2163cce7aa352dab428a57 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Mon, 26 Oct 2026 01:19:06 -0500 Subject: [PATCH 1/4] Prove quadratic extension and sharp all-pivot incidence through seven deletions --- .../PROOF.md | 199 +++++++++++++ .../README.md | 29 ++ .../RESULT.json | 104 +++++++ .../SMALL.json | 154 ++++++++++ .../SOURCES.json | 72 +++++ .../TASK.json | 72 +++++ .../VERIFY.json | 65 ++++ .../verify.py | 280 ++++++++++++++++++ 8 files changed, 975 insertions(+) create mode 100644 research/seven-deletion-quadratic-extension/PROOF.md create mode 100644 research/seven-deletion-quadratic-extension/README.md create mode 100644 research/seven-deletion-quadratic-extension/RESULT.json create mode 100644 research/seven-deletion-quadratic-extension/SMALL.json create mode 100644 research/seven-deletion-quadratic-extension/SOURCES.json create mode 100644 research/seven-deletion-quadratic-extension/TASK.json create mode 100644 research/seven-deletion-quadratic-extension/VERIFY.json create mode 100644 research/seven-deletion-quadratic-extension/verify.py diff --git a/research/seven-deletion-quadratic-extension/PROOF.md b/research/seven-deletion-quadratic-extension/PROOF.md new file mode 100644 index 0000000000..8620d11ca2 --- /dev/null +++ b/research/seven-deletion-quadratic-extension/PROOF.md @@ -0,0 +1,199 @@ +# Quadratic extension and the sharp seven-deletion boundary + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. + +## Theorem and scope + +Use the doubled E8 root lines and FRAME0 ordering from Josie Elliston's +PR1650. Let P112 be the complement of FRAME0. For every X subset of P112 with +|X|<=7, set L=P112 minus X and let M_L be the incidence matrix of **all** +orthogonal eight-line frames contained in L, with columns L. + +1. The kernel of M_L over every characteristic-zero field is exactly the + 35-dimensional space of restrictions of ambient trace-zero quadratics. + Each such extension is unique. +2. For every live pivot frame F in L and each pivot coordinate k, condition + D of Andrey Mas's PR1560 holds: the frame incidence on I_k has rank + |I_k|-7 and its kernel is the span of the seven canonical h_kl vectors. + No W, G or nonempty-block premise is needed for this conclusion. +3. Seven is sharp for the all-pivot conclusion. Josie Elliston's PR1668 + supplies eight-deletion examples with W, G and nonempty blocks but not D. + Those examples and their discovery remain predecessor work. + +This is a finite, complete computational proof plus uniform linear algebra. +The orbit cover, root geometry and E7 support theorem are credited inputs. +The new certificate checks the global incidence rank on every deletion class; +it does not repeat the earlier search for one passing pivot per class. + +No new rigidity floor, physical supplier or kappa follows. PR1650 already +supplied rigidity at P105 through a suitable pivot. This result removes the +choice of pivot from the D obligation and completes the precise extension +handoff. It does not prove G or W for every pivot. It does not address nine +or more costly terms, native realization, routing, ownership, restoration, +precision, preparation or the full recursive bill. The selected .00310045 +frontier and its main-transform bottleneck are unchanged. + +## 1. Uniform injectivity of quadratic evaluations + +The roots have norm squared eight. On the real vector space of symmetric +trace-zero 8 by 8 matrices with the Frobenius inner product, put +R_v=vv^T-I. Then + +```text + = 56, +|| = 8 for distinct root lines, +sum_v R_v = 192 H. +``` + +The verifier checks the last identity on a full rational basis of 35 forms, +the first two identities on the complete root set, and zero sums on all +2025 frames. Thus the full evaluation operator has squared norm identity +192 I. For any t deleted root lines, the Gram matrix of their R_v has +operator norm at most 56+8(t-1), by the absolute row-sum bound. For t<=17 +this is at most184<192. The remaining evaluations are therefore injective. +This argument proves a bound for every deletion set; it is not a sample. + +In our theorem t=8+|X|<=15. Thus the restrictions of trace-zero quadratics +have dimension35 on L. They lie in ker(M_L), since the eight equal-length +orthogonal roots of a frame have sum of outer products 8I. It remains to +prove rank(M_L)>=|L|-35. The next section supplies this lower bound for +every X. Together the bounds give equality and the extension assertion. + +The real positivity argument produces a rational matrix rank statement. +Every such nonzero rational minor stays nonzero in every characteristic-zero +field. Both the injectivity and the extension conclusion therefore hold over +all those fields, without an order or positivity assumption on the field. + +## 2. Complete deletion cover and new rank certificate + +The retained PR1650 source constructs the 120 lines and all 2025 frames. +Its eight FRAME0-stabilizer generators generate a group H of order172032. +The verifier rebuilds H, checks that each generator is a permutation fixing +FRAME0 and preserving every frame, and checks the full orbit-cover chain. +These maps come from orthogonal root reflections and preserve quadratic +restrictions and the incidence problem. + +For deletion sizes zero through three, the package regenerates the complete +orbits directly. They have 1,1,5,24 representatives. For sizes four through +seven it uses the retained PR1650 data, and checks every candidate transporter: + +| Deleted lines | Candidates checked | Representatives | +|---|---:|---:| +| 4 | 2517 | 180 | +| 5 | 18782 | 1614 | +| 6 | 156627 | 19295 | +| 7 | 1651528 | 242802 | + +The triple orbits cover all227920 triples. Every k-subset has a (k-1)-subset; +move that subset to a retained representative and add its remaining point. +Each resulting candidate is checked to be an actual H-image of its listed +k-unit. This induction proves coverage of all subsets, without trusting a +claimed count of distinct orbits or the original grouping algorithm. +The new package checks source hashes, all indices and lengths, all unit +memberships, every transporter and the absence of trailing cover data. +The data and this induction are Josie Elliston's predecessor contribution. + +For all263922 retained units of sizes0 through7, the new verifier enumerates +all frames disjoint from FRAME0 and X and row-reduces their incidence modulo3. +It obtains rank112-|X|-35 in every case. A nonzero minor modulo3 is a +nonzero integer minor, so this is a lower bound over Q. Section1 supplies +the matching upper bound. Transport through H gives the rank for every X. + +For speed, a ternary row has two disjoint bit planes, for coefficients1 and2. +The code implements the nine field additions by Boolean operations; its +row reduction uses only nonzero pivot scaling and row additions. A retained +PR1650 routine orders the rows by new columns before elimination. It changes +only row order. The new packed elimination is checked against separate dense +modulo3 elimination on512 matrices, all nine scalar additions and deficient +frame-family controls. It stops once the required lower bound is reached; +the matching upper bound is the written geometric proof, not that stop rule. +The registered parts partition the complete unit list with disjoint strides. +No pivot from the retained unit records is used by this rank calculation. + +## 3. Seven canonical directions remain independent + +Fix a root a in P112. Among the other root lines,56 are nonorthogonal to a. +For each such doubled root b, put u_b=2b-(a dot b)/4 a. These vectors lie in +a-perp. Exact full-geometry checks give + +```text +||u_b||^2 = 24, +sum_b u_b u_b^T = 192 I - 24 a a^T, +``` + +and each u_b has exactly one distinct twin with absolute inner product24. +Its inner product with every other distinct vector has absolute value8. +On a-perp the sum is192 I. Four of the56 lines belong to FRAME0. At most +seven more are in X. For any removed set of at most11 projected vectors, +its Gram operator norm is at most24+24+9*8=120<192. Therefore the surviving +projected vectors span all seven dimensions of a-perp. + +At a live pivot F, put a=F[k]. The other seven pivot roots are a basis of +a-perp. The functions h_kl(i)=G_ik G_il on I_k are the corresponding cross +terms. Since G_ik is nonzero on I_k and the projected vectors there span +a-perp, these seven functions are independent. Other pivot roots are +orthogonal to a and hence do not remove any of the56 vectors. This proves +independence for every deletion set in scope and every live pivot, with no +W, G or block-completeness hypothesis. + +## 4. Every local kernel vector is canonical + +Take z in the kernel of the live-frame incidence on I_k. Extend z by zero to +all other live lines, including the whole pivot. This new function has sum +zero on every live frame, so Sections1 and2 give a unique trace-zero ambient +quadratic q extending it. In particular q(a)=0. Its restriction to a-perp +therefore has trace zero. + +The full E7 slice orthogonal to a has63 root lines. Exactly four belong to +FRAME0 and at most seven more to X. On all the other orthogonal lines q is +zero. If the restriction were nonzero, it would have support at most11. +Nick Petalas's PR5238 theorem gives minimum support12 for a nonzero rational +trace-zero restricted quadratic. The package replays its complete +134217727-word binary certificate and root-transitivity check. The same +bound holds over every characteristic-zero field: a nontrivial solution of +the rational linear equations imposing trace zero and the stated zeros +would also give a nontrivial rational solution, since ranks do not change. +Thus the restricted quadratic is zero. + +A symmetric quadratic whose restriction to a-perp is zero and whose value +at a is zero consists only of cross terms between a and a-perp. Its values +on I_k are in the span of the seven h_kl. Conversely those seven vectors +have zero sums on every full frame, because the pivot roots are orthogonal. +Section3 proves their independence. Hence the local kernel has dimension7 +and its rank is |I_k|-7, which is D. This holds for every live pivot at once; +no census of individual pivots is substituted for the argument. + +## 5. Sharpness and acceptance limits + +The two retained PR1668 fixtures have eight deleted lines and all live +frames. The replay checks W, G, nonempty blocks, the exact rational rank +loss, an eighth independent integer kernel vector, and damaged-vector +rejection. Restoring any one deleted line gives128 checked pivot-coordinate +ranks across the two fixtures, consistent with the new theorem. The global +incidence rank is69 on both104-line boundary sets, so quadratic extension +still holds there: sixteen missing roots are within the uniform injectivity +bound. These D failures therefore do not imply extension failure. Their +counterexamples are credited results, not new discoveries. + +The complete finite rank certificate is not a proof-kernel certificate. +The source orbit cover and E7 support code are independently replayed, but +this is not independent human review. The packed-versus-dense comparison is +an algorithmic cross-check, not an exhaustive equivalence proof of arbitrary +program execution. Its nine-case arithmetic proof and ordinary elimination +argument supply that general justification. See RESULT.json and VALIDATION.md +for the executed commands, full coverage and portability checks. + +## Credit and sources + +- [Josie Elliston PR1650](https://github.com/CrocSwap/integer-mult-bounds/pull/1650): complete deletion orbit cover, data, geometry and row-ordering method. +- [Josie Elliston PR1668](https://github.com/CrocSwap/integer-mult-bounds/pull/1668): sharp eight-deletion boundary, D4 explanation and exact witnesses. +- [Andrey Mas PR1560](https://github.com/CrocSwap/integer-mult-bounds/pull/1560): the D/G/W structural criterion and projector proof. +- [Nick Petalas PR5238](https://github.com/CrocSwap/integer-mult-bounds/pull/5238): sharp trace-zero E7 support twelve and its complete binary certificate. +- [JoyboyBrian's handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1502#discussioncomment-19145642): the extension/support reduction and its precise open quantifiers. + +PR1616, Aaron Wang PR1649 and the retained Brett Halligan, themilkman216 and +DreamingOfClouds lineage supply prior E8 geometry and incidence work. All +source files and notices stay byte-exact. SOURCES.json binds their canonical +main objects. The new contribution is the uniform quadratic-injectivity and +cross-term bounds, the complete global rank certificate, and the resulting +all-pivot theorem. No global literature priority is claimed. diff --git a/research/seven-deletion-quadratic-extension/README.md b/research/seven-deletion-quadratic-extension/README.md new file mode 100644 index 0000000000..e43192a13f --- /dev/null +++ b/research/seven-deletion-quadratic-extension/README.md @@ -0,0 +1,29 @@ +# Quadratic extension through seven deletions + +For every X subset of P112 with |X|<=7, the full live-frame incidence kernel +is exactly the restriction of ambient trace-zero E8 quadratics. Consequently, +diagonal incidence D holds at every live pivot, without W/G premises. +The known eight-deletion counterexample makes this boundary sharp. + +[PROOF.md](PROOF.md) gives the uniform argument and exact scope. The complete +finite certificate checks all263922 deletion representatives and the retained +orbit cover. [RESULT.json](RESULT.json) records the evidence. The geometry, +orbit cover, E7 support theorem and eight-deletion witness retain full credit. +This result does not give a new rigidity floor, physical supplier or kappa. + +```sh +python3.12 -B scripts/research_package.py --package research/seven-deletion-quadratic-extension +``` + +Expected: `PASS_SEVEN_DELETION_QUADRATIC_EXTENSION` for each phase and +`PASS_REGISTERED_RESEARCH_PACKAGE`. Python3.12 and the standard library +suffice. Four worker processes check the independent deletion classes; no +subagents are used. Ali Romman with substantial OpenAI Codex assistance. +Apache-2.0. The selected frontier is unchanged. + +## Open next questions + +Determine the maximum deletion threshold for the global quadratic-extension +property itself. The all-pivot D threshold is already sharp at seven, so a +larger extension threshold alone cannot raise it. A decoder application must +still price a changed physical construction and every recursive obligation. diff --git a/research/seven-deletion-quadratic-extension/RESULT.json b/research/seven-deletion-quadratic-extension/RESULT.json new file mode 100644 index 0000000000..948628b190 --- /dev/null +++ b/research/seven-deletion-quadratic-extension/RESULT.json @@ -0,0 +1,104 @@ +{ + "deletion_subsets_covered": 38760897157, + "phases": { + "cover": { + "controls": { + "boundary_extension_ranks": [ + 69, + 69 + ], + "damaged_certificate_controls": 2, + "deficient_family_controls": 1, + "dense_F3_comparisons": 512, + "restored_coordinate_checks": 128, + "scalar_additions": 9, + "sharp_boundary_fixtures": 2 + }, + "coverage": { + "group": 172032, + "levels": { + "4": { + "candidates": 2517, + "units": 180 + }, + "5": { + "candidates": 18782, + "units": 1614 + }, + "6": { + "candidates": 156627, + "units": 19295 + }, + "7": { + "candidates": 1651528, + "units": 242802 + } + }, + "small_units": { + "0": 1, + "1": 1, + "2": 5, + "3": 24 + } + }, + "geometry": { + "missing_projection_bound": 120, + "pivot_roots": 112, + "projected_frame_constant": 192, + "quadratic_basis": 35, + "quadratic_frame_constant": 192, + "quadratic_injectivity_missing_limit": 17 + } + }, + "e7": { + "e7": { + "controls": 92, + "frames": 135, + "minimum": 12, + "visited": 134217727 + } + }, + "part1/2": { + "census": { + "certificate_sha256": "ee9447aab14901cde826d55a681356f0c9591ef3abed69a0cd6732c4b2532f8a", + "levels": { + "0": 1, + "2": 3, + "3": 12, + "4": 90, + "5": 807, + "6": 9647, + "7": 121401 + }, + "live_frame_range": [ + 630, + 1260 + ], + "part": "1/2", + "units": 131961 + } + }, + "part2/2": { + "census": { + "certificate_sha256": "5477b9d8c9eabf7dbf814b9d12bc59182b6bbc6f91ceb8d8f2b01cd463833640", + "levels": { + "1": 1, + "2": 2, + "3": 12, + "4": 90, + "5": 807, + "6": 9648, + "7": 121401 + }, + "live_frame_range": [ + 630, + 1170 + ], + "part": "2/2", + "units": 131961 + } + } + }, + "representatives": 263922, + "status": "PASS_SEVEN_DELETION_QUADRATIC_EXTENSION" +} diff --git a/research/seven-deletion-quadratic-extension/SMALL.json b/research/seven-deletion-quadratic-extension/SMALL.json new file mode 100644 index 0000000000..d27cb83647 --- /dev/null +++ b/research/seven-deletion-quadratic-extension/SMALL.json @@ -0,0 +1,154 @@ +{ + "0": [ + [] + ], + "1": [ + [ + 2 + ] + ], + "2": [ + [ + 2, + 3 + ], + [ + 2, + 5 + ], + [ + 2, + 12 + ], + [ + 2, + 13 + ], + [ + 2, + 30 + ] + ], + "3": [ + [ + 2, + 3, + 4 + ], + [ + 2, + 3, + 12 + ], + [ + 2, + 3, + 13 + ], + [ + 2, + 3, + 14 + ], + [ + 2, + 3, + 30 + ], + [ + 2, + 5, + 8 + ], + [ + 2, + 5, + 12 + ], + [ + 2, + 5, + 13 + ], + [ + 2, + 5, + 30 + ], + [ + 2, + 5, + 42 + ], + [ + 2, + 12, + 14 + ], + [ + 2, + 12, + 15 + ], + [ + 2, + 12, + 24 + ], + [ + 2, + 12, + 30 + ], + [ + 2, + 12, + 31 + ], + [ + 2, + 12, + 32 + ], + [ + 2, + 12, + 42 + ], + [ + 2, + 12, + 43 + ], + [ + 2, + 12, + 47 + ], + [ + 2, + 13, + 14 + ], + [ + 2, + 13, + 17 + ], + [ + 2, + 13, + 31 + ], + [ + 2, + 13, + 33 + ], + [ + 2, + 13, + 44 + ] + ] +} diff --git a/research/seven-deletion-quadratic-extension/SOURCES.json b/research/seven-deletion-quadratic-extension/SOURCES.json new file mode 100644 index 0000000000..5ebabd5262 --- /dev/null +++ b/research/seven-deletion-quadratic-extension/SOURCES.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/complex-rank8-rigidity-p105/verify.py", + "usage": "input", + "git_blob": "d60ada8e40a03efb4506c1cfadd589d16df0a281", + "sha256": "8bab6588f19f0280a98dfce90835746387ef9845cdfb5768f84ac75247af7b01" + }, + { + "path": "research/complex-rank8-rigidity-p105/UNITS.json.gz", + "usage": "input", + "git_blob": "15d42a2e1f2a74320a7436bc2b20e36e9bdc947c", + "sha256": "5eb77d66081f0cc8d11177867ce7bfb5d6690e93cbc4a330e966415e994b548e" + }, + { + "path": "research/complex-rank8-rigidity-p105/COVER.bin.gz", + "usage": "input", + "git_blob": "48bd58b3ef008034436d85e51e552aa011518c4f", + "sha256": "041992994a8fed9b68258779f2b648d4ece928eb691d142adaf7449f73409449" + }, + { + "path": "research/complex-rank8-rigidity-p105/README.md", + "usage": "input", + "git_blob": "e841127c54ad100457cc9044f6ef6269bd545afd", + "sha256": "73328080583e191540cbca656c1b435d2c5523d340212761b59822b9a12e10aa" + }, + { + "path": "research/e7-quadratic-support/verify.py", + "usage": "input", + "git_blob": "781a074d45126b1a84b92ee2393dc95790c0cb1b", + "sha256": "95502bb9e551302cbb0483097250441e96e5f858a5624745678875e3cedba9d2" + }, + { + "path": "research/e7-quadratic-support/README.md", + "usage": "input", + "git_blob": "5dc802961147c41af039e899d8baa3c8bb9e3909", + "sha256": "36e2263d28280043d6861caa4c81270be4800246e17647ec09da7cb4c2826085" + }, + { + "path": "research/full-family-g-without-d/verify.py", + "usage": "input", + "git_blob": "15f65fa7ddf02f5907f00aa83f2bd52fbe0a8583", + "sha256": "2e45790da2cc2b2eea2e47900a94cadf7aa4a7d42a3d38390729cd9b409d73fb" + }, + { + "path": "research/full-family-g-without-d/README.md", + "usage": "input", + "git_blob": "50cb846dc47e238a3f751966555e52aae887f702", + "sha256": "4ebf92cebdf400ccd63a89d09376378be86bbe6fdb9f1565b39ddd234958d96c" + }, + { + "path": "research/frame-incidence-zero-exclusion/proof.md", + "usage": "input", + "git_blob": "bfea905d386ce28d13d10682cb45da2050493ced", + "sha256": "3b9d25559ef38c6fbcfcd70dcd100ab09db7f36a33e827aba48b7f8d81c0befe" + } + ] +} diff --git a/research/seven-deletion-quadratic-extension/TASK.json b/research/seven-deletion-quadratic-extension/TASK.json new file mode 100644 index 0000000000..c7b6372bef --- /dev/null +++ b/research/seven-deletion-quadratic-extension/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "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": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Uniform trace-zero quadratic extension for every P112 deletion set of size at most seven, and sharp all-pivot diagonal incidence.", + "scope_change_reason": "Follow the explicit released extension handoff for the decoder-incidence criterion; no masked decoder construction is claimed.", + "bottleneck_link": "Remove the repeated pivot-specific D obligation from E8 decoder screens. Physical cost and a complete kappa improvement remain open.", + "budget_minutes": 120, + "stop_rule": "Finish the complete deletion cover and rank proof, or publish an exact counterexample.", + "outcome": "completed", + "evidence": "PROOF.md; RESULT.json; complete registered rank and source replay.", + "author": "Ali Romman with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance; no subagents; four ordinary verifier worker processes.", + "open_questions": [ + { + "question": "What is the global quadratic-extension threshold beyond seven deletions?", + "why_it_matters": "It distinguishes extension failure from the already sharp E7 support obstruction.", + "first_step": "Identify a changed application that needs the larger extension range before a larger census.", + "blocked_by": "No such physical caller is supplied." + } + ] +} diff --git a/research/seven-deletion-quadratic-extension/VERIFY.json b/research/seven-deletion-quadratic-extension/VERIFY.json new file mode 100644 index 0000000000..23660a20e0 --- /dev/null +++ b/research/seven-deletion-quadratic-extension/VERIFY.json @@ -0,0 +1,65 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/complex-rank8-rigidity-p105/verify.py", + "research/complex-rank8-rigidity-p105/UNITS.json.gz", + "research/complex-rank8-rigidity-p105/COVER.bin.gz", + "research/complex-rank8-rigidity-p105/README.md", + "research/e7-quadratic-support/verify.py", + "research/e7-quadratic-support/README.md", + "research/full-family-g-without-d/verify.py", + "research/full-family-g-without-d/README.md", + "research/frame-incidence-zero-exclusion/proof.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--cover" + ], + "timeout_seconds": 120, + "checks": "Complete source orbit cover, uniform geometry, separate dense rank controls and exact eight-deletion boundary." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--part", + "1/2", + "--jobs", + "4" + ], + "timeout_seconds": 450, + "checks": "Every global incidence rank in exhaustive deletion-unit part 1/2." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--part", + "2/2", + "--jobs", + "4" + ], + "timeout_seconds": 450, + "checks": "Every global incidence rank in exhaustive deletion-unit part 2/2." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--e7" + ], + "timeout_seconds": 180, + "checks": "Complete retained E7 binary support census and all92 controls." + } + ] +} diff --git a/research/seven-deletion-quadratic-extension/verify.py b/research/seven-deletion-quadratic-extension/verify.py new file mode 100644 index 0000000000..9c5db8d6b0 --- /dev/null +++ b/research/seven-deletion-quadratic-extension/verify.py @@ -0,0 +1,280 @@ +#!/usr/bin/env python3 +"""Check every deletion class and the uniform all-pivot proof premises. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +import array +from concurrent.futures import ProcessPoolExecutor +from collections import Counter +import gzip +import hashlib +import importlib.util +import itertools +import json +from pathlib import Path +import random +import sys + +ROOT = Path(__file__).resolve().parent +REPO = ROOT.parents[1] +MASK = (1 << 120)-1 + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def authenticate(): + rows = json.loads((ROOT/'SOURCES.json').read_text())['files'] + inputs = [r for r in rows if r['usage'] == 'input'] + for r in inputs: + need(hashlib.sha256((REPO/r['path']).read_bytes()).hexdigest() == r['sha256'], 'source hash: '+r['path']) + return len(inputs) + + +def load(name, path): + spec = importlib.util.spec_from_file_location(name, REPO/path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +s = load('p105_source', 'research/complex-rank8-rigidity-p105/verify.py') + + +def add3(a, b, c, d): + z1, z2 = MASK ^ (a | b), MASK ^ (c | d) + return (z1 & c) | (a & z2) | (b & d), (z1 & d) | (b & z2) | (a & c) + + +def rank3(pairs, target=121): + basis = {} + for a, b in pairs: + while a | b: + pivot = (a | b).bit_length()-1 + if pivot not in basis: + basis[pivot] = (b, a) if (b >> pivot) & 1 else (a, b) + if len(basis) == target: + return target + break + c, d = basis[pivot] + if (a >> pivot) & 1: + c, d = d, c + a, b = add3(a, b, c, d) + return len(basis) + + +def dense_rank(rows, prime=3): + basis = {} + for row in rows: + v = [x % prime for x in row] + for j in sorted(basis): + c = v[j] + if c: + v = [(x-c*y) % prime for x, y in zip(v,basis[j])] + j = next((j for j,x in enumerate(v) if x), None) + if j is not None: + inv = pow(v[j],-1,prime) + basis[j] = [x*inv % prime for x in v] + return len(basis) + + +def encode(row): + return sum(1< Date: Mon, 26 Oct 2026 01:20:02 -0500 Subject: [PATCH 2/4] Compare serialized phase keys and enforce the registered partition --- research/seven-deletion-quadratic-extension/verify.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/research/seven-deletion-quadratic-extension/verify.py b/research/seven-deletion-quadratic-extension/verify.py index 9c5db8d6b0..818087c448 100644 --- a/research/seven-deletion-quadratic-extension/verify.py +++ b/research/seven-deletion-quadratic-extension/verify.py @@ -157,7 +157,7 @@ def check_unit(item): def census(part, jobs): i,n=map(int,part.split('/')) - need(1<=i<=n<=32 and 1<=jobs<=16,'part and worker bounds') + need(n==2 and i in (1,2) and 1<=jobs<=16,'registered part and worker bounds') levels=unit_levels() all_units=[(k,tuple(X)) for k in range(8) for X in levels[k]] chosen=all_units[i-1::n] @@ -273,6 +273,7 @@ def main(): else: result={'census':census(args.part,args.jobs)} key='cover' if args.cover else 'e7' if args.e7 else 'part'+args.part expected=json.loads((ROOT/'RESULT.json').read_text())['phases'] + result=json.loads(json.dumps(result)) need(key in expected and result==expected[key],'committed phase result differs') print(json.dumps({'status':'PASS_SEVEN_DELETION_QUADRATIC_EXTENSION',**result},sort_keys=True),flush=True) From 8fd0a5ace34b7accd39bcce871a1b3b339b80074 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Mon, 26 Oct 2026 01:25:48 -0500 Subject: [PATCH 3/4] Clarify the uniform incidence proof and boundary scope --- .../PROOF.md | 38 +++++++++---------- .../README.md | 4 +- 2 files changed, 21 insertions(+), 21 deletions(-) diff --git a/research/seven-deletion-quadratic-extension/PROOF.md b/research/seven-deletion-quadratic-extension/PROOF.md index 8620d11ca2..2b64a548aa 100644 --- a/research/seven-deletion-quadratic-extension/PROOF.md +++ b/research/seven-deletion-quadratic-extension/PROOF.md @@ -50,11 +50,11 @@ the first two identities on the complete root set, and zero sums on all 2025 frames. Thus the full evaluation operator has squared norm identity 192 I. For any t deleted root lines, the Gram matrix of their R_v has operator norm at most 56+8(t-1), by the absolute row-sum bound. For t<=17 -this is at most184<192. The remaining evaluations are therefore injective. +this is at most 184<192. The remaining evaluations are therefore injective. This argument proves a bound for every deletion set; it is not a sample. In our theorem t=8+|X|<=15. Thus the restrictions of trace-zero quadratics -have dimension35 on L. They lie in ker(M_L), since the eight equal-length +have dimension 35 on L. They lie in ker(M_L), since the eight equal-length orthogonal roots of a frame have sum of outer products 8I. It remains to prove rank(M_L)>=|L|-35. The next section supplies this lower bound for every X. Together the bounds give equality and the extension assertion. @@ -67,7 +67,7 @@ all those fields, without an order or positivity assumption on the field. ## 2. Complete deletion cover and new rank certificate The retained PR1650 source constructs the 120 lines and all 2025 frames. -Its eight FRAME0-stabilizer generators generate a group H of order172032. +Its eight FRAME0-stabilizer generators generate a group H of order 172032. The verifier rebuilds H, checks that each generator is a permutation fixing FRAME0 and preserving every frame, and checks the full orbit-cover chain. These maps come from orthogonal root reflections and preserve quadratic @@ -84,7 +84,7 @@ seven it uses the retained PR1650 data, and checks every candidate transporter: | 6 | 156627 | 19295 | | 7 | 1651528 | 242802 | -The triple orbits cover all227920 triples. Every k-subset has a (k-1)-subset; +The triple orbits cover all 227920 triples. Every k-subset has a (k-1)-subset; move that subset to a retained representative and add its remaining point. Each resulting candidate is checked to be an actual H-image of its listed k-unit. This induction proves coverage of all subsets, without trusting a @@ -93,18 +93,18 @@ The new package checks source hashes, all indices and lengths, all unit memberships, every transporter and the absence of trailing cover data. The data and this induction are Josie Elliston's predecessor contribution. -For all263922 retained units of sizes0 through7, the new verifier enumerates +For all 263922 retained units of sizes 0 through 7, the new verifier enumerates all frames disjoint from FRAME0 and X and row-reduces their incidence modulo3. It obtains rank112-|X|-35 in every case. A nonzero minor modulo3 is a -nonzero integer minor, so this is a lower bound over Q. Section1 supplies +nonzero integer minor, so this is a lower bound over Q. Section 1 supplies the matching upper bound. Transport through H gives the rank for every X. -For speed, a ternary row has two disjoint bit planes, for coefficients1 and2. +For speed, a ternary row has two disjoint bit planes, for coefficients 1 and 2. The code implements the nine field additions by Boolean operations; its row reduction uses only nonzero pivot scaling and row additions. A retained PR1650 routine orders the rows by new columns before elimination. It changes only row order. The new packed elimination is checked against separate dense -modulo3 elimination on512 matrices, all nine scalar additions and deficient +modulo3 elimination on 512 matrices, all nine scalar additions and deficient frame-family controls. It stops once the required lower bound is reached; the matching upper bound is the written geometric proof, not that stop rule. The registered parts partition the complete unit list with disjoint strides. @@ -112,7 +112,7 @@ No pivot from the retained unit records is used by this rank calculation. ## 3. Seven canonical directions remain independent -Fix a root a in P112. Among the other root lines,56 are nonorthogonal to a. +Fix a root a in P112. Among the other root lines, 56 are nonorthogonal to a. For each such doubled root b, put u_b=2b-(a dot b)/4 a. These vectors lie in a-perp. Exact full-geometry checks give @@ -123,8 +123,8 @@ sum_b u_b u_b^T = 192 I - 24 a a^T, and each u_b has exactly one distinct twin with absolute inner product24. Its inner product with every other distinct vector has absolute value8. -On a-perp the sum is192 I. Four of the56 lines belong to FRAME0. At most -seven more are in X. For any removed set of at most11 projected vectors, +On a-perp the sum is192 I. Four of the 56 lines belong to FRAME0. At most +seven more are in X. For any removed set of at most 11 projected vectors, its Gram operator norm is at most24+24+9*8=120<192. Therefore the surviving projected vectors span all seven dimensions of a-perp. @@ -132,7 +132,7 @@ At a live pivot F, put a=F[k]. The other seven pivot roots are a basis of a-perp. The functions h_kl(i)=G_ik G_il on I_k are the corresponding cross terms. Since G_ik is nonzero on I_k and the projected vectors there span a-perp, these seven functions are independent. Other pivot roots are -orthogonal to a and hence do not remove any of the56 vectors. This proves +orthogonal to a and hence do not remove any of the 56 vectors. This proves independence for every deletion set in scope and every live pivot, with no W, G or block-completeness hypothesis. @@ -140,14 +140,14 @@ W, G or block-completeness hypothesis. Take z in the kernel of the live-frame incidence on I_k. Extend z by zero to all other live lines, including the whole pivot. This new function has sum -zero on every live frame, so Sections1 and2 give a unique trace-zero ambient +zero on every live frame, so Sections 1 and 2 give a unique trace-zero ambient quadratic q extending it. In particular q(a)=0. Its restriction to a-perp therefore has trace zero. -The full E7 slice orthogonal to a has63 root lines. Exactly four belong to +The full E7 slice orthogonal to a has 63 root lines. Exactly four belong to FRAME0 and at most seven more to X. On all the other orthogonal lines q is -zero. If the restriction were nonzero, it would have support at most11. -Nick Petalas's PR5238 theorem gives minimum support12 for a nonzero rational +zero. If the restriction were nonzero, it would have support at most 11. +Nick Petalas's PR5238 theorem gives minimum support 12 for a nonzero rational trace-zero restricted quadratic. The package replays its complete 134217727-word binary certificate and root-transitivity check. The same bound holds over every characteristic-zero field: a nontrivial solution of @@ -159,7 +159,7 @@ A symmetric quadratic whose restriction to a-perp is zero and whose value at a is zero consists only of cross terms between a and a-perp. Its values on I_k are in the span of the seven h_kl. Conversely those seven vectors have zero sums on every full frame, because the pivot roots are orthogonal. -Section3 proves their independence. Hence the local kernel has dimension7 +Section 3 proves their independence. Hence the local kernel has dimension 7 and its rank is |I_k|-7, which is D. This holds for every live pivot at once; no census of individual pivots is substituted for the argument. @@ -168,9 +168,9 @@ no census of individual pivots is substituted for the argument. The two retained PR1668 fixtures have eight deleted lines and all live frames. The replay checks W, G, nonempty blocks, the exact rational rank loss, an eighth independent integer kernel vector, and damaged-vector -rejection. Restoring any one deleted line gives128 checked pivot-coordinate +rejection. Restoring any one deleted line gives 128 checked pivot-coordinate ranks across the two fixtures, consistent with the new theorem. The global -incidence rank is69 on both104-line boundary sets, so quadratic extension +incidence rank is 69 on both 104-line boundary sets, so quadratic extension still holds there: sixteen missing roots are within the uniform injectivity bound. These D failures therefore do not imply extension failure. Their counterexamples are credited results, not new discoveries. diff --git a/research/seven-deletion-quadratic-extension/README.md b/research/seven-deletion-quadratic-extension/README.md index e43192a13f..3e027ca28e 100644 --- a/research/seven-deletion-quadratic-extension/README.md +++ b/research/seven-deletion-quadratic-extension/README.md @@ -6,7 +6,7 @@ diagonal incidence D holds at every live pivot, without W/G premises. The known eight-deletion counterexample makes this boundary sharp. [PROOF.md](PROOF.md) gives the uniform argument and exact scope. The complete -finite certificate checks all263922 deletion representatives and the retained +finite certificate checks all 263922 deletion representatives and the retained orbit cover. [RESULT.json](RESULT.json) records the evidence. The geometry, orbit cover, E7 support theorem and eight-deletion witness retain full credit. This result does not give a new rigidity floor, physical supplier or kappa. @@ -16,7 +16,7 @@ python3.12 -B scripts/research_package.py --package research/seven-deletion-quad ``` Expected: `PASS_SEVEN_DELETION_QUADRATIC_EXTENSION` for each phase and -`PASS_REGISTERED_RESEARCH_PACKAGE`. Python3.12 and the standard library +`PASS_REGISTERED_RESEARCH_PACKAGE`. Python 3.12 and the standard library suffice. Four worker processes check the independent deletion classes; no subagents are used. Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. The selected frontier is unchanged. From a6ae9be34f8db157f285e1bb77e23452f7338c5d Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Mon, 26 Oct 2026 01:32:17 -0500 Subject: [PATCH 4/4] Record full deletion proof replay and sealed portable evidence --- .../VALIDATION.md | 38 +++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 research/seven-deletion-quadratic-extension/VALIDATION.md diff --git a/research/seven-deletion-quadratic-extension/VALIDATION.md b/research/seven-deletion-quadratic-extension/VALIDATION.md new file mode 100644 index 0000000000..a234559da1 --- /dev/null +++ b/research/seven-deletion-quadratic-extension/VALIDATION.md @@ -0,0 +1,38 @@ +# Validation record + +The Python 3.12.14 registered replay passes all four phases: complete source +coverage and uniform geometry, both exhaustive rank parts, and the full E7 +support census. The two parts check 131961 units each with distinct strides, +for all 263922 units. The retained cover reaches every one of the 38760897157 +subsets of P112 of size zero through seven. This is orbit coverage, not a +claim that each subset was separately row-reduced. + +The new modular ranks all equal 112-|X|-35. The proof supplies the matching +upper bound and transport. Independent dense arithmetic agrees on 512 matrix +controls and all nine scalar additions. Both exact eight-deletion witnesses +and all 128 restored-coordinate checks pass. Their global extension ranks +are both 69, which separates extension from the failing D condition. +The E7 replay visits all 134217727 nonzero binary words and rejects all +92 source controls. Its minimum support remains 12. + +An optimized isolated replay of every registered command passes in a sealed, +read-only Git-free export with empty PATH. All eighteen exported files retain +their exact bytes and modes. An actual appended source change is rejected. +The exact committed-byte and official export checks pass. The final export +adds this validation record; all mathematical code and data are the sealed +replay's bytes. Nine consumed source files remain byte-exact. The five linked +proof/source objects were also compared with GitHub's exact main objects. + +The final overlap refresh covers all 7678 local records, 380 open PRs and +5019 Discussion records, with complete remote pagination through +2026-10-26T06:20:45Z. No competing extension claim was found. Canonical main +was fetched again and remains df0137efd35e11b4445734bf612bdd4c7ebc330c. +Unpublished work and every historical diff are outside this check. + +Full-history ancestry preflight is unavailable in the shallow checkout. +Immediate base ancestry and all declared source bytes were checked. The PR +body is rendered and its exact link targets are checked before publication; +the published body and HTML must then match the reviewed draft. Hosted CI, +independent human review and proof-kernel acceptance are separate and are +not inferred from these checks. No selected-frontier edit, merge or closure +of another contributor's work occurs.