diff --git a/research/e6-coordinate-bilinear-form-seed8e9cf2/README.md b/research/e6-coordinate-bilinear-form-seed8e9cf2/README.md new file mode 100644 index 0000000000..9f6f12f394 --- /dev/null +++ b/research/e6-coordinate-bilinear-form-seed8e9cf2/README.md @@ -0,0 +1,84 @@ +# E6 B0 root-coordinate bilinear forms: exact rank-six floor + +**Scoped negative result. No κ or selected-result change.** For one fixed E6 root-line realization and the B0 zero mask, every exact decoder that factors through the six-dimensional root-coordinate map is a scalar multiple of the Gram decoder. Its coordinate form has rational rank six, so this family contains no decoder with four or fewer totals. + +This closes only a narrow algebraic ansatz. It does not rule out arbitrary rational E6 decoders, another admissible pairing, or a better multiplication bound. + +## Exact statement + +Scale E8 roots by two, so every root has squared norm eight. Start from its 120 root lines and retain the lines orthogonal to + +```text +r1 = (2, 2, 0, 0, 0, 0, 0, 0) +r2 = (2, 0, 2, 0, 0, 0, 0, 0) +``` + +These roots have inner product four (one in the unscaled E8 normalization); their common orthogonal root lines form an E6 subsystem with 36 lines. Choose the first six independent normalized lines in lexicographic order as a basis. For each line `t`, let `x_t` be its exact `Q^6` coordinate column in that basis, and let `R` be the 36-by-6 matrix with rows `x_t^T`. + +The fixed B0 mask is one on each **distinct orthogonal pair**. Consider all rational 6-by-6 matrices `L`, including nonsymmetric ones, satisfying + +```text +x_t^T L x_s = 0 for every ordered pair t != s with = 0, +x_t^T L x_t != 0 for all 36 lines. +``` + +Equivalently, the decoded matrix is `M = R L R^T`. Since `rank_Q(L)` is the number of rational rank-one terms needed to factor this coordinate form, `rank_Q(L) <= 4` would give a four-total decoder in this family. + +The verifier constructs all 540 ordered orthogonal-pair equations on the 36 entries of `L` and row-reduces them over `Q`. The constraint matrix has rank 35 and its nullspace is exactly the one-dimensional span of the basis Gram matrix `G`. The matrix `G` has rank six; the scaled decoder diagonal is eight on every root line. Therefore every nonzero exact form in this family is `L = λG`, with `λ != 0`, and has rank six. No such form can use four or fewer totals. + +## Cost screen and scope + +For E6, the per-total floor is `w=5`. A T=4 candidate gets an optimistic floor-only bill of 20 if every term costs exactly five; the open E6 T=4 window thresholds are 23 at h=8, 22 at h=9 and 21 at h=10–11. Copies, frames, source access, restoration, hosting and precision are all granted free in this screen. This shows that the family was not screened out by the most favorable cost model before testing its exactness constraints. + +The exact result removes this one root-coordinate route to those windows. It leaves open factors outside the image of `R`, other admissible pairings, larger total counts, and the full E6 non-star decoder problem. No actual decoder support tariff or supplier admission is claimed because no rank-at-most-four form survives. + +## Evidence and controls + +`RESULT.json` records the exact root, basis, coordinate and constraint hashes, the nullspace generator, its rank, and the diagonal. The positive control `L=G` satisfies every required zero and has diagonal eight. Negative controls confirm that `L=0` fails the nonzero-diagonal condition and that `G+E_00` violates an orthogonal-pair zero (260 ordered violations). + +The root set is generated directly with integer vectors for the E8 D8 and even-half-sign families. The predecessor file `research/root-unit-decoder-lemmas/lib/ade.py` is pinned as provenance and checked for byte drift, but its floating-point root construction is not used by the proof calculation. All coordinates, constraints, ranks and controls in `verify.py` use `fractions.Fraction`. + +## Reproduce + +```sh +python3 -I -O -B research/e6-coordinate-bilinear-form-seed8e9cf2/verify.py +python3 -I -O -B research/e6-coordinate-bilinear-form-seed8e9cf2/test_verify.py +python3 scripts/research_package.py --package research/e6-coordinate-bilinear-form-seed8e9cf2 --check-only +``` + +The first command prints: + +```text +PASS_E6_B0_COORDINATE_BILINEAR_RANK_FLOOR lines=36 orthogonal_ordered=540 constraint_rank=35 kernel=1 generator_rank=6 no_rank_le4_in_coordinate_form_family no_new_kappa +``` + +The generic package manifest registers a full replay with Python 3.12: + +```sh +python3.12 scripts/research_package.py --package research/e6-coordinate-bilinear-form-seed8e9cf2 +``` + +Python 3.12 is not installed in this environment. Direct verifier, focused tests, and metadata/pin checks were exercised with the available Python 3.14.7; the registered 3.12 replay remains for hosted CI. + +## Provenance and coordination + +- Assignment: OS seed `8e9cf2d0cc1e238cdbea7700328e99f0`; track `complex-mechanisms`; card `complex-rank-shape-decoder`, refined from selector scope `cad3ba853d7f324f16fa`. +- Base: `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`. +- Priority revision 4; catalogue SHA-256 `d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7`. +- Selected record SHA-256 `10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. +- Coordination claim: [Discussion #1166](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18933558), taking the E6 T=4 handoff and narrowing it to this coordinate-form family. +- Predecessor pins: #1590 head `08e134b4a0c7f04869dae703f2a2e688e53c44f0` (merged/closed partial result); #2111 head `98da76c2839ba38538b510420dec54546ccabf0b`; #2125 head `d9eb80ac183bb4df185ca044fd65432b817333bb` at the overlap check. #1590 and #2111 develop the root-unit cost/decoder model; #2125 checks the standard-Gram E6 costs and leaves the E6 windows open. None classifies this rational `L` family. +- Exact predecessor source in this base: `research/root-unit-decoder-lemmas/lib/ade.py`, git blob `7e0063d97673b7d278ac9b5b4b511df8705d5f98`, SHA-256 `8185afc77fd34a599094e9f93b293a5afac61f4184ec5c5a02b81ee3c0b0053c`. + +### Selected-result context + +At the pinned base, `certificates/selected-result.json` points to review `docs/research/community-batch1099-review.md` (SHA-256 `7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb`), source manifest `research/community-frontier1094-audit/SELECTED-SOURCE.json` (SHA-256 `79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b`), certificate `research/community-frontier1094-audit/ASSEMBLY.json` (SHA-256 `1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045`), and full reproduction command `make frontier1094-verify`. `make selected-record-check` and the selected binding baseline pass in this cycle; the full cold replay was not run here and is not evidence for this E6 result. + +Predecessor attribution: DreamingOfClouds' #1590/#2111/#2125 root-unit decoder work and the inherited #446/#595 cost model. Prepared for Adam Gall with substantial OpenAI Codex assistance. No independent human review is claimed. Apache-2.0. + +Prepared for Adam Gall with substantial OpenAI Codex assistance. No independent human review is claimed. Apache-2.0. + +## Open next questions + +- Can an E6 T=4 decoder outside the image of `R` meet a 21–23 cost window? This would test the main omitted decoder family. First name a support alphabet and screen its exact minimum B0 F2 tariff. Arbitrary rational factors are outside the present linear system. +- Does another admissible E6 pairing admit a rank-at-most-four root-coordinate form? The current equations use only B0; a new pairing needs its own exact mask and constraint matrix. diff --git a/research/e6-coordinate-bilinear-form-seed8e9cf2/RESULT.json b/research/e6-coordinate-bilinear-form-seed8e9cf2/RESULT.json new file mode 100644 index 0000000000..d34f72d6db --- /dev/null +++ b/research/e6-coordinate-bilinear-form-seed8e9cf2/RESULT.json @@ -0,0 +1,224 @@ +{ + "ade_source_sha256": "8185afc77fd34a599094e9f93b293a5afac61f4184ec5c5a02b81ee3c0b0053c", + "constraint_rank_Q": 35, + "coordinate_basis_scaled": [ + [ + 0, + 0, + 0, + 0, + 0, + 0, + 2, + -2 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 2 + ], + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + -2, + 0, + 0 + ], + [ + 0, + 0, + 0, + 2, + -2, + 0, + 0, + 0 + ], + [ + 1, + -1, + -1, + -1, + -1, + -1, + -1, + 1 + ] + ], + "decoder_diagonal_scaled": [ + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1", + "8/1" + ], + "gram_matrix": [ + [ + "8/1", + "0/1", + "-4/1", + "0/1", + "0/1", + "-4/1" + ], + [ + "0/1", + "8/1", + "-4/1", + "0/1", + "0/1", + "0/1" + ], + [ + "-4/1", + "-4/1", + "8/1", + "-4/1", + "0/1", + "0/1" + ], + [ + "0/1", + "0/1", + "-4/1", + "8/1", + "-4/1", + "0/1" + ], + [ + "0/1", + "0/1", + "0/1", + "-4/1", + "8/1", + "0/1" + ], + [ + "-4/1", + "0/1", + "0/1", + "0/1", + "0/1", + "8/1" + ] + ], + "input_sha256": { + "basis_scaled": "2b4ad503983b968340b5085814e9865b34a515043c7c9148cc5320c7cb7bdd4a", + "constraints": "718c0bc1a8bc1e74e3a1169007d5e01de404674a17661f63292e531bacbff2ec", + "coordinates": "9564c2c5284ea068a63782cc851f2340e58be14ddc0a72348fd33cc265b42f83", + "e6_lines_scaled": "a6bb381305c166300356c7f8227dc3c49373668f1e349b718253434efb7b1d42", + "e8_lines_scaled": "499909f15616b21ed34b704054685a0c90c244fb81819ba458e076b8dd97308c" + }, + "kernel_dimension_Q": 1, + "kernel_equals_gram_line": true, + "kernel_generator": [ + [ + "1/1", + "0/1", + "-1/2", + "0/1", + "0/1", + "-1/2" + ], + [ + "0/1", + "1/1", + "-1/2", + "0/1", + "0/1", + "0/1" + ], + [ + "-1/2", + "-1/2", + "1/1", + "-1/2", + "0/1", + "0/1" + ], + [ + "0/1", + "0/1", + "-1/2", + "1/1", + "-1/2", + "0/1" + ], + [ + "0/1", + "0/1", + "0/1", + "-1/2", + "1/1", + "0/1" + ], + [ + "-1/2", + "0/1", + "0/1", + "0/1", + "0/1", + "1/1" + ] + ], + "kernel_generator_rank_Q": 6, + "mutant_orthogonal_pair_violations": 260, + "negative_controls": 2, + "positive_controls": 2, + "root_counts": { + "E6_lines": 36, + "E8_lines": 120, + "ordered_orthogonal_pairs": 540 + }, + "scope": "Only M=R L R^T on this fixed E6 root-coordinate realization and B0 orthogonality mask. This is not a theorem about arbitrary E6 decoders, other admissible pairings, or the selected multiplication bound.", + "status": "PASS_E6_B0_COORDINATE_BILINEAR_RANK_FLOOR" +} diff --git a/research/e6-coordinate-bilinear-form-seed8e9cf2/SOURCES.json b/research/e6-coordinate-bilinear-form-seed8e9cf2/SOURCES.json new file mode 100644 index 0000000000..47682f7a74 --- /dev/null +++ b/research/e6-coordinate-bilinear-form-seed8e9cf2/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/root-unit-decoder-lemmas/README.md", + "usage": "provenance", + "git_blob": "de305484c78226a3f8da5f3277ced78974116fbb", + "sha256": "e3c856bc361a57cc2424c829001dba94e8f3a1bc8f6616f9c2f740e9665506a9" + }, + { + "path": "research/root-unit-decoder-lemmas/checks/windows.py", + "usage": "provenance", + "git_blob": "df5d7295d90b90dad39f36f7122179e51fa987f0", + "sha256": "a57dbd02f9576bb2d2aefbd0ed4aac79112ab50a75adb84dfccab79234f13d7a" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "provenance", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "provenance", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "provenance", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/root-unit-decoder-lemmas/lib/ade.py", + "usage": "input", + "git_blob": "7e0063d97673b7d278ac9b5b4b511df8705d5f98", + "sha256": "8185afc77fd34a599094e9f93b293a5afac61f4184ec5c5a02b81ee3c0b0053c" + } + ] +} diff --git a/research/e6-coordinate-bilinear-form-seed8e9cf2/TASK.json b/research/e6-coordinate-bilinear-form-seed8e9cf2/TASK.json new file mode 100644 index 0000000000..ccd6351469 --- /dev/null +++ b/research/e6-coordinate-bilinear-form-seed8e9cf2/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "track": "complex-mechanisms", + "selection_seed": "8e9cf2d0cc1e238cdbea7700328e99f0", + "priority_revision": 4, + "catalogue_sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "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": [ + "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.", + "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." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "scope_key": "e6-b0/root-coordinate-bilinear-form/rankQ-at-most-4", + "scope_change_reason": "The broad E6 non-star/T=4 windows and E6/E7 root-unit threshold evidence are active nearby. This fixes one new algebraic decoder family: a single rational bilinear form on the six-dimensional E6 root coordinates, with rank at most four. It tests a strict construction ansatz not covered by the standard-Gram table and gives a complete exact linear constraint system rather than an open-ended search.", + "object_and_question": "For the 36 normalized E6 root lines with the fixed B0 pairing (B0_ts=1 on distinct orthogonal pairs), determine whether any rational 6x6 matrix L of rank at most four makes M_ts=x_t^T L x_s vanish on every ordered distinct orthogonal pair and remain nonzero on every diagonal entry, where x_t are exact root coordinates in a pinned basis.", + "changed_hypothesis": "Restrict the decoder to M=R L R^T and rank_Q(L)<=4. This is narrower than an arbitrary rational four-total decoder. The favorable T=4 cost screen charges only the E6 per-total floor w=5, giving 20; E6 T=4 window thresholds are 21, 22 and 23. Forms with fewer than four totals are cheaper in this relaxation. Grant copies, frame changes, source access, restoration, hosting and precision for free. If a form survives, compute the exact F2 support-rank tariff before making any construction claim.", + "method_and_domain": "Generate the complete E6 line set exactly from the E8 D8 and half-sign root families, choose and pin six independent roots, express all 36 roots in Q^6, then row-reduce over Q the 540 ordered orthogonal-pair constraints on all 36 entries of L. Test the complete solution-space basis for rank and diagonal conditions. One bounded pivot is allowed only if the exact nullspace is not one-dimensional; no random rational sampling or general E6 decoder search.", + "predecessors_and_overlap": [ + "PR #1590 head 08e134b4a0c7f04869dae703f2a2e688e53c44f0 / research/root-unit-decoder-lemmas: Lemma A covers T<=2 and E6 T>=3 remains open; standard-Gram B0 decoder is cost 37.", + "PR #2111 head 98da76c2839ba38538b510420dec54546ccabf0 / research/three-total-decoders: T=3 reductions and lift question, not the T=4 coordinate-form family.", + "PR #2125 head d9eb80ac183bb4df185ca044fd65432b817333bb / research/char2-threshold: exact standard-Gram costs and broad threshold evidence; it explicitly leaves E6 windows open and does not classify this L-family.", + "Discussion #1166 comment DC_kwDOU-508s4BIOSd: unclaimed E6 non-star and T=4 handoff; this claim narrows that handoff to a distinct rational coordinate-form family." + ], + "expected_evidence": "A standard-library exact verifier with the root-coordinate and constraint hashes, rational row-reduction result, rank and diagonal certificates, Gram positive control, and semantic negative controls. If a rank<=4 form survives, include its exact support decomposition and fully charged B0 F2 block profile; otherwise state only the scoped family obstruction. No selected-record or kappa change.", + "stop_rule": "Stop after exact elimination and one bounded structural pivot if needed. This replay found a one-dimensional kernel, so no pivot is needed. Do not promote the result to an obstruction for unrestricted E6 decoders.", + "claim_expiry_utc": "2026-10-14T22:30:00Z", + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18933558", + "actual_scope": "Classify the full rational linear space of E6 B0 exact decoders that factor through the six-dimensional root-coordinate map, then test whether any member has at most four rational totals.", + "bottleneck_link": "The open E6 T=4 root-unit windows require costs 21-23. A root-coordinate form with rank at most four would have an ideal floor-only bill at most 20, so excluding this family removes one plausible low-total mechanism while leaving arbitrary decoders open.", + "evidence": "Exact standard-library replay: 36 E6 lines, 540 ordered orthogonal-pair equations, rational constraint rank 35, one-dimensional kernel generated by the rank-six Gram form; positive Gram controls and zero/mutant negative controls pass.", + "budget_minutes": 60, + "outcome": "negative-result", + "author": "Adam Gall", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematical formulation, exact implementation, verification and documentation.", + "open_questions": [ + { + "question": "Can an E6 T=4 decoder outside the image of the six-dimensional root-coordinate map meet one of the 21-23 cost windows?", + "why_it_matters": "The exact kernel result rules out only a natural four-total coordinate-form family; other rational support vectors could still improve the E6 window.", + "first_step": "Specify a new support alphabet outside the root-coordinate image and compute its optimistic B0 F2 tariff before any synthesis.", + "blocked_by": "This package imposes p_j and q_j in the root-coordinate image and does not classify arbitrary rational decoder factors." + }, + { + "question": "Can another admissible E6 pairing admit a rank-at-most-four coordinate form?", + "why_it_matters": "The computed constraints use only the fixed B0 orthogonality mask.", + "first_step": "Name a new admissible pairing and generate its exact ordered zero constraints.", + "blocked_by": "This package does not enumerate or classify admissible pairings." + } + ], + "selector_scope_key": "cad3ba853d7f324f16fa", + "selected_method": "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." +} diff --git a/research/e6-coordinate-bilinear-form-seed8e9cf2/VERIFY.json b/research/e6-coordinate-bilinear-form-seed8e9cf2/VERIFY.json new file mode 100644 index 0000000000..9076aa432a --- /dev/null +++ b/research/e6-coordinate-bilinear-form-seed8e9cf2/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/root-unit-decoder-lemmas/lib/ade.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact E8/E6 root generation, all 540 ordered orthogonal constraints on Q^36, rational rank 35 and one-dimensional Gram kernel, full-rank conclusion, diagonal and orthogonality positive controls, and zero/mutated-form negative controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Focused unittest groups for domain counts, exact kernel result, Gram positive control, and semantic zero/mutant negative controls." + } + ] +} diff --git a/research/e6-coordinate-bilinear-form-seed8e9cf2/test_verify.py b/research/e6-coordinate-bilinear-form-seed8e9cf2/test_verify.py new file mode 100644 index 0000000000..1a44f8df9d --- /dev/null +++ b/research/e6-coordinate-bilinear-form-seed8e9cf2/test_verify.py @@ -0,0 +1,37 @@ +#!/usr/bin/env python3 +"""Focused positive and semantic negative controls for the exact E6 screen.""" + +import unittest +import sys +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from verify import solve_family + + +class E6CoordinateBilinearFormTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.result = solve_family() + + def test_exact_domain_and_constraint_rank(self): + self.assertEqual(self.result["root_counts"], { + "E8_lines": 120, + "E6_lines": 36, + "ordered_orthogonal_pairs": 540, + }) + self.assertEqual(self.result["constraint_rank_Q"], 35) + self.assertEqual(self.result["kernel_dimension_Q"], 1) + + def test_gram_positive_control_and_rank_obstruction(self): + self.assertTrue(self.result["kernel_equals_gram_line"]) + self.assertEqual(self.result["kernel_generator_rank_Q"], 6) + self.assertEqual(set(self.result["decoder_diagonal_scaled"]), {"8/1"}) + + def test_zero_and_mutated_form_negative_controls(self): + self.assertEqual(self.result["negative_controls"], 2) + self.assertGreater(self.result["mutant_orthogonal_pair_violations"], 0) + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/e6-coordinate-bilinear-form-seed8e9cf2/verify.py b/research/e6-coordinate-bilinear-form-seed8e9cf2/verify.py new file mode 100644 index 0000000000..4b04bdf4de --- /dev/null +++ b/research/e6-coordinate-bilinear-form-seed8e9cf2/verify.py @@ -0,0 +1,233 @@ +#!/usr/bin/env python3 +"""Exact E6 B0 screen for one rational root-coordinate bilinear form.""" + +import hashlib +import itertools +import json +import sys +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +ADE = ROOT / "research/root-unit-decoder-lemmas/lib/ade.py" +ADE_SHA256 = "8185afc77fd34a599094e9f93b293a5afac61f4184ec5c5a02b81ee3c0b0053c" + + +def check(condition, message): + if not condition: + raise RuntimeError(message) + + +def normalized_lines(vectors): + out = set() + for vector in vectors: + v = tuple(vector) + first = next((x for x in v if x), None) + check(first is not None, "zero root") + if first < 0: + v = tuple(-x for x in v) + out.add(v) + return sorted(out) + + +def e8_lines_scaled(): + """The 120 E8 root lines, with every root scaled by two.""" + roots = [] + for i in range(8): + for j in range(i + 1, 8): + for sign in (1, -1): + v = [0] * 8 + v[i], v[j] = 2, 2 * sign + roots.append(v) + for signs in itertools.product((-1, 1), repeat=8): + if signs.count(-1) % 2 == 0: + roots.append(signs) + return normalized_lines(roots) + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b)) + + +def rref(rows, ncols): + a = [list(map(Q, row)) for row in rows] + pivot_cols = [] + row = 0 + for col in range(ncols): + p = next((i for i in range(row, len(a)) if a[i][col]), None) + if p is None: + continue + a[row], a[p] = a[p], a[row] + scale = a[row][col] + a[row] = [x / scale for x in a[row]] + for i in range(len(a)): + if i != row and a[i][col]: + scale = a[i][col] + a[i] = [x - scale * y for x, y in zip(a[i], a[row])] + pivot_cols.append(col) + row += 1 + if row == len(a): + break + return a[:row], pivot_cols + + +def rank_q(rows, ncols): + return len(rref(rows, ncols)[1]) + + +def solve_square(a, b): + n = len(a) + m = [list(map(Q, row)) + [Q(x)] for row, x in zip(a, b)] + for col in range(n): + p = next((i for i in range(col, n) if m[i][col]), None) + check(p is not None, "coordinate Gram matrix is singular") + m[col], m[p] = m[p], m[col] + d = m[col][col] + m[col] = [x / d for x in m[col]] + for i in range(n): + if i != col and m[i][col]: + c = m[i][col] + m[i] = [x - c * y for x, y in zip(m[i], m[col])] + return [m[i][-1] for i in range(n)] + + +def qstr(x): + x = Q(x) + return f"{x.numerator}/{x.denominator}" + + +def matrix_rank(a): + return rank_q(a, len(a[0]) if a else 0) + + +def bilinear(x, l, y): + return sum(x[i] * l[i][j] * y[j] for i in range(len(x)) for j in range(len(y))) + + +def solve_family(): + source_hash = hashlib.sha256(ADE.read_bytes()).hexdigest() + check(source_hash == ADE_SHA256, "pinned ADE root source changed") + + e8 = e8_lines_scaled() + check(len(e8) == 120, "E8 line count") + r1, r2 = (2, 2, 0, 0, 0, 0, 0, 0), (2, 0, 2, 0, 0, 0, 0, 0) + check(dot(r1, r1) == dot(r2, r2) == 8 and abs(dot(r1, r2)) == 4, "A2 pin") + roots = [r for r in e8 if dot(r, r1) == 0 and dot(r, r2) == 0] + check(len(roots) == 36, "E6 line count") + check(all(dot(r, r) == 8 for r in roots), "E6 root norm") + + basis = [] + for r in roots: + if rank_q(basis + [r], 8) > len(basis): + basis.append(r) + if len(basis) == 6: + break + check(len(basis) == 6, "E6 coordinate basis rank") + gram = [[Q(dot(x, y)) for y in basis] for x in basis] + check(matrix_rank(gram) == 6, "basis Gram rank") + coords = [] + for r in roots: + rhs = [dot(b, r) for b in basis] + coords.append(solve_square(gram, rhs)) + check(all(sum(coords[t][i] * basis[i][k] for i in range(6)) == roots[t][k] + for t in range(36) for k in range(8)), "root coordinate reconstruction") + + orthogonal = [(t, s) for t in range(36) for s in range(36) + if t != s and dot(roots[t], roots[s]) == 0] + check(len(orthogonal) == 540, "ordered B0 orthogonal-pair count") + constraints = [] + for t, s in orthogonal: + constraints.append([coords[t][i] * coords[s][j] + for i in range(6) for j in range(6)]) + reduced, pivots = rref(constraints, 36) + free = [j for j in range(36) if j not in pivots] + check(len(free) == 1, f"unexpected kernel dimension {len(free)}") + f = free[0] + vector = [Q(0)] * 36 + vector[f] = Q(1) + for ri, p in enumerate(pivots): + vector[p] = -reduced[ri][f] + kernel = [[vector[6 * i + j] for j in range(6)] for i in range(6)] + check(matrix_rank(kernel) == 6, "kernel generator is not full rank") + + factor = None + for i in range(6): + for j in range(6): + if gram[i][j]: + factor = kernel[i][j] / gram[i][j] + break + if factor is not None: + break + check(factor is not None and factor != 0, "zero kernel generator") + check(all(kernel[i][j] == factor * gram[i][j] for i in range(6) for j in range(6)), + "kernel is not exactly the Gram line") + + # Positive control: the Gram form vanishes on every orthogonal pair and has nonzero diagonal. + diagonal = [bilinear(coords[t], gram, coords[t]) for t in range(36)] + check(diagonal == [Q(8)] * 36, "Gram diagonal control") + check(all(bilinear(coords[t], gram, coords[s]) == 0 for t, s in orthogonal), + "Gram orthogonality control") + + # Negative controls: the zero form violates exactness; a rank-one perturbation violates B0. + zero_diagonal = [bilinear(x, [[Q(0)] * 6 for _ in range(6)], x) for x in coords] + check(not any(zero_diagonal), "zero-form control should fail exactness") + mutant = [row[:] for row in gram] + mutant[0][0] += 1 + violating = [(t, s) for t, s in orthogonal if bilinear(coords[t], mutant, coords[s]) != 0] + check(violating, "mutated-form control should violate an orthogonal-pair zero") + + def matrix_json(m): + return [[qstr(x) for x in row] for row in m] + + canonical = { + "e8_lines_scaled": [list(x) for x in e8], + "e6_lines_scaled": [list(x) for x in roots], + "basis_scaled": [list(x) for x in basis], + "coordinates": matrix_json(coords), + "constraints": [[qstr(x) for x in row] for row in constraints], + } + hashes = { + key: hashlib.sha256(json.dumps(value, sort_keys=True, separators=(",", ":")).encode()).hexdigest() + for key, value in canonical.items() + } + return { + "status": "PASS_E6_B0_COORDINATE_BILINEAR_RANK_FLOOR", + "ade_source_sha256": source_hash, + "root_counts": {"E8_lines": len(e8), "E6_lines": len(roots), "ordered_orthogonal_pairs": len(orthogonal)}, + "coordinate_basis_scaled": [list(x) for x in basis], + "constraint_rank_Q": len(pivots), + "kernel_dimension_Q": len(free), + "kernel_generator": matrix_json(kernel), + "gram_matrix": matrix_json(gram), + "kernel_equals_gram_line": True, + "kernel_generator_rank_Q": matrix_rank(kernel), + "decoder_diagonal_scaled": [qstr(x) for x in diagonal], + "mutant_orthogonal_pair_violations": len(violating), + "negative_controls": 2, + "positive_controls": 2, + "input_sha256": hashes, + "scope": "Only M=R L R^T on this fixed E6 root-coordinate realization and B0 orthogonality mask. This is not a theorem about arbitrary E6 decoders, other admissible pairings, or the selected multiplication bound.", + } + + +def main(): + write = "--write" in sys.argv[1:] + result = solve_family() + encoded = json.dumps(result, sort_keys=True, indent=2) + "\n" + out = HERE / "RESULT.json" + if write: + out.write_text(encoded) + elif out.exists(): + check(json.loads(out.read_text()) == result, "RESULT.json differs from exact replay") + print(result["status"], + f"lines={result['root_counts']['E6_lines']}", + f"orthogonal_ordered={result['root_counts']['ordered_orthogonal_pairs']}", + f"constraint_rank={result['constraint_rank_Q']}", + f"kernel={result['kernel_dimension_Q']}", + f"generator_rank={result['kernel_generator_rank_Q']}", + "no_rank_le4_in_coordinate_form_family no_new_kappa") + + +if __name__ == "__main__": + main()