From c01e6854c5d3614477f37f4b712b5b09a1bba5e6 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Thu, 15 Oct 2026 16:09:37 +0530 Subject: [PATCH 1/3] E6/D5 rank-T realisations: E6 Gram point locally rigid; D5 non-Gram family, normal form and floor 20 (#2277 OQ4) Research note, no kappa claim. New package research/e6-d5-gram-realisation-rigidity: - E6: dim T_G V = 71 = 2v-1 (prime-rank upper bound at two primes and in a second coordinate model, matched by the scaling orbit) => Gram point smooth, local component = scaling orbit (local rigidity only). - D5: tangent 55 = 39 + 16, explicit 16-parameter non-Gram rank-5 family; written proofs that D5 has no rank-4 realisation and every rank-5 realisation is edge-supported (construction replayed exactly), so the #2277 dense floor 20 holds for every rank-<=5 realisation of D5. - Controls D4/D6/E7 (E8 behind --e8) and negative controls. Credits #2277/#2228 (DreamingOfClouds), #2338, #1212/#1292/#1389/#1399/#1425/#1367, #2351. Prepared by thakrarsagar with substantial AI assistance from Claude (Claude Opus 5.5). Co-Authored-By: Claude Opus 5.5 --- .../e6-d5-gram-realisation-rigidity/README.md | 268 +++++++ .../SOURCES.json | 18 + .../e6-d5-gram-realisation-rigidity/TASK.json | 88 +++ .../VERIFY.json | 18 + .../e6-d5-gram-realisation-rigidity/verify.py | 671 ++++++++++++++++++ 5 files changed, 1063 insertions(+) create mode 100644 research/e6-d5-gram-realisation-rigidity/README.md create mode 100644 research/e6-d5-gram-realisation-rigidity/SOURCES.json create mode 100644 research/e6-d5-gram-realisation-rigidity/TASK.json create mode 100644 research/e6-d5-gram-realisation-rigidity/VERIFY.json create mode 100644 research/e6-d5-gram-realisation-rigidity/verify.py diff --git a/research/e6-d5-gram-realisation-rigidity/README.md b/research/e6-d5-gram-realisation-rigidity/README.md new file mode 100644 index 0000000000..c32aa37d00 --- /dev/null +++ b/research/e6-d5-gram-realisation-rigidity/README.md @@ -0,0 +1,268 @@ +# E6 is locally rigid at the Gram point; D5 is not rigid, but every rank-5 D5 realisation keeps the floor 20 (#2277 OQ4) + +**Status: research note (scoped result). No κ claim, no supplier change, no +frontier unit.** This note addresses open question 4 of #2277 ("E6 / D5 +realisation-free: rigidity of the Gram point and global uniqueness at rank `T` +are open"). The **D5 half is answered at rank `T`.** D5 has no rank-4 +realisation. Its rank-5 realisations are *not* unique up to scaling, since they +form an irreducible 55-dimensional family, which is 16 dimensions more than the +scaled-Gram orbit. Even so, every one of them keeps #2277's dense floor 20. The +**E6 half is answered locally.** The Gram point is a smooth point whose only +local component is the scaling orbit. Global uniqueness for E6 and rank-5 +realisations of E6 remain open. + +## Setting (from #2277 §1, §5, §7) + +A **realisation** of a unit with lines `r_1..r_v` is `M ∈ K^{v×v}` with +`M_tt ≠ 0` and `M_ts = 0` whenever `r_t ⊥ r_s`. Let `V_U` be the variety of +realisations of rank `≤ T` (`T = dim span r_t`) and `G` the Gram matrix. The +**scaling orbit** `{D₁ G D₂}` (invertible diagonal `D₁, D₂`) lies in `V_U` +and has dimension `2v − 1`. #2277 proves E6 `≥ 36` and D5 `≥ 20` (dense +pairing, factors in `col M` / `row M`, any number of terms) for the scaled-Gram +realisations `D₁ G D₂` only; E6 and D5 have no `T`-frame (`α_⊥ = 4`), so its +realisation-free Theorem 4′ / Lemma 5.2 certificate gives nothing for them. + +## Results + +| unit | v | T | `dim T_G V_U` (exact) | scaling orbit `2v−1` | verdict at `G` | +|---|---|---|---|---|---| +| **E6** | 36 | 6 | **71** | 71 | smooth point; local component = scaling orbit (**locally rigid**) | +| **D5** | 20 | 5 | **55** | 39 | not rigid: every rank-5 realisation is edge-supported (Theorem D), i.e. a scaling of an explicit **16-parameter non-Gram family** or a boundary point of it; no rank-4 realisation (Theorem E); floor 20 everywhere | +| E7 (control) | 63 | 7 | 125 | 125 | locally rigid | +| E8 (control, `--e8`, ~145 s) | 120 | 8 | 239 | 239 | locally rigid | +| D6 (control) | 30 | 6 | 84 | 59 | smooth; edge family realises all 25 extra directions | +| D4 (control) | 12 | 4 | 44 | 23 | edge family gives only 9 of the 21 extra directions (rest not integrated here) | + +**Theorem A (E6 local rigidity) — PROVEN from CHECKED data.** The Zariski +tangent space of `V_E6` at `G` has dimension 71. Hence `G` is a nonsingular +point of `V_E6`, the only irreducible component through `G` is the closure of +the scaling orbit, and there is a Zariski-open neighbourhood `W ∋ G` in `V_E6` +with `W ⊆ {D₁ G D₂}`. In particular every rank-6 realisation of E6 close enough +to `G` (Zariski, or Euclidean over `R`/`C`) is scaled-Gram, so #2277 Theorem 7.3 +(E6 `≥ 36`) applies to it. + +*Proof.* At a rank-`T` point the determinantal variety is smooth with tangent +`{dX Yᵀ + X dYᵀ}` (`G = X Yᵀ`, `X, Y ∈ K^{v×T}` of rank `T`), so +`T_G V = {dX Yᵀ + X dYᵀ : entries on ordered orthogonal pairs vanish}`. The +map `(dX, dY) ↦ dX Yᵀ + X dYᵀ` has kernel `{(XA, −YAᵀ)}` of dimension `T²`. +`verify.py` builds the 540 × 432 integer system and finds rank 325 modulo +`p = 1000003` and `p = 998244353`; since `rank_p ≤ rank_Q`, the solution space +has dimension `≤ 432 − 325 = 107`, so `dim T_G V ≤ 107 − 36 = 71`. The `2v` +vectors `E_tt G`, `G E_ss` lie in `T_G V` and have prime rank 71, so they span +71 dimensions over `Q`. The orbit is a 71-dimensional irreducible subvariety of +`V` through `G`, so `71 ≤ dim_G V ≤ dim T_G V = 71`. A local ring whose +dimension equals its tangent dimension is regular, hence a domain, so exactly +one component passes through `G`. It contains the orbit closure and has the +same dimension, so it equals that closure. Torus orbits are open in their +closures. ∎ +The count is reproduced in a second coordinate model: E6 as the E8 lines in +doubled coordinates orthogonal to two roots at 120°, using `#2277`'s +convention, with 36 vectors in `Z⁸` of rank 6. Ambient components orthogonal +to the span add a known kernel. + +**Theorem B (D5 is not rigid; explicit family) — PROVEN, CHECKED.** For +parameters `a_ij, b_ij ∈ K^*` with `a_ij + b_ij ≠ 0` (one pair per edge +`{i, j}` of `K₅`), put +``` +x_{ij+} = e_i + a_ij e_j, x_{ij-} = e_i − b_ij e_j, +y_{ij+} = e_i + b_ij⁻¹ e_j, y_{ij-} = e_i − a_ij⁻¹ e_j, M(a,b) = X Yᵀ. +``` +Then `M(a,b)` is a rank-5 realisation of D5. Lines with disjoint support give +0. For the same edge, opposite signs give `1 − a·a⁻¹ = 0` and +`1 − b·b⁻¹ = 0`. The diagonal entries are `1 + a/b` and `1 + b/a`, both +nonzero. `M(1,1) = G`. At three explicit rational points (`D5_POINTS` in +`verify.py`), `M` has 240 ordered pairs that violate the scaled-Gram invariant +`M_ts M_st G_tt G_ss = G_ts² M_tt M_ss`, so `M ≠ D₁ G D₂`. The Gram parameters +give 0 violations, which is the control. The tangent space has `dim T_G V_D5 = 55` +(the upper bound comes from the prime rank). The 20 parameter derivatives +together with the 40 scaling directions span 55 dimensions, which is the lower +bound. So `G` is a smooth point with local dimension 55. Near `G`, every rank-5 +realisation has the form `D₁ M(a,b) D₂`, because the inverse function theorem +applies to `(a, b, D₁, D₂) ↦ D₁ M(a,b) D₂`. The family has `16 = 20 − 4` +parameters modulo the coordinate torus `e_i ↦ d_i e_i`. + +**Theorem C (the D5 floor 20 survives on the whole family) — PROVEN from +CHECKED data, using #2277's Theorem 4′ and the argument of its Theorem 7.4.** +Take any member `M(a,b)` and any decoder with `p_j = X x_j`, `q_j = Y y_j` +(`col P ⊆ col M`, `col Q ⊆ row M`, every square decoder) under the dense +pairing. Its cost is at least 20, and the coordinate decoder `p_a = X e_a`, +`q_a = Y e_a` attains 20. +*Proof.* The columns of `e_i+e_j` and `e_i−e_j` in `B_d` coincide, so every +one of the 31 classes is a union of `±` edge pairs (CHECKED). **Lemma S:** +`span{x_t : t ∈ O} = span{e_i : i covered by the edges of O}`, and the same +holds for `y`. This follows because `x_{ij±}` span `⟨e_i, e_j⟩` iff +`a + b ≠ 0`, and `y_{ij±}` span it iff `(a+b)/(ab) ≠ 0`. Only the 5 axis +classes (all 12 lines avoiding a vertex `a`) miss a vertex (CHECKED). So in +every member the π- and κ-deficient classes are exactly the 5 axis classes, +with annihilator `e_a`. Also `R(e_a) = A(e_a) = {lines through a}`. Both facts +are identical to the Gram case. By #2277 Lemma 5.1 the term ranks are therefore +the same: matched 4, unmatched 3, one deficient 4, none 5 (CHECKED). Since +`M = X I Yᵀ` with injective `X`, `Y`, we get `Σ_j x_j y_jᵀ = I_5` under the +standard pairing. The proof of #2277 Theorem 7.4 then goes through verbatim; its +core combinatorial fact, that no three pairs satisfy `b_i = a_j`, is +re-checked. ∎ +Theorem D below shows that this family, together with its boundary, contains +*every* rank-5 realisation and not just those near `G`. + +**Theorem E (D5 has no realisation of rank 4) — PROVEN (written proof).** +Every realisation of D5 therefore has rank `≥ 5`, which improves the frame +bound `α_⊥ = 4`. +*Proof.* Write `M = P Qᵀ` (`P, Q ∈ K^{20×ρ}` of rank `ρ`). Let `W_e` and +`U_e` be the spans of the `p`- and `q`-rows of the two lines on an edge `e`. +Each is 2-dimensional because the 2×2 block of the two orthogonal lines is +diagonal and invertible. For disjoint edges `W_e ⊥ U_f`. The four lines of two +disjoint edges form a 4-frame, so their `p`-rows are independent, and likewise +their `q`-rows. Now let `ρ = 4` and take any edge `ij` with complementary +vertices `k, l, m`. Then `W_ij` is 2-dimensional and lies in `U_kl^⊥`, which is +also 2-dimensional, so `W_ij = U_kl^⊥ = U_km^⊥ = U_lm^⊥`. Hence +`U_kl = U_km = U_lm =: U`. Since `W_ik ⊥ U_lm = U` and `W_jl ⊥ U_km = U`, the +4-dimensional space `W_ik ⊕ W_jl` (from the 4-frame `{ik±, jl±}`) lies in the +2-dimensional `U^⊥`, a contradiction. ∎ + +**Theorem D (every rank-5 realisation of D5 is edge-supported) — PROVEN +(written proof); construction CHECKED on 5 instances.** If `rank M = 5`, there +are dual bases `f_a`, `g_a` (`f_a·g_c = δ_ac`) with `p_t ∈ ⟨f_i, f_j⟩` and +`q_t ∈ ⟨g_i, g_j⟩` for every line `t` on edge `ij`. Equivalently, +`M = X Yᵀ` with `x_t, y_t` supported on the edge of `t`, `x_{ij±}` a basis of +`⟨e_i, e_j⟩`, `y_{ij+} ⊥ x_{ij−}` and `y_{ij−} ⊥ x_{ij+}`. This is the +closure of the family of Theorem B, with boundary points such as +`x_{01+} = e_0`. The realisation variety of D5 is therefore irreducible of +dimension `60 − 5 = 55`, consistent with the tangent count. +*Proof* (notation as in Theorem E, `ρ = 5`, complements taken in the five +vertices). +(i) Suppose `U_ij = U_ik = U_jk = U` for a triangle `ijk` with complement +`lm`. Then `W_il ⊥ U_jk` and `W_jm ⊥ U_ik`, so the 4-frame `{il±, jm±}` lies +in the 3-dimensional `U^⊥`, which is impossible. Also `W_e ⊥ U_lm` for every +edge `e ⊂ ijk`. Hence `dim U_ijk = dim W_ijk = 3`, `W_ijk = U_lm^⊥`, and +`W_ab = U_cde^⊥`; dually `U_ab = W_cde^⊥`. +(ii) At a vertex `a`, any two planes `W_ak`, `W_al` meet in exactly a line. +They meet in at least a line because both lie in the 3-dimensional `W_akl`. +They meet in at most a line because `W_ak ∩ W_al = (U_lrs + U_krs)^⊥`, and that +sum contains the 4-frame span `U_lr ⊕ U_ks`. +(iii) No three of the `W_ak` lie in one 3-space `Z`. Otherwise the three +triangle spans `U_T` (with `W_ak = U_T^⊥`) would all contain `N = Z^⊥`. Any two +of these spans are distinct, because their sum contains a 4-frame span such as +`U_24 ⊕ U_13`. Their pairwise intersections are therefore the shared edge +planes, so this gives +`U_14 = U_24 = U_34 = N` (written for `a = 0` and `k = 1, 2, 3`). Then +`W_012 = W_013 = W_023 = N^⊥` by (i), and this 3-space would contain the +4-frame span `W_01 ⊕ W_23`. +(iv) Lines in `P⁴` that pairwise meet and of which no three are coplanar all +pass through one point. So `L_a := ∩_k W_ak` is a line. If `L_a = L_b`, it would +lie in `W_ac ∩ W_bd` for a 4-frame `{ac±, bd±}`, so the `L_a` are distinct and +`W_ab = L_a ⊕ L_b`. Since `rank P = 5`, the `L_a` form a basis `f_a`. The same +argument on the `q` side gives `g_a`. +(v) For `a ≠ c`, pick `b, d` so that `ab` and `cd` are disjoint. Then +`W_ab ⊥ U_cd` gives `f_a ⊥ g_c`. Rescaling makes the bases dual. ∎ +`verify.py` (`d5_normal_form`) starts from `M` alone and carries out (i)–(v) +with exact Fractions: it builds the rank factorisation, computes the `W_e`, +triangle spans, the pairwise meets, `L_a`, the dual pairing and the +edge-supported normal form. The inputs are the three family points and the Gram +matrix (each with fixed non-trivial `D₁`, `D₂`) and one boundary member. The +negative control is a rank-5 matrix that breaks 4 orthogonal zeros, and the +construction fails on it. + +**Corollary (#2277 OQ4, D5 half).** Theorem C applies verbatim to every +edge-supported realisation, including boundary members. Lemma S needs only +that `x_{ij±}` and `y_{ij±}` each span `⟨e_i, e_j⟩`. On boundary members +`R(e_a)` can lose one line of an edge, but classes are `±`-closed, so `Def(R(e_a))` +is unchanged. The verifier recomputes the actual ranks, matched 4 and +unmatched 3. By Theorems D and E, **every realisation of D5 of rank `≤ 5` +has dense-pairing cost `≥ 20`** for decoders with `col P ⊆ col M` and +`col Q ⊆ row M`, which includes all square decoders. The bound is attained. +Realisations of rank `> 5` remain outside, as in #2277 §6. + +**Robustness observation (CHECKED).** The E6 count is insensitive to small +pattern deletions. Removing one orthogonal pair, or up to 10 of the 15 +orthogonality constraints of one line (in the verifier's order), leaves +dimension 71. Each further removal adds 2, reaching 81 when line 0 is +unconstrained. + +## Reproduce + +```sh +python3 -I -B research/e6-d5-gram-realisation-rigidity/verify.py # ~8 s, stdlib +# expected last line: ALL 41 CHECKS PASSED in s +python3 -I -B research/e6-d5-gram-realisation-rigidity/verify.py --e8 # adds E8 239 = 2v-1: ALL 42 CHECKS PASSED (~145 s) +python3 scripts/research_package.py --package research/e6-d5-gram-realisation-rigidity --check-only +``` + +**Negative controls (each must fail its acceptance test; verify.py asserts that +they do):** +- E6 with the 15 orthogonality constraints of line 0 removed is not rigid + (81 > 71). +- D5 with one orthogonal pair removed has tangent 57 ≠ 55, which shows the + count depends on the pattern. +- A sign error in `y_{ij-}` breaks the pattern zeros. +- The inadmissible `a = −b` on one edge gives a zero diagonal and 6 deficient + classes, so Lemma S fails. +- Half the family (`b` frozen) together with the orbit spans only 49 < 55. +- The Theorem D construction applied to a rank-5 non-realisation (4 orthogonal + zeros broken) fails. +- Positive control: the Gram parameters give 0 scaling violations. + +## Scope, inherited assumptions, unresolved obligations + +- **E6: local, not global.** Theorem A says nothing about rank-6 realisations + outside a neighbourhood of `G`, for example on other components of `V_E6`. + It does not exclude rank-5 realisations of E6, and no rank-5 search was run. +- **D5: rank `≤ 5` only.** Theorems D and E are written proofs. The verifier + replays the construction of Theorem D on 5 exact instances and one negative + control. That replay is evidence for the proof, not a machine-checked proof + of it. Realisations of rank `> 5` are not covered. +- **Rank exactly `T`, factors in `col M` / `row M`, dense pairing.** These + hypotheses are inherited from #2277 Theorem 4′. Arbitrary `B`, factors + outside `col M`, and realisations of rank `> T` are not covered. +- **Inherited:** #2277 Lemma 5.1, Theorem 4′, Lemma OC and the Theorem 7.4 + argument. These are PROVEN in the open PR #2277 (head `ca7f9992`) and are not + re-proved here; only their hypotheses for the D5 family are checked. +- Prime ranks are used only in the safe direction (`rank_p ≤ rank_Q`). All + other acceptance checks use exact integer, `Fraction` or `F₂` arithmetic. + This is a finite exact certificate combined with written proofs. It is not + a formalisation. +- D5 is not a frontier unit. Nothing here changes a supplier, a call profile + or κ. + +## Open next questions + +The structured list is in [TASK.json](TASK.json): +1. **Global uniqueness at rank 6 for E6.** This would make E6 `≥ 36` + realisation-free at rank `T`. A first step is exact elimination on a + normalised sub-configuration. The blocker is that there is no frame argument. +2. **Rank-5 realisations of E6** (dense cost `≤ 35` if one exists). By + Theorems D and E, the D5 sub-configuration of such a realisation would have + rank exactly 5 and be edge-supported. For each of the 16 extra lines `s` + (signs `ε`), `p_s` restricted to edge `ij` must then be proportional to the + `x` of the line on `ij` that is not orthogonal to `s`. *Unchecked sketch:* + in the open chart, where every `x_t, y_t` has full edge support, the 16 sign + patterns force `a_ij = b_ij` and a cocycle. That means a scaled-Gram D5 + part, which then violates the 5 extra–extra orthogonalities + (`ε·ε' = −3 ≠ 0`). The first step is to make this exact and extend it to + the boundary charts. The blocker is the case analysis of degenerate edges. +3. **D5 at rank `> 5`.** This is #2277's §6 cap and the last gap in a + realisation-free D5 `≥ 20` with factors in `col M`. A first step is to count + deficient classes in a rank-6 lift of the edge-supported family. The blocker + is that Theorem 4′ no longer forces `ρ` terms of full deficiency control. +4. **Which other units are first-order rigid?** For D4 there are 12 tangent + directions beyond the edge family. P112, P104 and E7-frame can be tested + with this verifier's functions. + +## Base, sources, credit + +- Base commit `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`. The selected record + `certificates/selected-result.json` (sha256 `10b9e340…fa32`) is unchanged. + Provenance pins are in [SOURCES.json](SOURCES.json). The package has no live + input files: every unit is rebuilt from Cartan matrices or coordinates. +- Definitions, Theorem 4′, Lemma 5.1, Lemma 7.1, Theorem 7.4 and OQ4 are from + **#2277** and **#2228** (DreamingOfClouds), cited at #2277 head + `ca7f99921f03398d303bba90245d3ee2e38e95c3`. +- **#2338** (Theorem R) concerns F₂ pairing-table rigidity, which is a + different object. +- The tangent-versus-torus rigidity method on rank-8 units comes from **#1212, + #1292, #1389, #1399, #1425**, with the audit in **#1367**. The model comes + from **#2125** and **#1590**. +- The E6 screens are **#2137, #2232, #2240, #2247** (1337isnot1337) and + **#2272** (navinor). EdDiboi contributed the local E6 seven-term audit (#1166). + The first-order jet method follows the earlier loop PR **#2351**. + +Prepared by thakrarsagar with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). Apache-2.0. diff --git a/research/e6-d5-gram-realisation-rigidity/SOURCES.json b/research/e6-d5-gram-realisation-rigidity/SOURCES.json new file mode 100644 index 0000000000..392737aa2a --- /dev/null +++ b/research/e6-d5-gram-realisation-rigidity/SOURCES.json @@ -0,0 +1,18 @@ +{ + "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" + } + ] +} diff --git a/research/e6-d5-gram-realisation-rigidity/TASK.json b/research/e6-d5-gram-realisation-rigidity/TASK.json new file mode 100644 index 0000000000..95a9f95f53 --- /dev/null +++ b/research/e6-d5-gram-realisation-rigidity/TASK.json @@ -0,0 +1,88 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "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", + "actual_scope": "#2277 open question 4 (E6 / D5 realisation-free): is the Gram point G of the rank-<=T realisation variety (M_tt != 0, M_ts = 0 for orthogonal t,s) rigid up to diagonal scalings D1 G D2 for E6 (v=36, T=6) and D5 (v=20, T=5), and does the dense-pairing floor of #2277 survive on non-Gram realisations?", + "scope_change_reason": "The generic rank-shape card is crowded by masked/overcomplete decoder searches (#2430, #2338, #2240, #2247, #2232, #2137). #2277 proves E6 >= 36 and D5 >= 20 only for scaled-Gram realisations and lists rigidity of the Gram point as open; a non-Gram rank-T realisation is a decoder geometry outside those floors (Theorem 4' gives nothing because E6/D5 have no T-frame). This is a structural decoder question (seed 49, track 40-49), not a per-call profile, so the card's 5% ceiling gate does not apply.", + "bottleneck_link": "Side result for the complex decoder floor programme: it closes (locally, at rank T) the realisation loophole of the #2277 E6 36 / D5 20 floors. It is not a per-call profile, frontier unit or supplier change; no kappa claim.", + "budget_minutes": 90, + "stop_rule": "Stop when (A) E6 tangent dimension and (B) the D5 family are exact and the controls pass; one bounded pivot (C) limited to the D5 family (explicit points plus a symbolic span lemma), no rank-5 E6 search.", + "outcome": "completed", + "evidence": "verify.py (stdlib, exact; ~8 s, 41 checks): E6 dim T_G V = 71 = 2v-1 (prime-rank upper bound at two primes and in a second coordinate model, matched by the explicit scaling-orbit span) => G smooth, local component = scaling orbit (local rigidity). E7 125 = 2v-1 control (E8 239 = 2v-1 behind --e8). D5: tangent 55 = 39 + 16, explicit 16-parameter non-Gram family; written proofs that D5 has no rank-4 realisation (Theorem E) and that every rank-5 realisation is edge-supported (Theorem D, construction replayed exactly on 5 instances incl. a boundary member); on every edge-supported realisation the deficient classes are the 5 axis classes, so #2277's floor 20 holds for every rank-<=5 realisation of D5 and is attained. Controls D4 44>23 (edge family only 32), D6 84 = edge family; negative controls fail as required.", + "author": "thakrarsagar", + "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) for computation design, code and text; reviewed and submitted by thakrarsagar.", + "open_questions": [ + { + "question": "Global uniqueness at rank 6 for E6: is every rank-6 realisation of E6 of the form D1 G D2 (not only those near G)?", + "why_it_matters": "It would make #2277's E6 >= 36 realisation-free at rank T, closing the non-Gram loophole for square decoders.", + "first_step": "Exact Groebner / elimination on a 6-line sub-configuration with a normalised basis, or show every rank-6 realisation has a 6-dim span on each A5-sub-configuration and propagate.", + "blocked_by": "No frame argument (alpha_perp = 4); the local certificate here says nothing about other components." + }, + { + "question": "Rank-5 realisations of E6 (dense cost <= 35 if one exists).", + "why_it_matters": "#2277 section 8.4: the only remaining way below 36 with factors in col M.", + "first_step": "By Theorems D/E the D5 sub-configuration is edge-supported of rank 5; each extra line s forces p_s|_ij proportional to the x of the non-orthogonal line on ij. Make exact the (unchecked) open-chart sketch (forces a=b and a cocycle, then extra-extra orthogonality fails) and extend it to boundary charts.", + "blocked_by": "Case analysis of degenerate (boundary) edges; not attempted here." + }, + { + "question": "D5 realisations of rank > 5.", + "why_it_matters": "The last gap (#2277 section 6 cap) in a realisation-free D5 >= 20 with factors in col M / row M.", + "first_step": "Count deficient classes in rank-6 lifts of the edge-supported family; test whether Lemma S survives one extra dimension.", + "blocked_by": "Theorem 4' no longer controls deficiency once rho > T." + }, + { + "question": "Which units with an exceptional (non-D) orthogonality pattern are first-order rigid, and does the D-type family generalise (D4 has 21 = 9 + 12 excess, larger than its edge family)?", + "why_it_matters": "Non-rigid units admit decoder geometries outside scaled-Gram floors; rigid ones reduce realisation-free floors to the Gram case locally.", + "first_step": "Run tangent_upper on P112 / P104 / E7-frame and the D4 triality directions with this verifier's functions.", + "blocked_by": "Nothing; rank-8 units are covered in part by #1212/#1292/#1389/#1399/#1425 in their own setting." + } + ] +} diff --git a/research/e6-d5-gram-realisation-rigidity/VERIFY.json b/research/e6-d5-gram-realisation-rigidity/VERIFY.json new file mode 100644 index 0000000000..e9671bba4b --- /dev/null +++ b/research/e6-d5-gram-realisation-rigidity/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "E6 tangent dim 71 = scaling orbit (two primes, two coordinate models); D5 tangent 55 with explicit 16-parameter non-Gram family (exact Fraction checks at three points); D5 deficient-class census and floor-20 term table; Theorem D normal-form construction replayed from M on 5 instances incl. a boundary member; controls D4/D6/E7; negative controls (unconstrained line, removed pair, sign error, a=-b, half family, non-realisation for Theorem D) must fail" + } + ] +} diff --git a/research/e6-d5-gram-realisation-rigidity/verify.py b/research/e6-d5-gram-realisation-rigidity/verify.py new file mode 100644 index 0000000000..9264168108 --- /dev/null +++ b/research/e6-d5-gram-realisation-rigidity/verify.py @@ -0,0 +1,671 @@ +#!/usr/bin/env python3 +"""E6 / D5 rank-T realisations: E6 local rigidity at the Gram point, D5 non-Gram +family, D5 normal form and floor 20 (#2277 open question 4). + +Standard library only, exact arithmetic (integers, Fractions, ranks modulo +primes used only in the safe direction). Run: python3 -I verify.py +Options: --skip-e7 (drop the 63-line E7 control), --e8 (add the slow E8 control). + +Prepared by thakrarsagar with substantial AI assistance from Claude +(Anthropic, Claude Opus 5.5). Apache-2.0. + +Rigour of the prime-rank steps. For an integer matrix A and a prime p, +rank_p(A mod p) <= rank_Q(A) (a nonzero minor mod p is a nonzero integer). So + * a prime rank of the tangent system bounds the rational SOLUTION dimension + from above, and + * a prime rank of an explicit family of rational tangent vectors bounds + their rational SPAN from below. +The two bounds meet, so every dimension asserted below is exact over Q (and +over every field of characteristic 0). +""" +import itertools +import sys +import time +from fractions import Fraction as F + +P1 = 1000003 +P2 = 998244353 +CHECKS = [] + + +def check(name, cond, detail=""): + CHECKS.append((name, bool(cond))) + print(("PASS " if cond else "FAIL ") + name + (" :: " + detail if detail else ""), flush=True) + if not cond: + raise SystemExit("verification failed: " + name) + + +# ---------------------------------------------------------------- units +def cartan(kind, n): + C = [[2 if i == j else 0 for j in range(n)] for i in range(n)] + + def link(a, b): + C[a][b] = C[b][a] = -1 + if kind == "D": + for i in range(n - 2): + link(i, i + 1) + link(n - 3, n - 1) + elif kind == "E": # Bourbaki numbering 1-3-4-5-6-(7-8), 2-4 (0-based here) + link(0, 2); link(2, 3); link(1, 3) + for k in range(3, n - 1): + link(k, k + 1) + else: + raise ValueError(kind) + return C + + +def positive_roots(C): + """All positive roots in simple-root coordinates (reflection closure).""" + n = len(C) + simple = [tuple(int(i == j) for i in range(n)) for j in range(n)] + seen, frontier = set(simple), list(simple) + while frontier: + nxt = [] + for c in frontier: + Cc = [sum(C[i][k] * c[k] for k in range(n)) for i in range(n)] + for i in range(n): + r = list(c); r[i] -= Cc[i]; r = tuple(r) + if r not in seen and (all(x >= 0 for x in r) or all(x <= 0 for x in r)): + seen.add(r); nxt.append(r) + frontier = nxt + return sorted(r for r in seen if all(x >= 0 for x in r)) + + +def simple_root_unit(kind, n): + """Lines = positive roots; X = simple-root coordinates, Y = X C; G = X Y^T.""" + C = cartan(kind, n) + X = [list(r) for r in positive_roots(C)] + Y = [[sum(C[i][k] * x[k] for k in range(n)) for i in range(n)] for x in X] + return X, Y + + +def dn_lines(n): + return [(i, j, s) for i, j in itertools.combinations(range(n), 2) for s in (1, -1)] + + +def dn_unit(n): + X = [] + for i, j, s in dn_lines(n): + r = [0] * n; r[i] = 1; r[j] = s; X.append(r) + return X, [list(r) for r in X] + + +def dot(u, w): + return sum(a * b for a, b in zip(u, w)) + + +def mat(X, Y): + return [[dot(x, y) for y in Y] for x in X] + + +# ---------------------------------------------------------------- linear algebra +def rank_mod(rows, ncols, p): + rows = [[x % p for x in r] for r in rows] + rows = [r for r in rows if any(r)] + rk = 0 + for c in range(ncols): + piv = next((i for i in range(rk, len(rows)) if rows[i][c]), None) + if piv is None: + continue + rows[rk], rows[piv] = rows[piv], rows[rk] + inv = pow(rows[rk][c], p - 2, p) + pr = [x * inv % p for x in rows[rk]] + rows[rk] = pr + for i in range(rk + 1, len(rows)): + f = rows[i][c] + if f: + rows[i] = [(a - f * b) % p for a, b in zip(rows[i], pr)] + rk += 1 + return rk + + +def rank_frac(rows): + rows = [[F(x) for x in r] for r in rows if any(r)] + if not rows: + return 0 + rk = 0 + for c in range(len(rows[0])): + piv = next((i for i in range(rk, len(rows)) if rows[i][c] != 0), None) + if piv is None: + continue + rows[rk], rows[piv] = rows[piv], rows[rk] + pr = rows[rk] + for i in range(rk + 1, len(rows)): + f = rows[i][c] / pr[c] + if f: + rows[i] = [a - f * b for a, b in zip(rows[i], pr)] + rk += 1 + return rk + + +# ---------------------------------------------------------------- tangent machinery +def orth_pairs(G, drop=()): + v = len(G) + return [(t, s) for t in range(v) for s in range(v) + if t != s and G[t][s] == 0 and (t, s) not in drop and (s, t) not in drop] + + +def tangent_system(X, Y, pairs): + """Rows of (dX, dY) -> (dX Y^T + X dY^T)_{ts} for the constrained pairs.""" + v, T = len(X), len(X[0]) + rows = [] + for t, s in pairs: + r = [0] * (2 * v * T) + for a in range(T): + r[t * T + a] = Y[s][a] + r[v * T + s * T + a] = X[t][a] + rows.append(r) + return rows + + +def tangent_upper(X, Y, pairs, p): + """Upper bound on dim T_M V (exact when matched by a lower bound). + + T_M(rank<=T) = {dX Y^T + X dY^T}; the kernel of (dX,dY) -> dX Y^T + X dY^T is + {(XA, -YA^T)}, of dimension T^2 when rank X = rank Y = T.""" + v, T = len(X), len(X[0]) + assert rank_mod(X, T, p) == T and rank_mod(Y, T, p) == T + rk = rank_mod(tangent_system(X, Y, pairs), 2 * v * T, p) + return 2 * v * T - rk - T * T, rk + + +def orbit_tangent_vectors(M): + """Delta1 M + M Delta2: row and column scalings, as vectors in K^{v*v}.""" + v = len(M) + vecs = [] + for t in range(v): + z = [0] * (v * v) + for s in range(v): + z[t * v + s] = M[t][s] + vecs.append(z) + for s in range(v): + z = [0] * (v * v) + for t in range(v): + z[t * v + s] = M[t][s] + vecs.append(z) + return vecs + + +def orbit_dim_combinatorial(M): + """Exact dim of {Delta1 M + M Delta2}: (Delta1 M + M Delta2)_ts = (d1_t + d2_s) M_ts, + whose kernel has one free parameter per connected component of the bipartite + support graph (rows + columns, edge where M_ts != 0); so dim = 2v - #components.""" + v = len(M) + parent = list(range(2 * v)) + + def find(a): + while parent[a] != a: + parent[a] = parent[parent[a]] + a = parent[a] + return a + for t in range(v): + for s in range(v): + if M[t][s] != 0: + parent[find(t)] = find(v + s) + return 2 * v - len({find(a) for a in range(2 * v)}) + + +def in_pattern(vec, v, pairs): + return all(vec[t * v + s] == 0 for t, s in pairs) + + +def rigidity_report(name, X, Y, primes=(P1,), drop=()): + G = mat(X, Y) + v, T = len(X), len(X[0]) + pairs = orth_pairs(G, drop) + assert all(G[t][t] != 0 for t in range(v)) + t0 = time.time() + ups = [tangent_upper(X, Y, pairs, p) for p in primes] + # orbit tangent vectors lie in T_G V: they have the form dX Y^T + X dY^T + # (dX = Delta1 X, dY = Delta2 Y) and vanish on every constrained pair. + olow = orbit_dim_combinatorial(G) + if v <= 63: # independent prime-rank recomputation (skipped for E8: 240 x 14400) + orbit = orbit_tangent_vectors(G) + assert all(in_pattern(z, v, pairs) for z in orbit) + assert rank_mod(orbit, v * v, primes[0]) == olow + return dict(name=name, v=v, T=T, pairs=len(pairs), upper=[u for u, _ in ups], + sysrank=[r for _, r in ups], orbit=olow, secs=round(time.time() - t0, 2)) + + +def alpha_perp(G): + v = len(G) + nb = [{s for s in range(v) if s != t and G[t][s] == 0} for t in range(v)] + best = 0 + + def grow(clique, cand): + nonlocal best + best = max(best, len(clique)) + for c in sorted(cand): + if c > (clique[-1] if clique else -1): + grow(clique + [c], cand & nb[c]) + grow([], set(range(v))) + return best + + +def e6_in_e8_coordinates(): + """Second, independent model of E6 (the #2277 convention): the E8 lines in + doubled integer coordinates orthogonal to two roots at 120 degrees. X = Y = + the 36 integer line vectors in Z^8 (rank 6, ambient 8).""" + E8 = [] + for i, j in itertools.combinations(range(8), 2): + for s in (2, -2): + for t in (2, -2): + r = [0] * 8; r[i] = s; r[j] = t; E8.append(r) + for signs in itertools.product((1, -1), repeat=8): + if signs.count(-1) % 2 == 0: + E8.append(list(signs)) + a = E8[0] + b = next(r for r in E8 if dot(a, r) == -4) + lines = {} + for r in E8: + if dot(a, r) == 0 and dot(b, r) == 0: + k = max(tuple(r), tuple(-x for x in r)) + lines[k] = list(k) + X = sorted(lines.values()) + return X, [list(x) for x in X] + + +def tangent_upper_ambient(X, pairs, p, T): + """Same tangent space with X = Y of rank T inside K^n (n > T), positive + definite form: the kernel of (dX, dY) -> dX X^T + X dY^T is T^2 + 2 v (n - T) + (components orthogonal to the row space are free), so + dim T_G V <= 2 v n - rank_p - T^2 - 2 v (n - T).""" + v, n = len(X), len(X[0]) + assert rank_mod(X, n, p) == T + rk = rank_mod(tangent_system(X, X, pairs), 2 * v * n, p) + return 2 * v * n - rk - T * T - 2 * v * (n - T) + + +# ---------------------------------------------------------------- D5 family +D5_LINES = dn_lines(5) +D5_EDGES = list(itertools.combinations(range(5), 2)) + + +def d5_family(par, sign_bug=False): + """x_{ij+}=e_i+a e_j, x_{ij-}=e_i-b e_j, y_{ij+}=e_i+b^{-1} e_j, y_{ij-}=e_i-a^{-1} e_j.""" + X, Y = [], [] + for i, j, s in D5_LINES: + a, b = (F(z) for z in par[(i, j)]) + x = [F(0)] * 5; y = [F(0)] * 5 + x[i] = y[i] = F(1) + if s == 1: + x[j] = a; y[j] = 1 / b + else: + x[j] = -b; y[j] = (1 / a) if sign_bug else -1 / a + X.append(x); Y.append(y) + return X, Y + + +GRAM_PAR = {e: (1, 1) for e in D5_EDGES} +# Three explicit generic rational parameter points (fixed, not searched). +D5_POINTS = { + "pt1": {e: (F(2 + k, 3), F(5, 7 + 2 * k)) for k, e in enumerate(D5_EDGES)}, + "pt2": {e: (F(-3, 4 + k), F(11 + k, 6)) for k, e in enumerate(D5_EDGES)}, + "pt3": {e: (F(7 * k + 1, 13), F(-(k + 2), 9)) for k, e in enumerate(D5_EDGES)}, +} + + +def nonscaling_witnesses(M, G): + """Pairs violating the D1 G D2 invariant M_ts M_st G_tt G_ss = G_ts^2 M_tt M_ss + (G symmetric); any violation proves M != D1 G D2.""" + v = len(M) + return sum(1 for t in range(v) for s in range(v) + if G[t][s] != 0 and M[t][s] * M[s][t] * G[t][t] * G[s][s] != G[t][s] ** 2 * M[t][t] * M[s][s]) + + +def family_tangent_vectors(n=5): + """d/da_e and d/db_e of the D_n edge family M(a,b) = X Y^T at a = b = 1 + (exact derivative; x_{ij+}=e_i+a e_j, x_{ij-}=e_i-b e_j, y_{ij+}=e_i+b^{-1} e_j, + y_{ij-}=e_i-a^{-1} e_j).""" + X, Y = dn_unit(n) + v = len(X) + lines = dn_lines(n) + idx = {l: k for k, l in enumerate(lines)} + vecs = [] + for (i, j) in itertools.combinations(range(n), 2): + tp, tm = idx[(i, j, 1)], idx[(i, j, -1)] + for which in "ab": + dX = [[0] * n for _ in range(v)]; dY = [[0] * n for _ in range(v)] + if which == "a": # x_{ij+} += da e_j ; y_{ij-} = e_i - a^{-1} e_j -> +da e_j + dX[tp][j] = 1; dY[tm][j] = 1 + else: # x_{ij-} -> -db e_j ; y_{ij+} = e_i + b^{-1} e_j -> -db e_j + dX[tm][j] = -1; dY[tp][j] = -1 + dM = [[dot(dX[t], Y[s]) + dot(X[t], dY[s]) for s in range(v)] for t in range(v)] + vecs.append([int(dM[t][s]) for t in range(v) for s in range(v)]) + return vecs + + +# ---------------------------------------------------------------- Theorem D (global D5 normal form) +def kernel_frac(cols): + """Basis of {c : sum_k c_k cols[k] = 0} (exact).""" + n, k = len(cols[0]), len(cols) + rows = [[F(cols[j][i]) for j in range(k)] for i in range(n)] + piv, r = [], 0 + for c in range(k): + pr = next((i for i in range(r, n) if rows[i][c] != 0), None) + if pr is None: + continue + rows[r], rows[pr] = rows[pr], rows[r] + inv = 1 / rows[r][c] + rows[r] = [x * inv for x in rows[r]] + for i in range(n): + if i != r and rows[i][c] != 0: + f = rows[i][c] + rows[i] = [a - f * b for a, b in zip(rows[i], rows[r])] + piv.append(c); r += 1 + free = [c for c in range(k) if c not in piv] + basis = [] + for fc in free: + z = [F(0)] * k; z[fc] = F(1) + for i, pc in enumerate(piv): + z[pc] = -rows[i][fc] + basis.append(z) + return basis + + +def inverse_frac(A): + n = len(A) + aug = [[F(x) for x in row] + [F(int(i == j)) for j in range(n)] for i, row in enumerate(A)] + for c in range(n): + pr = next(i for i in range(c, n) if aug[i][c] != 0) + aug[c], aug[pr] = aug[pr], aug[c] + inv = 1 / aug[c][c] + aug[c] = [x * inv for x in aug[c]] + for i in range(n): + if i != c and aug[i][c] != 0: + f = aug[i][c] + aug[i] = [a - f * b for a, b in zip(aug[i], aug[c])] + return [row[n:] for row in aug] + + +def d5_normal_form(M, check_pattern=True): + """Run the construction of Theorem D on a rank-5 realisation M of D5, + starting from M alone; assert every intermediate claim; return the + edge-supported factors (x_t, y_t) in dual coordinates.""" + v, lines = 20, D5_LINES + G = mat(*dn_unit(5)) + if check_pattern: + assert all(M[t][s] == 0 for t, s in orth_pairs(G)) and all(M[t][t] != 0 for t in range(v)) + assert rank_frac(M) == 5 + # rank factorisation M = P Q^T from pivot rows R / columns C of M + C, R = [], [] + for c in range(v): + if rank_frac([[M[t][s] for s in C + [c]] for t in range(v)]) > len(C): + C.append(c) + for t in range(v): + if rank_frac([M[r] for r in R + [t]]) > len(R): + R.append(t) + Pm = [[M[t][c] for c in C] for t in range(v)] + Ainv = inverse_frac([[M[r][c] for c in C] for r in R]) + Qm = [[sum(Ainv[i][k] * M[R[k]][s] for k in range(5)) for i in range(5)] for s in range(v)] + assert all(dot(Pm[t], Qm[s]) == M[t][s] for t in range(v) for s in range(v)) + idx = {l: k for k, l in enumerate(lines)} + + def side(Z): + W = {e: [Z[idx[(e[0], e[1], 1)]], Z[idx[(e[0], e[1], -1)]]] for e in D5_EDGES} + assert all(rank_frac(W[e]) == 2 for e in D5_EDGES) # dim W_e = 2 + for tri in itertools.combinations(range(5), 3): # dim W_ijk = 3 + assert rank_frac([z for e in itertools.combinations(tri, 2) for z in W[e]]) == 3 + f = [] + for a in range(5): + at = [tuple(sorted((a, b))) for b in range(5) if b != a] + for e1, e2 in itertools.combinations(at, 2): # pairwise meet in a line + assert rank_frac(W[e1] + W[e2]) == 3 + ker = kernel_frac(W[at[0]] + [[-x for x in z] for z in W[at[1]]]) + assert len(ker) == 1 + fa = [ker[0][0] * W[at[0]][0][i] + ker[0][1] * W[at[0]][1][i] for i in range(5)] + assert all(rank_frac(W[e] + [fa]) == 2 for e in at) # common line L_a + f.append(fa) + assert rank_frac(f) == 5 # L_0..L_4 basis + return f + fP, gQ = side(Pm), side(Qm) + pair = [[dot(fP[a], gQ[c]) for c in range(5)] for a in range(5)] + assert all((pair[a][c] == 0) == (a != c) for a in range(5) for c in range(5)) # dual up to scale + # coordinates: p_t = sum_a x_t[a] f_a, q_t = sum_a y_t[a] g_a / pair[a][a] + Sinv = inverse_frac([[fP[a][i] for a in range(5)] for i in range(5)]) + Tinv = inverse_frac([[gQ[a][i] / pair[a][a] for a in range(5)] for i in range(5)]) + X = [[sum(Sinv[a][i] * Pm[t][i] for i in range(5)) for a in range(5)] for t in range(v)] + Y = [[sum(Tinv[a][i] * Qm[t][i] for i in range(5)) for a in range(5)] for t in range(v)] + for t, (i, j, s) in enumerate(lines): # edge-supported + assert all(X[t][a] == 0 and Y[t][a] == 0 for a in range(5) if a not in (i, j)) + assert all(dot(X[t], Y[u]) == M[t][u] for t in range(v) for u in range(v)) + return X, Y + + +def scaled(M, d1, d2): + return [[d1[t] * M[t][s] * d2[s] for s in range(len(M))] for t in range(len(M))] + + +def boundary_member(): + """A rank-5 realisation outside the open family chart: x_{01+} = e_0 (a_01 = 0).""" + X, Y = d5_family(D5_POINTS["pt1"]) + idx = {l: k for k, l in enumerate(D5_LINES)} + tp, tm = idx[(0, 1, 1)], idx[(0, 1, -1)] + X[tp] = [F(1), F(0), F(0), F(0), F(0)]; X[tm] = [F(1), F(-1), F(0), F(0), F(0)] + Y[tp] = [F(1), F(1), F(0), F(0), F(0)]; Y[tm] = [F(0), F(1), F(0), F(0), F(0)] + return X, Y + + +# ---------------------------------------------------------------- F2 dense pairing +def dense_classes(G): + v = len(G) + cols = [sum((1 if (t == s or G[t][s] == 0) else 0) << t for t in range(v)) for s in range(v)] + basis = [] + for c in cols: + for b in basis: + c = min(c, c ^ b) + if c: + basis.append(c) + span = {0} + for b in basis: + span |= {x ^ b for x in span} + return len(basis), sorted(w for w in span if w), cols + + +def f2_rank(rowmasks): + basis = [] + for r in rowmasks: + for b in basis: + r = min(r, r ^ b) + if r: + basis.append(r) + return len(basis) + + +def bd_block_rank(G, R, A): + v = len(G) + Aset = set(A) + rows = [] + for t in R: + m = 0 + for s in Aset: + if t == s or G[t][s] == 0: + m |= 1 << s + rows.append(m) + return f2_rank(rows) + + +# ---------------------------------------------------------------- main +def main(argv): + t_start = time.time() + print("== Part A: E6 first-order rigidity at the Gram point ==") + X6, Y6 = simple_root_unit("E", 6) + G6 = mat(X6, Y6) + check("E6 unit: 36 lines, T=6, Gram diagonal 2", + len(X6) == 36 and all(G6[t][t] == 2 for t in range(36))) + deg = {sum(1 for s in range(36) if s != t and G6[t][s] == 0) for t in range(36)} + ap = alpha_perp(G6) + check("E6 orthogonality: 15 orthogonal lines each, alpha_perp=4 (no 6-frame)", deg == {15} and ap == 4, + "degrees %s alpha_perp %d" % (deg, ap)) + r = rigidity_report("E6", X6, Y6, primes=(P1, P2)) + check("E6 tangent upper bound (primes %d, %d) = 71" % (P1, P2), r["upper"] == [71, 71], + "system rank %s over %d ordered orthogonal pairs, 432 unknowns" % (r["sysrank"], r["pairs"])) + check("E6 scaling-orbit tangent rank >= 71 = 2v-1 (and <= 2v-1: rows-sum = cols-sum)", r["orbit"] == 71) + Xe, _ = e6_in_e8_coordinates() + Ge = mat(Xe, Xe) + pe = orth_pairs(Ge) + up_e = tangent_upper_ambient(Xe, pe, P1, 6) + check("E6 cross-check in E8 doubled coordinates (36 lines in Z^8, rank 6): tangent upper bound 71", + len(Xe) == 36 and len(pe) == 540 and up_e == 71 and rank_mod(orbit_tangent_vectors(Ge), 36 * 36, P1) == 71) + print(" => dim T_G V(E6, rank<=6) = 71 = dim of the scaling orbit {D1 G D2}: G is a smooth point," + " locally V = scaling orbit (local rigidity, not global uniqueness)") + + print("== Part B: D5 Gram point is not rigid; explicit 16-parameter non-Gram family ==") + X5, Y5 = dn_unit(5) + G5 = mat(X5, Y5) + v5 = 20 + check("D5 alpha_perp=4 (no 5-frame)", alpha_perp(G5) == 4) + r5 = rigidity_report("D5", X5, Y5, primes=(P1, P2)) + check("D5 tangent upper bound = 55 (two primes)", r5["upper"] == [55, 55], "system rank %s" % r5["sysrank"]) + check("D5 scaling-orbit tangent = 39", r5["orbit"] == 39) + Xg, Yg = d5_family(GRAM_PAR) + check("D5 family at a=b=1 is the Gram matrix", mat(Xg, Yg) == [[F(x) for x in row] for row in G5]) + pairs5 = orth_pairs(G5) + fam = family_tangent_vectors() + check("D5 family tangent directions satisfy the pattern zeros", all(in_pattern(z, v5, pairs5) for z in fam)) + orbit5 = orbit_tangent_vectors(G5) + low = rank_mod(fam + orbit5, v5 * v5, P1) + check("D5 family directions + scaling orbit span 55 (prime lower bound) = tangent upper bound", low == 55) + check("D5 family directions modulo the orbit: 55 - 39 = 16 = 20 parameters - 4 (coordinate torus)", + low - r5["orbit"] == 16 and len(fam) == 20) + for name, par in D5_POINTS.items(): + X, Y = d5_family(par) + M = mat(X, Y) + zeros = all(M[t][s] == 0 for t, s in pairs5) + diag = all(M[t][t] != 0 for t in range(v5)) + rk = (rank_frac(X), rank_frac(Y), rank_frac(M)) + wit = nonscaling_witnesses(M, G5) + check("D5 family %s: pattern zeros, nonzero diagonal, rank 5, %d D1 G D2 violations" % (name, wit), + zeros and diag and rk == (5, 5, 5) and wit > 0) + check("D5 control: Gram parameters give 0 D1 G D2 violations", + nonscaling_witnesses(mat(Xg, Yg), G5) == 0) + + print("== Part C: the D5 dense-pairing floor 20 on the whole family ==") + h, classes, cols = dense_classes(G5) + check("D5 dense pairing: h=5, 31 classes", h == 5 and len(classes) == 31) + idx = {l: k for k, l in enumerate(D5_LINES)} + edge_classes = [] + for w in classes: + O = {t for t in range(v5) if w >> t & 1} + E = {(i, j) for (i, j, s) in (D5_LINES[t] for t in O)} + closed = all(idx[(i, j, 1)] in O and idx[(i, j, -1)] in O for (i, j) in E) + edge_classes.append((w, E, closed)) + check("every class is a union of +/- edge pairs (columns of e_i+e_j and e_i-e_j in B_d coincide)", + all(c for _, _, c in edge_classes)) + missing = [(w, E) for w, E, _ in edge_classes if len({i for e in E for i in e}) < 5] + check("exactly 5 classes miss a vertex; each is the axis class {lines avoiding a} (12 lines)", + len(missing) == 5 and all(len(E) == 6 for _, E in missing)) + # Lemma S (proved in README): span{x_t : t in O} = span{e_i : i covered by E_O} + # because x_{ij+}, x_{ij-} span iff a+b != 0 iff M_tt != 0. + for name, par in list(D5_POINTS.items()) + [("gram", GRAM_PAR)]: + X, Y = d5_family(par) + dx = [w for w in classes if rank_frac([X[t] for t in range(v5) if w >> t & 1]) < 5] + dy = [w for w in classes if rank_frac([Y[t] for t in range(v5) if w >> t & 1]) < 5] + ok_lemma = all(rank_frac([X[t] for t in range(v5) if w >> t & 1]) == len({i for e in E for i in e}) + for w, E, _ in edge_classes) + check("Lemma S exact at %s; deficient classes = the 5 axis classes on both sides" % name, + ok_lemma and sorted(dx) == sorted(dy) == sorted(w for w, _ in missing)) + # term-rank table (Lemma 5.1 of #2277: depends only on Def(R), Def(A)); R(e_a) = lines through a + through = {a: [t for t, (i, j, s) in enumerate(D5_LINES) if a in (i, j)] for a in range(5)} + full = list(range(v5)) + table = { + "matched": {bd_block_rank(G5, through[a], through[a]) for a in range(5)}, + "unmatched": {bd_block_rank(G5, through[a], through[b]) for a in range(5) for b in range(5) if a != b}, + "one-deficient": {bd_block_rank(G5, through[a], full) for a in range(5)} | + {bd_block_rank(G5, full, through[a]) for a in range(5)}, + "none": {bd_block_rank(G5, full, full)}, + } + check("D5 term ranks: matched 4, unmatched 3, one deficient 4, none 5", + table == {"matched": {4}, "unmatched": {3}, "one-deficient": {4}, "none": {5}}, str(table)) + trip = [c for c in itertools.permutations([(a, b) for a in range(5) for b in range(5) if a != b], 3) + if all(c[i][1] == c[j][0] for i in range(3) for j in range(3) if i != j)] + check("#2277 c1.d5core re-derived: no three pairs (a_i!=b_i) with b_i = a_j for all i != j", not trip) + check("coordinate decoder p_a = X e_a, q_a = Y e_a attains 5*4 = 20 in every family member", + 5 * min(table["matched"]) == 20) + + print("== Part D: every rank-5 realisation of D5 is edge-supported (Theorem D, constructive replay) ==") + d1 = [F(k + 2, 3) * (-1) ** k for k in range(v5)] + d2 = [F(5, k + 1) for k in range(v5)] + inst = [("pt%d scaled" % (k + 1), scaled(mat(*d5_family(par)), d1, d2)) for k, par in enumerate(D5_POINTS.values())] + inst.append(("Gram scaled", scaled([[F(x) for x in row] for row in G5], d1, d2))) + Xbd, Ybd = boundary_member() + inst.append(("boundary member (x_01+ = e_0)", mat(Xbd, Ybd))) + for name, M in inst: + Xn, Yn = d5_normal_form(M) + dx = [w for w in classes if rank_frac([Xn[t] for t in range(v5) if w >> t & 1]) < 5] + dy = [w for w in classes if rank_frac([Yn[t] for t in range(v5) if w >> t & 1]) < 5] + Rx = {a: [t for t in range(v5) if Xn[t][a] != 0] for a in range(5)} + Ay = {a: [t for t in range(v5) if Yn[t][a] != 0] for a in range(5)} + tab = ({bd_block_rank(G5, Rx[a], Ay[a]) for a in range(5)}, + {bd_block_rank(G5, Rx[a], Ay[b]) for a in range(5) for b in range(5) if a != b}) + check("Theorem D construction replayed on %s: W_e, triangles, L_a, dual pairing, edge-supported; " + "deficient classes = axis classes; actual R(e_a), A(e_b) ranks matched 4 / unmatched 3" % name, + sorted(dx) == sorted(dy) == sorted(w for w, _ in missing) and tab == ({4}, {3}), str(tab)) + + X4, Y4 = dn_unit(4) + r4 = rigidity_report("D4", X4, Y4) + f4 = rank_mod(family_tangent_vectors(4) + orbit_tangent_vectors(mat(X4, Y4)), 144, P1) + check("D4 control (has a 4-frame): tangent 44 > orbit 23 (not rigid); edge family covers only 23+9=32", + r4["upper"] == [44] and r4["orbit"] == 23 and f4 == 32, "family+orbit span %d" % f4) + X6d, Y6d = dn_unit(6) + r6 = rigidity_report("D6", X6d, Y6d) + f6 = rank_mod(family_tangent_vectors(6) + orbit_tangent_vectors(mat(X6d, Y6d)), 900, P1) + check("D6 control: tangent 84 = 59 + 25, all realised by the edge family (30 params - 5 torus)", + r6["upper"] == [84] and r6["orbit"] == 59 and f6 == 84, "family+orbit span %d" % f6) + if "--skip-e7" not in argv: + X7, Y7 = simple_root_unit("E", 7) + r7 = rigidity_report("E7", X7, Y7) + check("E7 control: tangent 125 = 2v-1 (rigid at first order)", r7["upper"] == [125] and r7["orbit"] == 125, + "%.1fs" % r7["secs"]) + if "--e8" in argv: + X8, Y8 = simple_root_unit("E", 8) + r8 = rigidity_report("E8", X8, Y8) + check("E8 control: tangent 239 = 2v-1", r8["upper"] == [239] and r8["orbit"] == 239) + + print("== Negative controls (each must FAIL the corresponding acceptance test) ==") + # Removing a single orthogonal pair (or up to 10 of the 15 at line 0, in this + # order) leaves E6 first-order rigid -- the zero pattern is redundant at first + # order -- so the perturbation that must break rigidity removes all 15 + # orthogonality constraints of line 0 (row and column). + one = rigidity_report("E6-minus-one-pair", X6, Y6, drop={orth_pairs(G6)[0]}) + check("E6 robustness: one orthogonal pair removed, still 71", one["upper"] == [71]) + drop0 = {(0, s) for s in range(36) if s != 0 and G6[0][s] == 0} + rn = rigidity_report("E6-line0-unconstrained", X6, Y6, drop=drop0) + neg1 = rn["upper"][0] == rn["orbit"] + check("NEG E6 pattern with the 15 orthogonality constraints of line 0 removed is NOT rigid (81 > 71)", + not neg1 and rn["upper"] == [81], "tangent upper %d vs orbit %d" % (rn["upper"][0], rn["orbit"])) + rd = rigidity_report("D5-minus-one-pair", X5, Y5, drop={orth_pairs(G5)[0]}) + check("NEG D5 pattern with one orthogonal pair removed: tangent 57 != 55 (dimension is pattern-sensitive)", + rd["upper"] == [57]) + Xb, Yb = d5_family(D5_POINTS["pt1"], sign_bug=True) + Mb = mat(Xb, Yb) + check("NEG D5 family with sign error in y_{ij-} violates the pattern zeros", + not all(Mb[t][s] == 0 for t, s in pairs5)) + bad = {e: (F(2), F(-2)) if e == (0, 1) else (F(1), F(1)) for e in D5_EDGES} + Xc, Yc = d5_family(bad) + Mc = mat(Xc, Yc) + extra = [w for w in classes if rank_frac([Xc[t] for t in range(v5) if w >> t & 1]) < 5] + check("NEG inadmissible a=-b on edge 01: zero diagonal entry and extra deficient classes", + any(Mc[t][t] == 0 for t in range(v5)) and len(extra) > 5, "%d deficient classes" % len(extra)) + a_only = rank_mod(fam[0::2] + orbit5, v5 * v5, P1) + check("NEG half family (b frozen, 10 a-directions) + orbit spans < 55: the lower bound is not automatic", + a_only < 55, "span %d" % a_only) + + Mbad = mat(*d5_family(D5_POINTS["pt2"])) + t1, s1 = pairs5[0] + Xq, Yq = d5_family(D5_POINTS["pt2"]) + Yq[s1] = [y + (F(1) if i == 2 else 0) for i, y in enumerate(Yq[s1])] # breaks M_{t1 s1} = 0 only + Mbad = mat(Xq, Yq) + broke = sum(1 for t, s in pairs5 if Mbad[t][s] != 0) + try: + d5_normal_form(Mbad, check_pattern=False) + failed = False + except AssertionError: + failed = True + check("NEG Theorem D construction on a rank-5 non-realisation (%d orthogonal zeros broken) fails" % broke, + failed and broke > 0) + print("ALL %d CHECKS PASSED in %.1fs" % (len(CHECKS), time.time() - t_start)) + + +if __name__ == "__main__": + main(sys.argv[1:]) From ffae2c23a69d594c7b71673f6a6a36bb9f211937 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Thu, 15 Oct 2026 16:13:35 +0530 Subject: [PATCH 2/3] e6-d5 package: D5 tangent consistency at family/boundary points; restore controls header Adds an exact tangent upper bound (55) at the three family points and the boundary member (rational entries reduced mod p, safe direction), restores the Controls section header, and records the --e8 run (ALL 43 CHECKS PASSED). Co-Authored-By: Claude Opus 5.5 --- .../e6-d5-gram-realisation-rigidity/README.md | 10 ++++++---- .../e6-d5-gram-realisation-rigidity/verify.py | 16 ++++++++++++++++ 2 files changed, 22 insertions(+), 4 deletions(-) diff --git a/research/e6-d5-gram-realisation-rigidity/README.md b/research/e6-d5-gram-realisation-rigidity/README.md index c32aa37d00..7b7e827118 100644 --- a/research/e6-d5-gram-realisation-rigidity/README.md +++ b/research/e6-d5-gram-realisation-rigidity/README.md @@ -29,7 +29,7 @@ realisation-free Theorem 4′ / Lemma 5.2 certificate gives nothing for them. | **E6** | 36 | 6 | **71** | 71 | smooth point; local component = scaling orbit (**locally rigid**) | | **D5** | 20 | 5 | **55** | 39 | not rigid: every rank-5 realisation is edge-supported (Theorem D), i.e. a scaling of an explicit **16-parameter non-Gram family** or a boundary point of it; no rank-4 realisation (Theorem E); floor 20 everywhere | | E7 (control) | 63 | 7 | 125 | 125 | locally rigid | -| E8 (control, `--e8`, ~145 s) | 120 | 8 | 239 | 239 | locally rigid | +| E8 (control, `--e8`, ~140 s) | 120 | 8 | 239 | 239 | locally rigid | | D6 (control) | 30 | 6 | 84 | 59 | smooth; edge family realises all 25 extra directions | | D4 (control) | 12 | 4 | 44 | 23 | edge family gives only 9 of the 21 extra directions (rest not integrated here) | @@ -160,7 +160,9 @@ triangle spans, the pairwise meets, `L_a`, the dual pairing and the edge-supported normal form. The inputs are the three family points and the Gram matrix (each with fixed non-trivial `D₁`, `D₂`) and one boundary member. The negative control is a rank-5 matrix that breaks 4 orthogonal zeros, and the -construction fails on it. +construction fails on it. As a consistency check, the tangent upper bound is +also 55 at the three family points and at the boundary member, so these are +smooth points of a single 55-dimensional component. **Corollary (#2277 OQ4, D5 half).** Theorem C applies verbatim to every edge-supported realisation, including boundary members. Lemma S needs only @@ -182,8 +184,8 @@ unconstrained. ```sh python3 -I -B research/e6-d5-gram-realisation-rigidity/verify.py # ~8 s, stdlib -# expected last line: ALL 41 CHECKS PASSED in s -python3 -I -B research/e6-d5-gram-realisation-rigidity/verify.py --e8 # adds E8 239 = 2v-1: ALL 42 CHECKS PASSED (~145 s) +# expected last line: ALL 42 CHECKS PASSED in s +python3 -I -B research/e6-d5-gram-realisation-rigidity/verify.py --e8 # adds E8 239 = 2v-1: ALL 43 CHECKS PASSED (~140 s) python3 scripts/research_package.py --package research/e6-d5-gram-realisation-rigidity --check-only ``` diff --git a/research/e6-d5-gram-realisation-rigidity/verify.py b/research/e6-d5-gram-realisation-rigidity/verify.py index 9264168108..a8881fd44a 100644 --- a/research/e6-d5-gram-realisation-rigidity/verify.py +++ b/research/e6-d5-gram-realisation-rigidity/verify.py @@ -432,6 +432,17 @@ def side(Z): return X, Y +def modp(x, p=P1): + x = F(x) + return x.numerator * pow(x.denominator, p - 2, p) % p + + +def tangent_upper_rational(X, Y, pairs, p=P1): + """tangent_upper for rational X, Y (denominators prime to p: reduction + Z_(p) -> F_p is a ring map, so rank_p <= rank_Q still holds).""" + return tangent_upper([[modp(a, p) for a in r] for r in X], [[modp(a, p) for a in r] for r in Y], pairs, p)[0] + + def scaled(M, d1, d2): return [[d1[t] * M[t][s] * d2[s] for s in range(len(M))] for t in range(len(M))] @@ -601,7 +612,12 @@ def main(argv): check("Theorem D construction replayed on %s: W_e, triangles, L_a, dual pairing, edge-supported; " "deficient classes = axis classes; actual R(e_a), A(e_b) ranks matched 4 / unmatched 3" % name, sorted(dx) == sorted(dy) == sorted(w for w, _ in missing) and tab == ({4}, {3}), str(tab)) + ups = [tangent_upper_rational(*d5_family(par), pairs5) for par in D5_POINTS.values()] + ups.append(tangent_upper_rational(Xbd, Ybd, pairs5)) + check("D5 tangent upper bound 55 also at pt1-3 and at the boundary member (consistent with Theorem D: " + "smooth points of one 55-dimensional component)", ups == [55, 55, 55, 55], str(ups)) + print("== Controls (dimension changes / non-rigid units) ==") X4, Y4 = dn_unit(4) r4 = rigidity_report("D4", X4, Y4) f4 = rank_mod(family_tangent_vectors(4) + orbit_tangent_vectors(mat(X4, Y4)), 144, P1) From d7fa28209914f97f4f738b2eb26b19d0f3656024 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Thu, 15 Oct 2026 16:26:52 +0530 Subject: [PATCH 3/3] e6-d5 package: address review (exact negative controls, -O guard, scope and credit) - D4 tangent 44, D4 family span 32, D5-minus-one-pair 57 and half-family 49 now certified by exact Fraction rank; E6 line-0 negative control certified exactly (81) by an explicit lower-bound span. - verify.py refuses to run under python -O; modp rejects p | denominator. - README: partial-removal robustness relabelled as uncertified; #2277 section 5 T-frame preamble clarified; algebraic-cost scope; E8 subsumed by #1212; #2277 marked draft; author names for method predecessors; tested interpreter. - TASK.json: 42 checks (43 with --e8). Co-Authored-By: Claude Opus 5.5 --- .../e6-d5-gram-realisation-rigidity/README.md | 72 +++++++++++++------ .../e6-d5-gram-realisation-rigidity/TASK.json | 2 +- .../e6-d5-gram-realisation-rigidity/verify.py | 58 +++++++++++---- 3 files changed, 94 insertions(+), 38 deletions(-) diff --git a/research/e6-d5-gram-realisation-rigidity/README.md b/research/e6-d5-gram-realisation-rigidity/README.md index 7b7e827118..136fefb85c 100644 --- a/research/e6-d5-gram-realisation-rigidity/README.md +++ b/research/e6-d5-gram-realisation-rigidity/README.md @@ -20,7 +20,17 @@ realisations of rank `≤ T` (`T = dim span r_t`) and `G` the Gram matrix. The and has dimension `2v − 1`. #2277 proves E6 `≥ 36` and D5 `≥ 20` (dense pairing, factors in `col M` / `row M`, any number of terms) for the scaled-Gram realisations `D₁ G D₂` only; E6 and D5 have no `T`-frame (`α_⊥ = 4`), so its -realisation-free Theorem 4′ / Lemma 5.2 certificate gives nothing for them. +realisation-free Lemma 5.2 certificate gives nothing for them. #2277 §5 opens +with "Fix a unit with a T-frame", but the proofs of the Theorem 4′ inequality and +of the Lemma 5.1 rank invariance use only an F₂ rank factorisation of `B_d` and +the term count from `N = Σ x_j y_jᵀ`; only Lemma 5.2 uses the frame. Theorem C +below uses only Theorem 4′, Lemma 5.1, Lemma OC and the Theorem 7.4 count, so it +applies to D5 despite the missing frame. + +"Cost" and "floor 20" throughout mean #2277's algebraic decoder cost +`Σ_j rank_F₂ B_d[R_j, A_j]` only. As in #2277's scope, this excludes copy, +hosting, restoration and every supplier or assembly cost, so the floor is not a +complete multiplication cost. ## Results @@ -29,10 +39,17 @@ realisation-free Theorem 4′ / Lemma 5.2 certificate gives nothing for them. | **E6** | 36 | 6 | **71** | 71 | smooth point; local component = scaling orbit (**locally rigid**) | | **D5** | 20 | 5 | **55** | 39 | not rigid: every rank-5 realisation is edge-supported (Theorem D), i.e. a scaling of an explicit **16-parameter non-Gram family** or a boundary point of it; no rank-4 realisation (Theorem E); floor 20 everywhere | | E7 (control) | 63 | 7 | 125 | 125 | locally rigid | -| E8 (control, `--e8`, ~140 s) | 120 | 8 | 239 | 239 | locally rigid | +| E8 (control, `--e8`, ~140 s) | 120 | 8 | 239 | 239 | locally rigid (not new: subsumed by #1212 Theorem 1, global uniqueness up to the torus on P120 = E8) | | D6 (control) | 30 | 6 | 84 | 59 | smooth; edge family realises all 25 extra directions | | D4 (control) | 12 | 4 | 44 | 23 | edge family gives only 9 of the 21 extra directions (rest not integrated here) | +Every entry of the `dim T_G V_U` column is certified exactly: a prime-rank upper +bound matched by an explicit lower-bound span (E6, D5, E7, E8, D6), or an exact +`Fraction` rank (D4). The D4 family-plus-orbit span 32 is also an exact +`Fraction` rank. The new results are E6 (local rigidity), D5 (Theorems B–E) and +the D6/D4 controls; E7 is a first-order control, and E8 only re-confirms +#1212. + **Theorem A (E6 local rigidity) — PROVEN from CHECKED data.** The Zariski tangent space of `V_E6` at `G` has dimension 71. Hence `G` is a nonsingular point of `V_E6`, the only irreducible component through `G` is the closure of @@ -174,11 +191,13 @@ has dense-pairing cost `≥ 20`** for decoders with `col P ⊆ col M` and `col Q ⊆ row M`, which includes all square decoders. The bound is attained. Realisations of rank `> 5` remain outside, as in #2277 §6. -**Robustness observation (CHECKED).** The E6 count is insensitive to small -pattern deletions. Removing one orthogonal pair, or up to 10 of the 15 -orthogonality constraints of one line (in the verifier's order), leaves -dimension 71. Each further removal adds 2, reaching 81 when line 0 is -unconstrained. +**Robustness observation.** CHECKED: removing one orthogonal pair from the E6 +pattern leaves the tangent dimension at exactly 71, and removing all 15 +orthogonality constraints of line 0 gives exactly 81. NOT CERTIFIED (scratch +observation only, not replayed by verify.py): for partial removals at line 0, +the dimension stays 71 for the first 10 removals in the verifier's pair order +and then rises by 2 per removal. The threshold depends on the removal order; +an independent reviewer found 73 already at 10 removals in another ordering. ## Reproduce @@ -191,14 +210,16 @@ python3 scripts/research_package.py --package research/e6-d5-gram-realisation-ri **Negative controls (each must fail its acceptance test; verify.py asserts that they do):** -- E6 with the 15 orthogonality constraints of line 0 removed is not rigid - (81 > 71). -- D5 with one orthogonal pair removed has tangent 57 ≠ 55, which shows the - count depends on the pattern. +- E6 with the 15 orthogonality constraints of line 0 removed is not rigid: + its tangent is exactly 81 > 71. The prime upper bound 81 is matched by the + orbit plus the free first-order moves of `x_0` and `y_0`. +- D5 with one orthogonal pair removed has tangent exactly 57 ≠ 55 (exact + `Fraction` rank), which shows the count depends on the pattern. - A sign error in `y_{ij-}` breaks the pattern zeros. - The inadmissible `a = −b` on one edge gives a zero diagonal and 6 deficient classes, so Lemma S fails. -- Half the family (`b` frozen) together with the orbit spans only 49 < 55. +- Half the family (`b` frozen) together with the orbit spans exactly 49 < 55 + (exact `Fraction` rank). - The Theorem D construction applied to a rank-5 non-realisation (4 orthogonal zeros broken) fails. - Positive control: the Gram parameters give 0 scaling violations. @@ -216,12 +237,16 @@ they do):** hypotheses are inherited from #2277 Theorem 4′. Arbitrary `B`, factors outside `col M`, and realisations of rank `> T` are not covered. - **Inherited:** #2277 Lemma 5.1, Theorem 4′, Lemma OC and the Theorem 7.4 - argument. These are PROVEN in the open PR #2277 (head `ca7f9992`) and are not - re-proved here; only their hypotheses for the D5 family are checked. -- Prime ranks are used only in the safe direction (`rank_p ≤ rank_Q`). All - other acceptance checks use exact integer, `Fraction` or `F₂` arithmetic. - This is a finite exact certificate combined with written proofs. It is not - a formalisation. + argument. These are proven in the draft, unmerged PR #2277 (head + `ca7f9992`) and are not re-proved here; only their hypotheses for the D5 + family are checked. Theorem C and the Corollary are conditional on them. +- Prime ranks are used only in the safe direction (`rank_p ≤ rank_Q`), and + each one is matched by a bound in the other direction. All other acceptance + checks, including the negative controls, use exact integer, `Fraction` or `F₂` + arithmetic. Proof-relevant intermediate steps use `assert`, so verify.py + refuses to run under `python -O`. This is a finite exact certificate combined + with written proofs. It is not a formalisation. +- VERIFY.json declares the generic replay interpreter (3.12, required by the package tooling), but every run recorded here used CPython 3.14 (stdlib only); 3.12 itself was not tested. - D5 is not a frontier unit. Nothing here changes a supplier, a call profile or κ. @@ -256,13 +281,16 @@ The structured list is in [TASK.json](TASK.json): Provenance pins are in [SOURCES.json](SOURCES.json). The package has no live input files: every unit is rebuilt from Cartan matrices or coordinates. - Definitions, Theorem 4′, Lemma 5.1, Lemma 7.1, Theorem 7.4 and OQ4 are from - **#2277** and **#2228** (DreamingOfClouds), cited at #2277 head + **#2277** (draft) and **#2228** (DreamingOfClouds), cited at #2277 head `ca7f99921f03398d303bba90245d3ee2e38e95c3`. - **#2338** (Theorem R) concerns F₂ pairing-table rigidity, which is a different object. -- The tangent-versus-torus rigidity method on rank-8 units comes from **#1212, - #1292, #1389, #1399, #1425**, with the audit in **#1367**. The model comes - from **#2125** and **#1590**. +- The tangent-versus-torus rigidity method on rank-8 units comes from **#1212** + (burntout76; its Theorem 1 already proves global uniqueness up to the torus + for rank-≤8 P120 = E8 and P112 realisations), **#1292** (navinor), and + **#1389, #1399, #1425** (JosieElliston), with the audit in **#1367** + (1337isnot1337). The model comes from **#2125** and **#1590** + (DreamingOfClouds). - The E6 screens are **#2137, #2232, #2240, #2247** (1337isnot1337) and **#2272** (navinor). EdDiboi contributed the local E6 seven-term audit (#1166). The first-order jet method follows the earlier loop PR **#2351**. diff --git a/research/e6-d5-gram-realisation-rigidity/TASK.json b/research/e6-d5-gram-realisation-rigidity/TASK.json index 95a9f95f53..dcb17b73fd 100644 --- a/research/e6-d5-gram-realisation-rigidity/TASK.json +++ b/research/e6-d5-gram-realisation-rigidity/TASK.json @@ -56,7 +56,7 @@ "budget_minutes": 90, "stop_rule": "Stop when (A) E6 tangent dimension and (B) the D5 family are exact and the controls pass; one bounded pivot (C) limited to the D5 family (explicit points plus a symbolic span lemma), no rank-5 E6 search.", "outcome": "completed", - "evidence": "verify.py (stdlib, exact; ~8 s, 41 checks): E6 dim T_G V = 71 = 2v-1 (prime-rank upper bound at two primes and in a second coordinate model, matched by the explicit scaling-orbit span) => G smooth, local component = scaling orbit (local rigidity). E7 125 = 2v-1 control (E8 239 = 2v-1 behind --e8). D5: tangent 55 = 39 + 16, explicit 16-parameter non-Gram family; written proofs that D5 has no rank-4 realisation (Theorem E) and that every rank-5 realisation is edge-supported (Theorem D, construction replayed exactly on 5 instances incl. a boundary member); on every edge-supported realisation the deficient classes are the 5 axis classes, so #2277's floor 20 holds for every rank-<=5 realisation of D5 and is attained. Controls D4 44>23 (edge family only 32), D6 84 = edge family; negative controls fail as required.", + "evidence": "verify.py (stdlib, exact; ~8 s, 42 checks; 43 with --e8): E6 dim T_G V = 71 = 2v-1 (prime-rank upper bound at two primes and in a second coordinate model, matched by the explicit scaling-orbit span) => G smooth, local component = scaling orbit (local rigidity). E7 125 = 2v-1 control (E8 239 = 2v-1 behind --e8). D5: tangent 55 = 39 + 16, explicit 16-parameter non-Gram family; written proofs that D5 has no rank-4 realisation (Theorem E) and that every rank-5 realisation is edge-supported (Theorem D, construction replayed exactly on 5 instances incl. a boundary member); on every edge-supported realisation the deficient classes are the 5 axis classes, so #2277's floor 20 holds for every rank-<=5 realisation of D5 and is attained. Controls D4 44>23 exact (edge family only 32, exact), D6 84 = edge family; negative controls fail as required.", "author": "thakrarsagar", "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) for computation design, code and text; reviewed and submitted by thakrarsagar.", "open_questions": [ diff --git a/research/e6-d5-gram-realisation-rigidity/verify.py b/research/e6-d5-gram-realisation-rigidity/verify.py index a8881fd44a..515a0a6dbb 100644 --- a/research/e6-d5-gram-realisation-rigidity/verify.py +++ b/research/e6-d5-gram-realisation-rigidity/verify.py @@ -15,8 +15,12 @@ from above, and * a prime rank of an explicit family of rational tangent vectors bounds their rational SPAN from below. -The two bounds meet, so every dimension asserted below is exact over Q (and -over every field of characteristic 0). +Every load-bearing dimension is certified either by such a matching pair of +bounds or by an exact Fraction rank (rank_frac, tangent_exact); it is then exact +over Q (and over every field of characteristic 0). Negative controls whose +exact value would need the unsafe direction of a prime rank are computed with +rank_frac or with an explicit lower-bound family. Proof-relevant intermediate +checks use assert, so the script refuses to run under python -O. """ import itertools import sys @@ -265,6 +269,13 @@ def e6_in_e8_coordinates(): return X, [list(x) for x in X] +def tangent_exact(X, Y, pairs): + """Exact dim T_M V over Q (Fraction elimination; small units only).""" + v, T = len(X), len(X[0]) + assert rank_frac(X) == T and rank_frac(Y) == T + return 2 * v * T - rank_frac(tangent_system(X, Y, pairs)) - T * T + + def tangent_upper_ambient(X, pairs, p, T): """Same tangent space with X = Y of rank T inside K^n (n > T), positive definite form: the kernel of (dX, dY) -> dX X^T + X dY^T is T^2 + 2 v (n - T) @@ -434,6 +445,8 @@ def side(Z): def modp(x, p=P1): x = F(x) + if x.denominator % p == 0: + raise ValueError("denominator divisible by p") return x.numerator * pow(x.denominator, p - 2, p) % p @@ -498,6 +511,8 @@ def bd_block_rank(G, R, A): # ---------------------------------------------------------------- main def main(argv): + if not __debug__: + raise SystemExit("verify.py relies on assert for proof-relevant intermediate checks; run without -O") t_start = time.time() print("== Part A: E6 first-order rigidity at the Gram point ==") X6, Y6 = simple_root_unit("E", 6) @@ -620,9 +635,11 @@ def main(argv): print("== Controls (dimension changes / non-rigid units) ==") X4, Y4 = dn_unit(4) r4 = rigidity_report("D4", X4, Y4) - f4 = rank_mod(family_tangent_vectors(4) + orbit_tangent_vectors(mat(X4, Y4)), 144, P1) - check("D4 control (has a 4-frame): tangent 44 > orbit 23 (not rigid); edge family covers only 23+9=32", - r4["upper"] == [44] and r4["orbit"] == 23 and f4 == 32, "family+orbit span %d" % f4) + f4 = rank_frac(family_tangent_vectors(4) + orbit_tangent_vectors(mat(X4, Y4))) + e4 = tangent_exact(X4, Y4, orth_pairs(mat(X4, Y4))) + check("D4 control (has a 4-frame): tangent 44 > orbit 23 (not rigid; exact Fraction rank); " + "edge family + orbit spans exactly 32 (exact)", + r4["upper"] == [44] and e4 == 44 and r4["orbit"] == 23 and f4 == 32, "family+orbit span %d" % f4) X6d, Y6d = dn_unit(6) r6 = rigidity_report("D6", X6d, Y6d) f6 = rank_mod(family_tangent_vectors(6) + orbit_tangent_vectors(mat(X6d, Y6d)), 900, P1) @@ -639,20 +656,30 @@ def main(argv): check("E8 control: tangent 239 = 2v-1", r8["upper"] == [239] and r8["orbit"] == 239) print("== Negative controls (each must FAIL the corresponding acceptance test) ==") - # Removing a single orthogonal pair (or up to 10 of the 15 at line 0, in this - # order) leaves E6 first-order rigid -- the zero pattern is redundant at first - # order -- so the perturbation that must break rigidity removes all 15 - # orthogonality constraints of line 0 (row and column). + # Removing a single orthogonal pair leaves E6 first-order rigid (checked + # below), so the perturbation that must break rigidity removes all 15 + # orthogonality constraints of line 0 (row and column). (Partial removals + # at line 0 were explored in scratch only; the outcome depends on the + # removal order and is NOT certified here.) one = rigidity_report("E6-minus-one-pair", X6, Y6, drop={orth_pairs(G6)[0]}) check("E6 robustness: one orthogonal pair removed, still 71", one["upper"] == [71]) drop0 = {(0, s) for s in range(36) if s != 0 and G6[0][s] == 0} rn = rigidity_report("E6-line0-unconstrained", X6, Y6, drop=drop0) neg1 = rn["upper"][0] == rn["orbit"] - check("NEG E6 pattern with the 15 orthogonality constraints of line 0 removed is NOT rigid (81 > 71)", - not neg1 and rn["upper"] == [81], "tangent upper %d vs orbit %d" % (rn["upper"][0], rn["orbit"])) + # exact lower bound: orbit + free first-order moves of x_0 and y_0 (dX = E_0 u, dY = E_0 w); + # these vectors vanish on every remaining constrained pair because no pair involves line 0. + free0 = [[(Y6[s][a] if t == 0 else 0) for t in range(36) for s in range(36)] for a in range(6)] + free0 += [[(X6[t][a] if s == 0 else 0) for t in range(36) for s in range(36)] for a in range(6)] + pairs_rn = orth_pairs(G6, drop0) + low_rn = rank_mod(orbit_tangent_vectors(G6) + free0, 36 * 36, P1) + check("NEG E6 pattern with the 15 orthogonality constraints of line 0 removed: rigidity certificate fails; " + "tangent exactly 81 > 71 (prime upper bound 81 matched by orbit + free line-0 moves, prime lower bound 81)", + not neg1 and rn["upper"] == [81] and low_rn == 81 and all(in_pattern(z, 36, pairs_rn) for z in free0), + "tangent upper %d, explicit lower %d, orbit %d" % (rn["upper"][0], low_rn, rn["orbit"])) rd = rigidity_report("D5-minus-one-pair", X5, Y5, drop={orth_pairs(G5)[0]}) - check("NEG D5 pattern with one orthogonal pair removed: tangent 57 != 55 (dimension is pattern-sensitive)", - rd["upper"] == [57]) + ed = tangent_exact(X5, Y5, orth_pairs(G5, {orth_pairs(G5)[0]})) + check("NEG D5 pattern with one orthogonal pair removed: tangent exactly 57 != 55 (exact Fraction rank)", + rd["upper"] == [57] and ed == 57) Xb, Yb = d5_family(D5_POINTS["pt1"], sign_bug=True) Mb = mat(Xb, Yb) check("NEG D5 family with sign error in y_{ij-} violates the pattern zeros", @@ -663,8 +690,9 @@ def main(argv): extra = [w for w in classes if rank_frac([Xc[t] for t in range(v5) if w >> t & 1]) < 5] check("NEG inadmissible a=-b on edge 01: zero diagonal entry and extra deficient classes", any(Mc[t][t] == 0 for t in range(v5)) and len(extra) > 5, "%d deficient classes" % len(extra)) - a_only = rank_mod(fam[0::2] + orbit5, v5 * v5, P1) - check("NEG half family (b frozen, 10 a-directions) + orbit spans < 55: the lower bound is not automatic", + a_only = rank_frac(fam[0::2] + orbit5) + check("NEG half family (b frozen, 10 a-directions) + orbit spans < 55 (exact Fraction rank): " + "the lower bound is not automatic", a_only < 55, "span %d" % a_only) Mbad = mat(*d5_family(D5_POINTS["pt2"]))