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..136fefb85c --- /dev/null +++ b/research/e6-d5-gram-realisation-rigidity/README.md @@ -0,0 +1,298 @@ +# 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 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 + +| 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`, ~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 +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. 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 +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: 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 + +```sh +python3 -I -B research/e6-d5-gram-realisation-rigidity/verify.py # ~8 s, stdlib +# 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 +``` + +**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: + 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 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. + +## 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 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 κ. + +## 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** (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** + (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**. + +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..dcb17b73fd --- /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, 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": [ + { + "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..515a0a6dbb --- /dev/null +++ b/research/e6-d5-gram-realisation-rigidity/verify.py @@ -0,0 +1,715 @@ +#!/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. +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 +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_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) + (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 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 + + +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))] + + +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): + 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) + 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)) + 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_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) + 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 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"] + # 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]}) + 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", + 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_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"])) + 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:])