From 210e51410de90e1910c3f9e40cdc3efd6d410a08 Mon Sep 17 00:00:00 2001 From: CodeBuddy WorkBuddy Date: Tue, 8 Sep 2026 23:41:55 +0800 Subject: [PATCH] #673: combinatorial proofs of the #659 five-cell onsets (I1, I2, axis I3/I4 proved; diamond d0(2L)=L*C(2L,L) kills 4*C(2L,4); diamond b*n onset left OPEN with line+plug reading) - notes/wrapping-five-cell-onset-proofs-20260908.md: proofs from geometry only; committed tables and the PR #669 reader used as checks, not proofs. - I1/I2 binomial regimes proved for both geometries (incl. sharpness at N-L). - Axis I3: d0(L)=d1(L)=L (full row/column; white side direct), b*n(2L-1)=L^2 (cross structure). Axis I4 deficit decomposition proved. - Diamond: b*b(2L)=2L proved (straight diagonal lines + sibling-line argument); d0(2L)=L*C(2L,L) proved on the black side, killing #669's 4*C(2L,4) two-point fit (falsified at L=2: 12 != 4). Corrected diamond L=5 prediction: 1260, not 840. - Diamond b*n onset 3L-1 / value 4L^2: geometric reading obtained (full diagonal line + (L-1)-site plug; 2 families x L lines x 2L plugs), exact at L=2,3 by brute force, consistent with committed L=4; general proof OPEN. - scripts/wrapping_onset_proof_checks.py: seconds-scale brute force at committed sizes only (axis L=3,4; diamond L=2,3). No new census, no L=6, no diamond L=5. --- ...rapping-five-cell-onset-proofs-20260908.md | 390 ++++++++++++++++++ results/wrapping-type-census/axis-L3.json | 1 + results/wrapping-type-census/axis-L4.json | 1 + results/wrapping-type-census/axis-L5.json | 243 +++++++++++ results/wrapping-type-census/diamond-L3.json | 1 + .../wrapping-type-census/diamond-L4-k1.json | 153 +++++++ scripts/wrapping_five_cell_reader.py | 118 ++++++ scripts/wrapping_onset_proof_checks.py | 180 ++++++++ 8 files changed, 1087 insertions(+) create mode 100644 notes/wrapping-five-cell-onset-proofs-20260908.md create mode 100644 results/wrapping-type-census/axis-L3.json create mode 100644 results/wrapping-type-census/axis-L4.json create mode 100644 results/wrapping-type-census/axis-L5.json create mode 100644 results/wrapping-type-census/diamond-L3.json create mode 100644 results/wrapping-type-census/diamond-L4-k1.json create mode 100644 scripts/wrapping_five_cell_reader.py create mode 100644 scripts/wrapping_onset_proof_checks.py diff --git a/notes/wrapping-five-cell-onset-proofs-20260908.md b/notes/wrapping-five-cell-onset-proofs-20260908.md new file mode 100644 index 00000000..6a3ac9dc --- /dev/null +++ b/notes/wrapping-five-cell-onset-proofs-20260908.md @@ -0,0 +1,390 @@ +# #673 Combinatorial proofs of the #659 five-cell onsets (2026-09-08) + +Ticket: #673 (parent #650, follow-up to PR #669 / #659). **No new census. No L=6. No diamond L=5. No diamond L=4 enumeration** (diamond L=4 stays at the committed `k`-window tables of PR #657). + +Every claim below is proved from the geometry of the two committed tori as +built by `scripts/matched_torus_reference.py` and classified by +`scripts/torus_homology.py` (`dir0`/`dir1` = winding along the two quotient +generators). The committed tables +(`results/wrapping-type-census/*.json`, PRs #653/#657) and the PR #669 reader +`scripts/wrapping_five_cell_reader.py` are used **only as checks**; no proof +below cites a table entry. An independent brute-force cross-check at committed +sizes (axis L=3,4; diamond L=2,3 — `2^8`, `2^18`, seconds-scale, no new rung) +is provided in `scripts/wrapping_onset_proof_checks.py` (all checks pass; run +instructions at the end). + +Notation as in PR #669: `n×b = neither×both`, `b×n = both×neither`, +`d0 = dir0×dir0`, `d1 = dir1×dir1`, `b×b = both×both`, all at black mass `k`. +`N = L²` (axis) or `2L²` (diamond). + +## 0. Geometry and lemmas + +**Conventions.** Axis torus: sites `(x,y) ∈ (ℤ/L)²`, NN primal edges +`(±1,0),(0,±1)`; `dir0` = x-period `(L,0)`, `dir1` = y-period `(0,L)`. +Diamond torus: coordinates `(u,v) = (x+y, y−x)`, periods `2L` in each of +`u, v`, sites `S = {(u,v) : u ≡ v (mod 2)}`, `N = 2L²`; NN primal edges are +the steps `(1,1)` and `(1,−1)` (each changes both `u` and `v` by ±1); the +white matching lattice adds NNN steps `(2,0)` and `(0,2)`. Quotient +generator 0 = the `u`-period, generator 1 = the `v`-period. + +**Lemma A (straight lines on both tori).** + +- *Axis.* A full row `y = c` is `L` sites joined by `(1,0)` steps and closes + with displacement `(L,0)`: it wraps `dir0` **only**. A full column `x = c` + wraps `dir1` only. +- *Diamond.* A *diagonal line* of slope `(1,1)` is + `𝔡_r = {(u, u+r) ∈ S : u ∈ ℤ/2L}` for fixed even `r = v−u`; it has `2L` + sites, is NN-connected, and closes with displacement `(2L, 2L)` — it wraps + **both** generators (nonzero projection on both periods). Symmetrically + the slope-`(1,−1)` line `𝔞_c = {(u, c−u)}` (fixed even `c = v+u`) has + displacement `(2L, −2L)` and wraps both. **No NN cycle on the diamond torus + winds exactly one generator in a straight line**: a cycle winding dir0 + only has displacement `(2aL, 0)`-type, and since every NN step changes + `v` by ±1, its steps must cancel in `v`: it mixes `(1,1)` and `(1,−1)` + steps. + +**Lemma B (minimum winding mass).** + +- *Axis (black).* A black NN cycle with displacement `(L, m)` has `L + |m|` + steps, each changing `x` by at most 1, hence visits ≥ `L + |m|` distinct + sites. So `k < L` ⇒ black winds neither generator. Equality `k = L` with + dir0 winding forces `m = 0` and all steps `(1,0)`: the set **is** a full + row. +- *Diamond (black).* A black NN cycle with displacement `(2aL, 2bL)` + (its winding numbers) has length ≥ `max(|a|,|b|) · 2L`, with equality iff + every step has the sign pattern of `(a,b)` — i.e. a straight diagonal + line when `ab ≠ 0`, and a *drift-0 mixed cycle* (see §5a) when `ab = 0`. + So `k < 2L` ⇒ black winds neither generator. + +**Lemma C (minimum white winding mass).** The white matching lattice has +extra edges `(2,0)`/`(0,2)` (diamond) or diagonals (axis). Minimum +winding cycles: on axis, a straight line of `L` sites (NN); on diamond, an +NNN chain `L` sites long (`(2,0)` steps along a `v = const` line) winding +one generator, or a straight NN diagonal of `2L` sites winding both. Hence +white with `< L` sites (axis) or `< L` sites via NNN / `< 2L` via NN (diamond) +still cannot wind carelessly — the precise bounds used below are stated +where needed. + +**Lemma D (MZ pairing; the cells' meaning).** The joint (black primal, +white matching) wrap types are supported on the five Mertens–Ziff cells with +the pairing already committed in this repo (PR #653 note; Mertens–Ziff PRE +94, 062152 (2016), eqs. (9)–(11), (19)): black-neither ⇔ white-both (`n×b`); +black-both ⇒ white-neither (`b×n`) or white-both (`b×b`); black exactly-dir0 +⇔ white exactly-dir0 (`d0`); black exactly-dir1 ⇔ white exactly-dir1 (`d1`). +The note uses this pairing for cell bookkeeping; the *black-side* structure +is proved directly, and the white sides of the axis proofs are also proved +directly (barrier arguments), so duality is imported only as bookkeeping. + +**Counting convention.** At mass `k`, a cell's count is the number of +`k`-subsets whose type pair is that cell; `C(N,k)` is the row sum. + +--- + +## 1. I1 — low-`k` binomial regime (PROVED) + +**Claim (axis).** `n×b(k) = C(L², k)` for `k < L`. +**Claim (diamond).** `n×b(k) = C(2L², k)` for `k < 2L`. + +**Proof.** By Lemma B, a black set of size below the respective threshold +wraps neither generator. By Lemma D, its cell is `n×b`, and every `k`-subset +is counted. ∎ + +The thresholds are sharp: at `k = L` (axis) a full row exists (Lemma A), at +`k = 2L` (diamond) a diagonal line or drift-0 cycle exists (§5), so the +first deficit occurs exactly at the threshold. That the deficit at the +threshold is *exactly* the `d0`+`d1` onset mass is §3/§4/§5. + +## 2. I2 — high-`k` binomial regime (PROVED) + +**Claim (both geometries).** `b×n(k) = C(N,k)` for `k ≥ N − L + 1`, and +`b×n(N − L) < C(N, N − L)` strictly. + +Note the threshold is `L`-governed on **both** geometries — on the diamond +this is because the complement is small (`≤ L−1` sites), not because the +diamond's own line length is `2L`. + +**Proof.** Let black have `k ≥ N − L + 1`, so white has `≤ L − 1` sites. + +*Black wraps both.* Missing sites: ≤ `L−1`. On the axis torus there are `L` +rows and `L` columns; making **all** `L` rows non-full requires ≥ `L` +missing sites, so some row is fully black (wraps dir0, Lemma A) and +symmetrically some column (dir1). On the diamond torus there are `2L` +slope-`(1,1)` lines and `2L` slope-`(1,−1)` lines; making all `2L` lines of +one family non-full requires ≥ `2L > L − 1` missing sites, so some +`(1,1)`-line and some `(1,−1)`-line are fully black — each wraps **both** +generators (Lemma A). In both geometries black wraps both directions. + +*White wraps neither.* White has `≤ L − 1` sites. On axis, any winding NN +cycle has ≥ `L` sites (Lemma B). On diamond, a matching-lattice winding +cycle with displacement `(2aL, 2bL)`, `(a,b) ≠ (0,0)`: each NN step changes +`u` by ±1 and each NNN step by ±2, so the cycle has `u`-extent ≥ `|a|·2L` +covered by ≥ `|a|·L` NNN steps... precisely: the cycle needs ≥ `|a|·L + |b|·L` +edges (each edge advances `u` by ≤ 2), hence ≥ `L·(|a|+|b|) ≥ L` distinct +sites. With `≤ L−1` sites, white wraps neither. + +By Lemma D the cell is `b×n` and the count is `C(N,k)`. ∎ + +**Sharpness at `k = N − L`.** Take white = one full straight line: axis, a +full row (`L` sites, NN-connected, displacement `(L,0)`, wraps dir0); +diamond, a full `(1,−1)`-line `𝔞_c` (`2L` sites, NN-connected, wraps both — +but at minimum it wraps dir0 and dir1 both, which already excludes the +`b×n` cell). Black = complement does not enter the argument: white wraps +something, so the cell is not `b×n` (Lemma D), while §1-style counting +still leaves `C(N,k)` subsets total. Hence strict inequality. ∎ + +## 3. Axis I3 — onset values (PROVED) + +### 3a. `d0(L) = d1(L) = L` + +**Proof (black side).** Let `B`, `|B| = L`, wrap dir0 and not dir1. By +Lemma B (equality case), `B` **is** a full row `y = c`. A full row is a +single `(L,0)` cycle: black type is exactly dir0. + +**Proof (white side, direct).** White = torus minus row `y = c`. + +- *White does not wind dir1.* Any white NN or diagonal-matching path + (axis matching edges: `(1,0),(0,1),(1,1),(1,−1)`, each with `|Δy| ≤ 1`) + with net `y`-displacement `L` visits some site of every row, in + particular row `y = c` — entirely black. Contradiction. +- *White does wind dir0.* Row `y = c + 1` is fully white and closes with + displacement `(L, 0)`. + +So white is exactly-dir0 and the configuration is in cell `d0`. The `L` +choices of `c` give `d0(L) = L`. Exchanging the generator labels +(`(x,y) → (y,x)`, an automorphism of the axis torus commuting with both +classifications) gives `d1(L) = L` (full columns). ∎ + +### 3b. `b×n(2L−1) = L²` and `b×n(k) = 0` for `k < 2L−1` + +**Proof (onset).** Black wraps both directions ⇒ black contains a +dir0-winding cycle (≥ `L` sites) and a dir1-winding cycle (≥ `L` sites). +If they lie in different components, `|B| ≥ 2L`; if in one component, the +two cycles share ≥ 1 site, so `|B| ≥ 2L − 1`. Hence black-both requires +`k ≥ 2L − 1`, proving `b×n(k) = 0` (and `b×b(k) = 0`) below the onset. + +**Proof (value and structure at `k = 2L−1`).** The bounds above must all be +tight: one black component containing a dir0 cycle with exactly `L` sites +and a dir1 cycle with exactly `L` sites, sharing exactly one site. By +Lemma B equality cases, the dir0 cycle is a full row and the dir1 cycle is +a full column; sharing one site means black = row `y = c` ∪ column +`x = c'` (a *cross*, `2L − 1` sites). + +*White side (direct).* White = complement of the cross, `(L−1)²` sites. +Any white winding path must cross the missing row *and* the missing column +(its `y`-coordinate sweeps all residues, hitting row `c`; similarly `x`), +but every step has `|Δx| ≤ 1, |Δy| ≤ 1` (axis matching edges), so a +dir1-winding path must **stand on** row `c` at some step — impossible; a +dir0-winding path must stand on column `c'` — impossible. White wraps +neither. Cell: `b×n`. Count: `L` rows × `L` columns = `L²`. ∎ + +*(Consistency: `b×b(2L−1) = 0` follows — the cross's white complement is +barrier-bounded in both directions, so no white winding of any kind.)* + +## 4. Axis I4 — pre-both-wrap deficit decomposition (PROVED) + +**Claim.** For `L ≤ k < 2L−1` (axis): `C(N,k) − n×b(k) = d0(k) + d1(k)`. + +**Proof.** The five-cell row sum (Lemma D bookkeeping) reads +`C(N,k) = n×b + b×n + d0 + d1 + b×b`. By §3b's onset proof, +`b×n(k) = b×b(k) = 0` on this window (black-both needs `≥ 2L − 1` sites). +Hence the deficit `C(N,k) − n×b(k)` is exactly `d0 + d1`. ∎ + +Combined with §3a, the first deficit at `k = L` is exactly `2L`. +(Checks: axis L=3: `C(9,3) − 78 = 6`; L=4: `C(16,4) − 1812 = 8`; L=5: +`C(25,5) − 12650 = 10` — all `= 2L`. Table check only.) + +--- + +## 5. Diamond I3 + +The diamond geometry differs from the axis in one decisive way (Lemma A): +**a straight diagonal line winds both generators**, and single-generator +winding at minimal mass is carried by *drift-0 mixed cycles*, not lines. + +### 5a. `d0(2L)` — closed form `L·C(2L,L)` (PROVED; #669's `4·C(2L,4)` KILLED) + +**Theorem 5a.** `d0(2L) = d1(2L) = L·C(2L, L)`. + +**Proof.** Let `B`, `|B| = 2L`, wrap dir0 and not dir1. Then `B` contains a +black NN cycle with displacement `(2aL, 0)`, `a ≠ 0` (and no cycle with +`b ≠ 0`). Such a cycle has length ≥ `2L|a| ≥ 2L` = `|B|`, so `a = 1` and +`B` is a single simple cycle of exactly `2L` steps `s_0, …, s_{2L−1}` with +each `s_i ∈ {(1,1), (1,−1)}` (every NN step has `Δu = +1` after choosing +direction — net `Δu = 2L` forces all steps to advance `u`; net `Δv = 0` +forces exactly `L` steps of each type) — the *drift-0* cycles of Lemma B. + +*Enumerate them.* Because every step advances `u` by exactly `+1`, the +cycle visits each `u`-residue exactly once: `B = {(u, v_u) : u ∈ ℤ/2L}` +with `v_{u+1} − v_u ∈ {+1, −1}` for all `u` (cyclically). Conversely any +function `v: ℤ/2L → ℤ/2L` with `v_{u+1} − v_u ∈ {±1}` and `∑(v_{u+1}−v_u) +≡ 0` (automatic) gives such a cycle **provided the sites are valid**: +`u ≡ v (mod 2)` for every site, i.e. `v_u ≡ u (mod 2)` for all `u`. Since +`v_{u+1} − v_u = ±1` alternates the parity of `v` exactly as `u` does, the +parity constraint reduces to `v_0 ≡ 0 (mod 2)`: `L` choices of `v_0`. +Given `v_0`, the cycle is determined by the *step word* +`w ∈ {+1, −1}^{2L}` with exactly `L` of each — `C(2L, L)` choices. The map +`(v_0, w) ↦ {(u, v_0 + w-prefix(u))}` is a bijection onto the dir0-winding +`2L`-site black cycles (distinct pairs give distinct site sets, since +`v_0` and all prefixes are recoverable from the set). Also, a single cycle +with displacement `(2L, 0)` does not wind dir1, so black type is +exactly dir0: there are `L · C(2L, L)` such black sets. + +*White side (direct, mirroring §3a).* Let `B` be such a drift-0 cycle. + +- *White does not wind dir1.* A white winding-dir1 path (matching edges: + `(1,±1)` and `(2,0)`; every edge changes `u` by ±1 or ±2) with net + `v`-displacement `2L` must visit sites of every `v`-residue class... more + carefully: its `v`-coordinate sweeps a connected interval of the + universal cover of length ≥ `2L`, covering all residues `mod 2L`. The + black cycle `B` meets every `v`-residue? Not necessarily — but `B` meets + every **site with `v ≡ v_u` at `u`**: the path needs to *stand on* a site + of the residue class it crosses while `u` also matches... The clean + statement: a dir1-winding path's `v`-coordinate takes every value mod + `2L` **at some visit**, and at that visit the path is on a site + `(u, v)` with that `v`; the black set blocks only *its own* `2L` sites. + This does not immediately forbid the path. **So the white side of the + cell assignment at the onset is the one place duality (Lemma D) is + load-bearing** — as on the axis (§3a) a direct argument exists (the + drift-0 black cycle acts as a "spiral barrier"), but I did not complete + it in this ticket's budget. The black-side count `L·C(2L,L)` is the + geometric content and is proved; the cell bookkeeping `d0` vs `d1` is + by duality + the `(u,v) → (v,u)` automorphism, consistent with the + committed `d0 = d1` fact. + +Hence `d0(2L) = L·C(2L, L)`. ∎ + +**Verification.** L=2: `2·C(4,2) = 12`; L=3: `3·C(6,3) = 60`; L=4: +`4·C(8,4) = 280`. The committed diamond L=3 table has `d0(6) = 60` ✓ and +diamond L=4 has `d0(8) = 280` ✓. Brute force at L=2 gives 12 ✓ +(`scripts/wrapping_onset_proof_checks.py`). + +**This kills #669's two-point fit `d0(2L) = 4·C(2L,4)`:** that form gives +`4·C(4,4) = 4` at L=2 (brute force: 12 — violated), `4·C(6,4) = 60` at L=3 +(✓ coincidentally `4·C(2L,4) = L·C(2L,L)` iff `C(2L,4)·4 = L·C(2L,L)`, which +holds exactly at L=3,4 — the two points #669 had). The correct closed form +is `L·C(2L,L)`; the #669 diamond-L5 prediction for `d0(10)` should be +`5·C(10,5) = 1260`, **not** `840`. The #669 falsification kit entry +"`d0(10) = 840` if I3 extends" must be corrected accordingly: if a future +diamond L=5 run yields `d0(10) = 1260`, the `4·C(2L,4)` conjecture was the +wrong generalization, not the onset. + +### 5b. `b×b(2L) = 2L` (PROVED) + +**Proof.** Let `B`, `|B| = 2L`, wrap both generators. `B` contains a cycle +with displacement `(2aL, 2bL)`, `a,b ≠ 0` (if the two windings lived on +different cycles of different components, `|B| ≥ 4L > 2L`; if one component +held two independent winding cycles, their union has ≥ `2L + 2L − 1 = 4L−1 +> 2L` sites). So a single cycle, length ≥ `2L·max(|a|,|b|) ≥ 2L` with +equality iff `|a| = |b| = 1` and every step is `(1,1)` or every step is +`(1,−1)`: `B` is a straight diagonal line (Lemma A), slope `(1,1)` or +`(1,−1)` — `2L` lines total (`L` even residues of `v−u`, `L` of `v+u`). + +*White side (direct).* Let black be the line `𝔞_c` (slope `(1,−1)`, fixed +`v+u = c`). The **sibling lines** `𝔞_{c'}` for `c' ≠ c` are entirely white +(two distinct slope-`(1,−1)` lines are disjoint — they share no site), and +each closes with displacement `(2L, −2L)`, winding **both** generators. So +white wraps both. (Symmetric for black slope `(1,1)`.) By Lemma D, cell +`b×b`. Count: `2L` lines. And no other black-both set exists at `k = 2L` +(above). ∎ + +**Verification.** diamond L=2: 4; L=3: 6 (committed) ✓; brute force at +L=2,3 confirms every `b×b(2L)` set is a straight diagonal line ✓. + +### 5c. Diamond `b×n` onset `3L−1` with value `4L²` — geometric reading obtained; general proof OPEN + +**Structure (verified exactly at L=2,3 by seconds-scale brute force; +consistent with the committed L=4 count).** At `k = 3L−1`, every `b×n` +configuration is + +> a **full straight diagonal line** (slope `(1,−1)` or `(1,1)`, `2L` sites, +> black-both by Lemma A) **plus `L − 1` extra sites** forming an +> NN-connected "plug" on a single transverse slope-line, each plug site +> NN-adjacent to the full line or to the next plug site. + +At L=2 the plug is a single site (4 positions per anti-line); at L=3 the +plug is a **domino** `{q, q+(1,1)}` with both ends NN-adjacent to the +removed line (6 positions per anti-line: 2 per transverse slope-line × 3). + +**Count reading.** `4L² = 2` (slope families) `× L` (full lines per family) +`× 2L` (plug placements per line). This reproduces `16, 36, 64` at +`L = 2, 3, 4` (the L=4 value is the committed table's). The per-line plug +count `2L` is direct at L=2 (the 4 sites not on the line, each works — +brute force) and L=3 (the 6 dominoes, enumerated above); at general `L` +the plug is an `(L−1)`-site object and the `2L` placements would need a +structural classification of plugs — **this is the missing proof step**. + +**Why the value is plausible (white-side reading).** The full line alone +is `b×b` (§5b): white's sibling lines wind both. Adding the plug on a +transverse line cuts the annulus complement in the transverse direction +as well: white (matching lattice) retains no winding in either generator, +while black still winds both (the line survives) — cell `b×n`. The plug +must simultaneously block the white NNN chains (`(2,0)`/`(0,2)` steps) and +NN detours in both directions; the classification of minimal such plugs +is exactly the `(L−1)`-site structure above. + +**What remains for a proof (OPEN).** + +1. *Onset:* no `b×n` exists for `2L ≤ k < 3L−1` — equivalently, any + black-both set with `k < 3L−1` has white wrapping something (white-both, + i.e. the config is `b×b`). Verified exactly at L=2,3. +2. *Count:* every `b×n(3L−1)` set is line + `(L−1)`-plug, and there are + exactly `2L` plugs per line. Verified exactly at L=2,3; count + consistent at L=4 (committed). + +Both are sharp integer predictions for diamond L=5 in the #669 +falsification kit (§5 of the #669 note): onset `k = 14`, value `100`. +**Until (1)–(2) are proved for general L, the `3L−1`/`4L²` claims remain +two-point (+L=2 brute-force) conjectures.** Do not enumerate diamond L=5 +to settle them. + +--- + +## 6. Summary of proof status + +| Item | Status | Where | +|---|---|---| +| I1 axis `n×b = C(N,k)`, `k < L` | **PROVED** | §1 | +| I1 diamond `k < 2L` | **PROVED** | §1 | +| I2 `b×n = C(N,k)`, `k ≥ N−L+1`, both geometries, strict at `N−L` | **PROVED** | §2 | +| Axis I3 `d0(L) = d1(L) = L` (full rows/columns; white side direct) | **PROVED** | §3a | +| Axis I3 `b×n(2L−1) = L²`, onset, cross structure | **PROVED** | §3b | +| Axis I4 deficit `= d0 + d1` on `L ≤ k < 2L−1` | **PROVED** | §4 | +| Diamond `d0(2L) = L·C(2L,L)` (black side proved; #669's `4·C(2L,4)` killed) | **PROVED** (black side; white cell-assignment by duality) | §5a | +| Diamond `b×b(2L) = 2L` (straight diagonal lines; white sibling-lines argument) | **PROVED** | §5b | +| Diamond `b×n` onset `3L−1`, value `4L²` | **OPEN** (geometric reading: line + `(L−1)`-plug, count `2·L·2L`; exact at L=2,3, consistent at L=4) | §5c | + +**On `M_L` irreducibility (per the ticket):** the irreducibility of `M_L` +over ℚ at the five committed sizes (PR #669 §4) is recorded as a +**factorization fact**, not a wrapping theorem: no mechanism is known (or +claimed) that forces irreducibility; a reducible case at a future size +would contradict no wrapping statement. Not pursued further per the +ticket. + +## 7. Correction to the #669 falsification kit + +The #669 note's §5 diamond-L=5 predictions contain one entry derived from +the now-dead `4·C(2L,4)` fit: + +- "`d0(10) = 840` if I3 extends" → corrected prediction: + **`d0(10) = L·C(2L,L) = 5·C(10,5) = 1260`** (and `d1(10) = 1260`). +- `b×b(10) = 10` and `b×n` onset `k = 14` value `100` stand as before + (two-point conjectures with the §5c geometric reading). + +A future diamond L=5 rung should be checked against **both** the corrected +`1260` and the old `840` before any conclusion is drawn. + +## 8. Tripwire compliance and reproduction + +- No L=6 enumeration, no diamond L=5 enumeration, no new census rung. +- The only new computation is a seconds-scale brute force at *already + committed or trivially small* sizes (axis L=3,4 = `2^9`,`2^16`; diamond + L=2,3 = `2^8`,`2^18`) using the repo's own classifier: + `python3 scripts/wrapping_onset_proof_checks.py` — all checks pass. + It re-verifies I1, I2 (incl. sharpness), axis I3a/I3b structure, axis I4, + the diamond `d0(2L) = L·C(2L,L)` black-side count, `b×b(2L) = 2L` with + diagonal-line structure, and the diamond I4 window. +- `scripts/wrapping_five_cell_reader.py` (PR #669) re-verifies the + identities on the committed tables; it needs the census JSONs, which + are on the #669 branch — fetched to this branch for the check run. +- The two OPEN items carry sharp integer predictions in the #669 + falsification kit (§5 there, with the §7 correction above). diff --git a/results/wrapping-type-census/axis-L3.json b/results/wrapping-type-census/axis-L3.json new file mode 100644 index 00000000..645a4097 --- /dev/null +++ b/results/wrapping-type-census/axis-L3.json @@ -0,0 +1 @@ +{"tables": {"0": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 1}, "dir0": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "both": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}}, "1": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 9}, "dir0": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "both": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}}, "2": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 36}, "dir0": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "both": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}}, "3": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 78}, "dir0": {"neither": 0, "dir0": 3, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 3, "both": 0}, "both": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}}, "4": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 90}, "dir0": {"neither": 0, "dir0": 18, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 18, "both": 0}, "both": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}}, "5": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 45}, "dir0": {"neither": 0, "dir0": 36, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 36, "both": 0}, "both": {"neither": 9, "dir0": 0, "dir1": 0, "both": 0}}, "6": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir0": {"neither": 0, "dir0": 21, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 21, "both": 0}, "both": {"neither": 36, "dir0": 0, "dir1": 0, "both": 6}}, "7": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir0": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "both": {"neither": 36, "dir0": 0, "dir1": 0, "both": 0}}, "8": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir0": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "both": {"neither": 9, "dir0": 0, "dir1": 0, "both": 0}}, "9": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir0": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "both": {"neither": 1, "dir0": 0, "dir1": 0, "both": 0}}}, "collapsed": [-1, -9, -36, -78, -90, -36, 36, 36, 9, 1], "tripwire": "pass", "committed_bernstein": [-1, -9, -36, -78, -90, -36, 36, 36, 9, 1], "geometry": "axis", "L": 3, "N": 9, "mask_lo": 0, "mask_hi": 512} diff --git a/results/wrapping-type-census/axis-L4.json b/results/wrapping-type-census/axis-L4.json new file mode 100644 index 00000000..55bcaf40 --- /dev/null +++ b/results/wrapping-type-census/axis-L4.json @@ -0,0 +1 @@ +{"tables": {"0": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 1}, "dir0": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "both": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}}, "1": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 16}, "dir0": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "both": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}}, "2": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 120}, "dir0": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "both": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}}, "3": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 560}, "dir0": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "both": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}}, "4": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 1812}, "dir0": {"neither": 0, "dir0": 4, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 4, "both": 0}, "both": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}}, "5": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 4272}, "dir0": {"neither": 0, "dir0": 48, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 48, "both": 0}, "both": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}}, "6": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 7448}, "dir0": {"neither": 0, "dir0": 280, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 280, "both": 0}, "both": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}}, "7": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 9440}, "dir0": {"neither": 0, "dir0": 992, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 992, "both": 0}, "both": {"neither": 16, "dir0": 0, "dir1": 0, "both": 0}}, "8": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 8082}, "dir0": {"neither": 0, "dir0": 2230, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 2230, "both": 0}, "both": {"neither": 208, "dir0": 0, "dir1": 0, "both": 120}}, "9": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 3984}, "dir0": {"neither": 0, "dir0": 2976, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 2976, "both": 0}, "both": {"neither": 1088, "dir0": 0, "dir1": 0, "both": 416}}, "10": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 792}, "dir0": {"neither": 0, "dir0": 2128, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 2128, "both": 0}, "both": {"neither": 2512, "dir0": 0, "dir1": 0, "both": 448}}, "11": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 32}, "dir0": {"neither": 0, "dir0": 672, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 672, "both": 0}, "both": {"neither": 2864, "dir0": 0, "dir1": 0, "both": 128}}, "12": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir0": {"neither": 0, "dir0": 76, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 76, "both": 0}, "both": {"neither": 1660, "dir0": 0, "dir1": 0, "both": 8}}, "13": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir0": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "both": {"neither": 560, "dir0": 0, "dir1": 0, "both": 0}}, "14": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir0": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "both": {"neither": 120, "dir0": 0, "dir1": 0, "both": 0}}, "15": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir0": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "both": {"neither": 16, "dir0": 0, "dir1": 0, "both": 0}}, "16": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir0": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "both": {"neither": 1, "dir0": 0, "dir1": 0, "both": 0}}}, "collapsed": [-1, -16, -120, -560, -1812, -4272, -7448, -9424, -7874, -2896, 1720, 2832, 1660, 560, 120, 16, 1], "tripwire": "pass", "committed_bernstein": [-1, -16, -120, -560, -1812, -4272, -7448, -9424, -7874, -2896, 1720, 2832, 1660, 560, 120, 16, 1], "geometry": "axis", "L": 4, "N": 16, "mask_lo": 0, "mask_hi": 65536} diff --git a/results/wrapping-type-census/axis-L5.json b/results/wrapping-type-census/axis-L5.json new file mode 100644 index 00000000..51d053ed --- /dev/null +++ b/results/wrapping-type-census/axis-L5.json @@ -0,0 +1,243 @@ +{ + "geometry": "axis", + "L": 5, + "N": 25, + "physical_period": "5", + "threads": 14, + "configs_expect": 33554432, + "k1": { + "configs_visited": 33554432, + "wall_seconds": 2.209, + "collapsed_D_per_k": [-1,-25,-300,-2300,-12650,-53120,-176900,-478700,-1068575,-1982325,-3054280,-3863250,-3890950,-2905150,-1290250,128000,765475,709225,406900,168100,52610,12650,2300,300,25,1], + "joint_label_counts_per_k": [ + [0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,25,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,300,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,2300,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,12650,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,53120,0,0,5,0,0,0,0,0,5,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,176900,0,0,100,0,0,0,0,0,100,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,478700,0,0,1000,0,0,0,0,0,1000,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,1068575,0,0,6500,0,0,0,0,0,6500,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,1982350,0,0,30300,0,0,0,0,0,30300,0,0,25,0,0,0,0,0,0,0,0,0], + [0,0,0,3054880,0,0,106185,0,0,0,0,0,106185,0,0,600,0,0,910,0,0,0,0,0,0], + [0,0,0,3869650,0,0,285725,0,0,0,0,0,285725,0,0,6400,0,0,9900,0,0,0,0,0,0], + [0,0,0,3931075,0,0,591150,0,0,0,0,0,591150,0,0,40125,0,0,46800,0,0,0,0,0,0], + [0,0,0,3067350,0,0,923875,0,0,0,0,0,923875,0,0,162200,0,0,123000,0,0,0,0,0,0], + [0,0,0,1723100,0,0,1054375,0,0,0,0,0,1054375,0,0,432850,0,0,192700,0,0,0,0,0,0], + [0,0,0,639850,0,0,840585,0,0,0,0,0,840585,0,0,767850,0,0,179890,0,0,0,0,0,0], + [0,0,0,141575,0,0,448500,0,0,0,0,0,448500,0,0,907050,0,0,97350,0,0,0,0,0,0], + [0,0,0,15900,0,0,155450,0,0,0,0,0,155450,0,0,725125,0,0,29650,0,0,0,0,0,0], + [0,0,0,550,0,0,33950,0,0,0,0,0,33950,0,0,407450,0,0,4800,0,0,0,0,0,0], + [0,0,0,0,0,0,4325,0,0,0,0,0,4325,0,0,168100,0,0,350,0,0,0,0,0,0], + [0,0,0,0,0,0,255,0,0,0,0,0,255,0,0,52610,0,0,10,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,12650,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,2300,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,300,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,25,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0] + ], + "coarse_4x4_counts_per_k": [ + [0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,25,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,300,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,2300,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,12650,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,53120,0,5,0,0,0,0,5,0,0,0,0,0], + [0,0,0,176900,0,100,0,0,0,0,100,0,0,0,0,0], + [0,0,0,478700,0,1000,0,0,0,0,1000,0,0,0,0,0], + [0,0,0,1068575,0,6500,0,0,0,0,6500,0,0,0,0,0], + [0,0,0,1982350,0,30300,0,0,0,0,30300,0,25,0,0,0], + [0,0,0,3054880,0,106185,0,0,0,0,106185,0,600,0,0,910], + [0,0,0,3869650,0,285725,0,0,0,0,285725,0,6400,0,0,9900], + [0,0,0,3931075,0,591150,0,0,0,0,591150,0,40125,0,0,46800], + [0,0,0,3067350,0,923875,0,0,0,0,923875,0,162200,0,0,123000], + [0,0,0,1723100,0,1054375,0,0,0,0,1054375,0,432850,0,0,192700], + [0,0,0,639850,0,840585,0,0,0,0,840585,0,767850,0,0,179890], + [0,0,0,141575,0,448500,0,0,0,0,448500,0,907050,0,0,97350], + [0,0,0,15900,0,155450,0,0,0,0,155450,0,725125,0,0,29650], + [0,0,0,550,0,33950,0,0,0,0,33950,0,407450,0,0,4800], + [0,0,0,0,0,4325,0,0,0,0,4325,0,168100,0,0,350], + [0,0,0,0,0,255,0,0,0,0,255,0,52610,0,0,10], + [0,0,0,0,0,0,0,0,0,0,0,0,12650,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,2300,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,300,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,25,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0] + ], + "D_positive_attribution_per_k": [ + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,5,0,0,0,0,0,5,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,100,0,0,0,0,0,100,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,1000,0,0,0,0,0,1000,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,6500,0,0,0,0,0,6500,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,30300,0,0,0,0,0,30300,0,0,25,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,106185,0,0,0,0,0,106185,0,0,600,0,0,910,0,0,0,0,0,0], + [0,0,0,0,0,0,285725,0,0,0,0,0,285725,0,0,6400,0,0,9900,0,0,0,0,0,0], + [0,0,0,0,0,0,591150,0,0,0,0,0,591150,0,0,40125,0,0,46800,0,0,0,0,0,0], + [0,0,0,0,0,0,923875,0,0,0,0,0,923875,0,0,162200,0,0,123000,0,0,0,0,0,0], + [0,0,0,0,0,0,1054375,0,0,0,0,0,1054375,0,0,432850,0,0,192700,0,0,0,0,0,0], + [0,0,0,0,0,0,840585,0,0,0,0,0,840585,0,0,767850,0,0,179890,0,0,0,0,0,0], + [0,0,0,0,0,0,448500,0,0,0,0,0,448500,0,0,907050,0,0,97350,0,0,0,0,0,0], + [0,0,0,0,0,0,155450,0,0,0,0,0,155450,0,0,725125,0,0,29650,0,0,0,0,0,0], + [0,0,0,0,0,0,33950,0,0,0,0,0,33950,0,0,407450,0,0,4800,0,0,0,0,0,0], + [0,0,0,0,0,0,4325,0,0,0,0,0,4325,0,0,168100,0,0,350,0,0,0,0,0,0], + [0,0,0,0,0,0,255,0,0,0,0,0,255,0,0,52610,0,0,10,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,12650,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,2300,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,300,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,25,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0] + ], + "D_negative_attribution_per_k": [ + [0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-25,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-300,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-2300,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-12650,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-53120,0,0,-5,0,0,0,0,0,-5,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-176900,0,0,-100,0,0,0,0,0,-100,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-478700,0,0,-1000,0,0,0,0,0,-1000,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-1068575,0,0,-6500,0,0,0,0,0,-6500,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-1982350,0,0,-30300,0,0,0,0,0,-30300,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-3054880,0,0,-106185,0,0,0,0,0,-106185,0,0,0,0,0,-910,0,0,0,0,0,0], + [0,0,0,-3869650,0,0,-285725,0,0,0,0,0,-285725,0,0,0,0,0,-9900,0,0,0,0,0,0], + [0,0,0,-3931075,0,0,-591150,0,0,0,0,0,-591150,0,0,0,0,0,-46800,0,0,0,0,0,0], + [0,0,0,-3067350,0,0,-923875,0,0,0,0,0,-923875,0,0,0,0,0,-123000,0,0,0,0,0,0], + [0,0,0,-1723100,0,0,-1054375,0,0,0,0,0,-1054375,0,0,0,0,0,-192700,0,0,0,0,0,0], + [0,0,0,-639850,0,0,-840585,0,0,0,0,0,-840585,0,0,0,0,0,-179890,0,0,0,0,0,0], + [0,0,0,-141575,0,0,-448500,0,0,0,0,0,-448500,0,0,0,0,0,-97350,0,0,0,0,0,0], + [0,0,0,-15900,0,0,-155450,0,0,0,0,0,-155450,0,0,0,0,0,-29650,0,0,0,0,0,0], + [0,0,0,-550,0,0,-33950,0,0,0,0,0,-33950,0,0,0,0,0,-4800,0,0,0,0,0,0], + [0,0,0,0,0,0,-4325,0,0,0,0,0,-4325,0,0,0,0,0,-350,0,0,0,0,0,0], + [0,0,0,0,0,0,-255,0,0,0,0,0,-255,0,0,0,0,0,-10,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0] + ] + }, + "k2": { + "configs_visited": 33554432, + "wall_seconds": 0.536, + "collapsed_D_per_k": [-1,-25,-300,-2300,-12650,-53120,-176900,-478700,-1068575,-1982325,-3054280,-3863250,-3890950,-2905150,-1290250,128000,765475,709225,406900,168100,52610,12650,2300,300,25,1], + "joint_label_counts_per_k": [ + [0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,25,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,300,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,2300,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,12650,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,53120,0,0,5,0,0,0,0,0,5,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,176900,0,0,100,0,0,0,0,0,100,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,478700,0,0,1000,0,0,0,0,0,1000,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,1068575,0,0,6500,0,0,0,0,0,6500,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,1982350,0,0,30300,0,0,0,0,0,30300,0,0,25,0,0,0,0,0,0,0,0,0], + [0,0,0,3054880,0,0,106185,0,0,0,0,0,106185,0,0,600,0,0,910,0,0,0,0,0,0], + [0,0,0,3869650,0,0,285725,0,0,0,0,0,285725,0,0,6400,0,0,9900,0,0,0,0,0,0], + [0,0,0,3931075,0,0,591150,0,0,0,0,0,591150,0,0,40125,0,0,46800,0,0,0,0,0,0], + [0,0,0,3067350,0,0,923875,0,0,0,0,0,923875,0,0,162200,0,0,123000,0,0,0,0,0,0], + [0,0,0,1723100,0,0,1054375,0,0,0,0,0,1054375,0,0,432850,0,0,192700,0,0,0,0,0,0], + [0,0,0,639850,0,0,840585,0,0,0,0,0,840585,0,0,767850,0,0,179890,0,0,0,0,0,0], + [0,0,0,141575,0,0,448500,0,0,0,0,0,448500,0,0,907050,0,0,97350,0,0,0,0,0,0], + [0,0,0,15900,0,0,155450,0,0,0,0,0,155450,0,0,725125,0,0,29650,0,0,0,0,0,0], + [0,0,0,550,0,0,33950,0,0,0,0,0,33950,0,0,407450,0,0,4800,0,0,0,0,0,0], + [0,0,0,0,0,0,4325,0,0,0,0,0,4325,0,0,168100,0,0,350,0,0,0,0,0,0], + [0,0,0,0,0,0,255,0,0,0,0,0,255,0,0,52610,0,0,10,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,12650,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,2300,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,300,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,25,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0] + ], + "coarse_4x4_counts_per_k": [ + [0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,25,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,300,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,2300,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,12650,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,53120,0,5,0,0,0,0,5,0,0,0,0,0], + [0,0,0,176900,0,100,0,0,0,0,100,0,0,0,0,0], + [0,0,0,478700,0,1000,0,0,0,0,1000,0,0,0,0,0], + [0,0,0,1068575,0,6500,0,0,0,0,6500,0,0,0,0,0], + [0,0,0,1982350,0,30300,0,0,0,0,30300,0,25,0,0,0], + [0,0,0,3054880,0,106185,0,0,0,0,106185,0,600,0,0,910], + [0,0,0,3869650,0,285725,0,0,0,0,285725,0,6400,0,0,9900], + [0,0,0,3931075,0,591150,0,0,0,0,591150,0,40125,0,0,46800], + [0,0,0,3067350,0,923875,0,0,0,0,923875,0,162200,0,0,123000], + [0,0,0,1723100,0,1054375,0,0,0,0,1054375,0,432850,0,0,192700], + [0,0,0,639850,0,840585,0,0,0,0,840585,0,767850,0,0,179890], + [0,0,0,141575,0,448500,0,0,0,0,448500,0,907050,0,0,97350], + [0,0,0,15900,0,155450,0,0,0,0,155450,0,725125,0,0,29650], + [0,0,0,550,0,33950,0,0,0,0,33950,0,407450,0,0,4800], + [0,0,0,0,0,4325,0,0,0,0,4325,0,168100,0,0,350], + [0,0,0,0,0,255,0,0,0,0,255,0,52610,0,0,10], + [0,0,0,0,0,0,0,0,0,0,0,0,12650,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,2300,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,300,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,25,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0] + ], + "D_positive_attribution_per_k": [ + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,5,0,0,0,0,0,5,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,100,0,0,0,0,0,100,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,1000,0,0,0,0,0,1000,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,6500,0,0,0,0,0,6500,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,30300,0,0,0,0,0,30300,0,0,25,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,106185,0,0,0,0,0,106185,0,0,600,0,0,910,0,0,0,0,0,0], + [0,0,0,0,0,0,285725,0,0,0,0,0,285725,0,0,6400,0,0,9900,0,0,0,0,0,0], + [0,0,0,0,0,0,591150,0,0,0,0,0,591150,0,0,40125,0,0,46800,0,0,0,0,0,0], + [0,0,0,0,0,0,923875,0,0,0,0,0,923875,0,0,162200,0,0,123000,0,0,0,0,0,0], + [0,0,0,0,0,0,1054375,0,0,0,0,0,1054375,0,0,432850,0,0,192700,0,0,0,0,0,0], + [0,0,0,0,0,0,840585,0,0,0,0,0,840585,0,0,767850,0,0,179890,0,0,0,0,0,0], + [0,0,0,0,0,0,448500,0,0,0,0,0,448500,0,0,907050,0,0,97350,0,0,0,0,0,0], + [0,0,0,0,0,0,155450,0,0,0,0,0,155450,0,0,725125,0,0,29650,0,0,0,0,0,0], + [0,0,0,0,0,0,33950,0,0,0,0,0,33950,0,0,407450,0,0,4800,0,0,0,0,0,0], + [0,0,0,0,0,0,4325,0,0,0,0,0,4325,0,0,168100,0,0,350,0,0,0,0,0,0], + [0,0,0,0,0,0,255,0,0,0,0,0,255,0,0,52610,0,0,10,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,12650,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,2300,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,300,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,25,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0] + ], + "D_negative_attribution_per_k": [ + [0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-25,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-300,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-2300,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-12650,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-53120,0,0,-5,0,0,0,0,0,-5,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-176900,0,0,-100,0,0,0,0,0,-100,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-478700,0,0,-1000,0,0,0,0,0,-1000,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-1068575,0,0,-6500,0,0,0,0,0,-6500,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-1982350,0,0,-30300,0,0,0,0,0,-30300,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-3054880,0,0,-106185,0,0,0,0,0,-106185,0,0,0,0,0,-910,0,0,0,0,0,0], + [0,0,0,-3869650,0,0,-285725,0,0,0,0,0,-285725,0,0,0,0,0,-9900,0,0,0,0,0,0], + [0,0,0,-3931075,0,0,-591150,0,0,0,0,0,-591150,0,0,0,0,0,-46800,0,0,0,0,0,0], + [0,0,0,-3067350,0,0,-923875,0,0,0,0,0,-923875,0,0,0,0,0,-123000,0,0,0,0,0,0], + [0,0,0,-1723100,0,0,-1054375,0,0,0,0,0,-1054375,0,0,0,0,0,-192700,0,0,0,0,0,0], + [0,0,0,-639850,0,0,-840585,0,0,0,0,0,-840585,0,0,0,0,0,-179890,0,0,0,0,0,0], + [0,0,0,-141575,0,0,-448500,0,0,0,0,0,-448500,0,0,0,0,0,-97350,0,0,0,0,0,0], + [0,0,0,-15900,0,0,-155450,0,0,0,0,0,-155450,0,0,0,0,0,-29650,0,0,0,0,0,0], + [0,0,0,-550,0,0,-33950,0,0,0,0,0,-33950,0,0,0,0,0,-4800,0,0,0,0,0,0], + [0,0,0,0,0,0,-4325,0,0,0,0,0,-4325,0,0,0,0,0,-350,0,0,0,0,0,0], + [0,0,0,0,0,0,-255,0,0,0,0,0,-255,0,0,0,0,0,-10,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0] + ] + } + ,"k1_k2_collapsed_agree": true +} diff --git a/results/wrapping-type-census/diamond-L3.json b/results/wrapping-type-census/diamond-L3.json new file mode 100644 index 00000000..c4f73a37 --- /dev/null +++ b/results/wrapping-type-census/diamond-L3.json @@ -0,0 +1 @@ +{"tables": {"0": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 1}, "dir0": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "both": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}}, "1": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 18}, "dir0": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "both": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}}, "2": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 153}, "dir0": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "both": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}}, "3": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 816}, "dir0": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "both": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}}, "4": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 3060}, "dir0": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "both": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}}, "5": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 8568}, "dir0": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "both": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}}, "6": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 18438}, "dir0": {"neither": 0, "dir0": 60, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 60, "both": 0}, "both": {"neither": 0, "dir0": 0, "dir1": 0, "both": 6}}, "7": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 30528}, "dir0": {"neither": 0, "dir0": 612, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 612, "both": 0}, "both": {"neither": 0, "dir0": 0, "dir1": 0, "both": 72}}, "8": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 37674}, "dir0": {"neither": 0, "dir0": 2790, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 2790, "both": 0}, "both": {"neither": 36, "dir0": 0, "dir1": 0, "both": 468}}, "9": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 32360}, "dir0": {"neither": 0, "dir0": 7038, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 7038, "both": 0}, "both": {"neither": 720, "dir0": 0, "dir1": 0, "both": 1464}}, "10": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 17145}, "dir0": {"neither": 0, "dir0": 10350, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 10350, "both": 0}, "both": {"neither": 3609, "dir0": 0, "dir1": 0, "both": 2304}}, "11": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 4716}, "dir0": {"neither": 0, "dir0": 8496, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 8496, "both": 0}, "both": {"neither": 8532, "dir0": 0, "dir1": 0, "both": 1584}}, "12": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 504}, "dir0": {"neither": 0, "dir0": 3741, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 3741, "both": 0}, "both": {"neither": 10200, "dir0": 0, "dir1": 0, "both": 378}}, "13": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 18}, "dir0": {"neither": 0, "dir0": 864, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 864, "both": 0}, "both": {"neither": 6822, "dir0": 0, "dir1": 0, "both": 0}}, "14": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir0": {"neither": 0, "dir0": 108, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 108, "both": 0}, "both": {"neither": 2844, "dir0": 0, "dir1": 0, "both": 0}}, "15": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir0": {"neither": 0, "dir0": 6, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 6, "both": 0}, "both": {"neither": 804, "dir0": 0, "dir1": 0, "both": 0}}, "16": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir0": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "both": {"neither": 153, "dir0": 0, "dir1": 0, "both": 0}}, "17": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir0": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "both": {"neither": 18, "dir0": 0, "dir1": 0, "both": 0}}, "18": {"neither": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir0": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "dir1": {"neither": 0, "dir0": 0, "dir1": 0, "both": 0}, "both": {"neither": 1, "dir0": 0, "dir1": 0, "both": 0}}}, "collapsed": [-1, -18, -153, -816, -3060, -8568, -18438, -30528, -37638, -31640, -13536, 3816, 9696, 6804, 2844, 804, 153, 18, 1], "tripwire": "pass", "committed_bernstein": [-1, -18, -153, -816, -3060, -8568, -18438, -30528, -37638, -31640, -13536, 3816, 9696, 6804, 2844, 804, 153, 18, 1], "geometry": "diamond", "L": 3, "N": 18, "mask_lo": 0, "mask_hi": 262144} diff --git a/results/wrapping-type-census/diamond-L4-k1.json b/results/wrapping-type-census/diamond-L4-k1.json new file mode 100644 index 00000000..50a7abb2 --- /dev/null +++ b/results/wrapping-type-census/diamond-L4-k1.json @@ -0,0 +1,153 @@ +{ + "geometry": "diamond", + "L": 4, + "N": 32, + "physical_period": "sqrt(2)*4", + "threads": 14, + "configs_expect": 4294967296, + "k1": { + "configs_visited": 4294967296, + "wall_seconds": 323.827, + "collapsed_D_per_k": [-1,-32,-496,-4960,-35960,-201376,-906192,-3365856,-10517732,-28036448,-64383504,-128169312,-221730472,-332706976,-429729648,-470311264,-423397330,-294981856,-133649680,-2692064,61769064,67601440,46308016,23815392,9756620,3263072,896432,200800,35944,4960,496,32,1], + "joint_label_counts_per_k": [ + [0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,32,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,496,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,4960,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,35960,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,201376,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,906192,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,3365856,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,10517732,0,0,280,0,0,0,0,0,280,0,0,0,0,0,8,0,0,0,0,0,0], + [0,0,0,28036448,0,0,6080,0,0,0,0,0,6080,0,0,0,0,0,192,0,0,0,0,0,0], + [0,0,0,64383504,0,0,63104,0,0,0,0,0,63104,0,0,0,0,0,2528,0,0,0,0,0,0], + [0,0,0,128169376,0,0,416256,0,0,0,0,0,416256,0,0,64,0,0,22528,0,0,0,0,0,0], + [0,0,0,221733160,0,0,1955800,0,0,0,0,0,1955800,0,0,2688,0,0,145392,0,0,0,0,0,0], + [0,0,0,332752416,0,0,6939136,0,0,0,0,0,6939136,0,0,45440,0,0,697472,0,0,0,0,0,0], + [0,0,0,430139712,0,0,19184832,0,0,0,0,0,19184832,0,0,410064,0,0,2516160,0,0,0,0,0,0], + [0,0,0,472630784,0,0,41955584,0,0,0,0,0,41955584,0,0,2319520,0,0,6861248,0,0,0,0,0,0], + [0,0,0,432377890,0,0,72799556,0,0,0,0,0,72799556,0,0,8980560,0,0,14122828,0,0,0,0,0,0], + [0,0,0,319948992,0,0,99548800,0,0,0,0,0,99548800,0,0,24967136,0,0,21708992,0,0,0,0,0,0], + [0,0,0,184581168,0,0,105751456,0,0,0,0,0,105751456,0,0,50931488,0,0,24420032,0,0,0,0,0,0], + [0,0,0,79528832,0,0,85723936,0,0,0,0,0,85723936,0,0,76836768,0,0,19560128,0,0,0,0,0,0], + [0,0,0,24432232,0,0,52177384,0,0,0,0,0,52177384,0,0,86201296,0,0,10804544,0,0,0,0,0,0], + [0,0,0,5103360,0,0,23625792,0,0,0,0,0,23625792,0,0,72704800,0,0,3964736,0,0,0,0,0,0], + [0,0,0,687232,0,0,7955456,0,0,0,0,0,7955456,0,0,46995248,0,0,918848,0,0,0,0,0,0], + [0,0,0,55232,0,0,2000384,0,0,0,0,0,2000384,0,0,23870624,0,0,122176,0,0,0,0,0,0], + [0,0,0,2240,0,0,375004,0,0,0,0,0,375004,0,0,9758860,0,0,7192,0,0,0,0,0,0], + [0,0,0,32,0,0,51360,0,0,0,0,0,51360,0,0,3263104,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,4880,0,0,0,0,0,4880,0,0,896432,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,288,0,0,0,0,0,288,0,0,200800,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,8,0,0,0,0,0,8,0,0,35944,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,4960,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,496,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,32,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0] + ], + "coarse_4x4_counts_per_k": [ + [0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,32,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,496,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,4960,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,35960,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,201376,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,906192,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,3365856,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,10517732,0,280,0,0,0,0,280,0,0,0,0,8], + [0,0,0,28036448,0,6080,0,0,0,0,6080,0,0,0,0,192], + [0,0,0,64383504,0,63104,0,0,0,0,63104,0,0,0,0,2528], + [0,0,0,128169376,0,416256,0,0,0,0,416256,0,64,0,0,22528], + [0,0,0,221733160,0,1955800,0,0,0,0,1955800,0,2688,0,0,145392], + [0,0,0,332752416,0,6939136,0,0,0,0,6939136,0,45440,0,0,697472], + [0,0,0,430139712,0,19184832,0,0,0,0,19184832,0,410064,0,0,2516160], + [0,0,0,472630784,0,41955584,0,0,0,0,41955584,0,2319520,0,0,6861248], + [0,0,0,432377890,0,72799556,0,0,0,0,72799556,0,8980560,0,0,14122828], + [0,0,0,319948992,0,99548800,0,0,0,0,99548800,0,24967136,0,0,21708992], + [0,0,0,184581168,0,105751456,0,0,0,0,105751456,0,50931488,0,0,24420032], + [0,0,0,79528832,0,85723936,0,0,0,0,85723936,0,76836768,0,0,19560128], + [0,0,0,24432232,0,52177384,0,0,0,0,52177384,0,86201296,0,0,10804544], + [0,0,0,5103360,0,23625792,0,0,0,0,23625792,0,72704800,0,0,3964736], + [0,0,0,687232,0,7955456,0,0,0,0,7955456,0,46995248,0,0,918848], + [0,0,0,55232,0,2000384,0,0,0,0,2000384,0,23870624,0,0,122176], + [0,0,0,2240,0,375004,0,0,0,0,375004,0,9758860,0,0,7192], + [0,0,0,32,0,51360,0,0,0,0,51360,0,3263104,0,0,0], + [0,0,0,0,0,4880,0,0,0,0,4880,0,896432,0,0,0], + [0,0,0,0,0,288,0,0,0,0,288,0,200800,0,0,0], + [0,0,0,0,0,8,0,0,0,0,8,0,35944,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,4960,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,496,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,32,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0] + ], + "D_positive_attribution_per_k": [ + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,280,0,0,0,0,0,280,0,0,0,0,0,8,0,0,0,0,0,0], + [0,0,0,0,0,0,6080,0,0,0,0,0,6080,0,0,0,0,0,192,0,0,0,0,0,0], + [0,0,0,0,0,0,63104,0,0,0,0,0,63104,0,0,0,0,0,2528,0,0,0,0,0,0], + [0,0,0,0,0,0,416256,0,0,0,0,0,416256,0,0,64,0,0,22528,0,0,0,0,0,0], + [0,0,0,0,0,0,1955800,0,0,0,0,0,1955800,0,0,2688,0,0,145392,0,0,0,0,0,0], + [0,0,0,0,0,0,6939136,0,0,0,0,0,6939136,0,0,45440,0,0,697472,0,0,0,0,0,0], + [0,0,0,0,0,0,19184832,0,0,0,0,0,19184832,0,0,410064,0,0,2516160,0,0,0,0,0,0], + [0,0,0,0,0,0,41955584,0,0,0,0,0,41955584,0,0,2319520,0,0,6861248,0,0,0,0,0,0], + [0,0,0,0,0,0,72799556,0,0,0,0,0,72799556,0,0,8980560,0,0,14122828,0,0,0,0,0,0], + [0,0,0,0,0,0,99548800,0,0,0,0,0,99548800,0,0,24967136,0,0,21708992,0,0,0,0,0,0], + [0,0,0,0,0,0,105751456,0,0,0,0,0,105751456,0,0,50931488,0,0,24420032,0,0,0,0,0,0], + [0,0,0,0,0,0,85723936,0,0,0,0,0,85723936,0,0,76836768,0,0,19560128,0,0,0,0,0,0], + [0,0,0,0,0,0,52177384,0,0,0,0,0,52177384,0,0,86201296,0,0,10804544,0,0,0,0,0,0], + [0,0,0,0,0,0,23625792,0,0,0,0,0,23625792,0,0,72704800,0,0,3964736,0,0,0,0,0,0], + [0,0,0,0,0,0,7955456,0,0,0,0,0,7955456,0,0,46995248,0,0,918848,0,0,0,0,0,0], + [0,0,0,0,0,0,2000384,0,0,0,0,0,2000384,0,0,23870624,0,0,122176,0,0,0,0,0,0], + [0,0,0,0,0,0,375004,0,0,0,0,0,375004,0,0,9758860,0,0,7192,0,0,0,0,0,0], + [0,0,0,0,0,0,51360,0,0,0,0,0,51360,0,0,3263104,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,4880,0,0,0,0,0,4880,0,0,896432,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,288,0,0,0,0,0,288,0,0,200800,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,8,0,0,0,0,0,8,0,0,35944,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,4960,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,496,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,32,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0] + ], + "D_negative_attribution_per_k": [ + [0,0,0,-1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-32,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-496,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-4960,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-35960,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-201376,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-906192,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-3365856,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,-10517732,0,0,-280,0,0,0,0,0,-280,0,0,0,0,0,-8,0,0,0,0,0,0], + [0,0,0,-28036448,0,0,-6080,0,0,0,0,0,-6080,0,0,0,0,0,-192,0,0,0,0,0,0], + [0,0,0,-64383504,0,0,-63104,0,0,0,0,0,-63104,0,0,0,0,0,-2528,0,0,0,0,0,0], + [0,0,0,-128169376,0,0,-416256,0,0,0,0,0,-416256,0,0,0,0,0,-22528,0,0,0,0,0,0], + [0,0,0,-221733160,0,0,-1955800,0,0,0,0,0,-1955800,0,0,0,0,0,-145392,0,0,0,0,0,0], + [0,0,0,-332752416,0,0,-6939136,0,0,0,0,0,-6939136,0,0,0,0,0,-697472,0,0,0,0,0,0], + [0,0,0,-430139712,0,0,-19184832,0,0,0,0,0,-19184832,0,0,0,0,0,-2516160,0,0,0,0,0,0], + [0,0,0,-472630784,0,0,-41955584,0,0,0,0,0,-41955584,0,0,0,0,0,-6861248,0,0,0,0,0,0], + [0,0,0,-432377890,0,0,-72799556,0,0,0,0,0,-72799556,0,0,0,0,0,-14122828,0,0,0,0,0,0], + [0,0,0,-319948992,0,0,-99548800,0,0,0,0,0,-99548800,0,0,0,0,0,-21708992,0,0,0,0,0,0], + [0,0,0,-184581168,0,0,-105751456,0,0,0,0,0,-105751456,0,0,0,0,0,-24420032,0,0,0,0,0,0], + [0,0,0,-79528832,0,0,-85723936,0,0,0,0,0,-85723936,0,0,0,0,0,-19560128,0,0,0,0,0,0], + [0,0,0,-24432232,0,0,-52177384,0,0,0,0,0,-52177384,0,0,0,0,0,-10804544,0,0,0,0,0,0], + [0,0,0,-5103360,0,0,-23625792,0,0,0,0,0,-23625792,0,0,0,0,0,-3964736,0,0,0,0,0,0], + [0,0,0,-687232,0,0,-7955456,0,0,0,0,0,-7955456,0,0,0,0,0,-918848,0,0,0,0,0,0], + [0,0,0,-55232,0,0,-2000384,0,0,0,0,0,-2000384,0,0,0,0,0,-122176,0,0,0,0,0,0], + [0,0,0,-2240,0,0,-375004,0,0,0,0,0,-375004,0,0,0,0,0,-7192,0,0,0,0,0,0], + [0,0,0,-32,0,0,-51360,0,0,0,0,0,-51360,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,-4880,0,0,0,0,0,-4880,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,-288,0,0,0,0,0,-288,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,-8,0,0,0,0,0,-8,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], + [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0] + ] + } +} diff --git a/scripts/wrapping_five_cell_reader.py b/scripts/wrapping_five_cell_reader.py new file mode 100644 index 00000000..8a26a500 --- /dev/null +++ b/scripts/wrapping_five_cell_reader.py @@ -0,0 +1,118 @@ +#!/usr/bin/env python3 +"""#659 reader: verify the five-cell wrapping-type identities on the committed tables. + +Reads only results/wrapping-type-census/*.json (PR #653 and PR #657 artifacts). +Exact integer arithmetic throughout. No enumeration. + +Usage: + python3 scripts/wrapping_five_cell_reader.py # verify all + python3 scripts/wrapping_five_cell_reader.py --json # also dump cell sequences +""" +import argparse +import json +import os +import sys +from math import comb + +HERE = os.path.dirname(os.path.abspath(__file__)) +RESULTS = os.path.join(HERE, os.pardir, "results", "wrapping-type-census") + +# (file, geometry, L, N) +TABLES = [ + ("axis-L3.json", "axis", 3, 9), + ("axis-L4.json", "axis", 4, 16), + ("axis-L5.json", "axis", 5, 25), + ("diamond-L3.json", "diamond", 3, 18), + ("diamond-L4-k1.json", "diamond", 4, 32), +] + + +def load_cells(path, N): + """Return dict of the five cell sequences indexed 0..N.""" + with open(path) as f: + d = json.load(f) + if "tables" in d: # PR #653 nested 4x4 format + t = d["tables"] + order = ["neither", "dir0", "dir1", "both"] + flat = [[t[str(k)][r][c] for r in order for c in order] for k in range(N + 1)] + else: # PR #657 coarse 4x4 format + key = "k1" if "k1" in d else "k2" + flat = d[key]["coarse_4x4_counts_per_k"] + return { + "n×b": [row[3] for row in flat], + "b×n": [row[12] for row in flat], + "d0": [row[5] for row in flat], + "d1": [row[10] for row in flat], + "b×b": [row[15] for row in flat], + } + + +def collapsed(path): + with open(path) as f: + d = json.load(f) + return d["collapsed"] if "collapsed" in d else d["k1"]["collapsed_D_per_k"] + + +def check(name, ok): + print(("PASS" if ok else "FAIL"), name) + return ok + + +def verify(geometry, L, N, C, ak): + ok = True + # support + row sums + spiral pairing + MZ pairing + ok &= check(f"{geometry} L={L}: row sums nb+bn+d0+d1+bb = C(N,k)", + all(C["n×b"][k] + C["b×n"][k] + C["d0"][k] + C["d1"][k] + C["b×b"][k] == comb(N, k) + for k in range(N + 1))) + ok &= check(f"{geometry} L={L}: d0 == d1 at every k", C["d0"] == C["d1"]) + ok &= check(f"{geometry} L={L}: a_k == b×n − n×b (MZ pairing)", + [C["b×n"][k] - C["n×b"][k] for k in range(N + 1)] == ak) + ok &= check(f"{geometry} L={L}: a_k == b×n − n×b == collapsed committed", True) # ak is collapsed + + kstart = L if geometry == "axis" else 2 * L + ok &= check(f"{geometry} L={L}: n×b(k) = C(N,k) for k < {kstart}", + all(C["n×b"][k] == comb(N, k) for k in range(kstart))) + ok &= check(f"{geometry} L={L}: b×n(k) = C(N,k) for k >= N-L+1 = {N - L + 1}", + all(C["b×n"][k] == comb(N, k) for k in range(N - L + 1, N + 1))) + if geometry == "axis": + ok &= check(f"axis L={L}: d0(L) = L", C["d0"][L] == L) + ok &= check(f"axis L={L}: b×n(2L-1) = L^2", C["b×n"][2 * L - 1] == L * L) + ok &= check(f"axis L={L}: C-n×b = d0+d1 for L <= k < 2L-1", + all(comb(N, k) - C["n×b"][k] == C["d0"][k] + C["d1"][k] + for k in range(L, 2 * L - 1))) + else: + ok &= check(f"diamond L={L}: d0(2L) = 4*C(2L,4)", C["d0"][2 * L] == 4 * comb(2 * L, 4)) + ok &= check(f"diamond L={L}: b×b(2L) = 2L", C["b×b"][2 * L] == 2 * L) + ok &= check(f"diamond L={L}: C-n×b = d0+d1+b×b for 2L <= k < 3L-1", + all(comb(N, k) - C["n×b"][k] == C["d0"][k] + C["d1"][k] + C["b×b"][k] + for k in range(2 * L, 3 * L - 1))) + if L in (3, 4): # onset conjecture, only two committed points + ok &= check(f"diamond L={L}: b×n onset k = 3L-1 = {3 * L - 1}", + all(C["b×n"][k] == 0 for k in range(3 * L - 1)) and C["b×n"][3 * L - 1] > 0) + ok &= check(f"diamond L={L}: b×n(3L-1) = 4L^2", C["b×n"][3 * L - 1] == 4 * L * L) + return ok + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--json", action="store_true", help="dump the five cell sequences") + args = ap.parse_args() + all_ok = True + for fname, geometry, L, N in TABLES: + path = os.path.join(RESULTS, fname) + if not os.path.exists(path): + print(f"SKIP {fname} (not present; PR branch artifact)") + continue + C = load_cells(path, N) + ak = collapsed(path) + print(f"== {fname} (geometry={geometry}, L={L}, N={N})") + if args.json: + for cell, seq in C.items(): + print(f" {cell}: {seq}") + all_ok &= verify(geometry, L, N, C, ak) + print("ALL CHECKS PASS" if all_ok else "FAILURES PRESENT") + return 0 if all_ok else 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/wrapping_onset_proof_checks.py b/scripts/wrapping_onset_proof_checks.py new file mode 100644 index 00000000..0ec79605 --- /dev/null +++ b/scripts/wrapping_onset_proof_checks.py @@ -0,0 +1,180 @@ +#!/usr/bin/env python3 +"""#673 verification: brute-force re-derivation of the five-cell onsets at +COMMITTED sizes only (axis L=3,4; diamond L=2,3), using the repo's own +classifier (torus_homology). No new census: this re-verifies identities at +sizes whose tables are already committed (PRs #653/#657; diamond L=2 is +recomputable in seconds at 2^8 and is used only to test the *L=2 point* of +the closed forms, not as a new census rung). + +Checks: + I1: n*b = C(N,k) below onset (axis k= N-L+1, strict at k=N-L (both geometries) + axis I3a: d0(L) = d1(L) = L, and every such set is a full row/column + axis I3b: b*n(2L-1) = L^2, b*n = 0 below, and every such set is a cross + axis I4: C - n*b = d0 + d1 on L <= k < 2L-1 + diamond d0 black side: #black-dir0-only sets at k=2L == L*C(2L,L) + diamond b*b(2L) = 2L, and every such set is a straight diagonal line +""" +import itertools +import os +import sys +from collections import Counter +from math import comb + +HERE = os.path.dirname(os.path.abspath(__file__)) +sys.path.insert(0, os.path.join(HERE, os.pardir, "scripts")) + +from matched_torus_reference import axis_geometry, diamond_geometry +from torus_homology import classify_configuration + +failures = [] + + +def check(name, ok): + print(("PASS" if ok else "FAIL"), name) + if not ok: + failures.append(name) + + +def type_pair(g, combo): + active = [False] * g.n + for i in combo: + active[i] = True + black, _ = classify_configuration(g, active) + white, _ = classify_configuration(g, [not a for a in active], matching=True) + bt = ("both" if black.both else "dir0" if black.direction_0 else + "dir1" if black.direction_1 else "neither") + wt = ("both" if white.both else "dir0" if white.direction_0 else + "dir1" if white.direction_1 else "neither") + return bt, wt + + +def cell_counts(g, k): + counts = {} + for combo in itertools.combinations(range(g.n), k): + t = type_pair(g, combo) + counts[t] = counts.get(t, 0) + 1 + return counts + + +def is_full_line_axis(g, combo, orientation): + """orientation 'row' = fixed y, 'col' = fixed x; full = L sites.""" + coords = [g.coordinates[i] for i in combo] + fixed = {c[1] for c in coords} if orientation == "row" else {c[0] for c in coords} + return len(coords) == g.L and len(fixed) == 1 + + +def run_axis(L): + g = axis_geometry(L) + N = L * L + print(f"== axis L={L} (N={N})") + ok = all(all(t == ("neither", "both") for t in + (type_pair(g, c) for c in itertools.combinations(range(g.n), k))) + for k in range(L)) + check(f"I1: n*b=C(N,k) for k<{L}", ok) + ok = all(all(t == ("both", "neither") for t in + (type_pair(g, c) for c in itertools.combinations(range(g.n), k))) + for k in range(N - L + 1, N + 1)) + ok = ok and any(t != ("both", "neither") for t in cells_at(g, N - L)) + check(f"I2: b*n=C(N,k) for k>={N-L+1}, strict at {N-L}", ok) + c = cell_counts(g, L) + check(f"I3a: d0({L}) == {L}", c.get(("dir0", "dir0"), 0) == L) + check(f"I3a: d1({L}) == {L}", c.get(("dir1", "dir1"), 0) == L) + ok = True + for combo in itertools.combinations(range(g.n), L): + bt, wt = type_pair(g, combo) + if bt == "dir0" and wt == "dir0": + ok &= is_full_line_axis(g, combo, "row") + if bt == "dir1" and wt == "dir1": + ok &= is_full_line_axis(g, combo, "col") + check("I3a: every d0 set is a full row and every d1 set a full column", ok) + if 2 * L - 1 <= N: + c = cell_counts(g, 2 * L - 1) + check(f"I3b: b*n({2*L-1}) == L^2 == {L*L}", + c.get(("both", "neither"), 0) == L * L) + below = all(cell_counts(g, k).get(("both", "neither"), 0) == 0 + for k in range(2 * L - 1)) + check(f"I3b: b*n = 0 for k < {2*L-1}", below) + ok = True + for combo in itertools.combinations(range(g.n), 2 * L - 1): + bt, wt = type_pair(g, combo) + if bt == "both" and wt == "neither": + coords = [g.coordinates[i] for i in combo] + cx = Counter(x for x, _ in coords) + cy = Counter(y for _, y in coords) + ok &= (max(cx.values()) == L and max(cy.values()) == L) + check("I3b: every b*n set at k=2L-1 contains a full row and a full column", + ok) + ok = True + for k in range(L, min(2 * L - 1, N + 1)): + c = cell_counts(g, k) + ok &= (c.get(("both", "both"), 0) == 0 and c.get(("both", "neither"), 0) == 0) + ok &= (comb(N, k) - c.get(("neither", "both"), 0) + == c.get(("dir0", "dir0"), 0) + c.get(("dir1", "dir1"), 0)) + check(f"I4: C-n*b = d0+d1 for {L} <= k < {2*L-1} (b*n = b*b = 0 there)", ok) + + +def is_diag_line_diamond(g, combo, slope): + """slope 'm1': v-u constant (winds both via (1,1) steps); + slope 'p1': v+u constant.""" + coords = [g.coordinates[i] for i in combo] + if slope == "m1": + vals = {(v - u) % (2 * g.L) for u, v in coords} + else: + vals = {(v + u) % (2 * g.L) for u, v in coords} + return len(coords) == 2 * g.L and len(vals) == 1 + + +def cells_at(g, k): + return [type_pair(g, c) for c in itertools.combinations(range(g.n), k)] + + +def run_diamond(L): + g = diamond_geometry(L) + N = 2 * L * L + print(f"== diamond L={L} (N={N})") + ok = all(t == ("neither", "both") for k in range(2 * L) + for t in cells_at(g, k)) + check(f"I1: n*b=C(N,k) for k<{2*L}", ok) + ok = all(t == ("both", "neither") for k in range(N - L + 1, N + 1) + for t in cells_at(g, k)) + ok = ok and any(t != ("both", "neither") for t in cells_at(g, N - L)) + check(f"I2: b*n=C(N,k) for k>={N-L+1}, strict at {N-L}", ok) + cnt = 0 + bb = 0 + all_bb_are_diag = True + for combo in itertools.combinations(range(g.n), 2 * L): + bt, wt = type_pair(g, combo) + if bt == "dir0" and wt == "dir0": + cnt += 1 + if bt == "both" and wt == "both": + bb += 1 + all_bb_are_diag &= (is_diag_line_diamond(g, combo, "m1") + or is_diag_line_diamond(g, combo, "p1")) + check(f"diamond: #black dir0-only sets at k={2*L} == L*C(2L,L) == {L*comb(2*L,L)}", + cnt == L * comb(2 * L, L)) + check(f"diamond: b*b({2*L}) == 2L == {2*L}", bb == 2 * L) + check("diamond: every b*b set at k=2L is a straight diagonal line", + all_bb_are_diag) + c = cell_counts(g, 2 * L) + check(f"diamond: d0 cell at k={2*L} == L*C(2L,L)", + c.get(("dir0", "dir0"), 0) == L * comb(2 * L, L)) + check(f"diamond: d1 cell at k={2*L} == L*C(2L,L)", + c.get(("dir1", "dir1"), 0) == L * comb(2 * L, L)) + ok = True + for k in range(2 * L, min(3 * L - 1, N + 1)): + c = cell_counts(g, k) + ok &= (c.get(("both", "neither"), 0) == 0) + ok &= (comb(N, k) - c.get(("neither", "both"), 0) + == c.get(("dir0", "dir0"), 0) + c.get(("dir1", "dir1"), 0) + + c.get(("both", "both"), 0)) + check(f"diamond I4: C-n*b = d0+d1+b*b for {2*L} <= k < {3*L-1}", ok) + + +if __name__ == "__main__": + run_axis(3) + run_axis(4) + run_diamond(2) + run_diamond(3) + print("ALL CHECKS PASS" if not failures else f"FAILURES: {failures}") + sys.exit(1 if failures else 0)