diff --git a/research/p112-masked-fixed-reader-lift/PROOF.md b/research/p112-masked-fixed-reader-lift/PROOF.md new file mode 100644 index 0000000000..58b31eb8fb --- /dev/null +++ b/research/p112-masked-fixed-reader-lift/PROOF.md @@ -0,0 +1,184 @@ +# One E-graph term does not beat the fixed coordinate readers + +This is a theorem about one finite model. The executable checks in +`verify.py` certify the finite premises. The classical all-pairs floor is +an inherited theorem, pinned in `SOURCES.json` and not re-proved here. + +## Model + +Start from the 120 real E8 root lines and delete the eight mutually +orthogonal frame lines `e_(2a) ± e_(2a+1)`. The remaining 112 ports have +coordinate matrix `X`, with columns `x_0, ..., x_7`. Every entry of `X` is +0 or ±1, every row has four nonzeros, and each column support (a star) has +size 56. The Gram matrix `M4 = X X^T` equals 4 on the diagonal. Its +off-diagonal entry is 0 exactly on the pairs with label product 1. That +undirected graph, including loops at every port, is the E-graph: 60 ones +in each row. The other 52 ports in a row are the odd neighborhood. Label +pairing is the F2 matrix of this graph; its rank on all 112 ports is 9. + +A term has a reader vector and a source vector in `R^112`. Its copy cost +is the F2 rank of the label pairing between those two supports. The eight +coordinate terms `(x_k, x_k)` cost 8 each, total 64. That value belongs +to the coordinate decoder of PR620. An extra term is a pair `(d, t)`. + +**Theorem.** Suppose the eight coordinate readers stay equal to the columns +of `X`, and equality to `M4` is required only on the E-graph. For every +real reader `d`, every real source `t`, and every real source matrix whose +eight columns `s_0, ..., s_7` satisfy + +```text +sum_k X[i,k] s_k[j] + d[i] t[j] = M4[i,j] +``` + +whenever port `i` is on the E-graph at port `j`, + +```text +sum_k beta(x_k, s_k) + beta(d, t) >= 64. +``` + +Equality is attained by an E-graph-exact term that is not exact on the odd +pairs. No new multiplication exponent is claimed. Frames, restoration, +hosting, precision, and all-size analytic charges were not priced; they +were left at zero, and the copy-rank sum still does not fall below 64. + +## Normal form + +Write `N(j)` for the E-graph neighborhood of port `j`, a set of 60 ports. +`X` restricted to `N(j)` has rank 8, so it is injective on `R^8`. The same +count on `N(j) ∩ N(j')` is 8 for every one of the 3,304 E-graph edges and +6 for every one of the 2,912 odd pairs. Thus, at each `j`: + +- if `t[j] = 0`, the source row equals the row `X[j]`; +- if `t[j] ≠ 0`, then `d` agrees on `N(j)` with `X a` for a unique + `a = a(j) in R^8`, and the source row is `X[j] - t[j] a(j)`. + +Adjacent ports of the support `J = supp(t)` have the same `a`, because +their neighborhoods intersect in rank 8. So `a` is constant on each +E-component of `J`. + +`N(v)` without `v` has rank 7 and is orthogonal to the row `X[v]`. The +right kernel of those rows is the line through `X[v]`. + +## Star code + +On each star, the E-graph adjacency has F2 rank 8. Its 255 nonempty +codewords, 2,040 in total, fall into six families: + +| weight | components | common odd neighbors | count | +|---:|---|---:|---:| +| 28 | one | 0 | 576 | +| 32 | one | 0 | 504 | +| 28 | one | 1 | 448 | +| 24 | one | 1 | 448 | +| 24 | one | 0 | 56 | +| 56 | one | 0 | 8 | + +Every codeword is E-connected, and the minimum weight is 24. A coordinate +pairing rank drops below 8 only when the zero set of that source column +contains one of these codewords. Outside `J`, every source column agrees +with `X`, whose star support is the whole star. Therefore every dropped +coordinate meets a codeword inside `J`. + +Each of the 448 star memberships has 27 E-neighbors inside its star. The +pairing rank of that one column is 1. The 27 neighbors have rank 7, and +adding the point does not raise it. Those neighbors are disjoint from the +odd neighborhood of the point. While they remain in the source support, +changing the source entry at that single port does not change the +coordinate cost. + +## One codeword leaves at most one extra port + +If `J` contains no star codeword, every coordinate costs 8 and the extra +term costs at least 0, so the sum is at least 64. + +Now suppose `J` contains a codeword `W`. + +If `W` has no common odd neighbor, every port outside `W` has an E-edge +into `W`. Any further point of `J` joins the same component, so there is +one vector `a`. The reader `d` equals `Xa` on every E-neighborhood of `J`. +The complementary ports, if any, are orthogonal to all of `J`, so their +pairing rows do not affect `beta(d, t)`. The sources are exactly the +classical sources `X - t a^T`. The cost equals the classical single-lift +cost of `(a, t)`. + +If `W` has one common odd neighbor `v`, the same counting leaves at most +the port `v` outside `W`'s component: a second component would need +another port orthogonal to every point of `W`, and every such codeword has +only one. Both the 448 weight-28 codewords and the 448 weight-24 codewords +lie entirely in the odd neighborhood of their neighbor `v`. For each of +them, `X` on `N(v) ∩ (union of N(w) for w in W)` has rank 7 and is +orthogonal to `X[v]`, so its kernel is the line through `X[v]`. A larger +odd component only adds rows, so it does not enlarge that kernel. + +- If `v` is not in `J`, the sources are classical. The pairing row of `v` + against `J` is zero, so a reader value at `v` does not change the extra + rank. +- If `v` is in `J` and some E-neighbor of `v` is also in `J`, that neighbor + meets `W` (otherwise it would be a second common odd neighbor) and the + edge to `v` pulls `v` into `W`'s component. Again there is one vector `a`. +- If `v` is in `J` and no E-neighbor of `v` is in `J`, then + `J ⊆ {v} ∪ odd(v)`. The big component has a vector `a` and the singleton + `{v}` has a vector `b` with `b - a` in the joint kernel, hence + `b = a + λ X[v]`. The 27 E-neighbors of `v` stay outside `J`, so every + coordinate cost equals the classical cost of `(a, t)`. On `N(v)` the + Gram column of `v` vanishes off the diagonal, so `X b` and `X a` differ + only at port `v`. Ports outside every E-neighborhood of `J` contribute + zero pairing rows. The masked reader therefore differs from `Xa`, for + pairing against `J`, by at most the membership of port `v`. + +## Reduction to the classical floor, except one parallel line + +The inherited theorem, `research/p112-single-lift/PROOF.md`, states that +every classical single lift costs at least 64, and it says explicitly that +its argument does not cover a masked completion. This package uses that +theorem only after the masked term has been given the same coordinate +costs and the same extra rank as a classical lift. It does not replay the +3,272 sign systems. + +Let `S = supp(Xa)`. Over all 511 nonzero label functionals `q` and every +port `v` in the support `I_q`, the rows `X[I_q without v]` have corank at +most 1. The 112 corank-1 kernels that meet `X[v]` are parallel to that +row. The other 448 corank-1 kernels are orthogonal to `X[v]`. There is no +corank greater than 1. + +Consequently `v` is label-critical for `S` only when `a` is a nonzero +multiple of the row `X[v]`. If `a` is not such a multiple, `lab[v]` is in +the span of the other rows of `S`, so toggling port `v` in the reader does +not change the extra rank. The masked cost equals the classical cost and +is at least 64. + +If `a` is a nonzero multiple of `X[v]`, the four stars that do not contain +`v` have a zero coefficient, so they are not cancelled and cost 8. Each of +the four stars that contain `v` keeps its 27 E-neighbors in the source, so +it costs at least 7. When all four cost 8, the sum is at least 64. When +one costs less than 8, `J` contains an active codeword `W` of weight 28. +There are 448 of these, four at each port. Every odd neighbor of `v` lies +in an E-neighborhood of `W`, the Gram column is nonzero on all 52 of them, +and their pairing rank against `W` is 7. The coefficient `λ` does not +change that column off `N(v)`. The extra term therefore costs at least 7, +the coordinates cost at least 60, and the sum is at least 67. The zero +vector `a` cancels nothing; redundancy again leaves every coordinate at 8. + +## Equality and a strict deformation + +At port `v`, take `d` equal to the Gram column of `v` on the odd +neighborhood and equal to 0 on `N(v)`, with the extra source supported +only at `v` and with the eight coordinate sources left equal to `X`. The +E-graph column is unchanged. Every odd entry of that column is nonzero, so +the term is not all-pairs exact. All eight stars still cost 8, and the odd +reader pairs with `{v}` at rank 0. The sum is 64. + +A second witness cancels one active weight-28 codeword and retunes port +`v` by `λ = 1`. The resulting E-graph identity holds, one coordinate falls +to 7, and the extra rank rises enough that the sum is 71. + +## What was not proved + +The verifier's rational ranks are modular ranks at the prime 65,537. Every +8×8 minor of a 0/±1 matrix has absolute value at most `8^4 = 4096`, so +this prime does not hide a nonzero minor. Kernel vectors used for the +parallelism test are rebuilt over `Q` from seven original rows. + +The classical sign census inside the inherited proof was not run. Two +extra terms, a replaced coordinate reader, and any cost outside this +pairing-rank sum are outside the theorem. diff --git a/research/p112-masked-fixed-reader-lift/README.md b/research/p112-masked-fixed-reader-lift/README.md new file mode 100644 index 0000000000..536cc3939b --- /dev/null +++ b/research/p112-masked-fixed-reader-lift/README.md @@ -0,0 +1,106 @@ +# Fixed coordinate readers plus one E-graph term still cost 64 + +**Negative result for one masked family. No new κ, and the selected frontier is unchanged.** + +The eight P112 coordinate readers stay fixed. One extra term has to match +`X X^T` only on the E-graph, not on the odd pairs. In that model the sum of +pairing-rank copy costs is at least 64. Equality is attained by a reader +supported on an odd neighborhood: the term is E-graph exact, it moves odd +Gram entries, and its own pairing rank is 0. + +This is the masked gap left open by the classical single-lift theorem. That +theorem already proves the same floor when the identity is required on every +pair, and it says that a masked completion is outside its argument. The +normal form here puts every one-term E-graph completion next to a classical +lift, except for a one-port retuning along the port's own row. That parallel +line is bounded directly. The non-parallel line quotes the classical floor +and does not replay its sign census. + +## Scope + +Catalogue card `complex-masked-decoder`, scope **refined**. Selector nonce +`9ea1268e3ca1bd3df643b60bf3142efd`, track `complex-mechanisms`, priority +revision 2. Base commit `ef5f39403610d231a0c27e8a6b4f08c10209bcd6`. + +The card asks whether one specified masked or overcomplete decoder can +improve the complete moment budget. The family actually proved is narrower: +eight fixed coordinate readers, one extra term, exactness only on the P112 +E-graph, and cost equal to the pairing-rank sum. The eight-term all-pairs +search is not repeated. Frames, restoration, hosting, precision, and +all-size analytic obligations were not priced. They were treated as zero, +and the copy-rank sum still does not drop. + +A cheaper fully realized decoder could still move the binding complex side. +This family does not. It is a side constraint on one decoder shape, not a +new supplier and not a change to the selected record. + +## Evidence + +The argument is in [PROOF.md](PROOF.md). The finite census is +[verify.py](verify.py): 3,304 E-pair intersections of rank 8, 2,912 odd +pairs of rank 6, 2,040 star codewords, 112 label-critical rows, 448 active +odd-closure codewords, and five mutation controls. Two algebraic fixtures +are included. One meets 64 and is not all-pairs exact. The other is an +E-graph deformation whose coordinate costs are `[7,8,8,8,8,8,8,8]` and +whose total is 71. + +Checks that name an inherited sentence only confirm that the pinned file +still contains it. They are not a replay of that proof. + +Overlap refreshed 2026-10-21 against 458 open PRs and 3,225 discussions. +Nearby results are different objects: the classical all-pairs lift, free +odd rectangles mixed into one coordinate, two-column masked Gram +completions and their COPY-power screens, and trimmed-star or rank-8 +rigidity censuses. No match was a fixed eight-reader, one-extra-term, +E-graph-only pairing-rank floor. That search is not a novelty certificate. + +## Reproduce + +Python 3.12, standard library only. From the repository root: + +```sh +python3 scripts/research_package.py --package research/p112-masked-fixed-reader-lift --check-only +python3.12 scripts/research_package.py --package research/p112-masked-fixed-reader-lift +``` + +Expected final line of the package verifier: + +```text +PASS_P112_MASKED_FIXED_READER_LIFT floor=64 readers=coordinate extra-terms=1 mask=E-graph e-pairs=3304 codewords=2040 critical=112 active-closure=448 inactive-closure=448 controls=5 +``` + +`PYTHONOPTIMIZE` must be unset. The script raises on failure, so `python -O` +cannot skip a broken check. No artifact-regenerating suite was run beside +this verifier. + +## Open next questions + +1. **Two extra terms with the same fixed readers.** The one-term normal form + uses a single reader, so two source supports can carry two vectors even + when each codeword has only one odd neighbor. A first step is to fix two + odd-disjoint star codewords, give each its own reader, and price the sum. + The blocker is that the rank-8 intersection argument no longer forces + those readers to be the same classical column. + +2. **Replacing one coordinate reader instead of only adding a term.** + Uniqueness of the neighborhood vector `a(j)` uses the fixed columns of + `X`. A first step is to delete one star, let that reader be an arbitrary + real vector, and rerun the neighborhood rank. The blocker is that the + coordinate frame is an input to the normal form, not a conclusion. + +## Attribution and discussion access + +Coordinate cost 64 belongs to Joel Pulikkan / GamingPuzzled, PR620. The P112 +E-graph model belongs to DreamingOfClouds, PR717. The classical single-lift +floor belongs to Mihir Srivastava, `research/p112-single-lift`. The card's +starting points are `research/complex-decoder-field-extension-seed44` and +`research/complex-frame-pair-decoders`; their eight-term all-pairs floor is +not re-opened here. + +Discussion writes to CrocSwap/integer-mult-bounds are forbidden for this +account (`FORBIDDEN` / resource not accessible by integration). No discussion +post was attempted on this run, and none should be retried until that +access changes. + +Prepared by hevlyo. Substantial AI assistance was used for the normal form, +the finite census, the verifier, and the write-up. New work is Apache-2.0. diff --git a/research/p112-masked-fixed-reader-lift/SOURCES.json b/research/p112-masked-fixed-reader-lift/SOURCES.json new file mode 100644 index 0000000000..a310249a6b --- /dev/null +++ b/research/p112-masked-fixed-reader-lift/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "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" + }, + { + "path": "research/p112-single-lift/PROOF.md", + "usage": "input", + "git_blob": "609a2b1f83f17523a570a1a2e1731817c87a587a", + "sha256": "02147aa2a93a449dcbd15886b42d993bd0dbb554d7c15d347a9567fbe2a442e1" + } + ] +} diff --git a/research/p112-masked-fixed-reader-lift/TASK.json b/research/p112-masked-fixed-reader-lift/TASK.json new file mode 100644 index 0000000000..fc03ada8b6 --- /dev/null +++ b/research/p112-masked-fixed-reader-lift/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "complex-masked-decoder", + "priority_revision": 2, + "base_commit": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "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": "With the eight P112 coordinate readers fixed, does one extra term that is required to match X X^T only on the E-graph have pairing-rank copy cost at least 64?", + "scope_change_reason": "The card asks whether some masked or overcomplete decoder improves the full moment budget. This package keeps the coordinate readers, weakens all-pairs exactness to the E-graph, and prices the one extra term by pairing rank. It does not repeat the excluded eight-term all-pairs search.", + "bottleneck_link": "A cheaper fully realized decoder could increase deficit or lower recursive cost on the binding complex side. This masked one-term family does not lower the copy-rank sum, so it does not move that side.", + "budget_minutes": 60, + "stop_rule": "The finite census and the one-term normal form are complete. The run stops on that negative result rather than on a timeout.", + "outcome": "negative-result", + "evidence": "research/p112-masked-fixed-reader-lift/verify.py prints PASS_P112_MASKED_FIXED_READER_LIFT. PROOF.md records the normal form, the reduction to the pinned classical floor, and the self-contained parallel line.", + "author": "hevlyo", + "ai_assistance": "Substantial AI assistance was used for the normal form, the finite census, the verifier, and the write-up.", + "open_questions": [ + { + "question": "With the same eight coordinate readers fixed, can two extra E-graph terms have pairing-rank sum below 64?", + "why_it_matters": "A second reader can carry a second vector on a second codeword. The one-term intersection argument does not forbid that, and a drop would be a masked decoder outside this theorem.", + "first_step": "Fix two odd-disjoint star codewords, assign each a reader vector, and compute the pairing-rank sum on that support.", + "blocked_by": "Rank-8 agreement of E-neighborhoods forces one vector only inside a single reader's support." + }, + { + "question": "Does the floor survive if one coordinate reader is replaced instead of being held fixed while a term is added?", + "why_it_matters": "Uniqueness of the neighborhood vector uses the fixed columns of X. Replacing a reader is a different masked family and could change the copy sum.", + "first_step": "Delete one star, let that reader be an arbitrary real vector, and rerun the neighborhood rank count.", + "blocked_by": "The coordinate frame is an input to the normal form, not a consequence of it." + } + ] +} diff --git a/research/p112-masked-fixed-reader-lift/VERIFY.json b/research/p112-masked-fixed-reader-lift/VERIFY.json new file mode 100644 index 0000000000..64110eff9c --- /dev/null +++ b/research/p112-masked-fixed-reader-lift/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p112-single-lift/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 90, + "checks": "Pins the classical floor text, then checks E-graph rank, star-code signature, odd-closure kernels, label criticality, the cost-64 masked fixture, one E-graph deformation, and five mutation controls." + } + ] +} diff --git a/research/p112-masked-fixed-reader-lift/verify.py b/research/p112-masked-fixed-reader-lift/verify.py new file mode 100644 index 0000000000..88e00dcfa4 --- /dev/null +++ b/research/p112-masked-fixed-reader-lift/verify.py @@ -0,0 +1,568 @@ +#!/usr/bin/env python3 +"""P112 E-graph lift with fixed coordinate readers and one extra term. + +Copy-rank sum is at least 64. Standard library only. Exact integer rank, +with rational kernels only on the 7-row bases that meet corank 1. +Assertions raise SystemExit, so python -O cannot skip a failed check. +""" +import hashlib +import itertools +import json +import math +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +NPORTS = 112 +FULL = (1 << NPORTS) - 1 + + +def die(tag, detail=""): + raise SystemExit("FAIL " + tag + ((" | " + detail) if detail else "")) + + +def check(tag, cond, detail=""): + if not cond: + die(tag, detail) + print("PASS " + tag + ((" | " + detail) if detail else ""), flush=True) + + +def e8_lines(): + roots = [] + for i, j in itertools.combinations(range(8), 2): + for si in (1, -1): + for sj in (1, -1): + v = [0] * 8 + v[i], v[j] = 2 * si, 2 * sj + roots.append(tuple(v)) + for s in itertools.product((1, -1), repeat=8): + if s.count(-1) % 2 == 0: + roots.append(tuple(s)) + lines, seen = [], set() + for r in roots: + key = r if r > tuple(-a for a in r) else tuple(-a for a in r) + if key not in seen: + seen.add(key) + lines.append(r) + return lines + + +def ip(x, y): + d = sum(a * b for a, b in zip(x, y)) + if d % 4: + die("model.ip-scale", str(d)) + return d // 4 + + +# Entries of X are 0 or ±1, so every 8×8 minor has absolute value at most +# 8**(8/2) = 4096. Rank over Q therefore agrees with rank modulo any larger prime. +MOD = 65537 + + +def rank_int(rows): + basis = [] + for row in rows: + v = [int(x) % MOD for x in row] + for piv, b in basis: + f = v[piv] + if f: + v = [(x - f * b[c]) % MOD for c, x in enumerate(v)] + piv = next((c for c in range(8) if v[c]), None) + if piv is None: + continue + inv = pow(v[piv], -1, MOD) + basis.append((piv, [(x * inv) % MOD for x in v])) + if len(basis) == 8: + break + return len(basis) + + +def independent_rows(rows, need): + basis = [] + kept = [] + for row in rows: + original = tuple(int(x) for x in row) + v = [x % MOD for x in original] + for piv, b in basis: + f = v[piv] + if f: + v = [(x - f * b[c]) % MOD for c, x in enumerate(v)] + piv = next((c for c in range(8) if v[c]), None) + if piv is None: + continue + inv = pow(v[piv], -1, MOD) + basis.append((piv, [(x * inv) % MOD for x in v])) + kept.append(original) + if len(kept) == need: + break + return kept + + +def kernel_vector(rows): + """One integer right-kernel vector of a rank-7 integer system.""" + kept = independent_rows(rows, 7) + if len(kept) != 7: + die("kernel.rank", str(len(kept))) + A = [[Q(x) for x in row] for row in kept] + pivots = [] + r = 0 + for c in range(8): + p = next((i for i in range(r, len(A)) if A[i][c] != 0), None) + if p is None: + continue + A[r], A[p] = A[p], A[r] + piv = A[r][c] + A[r] = [x / piv for x in A[r]] + for i in range(len(A)): + if i != r and A[i][c] != 0: + f = A[i][c] + A[i] = [x - f * y for x, y in zip(A[i], A[r])] + pivots.append(c) + r += 1 + free = [c for c in range(8) if c not in pivots] + if len(free) != 1: + die("kernel.corank", str(free)) + fcol = free[0] + vec = [Q(0)] * 8 + vec[fcol] = Q(1) + for i, c in enumerate(pivots): + vec[c] = -A[i][fcol] + den = 1 + for x in vec: + den = math.lcm(den, x.denominator) + return [int(x * den) for x in vec] + + +def parallel_int(vec, row): + seen = None + for c in range(8): + if row[c] == 0: + if vec[c] != 0: + return False + continue + ratio = (vec[c], row[c]) + g = math.gcd(ratio[0], ratio[1]) + ratio = (ratio[0] // g, ratio[1] // g) + if ratio[1] < 0: + ratio = (-ratio[0], -ratio[1]) + if seen is None: + seen = ratio + elif seen != ratio: + return False + return seen is not None + + +def f2_rank(masks): + basis = {} + rank = 0 + for v in masks: + x = v + while x: + h = x.bit_length() - 1 + if h in basis: + x ^= basis[h] + else: + basis[h] = x + rank += 1 + break + return rank + + +def f2_basis(masks): + basis = {} + for v in masks: + x = v + while x: + h = x.bit_length() - 1 + if h in basis: + x ^= basis[h] + else: + basis[h] = x + break + return list(basis.values()) + + +def span_from_basis(basis): + out = [0] + for b in basis: + # Snapshot the current block. A generator would see the items it appends. + out.extend([z ^ b for z in out]) + return out + + +def bits(mask): + while mask: + bit = mask & -mask + yield bit.bit_length() - 1 + mask ^= bit + + +def pair_rank(lab, rows, cols): + if rows == 0 or cols == 0: + return 0 + return f2_rank(lab[i] & cols for i in bits(rows)) + + +def component_sizes(mask, lab): + left = mask + sizes = [] + while left: + seen = 0 + stack = left & -left + while stack: + bit = stack & -stack + stack ^= bit + if seen & bit: + continue + seen |= bit + i = bit.bit_length() - 1 + stack |= lab[i] & mask & ~seen + sizes.append(seen.bit_count()) + left &= ~seen + sizes.sort() + return tuple(sizes) + + +def common_odd_mask(mask, lab): + out = 0 + for i in range(NPORTS): + if ((mask >> i) & 1) == 0 and (lab[i] & mask) == 0: + out |= 1 << i + return out + + +def build(): + lines = e8_lines() + if len(lines) != 120: + die("model.lines", str(len(lines))) + ipm = [[ip(lines[i], lines[j]) for j in range(120)] for i in range(120)] + frame = [] + for a in range(4): + for s in (1, -1): + v = [0] * 8 + v[2 * a], v[2 * a + 1] = 2, 2 * s + frame.append(lines.index(tuple(v))) + frame_set = set(frame) + ports = [i for i in range(120) if i not in frame_set] + if len(frame) != 8 or len(ports) != NPORTS: + die("model.frame") + X = [tuple(ipm[ports[p]][frame[k]] for k in range(8)) for p in range(NPORTS)] + lab = [0] * NPORTS + for i in range(NPORTS): + m = 0 + for j in range(NPORTS): + if ((ipm[ports[i]][ports[j]] + 1) & 1) == 1: + m |= 1 << j + lab[i] = m + stars = [0] * 8 + for k in range(8): + m = 0 + for i in range(NPORTS): + if X[i][k] != 0: + m |= 1 << i + stars[k] = m + return X, lab, stars + + +def star_code_masks(star, lab): + ports = list(bits(star)) + pos = {p: i for i, p in enumerate(ports)} + rows = [] + for i in ports: + m = 0 + for j in bits(lab[i] & star): + m |= 1 << pos[j] + rows.append(m) + basis = f2_basis(rows) + if len(basis) != 8: + die("code.dimension", str(len(basis))) + space = span_from_basis(basis) + out = [] + for vec in space: + if vec == 0: + continue + g = 0 + for i in range(len(ports)): + if (vec >> i) & 1: + g |= 1 << ports[i] + out.append(g) + return out + + +def gram(X, i, j): + return sum(X[i][k] * X[j][k] for k in range(8)) + + +def main(): + pin = json.loads((HERE / "SOURCES.json").read_text()) + proof_row = next(r for r in pin["files"] if r["path"] == "research/p112-single-lift/PROOF.md") + proof = (ROOT / proof_row["path"]).read_bytes() + check("pin.pr845-proof", hashlib.sha256(proof).hexdigest() == proof_row["sha256"], proof_row["sha256"][:16]) + check( + "pin.pr845-states-floor", + b">= 64" in proof and b"masked completion" in proof, + "inherited classical floor; masked completions stay outside that proof", + ) + + X, lab, stars = build() + check("model.lines-frame", True, "120 lines, P112 = 112, coordinate frame 8") + check( + "model.row-weight", + all(sum(x != 0 for x in row) == 4 and all(x in (-1, 0, 1) for x in row) for row in X), + "four nonzeros per row, entries in {-1,0,1}; modular rank uses this Hadamard bound", + ) + check("model.star-size", [m.bit_count() for m in stars] == [56] * 8, "eight stars of size 56") + e_off = diag = odd_nz = True + ones = 0 + for i in range(NPORTS): + if lab[i].bit_count() != 60 or gram(X, i, i) != 4: + diag = False + for j in bits(lab[i]): + ones += 1 + if i != j and gram(X, i, j) != 0: + e_off = False + if (lab[i] >> j) & 1 != (lab[j] >> i) & 1: + die("model.dot-symmetry") + for j in bits(FULL ^ lab[i]): + if gram(X, i, j) == 0: + odd_nz = False + check("model.e-graph-target", e_off and diag and odd_nz and ones == 112 * 60, + "M4 is 4I on the E-graph and nonzero off it") + check("model.label-rank", f2_rank(lab) == 9, "label pairing has F2 rank 9") + + e_pairs = odd_pairs = 0 + for j in range(NPORTS): + for jp in range(j + 1, NPORTS): + inter = lab[j] & lab[jp] + rk = rank_int(X[i] for i in bits(inter)) + if (lab[j] >> jp) & 1: + e_pairs += 1 + if rk != 8: + die("nbhd.e-intersection-rank-8", "pair %d %d rank %d" % (j, jp, rk)) + else: + odd_pairs += 1 + if rk != 6: + die("nbhd.odd-intersection-rank-6", "pair %d %d rank %d" % (j, jp, rk)) + check("nbhd.e-intersection-rank-8", e_pairs == 3304, "all %d E-pairs" % e_pairs) + check("nbhd.odd-intersection-rank-6", odd_pairs == 2912, "sharpness: odd pairs are rank 6") + for v in range(NPORTS): + rows = [X[i] for i in bits(lab[v] ^ (1 << v))] + if rank_int(rows) != 7 or any(gram(X, i, v) != 0 for i in bits(lab[v] ^ (1 << v))): + die("nbhd.off-diagonal-rank-7", "v %d" % v) + check("nbhd.off-diagonal-rank-7", True, "N(v) without v is an X[v]-perp of rank 7") + + signature = {} + fixture = None + active_closure = inactive_closure = 0 + for k, star in enumerate(stars): + masks = star_code_masks(star, lab) + if len(masks) != 255: + die("code.count", "star %d has %d" % (k, len(masks))) + for supp in masks: + comp = component_sizes(supp, lab) + odd = common_odd_mask(supp, lab) + signature[(supp.bit_count(), comp, odd.bit_count())] = ( + signature.get((supp.bit_count(), comp, odd.bit_count()), 0) + 1 + ) + if odd.bit_count() == 1 and (supp & odd) == 0: + v = odd.bit_length() - 1 + odd_v = common_odd_mask(1 << v, lab) + if supp & ~odd_v: + die("normal.not-in-odd-neighborhood", "star %d weight %d" % (k, supp.bit_count())) + union = 0 + for w in bits(supp): + union |= lab[w] + cover = lab[v] & union + if rank_int(X[i] for i in bits(cover)) != 7: + die("normal.joint-kernel", "star %d v %d" % (k, v)) + if any(gram(X, i, v) != 0 for i in bits(cover)): + die("normal.joint-orth", "star %d v %d" % (k, v)) + if pair_rank(lab, odd_v, supp) != 7: + die("closure.odd-reader-rank", "star %d v %d" % (k, v)) + if X[v][k] != 0: + if supp.bit_count() != 28: + die("closure.active-weight", str(supp.bit_count())) + if odd_v & ~union: + die("closure.odd-uncovered", "star %d v %d" % (k, v)) + if any(gram(X, i, v) == 0 for i in bits(odd_v)): + die("closure.odd-gram", "v %d" % v) + active_closure += 1 + if fixture is None: + fixture = (k, supp, v) + else: + if supp.bit_count() != 24: + die("closure.inactive-weight", str(supp.bit_count())) + inactive_closure += 1 + expected = { + (28, (28,), 0): 576, + (32, (32,), 0): 504, + (28, (28,), 1): 448, + (24, (24,), 1): 448, + (24, (24,), 0): 56, + (56, (56,), 0): 8, + } + check("code.signature", signature == expected and sum(signature.values()) == 2040, + "2040 supports, all E-connected, at most one odd neighbor") + check( + "normal.joint-kernel", + active_closure == 448 and inactive_closure == 448 and fixture is not None, + "896 odd-neighbor codewords, joint corank 1; 448 active weight-28 and 448 inactive weight-24", + ) + + redundant = 0 + for k, star in enumerate(stars): + for v in bits(star): + en = star & lab[v] & ~(1 << v) + if en.bit_count() != 27: + die("redundancy.degree", "star %d v %d" % (k, v)) + alone = pair_rank(lab, star, 1 << v) + base = pair_rank(lab, star, en) + both = pair_rank(lab, star, en | (1 << v)) + if not (alone == 1 and base == 7 and both == 7): + die("redundancy.column", "star %d v %d" % (k, v)) + odd = common_odd_mask(1 << v, lab) + if en & odd: + die("redundancy.odd-disjoint") + redundant += 1 + check("redundancy.e-neighbor-columns", redundant == 448, + "each star point is redundant beside its 27 E-neighbors") + + basis = f2_basis(lab) + if len(basis) != 9: + die("critical.basis") + parallel_meet = skew_orth = high = 0 + for mask in range(1, 512): + q = 0 + for b in range(9): + if (mask >> b) & 1: + q ^= basis[b] + active = [i for i in bits(q)] + active_mask = q + for v in active: + corank = 8 - rank_int(X[i] for i in bits(active_mask ^ (1 << v))) + if corank > 1: + high += 1 + elif corank == 1: + vec = kernel_vector(X[i] for i in bits(active_mask ^ (1 << v))) + meet = sum(vec[c] * X[v][c] for c in range(8)) != 0 + if meet: + if not parallel_int(vec, X[v]): + die("critical.skew-meet", "v %d" % v) + parallel_meet += 1 + else: + skew_orth += 1 + elif corank < 0: + die("critical.rank") + check("critical.only-row-parallel", high == 0 and parallel_meet == 112 and skew_orth == 448, + "112 row-parallel witnesses; 448 skew kernels miss the port") + + k0, supp, v = fixture + odd = common_odd_mask(1 << v, lab) + if supp & ~odd: + die("fixture.selection") + reader = odd + for k in range(8): + if pair_rank(lab, stars[k], stars[k]) != 8: + die("fixture.coordinate-beta") + extra = pair_rank(lab, reader, 1 << v) + check("fixture.masked-cost-64", extra == 0, "eight stars at 8 and a cost-free odd reader") + # d[i] = 0 on N(v) and d[i] = M4[i,v] on the odd neighborhood. Column v of + # XX^T + d e_v^T therefore matches M4 on the E-graph and doubles off it. + e_ok = True + full_fail = False + for i in range(NPORTS): + on_edge = ((lab[v] >> i) & 1) == 1 + d_i = 0 if on_edge else gram(X, i, v) + value = gram(X, i, v) + d_i + if on_edge: + if d_i != 0 or value != gram(X, i, v): + e_ok = False + elif d_i == 0 or value == gram(X, i, v): + e_ok = False + else: + full_fail = True + check("fixture.e-graph-exact", e_ok, "d vanishes on N(v), so column v matches M4 there") + check("fixture.not-all-pairs", full_fail, "every odd entry of column v is nonzero and doubles") + + a = X[v] + if a[k0] == 0: + die("fixture.deformation-coordinate") + t = {j: Q(X[j][k0], a[k0]) for j in bits(supp)} + t[v] = Q(1) + lam = Q(1) + betas = [] + for k in range(8): + column = 0 + for j in range(NPORTS): + if j == v: + coeff = a[k] + lam * X[v][k] + val = X[j][k] - t[v] * coeff + elif j in t: + val = X[j][k] - t[j] * a[k] + else: + val = X[j][k] + if val != 0: + column |= 1 << j + betas.append(pair_rank(lab, stars[k], column)) + drow = [0] * NPORTS + for i in range(NPORTS): + coeff = [a[c] + (lam * X[v][c] if i == v else 0) for c in range(8)] + drow[i] = sum(X[i][c] * coeff[c] for c in range(8)) + dsupp = 0 + for i in range(NPORTS): + if drow[i] != 0: + dsupp |= 1 << i + J = 0 + for j, val in t.items(): + if val != 0: + J |= 1 << j + extra = pair_rank(lab, dsupp, J) + total = sum(betas) + extra + e_identity = True + for j in range(NPORTS): + tj = t[j] if j in t else Q(0) + for i in bits(lab[j]): + acc = 0 + for k in range(8): + if j == v: + sk = X[j][k] - tj * (a[k] + lam * X[v][k]) + elif j in t: + sk = X[j][k] - tj * a[k] + else: + sk = X[j][k] + acc += X[i][k] * sk + if tj != 0: + if i == v: + di = sum(X[v][c] * (a[c] + lam * X[v][c]) for c in range(8)) + else: + di = sum(X[i][c] * a[c] for c in range(8)) + acc += di * tj + if acc != gram(X, i, j): + e_identity = False + break + if not e_identity: + break + check("fixture.deformation-e-exact", e_identity and total >= 64, + "betas %s extra %d total %d" % (betas, extra, total)) + + anchor = next(j for j in range(1, NPORTS) if (lab[0] >> j) & 1) + truncated = [X[i] for i in bits(lab[0] & lab[anchor])][:4] + controls = [ + rank_int(truncated) < 8, + pair_rank(lab, stars[0], 1 << (stars[0] & -stars[0]).bit_length() - 1) < 8, + pair_rank(lab, reader, 1 << v) == 0, + signature.get((23, (23,), 0), 0) == 0, + any(gram(X, i, v) != 0 for i in bits(odd)), + ] + check("controls.reject-mutations", all(controls) and len(controls) == 5, + "truncated intersection, one-point column, free odd reader, no weight-23 word, odd Gram") + print( + "PASS_P112_MASKED_FIXED_READER_LIFT " + "floor=64 readers=coordinate extra-terms=1 mask=E-graph " + "e-pairs=3304 codewords=2040 critical=112 active-closure=448 inactive-closure=448 controls=5" + ) + + +if __name__ == "__main__": + main()