diff --git a/research/complex-rank8-rigidity-extension/PROOF.md b/research/complex-rank8-rigidity-extension/PROOF.md new file mode 100644 index 0000000000..4469afe008 --- /dev/null +++ b/research/complex-rank8-rigidity-extension/PROOF.md @@ -0,0 +1,100 @@ +# Rank-8 rigidity passes to supersets + +Notation and the system (E) are those of PR1212 (`research/complex-rank8-decoder-rigidity/PROOF.md` at head +`57099cb5`, §0). For a set L of root lines, call L *rigid* if every L × L matrix K of rank at most 8 over a field +of characteristic 0 that satisfies (E) on L equals `D (2 G_L) D⁻¹` for an invertible diagonal D. Finite facts +marked **[X]** are recomputed by this package's `verify.py` (check id `X`). + +## Lemma 10 (extension) + +**Lemma 10.** Let L ⊂ L′ be sets of lines with L rigid and with the roots of L spanning R⁸. Suppose that for +every i ∈ L′ \ L, the lines j ∈ L with G_ij = 0 span `r_i^⊥`. Then L′ is rigid. + +*Proof.* Let K′ have rank at most 8 and satisfy (E) on L′. Its principal submatrix K′[L,L] satisfies (E) on L +and has rank at most 8. So K′[L,L] = D (2 G_L) D⁻¹ = 2 D R Rᵀ D⁻¹, where R is the L × 8 matrix of the roots +r_j (Gram units). R has rank 8, so K′[L,L] has rank 8, and so does K′. + +Because rank K′ = rank K′[L,L] = 8, every row of K′ is a combination of the rows indexed by L. Write +K′[i,:] = y_iᵀ K′[L,:]. On the columns L this reads K′[i,L] = y_iᵀ K′[L,L] = 2 u_iᵀ Rᵀ D⁻¹ with +u_i = Rᵀ D y_i ∈ R⁸. That is, K′_ij = 2 ⟨u_i, r_j⟩ / d_j for j ∈ L. + +(E) gives K′_ij = 0 for every j ∈ L orthogonal to i. These r_j span `r_i^⊥`, so u_i = c_i r_i for some +scalar c_i. The same argument on columns gives K′_ji = 2 d_j ⟨r_j, w_i⟩ with w_i = c′_i r_i. + +Next, compare entries between two new lines i, i′. Since K′[i,:] = y_iᵀ K′[L,:], we get +K′_ii′ = y_iᵀ K′[L,i′] = 2 c′_i′ y_iᵀ D R r_i′, and y_iᵀ D R = u_iᵀ = c_i r_iᵀ by definition. So +K′_ii′ = 2 c_i c′_i′ G_ii′ for all new i, i′. Taking i = i′, (E) gives +K′_ii = 4 c_i c′_i = 4, so c′_i = 1/c_i. Set d_i = c_i for the new lines. Then K′_ab = 2 G_ab d_a / d_b +for all a, b ∈ L′. ∎ + +The proof uses the constraints of (E) only on new-versus-old orthogonal pairs and on the new diagonal. The +constraints between two new lines hold automatically. It needs no zero exclusion, no pivot and no class +structure. + +Both hypotheses matter: + +- **Rank.** A rank-one term supported on the odd entries of a new row satisfies (E). It gives a rank-9 + solution that is not gauge **[control.rank9-escapes]**. +- **Span.** If the orthogonal old lines span only a hyperplane of `r_i^⊥`, there is a rank-8 extension of a + gauge solution that satisfies (E) and is not gauge **[control.span-needed]**. + +## Theorem (bi-frame supersets) + +**Theorem.** Let F1, F2 be disjoint frames and S ⊆ F1 ∪ F2. Then the live set E8 \ S is rigid. + +*Proof.* W(E8) is transitive on the 2025 frames **[model.frame-transitivity]**, and its elements preserve +(E) and the gauge form (PR1212 §0). So take F1 = FRAME0, which puts F2 inside P112. + +The unit L = E8 \ (FRAME0 ∪ F2) is rigid in each of the three FRAME0-stabiliser orbits of F2 +**[unit.frame-orbits]**: + +- type (2,2,2,2): PR1212, Theorem 1′; +- type (4,4): PR1389; +- type (1,…,1): PR1399. + +For every one of the 1260 units and every one of the 16 lines i ∈ FRAME0 ∪ F2, the live lines orthogonal to i +span `r_i^⊥`. There are at least 52 of them in each case **[lemma10.span-condition]**. The roots of L span R⁸, +because L also contains a line non-orthogonal to i: i has 56 such lines in E8, and at most 15 of them are +removed. Lemma 10 then applies to L ⊂ E8 \ S. ∎ + +**Corollary (floor).** On each of these live sets, every decoder with exactly eight costly terms in the E-graph +model has cst ≥ 72 − |S| when |S| ≤ 15, and cst ≥ 56 when |S| = 16. The proof is PR1212 §8 verbatim with +PR968's Theorem 4(b); see `research/complex-frame-pair-decoders/PROOF.md` §4. It inherits PR968's cited premise +(F6). + +## Which intermediate punctures this reaches + +Now take S = FRAME0 ∪ X with X ⊂ P112. The question is when FRAME0 ∪ X lies in the union of two disjoint +frames. + +- **Exactly when X lies in a frame inside P112.** Running over all pairs of disjoint frames whose union + contains FRAME0, the sets (F1 ∪ F2) \ FRAME0 are exactly the 1260 frames inside P112 + **[census.biframe-covers]**. +- **P111.** Every line of P112 lies in a type-(2,2,2,2) frame inside P112 **[census.p111-from-2222]**. So + P111 rigidity follows from PR1212's Theorem 1′ alone. This is a second proof of PR1389's P111 result. It + needs neither PR1389's three-row class argument nor P111's own zero-exclusion certificate. +- **P110.** Every orthogonal pair in P112 lies in a type-(2,2,2,2) frame inside P112. So all 3304 + orthogonal-pair P110 units are rigid, again from PR1212 alone **[census.table]**. +- **P105–P109.** The covered X are counted below **[census.table]**. The "cheapest" column gives the + first rigid P104 type that contains X, in the order PR1212, then PR1399, then PR1389. + +| \|X\| | unit | all X | orthogonal X | covered X | cheapest: PR1212 / PR1399 / PR1389 | +|---:|---|---:|---:|---:|---| +| 1 | P111 | 112 | 112 | 112 | 112 / 0 / 0 | +| 2 | P110 | 6216 | 3304 | 3304 | 3304 / 0 / 0 | +| 3 | P109 | 227920 | 31024 | 29232 | 14784 / 14336 / 112 | +| 4 | P108 | 6210820 | 94892 | 77868 | 22512 / 53760 / 1596 | +| 5 | P107 | 134153712 | 82656 | 70560 | 18816 / 50176 / 1568 | +| 6 | P106 | 2392407864 | 39088 | 35280 | 9408 / 25088 / 784 | +| 7 | P105 | 36227890512 | 10592 | 10080 | 2688 / 7168 / 224 | + +**What is not reached.** + +- Any X containing an odd pair. No frame contains an odd pair, so Lemma 10 from a P104 unit cannot apply. + At P110 these are 2912 pairs in two stabiliser orbits, of sizes 224 and 2688. Write T_x for the four FRAME0 + lines not orthogonal to x. In the 224-orbit T_x = T_y; in the 2688-orbit T_x and T_y share two lines + **[census.p110-odd-orbits]**. +- Orthogonal sets X that do not extend to a frame inside P112, for example 1792 of the 31024 orthogonal + triples. + +For |X| ≥ 4 the covered X are a small fraction of all X, so most of P105–P108 is still open. diff --git a/research/complex-rank8-rigidity-extension/README.md b/research/complex-rank8-rigidity-extension/README.md new file mode 100644 index 0000000000..309c5085e5 --- /dev/null +++ b/research/complex-rank8-rigidity-extension/README.md @@ -0,0 +1,99 @@ +# Rank-8 rigidity passes to supersets: P105–P110 partial-frame punctures, and P111 from PR1212 alone (no new κ) + +**Status: scoped structural result. No κ claim, no construction.** It builds on the rank-8 rigidity line of PR1212 +(burntout76, `research/complex-rank8-decoder-rigidity/`, open, head `57099cb5`), PR1389 and PR1399. It answers +PR1399's open next question, the intermediate punctures P105–P110, as far as a linear argument reaches. + +In PR717's E-graph (masked) model, a live set L is *rigid* if every rank-≤8 solution K of PR1212's system (E) +(`K_ii = 4`, `K_ij = 0` on orthogonal live pairs, odd entries free) is `D(2G)D⁻¹`. Rigidity is what turns +PR968's eight-term floor into a floor for masked decoders with exactly eight costly terms (PR1212 §8). + +**Lemma 10 (extension).** Suppose L ⊂ L′, L is rigid, and the roots of L span R⁸. Suppose also that for each new +line i, the lines of L orthogonal to i span `r_i^⊥`. Then L′ is rigid. + +The proof ([PROOF.md](PROOF.md)) is a few lines of linear algebra. K′[L,L] already has rank 8, so each new row +is `2uᵀRᵀD⁻¹` on L. The zeros against the orthogonal old lines force `u ∝ r_i`, and the diagonal fixes the +scale. There is no zero exclusion, no DRUP certificate and no class argument. + +**Theorem.** E8 \ S is rigid whenever S lies in the union of two disjoint frames. The P104 units are rigid by +PR1212, PR1389 and PR1399. The span condition holds on all 1260 units for all 16 new lines, with at least 52 +orthogonal live lines each. + +**What it reaches.** For P112 minus X: + +- **Coverage rule.** FRAME0 ∪ X lies in a union of two disjoint frames exactly when X lies in a frame inside + P112. +- **P111.** Every line lies in a type-(2,2,2,2) frame, so P111 rigidity follows from PR1212 alone. This is a + second proof of PR1389's P111 result. +- **P110.** All 3304 orthogonal-pair units are rigid, again from PR1212 alone. +- **P105–P109.** 29232, 77868, 70560, 35280 and 10080 covered X for |X| = 3, …, 7. The PROOF.md table splits + them by which predecessor they need. + +The eight-costly-term floor on each covered unit is then cst ≥ 72 − p with p = 8 + |X|, by PR968 +Theorem 4(b) via PR1212 §8. + +## Reproduce + +From the repository root, Python 3.10+, standard library only, about 1 s: + +```sh +python3 -I -B research/complex-rank8-rigidity-extension/verify.py +``` + +Expected final line: + +```text +PASS_COMPLEX_RANK8_RIGIDITY_EXTENSION: checks 14; Lemma 10 on all 1260 bi-frame units; 226324 punctures P105-P110 covered (all 3304 orthogonal-pair P110); P111 from PR1212 alone; P104 rigidity cited from PR1212/PR1389/PR1399 +``` + +The verifier has its own E8 model and recomputes everything it uses: + +- the 2025 frames and W(E8) transitivity on them; +- the three FRAME0-stabiliser orbits of the 1260 frames in P112, matched to the three types; +- the span condition; +- the cover census, the P111 cover, the P105–P110 table and the odd-pair P110 orbits. + +It also runs exact rational checks of the lemma's mechanism and three controls: + +- a rank-9 solution escapes; +- without the span condition there is a rank-8 non-gauge extension; +- a perturbed orthogonal entry is rejected. + +## Not covered + +- **Punctures containing an odd pair.** No frame contains an odd pair, so Lemma 10 from a P104 unit cannot + reach them. This is most of P105–P110. At P110 it is 2912 pairs in two stabiliser orbits, of sizes 224 + and 2688. +- Orthogonal X that do not extend to a frame inside P112, for example 1792 of the 31024 orthogonal triples. +- **Inherited P104 rigidity** is cited, not recomputed. The type-(2,2,2,2) units come from PR1212 Theorem 1′, + which is open and so is the whole chain. The other two types come from PR1389 and PR1399, both unmerged and + unreviewed. P111 and all of P110's covered units need only PR1212. +- **Nine or more costly terms.** Rank-8 rigidity says nothing about rank ≥ 9; see control.rank9-escapes. +- PR968's flat-classification premise (F6) is inherited through the floor. Attainment of 72 − p on these + particular units is not checked. +- The written proof has had no independent human review. There is no construction and no κ change, and every + condition of the selected record is unchanged. + +## Open next questions + +**Odd-pair P110.** Is P112 minus an odd pair {x, y} rigid? These are the two stabiliser orbits of sizes 224 and +2688 (see [TASK.json](TASK.json)). + +- *Why it matters.* They are the whole remaining eight-term gap at P110, and the extension lemma cannot reach + them. +- *A feasible first step.* Per orbit, pick a pivot frame inside the unit. Test PR1212's (I3) and (I4) on the + complete classes, then PR1399's Lemma 9 witness connectivity for the lines of incomplete classes. Build the + zero-exclusion CNF with PR1212's `make_proof.py`. +- *The blocker.* Zero exclusion passes up to supersets, but these units contain no smaller unit with a known + certificate. Each orbit therefore needs its own DRUP proof. + +## Credit + +- **burntout76 / Brett Halligan (PR1212):** the rigidity theorem, (E), the type-(2,2,2,2) units, the transport + and §8's floor argument. +- **themilkman216 (PR968):** the eight-term floor 72 − p and its puncture theorem. +- **DreamingOfClouds (PR717):** the E-graph model. +- **PR1389, PR1399 (JosieElliston):** the type-(4,4) and admissible P104 units. + +Prepared by JosieElliston with substantial assistance from Claude Opus 5.5 (Anthropic) via Claude Code, +covering the lemma, verifier and write-up. Apache-2.0. diff --git a/research/complex-rank8-rigidity-extension/SOURCES.json b/research/complex-rank8-rigidity-extension/SOURCES.json new file mode 100644 index 0000000000..43693ebc24 --- /dev/null +++ b/research/complex-rank8-rigidity-extension/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + } + ] +} diff --git a/research/complex-rank8-rigidity-extension/TASK.json b/research/complex-rank8-rigidity-extension/TASK.json new file mode 100644 index 0000000000..e7a88e02a4 --- /dev/null +++ b/research/complex-rank8-rigidity-extension/TASK.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "task_id": "complex-masked-decoder", + "priority_revision": 2, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "original_card": { + "id": "complex-masked-decoder", + "question": "Can one specified masked or overcomplete decoder improve the complete moment budget?", + "starting_points": [ + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md" + ], + "methods": [ + "Synthesize a decoder with exact coefficients and fully priced helper endpoints.", + "Bound the best possible budget for a fixed support alphabet before synthesis." + ], + "acceptance_gate": "Change an assumption of the eight-term all-pairs bound and count all copied information, frames and restoration.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-decoder-field-extension-seed44/verify.py" + ], + "expected": "PASS_COMPLEX_DECODER_FIELD_EXTENSION_S44", + "inspect": "Locate the excluded classes: masked identities, at least nine terms, and deeper punctures.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one finite support alphabet and test exact decoding constraints before building a whole network.", + "bottleneck_link": "A cheaper fully realized decoder could increase deficit or lower recursive cost on the binding complex side.", + "allowed_variations": [ + "Select a specific masked or overcomplete family with exact labels and supports." + ], + "scope_change_triggers": [ + "Repeating the exact eight-term all-pairs search inside its proved scope." + ], + "overlap_terms": [ + "masked decoder", + "overcomplete", + "eight-term" + ] + }, + "scope_status": "refined", + "actual_scope": "Proof obligation inside the masked (E-graph) model: on which intermediate punctures P112 minus X (|X| = 2..7, i.e. P105-P110) does every rank-<=8 solution of PR1212's system (E) equal D(2G)D^-1, so that decoders with exactly eight costly terms keep PR968's floor 72 - p? Answered by an extension lemma from the P104 frame complements, with an exact census of the punctures it reaches and of what is left.", + "scope_change_reason": "The card asks whether a masked decoder can beat the floor. PR1212, PR1389 and PR1399 answered it for exactly eight costly terms on P120, P112, P111 and every P104 frame complement, and PR1399 lists P105-P110 as its open next question. This settles the punctures that lie inside a frame and gives a second proof of P111 from PR1212 alone; it does not construct a decoder.", + "bottleneck_link": "Side result on the binding complex supplier: it rules out masked eight-costly-term decoders below PR968's floor on every partial-frame puncture between P112 and P104, so the remaining masked escape routes are nine or more costly terms or punctures containing an odd pair.", + "budget_minutes": 60, + "stop_rule": "Stop at what the extension lemma reaches; punctures with an odd pair (starting with the two P110 orbits) and nine or more costly terms are left as handoffs.", + "outcome": "completed", + "evidence": "verify.py: 9 exact checks (E8 model, 2025 frames and W(E8) transitivity, stabiliser orbits of the 1260 frames in P112, the span condition on all 1260 x 16 new lines, the bi-frame cover census, the P111 cover, the P105-P110 table, the odd-pair P110 orbits) plus 5 algebraic checks and controls, about 1 s. Rigidity of the P104 units is cited from PR1212, PR1389 and PR1399, not recomputed.", + "author": "JosieElliston (with Claude Opus 5.5 via Claude Code)", + "ai_assistance": "Claude Opus 5.5 via Claude Code: proof, verifier and write-up. Submitted by the account holder.", + "open_questions": [ + { + "question": "Does rank-8 rigidity of (E) hold on P112 minus an odd pair {x, y} (G_xy = +-1), the two FRAME0-stabiliser orbits of sizes 224 and 2688 that make up the rest of P110?", + "why_it_matters": "With this package every orthogonal-pair P110 unit is rigid; the odd pairs are the whole remaining eight-term gap at P110, and the extension lemma cannot reach them because no frame contains an odd pair.", + "first_step": "For each orbit representative pick a pivot frame inside P112 minus {x, y}, test PR1212's inputs (I3), (I4) on the complete classes and PR1399's Lemma 9 witness connectivity for the lines of incomplete classes, then build the zero-exclusion CNF with PR1212's make_proof.py.", + "blocked_by": "Zero exclusion is not inherited: P112 minus an odd pair contains no unit with a known certificate, so each orbit needs its own DRUP proof (python-sat), which no submitted package has." + } + ] +} diff --git a/research/complex-rank8-rigidity-extension/VERIFY.json b/research/complex-rank8-rigidity-extension/VERIFY.json new file mode 100644 index 0000000000..2963c3ff9b --- /dev/null +++ b/research/complex-rank8-rigidity-extension/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "9 exact census and structure checks (E8 model, frames, W(E8) transitivity, stabiliser orbits, Lemma 10 span condition on all 1260 bi-frame units, bi-frame cover census, P111 cover, P105-P110 table, odd-pair P110 orbits) and 5 algebraic checks/controls. P104 rigidity is cited from PR1212/PR1389/PR1399." + } + ] +} diff --git a/research/complex-rank8-rigidity-extension/verify.py b/research/complex-rank8-rigidity-extension/verify.py new file mode 100644 index 0000000000..104106747f --- /dev/null +++ b/research/complex-rank8-rigidity-extension/verify.py @@ -0,0 +1,411 @@ +#!/usr/bin/env python3 +"""Rank-8 rigidity of the E-graph system passes to supersets (Lemma 10), and the census of the +intermediate punctures P112 minus X that it reaches. + +Standard library only, exact integer arithmetic. Independent of PR1212's code: own E8 model, frames, +reflections, stabiliser orbits, span checks and census. Run from the repository root: + + python3 -I -B research/complex-rank8-rigidity-extension/verify.py +""" + +import itertools +import math +import sys +from collections import Counter +from fractions import Fraction + +RESULTS = [] + + +def check(tag, cond, info=''): + RESULTS.append(tag) + status = 'PASS' if cond else 'FAIL' + print(f'{status} {tag}' + (f': {info}' if info else '')) + if not cond: + print(f'FAIL_COMPLEX_RANK8_RIGIDITY_EXTENSION: {tag}') + sys.exit(1) + + +# ---------------------------------------------------------------- E8 model (doubled coordinates) + +def lines_e8(): + """One representative per root line, roots in doubled coordinates (norm 8), canonical sign: + the first nonzero coordinate is positive.""" + out = set() + for i, j in itertools.combinations(range(8), 2): + for sj in (2, -2): + v = [0] * 8 + v[i], v[j] = 2, sj + out.add(tuple(v)) + for s in itertools.product((1, -1), repeat=7): + v = (1,) + s + if v.count(-1) % 2 == 0: + out.add(v) + return sorted(out) + + +LINES = lines_e8() +NL = len(LINES) +IDX = {v: n for n, v in enumerate(LINES)} + + +def canon(v): + v = tuple(v) + first = next(a for a in v if a) + return v if first > 0 else tuple(-a for a in v) + + +def ip(x, y): + d = sum(a * b for a, b in zip(x, y)) + assert d % 4 == 0 + return d // 4 + + +G = [[ip(LINES[i], LINES[j]) for j in range(NL)] for i in range(NL)] +ORTH = [[j for j in range(NL) if j != i and G[i][j] == 0] for i in range(NL)] +ORTH_MASK = [sum(1 << j for j in ORTH[i]) for i in range(NL)] + +FRAME0 = frozenset(IDX[canon(v)] for v in [ + (2, 2, 0, 0, 0, 0, 0, 0), (2, -2, 0, 0, 0, 0, 0, 0), (0, 0, 2, 2, 0, 0, 0, 0), (0, 0, 2, -2, 0, 0, 0, 0), + (0, 0, 0, 0, 2, 2, 0, 0), (0, 0, 0, 0, 2, -2, 0, 0), (0, 0, 0, 0, 0, 0, 2, 2), (0, 0, 0, 0, 0, 0, 2, -2)]) +P112 = [i for i in range(NL) if i not in FRAME0] + + +def all_frames(): + out = [] + + def grow(cur, cand): + if len(cur) == 8: + out.append(frozenset(cur)) + return + c = cand + while c: + j = (c & -c).bit_length() - 1 + c &= c - 1 + grow(cur + [j], cand & ORTH_MASK[j] & ~((1 << (j + 1)) - 1)) + + grow([], (1 << NL) - 1) + return out + + +def reflection_perm(r): + """Line permutation of the reflection in root r: v -> v - r (Gram units).""" + rv = LINES[r] + return tuple(IDX[canon(tuple(a - G[i][r] * b for a, b in zip(LINES[i], rv)))] for i in range(NL)) + + +def frame_type(F1, F2): + """Multiplicities of the classes of F1 met by F2. A line f outside F1 is non-orthogonal to exactly four + lines T_f of F1; its class is T_f together with the sign pattern of (e in T_f) up to overall + sign and parity (PR1212's Hadamard classes).""" + F1s = sorted(F1) + cls = Counter() + for f in F2: + T = tuple(e for e in F1s if G[f][e] != 0) + signs = [G[f][e] for e in T] + cls[(T, signs.count(-1) % 2)] += 1 + return tuple(sorted(cls.values(), reverse=True)) + + +def rank_int(vectors, target=None): + """Exact rank by fraction-free incremental elimination; stops early at `target`.""" + basis = [] # list of (pivot, row) + for v in vectors: + v = list(v) + for p, b in basis: + if v[p]: + v = [x * b[p] - y * v[p] for x, y in zip(v, b)] + nz = [k for k, x in enumerate(v) if x] + if nz: + g = math.gcd(*v) + basis.append((nz[0], [x // g for x in v])) + if target is not None and len(basis) >= target: + break + return len(basis) + + +# ---------------------------------------------------------------- exact linear algebra for the controls + +def matmul(A, B): + return [[sum(A[i][k] * B[k][j] for k in range(len(B))) for j in range(len(B[0]))] for i in range(len(A))] + + +def rank_q(rows): + M = [[Fraction(x) for x in r] for r in rows] + rk, col = 0, 0 + ncol = len(M[0]) if M else 0 + while rk < len(M) and col < ncol: + piv = next((r for r in range(rk, len(M)) if M[r][col] != 0), None) + if piv is None: + col += 1 + continue + M[rk], M[piv] = M[piv], M[rk] + for r in range(len(M)): + if r != rk and M[r][col] != 0: + f = M[r][col] / M[rk][col] + M[r] = [a - f * b for a, b in zip(M[r], M[rk])] + rk += 1 + col += 1 + return rk + + +def e_system_holds(K, live): + """(E) on the live list: K_ii = 4 and K_ij = 0 on orthogonal live pairs; odd entries free.""" + for a, i in enumerate(live): + if K[a][a] != 4: + return False + for b, j in enumerate(live): + if a != b and G[i][j] == 0 and K[a][b] != 0: + return False + return True + + +def is_gauge(K, live): + """K = D (2G) D^{-1}: K_ij = 0 iff G_ij = 0, and d_i/d_j recovered consistently along a spanning tree.""" + n = len(live) + for a in range(n): + for b in range(n): + if (K[a][b] == 0) != (G[live[a]][live[b]] == 0): + return False + d = [None] * n + d[0] = Fraction(1) + stack = [0] + while stack: + a = stack.pop() + for b in range(n): + if d[b] is None and G[live[a]][live[b]] != 0: + d[b] = d[a] * 2 * G[live[a]][live[b]] / K[a][b] # K_ab = 2 G_ab d_a / d_b + stack.append(b) + if any(x is None for x in d): + return False + return all(K[a][b] == 2 * G[live[a]][live[b]] * d[a] / d[b] for a in range(n) for b in range(n)) + + +def lcg(seed): + x = seed + while True: + x = (x * 6364136223846793005 + 1442695040888963407) % (1 << 64) + yield x >> 33 + + +def rand_nonzero(rng): + v = 0 + while v == 0: + v = next(rng) % 9 - 4 + return Fraction(v, next(rng) % 5 + 1) + + +def gauge_matrix(live, d): + n = len(live) + return [[2 * G[live[a]][live[b]] * d[a] / d[b] for b in range(n)] for a in range(n)] + + +# ---------------------------------------------------------------- checks + +def main(): + check('model.lines', NL == 120 and all(G[i][i] == 2 for i in range(NL)) + and all(G[i][j] in (0, 1, -1) for i in range(NL) for j in range(NL) if i != j) + and all(len(ORTH[i]) == 63 for i in range(NL)), '120 lines, off-diagonal Gram in {0,+-1}, 63 orthogonal') + + frames = all_frames() + fset = set(frames) + check('model.frames', len(frames) == 2025 and FRAME0 in fset, '2025 frames, FRAME0 among them') + + # W(E8) is transitive on frames (BFS under the 120 root reflections). + refl = [reflection_perm(r) for r in range(NL)] + seen = {FRAME0} + todo = [FRAME0] + while todo: + F = todo.pop() + for p in refl: + H = frozenset(p[i] for i in F) + if H not in seen: + seen.add(H) + todo.append(H) + check('model.frame-transitivity', seen == fset, f'{len(seen)} frames in one orbit of W(E8)') + + # Frames inside P112, their three types, and that the types are exactly the FRAME0-stabiliser orbits. + inside = [F for F in frames if not F & FRAME0] + types = {F: frame_type(FRAME0, F) for F in inside} + tcount = Counter(types.values()) + want = {(1,) * 8: 896, (2, 2, 2, 2): 336, (4, 4): 28} + stab = [p for p in refl if frozenset(p[i] for i in FRAME0) == FRAME0] + for p, q in itertools.combinations(refl, 2): + pq = tuple(p[q[i]] for i in range(NL)) + if frozenset(pq[i] for i in FRAME0) == FRAME0: + stab.append(pq) + orbits = [] + left = set(inside) + while left: + F = left.pop() + orb, todo = {F}, [F] + while todo: + H = todo.pop() + for p in stab: + J = frozenset(p[i] for i in H) + if J not in orb: + orb.add(J) + todo.append(J) + left -= orb + orbits.append(orb) + orbit_types = sorted((len(o), sorted({types[F] for F in o})) for o in orbits) + check('unit.frame-orbits', len(inside) == 1260 and dict(tcount) == want and len(orbits) == 3 + and all(len(ts) == 1 and want[ts[0]] == n for n, ts in orbit_types), + f'1260 frames in P112; stabiliser orbits {[n for n, _ in orbit_types]} = types (4,4), (2,2,2,2), (1,...,1); ' + f'{len(stab)} stabiliser generators') + + # Lemma 10 span condition: for every bi-frame unit L = E8 \ (FRAME0 u F) and every i in FRAME0 u F, + # the lines of L orthogonal to i span r_i^perp (rank 7). By transitivity this covers every pair of + # disjoint frames. + worst = 63 + bad = 0 + for F in inside: + R = FRAME0 | F + for i in R: + vecs = [LINES[j] for j in ORTH[i] if j not in R] + worst = min(worst, len(vecs)) + if rank_int(vecs, 7) != 7: + bad += 1 + check('lemma10.span-condition', bad == 0, + f'1260 units x 16 new lines: orthogonal live lines span r_i^perp (at least {worst} such lines each)') + + # Census: FRAME0 u X lies in a union of two disjoint frames iff X lies in a frame inside P112. + covers = set() + for F1 in frames: + A = F1 & FRAME0 + if not A: + continue + for F2 in frames: + if not F2 & F1 and FRAME0 - A <= F2: + covers.add(frozenset((F1 | F2) - FRAME0)) + check('census.biframe-covers', covers == set(inside), + f'{len(covers)} maximal X; every one is a frame inside P112') + + # Every line of P112 lies in a type-(2,2,2,2) frame inside P112: P111 from PR1212 Theorem 1' alone. + by2222 = set().union(*(F for F in inside if types[F] == (2, 2, 2, 2))) + check('census.p111-from-2222', by2222 == set(P112), 'all 112 lines lie in a type-(2,2,2,2) frame') + + # Count, for each k, the X of size k inside a frame of P112, by the cheapest rigid unit available. + pref = [((2, 2, 2, 2), 'PR1212'), ((1,) * 8, 'PR1399'), ((4, 4), 'PR1389')] + rank_of = {t: n for n, (t, _) in enumerate(pref)} + orth_count = Counter() + p112_mask = sum(1 << i for i in P112) + + def cliques(size, cand): + orth_count[size] += 1 + if size == 8: + return + c = cand + while c: + j = (c & -c).bit_length() - 1 + c &= c - 1 + cliques(size + 1, cand & ORTH_MASK[j] & ~((1 << (j + 1)) - 1)) + + cliques(0, p112_mask) + table = {} + for k in range(1, 9): + best = {} + for F in inside: + r = rank_of[types[F]] + for X in itertools.combinations(sorted(F), k): + if best.get(X, 9) > r: + best[X] = r + dep = Counter(pref[r][1] for r in best.values()) + table[k] = (math.comb(112, k), orth_count[k], len(best), dep['PR1212'], dep['PR1399'], dep['PR1389']) + expect = {1: (112, 112, 112, 112, 0, 0), 2: (6216, 3304, 3304), 7: (36227890512, 10592, 10080), + 8: (475491062970, 1260, 1260, 336, 896, 28)} + ok = all(table[k][:len(v)] == v for k, v in expect.items()) + for k in range(1, 9): + tot, orth, cov, a, b, c = table[k] + print(f' |X|={k} P{112 - k}: {tot} X, {orth} orthogonal, {cov} inside a P112 frame ' + f'(PR1212 {a}, PR1399 {b}, PR1389 {c}); fraction {cov / tot:.3e}') + check('census.table', ok, 'all orthogonal pairs covered; table above') + + # What is left at P110: the odd pairs, by FRAME0-stabiliser orbit (for the open next question). + odd = [frozenset(x) for x in itertools.combinations(P112, 2) if G[x[0]][x[1]] != 0] + left, sizes = set(odd), [] + while left: + X = left.pop() + orb, todo = {X}, [X] + while todo: + H = todo.pop() + for p in stab: + J = frozenset(p[i] for i in H) + if J not in orb: + orb.add(J) + todo.append(J) + left -= orb + a, b = sorted(X) + meet = len([e for e in FRAME0 if G[a][e] and G[b][e]]) + sizes.append((len(orb), meet)) + sizes.sort() + check('census.p110-odd-orbits', len(odd) == 2912 and sizes == [(224, 4), (2688, 2)], + 'uncovered P110: 2912 odd pairs in two stabiliser orbits, 224 (same FRAME0 block) and 2688 ' + '(blocks meeting in 2)') + + controls(inside, types) + + n_cov = sum(table[k][2] for k in range(2, 8)) + print(f'PASS_COMPLEX_RANK8_RIGIDITY_EXTENSION: checks {len(RESULTS)}; Lemma 10 on all 1260 bi-frame units; ' + f'{n_cov} punctures P105-P110 covered (all {table[2][1]} orthogonal-pair P110); P111 from PR1212 alone; ' + f'P104 rigidity cited from PR1212/PR1389/PR1399') + + +def controls(inside, types): + rng = lcg(20261013) + # Base unit: a type-(2,2,2,2) bi-frame complement; superset L' adds one line i of the punctured frame F. + F = min((F for F in inside if types[F] == (2, 2, 2, 2)), key=sorted) + R = FRAME0 | F + base = [j for j in range(NL) if j not in R] + i = min(F) + live = base + [i] + d = [rand_nonzero(rng) for _ in live] + K = gauge_matrix(live, d) + check('lemma10.positive', e_system_holds(K, live) and is_gauge(K, live) + and rank_q([r[:] for r in K]) == 8, f'gauge solution on {len(live)} lines satisfies (E), rank 8') + + # Lemma 10 mechanism, exactly: new row i equals 2 u^T R^T D^{-1} on the base; the zeros at base lines + # orthogonal to i put u in the annihilator of 7 independent vectors of r_i^perp, i.e. on the line of r_i. + zs = [LINES[j] for j in ORTH[i] if j not in R] + check('lemma10.row-forced', rank_q(zs) == 7 and all(ip(LINES[i], z) == 0 for z in zs), + f'{len(zs)} orthogonal base lines: u in their annihilator, which is spanned by r_i') + + # Control 1: rank 9 escapes. Add a rank-one term supported on row i and odd columns only; (E) still holds. + odd_cols = [b for b, j in enumerate(live) if j != i and G[i][j] != 0] + K9 = [r[:] for r in K] + for b in odd_cols[:3]: + K9[-1][b] += rand_nonzero(rng) + check('control.rank9-escapes', e_system_holds(K9, live) and not is_gauge(K9, live) + and rank_q(K9) == 9, 'rank-9 perturbation on odd entries of the new row satisfies (E), not gauge') + + # Control 2: span condition needed. Choose n in r_i^perp and drop every base line orthogonal to i but not + # to n. The surviving orthogonal lines span only a hyperplane of r_i^perp; build a rank-8 non-gauge + # extension with new row u = c (r_i + t n) and column w = r_i / c (doubled-coordinate vectors). + n_vec = next(LINES[j] for j in ORTH[i] if j not in R) + drop = {j for j in ORTH[i] if j not in R and ip(LINES[j], n_vec) != 0} + base2 = [j for j in base if j not in drop] + zs2 = [LINES[j] for j in ORTH[i] if j in base2] + rows = [LINES[j] for j in base2] + full = rank_q(rows) + live2 = base2 + [i] + d2 = [rand_nonzero(rng) for _ in base2] + c, t = rand_nonzero(rng), rand_nonzero(rng) + u = [c * (a + t * b) for a, b in zip(LINES[i], n_vec)] + w = [Fraction(a) / c for a in LINES[i]] + X = [[d2[a] * x for x in LINES[j]] for a, j in enumerate(base2)] + [u] + Y = [[x / d2[a] for x in LINES[j]] for a, j in enumerate(base2)] + [w] + # K = X Y^T / 4 * 2: roots are doubled (norm 8), so _Gram = x.y / 4 and K = 2 <.,.>. + K2 = [[Fraction(2) * sum(p * q for p, q in zip(x, y)) / 4 for y in Y] for x in X] + check('control.span-needed', full == 8 and rank_q(zs2) == 6 and e_system_holds(K2, live2) + and not is_gauge(K2, live2) and rank_q(K2) == 8, + f'dropping {len(drop)} lines leaves rank 6 in r_i^perp; a rank-8 non-gauge extension satisfies (E)') + + # Control 3: a perturbed orthogonal entry of the extended gauge solution violates (E). + Kp = [r[:] for r in K] + b = next(b for b, j in enumerate(live) if j != i and G[i][j] == 0) + Kp[-1][b] = Fraction(1, 7) + check('control.perturbed-fails', not e_system_holds(Kp, live), 'nonzero orthogonal entry is rejected') + + +if __name__ == '__main__': + main()