From d4d09f8e00bebab83e6602b185423f603bf6caba Mon Sep 17 00:00:00 2001 From: lieoric <129092606+lieoric@users.noreply.github.com> Date: Tue, 11 Aug 2026 07:26:01 +1000 Subject: [PATCH 1/6] Audit global h7 bypass reductions --- .github/workflows/c4-h7-global-bypass.yml | 86 +++ docs/c4-h7-anchor-pair-potential.md | 402 +++++++++++++ docs/c4-h7-critical-pair-bypass.md | 486 +++++++++++++++ docs/c4-h7-rainbow-lift.md | 309 ++++++++++ tests/check_c4_h7_anchor_pair_potential.py | 664 +++++++++++++++++++++ tests/check_c4_h7_critical_pair_bypass.py | 526 ++++++++++++++++ tests/check_c4_h7_rainbow_lift.py | 641 ++++++++++++++++++++ 7 files changed, 3114 insertions(+) create mode 100644 .github/workflows/c4-h7-global-bypass.yml create mode 100644 docs/c4-h7-anchor-pair-potential.md create mode 100644 docs/c4-h7-critical-pair-bypass.md create mode 100644 docs/c4-h7-rainbow-lift.md create mode 100644 tests/check_c4_h7_anchor_pair_potential.py create mode 100644 tests/check_c4_h7_critical_pair_bypass.py create mode 100644 tests/check_c4_h7_rainbow_lift.py diff --git a/.github/workflows/c4-h7-global-bypass.yml b/.github/workflows/c4-h7-global-bypass.yml new file mode 100644 index 0000000..26d2767 --- /dev/null +++ b/.github/workflows/c4-h7-global-bypass.yml @@ -0,0 +1,86 @@ +name: Audit c4 h7 global bypass lemmas +run-name: Check the critical-pair, anchor-pair, and rainbow-lift reductions + +on: + push: + branches: [codex/c4-h7-global-bypass] + workflow_dispatch: + +permissions: + contents: read + +concurrency: + group: c4-h7-global-bypass-${{ github.ref }} + cancel-in-progress: true + +jobs: + mathematical-reductions: + runs-on: ubuntu-latest + timeout-minutes: 30 + steps: + - uses: actions/checkout@v5 + - uses: actions/setup-python@v5 + with: + python-version: "3.12" + - name: Compile the independent audit programs + run: >- + python -m py_compile + tests/check_c4_h7_critical_pair_bypass.py + tests/check_c4_h7_rainbow_lift.py + tests/check_c4_h7_anchor_pair_potential.py + - name: Build the certified first-exhaustion census producer + run: | + cmake -S . -B build \ + -DCMAKE_BUILD_TYPE=Release \ + -DWSC_WARNINGS_AS_ERRORS=ON + cmake --build build \ + --target water-c4-h7-tq-exhaust-siblings --parallel 2 + - name: Rebuild the complete first-exhaustion ledger + run: | + mkdir -p out/anchor + build/water-c4-h7-tq-exhaust-siblings \ + --output-dir out/anchor + test "$(jq -r .status out/anchor/report.json)" = NEXT_RUN_CENSUS_COMPLETE + - name: Check every stated critical-pair and past-bypass formula + run: | + mkdir -p out/critical + set -o pipefail + python tests/check_c4_h7_critical_pair_bypass.py 2>&1 \ + | tee out/critical/audit.log + - name: Check rainbow factorization and exact token-lift fixtures + run: | + mkdir -p out/rainbow + set -o pipefail + python tests/check_c4_h7_rainbow_lift.py \ + --json out/rainbow/audit.json 2>&1 \ + | tee out/rainbow/audit.log + - name: Check the two-anchor potential and its complete ledger + run: | + set -o pipefail + python tests/check_c4_h7_anchor_pair_potential.py \ + --report out/anchor/report.json 2>&1 \ + | tee out/anchor/potential-audit.json + - name: Record the exact claim boundary + run: | + cat >> "$GITHUB_STEP_SUMMARY" <<'EOF' + These checks certify three mathematical reductions: the exact + critical-pair disable formula plus the past/future bypass, the + two-anchor vector potential and first-sweep inequalities, and the + rainbow-transversal/token-error formula. They deliberately do not + claim universal c4/k2/h7 solvability. + EOF + - name: Hash the complete audit bundle + if: always() + run: | + mkdir -p out + find out -type f ! -name SHA256SUMS -print0 \ + | sort -z \ + | xargs -0 -r sha256sum > out/SHA256SUMS + sha256sum --check out/SHA256SUMS + - uses: actions/upload-artifact@v6 + if: always() + with: + name: c4-h7-global-bypass-audit-${{ github.run_id }} + path: out/ + if-no-files-found: error + retention-days: 30 diff --git a/docs/c4-h7-anchor-pair-potential.md b/docs/c4-h7-anchor-pair-potential.md new file mode 100644 index 0000000..666cdd9 --- /dev/null +++ b/docs/c4-h7-anchor-pair-potential.md @@ -0,0 +1,402 @@ +# Anchor-pair potentials at `c=4, h=7, k=2` + +## Scope and claim boundary + +This note develops a two-dimensional replacement for the one-color debt +rotor used in the three-color proof. It applies at `z=0`, before the first +original column has been exhausted, and proves four facts. + +1. In a rich two-anchor state, source legality is exactly a two-bin fitting + test. +2. A genuine excursion through a complement color has a strictly increasing + scalar energy and a coordinatewise increasing **complement-exposure + vector**. A direct anchor-to-anchor edge is a separate zero-cost + transfer. +3. A first-exhaustion `Tq` state of energy two has already exposed all seven + items of its top color. +4. A `2+2` `D2` terminal created on the first two-anchor sweep satisfies + inequalities which exclude energy two and make energy one rigid. + +These are reduction lemmas, not a proof that every height-7 layout is +solvable. At `z=0`, an excursion can end by exhausting the first original +column; unlike the three-color problem, that is not yet the goal. A rotor can +also end at a genuine `D2` terminal. Finally, a losing nonzero-debt +checkpoint is not a losing zero-debt initial layout. + +The accompanying checker enumerates numerical macro types and committed +next-run cards only. It counts compatible residual words combinatorially and +never expands them. + +## 1. Border equations + +At a border checkpoint write + +\[ + d_c=F_c-G_c, +\] + +where `F_c` is the number of exposed items of color `c` and `G_c` is the sum +of the active host capacities currently topped by `c`. At `z=0`, + +\[ + \sum_c d_c=0. +\] + +A source of top color `x` and cumulative cap `r` is legal exactly when + +\[ + \#\{c:d_c+r[c=x]>0\}\le2. \tag{1} +\] + +A live event + +\[ + x_r\longrightarrow y_R,\qquad x\ne y,\quad r0, + \tag{3} +\] + +in that color order, and suppose every active top color belongs to +`{alpha,beta}`. Equation `sum d=0` gives + +\[ + A+B=X+Y. \tag{4} +\] + +Call `alpha,beta` the anchors and `x,y` the complement colors. + +**Lemma 1 (two-bin source test).** An `alpha` source of cap `c` is legal if +and only if `c<=A`. A `beta` source of cap `c` is legal if and only if +`c<=B`. + +**Proof.** Testing the `alpha` source changes only the first coordinate of +(3), from `-A` to `-A+c`. The two complement coordinates are already +positive and the `beta` coordinate is nonpositive. Thus (1) holds precisely +when `-A+c<=0`. The `beta` statement is symmetric. \(\square\) + +The interpretation is exact: `A,B` are two bin capacities and every +anchor-top source is an item which must fit in the bin named by its current +top color. A state of the form (3) is terminal exactly when no current item +fits. + +At height 7 a terminal of this form cannot have top multiplicity `4+0`. +Indeed, the unused anchor has no host, so its nonpositive debt must be zero. +The occupied-anchor energy is then `A=X+Y>=2`. Four caps strictly greater +than `A` would give + +\[ + F_{\alpha}=G_{\alpha}-A + \ge4(A+1)-A=3A+4\ge10>7. \tag{5} +\] + +Consequently the only terminal multiplicities are `3+1` and `2+2`. + +## 3. The anchor corridor and its vector potential + +Suppose an `alpha_c` source is legal, so `c<=A`, and its next run is a +complement color. Follow that same fixed column. If it does not exhaust, +stop at the first later event which enters either anchor. Write that final +event as + +\[ + z_w\longrightarrow \delta_T, + \qquad z\in\{x,y\},\quad + \delta\in\{\alpha,\beta\},\quad cA+B. \tag{8} +\] + +The more informative invariant is the complement-exposure vector. At an +all-anchor checkpoint the complement colors have no hosts, so + +\[ + (d_x,d_y)=(F_x,F_y). \tag{9} +\] + +The portion of the chosen column strictly between caps `c` and `w` consists +only of complement colors. If it contains `u_x` items of `x` and `u_y` +items of `y`, then + +\[ + (F'_x,F'_y)=(F_x+u_x,F_y+u_y), + \qquad u_x,u_y\ge0, + \qquad u_x+u_y=w-c\ge1. \tag{10} +\] + +Equations (8) and (10) agree through (4): + +\[ + A'+B'=F'_x+F'_y. +\] + +Thus `(F_x,F_y)` increases coordinatewise and strictly in at least one +coordinate. Equivalently, the hidden-inventory vector + +\[ + (7-F_x,7-F_y) \tag{11} +\] + +decreases coordinatewise and strictly in at least one coordinate. + +There is one zero-cost case which must not be hidden in the word +"excursion". If the selected source moves directly between anchors, + +\[ + \alpha_c\longrightarrow\beta_R, +\] + +then + +\[ + (A',B')=(A-c,B+c),\qquad + (F'_x,F'_y)=(F_x,F_y). \tag{12} +\] + +Thus total energy and the complement vector are unchanged. The transition +still makes irreversible progress because the fixed column cap advances +from `c` to `R>c`. The symmetric `beta -> alpha` formula is identical. + +**Corollary 3 (finite two-anchor rotor).** Repeatedly choose a fitting +anchor source. Apply Lemma 2 when it enters a complement color, and apply +(12) when it enters the other anchor directly. The process reaches either + +1. the first exhausted original column; or +2. an all-anchor state with no fitting source, which is a `D2` terminal. + +It cannot cycle because every selected fixed-column boundary advances. +Starting from `(F_x,F_y)`, it makes at most `14-F_x-F_y` **genuine +complement excursions** before one of those outcomes. Direct anchor +transfers are additional zero-cost events, but their number is bounded by +the finite remaining border count. + +This is the useful replacement for a scalar debt rotor. On genuine +excursions the scalar `A+B` proves progress, while the vector (10) records +*which* of the two complement inventories paid for that progress. The +complement part of a suffix can therefore be compressed to a monotone path +in a `7 x 7` grid; direct anchor transfers retain only their finite endpoint +sequence. + +## 4. Energy-two `Tq` saturation + +At `z=1`, a `Tq` terminal has three active `q` tops. Write + +\[ + d_q=-E, + \qquad d_c>0\quad(c\ne q), +\] + +and let the three `q` caps be `r_1,r_2,r_3`. Terminal blockedness gives +`r_i>E`, and physical balance gives + +\[ + F_q=r_1+r_2+r_3-E\le7. \tag{13} +\] + +**Lemma 4 (`E=2` saturation).** If `E=2`, then + +\[ + (r_1,r_2,r_3)=(3,3,3), + \qquad F_q=7. \tag{14} +\] + +**Proof.** Integrality and `r_i>2` give `sum r_i>=9`. Substitution in +(13) gives `F_q>=7`. Both inequalities must be equalities. \(\square\) + +The first-exhausting event which enters this `Tq` terminal does not expose +new `q` items: its isolated final run has another color. Hence the `z=0` +bridge parent also has `F_q=7`. No compatible residual suffix contains a +hidden `q` item. + +This has two different consequences in the two bridge normal forms. + +- If the bad source color is not `q`, the two-anchor sweep uses the bad + source color and the isolated final color as anchors. Then `q` is a + complement color fixed at exposure seven. Any later `D2` has positive + mass at least `7+1=8`. A `3+1` `D2` is impossible: the three-source + anchor has energy at most 2 by (5), while the one-source anchor has energy + at most 5, so their total is at most 7. Only a `2+2` terminal can remain. +- If the bad source color is `q`, then `q` is itself an anchor after a live + sibling move. Saturation still says that a column which leaves `q` can + never encounter another hidden `q`, but the preceding positive-mass + argument does not apply because `q` is hosted. + +The numerical terminal census reflects the same bounds. The 265 canonical +`3+1` types have total anchor energy at most 7. The 661 canonical `2+2` +types have energy at most 10; exactly ten of them have one positive +coordinate equal to seven. + +## 5. First-sweep `2+2` inequalities + +Consider the first-exhaustion bridge with bad source color `a!=q` and +isolated final color `f`. In parent coordinates its normal form is + +\[ + d(P)=(-E,0,-A,A+E) \tag{15} +\] + +in color order `(q,f,a,b)`. The active tops are the bad `a_s` source and +three `q` siblings. Each sibling cap is strictly greater than `E`. + +Suppose the **first** sweep sends exactly one sibling directly to `a` and +the other two directly to `f`: + +\[ + q_u\to a_{R_a}, + \qquad q_v\to f_{R_1}, + \qquad q_w\to f_{R_2}, \tag{16} +\] + +where all endpoints are live and therefore at most 6. Put + +\[ + A'=A+u, + \qquad B'=v+w. \tag{17} +\] + +After (16), the two `a` tops have caps `s,R_a`, the two `f` tops have caps +`R_1,R_2`, and the debts are + +\[ + d=(-E+u+v+w,\ -B',\ -A',\ A+E). \tag{18} +\] + +The first and last coordinates in (18) are positive exactly in the genuine +`D2` case. Lemma 1 gives the exact terminal test + +\[ + s>A',\qquad R_a>A',\qquad + R_1>B',\qquad R_2>B'. \tag{19} +\] + +There is also a fixed-future inventory constraint. The reserved bad tail +uses `7-s` items of color `f`, while the two live cards in (16) use +`R_1-v` and `R_2-w`. Joint realizability therefore requires + +\[ + (R_1-v)+(R_2-w)\le s. \tag{20} +\] + +**Lemma 5 (first-sweep lower bound).** Every jointly realizable first-sweep +`2+2` terminal satisfies + +\[ + s\ge A+u+1, + \qquad + s\ge v+w+2\ge2E+4. \tag{21} +\] + +**Proof.** The first inequality is integer strictness in (19). The last +two inequalities in (19) give `R_i>=v+w+1`; hence + +\[ + (R_1-v)+(R_2-w) + \ge2(v+w+1)-(v+w)=v+w+2. +\] + +Combine this with (20). Finally `v,w>E`, so `v+w>=2(E+1)`. \(\square\) + +Since a live bad source has `s<=6`, equation (21) proves that `E=2` can +never enter `D2` on the first sweep. Such a branch must make at least one +further anchor excursion before a later `D2` is possible. + +At `E=1`, (21) is rigid: + +\[ + s=6, + \qquad v=w=2, + \qquad R_1=R_2=5. \tag{22} +\] + +Moreover, parent exposure is `F_a=s-A=6-A`. The `a` card has length +`R_a-u>A`, while only `1+A` items of `a` remain. Therefore + +\[ + R_a-u=A+1, + \qquad F_a'=7. \tag{23} +\] + +The two `f` cards expose six `f` items, and the remaining one `f` item is +the reserved length-one bad tail. Thus all `a` inventory is exposed and all +`f` inventory is already assigned, even though the bad-tail `f` is still +hidden at this `z=0` checkpoint. + +## 6. Exact finite audit + +`tests/check_c4_h7_anchor_pair_potential.py` performs four independent +finite checks. + +1. It regenerates all `71 + 265 + 661 = 997` terminal macro types and checks + the source thresholds, multiplicity bounds, and the seven `E=2` `Tq` + types. +2. It exhausts the integer box of (3), (6), (7), and (12), checking the + two-bin legality test, the strict excursion increment, and the zero-cost + direct-anchor transfer. +3. It reads a complete first-exhaustion report and reclassifies every + reported `D2` count by `E`, bad-source form, and parent legal-source + count. +4. It enumerates only the direct cards in (16), counts residual words with + multinomial/Hall arithmetic, and checks (19)-(23). It does not enumerate + any residual word. + +For the certified first-exhaustion report, the new ledger is + +| slice | edges | card decorations | residual-word weight | +|---|---:|---:|---:| +| all `E=2` `D2` reductions | 30 | 2,350 | 96,108 | +| `E=2`, bad source `a!=q` | 18 | 1,369 | 57,090 | +| `E=2`, bad source `a=q` | 12 | 981 | 39,018 | +| first-sweep `2+2`, `E=0` | 41 | 304 | 322,825 | +| first-sweep `2+2`, `E=1` | 9 | 17 | 242 | +| first-sweep `2+2`, `E=2` | 0 | 0 | 0 | + +The 321 first-sweep decorations have 142 distinct numerical signatures: +133 at `E=0` and the nine rigid signatures from (22)-(23) at `E=1`. + +These counts are a strict reclassification of the existing 67,206 +`D2`-reduction decorations. They do not eliminate the later-rotor `D2` +remainder, the `a=q` anchor form, the unique-source `Tq` entrances, or the +full height-7 initial-layout universe. diff --git a/docs/c4-h7-critical-pair-bypass.md b/docs/c4-h7-critical-pair-bypass.md new file mode 100644 index 0000000..de4aeae --- /dev/null +++ b/docs/c4-h7-critical-pair-bypass.md @@ -0,0 +1,486 @@ +# Critical pairs and a past--future bypass at `c=4, h=7, k=2` + +## Scope and claim boundary + +This note gives a local exchange calculus for fixed border events and applies +it to the four-legal-source, all-`q`/all-`f` star that can precede a first +exhaustion `Tq` terminal. It proves two facts. + +1. Whether one live event disables another source has an exact three-clause + test. In particular, a direct two-color swap cannot be a mutual lock. +2. At height seven, an all-`q`/all-`f` four-way star has either a forward + executable square or an explicit zero-debt past-prefix bypass. The only + combinatorial corner of the past argument is a rigid `Q=7` pattern, and it + also has an explicit weave. + +The second statement is deliberately a **local bypass theorem**. Its output +is a legal state with a legal continuation; it does not say that this +continuation reaches `z=2`. A later `D2` or `Tq` obstruction may still occur. +Thus this note neither eliminates the full three-/four-source `D2` remainder +nor proves universal solvability at height seven. + +## 1. Border events as guarded commuting vectors + +For a border state write + +\[ + d_c=F_c-G_c, +\] + +and let `z` be the number of exhausted original columns. A physical source +of top color `x` and exposed host capacity `s` is legal exactly when + +\[ + \left|\operatorname{Pos}(d+s e_x)\right|\le K, + \qquad K=2+z, \tag{1} +\] + +where `Pos(v)={c:v_c>0}`. A live event + +\[ + A=(x_s\longrightarrow y_R),\qquad x\ne y,quad ss. &&\tag{4c} +\end{aligned} +\] + +**Proof.** The source test after `A` is + +\[ + w+s e_x-s e_y. \tag{5} +\] + +Only coordinate `x` can become newly positive, while subtracting at `y` can +only delete a positive coordinate. Hence a legal support can grow past `K` +only by starting with exactly `K` positives, crossing zero at `x`, and not +losing a positive at `y`. These are exactly (4a)--(4c). Conversely those +three conditions increase the positive support from `K` to `K+1`. QED. + +This is a dynamic trace relation: two distinct live events form an +executable commuting square precisely when neither corresponding instance of +(4) holds. + +### Mutual live locks at `z=0` + +Consider live events `A=(x_s -> y)` and `B=(u_t -> v)` which are both legal +at `z=0` and mutually disable one another. + +If `x=u`, put `E=-d_x`. Applying (4b) in the two directions gives + +\[ + \max(s,t)\le Es`; the reverse disabling would require `d_x+s>t`. +Since `d_x,d_u<=0`, these imply both `t>s` and `s>t`. + +The same direct-swap corollary holds at `z=1`. There the distinct old colors +are the two nonpositive anchors and the remaining two colors are positive. + +### First-exhaustion version + +Let + +\[ + A=(x_s\xrightarrow{\text{final }y^{7-s}}\varnothing) +\] + +be the first exhausting event. Its debt increment is + +\[ + s e_x+(7-s)e_y, \tag{9} +\] + +and the threshold rises from two to three. For a different source `B`, with +`w` as in (3), `A` disables `B` if and only if + +\[ +\begin{aligned} + |\operatorname{Pos}(w)|&=2,\\ + w_x&\le0=1`, then + +\[ + (7-s)+\sum_{i=1}^m\ell_i\le7, + \qquad\text{hence}\qquad + \sum_i\ell_i\le s\quad\text{and}\quad m\le s. \tag{11} +\] + +Thus a four-way common-`f` lock (`m=3`) is impossible for `s<=2`. It is not +impossible at height seven: `s=3` and three singleton `f` runs saturate the +budget exactly. Section 4 gives such an example. + +## 2. The four-source all-`q`/all-`f` star + +Use colors `(q,f,g,h)`. The all-`q` parent of a same-source-color first +exhaustion bridge has + +\[ + d(P)=(-Q,0,p_g,p_h), + \qquad + Q=p_g+p_h=s+E, \tag{12} +\] + +where `s` is the bad cap, `0<=E<=2`, and the bad event exhausts to +`f^{7-s}`. Let the three sibling caps be `c_1,c_2,c_3`. In the all-`f` +star considered here, each sibling's fixed next event is live into `f`. +All four sources are legal, so their caps are at most `Q`; the three sibling +caps also satisfy `c_i>E`, because they survive in the terminal `Tq` child. + +The exposed `q` count is + +\[ + F_q=s+c_1+c_2+c_3-Q=c_1+c_2+c_3-E\le7. \tag{13} +\] + +Since all four current tops are `q`, there are no `f`, `g`, or `h` hosts. +Consequently the four already exposed physical prefixes contain + +\[ + F_f=0, + \qquad F_g=p_g, + \qquad F_h=p_h. \tag{14} +\] + +In particular, their total non-`q` mass is exactly + +\[ + F_g+F_h=Q, \tag{15} +\] + +and it consists only of `g` and `h`. Every prefix ends in `q`. + +### The forward cap-sum alternative + +After a live sibling of cap `c_i` enters `f`, the two anchor energies are + +\[ + A_q=Q-c_i, + \qquad A_f=c_i. \tag{16} +\] + +An untouched `q` sibling of cap `c_j` remains legal exactly when + +\[ + c_j\le Q-c_i + \quad\Longleftrightarrow\quad + c_i+c_j\le Q. \tag{17} +\] + +Thus (17) gives an executable forward square and, in particular, the first +entry does not land in an immediate `D2` terminal. + +Moreover, if no pair of sibling caps satisfies (17), then `Q<=7`. The only +possible larger value is `Q=8`. Since `s<=6` and `E<=2`, it forces +`s=6,E=2`. Equations (13) and `c_i>E` then give + +\[ + 3\le c_i, + \qquad c_1+c_2+c_3\le9, +\] + +so `c_1=c_2=c_3=3`, and every sibling pair has sum `6<=8`, a contradiction. + +### Solo-prefix lemma + +Let `u` be one column's already exposed word in initial-top to current-border +order. Suppose that `u` uses at most two colors. Starting at zero debt, all +past border events of this one column may be performed before any other +column's past event. + +To see this, stop at any current source in `u`, of top color `a` and cap +`r`. Let `n_c` count exposed occurrences of color `c` in the corresponding +prefix of `u`. This one column contributes + +\[ + d_c=n_c-r[c=a]. \tag{18} +\] + +Its source test adds back `r e_a` and is exactly the nonnegative count vector +`n`. Its positive support is therefore the set of colors seen so far, of +size at most two. This proves every event legal, including the source test +at the final `q` gate. + +If the forward cap-sum alternative is absent, `Q<=7`. Were all four exposed +prefixes to contain both `g` and `h`, (15) would be at least eight. Hence at +least one prefix uses only `q` and at most one of `{g,h}` and is covered by +the solo-prefix lemma. + +### When the naive early `q -> f` is itself terminal + +Let a two-color prefix use `q` and `x` and omit the other color `y`. Perform +it solo and immediately take its fixed `q -> f` event. This may be either a +live sibling event or the bad exhaustion. + +If it is live, with `m` exposed `x` items and `k` exposed `q` items, the +successor debts are + +\[ + (d_q,d_f,d_x,d_y)=(k,-(k+m),m,0). \tag{19} +\] + +If it is the bad exhaustion, the successor has `z=1` and + +\[ + (d_q,d_f,d_x,d_y)=(k,7-k-m,m,0). \tag{20} +\] + +For `m=0` neither state is terminal. For `m>0`, (19) is an immediate `D2`, +or (20) an immediate `Tq`, exactly when all three other initial top colors +are `y`. Any source already topped by a positive color remains legal. + +If a second two-color prefix exists in this exceptional situation, its top +is `y`, so it omits `x`. Choosing that second prefix instead leaves at least +two of the other sources topped by the now-positive color `y`; the early +event is not terminal. Thus the only case not already bypassed has exactly +one two-color prefix. + +By (15), this forces the following rigid pattern: + +\[ + Q=7; \tag{21} +\] + +- the unique two-color prefix `A` contains exactly one `x` and no `y`; +- each other prefix contains exactly one `x` and one `y`; and +- all three other prefixes start with their unique `y`. + +### The rigid `Q=7` weave + +Choose one of the other prefixes and call it `B`. It has the form + +\[ + B=yq^a xq^b, + \qquad a\ge0,quad b\ge1. \tag{22} +\] + +Advance `B` only until its unique `x` becomes the current top. If `a=0` +this is the single event `y_1 -> x_2`; otherwise it is +`y_1 -> q_{a+1} -> x_{a+2}`. Both source tests see at most `y,q` and are +legal. At that point `B` contributes, in order `(q,f,x,y)`, + +\[ + d^{B}=(a,0,-a-1,1). \tag{23} +\] + +Now perform all of `A`'s past events. In any source test, let `n_q,n_x` be +the exposed counts of `A` so far. Since `A` contains only one `x`, the test +vector is + +\[ + d^{B}+(n_q,0,n_x,0), \tag{24} +\] + +whose `x` coordinate is at most `-a` and whose only possible positive +coordinates are `q` and `y`. Every event of `A`, and its final `q -> f` +source test, is therefore legal. + +Let `c` be `A`'s cap at its `q` gate. Immediately before the `q -> f` +event, the debts are `(a-1,0,-a,1)`. If `A` is a live sibling, afterward + +\[ + d=(a+c-1,-c,-a,1),qquad z=0. \tag{25} +\] + +If `A` is the bad source of cap `s=c`, afterward + +\[ + d=(a+s-1,7-s,-a,1),qquad z=1. \tag{26} + +The two untouched prefixes still start with `y`. Since `d_y=1`, their +source tests have respectively two positives in (25) and three positives in +(26). They are legal. Thus neither woven successor is terminal. + +### Past--future bypass theorem + +For a height-seven all-`q` parent (12) with four legal sources and a fixed +all-`f` star below it, at least one of the following holds. + +1. Two sibling caps have sum at most `Q`; taking the first live entry leaves + the second source legal. +2. From the true zero-debt past, a legal prefix schedule takes one of the + star's `q -> f` events before reaching the all-`q` parent and lands in a + state with another legal source. + +**Proof.** If (17) holds, use the forward square. Otherwise `Q<=7`, so a +two-color prefix exists by (15). Its solo early event works unless it has +the exceptional terminal form described above. A second two-color prefix +then gives a nonterminal choice. With exactly one such prefix, (21)--(26) +give the rigid weave. QED. + +This theorem proves that the displayed local star is not an unavoidable +one-step barrier from its zero-debt past. It does **not** prove that the +state produced in item 1 or 2 is checkpoint-YES. + +## 3. A tight four-way local lock at height seven + +The following balanced instance shows why the qualifier above is necessary. +Colors `q,f,g,h` are encoded as `0,1,2,3`; columns are written bottom to top. + +```text +height=7 +colors=4 +empty=2 +column=2221032 +column=3321023 +column=3321003 +column=1111000 +``` + +In top-to-bottom order the four words are + +```text +ghqfggg +hgqfghh +hqqfghh +qqqffff +``` + +Each color occurs seven times. The legal past event sequence + +```text +0,1,0,1,2 +``` + +is + +```text +g1 -> h2, +h1 -> g2, +h2 -> q3, +g2 -> q3, +h1 -> q3. +``` + +It reaches + +\[ + d(P)=(-5,0,2,3), + \qquad \text{tops }q_3,q_3,q_3,q_3. \tag{27} +\] + +All four sources are legal. Exhausting the last column through `f^4` +gives + +\[ + z=1,qquad d=(-2,4,2,3),qquad\text{tops }q_3^3, +\] + +an immediate `Tq` terminal. Taking any of the other three `q_3 -> f_4` +events gives + +\[ + z=0,qquad d=(-2,-3,2,3), + \qquad\text{tops }f_4,q_3,q_3,q_3, +\] + +an immediate `D2` terminal. The common `f` inventory is tight: +`4+1+1+1=7`. + +Nevertheless the initial layout is YES. One complete legal border sequence +is + +```text +0,0,1,0,2,2,0,1,1,1,1,2,2,3. +``` + +Its decisive beginning is + +\[ +\begin{array}{c|c} +\text{event}&d=(q,f,g,h)\\ \hline +0:g_1\to h_2&(0,0,1,-1)\\ +0:h_2\to q_3&(-2,0,1,1)\\ +1:h_1\to g_2&(-2,0,0,2)\\ +0:q_3\to f_4&(1,-3,0,2). +\end{array} +\] + +The trap path first makes both `g` and `h` positive and only then enters +`f`. The bypass keeps `g` suppressed at zero and moves `q_3 -> f_4` early. +This is the concrete mechanism behind the solo-prefix and rigid-weave +arguments: control the zero-debt past so that the second positive color has +not yet activated when the new anchor is entered. + +## 4. Independent finite checks + +`tests/check_c4_h7_critical_pair_bypass.py` performs no large instance +enumeration. It independently: + +- exhausts small integer boxes to compare (4) and (10) with direct positive + support counts; +- checks the mutual-lock consequences and the impossibility of (8); +- enumerates the height-seven cap constraints behind the `Q=8` argument and + the color charge (11); +- enumerates all `Q<=7` distributions of `g,h` over four prefixes and checks + the unique rigid `Q=7` corner; +- checks the rigid weave for every small word of the stated form; and +- replays the displayed instance, its route to (27), all four terminal + children, and the complete winning border sequence. + diff --git a/docs/c4-h7-rainbow-lift.md b/docs/c4-h7-rainbow-lift.md new file mode 100644 index 0000000..f54c220 --- /dev/null +++ b/docs/c4-h7-rainbow-lift.md @@ -0,0 +1,309 @@ +# Rainbow deletion and token lifting for four colours + +This note develops a route from the known universal height-six result toward +the unresolved balanced four-colour, height-seven, two-empty-column case. It +does **not** prove that every height-seven layout is solvable. Its purpose is +to isolate a global piece of structure that is absent from the current +terminal-state census and to state exactly what remains to be proved. + +Columns are labelled $0,1,2,3$, colours are labelled $0,1,2,3$, every +column has height $H$, and every colour occurs $H$ times. A *cell* below +always means a labelled physical occurrence, not merely a column-colour pair. + +## 1. Seven disjoint rainbow deletions + +For a layout $I$, let + +\[ +n_{ic}=\#\{\text{cells of colour }c\text{ in column }i\}. +\] + +Make a bipartite multigraph $B_I$. Its left vertices are the four columns, +its right vertices are the four colours, and each physical $c$-cell in +column $i$ is one edge from $i$ to $c$. Every vertex has degree $H$: +a column contains $H$ cells, and balance gives $H$ cells of every colour. + +### Rainbow-factorization lemma + +The $4H$ physical cells of every balanced layout can be partitioned into +$H$ sets + +\[ +T_1,\ldots,T_H, +\] + +such that every $T_r$ contains exactly one cell from each column and exactly +one cell of each colour. + +**Proof.** For any set $X$ of column vertices, $H|X|$ edges leave $X$. +They end in $N(X)$, whose total degree is $H|N(X)|$. Hence +$H|X|\le H|N(X)|$, so Hall's condition holds and $B_I$ has a perfect +matching. Delete that matching. Every vertex degree decreases by one, so +the remainder is $(H-1)$-regular. Repeat. After $H$ rounds no edge +remains. QED. + +Deleting one $T_r$ removes one cell from every column and one occurrence of +every colour. The result $I-T_r$ is therefore a balanced height-$(H-1)$ +layout. In particular, every balanced $4\times7$ layout has seven labelled +balanced height-six children. + +This is already a useful change of quantifiers. Since every balanced +height-six child is YES, a hypothetical height-seven NO layout must defeat +the lifting of a height-six winning path for **each of seven disjoint cell +transversals**. Merely observing that the children are YES is not enough: +solvability is not known to be monotone under arbitrary internal insertion. + +## 2. Thick transversals and the exact Hall alternative + +A selected cell is *thick* if its maximal monochrome run in the parent has +length at least two. Deleting one cell from such a run shortens the run but +does not change the sequence of run colours. A transversal is thick if all +four of its cells are thick. + +Define a simple bipartite graph $B_I^{\rm thick}$: column $i$ is adjacent +to colour $c$ exactly when column $i$ has a $c$-run of length at least +two. + +### Thick-transversal dichotomy + +Exactly one of the following holds. + +1. $B_I^{\rm thick}$ has a perfect matching. Choosing one cell from the + corresponding thick run in each column gives a run-skeleton-preserving + rainbow deletion. +2. There is a nonempty colour set $S$ for which + + \[ + |N_{B_I^{\rm thick}}(S)|<|S|. + \] + +**Proof.** This is Hall's theorem applied to the four-by-four thick support +graph. The two cases are mutually exclusive and exhaustive. QED. + +The second case is not a failure of the method. It is a small structural +branch: every rainbow transversal must use at least one singleton occurrence +from the Hall-deficient colours. The witness consists of at most four +colours and at most three neighbouring columns. + +Singletons must not be hidden inside a claimed lift. Deleting an endpoint +singleton removes one parent border. Deleting an internal singleton removes +one border when its two neighbours have different colours and two borders +when the neighbours have the same colour. Thus a height-six edge need not be +one parent edge. A separate one- or two-border local detour is required. +The same $F-G$ bookkeeping can be re-derived at an individually aligned +checkpoint, but there is no canonical edge-by-edge child path through the +extra parent borders. Accordingly, the checker below does not apply the +token-lift lemma to a singleton transversal; it reports that branch for a +separate detour proof. + +## 3. Exact perturbation made by four thick tokens + +Let $J$ have height $h$, let $I$ have height $H=h+1$, and suppose +$J$ is obtained from $I$ by deleting a thick rainbow transversal. The +two layouts have identical run-colour skeletons. Index a common top-border +checkpoint by the number of exposed runs in each column. + +For a checkpoint $x$, write: + +- $E(x)$ for the columns whose selected token lies in an exposed run; +- $A(x)$ for the active, non-exhausted columns; +- $t_j$ for the token colour in column $j$; +- $a_j(x)$ for the current top-border colour of active column $j$; +- $e_c$ for the unit vector of colour $c$. + +For a candidate active source $i$, let + +\[ +D_i=d+s_i e_{a_i} +\] + +be its Ito source-test vector. The source is legal precisely when + +\[ +|\operatorname{pos}(D_i)|\le 2+z, +\] + +where $z$ is the common number of exhausted original columns. + +### Token-error lemma + +At every common checkpoint and for every active source $i$, + +\[ +\boxed{ +D_i^{I}-D_i^{J} += +\sum_{j\in E(x)} e_{t_j} +- +\sum_{j\in E(x)\cap A(x),\ j\ne i} e_{a_j(x)}. +} +\tag{1} +\] + +**Proof.** Every exposed token contributes one item of its own colour, so + +\[ +F^{I}-F^{J}=\sum_{j\in E(x)}e_{t_j}. +\] + +If column $j$ is active and its token is exposed, its exposed host capacity +is one larger in $I$, assigned to its current top colour. Therefore + +\[ +G^{I}-G^{J} +=\sum_{j\in E(x)\cap A(x)}e_{a_j(x)}. +\] + +Finally, when the source token is exposed, +$s_i^I-s_i^J=1$. The added $e_{a_i}$ in the source term cancels the +source's own contribution in the second sum. Substitution into +$D_i=F-G+s_ie_{a_i}$ gives (1). QED. + +The formula is sparse and contains only four labelled tokens. It also gives +the checksum + +\[ +\sum_c(D_i^{I}-D_i^{J})_c +=z+\mathbf 1[i\in E(x)], +\] + +because every exhausted column has exposed its token. + +### Compatible-lift lemma + +Suppose a common-skeleton path starts at the initial checkpoint, reaches two +exhausted columns, and at every step its chosen source is legal in $J$ and, +after applying (1), legal in $I$. Then the same source sequence is a legal +top-border path for $I$, so $I$ is solvable. + +This follows by induction over the path. Thick deletion gives the same next +run-colour edge in both layouts, and the hypothesis gives its legality in +both. The paths therefore remain at corresponding checkpoints until the +two-exhausted-column finishing frontier. + +A convenient sufficient test at a step is that the positive part introduced +by the error vector lies entirely inside the child's existing positive +support. More generally, it is enough that the number of newly positive +coordinates does not exceed + +\[ +(2+z)-|\operatorname{pos}(D_i^J)|. +\] + +This is a checkable condition, not yet an existence theorem. The missing +global assertion is: + +> Every balanced height-seven layout has either a thick transversal with a +> compatible height-six winning path, or a bounded singleton detour from the +> Hall-deficient branch. + +Proving that statement would settle height seven. Failure produces a small +counter-witness: a Hall set, or four labelled tokens plus the first child- +legal/parent-illegal source test. + +## 4. An independent sequential-column bypass + +The deletion route also suggests a cheap global pruning lemma. For a column +$i$, let $S_i$ be the set of all colours in it and let $U_i$ be the set +of colours above its maximal bottom run. + +### Two-column support lemma + +If two distinct columns $i,j$ satisfy + +\[ +|U_i|\le2, +\qquad +|S_i\cup U_j|\le3, +\tag{2} +\] + +then the layout is solvable. + +**Proof.** First dispose of initially monochrome columns. If there are two, +the finishing frontier is already reached. If there is exactly one and it is +column $i$, start with the second paragraph below. If it is a different +column, its one colour together with $U_i$ has support at most three; the +existing monochrome column supplies the third bin, so advancing $i$ alone +reaches the finishing frontier. + +It remains to consider the case with no initially monochrome column, where +$d=0$. Advance only column $i$. Immediately before each of its borders is +removed, its source-test vector telescopes to the colour-count vector of the +currently exposed top prefix of that column. The last test excludes the +hidden bottom run. Condition $|U_i|\le2$ therefore makes every step legal +with the original two bins, and column $i$ is exhausted. + +Now advance only column $j$. Its source-test vector is the full colour- +count vector of exhausted column $i$, plus the colour-count vector of the +currently exposed top prefix of $j$. Before $j$'s last border, its +positive support is contained in $S_i\cup U_j$, of size at most three. +There are $2+1=3$ bins after the first exhaustion, so every step is legal +and $j$ is exhausted. The two-exhausted-column frontier finishes the +puzzle. QED. + +Consequently, any height-seven NO must violate (2) for all twelve ordered +column pairs. This condition is independent of D2/Tq terminal labels and is +cheap enough to use before any suffix expansion. + +## 5. What a height-seven NO would force at height eight + +The balanced bottom-layer monotonicity theorem gives a second global +necessary condition. If a balanced height-seven layout $I$ were NO, then +for every permutation $\pi$ of the four colours, inserting + +\[ +\pi(0),\pi(1),\pi(2),\pi(3) +\] + +as a new labelled bottom layer would produce a balanced height-eight NO +layout $I^\pi$. Thus one hypothetical labelled height-seven NO forces a +family of 24 labelled height-eight NO extensions sharing the same 28-cell +core. + +This implication is one-way. A height-eight NO can have a solvable balanced +height-seven deletion, as the committed height-eight witnesses already show. +Likewise, finding a height-seven core whose 24 extensions are NO would be a +necessary signature, not by itself a certificate that the core is NO. On +the other hand, proving that every height-seven core has at least one YES +rainbow-bottom extension would immediately rule out a height-seven NO. + +The three committed height-eight witnesses do not settle this subproblem. +Their labelled bottom-colour multiplicities are not rainbow; for the +symmetric witness the bottom row is (2,2,0,0). + +## 6. Independent checker + +[`check_c4_h7_rainbow_lift.py`](../tests/check_c4_h7_rainbow_lift.py) +implements the finite assertions in this note without using the production +border oracle. + +For each input layout it: + +1. constructs an $H$-factorization of the physical occurrence multigraph; +2. verifies that every factor deletes to a balanced height-$(H-1)$ child; +3. enumerates the thick support matchings, or emits an explicit Hall witness; +4. checks equation (1) coordinate by coordinate at every explored + child-legal source; +5. searches for a path legal in both the child and parent skeletons; +6. reports singleton-created borders instead of treating them as common + edges; +7. reports all ordered pairs covered by (2); and +8. for a height-seven input, exactly classifies its 24 labelled rainbow-bottom + height-eight extensions. + +The built-in regressions are the symmetric certified height-eight four-lock +NO and one true zero-debt height-seven member of the two-source D2 near-kernel. +The latter is intentionally a global YES even though its distinguished +nonzero-debt checkpoint is locally losing. + +Run it with + +```text +python tests/check_c4_h7_rainbow_lift.py +``` + +or add a plain repository instance with `--instance`. A reported compatible +path proves that one layout is YES. Absence of such a path proves only that +this thick-transversal lift did not close that layout; it is neither a Water +Sort NO certificate nor a universal height-seven conclusion. diff --git a/tests/check_c4_h7_anchor_pair_potential.py b/tests/check_c4_h7_anchor_pair_potential.py new file mode 100644 index 0000000..8b94fcd --- /dev/null +++ b/tests/check_c4_h7_anchor_pair_potential.py @@ -0,0 +1,664 @@ +#!/usr/bin/env python3 +"""Audit the c=4, h=7 anchor-pair potential and its bridge ledger. + +This checker does not expand residual words. It reuses the independent +first-exhaustion arithmetic in ``check_c4_h7_tq_exhaust_siblings.py`` to +reconstruct semantic bridge edges and to count a fixed card decoration by +multinomial/Hall arithmetic. It separately reuses the integer-partition +terminal generator in ``test_c4_h7_macro_recon_independent.py``. + +The input report must be the complete production first-exhaustion report. +Only the new E=2 and first-sweep D2 classifications are asserted here; this +script does not claim that the remaining D2 family is solved. +""" + +from __future__ import annotations + +import argparse +import importlib.util +import itertools +import json +import sys +from collections import Counter, defaultdict +from pathlib import Path +from types import ModuleType +from typing import Iterable, NoReturn, Sequence + + +HEIGHT = 7 +COLORS = 4 +TESTS = Path(__file__).resolve().parent + +EXPECTED_TERMINALS = {"tq": 71, "d2_3plus1": 265, "d2_2plus2": 661} +EXPECTED_TQ_ENERGY = {0: 44, 1: 20, 2: 7} +EXPECTED_D31_ENERGY = {2: 70, 3: 54, 4: 76, 5: 44, 6: 18, 7: 3} +EXPECTED_D22_ENERGY = { + 2: 117, + 3: 102, + 4: 162, + 5: 108, + 6: 93, + 7: 42, + 8: 28, + 9: 6, + 10: 3, +} + +# key = (bad_source_equals_q, parent_legal_source_count, Tq energy E) +# value = (canonical edges carrying D2 cards, decorations, residual-word weight) +EXPECTED_D2_LEDGER = { + (False, 4, 0): (154, 33_180, 2_530_458_586), + (False, 4, 1): (72, 9_187, 24_249_002), + (False, 4, 2): (18, 1_369, 57_090), + (True, 2, 0): (1, 132, 12_012), + (True, 2, 1): (1, 58, 924), + (True, 3, 0): (11, 1_529, 1_106_028), + (True, 3, 1): (1, 6, 462), + (True, 4, 0): (75, 15_392, 312_621_168), + (True, 4, 1): (40, 5_372, 15_314_415), + (True, 4, 2): (12, 981, 39_018), +} + +# value = (edges, parents, decorations, residual-word weight, signatures) +EXPECTED_FIRST_SWEEP = { + 0: (41, 41, 304, 322_825, 133), + 1: (9, 9, 17, 242, 9), + 2: (0, 0, 0, 0, 0), +} + + +def require(condition: bool, message: str) -> None: + if not condition: + raise AssertionError(message) + + +def fail(message: str) -> NoReturn: + raise AssertionError(message) + + +def load_module(name: str, path: Path) -> ModuleType: + require(path.is_file(), f"missing shared checker module: {path}") + spec = importlib.util.spec_from_file_location(name, path) + require(spec is not None and spec.loader is not None, f"cannot load {path}") + module = importlib.util.module_from_spec(spec) + # Dataclasses resolve forward annotations through sys.modules while the + # module body is executing. + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def read_report(path: Path) -> dict[str, object]: + require(path.is_file(), f"missing first-exhaustion report: {path}") + value = json.loads(path.read_text(encoding="utf-8")) + require(isinstance(value, dict), "report root must be an object") + return value + + +def check_two_anchor_integer_box(fork: ModuleType) -> dict[str, int]: + """Exhaust the tiny debt/cap box behind Lemmas 1 and 2.""" + + source_tests = 0 + live_returns = 0 + vector_splits = 0 + direct_anchor_transfers = 0 + for energy_a in range(HEIGHT + 1): + for energy_b in range(HEIGHT + 1): + total = energy_a + energy_b + for exposed_x in range(1, HEIGHT + 1): + exposed_y = total - exposed_x + if not 1 <= exposed_y <= HEIGHT: + continue + debts = [-energy_a, -energy_b, exposed_x, exposed_y] + for color, energy in ((0, energy_a), (1, energy_b)): + for cap in range(1, HEIGHT): + actual = fork.source_is_legal(debts, 0, color, cap) + require( + actual == (cap <= energy), + "two-anchor fitting test failed", + ) + source_tests += 1 + + for departure in range(1, min(energy_a, HEIGHT - 1) + 1): + # w is the old cap of the final non-anchor -> anchor edge. + # w<=5 leaves room for a live endpoint T with w= 0, "anchor energy became negative") + require( + sum(after) == total + increment, + "anchor energy increment used the wrong endpoint", + ) + live_returns += 1 + for delta_x in range(increment + 1): + delta_y = increment - delta_x + after_vector = ( + exposed_x + delta_x, + exposed_y + delta_y, + ) + require( + after_vector[0] >= exposed_x + and after_vector[1] >= exposed_y + and sum(after_vector) + == exposed_x + exposed_y + increment, + "complement vector is not coordinatewise monotone", + ) + vector_splits += 1 + + # Direct alpha -> beta: the endpoint advances, but debt + # transfer uses the old cap and complement exposure is + # unchanged. + for endpoint in range(departure + 1, HEIGHT): + after = (energy_a - departure, energy_b + departure) + require(min(after) >= 0, "direct transfer went negative") + require( + sum(after) == total, + "direct transfer changed total anchor energy", + ) + require(endpoint > departure, "direct border did not advance") + direct_anchor_transfers += 1 + + # Symmetric beta -> alpha direct transfers. + for departure in range(1, min(energy_b, HEIGHT - 1) + 1): + for endpoint in range(departure + 1, HEIGHT): + after = (energy_a + departure, energy_b - departure) + require(min(after) >= 0, "direct transfer went negative") + require( + sum(after) == total, + "direct transfer changed total anchor energy", + ) + require(endpoint > departure, "direct border did not advance") + direct_anchor_transfers += 1 + require( + source_tests > 0 and live_returns > 0 and direct_anchor_transfers > 0, + "integer box was empty", + ) + return { + "source_tests": source_tests, + "live_return_formulas": live_returns, + "complement_increment_splits": vector_splits, + "direct_anchor_transfers": direct_anchor_transfers, + } + + +def check_terminal_macros(macro: ModuleType) -> dict[str, object]: + tq = macro.tq_types() + d31 = macro.d2_3plus1_types() + d22 = macro.d2_2plus2_types() + require( + (len(tq), len(d31), len(d22)) + == ( + EXPECTED_TERMINALS["tq"], + EXPECTED_TERMINALS["d2_3plus1"], + EXPECTED_TERMINALS["d2_2plus2"], + ), + "terminal macro census drifted", + ) + + for _, state in (*tq, *d31, *d22): + require( + macro.physical_consistency_errors(state) == (), + "terminal macro failed physical checks", + ) + require( + not any( + macro.legal_source(state, source) + for source in range(len(state.active)) + ), + "enumerated terminal has a legal source", + ) + + tq_energy = Counter(energy for energy, _ in tq) + d31_energy = Counter(energy for energy, _ in d31) + d22_energy = Counter(energy for energy, _ in d22) + require(dict(tq_energy) == EXPECTED_TQ_ENERGY, "Tq energy distribution drifted") + require(dict(d31_energy) == EXPECTED_D31_ENERGY, "3+1 energy distribution drifted") + require(dict(d22_energy) == EXPECTED_D22_ENERGY, "2+2 energy distribution drifted") + + e2_types = [] + for energy, state in tq: + if energy != 2: + continue + caps = tuple(cap for _, cap in state.active) + exposed = macro.exposed_counts(state) + require(caps == (3, 3, 3), "E=2 Tq caps are not 3,3,3") + require(exposed[0] == HEIGHT, "E=2 Tq did not saturate q") + e2_types.append(state) + require(len(e2_types) == 7, "wrong number of E=2 Tq macro types") + + saturated_d31 = [ + state + for _, state in d31 + if HEIGHT in [value for value in state.d if value > 0] + ] + saturated_d22 = [ + state + for _, state in d22 + if HEIGHT in [value for value in state.d if value > 0] + ] + require(not saturated_d31, "a saturated-positive 3+1 D2 escaped the bound") + require( + len(saturated_d22) == 10, + "saturated-positive 2+2 D2 count drifted", + ) + return { + "terminal_types": EXPECTED_TERMINALS, + "tq_energy_distribution": dict(sorted(tq_energy.items())), + "d2_3plus1_energy_distribution": dict(sorted(d31_energy.items())), + "d2_2plus2_energy_distribution": dict(sorted(d22_energy.items())), + "e2_tq_types": len(e2_types), + "saturated_positive_d2_3plus1": len(saturated_d31), + "saturated_positive_d2_2plus2": len(saturated_d22), + } + + +def reconstruct_edges(fork: ModuleType): + terminals = fork.enumerate_tq_terminals() + _, pairs = fork.reverse_bridge(terminals) + edges = fork.build_sibling_edges(pairs) + require(len(edges) == 423, "sibling bridge edge count drifted") + e2_edges = [] + for edge in edges: + terminal_debts = fork.terminal_debts_in_parent_coordinates(edge) + energy = -terminal_debts[edge.q_color] + require(0 <= energy <= 2, "bridge Tq energy is outside 0..2") + if energy != 2: + continue + require(edge.q_caps == (3, 3, 3), "E=2 bridge q caps drifted") + require( + fork.exposed_counts(edge.parent)[edge.q_color] == HEIGHT, + "E=2 bridge parent has a hidden q item", + ) + e2_edges.append(edge) + require(len(e2_edges) == 36, "E=2 sibling bridge edge count drifted") + return edges + + +def report_d2_ledger( + report: dict[str, object], fork: ModuleType, edges: Sequence[object] +) -> tuple[dict[tuple[bool, int, int], tuple[int, int, int]], dict[str, int]]: + require( + report.get("coverage_scope") + == "first_exhaustion_tq_sibling_next_run_forks", + "wrong report scope", + ) + require(report.get("status") == "NEXT_RUN_CENSUS_COMPLETE", "report is not complete") + require(report.get("next_run_universe_complete") is True, "report lacks completion flag") + rows = report.get("per_edge") + require(isinstance(rows, list) and len(rows) == 423, "report must contain 423 edges") + + by_key = { + (edge.parent, edge.terminal, edge.action): edge # type: ignore[attr-defined] + for edge in edges + } + seen = set() + grouped_edges: Counter[tuple[bool, int, int]] = Counter() + grouped_decorations: Counter[tuple[bool, int, int]] = Counter() + grouped_words: Counter[tuple[bool, int, int]] = Counter() + for raw in rows: + require(isinstance(raw, dict), "per_edge row must be an object") + semantic = fork.edge_key_from_json(raw) + require(semantic in by_key and semantic not in seen, "unknown/duplicate report edge") + seen.add(semantic) + edge = by_key[semantic] + legal_count = len(fork.legal_sources(edge.parent, 0)) + require(raw.get("legal_source_count") == legal_count, "legal-source count drifted") + terminal_debts = fork.terminal_debts_in_parent_coordinates(edge) + energy = -terminal_debts[edge.q_color] + refined = raw.get("refined") + require(isinstance(refined, dict), "missing refined per-edge ledger") + d2 = refined.get("d2_reduction") + require(isinstance(d2, dict), "missing per-edge D2 ledger") + decorations = d2.get("decorations") + words = d2.get("residual_words") + require( + isinstance(decorations, int) + and decorations >= 0 + and isinstance(words, int) + and words >= 0, + "invalid D2 counts", + ) + if decorations == 0: + require(words == 0, "zero-decoration D2 row has nonzero weight") + continue + key = (edge.a_equals_q, legal_count, energy) + grouped_edges[key] += 1 + grouped_decorations[key] += decorations + grouped_words[key] += words + require(seen == set(by_key), "report edge coverage is incomplete") + + ledger = { + key: (grouped_edges[key], grouped_decorations[key], grouped_words[key]) + for key in grouped_edges + } + require(ledger == EXPECTED_D2_LEDGER, "D2 E/source ledger drifted") + totals = { + "edges_with_d2": sum(value[0] for value in ledger.values()), + "decorations": sum(value[1] for value in ledger.values()), + "residual_word_weight": sum(value[2] for value in ledger.values()), + "e2_edges": sum(value[0] for key, value in ledger.items() if key[2] == 2), + "e2_decorations": sum(value[1] for key, value in ledger.items() if key[2] == 2), + "e2_residual_word_weight": sum( + value[2] for key, value in ledger.items() if key[2] == 2 + ), + } + require( + totals + == { + "edges_with_d2": 385, + "decorations": 67_206, + "residual_word_weight": 2_883_858_705, + "e2_edges": 30, + "e2_decorations": 2_350, + "e2_residual_word_weight": 96_108, + }, + "D2 totals drifted", + ) + return ledger, totals + + +def raw_first_sweep_is_d2( + edge: object, chosen: tuple[tuple[int, int], ...] +) -> bool: + debts = [debt for debt, _ in edge.parent] # type: ignore[attr-defined] + caps = [list(values) for _, values in edge.parent] # type: ignore[attr-defined] + q_color = edge.q_color # type: ignore[attr-defined] + for old_cap, (new_color, endpoint) in zip(edge.q_caps, chosen): # type: ignore[attr-defined] + caps[q_color].remove(old_cap) + caps[new_color].append(endpoint) + debts[q_color] += old_cap + debts[new_color] -= old_cap + + positive = {color for color, debt in enumerate(debts) if debt > 0} + nonpositive = set(range(COLORS)) - positive + topped = {color for color, values in enumerate(caps) if values} + if len(positive) != 2 or len(nonpositive) != 2 or topped != nonpositive: + return False + if sorted(len(caps[color]) for color in nonpositive) != [2, 2]: + return False + for color in nonpositive: + for cap in caps[color]: + adjusted = debts.copy() + adjusted[color] += cap + if sum(value > 0 for value in adjusted) <= 2: + return False + + exposed = [debts[color] + sum(caps[color]) for color in range(COLORS)] + multiplicity = [len(caps[color]) for color in range(COLORS)] + if any( + not multiplicity[color] <= exposed[color] <= HEIGHT + for color in range(COLORS) + ): + return False + remaining = [HEIGHT - value for value in exposed] + return all( + multiplicity[color] + <= sum(remaining[other] for other in range(COLORS) if other != color) + for color in range(COLORS) + ) + + +def theoretical_first_sweep_signatures() -> dict[int, set[tuple[object, ...]]]: + result = {0: set(), 1: set(), 2: set()} + for energy in range(3): + for bad_cap, anchor_a, old_a, old_f1, old_f2, end_a, end_f1, end_f2 in itertools.product( + range(1, HEIGHT), + range(HEIGHT), + range(energy + 1, HEIGHT), + range(energy + 1, HEIGHT), + range(energy + 1, HEIGHT), + range(1, HEIGHT), + range(1, HEIGHT), + range(1, HEIGHT), + ): + anchor_f = old_f1 + old_f2 + if not (old_a < end_a and old_f1 < end_f1 and old_f2 < end_f2): + continue + if not ( + anchor_a + energy > 0 + and 1 <= bad_cap - anchor_a <= HEIGHT + and old_a + old_f1 + old_f2 - energy <= HEIGHT + ): + continue + if not ( + bad_cap > anchor_a + old_a + and end_a > anchor_a + old_a + and end_f1 > anchor_f + and end_f2 > anchor_f + ): + continue + if (end_f1 - old_f1) + (end_f2 - old_f2) > bad_cap: + continue + if end_a - old_a > HEIGHT - (bad_cap - anchor_a): + continue + result[energy].add( + ( + bad_cap, + anchor_a, + old_a, + end_a, + tuple(sorted(((old_f1, end_f1), (old_f2, end_f2)))), + ) + ) + return result + + +def first_sweep_ledger(fork: ModuleType, edges: Sequence[object]) -> dict[str, object]: + counts: Counter[int] = Counter() + weights: Counter[int] = Counter() + edge_sets: dict[int, set[object]] = defaultdict(set) + parent_sets: dict[int, set[object]] = defaultdict(set) + signatures: dict[int, set[tuple[object, ...]]] = defaultdict(set) + + for edge in edges: + if edge.a_equals_q: # type: ignore[attr-defined] + continue + terminal_debts = fork.terminal_debts_in_parent_coordinates(edge) + energy = -terminal_debts[edge.q_color] # type: ignore[attr-defined] + anchor_a, bad_cap, anchor_f = edge.action # type: ignore[attr-defined] + anchor_a_energy = -edge.parent[anchor_a][0] # type: ignore[attr-defined] + fourth = next( + color + for color in range(COLORS) + if color not in (edge.q_color, anchor_a, anchor_f) # type: ignore[attr-defined] + ) + + for a_slot in range(3): + f_slots = [slot for slot in range(3) if slot != a_slot] + card_sets = [] + for slot, old_cap in enumerate(edge.q_caps): # type: ignore[attr-defined] + target = anchor_a if slot == a_slot else anchor_f + card_sets.append( + tuple((target, endpoint) for endpoint in range(old_cap + 1, HEIGHT)) + ) + for chosen in itertools.product(*card_sets): + chosen = tuple(chosen) + _, _, weight = fork.decoration_balance(edge, chosen) + if weight == 0: + continue + + old_a = edge.q_caps[a_slot] # type: ignore[attr-defined] + end_a = chosen[a_slot][1] + old_f1, old_f2 = (edge.q_caps[slot] for slot in f_slots) # type: ignore[attr-defined] + end_f1, end_f2 = (chosen[slot][1] for slot in f_slots) + anchor_f_energy = old_f1 + old_f2 + formula = ( + edge.parent[edge.q_color][0] # type: ignore[attr-defined] + + sum(edge.q_caps) # type: ignore[attr-defined] + > 0 + and edge.parent[fourth][0] > 0 # type: ignore[attr-defined] + and bad_cap > anchor_a_energy + old_a + and end_a > anchor_a_energy + old_a + and end_f1 > anchor_f_energy + and end_f2 > anchor_f_energy + and (end_f1 - old_f1) + (end_f2 - old_f2) <= bad_cap + ) + actual = raw_first_sweep_is_d2(edge, chosen) + require(actual == formula, "first-sweep D2 inequalities are not exact") + if not actual: + continue + + require( + fork.refined_classify_decoration(edge, chosen) == "d2_reduction", + "first-sweep D2 escaped the production proof-ledger class", + ) + require( + bad_cap >= anchor_a_energy + old_a + 1, + "first-sweep a bound failed", + ) + require( + bad_cap >= old_f1 + old_f2 + 2 >= 2 * energy + 4, + "first-sweep f/E bound failed", + ) + require(energy <= 1, "E=2 first-sweep D2 survived") + + if energy == 1: + require( + ( + bad_cap, + old_f1, + old_f2, + end_f1, + end_f2, + ) + == (6, 2, 2, 5, 5), + "E=1 first-sweep f signature is not rigid", + ) + require( + end_a - old_a == anchor_a_energy + 1, + "E=1 a card did not consume all remaining a", + ) + parent_exposed = fork.exposed_counts(edge.parent) + require( + parent_exposed[anchor_a] + end_a - old_a == HEIGHT, + "E=1 first sweep did not saturate a", + ) + require( + (end_f1 - old_f1) + (end_f2 - old_f2) == 6 + and HEIGHT - bad_cap == 1, + "E=1 f inventory is not six exposed plus one bad-tail item", + ) + + signature = ( + bad_cap, + anchor_a_energy, + old_a, + end_a, + tuple(sorted(((old_f1, end_f1), (old_f2, end_f2)))), + ) + counts[energy] += 1 + weights[energy] += weight + edge_sets[energy].add((edge.parent, edge.terminal, edge.action)) # type: ignore[attr-defined] + parent_sets[energy].add(edge.parent) # type: ignore[attr-defined] + signatures[energy].add(signature) + + theoretical = theoretical_first_sweep_signatures() + for energy in range(3): + require( + signatures[energy] == theoretical[energy], + f"E={energy} numerical signature cover is incomplete", + ) + actual = ( + len(edge_sets[energy]), + len(parent_sets[energy]), + counts[energy], + weights[energy], + len(signatures[energy]), + ) + require(actual == EXPECTED_FIRST_SWEEP[energy], "first-sweep ledger drifted") + + return { + "by_energy": { + str(energy): { + "edges": len(edge_sets[energy]), + "parents": len(parent_sets[energy]), + "decorations": counts[energy], + "residual_word_weight": weights[energy], + "numerical_signatures": len(signatures[energy]), + } + for energy in range(3) + }, + "totals": { + "edges": sum(len(edge_sets[energy]) for energy in range(3)), + "parents": sum(len(parent_sets[energy]) for energy in range(3)), + "decorations": sum(counts.values()), + "residual_word_weight": sum(weights.values()), + "numerical_signatures": sum(len(values) for values in signatures.values()), + }, + } + + +def ledger_json( + ledger: dict[tuple[bool, int, int], tuple[int, int, int]] +) -> dict[str, object]: + return { + f"a_eq_q={str(equal).lower()},legal={legal},E={energy}": { + "edges": values[0], + "decorations": values[1], + "residual_word_weight": values[2], + } + for (equal, legal, energy), values in sorted(ledger.items()) + } + + +def parse_args(argv: Sequence[str] | None = None) -> argparse.Namespace: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "--report", + type=Path, + required=True, + help="complete c4-h7 first-exhaustion report.json", + ) + return parser.parse_args(argv) + + +def main(argv: Sequence[str] | None = None) -> int: + args = parse_args(argv) + fork = load_module( + "c4_h7_tq_exhaust_shared_audit", + TESTS / "check_c4_h7_tq_exhaust_siblings.py", + ) + macro = load_module( + "c4_h7_macro_shared_audit", + TESTS / "test_c4_h7_macro_recon_independent.py", + ) + report = read_report(args.report.resolve()) + terminal_summary = check_terminal_macros(macro) + potential_summary = check_two_anchor_integer_box(fork) + edges = reconstruct_edges(fork) + d2_ledger, d2_totals = report_d2_ledger(report, fork, edges) + first_sweep = first_sweep_ledger(fork, edges) + + result = { + "status": "ANCHOR_PAIR_REDUCTION_VERIFIED", + "claim_boundary": { + "h7_universal_solvability_proved": False, + "all_d2_eliminated": False, + "zero_debt_initial_layouts_checked": False, + "residual_words_expanded": False, + }, + "terminal_macro_audit": terminal_summary, + "two_anchor_integer_box": potential_summary, + "bridge": { + "sibling_edges": len(edges), + "e2_sibling_edges": 36, + "d2_ledger": ledger_json(d2_ledger), + "d2_totals": d2_totals, + "first_sweep_2plus2": first_sweep, + }, + } + print(json.dumps(result, indent=2, sort_keys=True)) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/tests/check_c4_h7_critical_pair_bypass.py b/tests/check_c4_h7_critical_pair_bypass.py new file mode 100644 index 0000000..711b17a --- /dev/null +++ b/tests/check_c4_h7_critical_pair_bypass.py @@ -0,0 +1,526 @@ +#!/usr/bin/env python3 +"""Independent small checks for the c=4,h=7 critical-pair bypass note.""" + +from __future__ import annotations + +from collections import Counter +from dataclasses import dataclass +from itertools import product + + +H = 7 +COLORS = 4 +Q, F, G, HH = range(COLORS) + + +def positive_count(values: list[int] | tuple[int, ...]) -> int: + return sum(value > 0 for value in values) + + +def add_at(values: tuple[int, ...], color: int, amount: int) -> tuple[int, ...]: + result = list(values) + result[color] += amount + return tuple(result) + + +def live_after_test( + debt: tuple[int, ...], source_color: int, source_cap: int, + old_color: int, old_cap: int, target_color: int, +) -> tuple[int, ...]: + tested = list(debt) + tested[source_color] += source_cap + tested[old_color] += old_cap + tested[target_color] -= old_cap + return tuple(tested) + + +def predicted_live_disable( + debt: tuple[int, ...], source_color: int, source_cap: int, + old_color: int, old_cap: int, target_color: int, threshold: int, +) -> bool: + tested = list(debt) + tested[source_color] += source_cap + return ( + positive_count(tested) == threshold + and tested[old_color] <= 0 < tested[old_color] + old_cap + and (tested[target_color] <= 0 or tested[target_color] > old_cap) + ) + + +def check_live_critical_pair_formula() -> int: + checked = 0 + debts = product(range(-3, 4), repeat=COLORS) + for debt in debts: + for threshold in (2, 3): + for old_color in range(COLORS): + for target_color in range(COLORS): + if target_color == old_color: + continue + for source_color in range(COLORS): + for old_cap in range(1, 4): + for source_cap in range(1, 4): + source_test = add_at(debt, source_color, source_cap) + if positive_count(source_test) > threshold: + continue + actual = positive_count( + live_after_test( + debt, source_color, source_cap, + old_color, old_cap, target_color, + ) + ) > threshold + predicted = predicted_live_disable( + debt, source_color, source_cap, + old_color, old_cap, target_color, threshold, + ) + assert actual == predicted, ( + debt, threshold, old_color, old_cap, + target_color, source_color, source_cap, + actual, predicted, + ) + checked += 1 + return checked + + +def live_action_legal( + debt: tuple[int, ...], old_color: int, old_cap: int, threshold: int, +) -> bool: + return positive_count(add_at(debt, old_color, old_cap)) <= threshold + + +def live_disables( + debt: tuple[int, ...], old_color: int, old_cap: int, target_color: int, + other_color: int, other_cap: int, threshold: int, +) -> bool: + if not live_action_legal(debt, other_color, other_cap, threshold): + return False + successor_test = live_after_test( + debt, other_color, other_cap, old_color, old_cap, target_color, + ) + return positive_count(successor_test) > threshold + + +def check_mutual_lock_consequences() -> int: + checked = 0 + for debt in product(range(-3, 4), repeat=COLORS): + for threshold in (2, 3): + for x in range(COLORS): + for u in range(COLORS): + for y in range(COLORS): + if y == x: + continue + for v in range(COLORS): + if v == u: + continue + for s in range(1, 4): + for t in range(1, 4): + if not live_action_legal(debt, x, s, threshold): + continue + if not live_action_legal(debt, u, t, threshold): + continue + mutual = live_disables( + debt, x, s, y, u, t, threshold, + ) and live_disables( + debt, u, t, v, x, s, threshold, + ) + if not mutual: + continue + checked += 1 + if x == u: + energy = -debt[x] + assert max(s, t) <= energy < s + t + assert sum( + debt[color] > 0 + for color in range(COLORS) + if color != x + ) == threshold + else: + assert -s < debt[x] <= 0 + assert -t < debt[u] <= 0 + assert sum( + debt[color] > 0 + for color in range(COLORS) + if color not in (x, u) + ) == threshold - 1 + assert not (y == u and v == x), ( + "direct swap was mutually disabling", + debt, threshold, x, s, u, t, + ) + assert checked > 0 + return checked + + +def predicted_exhaust_disable( + debt: tuple[int, ...], source_color: int, source_cap: int, + old_color: int, old_cap: int, final_color: int, +) -> bool: + tested = list(debt) + tested[source_color] += source_cap + return ( + positive_count(tested) == 2 + and tested[old_color] <= 0 < tested[old_color] + old_cap + and tested[final_color] <= 0 < tested[final_color] + H - old_cap + ) + + +def check_exhaust_formula() -> int: + checked = 0 + for debt in product(range(-3, 4), repeat=COLORS): + for old_color in range(COLORS): + for final_color in range(COLORS): + if final_color == old_color: + continue + for source_color in range(COLORS): + for old_cap in range(1, H): + for source_cap in range(1, 4): + tested = list(debt) + tested[source_color] += source_cap + if positive_count(tested) > 2: + continue + after = tested.copy() + after[old_color] += old_cap + after[final_color] += H - old_cap + actual = positive_count(after) > 3 + predicted = predicted_exhaust_disable( + debt, source_color, source_cap, + old_color, old_cap, final_color, + ) + assert actual == predicted + checked += 1 + return checked + + +def check_inventory_charge_and_cap_sum() -> tuple[int, int]: + charge_cases = 0 + for bad_cap in range(1, H): + for run_count in range(4): + for lengths in product(range(1, H + 1), repeat=run_count): + if (H - bad_cap) + sum(lengths) <= H: + assert sum(lengths) <= bad_cap + assert run_count <= bad_cap + charge_cases += 1 + assert not any( + (H - bad_cap) + sum(lengths) <= H + for bad_cap in (1, 2) + for lengths in product(range(1, H + 1), repeat=3) + ) + assert (H - 3) + 1 + 1 + 1 == H + + cap_cases = 0 + for energy in range(3): + for bad_cap in range(1, H): + total_energy = bad_cap + energy + if total_energy > 8: + continue + for siblings in product(range(energy + 1, H), repeat=3): + if sum(siblings) - energy > H: + continue + cap_cases += 1 + no_pair = all( + siblings[i] + siblings[j] > total_energy + for i in range(3) for j in range(i + 1, 3) + ) + if no_pair: + assert total_energy <= H + if total_energy == 8: + assert bad_cap == 6 and energy == 2 + assert siblings == (3, 3, 3) + assert not no_pair + assert cap_cases > 0 + return charge_cases, cap_cases + + +def compositions(total: int, parts: int): + if parts == 1: + yield (total,) + return + for first in range(total + 1): + for tail in compositions(total - first, parts - 1): + yield (first,) + tail + + +def allowed_tops(g_count: int, h_count: int) -> tuple[int, ...]: + result = [Q] + if g_count: + result.append(G) + if h_count: + result.append(HH) + return tuple(result) + + +def early_terminal_for_solo( + index: int, g_counts: tuple[int, ...], h_counts: tuple[int, ...], + tops: tuple[int, ...], +) -> bool: + g_count, h_count = g_counts[index], h_counts[index] + assert g_count == 0 or h_count == 0 + if g_count == 0 and h_count == 0: + return False + missing = HH if g_count else G + return all(tops[j] == missing for j in range(4) if j != index) + + +def check_prefix_pigeonhole_and_rigid_corner() -> tuple[int, int]: + distributions = 0 + rigid = 0 + for total_non_q in range(H + 1): + for counts in compositions(total_non_q, 8): + g_counts = counts[:4] + h_counts = counts[4:] + solo = [ + i for i in range(4) + if g_counts[i] == 0 or h_counts[i] == 0 + ] + assert solo, (total_non_q, g_counts, h_counts) + distributions += 1 + top_domains = [ + allowed_tops(g_counts[i], h_counts[i]) for i in range(4) + ] + for tops in product(*top_domains): + if not all( + early_terminal_for_solo(i, g_counts, h_counts, tops) + for i in solo + ): + continue + rigid += 1 + assert total_non_q == H + assert len(solo) == 1 + unique = solo[0] + assert g_counts[unique] + h_counts[unique] == 1 + if g_counts[unique] == 1: + missing = HH + else: + missing = G + for j in range(4): + if j == unique: + continue + assert g_counts[j] == h_counts[j] == 1 + assert tops[j] == missing + assert rigid > 0 + return distributions, rigid + + +def runs(word: str) -> list[tuple[str, int]]: + result: list[tuple[str, int]] = [] + for char in word: + if result and result[-1][0] == char: + result[-1] = (char, result[-1][1] + 1) + else: + result.append((char, 1)) + return result + + +def check_solo_prefixes_and_rigid_weave() -> tuple[int, int]: + solo_words = 0 + alphabet = "qgh" + index = {"q": Q, "f": F, "g": G, "h": HH} + for length in range(1, H): + for letters in product(alphabet, repeat=length): + if letters[-1] != "q" or len(set(letters)) > 2: + continue + word = "".join(letters) + chain = runs(word) + debt = [0] * COLORS + cap = chain[0][1] + for run_index in range(len(chain) - 1): + old = index[chain[run_index][0]] + new = index[chain[run_index + 1][0]] + tested = debt.copy() + tested[old] += cap + assert positive_count(tested) <= 2 + debt[old] += cap + debt[new] -= cap + cap += chain[run_index + 1][1] + tested = debt.copy() + tested[Q] += cap + assert positive_count(tested) <= 2 + solo_words += 1 + + weave_words = 0 + for cap in range(2, H): + for x_position in range(cap - 1): + a_word = ["q"] * cap + a_word[x_position] = "x" + assert a_word[-1] == "q" + for a in range(0, H - 2): + for b in range(1, H - a - 1): + if 2 + a + b > H: + continue + background = [a, 0, -a - 1, 1] + prefix_q = 0 + prefix_x = 0 + for char, _run_length in runs("".join(a_word)): + if char == "q": + prefix_q += _run_length + else: + prefix_x += _run_length + tested = background.copy() + tested[Q] += prefix_q + tested[G] += prefix_x + assert tested[G] <= 0 + assert positive_count(tested) <= 2 + live_debt = (a + cap - 1, -cap, -a, 1) + for y_cap in range(1, H): + assert positive_count(add_at(live_debt, HH, y_cap)) <= 2 + bad_debt = (a + cap - 1, H - cap, -a, 1) + for y_cap in range(1, H): + assert positive_count(add_at(bad_debt, HH, y_cap)) <= 3 + weave_words += 1 + assert solo_words > 0 and weave_words > 0 + return solo_words, weave_words + + +@dataclass +class BorderState: + debt: list[int] + positions: list[int] + caps: list[int] + exhausted: list[bool] + z: int = 0 + + def clone(self) -> "BorderState": + return BorderState( + self.debt.copy(), self.positions.copy(), self.caps.copy(), + self.exhausted.copy(), self.z, + ) + + +CHAR_COLOR = {"q": Q, "f": F, "g": G, "h": HH} + + +def make_state(columns_top_to_bottom: list[str]) -> tuple[list[list[tuple[int, int]]], BorderState]: + run_columns: list[list[tuple[int, int]]] = [] + caps: list[int] = [] + for word in columns_top_to_bottom: + encoded = [(CHAR_COLOR[char], length) for char, length in runs(word)] + assert len(encoded) >= 2 + run_columns.append(encoded) + caps.append(encoded[0][1]) + return run_columns, BorderState([0] * COLORS, [0] * 4, caps, [False] * 4) + + +def source_test(state: BorderState, run_columns, column: int) -> tuple[int, ...]: + assert not state.exhausted[column] + top = run_columns[column][state.positions[column]][0] + return add_at(tuple(state.debt), top, state.caps[column]) + + +def legal_sources(state: BorderState, run_columns) -> list[int]: + return [ + column for column in range(4) + if not state.exhausted[column] + and positive_count(source_test(state, run_columns, column)) <= 2 + state.z + ] + + +def apply_event(state: BorderState, run_columns, column: int) -> tuple[str, int]: + assert column in legal_sources(state, run_columns), ( + "illegal event", column, state, + source_test(state, run_columns, column), + ) + position = state.positions[column] + old_color = run_columns[column][position][0] + old_cap = state.caps[column] + final = position + 1 == len(run_columns[column]) - 1 + new_color, new_length = run_columns[column][position + 1] + if final: + assert new_length == H - old_cap + state.debt[old_color] += old_cap + state.debt[new_color] += H - old_cap + state.positions[column] += 1 + state.caps[column] = H + state.exhausted[column] = True + state.z += 1 + return "exhaust", old_cap + state.debt[old_color] += old_cap + state.debt[new_color] -= old_cap + state.positions[column] += 1 + state.caps[column] += new_length + return "live", old_cap + + +def active_tops(state: BorderState, run_columns) -> list[tuple[int, int]]: + return [ + (run_columns[column][state.positions[column]][0], state.caps[column]) + for column in range(4) if not state.exhausted[column] + ] + + +def check_four_lock_and_escape() -> tuple[int, int]: + bottom_to_top = ["2221032", "3321023", "3321003", "1111000"] + digit_to_char = {"0": "q", "1": "f", "2": "g", "3": "h"} + top_to_bottom = [ + "".join(digit_to_char[digit] for digit in reversed(column)) + for column in bottom_to_top + ] + assert top_to_bottom == ["ghqfggg", "hgqfghh", "hqqfghh", "qqqffff"] + counts = Counter("".join(top_to_bottom)) + assert counts == Counter({"q": H, "f": H, "g": H, "h": H}) + + run_columns, initial = make_state(top_to_bottom) + trap_parent = initial.clone() + trap_prefix = [0, 1, 0, 1, 2] + for column in trap_prefix: + apply_event(trap_parent, run_columns, column) + assert trap_parent.z == 0 + assert tuple(trap_parent.debt) == (-5, 0, 2, 3) + assert active_tops(trap_parent, run_columns) == [(Q, 3)] * 4 + assert legal_sources(trap_parent, run_columns) == [0, 1, 2, 3] + hosted_q = sum(cap for color, cap in active_tops(trap_parent, run_columns) if color == Q) + exposed = trap_parent.debt.copy() + exposed[Q] += hosted_q + assert tuple(exposed) == (H, 0, 2, 3) + + for sibling in (0, 1, 2): + child = trap_parent.clone() + kind, cap = apply_event(child, run_columns, sibling) + assert (kind, cap) == ("live", 3) + assert tuple(child.debt) == (-2, -3, 2, 3) + assert sorted(active_tops(child, run_columns)) == sorted( + [(F, 4), (Q, 3), (Q, 3), (Q, 3)] + ) + assert legal_sources(child, run_columns) == [] + + bad_child = trap_parent.clone() + kind, cap = apply_event(bad_child, run_columns, 3) + assert (kind, cap) == ("exhaust", 3) + assert bad_child.z == 1 + assert tuple(bad_child.debt) == (-2, 4, 2, 3) + assert active_tops(bad_child, run_columns) == [(Q, 3)] * 3 + assert legal_sources(bad_child, run_columns) == [] + + escape = initial.clone() + escape_path = [0, 0, 1, 0, 2, 2, 0, 1, 1, 1, 1, 2, 2, 3] + for column in escape_path: + apply_event(escape, run_columns, column) + assert escape.z == 4 + assert all(escape.exhausted) + assert tuple(escape.debt) == (H, H, H, H) + return len(trap_prefix), len(escape_path) + + +def main() -> None: + live_checks = check_live_critical_pair_formula() + mutual_checks = check_mutual_lock_consequences() + exhaust_checks = check_exhaust_formula() + charge_cases, cap_cases = check_inventory_charge_and_cap_sum() + distributions, rigid_cases = check_prefix_pigeonhole_and_rigid_corner() + solo_words, weave_words = check_solo_prefixes_and_rigid_weave() + trap_depth, escape_depth = check_four_lock_and_escape() + print( + "critical_pair_bypass_ok", + f"live_formula={live_checks}", + f"mutual_locks={mutual_checks}", + f"exhaust_formula={exhaust_checks}", + f"charge_cases={charge_cases}", + f"cap_cases={cap_cases}", + f"prefix_distributions={distributions}", + f"rigid_cases={rigid_cases}", + f"solo_words={solo_words}", + f"weave_words={weave_words}", + f"trap_depth={trap_depth}", + f"escape_depth={escape_depth}", + ) + + +if __name__ == "__main__": + main() diff --git a/tests/check_c4_h7_rainbow_lift.py b/tests/check_c4_h7_rainbow_lift.py new file mode 100644 index 0000000..6aadd9a --- /dev/null +++ b/tests/check_c4_h7_rainbow_lift.py @@ -0,0 +1,641 @@ +#!/usr/bin/env python3 +"""Independent checks for the c4 rainbow-transversal/token-lift route. + +The checker deliberately separates three statements: + +* every balanced 4 by H layout has an H-way cell factorization into rainbow + transversals; +* a *thick* transversal (one token in a run of length at least two) preserves + the run-colour skeleton after deletion; +* a skeleton-preserving height-(H-1) path lifts only when every selected + source is legal in both layouts. The exact token error is checked at every + visited source test. + +An arbitrary rainbow deletion is never silently treated as run preserving. +Singleton tokens are reported with the additional borders that need a +separate local detour. +""" + +from __future__ import annotations + +import argparse +from dataclasses import dataclass +from functools import lru_cache +import itertools +import json +from pathlib import Path +from typing import Iterable, Sequence + + +COLORS = 4 +EMPTY = 2 + + +class CheckError(RuntimeError): + pass + + +def require(condition: bool, message: str) -> None: + if not condition: + raise CheckError(message) + + +@dataclass(frozen=True) +class Run: + color: int + length: int + top_start: int + + +@dataclass(frozen=True) +class Token: + column: int + color: int + bottom_position: int + run_index: int + run_length: int + + +@dataclass +class LiftStats: + states: int = 0 + child_legal_edges: int = 0 + jointly_legal_edges: int = 0 + parent_blocked_edges: int = 0 + first_block: dict[str, object] | None = None + + +BUILTINS: dict[str, tuple[list[str], bool]] = { + # The especially symmetric certified h=8 NO instance. It is the smallest + # clean regression for a genuine four-way lock. + "four_lock_h8": ( + ["22111003", "22111003", "00333221", "00333221"], + False, + ), + # First independently reconstructed zero-debt member of the two-source D2 + # near-kernel. The local checkpoint is NO, but this full initial layout is + # YES; it is therefore a useful guard against confusing local and global + # obstruction. + "two_source_near_kernel_h7": ( + ["1111110", "2222100", "3332000", "3332032"], + True, + ), +} + + +def parse_instance(path: Path) -> list[str]: + height: int | None = None + colors: int | None = None + empty: int | None = None + words: list[str] = [] + for raw in path.read_text(encoding="utf-8").splitlines(): + line = raw.strip() + if not line or line.startswith("#"): + continue + require("=" in line, f"malformed instance line: {raw}") + key, value = (field.strip() for field in line.split("=", 1)) + if key == "height": + height = int(value) + elif key == "colors": + colors = int(value) + elif key == "empty": + empty = int(value) + elif key == "column": + words.append(value) + else: + raise CheckError(f"unknown instance key: {key}") + require(height is not None and colors == COLORS and empty == EMPTY, + "checker requires colors=4 and empty=2") + require(len(words) == COLORS and all(len(word) == height for word in words), + "instance dimensions disagree") + return words + + +def validate_layout(words: Sequence[str]) -> int: + require(len(words) == COLORS, "layout must have four original columns") + height = len(words[0]) + require(height >= 1 and all(len(word) == height for word in words), + "columns must have one common positive height") + require(all(character in "0123" for word in words for character in word), + "layout uses a colour outside 0..3") + counts = [sum(word.count(str(color)) for word in words) + for color in range(COLORS)] + require(counts == [height] * COLORS, + f"layout is not balanced: counts={counts}, height={height}") + return height + + +def top_runs(word_bottom_to_top: str) -> list[Run]: + top = list(reversed([int(character) for character in word_bottom_to_top])) + result: list[Run] = [] + start = 0 + while start < len(top): + end = start + 1 + while end < len(top) and top[end] == top[start]: + end += 1 + result.append(Run(top[start], end - start, start)) + start = end + return result + + +def run_index_at_bottom_position(word: str, bottom_position: int) -> tuple[int, int]: + top_position = len(word) - 1 - bottom_position + for index, run in enumerate(top_runs(word)): + if run.top_start <= top_position < run.top_start + run.length: + return index, run.length + raise CheckError("cell did not belong to a run") + + +def occurrence_factorization(words: Sequence[str]) -> list[tuple[Token, ...]]: + """Repeatedly extract a perfect matching from the regular multigraph.""" + + height = validate_layout(words) + remaining: dict[tuple[int, int], list[int]] = { + (column, color): [position for position, character in enumerate(word) + if int(character) == color] + for column, word in enumerate(words) + for color in range(COLORS) + } + factors: list[tuple[Token, ...]] = [] + for _round in range(height): + permutation = next( + (candidate for candidate in itertools.permutations(range(COLORS)) + if all(remaining[column, candidate[column]] + for column in range(COLORS))), + None, + ) + require(permutation is not None, + "regular remainder unexpectedly has no perfect matching") + factor: list[Token] = [] + for column, color in enumerate(permutation): + bottom_position = remaining[column, color].pop(0) + run_index, run_length = run_index_at_bottom_position( + words[column], bottom_position) + factor.append(Token(column, color, bottom_position, + run_index, run_length)) + factors.append(tuple(factor)) + + require(all(not positions for positions in remaining.values()), + "factorization did not consume every cell") + covered = {(token.column, token.bottom_position) + for factor in factors for token in factor} + require(len(covered) == COLORS * height, + "factorization reused a physical cell") + return factors + + +def delete_tokens(words: Sequence[str], tokens: Sequence[Token]) -> list[str]: + require({token.column for token in tokens} == set(range(COLORS)), + "transversal does not select every column once") + require({token.color for token in tokens} == set(range(COLORS)), + "transversal does not select every colour once") + child: list[str] = [] + by_column = {token.column: token for token in tokens} + for column, word in enumerate(words): + token = by_column[column] + require(int(word[token.bottom_position]) == token.color, + "token colour does not match its physical cell") + child.append(word[:token.bottom_position] + word[token.bottom_position + 1:]) + child_height = validate_layout(child) + require(child_height + 1 == len(words[0]), + "rainbow deletion did not lower height by exactly one") + return child + + +def skeleton(words: Sequence[str]) -> tuple[tuple[int, ...], ...]: + return tuple(tuple(run.color for run in top_runs(word)) for word in words) + + +def singleton_extra_borders(word: str, bottom_position: int) -> int: + run_index, run_length = run_index_at_bottom_position(word, bottom_position) + if run_length >= 2: + return 0 + before = len(top_runs(word)) - 1 + child = word[:bottom_position] + word[bottom_position + 1:] + after = len(top_runs(child)) - 1 if child else 0 + require(before >= after, "deleting a singleton unexpectedly added a border") + return before - after + + +def thick_run_options(words: Sequence[str], column: int, color: int) -> list[Token]: + result: list[Token] = [] + word = words[column] + height = len(word) + for run_index, run in enumerate(top_runs(word)): + if run.color != color or run.length < 2: + continue + # Any unit in the same run gives the same child run-length vector. + top_position = run.top_start + bottom_position = height - 1 - top_position + result.append(Token(column, color, bottom_position, + run_index, run.length)) + return result + + +def thick_hall_witness(words: Sequence[str]) -> dict[str, object] | None: + for size in range(1, COLORS + 1): + for subset in itertools.combinations(range(COLORS), size): + neighbors = sorted( + column for column in range(COLORS) + if any(thick_run_options(words, column, color) + for color in subset) + ) + if len(neighbors) < len(subset): + return { + "colors": list(subset), + "neighbor_columns": neighbors, + "color_count": len(subset), + "neighbor_count": len(neighbors), + } + return None + + +def enumerate_thick_transversals(words: Sequence[str]) -> Iterable[tuple[Token, ...]]: + for permutation in itertools.permutations(range(COLORS)): + options = [thick_run_options(words, column, permutation[column]) + for column in range(COLORS)] + if all(options): + yield from (tuple(choice) for choice in itertools.product(*options)) + + +def initial_levels(runs: Sequence[Sequence[Run]]) -> tuple[int, ...]: + # A one-run original column already has no border and is a monochrome bin. + return tuple(1 for _ in runs) + + +def exhausted_count(runs: Sequence[Sequence[Run]], levels: Sequence[int]) -> int: + return sum(level == len(column_runs) + for level, column_runs in zip(levels, runs)) + + +def source_test( + runs: Sequence[Sequence[Run]], levels: Sequence[int], source: int +) -> tuple[tuple[int, ...], bool]: + require(levels[source] < len(runs[source]), "exhausted column used as source") + exposed = [0] * COLORS + hosted = [0] * COLORS + capacities = [sum(run.length for run in column_runs[:level]) + for column_runs, level in zip(runs, levels)] + for column_runs, level in zip(runs, levels): + for run in column_runs[:level]: + exposed[run.color] += run.length + for column, (column_runs, level) in enumerate(zip(runs, levels)): + if level < len(column_runs): + hosted[column_runs[level - 1].color] += capacities[column] + debts = [exposed[color] - hosted[color] for color in range(COLORS)] + color = runs[source][levels[source] - 1].color + debts[color] += capacities[source] + test = tuple(debts) + legal = sum(value > 0 for value in test) <= EMPTY + exhausted_count(runs, levels) + return test, legal + + +def exact_winning(words: Sequence[str]) -> tuple[bool, int]: + runs = [top_runs(word) for word in words] + + @lru_cache(maxsize=None) + def win(levels: tuple[int, ...]) -> bool: + if exhausted_count(runs, levels) >= COLORS - EMPTY: + return True + for source, level in enumerate(levels): + if level == len(runs[source]): + continue + _test, legal = source_test(runs, levels, source) + if not legal: + continue + successor = list(levels) + successor[source] += 1 + if win(tuple(successor)): + return True + return False + + answer = win(initial_levels(runs)) + return answer, win.cache_info().currsize + + +def epsilon_for( + parent_runs: Sequence[Sequence[Run]], + levels: Sequence[int], + source: int, + tokens: Sequence[Token], +) -> tuple[int, ...]: + epsilon = [0] * COLORS + by_column = {token.column: token for token in tokens} + for column, (column_runs, level) in enumerate(zip(parent_runs, levels)): + token = by_column[column] + token_exposed = token.run_index < level + if not token_exposed: + continue + epsilon[token.color] += 1 + active = level < len(column_runs) + if active and column != source: + epsilon[column_runs[level - 1].color] -= 1 + return tuple(epsilon) + + +def compatible_lift(words: Sequence[str], tokens: Sequence[Token]) -> dict[str, object]: + child = delete_tokens(words, tokens) + require(skeleton(words) == skeleton(child), + "compatible_lift requires a run-preserving transversal") + parent_runs = [top_runs(word) for word in words] + child_runs = [top_runs(word) for word in child] + require([len(runs) for runs in parent_runs] == + [len(runs) for runs in child_runs], "run counts drifted") + stats = LiftStats() + chosen: dict[tuple[int, ...], int] = {} + + @lru_cache(maxsize=None) + def lift(levels: tuple[int, ...]) -> bool: + stats.states += 1 + if exhausted_count(parent_runs, levels) >= COLORS - EMPTY: + return True + for source, level in enumerate(levels): + if level == len(parent_runs[source]): + continue + child_test, child_legal = source_test(child_runs, levels, source) + if not child_legal: + continue + stats.child_legal_edges += 1 + parent_test, parent_legal = source_test(parent_runs, levels, source) + epsilon = epsilon_for(parent_runs, levels, source, tokens) + actual = tuple(parent_test[color] - child_test[color] + for color in range(COLORS)) + require(actual == epsilon, + f"token error formula failed at {levels}, source {source}: " + f"actual={actual}, formula={epsilon}") + if not parent_legal: + stats.parent_blocked_edges += 1 + if stats.first_block is None: + stats.first_block = { + "levels": list(levels), + "source": source, + "child_test": list(child_test), + "parent_test": list(parent_test), + "epsilon": list(epsilon), + "child_positive": sum(value > 0 for value in child_test), + "parent_positive": sum(value > 0 for value in parent_test), + "available_bins": EMPTY + exhausted_count(parent_runs, levels), + } + continue + stats.jointly_legal_edges += 1 + successor = list(levels) + successor[source] += 1 + successor_tuple = tuple(successor) + if lift(successor_tuple): + chosen[levels] = source + return True + return False + + start = initial_levels(parent_runs) + winning = lift(start) + path: list[int] = [] + trace: list[dict[str, object]] = [] + if winning: + levels = start + while exhausted_count(parent_runs, levels) < COLORS - EMPTY: + source = chosen[levels] + child_test, _ = source_test(child_runs, levels, source) + parent_test, _ = source_test(parent_runs, levels, source) + epsilon = epsilon_for(parent_runs, levels, source, tokens) + trace.append({ + "levels": list(levels), + "source": source, + "child_test": list(child_test), + "parent_test": list(parent_test), + "epsilon": list(epsilon), + }) + path.append(source) + successor = list(levels) + successor[source] += 1 + levels = tuple(successor) + return { + "winning": winning, + "path": path, + "trace": trace, + "states": stats.states, + "child_legal_edges": stats.child_legal_edges, + "jointly_legal_edges": stats.jointly_legal_edges, + "parent_blocked_child_edges": stats.parent_blocked_edges, + "first_block": stats.first_block, + "child_bottom_to_top": child, + } + + +def upper_support_without_bottom_run(word: str) -> set[int]: + bottom_color = word[0] + boundary = 0 + while boundary < len(word) and int(word[boundary]) == int(bottom_color): + boundary += 1 + return {int(character) for character in word[boundary:]} + + +def sequential_bypass_pairs(words: Sequence[str]) -> list[list[int]]: + supports = [{int(character) for character in word} for word in words] + upper = [upper_support_without_bottom_run(word) for word in words] + return [ + [first, second] + for first in range(COLORS) + for second in range(COLORS) + if first != second + and len(upper[first]) <= 2 + and len(supports[first] | upper[second]) <= 3 + ] + + +def bottom_extensions(words: Sequence[str]) -> dict[str, object] | None: + if len(words[0]) != 7: + return None + yes = no = 0 + first_no: list[str] | None = None + for permutation in itertools.permutations(range(COLORS)): + extension = [str(permutation[column]) + words[column] + for column in range(COLORS)] + validate_layout(extension) + winning, _states = exact_winning(extension) + yes += int(winning) + no += int(not winning) + if not winning and first_no is None: + first_no = extension + return { + "labeled_rainbow_bottom_extensions": 24, + "yes": yes, + "no": no, + "first_no_bottom_to_top": first_no, + } + + +def analyze_case(name: str, words: Sequence[str], expected: bool | None) -> dict[str, object]: + height = validate_layout(words) + winning, state_count = exact_winning(words) + if expected is not None: + require(winning == expected, + f"{name}: exact outcome drifted, got {winning}, expected {expected}") + + factors = occurrence_factorization(words) + require(len(factors) == height, f"{name}: wrong factor count") + factor_rows: list[dict[str, object]] = [] + for index, factor in enumerate(factors): + child = delete_tokens(words, factor) + child_winning, child_states = exact_winning(child) + thick = all(token.run_length >= 2 for token in factor) + factor_rows.append({ + "index": index, + "tokens": [token.__dict__ for token in factor], + "thick": thick, + "singleton_extra_borders": [ + singleton_extra_borders(words[token.column], token.bottom_position) + for token in factor + ], + "child_balanced_height": len(child[0]), + "child_winning": child_winning, + "child_states": child_states, + }) + child_yes = sum(bool(row["child_winning"]) for row in factor_rows) + if height == 7: + require(child_yes == 7, + f"{name}: a rainbow deletion contradicted the h=6 YES theorem") + + hall = thick_hall_witness(words) + thick_candidates = list(enumerate_thick_transversals(words)) + require((hall is None) == bool(thick_candidates), + f"{name}: thick Hall dichotomy disagrees with enumeration") + lift_found: dict[str, object] | None = None + representative_failure: dict[str, object] | None = None + checked = 0 + for tokens in thick_candidates: + checked += 1 + result = compatible_lift(words, tokens) + if result["winning"]: + lift_found = { + "tokens": [token.__dict__ for token in tokens], + **result, + } + break + if representative_failure is None or ( + int(result["parent_blocked_child_edges"]) + < int(representative_failure["parent_blocked_child_edges"]) + ): + representative_failure = { + "tokens": [token.__dict__ for token in tokens], + **result, + } + + if lift_found is not None: + require(winning, f"{name}: a compatible lift cannot exist for a NO layout") + if not winning: + require(lift_found is None, + f"{name}: certified NO unexpectedly had a compatible lift") + + return { + "name": name, + "height": height, + "columns_bottom_to_top": list(words), + "exact_winning": winning, + "exact_states": state_count, + "rainbow_factorization_count": len(factors), + "rainbow_children_winning": child_yes, + "rainbow_children_losing": len(factors) - child_yes, + "thick_factors_in_one_greedy_factorization": sum( + bool(row["thick"]) for row in factor_rows + ), + "factorization": factor_rows, + "thick_transversal": { + "exists": hall is None, + "hall_witness": hall, + "candidates_enumerated": len(thick_candidates), + }, + "token_compatible_lift": { + "found": lift_found is not None, + "candidates_checked": checked, + "witness": lift_found, + "representative_failure": representative_failure, + "scope": "thick/run-skeleton-preserving transversals only", + }, + "sequential_bypass_pairs": sequential_bypass_pairs(words), + "height8_rainbow_bottom_extension_profile": bottom_extensions(words), + } + + +def assert_builtin_regressions(cases: Sequence[dict[str, object]]) -> None: + by_name = {str(case["name"]): case for case in cases} + if "four_lock_h8" in by_name: + case = by_name["four_lock_h8"] + thick = case["thick_transversal"] + lift = case["token_compatible_lift"] + require(case["rainbow_factorization_count"] == 8, + "four-lock occurrence factorization drifted") + require(thick["exists"] and thick["candidates_enumerated"] == 8, + "four-lock thick-transversal catalog drifted") + require(not lift["found"] and lift["candidates_checked"] == 8, + "four-lock unexpectedly acquired a compatible lift") + failure = lift["representative_failure"] + require(failure is not None and failure["first_block"] is not None, + "four-lock lost its token-block diagnostic") + block = failure["first_block"] + require(block["child_positive"] == 3 and block["parent_positive"] == 4, + "four-lock diagnostic is no longer the saturated 3-to-4 flip") + + if "two_source_near_kernel_h7" in by_name: + case = by_name["two_source_near_kernel_h7"] + thick = case["thick_transversal"] + lift = case["token_compatible_lift"] + require(case["rainbow_factorization_count"] == 7, + "near-kernel occurrence factorization drifted") + require(all(row["child_winning"] for row in case["factorization"]), + "a balanced h=6 near-kernel child unexpectedly became NO") + require(thick["exists"] and thick["candidates_enumerated"] == 1, + "near-kernel thick-transversal catalog drifted") + require(lift["found"] and lift["witness"]["path"] == [0, 1, 1], + "near-kernel compatible lift witness drifted") + extensions = case["height8_rainbow_bottom_extension_profile"] + require(extensions is not None and extensions["yes"] == 24 + and extensions["no"] == 0, + "near-kernel rainbow-bottom extension profile drifted") + + +def parse_args() -> argparse.Namespace: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--instance", type=Path, + help="an additional balanced colors=4,empty=2 instance") + parser.add_argument("--json", type=Path, help="write the audit report") + parser.add_argument("--no-builtins", action="store_true", + help="skip the committed four-lock and near-kernel fixtures") + return parser.parse_args() + + +def main() -> int: + args = parse_args() + cases: list[tuple[str, list[str], bool | None]] = [] + if not args.no_builtins: + cases.extend((name, words, expected) + for name, (words, expected) in BUILTINS.items()) + if args.instance is not None: + cases.append((args.instance.stem, parse_instance(args.instance), None)) + require(cases, "no layouts were selected") + analyzed = [analyze_case(name, words, expected) + for name, words, expected in cases] + assert_builtin_regressions(analyzed) + report = { + "scope": "rainbow transversal factorization and thick-token lift audit", + "claims_global_c4_h7_theorem": False, + "cases": analyzed, + } + encoded = json.dumps(report, indent=2, sort_keys=True) + "\n" + if args.json is not None: + args.json.parent.mkdir(parents=True, exist_ok=True) + args.json.write_text(encoded, encoding="utf-8") + else: + print(encoded, end="") + for case in report["cases"]: + lift = case["token_compatible_lift"] + print( + f"rainbow-lift {case['name']}: exact={'YES' if case['exact_winning'] else 'NO'}, " + f"factors={case['rainbow_factorization_count']}, " + f"thick={case['thick_transversal']['exists']}, " + f"compatible={lift['found']}, checked={lift['candidates_checked']}" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) From 0c3ecf23e479373e288c826abd7acbe4d3c00974 Mon Sep 17 00:00:00 2001 From: lieoric <129092606+lieoric@users.noreply.github.com> Date: Tue, 11 Aug 2026 07:37:05 +1000 Subject: [PATCH 2/6] Audit three-source D2 checkpoint futures --- .github/workflows/c4-h7-d2-three-source.yml | 188 +++ CMakeLists.txt | 18 + apps/c4_h7_d2_three_source.cpp | 1395 +++++++++++++++++ .../validate_c4_h7_d2_three_source_report.py | 454 ++++++ tests/check_c4_h7_d2_three_source.py | 1047 +++++++++++++ 5 files changed, 3102 insertions(+) create mode 100644 .github/workflows/c4-h7-d2-three-source.yml create mode 100644 apps/c4_h7_d2_three_source.cpp create mode 100644 scripts/validate_c4_h7_d2_three_source_report.py create mode 100644 tests/check_c4_h7_d2_three_source.py diff --git a/.github/workflows/c4-h7-d2-three-source.yml b/.github/workflows/c4-h7-d2-three-source.yml new file mode 100644 index 0000000..ac26a45 --- /dev/null +++ b/.github/workflows/c4-h7-d2-three-source.yml @@ -0,0 +1,188 @@ +name: Audit c4 h7 three-source D2 checkpoints +run-name: Exact c4 k2 h7 three-legal-source fixed-future checkpoint audit + +on: + push: + branches: [codex/c4-h7-global-bypass] + workflow_dispatch: + +permissions: + contents: read + +concurrency: + group: c4-h7-d2-three-source-${{ github.ref }} + cancel-in-progress: true + +jobs: + build-and-bounded-differential: + runs-on: ubuntu-latest + timeout-minutes: 30 + steps: + - uses: actions/checkout@v5 + - uses: actions/setup-python@v5 + with: + python-version: "3.12" + - name: Configure Release with warnings as errors + run: >- + cmake -S . -B build + -DCMAKE_BUILD_TYPE=Release + -DWSC_WARNINGS_AS_ERRORS=ON + - name: Build the focused executable + run: >- + cmake --build build + --target water-c4-h7-d2-three-source + --parallel 2 + - name: Run the focused C++ smoke test + run: >- + ctest --test-dir build --output-on-failure + --no-tests=error + -R '^water-c4-h7-d2-three-source-smoke$' + - name: Differentially rebuild and solve a bounded prefix + run: | + mkdir -p out/bounded + set -o pipefail + python tests/check_c4_h7_d2_three_source.py \ + --program build/water-c4-h7-d2-three-source \ + --limit 64 \ + --json out/bounded/independent-64.json 2>&1 \ + | tee out/bounded/independent-64.log + - name: Preserve and strictly validate the same bounded prefix + run: | + set -o pipefail + build/water-c4-h7-d2-three-source \ + --self-test --limit 64 --output-dir out/bounded/production 2>&1 \ + | tee out/bounded/production.log + python scripts/validate_c4_h7_d2_three_source_report.py \ + out/bounded/production/report.json --negative-tests + test "$(python -c 'import json; print(json.load(open("out/bounded/production/report.json"))["status"])')" = INCOMPLETE + - name: Configure Clang ASan and UBSan + run: >- + cmake -S . -B build-sanitize + -DCMAKE_BUILD_TYPE=Debug + -DCMAKE_CXX_COMPILER=clang++ + -DWSC_WARNINGS_AS_ERRORS=ON + -DCMAKE_CXX_FLAGS='-fsanitize=address,undefined -fno-omit-frame-pointer' + -DCMAKE_EXE_LINKER_FLAGS='-fsanitize=address,undefined' + - name: Run bounded sanitizer self-tests + env: + ASAN_OPTIONS: detect_leaks=1:halt_on_error=1 + UBSAN_OPTIONS: halt_on_error=1:print_stacktrace=1 + run: | + cmake --build build-sanitize \ + --target water-c4-h7-d2-three-source --parallel 2 + build-sanitize/water-c4-h7-d2-three-source \ + --self-test --limit 8 --output-dir out/bounded/sanitized + - name: Create and verify the bounded SHA-256 manifest + if: always() + run: | + mkdir -p out/bounded + find out/bounded -type f ! -name SHA256SUMS -print0 \ + | sort -z \ + | xargs -0 -r sha256sum > out/bounded/SHA256SUMS + sha256sum --check out/bounded/SHA256SUMS + - uses: actions/upload-artifact@v6 + if: always() + with: + name: c4-h7-d2-three-source-bounded-${{ github.run_id }} + path: out/bounded/ + if-no-files-found: error + retention-days: 30 + + full-fixed-future-checkpoint-audit: + runs-on: ubuntu-latest + timeout-minutes: 240 + steps: + - uses: actions/checkout@v5 + - uses: actions/setup-python@v5 + with: + python-version: "3.12" + - name: Configure and build Release with warnings as errors + run: | + cmake -S . -B build \ + -DCMAKE_BUILD_TYPE=Release \ + -DWSC_WARNINGS_AS_ERRORS=ON + cmake --build build \ + --target water-c4-h7-d2-three-source --parallel 2 + - name: Enumerate and solve all 1106490 fixed futures + run: | + mkdir -p out/full + set -o pipefail + build/water-c4-h7-d2-three-source \ + --self-test --output-dir out/full 2>&1 \ + | tee out/full/production.log + - name: Strictly validate schema, ledgers, and claim boundaries + run: | + python scripts/validate_c4_h7_d2_three_source_report.py \ + out/full/report.json --negative-tests + python - <<'PY' + import json + from pathlib import Path + + report = json.loads(Path("out/full/report.json").read_text()) + if report["status"] != "LOCAL_NO_RESIDUALS_EXPORTED": + raise SystemExit(f"unexpected full status: {report['status']}") + if report["claims"] != { + "three_source_checkpoint_family_eliminated": False, + "zero_debt_initial_family_eliminated": False, + "universal_c4_h7_solvability": False, + }: + raise SystemExit("full report crossed its checkpoint-only claim boundary") + Path("out/full/status.txt").write_text(report["status"] + "\n") + PY + - name: Independently rebuild, solve, and compare every fixed future + run: | + set -o pipefail + python tests/check_c4_h7_d2_three_source.py \ + --report out/full/report.json \ + --json out/full/independent-audit.json \ + --local-no-ledger out/full/independent-local-no-ledger.jsonl 2>&1 \ + | tee out/full/independent.log + - name: Verify independent NO rows remain explicitly local-only + run: | + python - <<'PY' + import json + from pathlib import Path + + path = Path("out/full/independent-local-no-ledger.jsonl") + rows = [json.loads(line) for line in path.read_text().splitlines()] + if not rows: + raise SystemExit("expected at least one independently reproduced checkpoint local NO") + for index, row in enumerate(rows): + if row.get("scope") != "nonzero_debt_parent_checkpoint_fixed_future": + raise SystemExit(f"independent NO {index} lost its local scope") + if row.get("zero_debt_past_restored") is not False: + raise SystemExit(f"independent NO {index} claims restored zero debt") + if row.get("global_counterexample") is not False: + raise SystemExit(f"independent NO {index} claims a global counterexample") + report = json.loads(Path("out/full/report.json").read_text()) + if len(rows) != report["run"]["local_no"]: + raise SystemExit("independent local-NO ledger count drifted") + PY + - name: Record the intentionally narrow conclusion + run: | + python - <<'PY' >> "$GITHUB_STEP_SUMMARY" + import json + from pathlib import Path + + report = json.loads(Path("out/full/report.json").read_text()) + print("> Exact full result: " + f"{report['run']['local_no']} of {report['run']['fixed_futures_checked']} " + "fixed futures are local NO at nonzero-debt parent checkpoints. " + "They are exported for a later zero-debt past-restoration analysis; " + "this job proves no balanced initial-layout NO and no global c4/h7 theorem.") + PY + cat out/full/report.md >> "$GITHUB_STEP_SUMMARY" + - name: Create and verify the full SHA-256 manifest + if: always() + run: | + find out/full -type f ! -name SHA256SUMS -print0 \ + | sort -z \ + | xargs -0 -r sha256sum > out/full/SHA256SUMS + sha256sum --check out/full/SHA256SUMS + - uses: actions/upload-artifact@v6 + if: always() + with: + name: c4-h7-d2-three-source-full-${{ github.run_id }} + path: out/full/ + if-no-files-found: error + retention-days: 30 diff --git a/CMakeLists.txt b/CMakeLists.txt index 4dd0627..055af9e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -141,6 +141,19 @@ else() endif() endif() +add_executable(water-c4-h7-d2-three-source apps/c4_h7_d2_three_source.cpp) +if(MSVC) + target_compile_options(water-c4-h7-d2-three-source PRIVATE /W4) + if(WSC_WARNINGS_AS_ERRORS) + target_compile_options(water-c4-h7-d2-three-source PRIVATE /WX) + endif() +else() + target_compile_options(water-c4-h7-d2-three-source PRIVATE -Wall -Wextra -Wpedantic) + if(WSC_WARNINGS_AS_ERRORS) + target_compile_options(water-c4-h7-d2-three-source PRIVATE -Werror) + endif() +endif() + include(CTest) if(BUILD_TESTING) add_executable(water-sort-tests tests/test_main.cpp) @@ -168,6 +181,11 @@ if(BUILD_TESTING) --self-test --limit 64 --output-dir ${CMAKE_CURRENT_BINARY_DIR}/test-c4-h7-d2-two-source-output) + add_test(NAME water-c4-h7-d2-three-source-smoke + COMMAND water-c4-h7-d2-three-source + --self-test + --limit 64 + --output-dir ${CMAKE_CURRENT_BINARY_DIR}/test-c4-h7-d2-three-source-output) file(GLOB WSC_EXPERIMENT_INSTANCES "${CMAKE_CURRENT_SOURCE_DIR}/experiments/*.txt") foreach(WSC_EXPERIMENT_INSTANCE IN LISTS WSC_EXPERIMENT_INSTANCES) get_filename_component(WSC_EXPERIMENT_NAME ${WSC_EXPERIMENT_INSTANCE} NAME_WE) diff --git a/apps/c4_h7_d2_three_source.cpp b/apps/c4_h7_d2_three_source.cpp new file mode 100644 index 0000000..2e27703 --- /dev/null +++ b/apps/c4_h7_d2_three_source.cpp @@ -0,0 +1,1395 @@ +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +namespace { + +constexpr int kHeight = 7; +constexpr int kColors = 4; +constexpr int kEmpty = 2; +constexpr std::uint64_t kExpectedTqTerminals = 71; +constexpr std::uint64_t kExpectedLabeledCandidates = 624; +constexpr std::uint64_t kExpectedCanonicalParents = 418; +constexpr std::uint64_t kExpectedCanonicalEdges = 429; +constexpr std::uint64_t kExpectedSiblingEdges = 423; +constexpr std::uint64_t kExpectedSelectedEdges = 12; +constexpr std::uint64_t kExpectedDecorations = 1535; +constexpr std::uint64_t kExpectedResidualWords = 1106490; + +using Debts = std::array; +using Counts = std::array; +using Caps = std::array, kColors>; + +struct Options { + std::filesystem::path output_dir; + std::uint64_t limit = 0; + bool self_test = false; +}; + +struct Bucket { + int debt = 0; + std::vector caps; + + bool operator<(const Bucket& other) const { + return std::tie(debt, caps) < std::tie(other.debt, other.caps); + } + bool operator==(const Bucket& other) const { + return debt == other.debt && caps == other.caps; + } +}; + +using State = std::array; + +struct Source { + int color = 0; + int cap = 0; +}; + +struct ExhaustAction { + int old_color = 0; + int old_cap = 0; + int final_color = 0; + + bool operator<(const ExhaustAction& other) const { + return std::tie(old_color, old_cap, final_color) < + std::tie(other.old_color, other.old_cap, other.final_color); + } +}; + +struct Card { + int color = 0; + int endpoint = 0; +}; + +struct Edge { + std::size_t ordinal = 0; + State parent; + State terminal; + ExhaustAction bad; + Debts terminal_debts{}; + int q_color = -1; + std::array q_caps{}; + int legal_source_count = 0; +}; + +struct Bridge { + std::vector edges; + std::uint64_t terminal_count = 0; + std::uint64_t labeled_candidates = 0; + std::uint64_t canonical_parent_count = 0; + std::uint64_t canonical_edge_count = 0; + std::uint64_t sibling_edge_count = 0; +}; + +struct Decoration { + std::size_t ordinal = 0; + std::size_t edge_index = 0; + std::array cards{}; + Counts residual_after_forced{}; + std::array free_tail_lengths{}; + std::uint64_t residual_words_expected = 0; +}; + +struct FixedFixture { + Debts debts{}; + std::array sources{}; + std::array, kColors> hidden_bottom_to_top; +}; + +struct EdgeStats { + std::size_t edge_ordinal = 0; + std::uint64_t decorations = 0; + std::uint64_t residual_words_expected = 0; + std::uint64_t residual_words_checked = 0; + std::uint64_t local_yes = 0; + std::uint64_t local_no = 0; + std::uint64_t states = 0; + std::uint64_t transitions = 0; + std::map safe_mask_distribution; +}; + +struct Sample { + bool present = false; + std::uint64_t future_index = 0; + std::size_t decoration_index = 0; + std::size_t edge_ordinal = 0; + bool solvable = false; + std::uint32_t safe_mask = 0; + std::string path; + std::array hidden_words_bottom_to_top; +}; + +struct RunStats { + bool self_checks_passed = false; + bool universe_complete = false; + std::uint64_t limit_requested = 0; + std::uint64_t decorations_expected = 0; + std::uint64_t residual_words_expected = 0; + std::uint64_t residual_words_checked = 0; + std::uint64_t local_yes = 0; + std::uint64_t local_no = 0; + std::uint64_t winning_paths_replayed = 0; + std::uint64_t states = 0; + std::uint64_t transitions = 0; + std::uint64_t ledger_hash = 1469598103934665603ULL; + std::vector per_edge; + std::optional first_yes; + std::optional first_no; + double elapsed_seconds = 0.0; +}; + +void require(bool condition, const std::string& message) { + if (!condition) throw std::runtime_error("self-check failed: " + message); +} + +void usage() { + std::cerr << "Usage: water-c4-h7-d2-three-source --output-dir DIR " + "[--limit N] [--self-test]\n"; +} + +Options parse_options(int argc, char** argv) { + Options options; + for (int index = 1; index < argc; ++index) { + const std::string argument = argv[index]; + if (argument == "--output-dir" && index + 1 < argc) { + options.output_dir = argv[++index]; + } else if (argument == "--limit" && index + 1 < argc) { + options.limit = std::stoull(argv[++index]); + } else if (argument == "--self-test") { + options.self_test = true; + } else if (argument == "--help") { + usage(); + std::exit(0); + } else { + usage(); + throw std::runtime_error("unknown or incomplete argument: " + argument); + } + } + if (options.output_dir.empty() && !options.self_test) { + usage(); + throw std::runtime_error("--output-dir is required unless --self-test is used"); + } + return options; +} + +int positive_count(const Debts& debts) { + return static_cast(std::count_if( + debts.begin(), debts.end(), [](int value) { return value > 0; })); +} + +State canonical_state(const Debts& debts, Caps caps) { + State result; + for (int color = 0; color < kColors; ++color) { + std::sort(caps[color].begin(), caps[color].end()); + result[static_cast(color)] = {debts[color], caps[color]}; + } + std::sort(result.begin(), result.end()); + return result; +} + +Debts state_debts(const State& state) { + Debts result{}; + for (int color = 0; color < kColors; ++color) result[color] = state[color].debt; + return result; +} + +Caps state_caps(const State& state) { + Caps result; + for (int color = 0; color < kColors; ++color) result[color] = state[color].caps; + return result; +} + +Counts exposed_counts(const State& state) { + Counts result{}; + for (int color = 0; color < kColors; ++color) { + result[color] = state[color].debt; + for (const int cap : state[color].caps) result[color] += cap; + } + return result; +} + +bool algebraically_consistent(const State& state, int exhausted) { + if (!std::is_sorted(state.begin(), state.end())) return false; + int cap_count = 0; + int debt_sum = 0; + Counts multiplicity{}; + for (int color = 0; color < kColors; ++color) { + debt_sum += state[color].debt; + multiplicity[color] = static_cast(state[color].caps.size()); + cap_count += multiplicity[color]; + for (const int cap : state[color].caps) { + if (cap < 1 || cap >= kHeight) return false; + } + } + if (cap_count != kColors - exhausted || debt_sum != exhausted * kHeight) { + return false; + } + const Counts exposed = exposed_counts(state); + Counts remaining{}; + for (int color = 0; color < kColors; ++color) { + if (exposed[color] < multiplicity[color] || exposed[color] > kHeight) { + return false; + } + remaining[color] = kHeight - exposed[color]; + } + for (int color = 0; color < kColors; ++color) { + int allowed = 0; + for (int other = 0; other < kColors; ++other) { + if (other != color) allowed += remaining[other]; + } + if (multiplicity[color] > allowed) return false; + } + return true; +} + +bool source_is_legal(const Debts& debts, int exhausted, int color, int cap) { + Debts tested = debts; + tested[color] += cap; + return positive_count(tested) <= kEmpty + exhausted; +} + +bool source_is_legal(const State& state, int exhausted, int color, int cap) { + return source_is_legal(state_debts(state), exhausted, color, cap); +} + +std::vector sources(const State& state) { + std::vector result; + for (int color = 0; color < kColors; ++color) { + for (const int cap : state[color].caps) result.push_back({color, cap}); + } + return result; +} + +std::vector legal_sources(const State& state, int exhausted) { + std::vector result; + for (const Source source : sources(state)) { + if (source_is_legal(state, exhausted, source.color, source.cap)) { + result.push_back(source); + } + } + return result; +} + +bool is_tq_terminal(const State& state) { + if (!algebraically_consistent(state, 1) || !legal_sources(state, 1).empty()) { + return false; + } + int positive = 0; + int nonpositive = 0; + int topped_nonpositive = 0; + int topped_positive = 0; + for (const Bucket& bucket : state) { + if (bucket.debt > 0) { + ++positive; + topped_positive += !bucket.caps.empty(); + } else { + ++nonpositive; + topped_nonpositive += !bucket.caps.empty(); + } + } + return positive == 3 && nonpositive == 1 && topped_nonpositive == 1 && + topped_positive == 0; +} + +std::vector enumerate_tq_terminals() { + std::set terminals; + for (int energy = 0; energy <= 2; ++energy) { + for (int c0 = 1; c0 < kHeight; ++c0) { + for (int c1 = c0; c1 < kHeight; ++c1) { + for (int c2 = c1; c2 < kHeight; ++c2) { + if (c0 <= energy || c0 + c1 + c2 - energy > kHeight) continue; + for (int p0 = 1; p0 <= kHeight; ++p0) { + for (int p1 = p0; p1 <= kHeight; ++p1) { + for (int p2 = p1; p2 <= kHeight; ++p2) { + if (p0 + p1 + p2 - energy != kHeight) continue; + Debts debts{{-energy, p0, p1, p2}}; + Caps caps; + caps[0] = {c0, c1, c2}; + State state = canonical_state(debts, caps); + if (is_tq_terminal(state)) terminals.insert(state); + } + } + } + } + } + } + } + return {terminals.begin(), terminals.end()}; +} + +std::optional apply_exhausting_action(const State& state, int exhausted, + const ExhaustAction& action) { + if (action.old_color < 0 || action.old_color >= kColors || + action.final_color < 0 || action.final_color >= kColors || + action.old_color == action.final_color || action.old_cap < 1 || + action.old_cap >= kHeight || + !source_is_legal(state, exhausted, action.old_color, action.old_cap)) { + return std::nullopt; + } + Debts debts = state_debts(state); + Caps caps = state_caps(state); + auto& old_caps = caps[action.old_color]; + const auto found = std::find(old_caps.begin(), old_caps.end(), action.old_cap); + if (found == old_caps.end()) return std::nullopt; + old_caps.erase(found); + debts[action.old_color] += action.old_cap; + debts[action.final_color] += kHeight - action.old_cap; + State successor = canonical_state(debts, caps); + if (!algebraically_consistent(successor, exhausted + 1)) return std::nullopt; + return successor; +} + +std::vector reverse_exhausting_candidates(const State& terminal) { + std::vector candidates; + for (int old_cap = 1; old_cap < kHeight; ++old_cap) { + for (int old_color = 0; old_color < kColors; ++old_color) { + for (int final_color = 0; final_color < kColors; ++final_color) { + if (old_color == final_color) continue; + Debts debts = state_debts(terminal); + Caps caps = state_caps(terminal); + debts[old_color] -= old_cap; + debts[final_color] -= kHeight - old_cap; + caps[old_color].push_back(old_cap); + Debts tested = debts; + tested[old_color] += old_cap; + if (positive_count(tested) > kEmpty) continue; + State parent = canonical_state(debts, caps); + if (algebraically_consistent(parent, 0)) candidates.push_back(parent); + } + } + } + std::sort(candidates.begin(), candidates.end()); + return candidates; +} + +std::vector exhausting_actions_to(const State& parent, + const State& terminal) { + std::set actions; + for (int old_color = 0; old_color < kColors; ++old_color) { + const std::set unique_caps(parent[old_color].caps.begin(), + parent[old_color].caps.end()); + for (const int old_cap : unique_caps) { + for (int final_color = 0; final_color < kColors; ++final_color) { + ExhaustAction action{old_color, old_cap, final_color}; + const auto successor = apply_exhausting_action(parent, 0, action); + if (successor && *successor == terminal) actions.insert(action); + } + } + } + return {actions.begin(), actions.end()}; +} + +Bridge build_bridge() { + Bridge bridge; + const auto terminals = enumerate_tq_terminals(); + bridge.terminal_count = terminals.size(); + std::vector> labeled; + std::set> pairs; + for (const State& terminal : terminals) { + for (const State& parent : reverse_exhausting_candidates(terminal)) { + labeled.emplace_back(parent, terminal); + pairs.emplace(parent, terminal); + } + } + bridge.labeled_candidates = labeled.size(); + bridge.canonical_edge_count = pairs.size(); + std::set parents; + for (const auto& pair : pairs) parents.insert(pair.first); + bridge.canonical_parent_count = parents.size(); + + for (const auto& pair : pairs) { + const State& parent = pair.first; + const State& terminal = pair.second; + const auto legal = legal_sources(parent, 0); + const auto actions = exhausting_actions_to(parent, terminal); + require(actions.size() == 1, "bridge edge does not have a unique bad action"); + const ExhaustAction bad = actions.front(); + if (legal.size() == 1) continue; + ++bridge.sibling_edge_count; + + Debts labeled_terminal = state_debts(parent); + Caps remaining_caps = state_caps(parent); + auto& bad_caps = remaining_caps[bad.old_color]; + const auto found = std::find(bad_caps.begin(), bad_caps.end(), bad.old_cap); + require(found != bad_caps.end(), "bridge bad source is absent"); + bad_caps.erase(found); + labeled_terminal[bad.old_color] += bad.old_cap; + labeled_terminal[bad.final_color] += kHeight - bad.old_cap; + require(canonical_state(labeled_terminal, remaining_caps) == terminal, + "labeled bridge replay does not reach its terminal"); + + int q_color = -1; + for (int color = 0; color < kColors; ++color) { + if (remaining_caps[color].size() == 3) { + require(q_color == -1, "bridge has two three-column colors"); + q_color = color; + } else { + require(remaining_caps[color].empty(), + "bridge remainder is not an all-q triple"); + } + } + require(q_color >= 0, "bridge has no terminal q color"); + std::sort(remaining_caps[q_color].begin(), remaining_caps[q_color].end()); + Edge edge; + edge.ordinal = bridge.edges.size(); + edge.parent = parent; + edge.terminal = terminal; + edge.bad = bad; + edge.terminal_debts = labeled_terminal; + edge.q_color = q_color; + std::copy(remaining_caps[q_color].begin(), remaining_caps[q_color].end(), + edge.q_caps.begin()); + edge.legal_source_count = static_cast(legal.size()); + bridge.edges.push_back(std::move(edge)); + } + + require(bridge.terminal_count == kExpectedTqTerminals, + "Tq terminal count is not 71"); + require(bridge.labeled_candidates == kExpectedLabeledCandidates, + "labeled first-exhaust candidate count is not 624"); + require(bridge.canonical_parent_count == kExpectedCanonicalParents, + "canonical parent count is not 418"); + require(bridge.canonical_edge_count == kExpectedCanonicalEdges, + "canonical edge count is not 429"); + require(bridge.sibling_edge_count == kExpectedSiblingEdges, + "sibling edge count is not 423"); + return bridge; +} + +std::vector cards_for(int q_color, int cap) { + std::vector cards; + for (int color = 0; color < kColors; ++color) { + if (color == q_color) continue; + for (int endpoint = cap + 1; endpoint <= kHeight; ++endpoint) { + cards.push_back({color, endpoint}); + } + } + return cards; +} + +std::uint64_t multinomial(const Counts& counts) { + static constexpr std::array factorial{{ + 1ULL, 1ULL, 2ULL, 6ULL, 24ULL, 120ULL, 720ULL, 5040ULL, + 40320ULL, 362880ULL, 3628800ULL, 39916800ULL, 479001600ULL, + 6227020800ULL, 87178291200ULL, 1307674368000ULL, + 20922789888000ULL, 355687428096000ULL, 6402373705728000ULL, + 121645100408832000ULL, 2432902008176640000ULL}}; + int total = 0; + for (const int count : counts) { + if (count < 0) return 0; + total += count; + } + require(total >= 0 && total <= 20, "multinomial total exceeds table"); + std::uint64_t result = factorial[static_cast(total)]; + for (const int count : counts) { + result /= factorial[static_cast(count)]; + } + return result; +} + +std::uint64_t count_completions(const Counts& residual, + const std::array& tail_lengths, + const std::array& cards) { + int positions = 0; + int residual_total = 0; + for (const int length : tail_lengths) { + if (length < 0) return 0; + positions += length; + } + for (const int value : residual) { + if (value < 0) return 0; + residual_total += value; + } + if (positions != residual_total) return 0; + + Counts remaining = residual; + std::uint64_t result = 0; + const auto choose_boundaries = [&](const auto& self, int slot) -> void { + while (slot < 3 && tail_lengths[slot] == 0) ++slot; + if (slot == 3) { + result += multinomial(remaining); + return; + } + for (int color = 0; color < kColors; ++color) { + if (color == cards[slot].color || remaining[color] == 0) continue; + --remaining[color]; + self(self, slot + 1); + ++remaining[color]; + } + }; + choose_boundaries(choose_boundaries, 0); + return result; +} + +bool q_source_is_legal(const Edge& edge, int cap) { + return source_is_legal(edge.parent, 0, edge.q_color, cap); +} + +bool bad_source_legal_after_live(const Edge& edge, int q_cap, const Card& card) { + Debts debts = state_debts(edge.parent); + debts[edge.q_color] += q_cap; + debts[card.color] -= q_cap; + return source_is_legal(debts, 0, edge.bad.old_color, edge.bad.old_cap); +} + +bool immediate_tq_after_sibling_exhaust(const Edge& edge, int slot, + const Card& card) { + if (card.endpoint != kHeight) return false; + Debts debts = state_debts(edge.parent); + Caps caps = state_caps(edge.parent); + auto& q_caps = caps[edge.q_color]; + const auto found = std::find(q_caps.begin(), q_caps.end(), edge.q_caps[slot]); + require(found != q_caps.end(), "direct sibling cap is absent"); + q_caps.erase(found); + debts[edge.q_color] += edge.q_caps[slot]; + debts[card.color] += kHeight - edge.q_caps[slot]; + return is_tq_terminal(canonical_state(debts, caps)); +} + +bool is_exact_live_tq_corner(const Edge& edge, int slot, + const std::array& cards, int n_value) { + if (n_value != 0 || cards[slot].endpoint != 3) return false; + for (int other = 0; other < 3; ++other) { + if (other == slot) continue; + if (edge.q_caps[other] != 1 || + cards[other].color != cards[slot].color || + cards[other].endpoint != 3) { + return false; + } + } + return true; +} + +bool is_refined_d2_reduction(const Edge& edge, + const std::array& cards) { + bool direct_certified = false; + bool n_ge_3 = false; + bool n_le_2_noncorner = false; + bool nonhandoff = false; + for (int slot = 0; slot < 3; ++slot) { + const int q_cap = edge.q_caps[slot]; + if (!q_source_is_legal(edge, q_cap)) continue; + const Card& card = cards[slot]; + if (card.endpoint == kHeight) { + direct_certified = direct_certified || + !immediate_tq_after_sibling_exhaust(edge, slot, card); + continue; + } + if (!bad_source_legal_after_live(edge, q_cap, card)) { + nonhandoff = true; + continue; + } + const int n_value = q_cap - edge.terminal_debts[card.color]; + require(n_value >= 0, "live handoff has negative N"); + if (n_value >= 3) { + n_ge_3 = true; + } else if (!is_exact_live_tq_corner(edge, slot, cards, n_value)) { + n_le_2_noncorner = true; + } + } + return !direct_certified && !n_ge_3 && !n_le_2_noncorner && nonhandoff; +} + +std::vector enumerate_decorations(const Bridge& bridge) { + static constexpr std::array, 12> expected{{ + {116, 198, 64680}, {117, 732, 252252}, {174, 263, 620928}, + {175, 192, 51744}, {178, 104, 19404}, {184, 6, 462}, + {236, 8, 72072}, {237, 6, 11088}, {238, 4, 924}, + {242, 8, 11088}, {244, 6, 924}, {248, 8, 924}}}; + + std::map> rows; + std::vector decorations; + for (const Edge& edge : bridge.edges) { + if (edge.legal_source_count != 3) continue; + const auto cards0 = cards_for(edge.q_color, edge.q_caps[0]); + const auto cards1 = cards_for(edge.q_color, edge.q_caps[1]); + const auto cards2 = cards_for(edge.q_color, edge.q_caps[2]); + for (const Card& card0 : cards0) { + for (const Card& card1 : cards1) { + for (const Card& card2 : cards2) { + const std::array cards{{card0, card1, card2}}; + Counts residual{}; + const Counts exposed = exposed_counts(edge.parent); + for (int color = 0; color < kColors; ++color) { + residual[color] = kHeight - exposed[color]; + } + residual[edge.bad.final_color] -= kHeight - edge.bad.old_cap; + std::array tails{}; + for (int slot = 0; slot < 3; ++slot) { + residual[cards[slot].color] -= + cards[slot].endpoint - edge.q_caps[slot]; + tails[slot] = kHeight - cards[slot].endpoint; + } + const std::uint64_t completions = + count_completions(residual, tails, cards); + if (completions == 0 || + !is_refined_d2_reduction(edge, cards)) { + continue; + } + Decoration decoration; + decoration.ordinal = decorations.size(); + decoration.edge_index = edge.ordinal; + decoration.cards = cards; + decoration.residual_after_forced = residual; + decoration.free_tail_lengths = tails; + decoration.residual_words_expected = completions; + decorations.push_back(decoration); + auto& row = rows[edge.ordinal]; + ++row.first; + row.second += completions; + } + } + } + } + + require(rows.size() == kExpectedSelectedEdges, + "three-source D2 edge count is not 12"); + for (const auto& item : expected) { + const std::size_t edge = std::get<0>(item); + const auto found = rows.find(edge); + require(found != rows.end(), "expected three-source edge is absent"); + require(found->second.first == std::get<1>(item) && + found->second.second == std::get<2>(item), + "three-source per-edge decoration ledger drifted"); + } + require(decorations.size() == kExpectedDecorations, + "three-source D2 decoration count is not 1535"); + const std::uint64_t words = std::accumulate( + decorations.begin(), decorations.end(), std::uint64_t{0}, + [](std::uint64_t sum, const Decoration& decoration) { + return sum + decoration.residual_words_expected; + }); + require(words == kExpectedResidualWords, + "three-source residual-word weight is not 1106490"); + return decorations; +} + +class FixedFutureSolver { +public: + struct Result { + bool solvable = false; + std::uint32_t safe_mask = 0; + std::string path; + std::uint64_t states = 0; + std::uint64_t transitions = 0; + }; + + FixedFutureSolver(const Debts& debts, + const std::array& sources, + const std::array, kColors>& words) + : initial_debts_(debts), sources_(sources) { + std::uint32_t multiplier = 1; + for (std::size_t column = 0; column < kColors; ++column) { + build_events(column, words[column]); + multipliers_[column] = multiplier; + multiplier *= static_cast(events_[column].size() + 1); + } + memo_.assign(multiplier, -1); + } + + Result solve() { + Result result; + result.solvable = visit(0); + for (std::size_t column = 0; column < kColors; ++column) { + if (safe_from(0, column)) result.safe_mask |= 1U << column; + } + if (result.solvable) { + std::uint32_t state = 0; + while (!goal(state)) { + bool advanced = false; + for (std::size_t column = 0; column < kColors; ++column) { + if (!safe_from(state, column)) continue; + result.path.push_back(static_cast('0' + column)); + state += multipliers_[column]; + advanced = true; + break; + } + require(advanced, "winning fixed future has no safe successor"); + } + } + result.states = states_; + result.transitions = transitions_; + return result; + } + + bool replay(const std::string& path) const { + std::uint32_t state = 0; + for (const char value : path) { + const std::size_t column = static_cast(value - '0'); + if (column >= kColors || !legal(state, column)) return false; + state += multipliers_[column]; + } + return goal(state); + } + +private: + struct Event { + int old_color = 0; + int old_cap = 0; + int next_color = 0; + int next_cap = 0; + }; + + Debts initial_debts_{}; + std::array sources_{}; + std::array, kColors> events_; + std::array, kColors> deltas_; + std::array multipliers_{}; + std::vector memo_; + std::uint64_t states_ = 0; + std::uint64_t transitions_ = 0; + + void build_events(std::size_t column, const std::vector& word) { + int old_color = sources_[column].color; + int old_cap = sources_[column].cap; + int cursor = static_cast(word.size()) - 1; + while (cursor >= 0) { + const int next_color = word[static_cast(cursor)]; + require(next_color != old_color, "hidden word repeats current top color"); + int first = cursor; + while (first > 0 && + word[static_cast(first - 1)] == next_color) { + --first; + } + const int length = cursor - first + 1; + const int next_cap = old_cap + length; + events_[column].push_back({old_color, old_cap, next_color, next_cap}); + old_color = next_color; + old_cap = next_cap; + cursor = first - 1; + } + require(!events_[column].empty() && + events_[column].back().next_cap == kHeight, + "fixed future does not exhaust its column at height seven"); + deltas_[column].assign(events_[column].size() + 1, Debts{}); + for (std::size_t index = 0; index < events_[column].size(); ++index) { + deltas_[column][index + 1] = deltas_[column][index]; + const Event& event = events_[column][index]; + deltas_[column][index + 1][event.old_color] += event.old_cap; + if (event.next_cap == kHeight) { + deltas_[column][index + 1][event.next_color] += + kHeight - event.old_cap; + } else { + deltas_[column][index + 1][event.next_color] -= event.old_cap; + } + } + } + + std::array decode(std::uint32_t state) const { + std::array ranks{}; + for (std::size_t column = 0; column < kColors; ++column) { + ranks[column] = (state / multipliers_[column]) % + (events_[column].size() + 1); + } + return ranks; + } + + int exhausted(const std::array& ranks) const { + int result = 0; + for (std::size_t column = 0; column < kColors; ++column) { + result += ranks[column] == events_[column].size(); + } + return result; + } + + bool goal(std::uint32_t state) const { + return exhausted(decode(state)) >= kEmpty; + } + + bool legal(std::uint32_t state, std::size_t column) const { + const auto ranks = decode(state); + if (ranks[column] == events_[column].size()) return false; + Debts debts = initial_debts_; + for (std::size_t other = 0; other < kColors; ++other) { + for (int color = 0; color < kColors; ++color) { + debts[color] += deltas_[other][ranks[other]][color]; + } + } + const Event& event = events_[column][ranks[column]]; + debts[event.old_color] += event.old_cap; + return positive_count(debts) <= kEmpty + exhausted(ranks); + } + + bool safe_from(std::uint32_t state, std::size_t column) { + if (goal(state) || !legal(state, column)) return false; + ++transitions_; + return visit(state + multipliers_[column]); + } + + bool visit(std::uint32_t state) { + if (goal(state)) return true; + std::int8_t& memo = memo_[state]; + if (memo >= 0) return memo != 0; + ++states_; + for (std::size_t column = 0; column < kColors; ++column) { + if (safe_from(state, column)) { + memo = 1; + return true; + } + } + memo = 0; + return false; + } +}; + +std::string digits(const std::vector& values) { + std::string result; + result.reserve(values.size()); + for (const int value : values) { + result.push_back(static_cast('0' + value)); + } + return result; +} + +FixedFixture make_fixture(const Edge& edge, + const std::array, 3>& q_words) { + FixedFixture fixture; + fixture.debts = state_debts(edge.parent); + fixture.sources[0] = {edge.bad.old_color, edge.bad.old_cap}; + fixture.hidden_bottom_to_top[0].assign( + static_cast(kHeight - edge.bad.old_cap), + edge.bad.final_color); + for (std::size_t slot = 0; slot < 3; ++slot) { + fixture.sources[slot + 1] = {edge.q_color, edge.q_caps[slot]}; + fixture.hidden_bottom_to_top[slot + 1] = q_words[slot]; + } + + Counts used{}; + for (std::size_t column = 0; column < kColors; ++column) { + const auto& word = fixture.hidden_bottom_to_top[column]; + require(word.size() == static_cast( + kHeight - fixture.sources[column].cap), + "fixture hidden word has the wrong length"); + require(!word.empty() && word.back() != fixture.sources[column].color, + "fixture does not begin at a genuine run boundary"); + for (const int color : word) ++used[color]; + } + const Counts exposed = exposed_counts(edge.parent); + for (int color = 0; color < kColors; ++color) { + require(used[color] == kHeight - exposed[color], + "fixture does not realize the parent color inventory"); + } + return fixture; +} + +template +bool for_each_fixed_future(const Decoration& decoration, const Edge& edge, + Callback&& callback) { + Counts remaining = decoration.residual_after_forced; + std::array boundaries{{-1, -1, -1}}; + std::uint64_t emitted = 0; + bool stopped = false; + + const auto choose_boundaries = [&](const auto& self, int slot) -> void { + if (stopped) return; + while (slot < 3 && decoration.free_tail_lengths[slot] == 0) ++slot; + if (slot < 3) { + for (int color = 0; color < kColors; ++color) { + if (color == decoration.cards[slot].color || remaining[color] == 0) { + continue; + } + --remaining[color]; + boundaries[slot] = color; + self(self, slot + 1); + boundaries[slot] = -1; + ++remaining[color]; + if (stopped) return; + } + return; + } + + std::vector pool; + for (int color = 0; color < kColors; ++color) { + pool.insert(pool.end(), static_cast(remaining[color]), color); + } + std::array, 3> free_top_to_bottom; + int free_slots = 0; + for (int q_slot = 0; q_slot < 3; ++q_slot) { + const int length = decoration.free_tail_lengths[q_slot]; + free_top_to_bottom[q_slot].assign(static_cast(length), -1); + if (length > 0) { + require(boundaries[q_slot] >= 0, "free tail has no boundary color"); + free_top_to_bottom[q_slot][0] = boundaries[q_slot]; + free_slots += length - 1; + } + } + require(static_cast(pool.size()) == free_slots, + "free-tail pool has the wrong size"); + + do { + std::size_t cursor = 0; + for (int q_slot = 0; q_slot < 3; ++q_slot) { + for (std::size_t position = 1; + position < free_top_to_bottom[q_slot].size(); ++position) { + free_top_to_bottom[q_slot][position] = pool[cursor++]; + } + } + require(cursor == pool.size(), "free-tail permutation was not consumed"); + + std::array, 3> q_words_bottom_to_top; + for (int q_slot = 0; q_slot < 3; ++q_slot) { + q_words_bottom_to_top[q_slot].assign( + free_top_to_bottom[q_slot].rbegin(), + free_top_to_bottom[q_slot].rend()); + const int forced = decoration.cards[q_slot].endpoint - + edge.q_caps[q_slot]; + q_words_bottom_to_top[q_slot].insert( + q_words_bottom_to_top[q_slot].end(), + static_cast(forced), + decoration.cards[q_slot].color); + } + ++emitted; + if (!callback(q_words_bottom_to_top, free_top_to_bottom)) { + stopped = true; + return; + } + } while (std::next_permutation(pool.begin(), pool.end())); + }; + choose_boundaries(choose_boundaries, 0); + if (!stopped) { + require(emitted == decoration.residual_words_expected, + "fixed-future enumeration disagrees with its exact weight"); + } + return !stopped; +} + +std::string join_words(const std::array, kColors>& words, + char separator) { + std::ostringstream output; + for (std::size_t column = 0; column < kColors; ++column) { + if (column != 0) output << separator; + output << digits(words[column]); + } + return output.str(); +} + +std::string cards_text(const std::array& cards) { + std::ostringstream output; + for (std::size_t slot = 0; slot < 3; ++slot) { + if (slot != 0) output << ','; + output << cards[slot].color << ':' << cards[slot].endpoint; + } + return output.str(); +} + +void update_hash(std::uint64_t& hash, const std::string& text) { + static constexpr std::uint64_t prime = 1099511628211ULL; + for (const unsigned char value : text) { + hash ^= value; + hash *= prime; + } + hash ^= static_cast('\n'); + hash *= prime; +} + +Sample make_sample(std::uint64_t future_index, const Decoration& decoration, + const Edge& edge, const FixedFixture& fixture, + const FixedFutureSolver::Result& result) { + Sample sample; + sample.present = true; + sample.future_index = future_index; + sample.decoration_index = decoration.ordinal; + sample.edge_ordinal = edge.ordinal; + sample.solvable = result.solvable; + sample.safe_mask = result.safe_mask; + sample.path = result.path; + for (std::size_t column = 0; column < kColors; ++column) { + sample.hidden_words_bottom_to_top[column] = + digits(fixture.hidden_bottom_to_top[column]); + } + return sample; +} + +void write_local_no(std::ostream& output, const Sample& sample, + const Edge& edge, const Decoration& decoration) { + output << "{\"future_index\":" << sample.future_index + << ",\"decoration_index\":" << sample.decoration_index + << ",\"bridge_edge\":" << sample.edge_ordinal + << ",\"parent_debts\":["; + const Debts debts = state_debts(edge.parent); + for (int color = 0; color < kColors; ++color) { + if (color != 0) output << ','; + output << debts[color]; + } + output << "],\"bad_source\":[" << edge.bad.old_color << ',' + << edge.bad.old_cap << ',' << edge.bad.final_color + << "],\"q_color\":" << edge.q_color << ",\"q_caps\":["; + for (std::size_t slot = 0; slot < 3; ++slot) { + if (slot != 0) output << ','; + output << edge.q_caps[slot]; + } + output << "],\"cards\":["; + for (std::size_t slot = 0; slot < 3; ++slot) { + if (slot != 0) output << ','; + output << '[' << decoration.cards[slot].color << ',' + << decoration.cards[slot].endpoint << ']'; + } + output << "],\"hidden_words_bottom_to_top\":["; + for (std::size_t column = 0; column < kColors; ++column) { + if (column != 0) output << ','; + output << '"' << sample.hidden_words_bottom_to_top[column] << '"'; + } + output << "],\"local_status\":\"NO\",\"safe_source_mask\":0}\n"; +} + +void run_solver_self_tests() { + { + const Debts debts{{-5, 0, 2, 3}}; + const std::array sources{{ + Source{0, 3}, Source{0, 3}, Source{0, 3}, Source{0, 3}}}; + const std::array, kColors> words{{ + std::vector{2, 2, 2, 1}, + std::vector{3, 3, 2, 1}, + std::vector{3, 3, 2, 1}, + std::vector{1, 1, 1, 1}}}; + FixedFutureSolver solver(debts, sources, words); + const auto result = solver.solve(); + require(!result.solvable && result.safe_mask == 0 && result.path.empty(), + "known four-way local lock did not solve as local NO"); + } + { + const Debts debts{}; + const std::array sources{{ + Source{0, 6}, Source{1, 6}, Source{2, 6}, Source{3, 6}}}; + const std::array, kColors> words{{ + std::vector{1}, std::vector{2}, + std::vector{3}, std::vector{0}}}; + FixedFutureSolver solver(debts, sources, words); + const auto result = solver.solve(); + require(result.solvable && result.safe_mask != 0, + "synthetic two-exhaustion fixture is not YES"); + require(solver.replay(result.path), + "synthetic winning path did not replay"); + } +} + +RunStats run(const Options& options, const Bridge& bridge, + const std::vector& decorations) { + RunStats stats; + stats.limit_requested = options.limit; + stats.decorations_expected = decorations.size(); + for (const Decoration& decoration : decorations) { + stats.residual_words_expected += decoration.residual_words_expected; + } + require(stats.decorations_expected == kExpectedDecorations, + "run decoration universe is not 1535"); + require(stats.residual_words_expected == kExpectedResidualWords, + "run fixed-future universe is not 1106490"); + + std::map row_for_edge; + for (const Decoration& decoration : decorations) { + const std::size_t edge_ordinal = bridge.edges[decoration.edge_index].ordinal; + auto found = row_for_edge.find(edge_ordinal); + if (found == row_for_edge.end()) { + const std::size_t row = stats.per_edge.size(); + row_for_edge.emplace(edge_ordinal, row); + EdgeStats edge_stats; + edge_stats.edge_ordinal = edge_ordinal; + stats.per_edge.push_back(edge_stats); + found = row_for_edge.find(edge_ordinal); + } + EdgeStats& edge_stats = stats.per_edge[found->second]; + ++edge_stats.decorations; + edge_stats.residual_words_expected += decoration.residual_words_expected; + } + require(stats.per_edge.size() == kExpectedSelectedEdges, + "run edge universe is not 12"); + + std::optional result_ledger; + std::optional local_no_ledger; + if (!options.output_dir.empty()) { + std::filesystem::create_directories(options.output_dir); + result_ledger.emplace(options.output_dir / "fixed-future-results.tsv", + std::ios::binary); + local_no_ledger.emplace(options.output_dir / "local-no-ledger.jsonl", + std::ios::binary); + require(*result_ledger && *local_no_ledger, + "could not open fixed-future ledgers"); + *result_ledger << "future_index\tdecoration_index\tbridge_edge\tcards" + "\thidden_words_bottom_to_top\tlocal_status" + "\tsafe_source_mask\tescape_columns\n"; + } + + const std::uint64_t effective_limit = options.limit == 0 + ? stats.residual_words_expected + : std::min(options.limit, stats.residual_words_expected); + const auto started = std::chrono::steady_clock::now(); + bool stop = false; + for (const Decoration& decoration : decorations) { + if (stop) break; + const Edge& edge = bridge.edges[decoration.edge_index]; + EdgeStats& edge_stats = stats.per_edge[row_for_edge.at(edge.ordinal)]; + std::uint64_t decoration_checked = 0; + const bool complete_decoration = for_each_fixed_future( + decoration, edge, + [&](const std::array, 3>& q_words, + const std::array, 3>&) { + if (stats.residual_words_checked >= effective_limit) return false; + const FixedFixture fixture = make_fixture(edge, q_words); + FixedFutureSolver solver(fixture.debts, fixture.sources, + fixture.hidden_bottom_to_top); + const auto result = solver.solve(); + const std::uint64_t future_index = stats.residual_words_checked; + ++stats.residual_words_checked; + ++edge_stats.residual_words_checked; + ++decoration_checked; + stats.states += result.states; + stats.transitions += result.transitions; + edge_stats.states += result.states; + edge_stats.transitions += result.transitions; + ++edge_stats.safe_mask_distribution[result.safe_mask]; + + if (result.solvable) { + require(result.safe_mask != 0 && !result.path.empty(), + "local YES has no safe first source or path"); + require(solver.replay(result.path), + "local YES escape path did not replay"); + ++stats.local_yes; + ++edge_stats.local_yes; + ++stats.winning_paths_replayed; + if (!stats.first_yes) { + stats.first_yes = make_sample( + future_index, decoration, edge, fixture, result); + } + } else { + require(result.safe_mask == 0 && result.path.empty(), + "local NO unexpectedly has a winning first source"); + ++stats.local_no; + ++edge_stats.local_no; + const Sample sample = make_sample( + future_index, decoration, edge, fixture, result); + if (!stats.first_no) stats.first_no = sample; + if (local_no_ledger) { + write_local_no(*local_no_ledger, sample, edge, decoration); + } + } + + std::ostringstream row; + row << future_index << '\t' << decoration.ordinal << '\t' + << edge.ordinal << '\t' << cards_text(decoration.cards) << '\t' + << join_words(fixture.hidden_bottom_to_top, ',') << '\t' + << (result.solvable ? "YES" : "NO") << '\t' + << result.safe_mask << '\t' << result.path; + const std::string row_text = row.str(); + update_hash(stats.ledger_hash, row_text); + if (result_ledger) *result_ledger << row_text << '\n'; + + if (stats.residual_words_checked % 100000 == 0) { + std::cout << "progress fixed_futures=" + << stats.residual_words_checked << '/' + << stats.residual_words_expected + << " local_no=" << stats.local_no << '\n'; + } + return true; + }); + if (complete_decoration) { + require(decoration_checked == decoration.residual_words_expected, + "complete decoration did not enumerate its exact weight"); + } + if (stats.residual_words_checked >= effective_limit) stop = true; + } + + stats.elapsed_seconds = std::chrono::duration( + std::chrono::steady_clock::now() - started).count(); + stats.universe_complete = + stats.residual_words_checked == stats.residual_words_expected; + stats.self_checks_passed = true; + require(stats.local_yes + stats.local_no == stats.residual_words_checked, + "local YES/NO counts do not partition checked futures"); + require(stats.winning_paths_replayed == stats.local_yes, + "not every local YES path replayed"); + for (const EdgeStats& edge_stats : stats.per_edge) { + require(edge_stats.local_yes + edge_stats.local_no == + edge_stats.residual_words_checked, + "per-edge YES/NO counts do not partition checked futures"); + if (stats.universe_complete) { + require(edge_stats.residual_words_checked == + edge_stats.residual_words_expected, + "full run did not cover a selected edge"); + } + } + return stats; +} + +std::string status(const RunStats& stats) { + if (!stats.universe_complete) return "INCOMPLETE"; + if (stats.local_no != 0) return "LOCAL_NO_RESIDUALS_EXPORTED"; + return "THREE_SOURCE_D2_CHECKPOINT_FAMILY_ELIMINATED"; +} + +std::string bool_json(bool value) { + return value ? "true" : "false"; +} + +std::string hex_u64(std::uint64_t value) { + static constexpr char digits_table[] = "0123456789abcdef"; + std::string result(16, '0'); + for (int index = 15; index >= 0; --index) { + result[static_cast(index)] = digits_table[value & 15U]; + value >>= 4U; + } + return result; +} + +void write_sample_json(std::ostream& output, const std::optional& sample) { + if (!sample) { + output << "null"; + return; + } + output << "{\"future_index\":" << sample->future_index + << ",\"decoration_index\":" << sample->decoration_index + << ",\"bridge_edge\":" << sample->edge_ordinal + << ",\"local_status\":\"" + << (sample->solvable ? "YES" : "NO") + << "\",\"safe_source_mask\":" << sample->safe_mask + << ",\"escape_columns\":\"" << sample->path + << "\",\"hidden_words_bottom_to_top\":["; + for (std::size_t column = 0; column < kColors; ++column) { + if (column != 0) output << ','; + output << '"' << sample->hidden_words_bottom_to_top[column] << '"'; + } + output << "]}"; +} + +void write_report(const Options& options, const Bridge& bridge, + const RunStats& stats) { + require(!options.output_dir.empty(), "report output directory is empty"); + const std::string run_status = status(stats); + const bool eliminated = stats.universe_complete && stats.local_no == 0; + std::ofstream json(options.output_dir / "report.json", std::ios::binary); + require(static_cast(json), "could not create report.json"); + json << "{\n" + << " \"schema_version\": 1,\n" + << " \"experiment\": \"c4_h7_d2_three_source_checkpoint\",\n" + << " \"status\": \"" << run_status << "\",\n" + << " \"parameters\": {\"colors\":4,\"height\":7,\"empty\":2},\n" + << " \"scope\": {\n" + << " \"parent_checkpoint_only\": true,\n" + << " \"fixed_hidden_futures\": true,\n" + << " \"zero_debt_past_restored\": false,\n" + << " \"full_h7_theorem\": false\n" + << " },\n" + << " \"bridge_reconstruction\": {\"tq_terminals\":" + << bridge.terminal_count << ",\"labeled_candidates\":" + << bridge.labeled_candidates << ",\"canonical_parents\":" + << bridge.canonical_parent_count << ",\"canonical_edges\":" + << bridge.canonical_edge_count << ",\"sibling_edges\":" + << bridge.sibling_edge_count << "},\n" + << " \"universe\": {\"selected_edges\":" << stats.per_edge.size() + << ",\"decorations\":" << stats.decorations_expected + << ",\"labeled_fixed_futures\":" << stats.residual_words_expected + << "},\n" + << " \"run\": {\"limit_requested\":" << stats.limit_requested + << ",\"universe_complete\":" << bool_json(stats.universe_complete) + << ",\"fixed_futures_checked\":" << stats.residual_words_checked + << ",\"local_yes\":" << stats.local_yes + << ",\"local_no\":" << stats.local_no + << ",\"winning_paths_replayed\":" << stats.winning_paths_replayed + << ",\"states\":" << stats.states + << ",\"transitions\":" << stats.transitions + << ",\"elapsed_seconds\":" << stats.elapsed_seconds << "},\n" + << " \"claims\": {\"three_source_checkpoint_family_eliminated\":" + << bool_json(eliminated) + << ",\"zero_debt_initial_family_eliminated\":false," + "\"universal_c4_h7_solvability\":false},\n" + << " \"ledgers\": {\"fixed_future_results\":" + "\"fixed-future-results.tsv\",\"local_no\":" + "\"local-no-ledger.jsonl\",\"result_rows_fnv1a64\":\"" + << hex_u64(stats.ledger_hash) << "\"},\n" + << " \"first_local_yes\": "; + write_sample_json(json, stats.first_yes); + json << ",\n \"first_local_no\": "; + write_sample_json(json, stats.first_no); + json << ",\n \"per_edge\": [\n"; + for (std::size_t index = 0; index < stats.per_edge.size(); ++index) { + const EdgeStats& row = stats.per_edge[index]; + if (index != 0) json << ",\n"; + json << " {\"bridge_edge\":" << row.edge_ordinal + << ",\"decorations\":" << row.decorations + << ",\"fixed_futures_expected\":" << row.residual_words_expected + << ",\"fixed_futures_checked\":" << row.residual_words_checked + << ",\"local_yes\":" << row.local_yes + << ",\"local_no\":" << row.local_no + << ",\"states\":" << row.states + << ",\"transitions\":" << row.transitions + << ",\"safe_mask_distribution\":{"; + bool first = true; + for (const auto& mask : row.safe_mask_distribution) { + if (!first) json << ','; + first = false; + json << '"' << mask.first << "\":" << mask.second; + } + json << "}}"; + } + json << "\n ],\n \"self_checks_passed\": " + << bool_json(stats.self_checks_passed) << "\n}\n"; + require(static_cast(json), "failed while writing report.json"); + + std::ofstream markdown(options.output_dir / "report.md", std::ios::binary); + require(static_cast(markdown), "could not create report.md"); + markdown << "# c=4, h=7 three-source D2 checkpoint audit\n\n" + << "- Status: `" << run_status << "`.\n" + << "- Exact target universe: 12 bridge edges, 1,535 decorations, " + "1,106,490 labeled fixed futures.\n" + << "- Checked fixed futures: " << stats.residual_words_checked + << ".\n" + << "- Parent-checkpoint local YES / NO: " << stats.local_yes + << " / " << stats.local_no << ".\n" + << "- Replayed winning paths: " << stats.winning_paths_replayed + << ".\n\n" + << "This audit starts at the nonzero-debt first-exhaustion parent. " + "It does not restore any zero-debt past, eliminate an initial-layout " + "family, or prove the full c=4,h=7 theorem.\n\n" + << "| Bridge edge | Decorations | Expected futures | Checked | " + "Local YES | Local NO |\n" + << "|---:|---:|---:|---:|---:|---:|\n"; + for (const EdgeStats& row : stats.per_edge) { + markdown << '|' << row.edge_ordinal << '|' << row.decorations << '|' + << row.residual_words_expected << '|' + << row.residual_words_checked << '|' << row.local_yes << '|' + << row.local_no << "|\n"; + } + require(static_cast(markdown), "failed while writing report.md"); +} + +} // namespace + +int main(int argc, char** argv) { + try { + const Options options = parse_options(argc, argv); + if (options.self_test) run_solver_self_tests(); + const Bridge bridge = build_bridge(); + const auto decorations = enumerate_decorations(bridge); + const RunStats stats = run(options, bridge, decorations); + if (!options.output_dir.empty()) write_report(options, bridge, stats); + std::cout << "status=" << status(stats) + << " edges=" << stats.per_edge.size() + << " decorations=" << stats.decorations_expected + << " fixed_futures=" << stats.residual_words_checked << '/' + << stats.residual_words_expected + << " local_yes=" << stats.local_yes + << " local_no=" << stats.local_no + << " elapsed_seconds=" << stats.elapsed_seconds << '\n'; + return 0; + } catch (const std::exception& error) { + std::cerr << "error: " << error.what() << '\n'; + return 2; + } +} diff --git a/scripts/validate_c4_h7_d2_three_source_report.py b/scripts/validate_c4_h7_d2_three_source_report.py new file mode 100644 index 0000000..4673127 --- /dev/null +++ b/scripts/validate_c4_h7_d2_three_source_report.py @@ -0,0 +1,454 @@ +#!/usr/bin/env python3 +"""Strict evidence and claim-boundary validator for the c4/h7 D2 three-source audit. + +This validator intentionally does not promote a fixed-future parent-checkpoint NO +to a zero-debt initial-layout counterexample. The independent semantic checker in +tests/check_c4_h7_d2_three_source.py is responsible for rebuilding and solving the +enumerated universe; this script makes the emitted artifact set self-consistent. +""" + +from __future__ import annotations + +import argparse +import copy +import json +import math +from collections import Counter +from pathlib import Path +from typing import NoReturn + + +TOTAL_DECORATIONS = 1_535 +TOTAL_FUTURES = 1_106_490 +BRIDGE = { + "tq_terminals": 71, + "labeled_candidates": 624, + "canonical_parents": 418, + "canonical_edges": 429, + "sibling_edges": 423, +} +EDGE_ROWS = ( + (116, 198, 64_680), + (117, 732, 252_252), + (174, 263, 620_928), + (175, 192, 51_744), + (178, 104, 19_404), + (184, 6, 462), + (236, 8, 72_072), + (237, 6, 11_088), + (238, 4, 924), + (242, 8, 11_088), + (244, 6, 924), + (248, 8, 924), +) +TSV_HEADER = ( + "future_index\tdecoration_index\tbridge_edge\tcards\t" + "hidden_words_bottom_to_top\tlocal_status\tsafe_source_mask\tescape_columns" +) +ROOT_KEYS = { + "schema_version", + "experiment", + "status", + "parameters", + "scope", + "bridge_reconstruction", + "universe", + "run", + "claims", + "ledgers", + "first_local_yes", + "first_local_no", + "per_edge", + "self_checks_passed", +} +RUN_KEYS = { + "limit_requested", + "universe_complete", + "fixed_futures_checked", + "local_yes", + "local_no", + "winning_paths_replayed", + "states", + "transitions", + "elapsed_seconds", +} +PER_EDGE_KEYS = { + "bridge_edge", + "decorations", + "fixed_futures_expected", + "fixed_futures_checked", + "local_yes", + "local_no", + "states", + "transitions", + "safe_mask_distribution", +} +SAMPLE_KEYS = { + "future_index", + "decoration_index", + "bridge_edge", + "local_status", + "safe_source_mask", + "escape_columns", + "hidden_words_bottom_to_top", +} +LOCAL_NO_KEYS = { + "future_index", + "decoration_index", + "bridge_edge", + "parent_debts", + "bad_source", + "q_color", + "q_caps", + "cards", + "hidden_words_bottom_to_top", + "local_status", + "safe_source_mask", +} + + +def fail(message: str) -> NoReturn: + raise AssertionError(message) + + +def require(condition: bool, message: str) -> None: + if not condition: + fail(message) + + +def integer(value: object, label: str) -> int: + require(isinstance(value, int) and not isinstance(value, bool), f"{label} is not an integer") + return int(value) + + +def boolean(value: object, label: str) -> bool: + require(isinstance(value, bool), f"{label} is not a Boolean") + return bool(value) + + +def exact_keys(value: object, keys: set[str], label: str) -> dict[str, object]: + require(isinstance(value, dict), f"{label} is not an object") + actual = set(value) + require(actual == keys, f"{label} keys drifted: missing={sorted(keys - actual)} extra={sorted(actual - keys)}") + return value + + +def fnv1a64_rows(lines: list[str]) -> str: + # This is the historical offset used by the production experiment. It is + # deliberately reproduced exactly rather than replaced by the standard + # FNV-1a offset basis. + value = 1_469_598_103_934_665_603 + for line in lines: + for byte in (line + "\n").encode("utf-8"): + value ^= byte + value = (value * 1_099_511_628_211) & 0xFFFFFFFFFFFFFFFF + return f"{value:016x}" + + +def parse_words(text: str, label: str) -> list[str]: + words = text.split(",") + require(len(words) == 4, f"{label} does not contain four physical columns") + require( + all(word and len(word) <= 7 and set(word) <= set("0123") for word in words), + f"{label} contains an invalid bottom-to-top word", + ) + return words + + +def parse_cards(text: str, label: str) -> list[list[int]]: + fields = text.split(",") + require(len(fields) == 3, f"{label} does not contain three q cards") + cards: list[list[int]] = [] + for slot, field in enumerate(fields): + parts = field.split(":") + require(len(parts) == 2 and all(part.isdigit() for part in parts), f"{label}[{slot}] is malformed") + color, endpoint = map(int, parts) + require(0 <= color < 4 and 1 <= endpoint <= 7, f"{label}[{slot}] is outside c4/h7") + cards.append([color, endpoint]) + return cards + + +def validate_sample(sample: object, label: str, expected: dict[str, object] | None) -> None: + if expected is None: + require(sample is None, f"{label} exists although the corresponding class is empty") + return + row = exact_keys(sample, SAMPLE_KEYS, label) + require(row == expected, f"{label} does not match the first corresponding TSV row") + + +def load_report(path: Path) -> dict[str, object]: + value = json.loads(path.read_text(encoding="utf-8")) + return exact_keys(value, ROOT_KEYS, "report") + + +def validate_report(report: dict[str, object], report_path: Path) -> None: + require(report.get("schema_version") == 1, "unsupported schema version") + require(report.get("experiment") == "c4_h7_d2_three_source_checkpoint", "experiment name drifted") + require(report.get("parameters") == {"colors": 4, "height": 7, "empty": 2}, "parameter tuple drifted") + require( + report.get("scope") + == { + "parent_checkpoint_only": True, + "fixed_hidden_futures": True, + "zero_debt_past_restored": False, + "full_h7_theorem": False, + }, + "scope overclaims a zero-debt or full-h7 result", + ) + require(report.get("bridge_reconstruction") == BRIDGE, "bridge reconstruction census drifted") + require( + report.get("universe") + == {"selected_edges": 12, "decorations": TOTAL_DECORATIONS, "labeled_fixed_futures": TOTAL_FUTURES}, + "three-source universe census drifted", + ) + require(report.get("self_checks_passed") is True, "production structural self-checks did not pass") + + run = exact_keys(report.get("run"), RUN_KEYS, "run") + limit = integer(run.get("limit_requested"), "run.limit_requested") + checked = integer(run.get("fixed_futures_checked"), "run.fixed_futures_checked") + local_yes = integer(run.get("local_yes"), "run.local_yes") + local_no = integer(run.get("local_no"), "run.local_no") + replayed = integer(run.get("winning_paths_replayed"), "run.winning_paths_replayed") + states = integer(run.get("states"), "run.states") + transitions = integer(run.get("transitions"), "run.transitions") + elapsed = run.get("elapsed_seconds") + require(limit >= 0, "negative limit requested") + expected_checked = TOTAL_FUTURES if limit == 0 else min(limit, TOTAL_FUTURES) + require(checked == expected_checked, "checked count is not the exact requested prefix") + require(local_yes >= 0 and local_no >= 0 and local_yes + local_no == checked, "local YES/NO partition is invalid") + require(replayed == local_yes, "a local YES path was not replayed") + require(states >= checked and transitions >= 0, "DP counters are invalid") + require(isinstance(elapsed, (int, float)) and not isinstance(elapsed, bool), "elapsed_seconds is not numeric") + require(math.isfinite(float(elapsed)) and float(elapsed) >= 0.0, "elapsed_seconds is invalid") + complete = checked == TOTAL_FUTURES + require(boolean(run.get("universe_complete"), "run.universe_complete") is complete, "coverage flag disagrees with checked count") + + claims = report.get("claims") + require(isinstance(claims, dict), "claims is not an object") + require( + set(claims) + == {"three_source_checkpoint_family_eliminated", "zero_debt_initial_family_eliminated", "universal_c4_h7_solvability"}, + "claim keys drifted", + ) + eliminated = complete and local_no == 0 + require(claims.get("three_source_checkpoint_family_eliminated") is eliminated, "narrow checkpoint claim disagrees with evidence") + require(claims.get("zero_debt_initial_family_eliminated") is False, "report promotes checkpoint evidence to zero debt") + require(claims.get("universal_c4_h7_solvability") is False, "report promotes checkpoint evidence to the full h7 theorem") + expected_status = ( + "INCOMPLETE" + if not complete + else "LOCAL_NO_RESIDUALS_EXPORTED" + if local_no + else "THREE_SOURCE_D2_CHECKPOINT_FAMILY_ELIMINATED" + ) + require(report.get("status") == expected_status, "status is not the conservative checkpoint status") + + per_edge = report.get("per_edge") + require(isinstance(per_edge, list) and len(per_edge) == len(EDGE_ROWS), "per-edge ledger is incomplete") + remaining = checked + edge_totals = Counter() + for ordinal, (row, expected) in enumerate(zip(per_edge, EDGE_ROWS)): + value = exact_keys(row, PER_EDGE_KEYS, f"per_edge[{ordinal}]") + edge, decorations, futures = expected + row_checked = min(remaining, futures) + remaining -= row_checked + require(value.get("bridge_edge") == edge, f"per_edge[{ordinal}] edge/order drifted") + require(value.get("decorations") == decorations, f"edge {edge} decoration census drifted") + require(value.get("fixed_futures_expected") == futures, f"edge {edge} future census drifted") + require(value.get("fixed_futures_checked") == row_checked, f"edge {edge} is not the expected checked prefix") + row_yes = integer(value.get("local_yes"), f"edge {edge}.local_yes") + row_no = integer(value.get("local_no"), f"edge {edge}.local_no") + row_states = integer(value.get("states"), f"edge {edge}.states") + row_transitions = integer(value.get("transitions"), f"edge {edge}.transitions") + require(row_yes >= 0 and row_no >= 0 and row_yes + row_no == row_checked, f"edge {edge} local partition is invalid") + require(row_states >= row_checked and row_transitions >= 0, f"edge {edge} DP counters are invalid") + masks = value.get("safe_mask_distribution") + require(isinstance(masks, dict), f"edge {edge} mask distribution is not an object") + parsed_masks = Counter() + for key, count in masks.items(): + require(isinstance(key, str) and key.isdigit() and 0 <= int(key) < 16, f"edge {edge} has an invalid safe mask") + parsed_masks[int(key)] = integer(count, f"edge {edge}.mask[{key}]") + require(parsed_masks[int(key)] > 0, f"edge {edge} records a nonpositive mask count") + require(sum(parsed_masks.values()) == row_checked, f"edge {edge} mask counts do not cover checked rows") + require(parsed_masks[0] == row_no, f"edge {edge} mask zero is not exactly local NO") + edge_totals.update(checked=row_checked, yes=row_yes, no=row_no, states=row_states, transitions=row_transitions) + require(remaining == 0, "checked prefix extends past the expected edge universe") + require( + edge_totals == Counter(checked=checked, yes=local_yes, no=local_no, states=states, transitions=transitions), + "per-edge aggregates disagree with run totals", + ) + + ledgers = report.get("ledgers") + require( + isinstance(ledgers, dict) + and set(ledgers) == {"fixed_future_results", "local_no", "result_rows_fnv1a64"}, + "ledger declaration drifted", + ) + require(ledgers.get("fixed_future_results") == "fixed-future-results.tsv", "unexpected fixed-result ledger path") + require(ledgers.get("local_no") == "local-no-ledger.jsonl", "unexpected local-NO ledger path") + declared_hash = ledgers.get("result_rows_fnv1a64") + require( + isinstance(declared_hash, str) and len(declared_hash) == 16 and set(declared_hash) <= set("0123456789abcdef"), + "result row hash is not lowercase 64-bit hex", + ) + + directory = report_path.parent + result_path = directory / "fixed-future-results.tsv" + no_path = directory / "local-no-ledger.jsonl" + require(result_path.is_file(), "fixed-future-results.tsv is missing") + require(no_path.is_file(), "local-no-ledger.jsonl is missing") + require((directory / "report.md").is_file(), "report.md is missing") + raw_lines = result_path.read_text(encoding="utf-8").splitlines() + require(raw_lines and raw_lines[0] == TSV_HEADER, "fixed-result TSV header drifted") + data_lines = raw_lines[1:] + require(len(data_lines) == checked, "fixed-result TSV does not contain exactly the checked prefix") + require(fnv1a64_rows(data_lines) == declared_hash, "fixed-result TSV FNV-1a hash mismatch") + + tsv_rows: list[dict[str, object]] = [] + tsv_no_rows: list[dict[str, object]] = [] + tsv_yes = 0 + edge_from_tsv: Counter[tuple[int, str]] = Counter() + first_yes: dict[str, object] | None = None + first_no: dict[str, object] | None = None + previous_decoration = -1 + for future_index, line in enumerate(data_lines): + fields = line.split("\t") + require(len(fields) == 8, f"TSV row {future_index} does not have eight fields") + require(fields[0].isdigit() and int(fields[0]) == future_index, f"TSV row {future_index} index drifted") + require(fields[1].isdigit(), f"TSV row {future_index} decoration index is invalid") + decoration = int(fields[1]) + require(previous_decoration <= decoration < TOTAL_DECORATIONS, f"TSV row {future_index} decoration order is invalid") + previous_decoration = decoration + require(fields[2].isdigit(), f"TSV row {future_index} edge is invalid") + edge = int(fields[2]) + require(edge in {item[0] for item in EDGE_ROWS}, f"TSV row {future_index} has an unknown selected edge") + cards = parse_cards(fields[3], f"TSV row {future_index}.cards") + words = parse_words(fields[4], f"TSV row {future_index}.words") + status = fields[5] + require(fields[6].isdigit(), f"TSV row {future_index} safe mask is invalid") + mask = int(fields[6]) + path = fields[7] + require(set(path) <= set("0123"), f"TSV row {future_index} path has an invalid source") + if status == "YES": + require(0 < mask < 16 and path, f"TSV row {future_index} local YES lacks a witness") + tsv_yes += 1 + else: + require(status == "NO", f"TSV row {future_index} has an unknown local status") + require(mask == 0 and not path, f"TSV row {future_index} local NO has a witness") + sample = { + "future_index": future_index, + "decoration_index": decoration, + "bridge_edge": edge, + "local_status": status, + "safe_source_mask": mask, + "escape_columns": path, + "hidden_words_bottom_to_top": words, + } + detailed = {**sample, "cards": cards} + tsv_rows.append(detailed) + edge_from_tsv[edge, status] += 1 + if status == "YES" and first_yes is None: + first_yes = sample + if status == "NO": + tsv_no_rows.append(detailed) + if first_no is None: + first_no = sample + require(tsv_yes == local_yes and len(tsv_no_rows) == local_no, "TSV local partition disagrees with report") + for row in per_edge: + assert isinstance(row, dict) + edge = int(row["bridge_edge"]) + require(edge_from_tsv[edge, "YES"] == row["local_yes"], f"edge {edge} TSV YES count drifted") + require(edge_from_tsv[edge, "NO"] == row["local_no"], f"edge {edge} TSV NO count drifted") + validate_sample(report.get("first_local_yes"), "first_local_yes", first_yes) + validate_sample(report.get("first_local_no"), "first_local_no", first_no) + + no_lines = no_path.read_text(encoding="utf-8").splitlines() + require(len(no_lines) == local_no, "local-NO ledger line count disagrees with the report") + for ordinal, (raw, tsv_row) in enumerate(zip(no_lines, tsv_no_rows)): + value = json.loads(raw) + row = exact_keys(value, LOCAL_NO_KEYS, f"local_no[{ordinal}]") + require(row.get("local_status") == "NO" and row.get("safe_source_mask") == 0, f"local_no[{ordinal}] is not a local NO") + for key in ("future_index", "decoration_index", "bridge_edge", "hidden_words_bottom_to_top", "cards"): + require(row.get(key) == tsv_row[key], f"local_no[{ordinal}].{key} disagrees with TSV") + debts = row.get("parent_debts") + require( + isinstance(debts, list) + and len(debts) == 4 + and all(isinstance(value, int) and not isinstance(value, bool) for value in debts) + and sum(debts) == 0, + f"local_no[{ordinal}] parent debts are invalid", + ) + bad = row.get("bad_source") + require( + isinstance(bad, list) + and len(bad) == 3 + and all(isinstance(value, int) and not isinstance(value, bool) for value in bad) + and 0 <= bad[0] < 4 + and 0 <= bad[1] <= 7 + and 0 <= bad[2] < 4, + f"local_no[{ordinal}] bad source is invalid", + ) + require(isinstance(row.get("q_color"), int) and 0 <= int(row["q_color"]) < 4, f"local_no[{ordinal}] q color is invalid") + q_caps = row.get("q_caps") + require( + isinstance(q_caps, list) + and len(q_caps) == 3 + and all(isinstance(value, int) and not isinstance(value, bool) and 0 <= value <= 7 for value in q_caps), + f"local_no[{ordinal}] q caps are invalid", + ) + + +def run_negative_tests(report: dict[str, object], report_path: Path) -> None: + mutations = ( + ("claim zero-debt elimination", lambda value: value["claims"].__setitem__("zero_debt_initial_family_eliminated", True)), + ("claim the full h7 theorem", lambda value: value["claims"].__setitem__("universal_c4_h7_solvability", True)), + ("erase parent-checkpoint scope", lambda value: value["scope"].__setitem__("parent_checkpoint_only", False)), + ("claim a global NO status", lambda value: value.__setitem__("status", "GLOBAL_NO_FOUND")), + ("alter the bridge census", lambda value: value["bridge_reconstruction"].__setitem__("canonical_edges", 430)), + ("alter the TSV hash", lambda value: value["ledgers"].__setitem__("result_rows_fnv1a64", "0" * 16)), + ) + for label, mutate in mutations: + candidate = copy.deepcopy(report) + mutate(candidate) + try: + validate_report(candidate, report_path) + except AssertionError: + continue + fail(f"negative test accepted mutation: {label}") + if report["status"] == "INCOMPLETE": + candidate = copy.deepcopy(report) + candidate["status"] = "THREE_SOURCE_D2_CHECKPOINT_FAMILY_ELIMINATED" + candidate["claims"]["three_source_checkpoint_family_eliminated"] = True + try: + validate_report(candidate, report_path) + except AssertionError: + pass + else: + fail("negative test accepted bounded checkpoint-family elimination") + + +def parse_args() -> argparse.Namespace: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("report", type=Path) + parser.add_argument("--negative-tests", action="store_true") + return parser.parse_args() + + +def main() -> int: + args = parse_args() + report = load_report(args.report) + validate_report(report, args.report) + if args.negative_tests: + run_negative_tests(report, args.report) + run = report["run"] + assert isinstance(run, dict) + print( + "strict three-source checkpoint validation passed: " + f"status={report['status']} fixed={run['fixed_futures_checked']}/{TOTAL_FUTURES} " + f"checkpoint_local_no={run['local_no']} global_no_claimed=0" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/tests/check_c4_h7_d2_three_source.py b/tests/check_c4_h7_d2_three_source.py new file mode 100644 index 0000000..534b04b --- /dev/null +++ b/tests/check_c4_h7_d2_three_source.py @@ -0,0 +1,1047 @@ +#!/usr/bin/env python3 +"""Independent audit of the three-legal-source c4/h7 D2 checkpoint family. + +No production code is imported. This file independently rebuilds the +first-exhaustion bridge, the 12 selected canonical edges, 1,535 next-run +decorations, and their 1,106,490 labelled fixed hidden futures. Every checked +future is solved by a separate fixed-chain recursion and its YES/NO result, +safe-source mask, and deterministic winning path can be compared row-for-row +with the C++ ledger. + +The initial debts in this experiment are generally nonzero. A local NO is +therefore exported only as a parent-checkpoint residual. It is never called a +balanced initial-layout counterexample. +""" + +from __future__ import annotations + +import argparse +from collections import Counter +from dataclasses import dataclass +from functools import lru_cache +import itertools +import json +import math +from pathlib import Path +import subprocess +import tempfile +from typing import Iterable, Iterator, NoReturn, Sequence, TextIO + + +HEIGHT = 7 +COLORS = 4 +EMPTY = 2 +EXPERIMENT = "c4_h7_d2_three_source_checkpoint" + +EXPECTED_TERMINALS = 71 +EXPECTED_LABELED_CANDIDATES = 624 +EXPECTED_PARENTS = 418 +EXPECTED_CANONICAL_EDGES = 429 +EXPECTED_SIBLING_EDGES = 423 +EXPECTED_DECORATIONS = 1_535 +EXPECTED_FIXED_FUTURES = 1_106_490 +EXPECTED_EDGE_ROWS: tuple[tuple[int, int, int], ...] = ( + (116, 198, 64_680), + (117, 732, 252_252), + (174, 263, 620_928), + (175, 192, 51_744), + (178, 104, 19_404), + (184, 6, 462), + (236, 8, 72_072), + (237, 6, 11_088), + (238, 4, 924), + (242, 8, 11_088), + (244, 6, 924), + (248, 8, 924), +) + +FNV_OFFSET = 1_469_598_103_934_665_603 +FNV_PRIME = 1_099_511_628_211 +TSV_HEADER = ( + "future_index\tdecoration_index\tbridge_edge\tcards\t" + "hidden_words_bottom_to_top\tlocal_status\t" + "safe_source_mask\tescape_columns" +) + +Bucket = tuple[int, tuple[int, ...]] +State = tuple[Bucket, Bucket, Bucket, Bucket] +Action = tuple[int, int, int] +Card = tuple[int, int] +Source = tuple[int, int] +Run = tuple[int, int] +LiveColumn = tuple[int, int, tuple[Run, ...]] +Columns = tuple[ + LiveColumn | None, + LiveColumn | None, + LiveColumn | None, + LiveColumn | None, +] + + +def fail(message: str) -> NoReturn: + raise AssertionError(message) + + +def require(condition: bool, message: str) -> None: + if not condition: + fail(message) + + +def canonical_state(debts: Sequence[int], columns: Iterable[Source]) -> State: + caps: list[list[int]] = [[] for _ in range(COLORS)] + for color, cap in columns: + caps[color].append(cap) + result = tuple( + sorted( + (int(debts[color]), tuple(sorted(caps[color]))) + for color in range(COLORS) + ) + ) + require(len(result) == COLORS, "canonicalization lost a colour") + return result # type: ignore[return-value] + + +def state_debts(state: State) -> tuple[int, int, int, int]: + return tuple(bucket[0] for bucket in state) # type: ignore[return-value] + + +def state_caps(state: State) -> tuple[tuple[int, ...], ...]: + return tuple(bucket[1] for bucket in state) + + +def exposed_counts(state: State) -> tuple[int, int, int, int]: + return tuple(debt + sum(caps) for debt, caps in state) # type: ignore[return-value] + + +def source_legal( + debts_or_state: Sequence[int] | State, + exhausted: int, + color: int, + cap: int, +) -> bool: + if isinstance(debts_or_state[0], tuple): + debts = [bucket[0] for bucket in debts_or_state] # type: ignore[index] + else: + debts = [int(value) for value in debts_or_state] # type: ignore[arg-type] + debts[color] += cap + return sum(value > 0 for value in debts) <= EMPTY + exhausted + + +def physical_sources(state: State) -> Iterator[Source]: + for color, (_debt, caps) in enumerate(state): + for cap in caps: + yield color, cap + + +def legal_sources(state: State, exhausted: int) -> tuple[Source, ...]: + return tuple( + source + for source in physical_sources(state) + if source_legal(state, exhausted, source[0], source[1]) + ) + + +def state_consistent(state: State, exhausted: int) -> bool: + if tuple(sorted(state)) != state: + return False + if sum(len(caps) for _debt, caps in state) != COLORS - exhausted: + return False + if sum(debt for debt, _caps in state) != exhausted * HEIGHT: + return False + if any(not 1 <= cap < HEIGHT for _debt, caps in state for cap in caps): + return False + exposed = exposed_counts(state) + multiplicity = tuple(len(caps) for _debt, caps in state) + if any(not multiplicity[color] <= exposed[color] <= HEIGHT + for color in range(COLORS)): + return False + remaining = tuple(HEIGHT - count for count in exposed) + return all( + multiplicity[color] + <= sum(remaining[other] for other in range(COLORS) if other != color) + for color in range(COLORS) + ) + + +def is_tq_terminal(state: State) -> bool: + if not state_consistent(state, 1) or legal_sources(state, 1): + return False + positive = [index for index, (debt, _caps) in enumerate(state) if debt > 0] + nonpositive = [index for index, (debt, _caps) in enumerate(state) if debt <= 0] + topped = [index for index, (_debt, caps) in enumerate(state) if caps] + return len(positive) == 3 and len(nonpositive) == 1 and topped == nonpositive + + +def enumerate_tq_terminals() -> tuple[State, ...]: + terminals: set[State] = set() + for energy in range(3): + for caps in itertools.combinations_with_replacement(range(1, HEIGHT), 3): + if min(caps) <= energy or sum(caps) - energy > HEIGHT: + continue + for positive in itertools.combinations_with_replacement( + range(1, HEIGHT + 1), 3 + ): + if sum(positive) - energy != HEIGHT: + continue + candidate = tuple( + sorted(((-energy, caps), *((value, ()) for value in positive))) + ) + if is_tq_terminal(candidate): # type: ignore[arg-type] + terminals.add(candidate) # type: ignore[arg-type] + return tuple(sorted(terminals)) + + +def apply_exhausting(parent: State, exhausted: int, action: Action) -> State | None: + old_color, old_cap, final_color = action + if old_color == final_color or old_cap not in range(1, HEIGHT): + return None + if old_cap not in parent[old_color][1]: + return None + if not source_legal(parent, exhausted, old_color, old_cap): + return None + debts = list(state_debts(parent)) + caps = [list(values) for values in state_caps(parent)] + caps[old_color].remove(old_cap) + debts[old_color] += old_cap + debts[final_color] += HEIGHT - old_cap + successor = canonical_state( + debts, + ((color, cap) for color in range(COLORS) for cap in caps[color]), + ) + return successor if state_consistent(successor, exhausted + 1) else None + + +def exhausting_actions_to(parent: State, terminal: State) -> tuple[Action, ...]: + actions: set[Action] = set() + for old_color, (_debt, caps) in enumerate(parent): + for old_cap in sorted(set(caps)): + for final_color in range(COLORS): + action = old_color, old_cap, final_color + if apply_exhausting(parent, 0, action) == terminal: + actions.add(action) + return tuple(sorted(actions)) + + +def reverse_bridge( + terminals: Sequence[State], +) -> tuple[int, tuple[tuple[State, State], ...]]: + labelled: list[tuple[State, State]] = [] + for terminal in terminals: + for old_cap in range(1, HEIGHT): + for old_color in range(COLORS): + for final_color in range(COLORS): + if old_color == final_color: + continue + debts = list(state_debts(terminal)) + caps = [list(values) for values in state_caps(terminal)] + debts[old_color] -= old_cap + debts[final_color] -= HEIGHT - old_cap + caps[old_color].append(old_cap) + tested = debts.copy() + tested[old_color] += old_cap + if sum(value > 0 for value in tested) > EMPTY: + continue + parent = canonical_state( + debts, + ((color, cap) for color in range(COLORS) + for cap in caps[color]), + ) + if state_consistent(parent, 0): + labelled.append((parent, terminal)) + return len(labelled), tuple(sorted(set(labelled))) + + +@dataclass(frozen=True) +class Edge: + ordinal: int + parent: State + terminal: State + bad: Action + terminal_debts: tuple[int, int, int, int] + q_color: int + q_caps: tuple[int, int, int] + legal_source_count: int + legal_q_slots: tuple[int, ...] + + +@dataclass(frozen=True) +class Bridge: + edges: tuple[Edge, ...] + terminal_count: int + labelled_count: int + parent_count: int + canonical_edge_count: int + + +def build_bridge() -> Bridge: + terminals = enumerate_tq_terminals() + labelled_count, pairs = reverse_bridge(terminals) + parents = {parent for parent, _terminal in pairs} + edges: list[Edge] = [] + for parent, terminal in pairs: + legal = legal_sources(parent, 0) + actions = exhausting_actions_to(parent, terminal) + require(len(actions) == 1, "bridge edge lacks one unique bad action") + bad = actions[0] + if len(legal) == 1: + continue + caps = [list(values) for values in state_caps(parent)] + caps[bad[0]].remove(bad[1]) + labelled_debts = list(state_debts(parent)) + labelled_debts[bad[0]] += bad[1] + labelled_debts[bad[2]] += HEIGHT - bad[1] + require( + canonical_state( + labelled_debts, + ((color, cap) for color in range(COLORS) for cap in caps[color]), + ) == terminal, + "labelled bad action does not replay to its terminal", + ) + q_candidates = [color for color in range(COLORS) if len(caps[color]) == 3] + require(len(q_candidates) == 1, "all-q sibling colour is ambiguous") + q_color = q_candidates[0] + require(all(not caps[color] for color in range(COLORS) if color != q_color), + "terminal remainder is not an all-q triple") + q_caps = tuple(sorted(caps[q_color])) + legal_q_slots = tuple( + slot for slot, cap in enumerate(q_caps) + if source_legal(parent, 0, q_color, cap) + ) + edges.append( + Edge( + len(edges), parent, terminal, bad, + tuple(labelled_debts), # type: ignore[arg-type] + q_color, q_caps, len(legal), legal_q_slots, + ) + ) + require(len(terminals) == EXPECTED_TERMINALS, "Tq terminal census drifted") + require(labelled_count == EXPECTED_LABELED_CANDIDATES, + "labelled reverse census drifted") + require(len(parents) == EXPECTED_PARENTS, "canonical parent census drifted") + require(len(pairs) == EXPECTED_CANONICAL_EDGES, + "canonical edge census drifted") + require(len(edges) == EXPECTED_SIBLING_EDGES, "sibling edge census drifted") + return Bridge(tuple(edges), len(terminals), labelled_count, len(parents), len(pairs)) + + +def cards_for(q_color: int, cap: int) -> tuple[Card, ...]: + return tuple( + (color, endpoint) + for color in range(COLORS) + if color != q_color + for endpoint in range(cap + 1, HEIGHT + 1) + ) + + +def sibling_after_exhaust(edge: Edge, slot: int, card: Card) -> State: + cap = edge.q_caps[slot] + debts = list(state_debts(edge.parent)) + caps = [list(values) for values in state_caps(edge.parent)] + caps[edge.q_color].remove(cap) + debts[edge.q_color] += cap + debts[card[0]] += HEIGHT - cap + return canonical_state( + debts, + ((color, value) for color in range(COLORS) for value in caps[color]), + ) + + +def bad_legal_after_live(edge: Edge, slot: int, card: Card) -> bool: + debts = list(state_debts(edge.parent)) + cap = edge.q_caps[slot] + debts[edge.q_color] += cap + debts[card[0]] -= cap + return source_legal(debts, 0, edge.bad[0], edge.bad[1]) + + +def exact_live_corner( + edge: Edge, slot: int, chosen: tuple[Card, Card, Card], n_value: int +) -> bool: + card = chosen[slot] + if n_value != 0 or card[1] != 3: + return False + return all( + edge.q_caps[other] == 1 and chosen[other] == (card[0], 3) + for other in range(3) if other != slot + ) + + +def refined_d2(edge: Edge, chosen: tuple[Card, Card, Card]) -> bool: + direct = n_ge_3 = n_le_2 = nonhandoff = False + for slot in edge.legal_q_slots: + card = chosen[slot] + cap = edge.q_caps[slot] + if card[1] == HEIGHT: + direct = direct or not is_tq_terminal(sibling_after_exhaust(edge, slot, card)) + continue + if not bad_legal_after_live(edge, slot, card): + nonhandoff = True + continue + n_value = cap - edge.terminal_debts[card[0]] + require(n_value >= 0, "live handoff produced negative N") + if n_value >= 3: + n_ge_3 = True + elif not exact_live_corner(edge, slot, chosen, n_value): + n_le_2 = True + return not direct and not n_ge_3 and not n_le_2 and nonhandoff + + +def multinomial(counts: Sequence[int]) -> int: + if any(value < 0 for value in counts): + return 0 + result = math.factorial(sum(counts)) + for value in counts: + result //= math.factorial(value) + return result + + +def completion_count( + residual: tuple[int, int, int, int], + tails: tuple[int, int, int], + chosen: tuple[Card, Card, Card], +) -> int: + if any(value < 0 for value in residual) or sum(residual) != sum(tails): + return 0 + active_slots = tuple(slot for slot, length in enumerate(tails) if length) + result = 0 + for boundaries in itertools.product(range(COLORS), repeat=len(active_slots)): + counts = list(residual) + valid = True + for slot, color in zip(active_slots, boundaries): + if color == chosen[slot][0] or counts[color] == 0: + valid = False + break + counts[color] -= 1 + if valid: + result += multinomial(counts) + return result + + +@dataclass(frozen=True) +class Decoration: + ordinal: int + edge: Edge + chosen: tuple[Card, Card, Card] + residual: tuple[int, int, int, int] + tails: tuple[int, int, int] + weight: int + + +def derive_decorations() -> tuple[Bridge, tuple[Decoration, ...]]: + bridge = build_bridge() + decorations: list[Decoration] = [] + rows: dict[int, list[int]] = {} + for edge in bridge.edges: + if edge.legal_source_count != 3: + continue + options = tuple(cards_for(edge.q_color, cap) for cap in edge.q_caps) + for raw in itertools.product(*options): + chosen = tuple(raw) # type: ignore[assignment] + residual = [HEIGHT - count for count in exposed_counts(edge.parent)] + residual[edge.bad[2]] -= HEIGHT - edge.bad[1] + tails: list[int] = [] + for cap, card in zip(edge.q_caps, chosen): + residual[card[0]] -= card[1] - cap + tails.append(HEIGHT - card[1]) + residual_tuple = tuple(residual) # type: ignore[assignment] + tails_tuple = tuple(tails) # type: ignore[assignment] + weight = completion_count(residual_tuple, tails_tuple, chosen) + if not weight or not refined_d2(edge, chosen): + continue + decoration = Decoration( + len(decorations), edge, chosen, + residual_tuple, tails_tuple, weight, + ) + decorations.append(decoration) + row = rows.setdefault(edge.ordinal, [0, 0]) + row[0] += 1 + row[1] += weight + require(tuple((edge, *rows.get(edge, [0, 0])) for edge, _d, _w in EXPECTED_EDGE_ROWS) + == EXPECTED_EDGE_ROWS, "selected edge ledger drifted") + require(len(decorations) == EXPECTED_DECORATIONS, "decoration census drifted") + require(sum(item.weight for item in decorations) == EXPECTED_FIXED_FUTURES, + "fixed-future weight drifted") + return bridge, tuple(decorations) + + +def next_multiset_permutation(values: list[int]) -> bool: + pivot = len(values) - 2 + while pivot >= 0 and values[pivot] >= values[pivot + 1]: + pivot -= 1 + if pivot < 0: + return False + successor = len(values) - 1 + while values[successor] <= values[pivot]: + successor -= 1 + values[pivot], values[successor] = values[successor], values[pivot] + values[pivot + 1:] = reversed(values[pivot + 1:]) + return True + + +def fixed_futures( + decoration: Decoration, +) -> Iterator[tuple[tuple[int, ...], tuple[int, ...], tuple[int, ...]]]: + remaining = list(decoration.residual) + boundaries = [-1, -1, -1] + produced = 0 + + def choose(slot: int) -> Iterator[ + tuple[tuple[int, ...], tuple[int, ...], tuple[int, ...]] + ]: + while slot < 3 and decoration.tails[slot] == 0: + slot += 1 + if slot < 3: + for color in range(COLORS): + if color == decoration.chosen[slot][0] or remaining[color] == 0: + continue + remaining[color] -= 1 + boundaries[slot] = color + yield from choose(slot + 1) + boundaries[slot] = -1 + remaining[color] += 1 + return + + pool = sorted( + color for color in range(COLORS) for _ in range(remaining[color]) + ) + free_slots = sum(max(0, length - 1) for length in decoration.tails) + require(len(pool) == free_slots, "free-tail pool size drifted") + while True: + cursor = 0 + words: list[tuple[int, ...]] = [] + for q_slot in range(3): + length = decoration.tails[q_slot] + free_top: list[int] = [] + if length: + require(boundaries[q_slot] >= 0, "free tail lacks boundary colour") + free_top.append(boundaries[q_slot]) + free_top.extend(pool[cursor:cursor + length - 1]) + cursor += length - 1 + cap = decoration.edge.q_caps[q_slot] + card = decoration.chosen[q_slot] + forced = (card[0],) * (card[1] - cap) + words.append(tuple(reversed(free_top)) + forced) + require(cursor == len(pool), "free-tail permutation was not consumed") + yield tuple(words) # type: ignore[return-value] + if not next_multiset_permutation(pool): + break + + for future in choose(0): + produced += 1 + yield future + require(produced == decoration.weight, + f"decoration {decoration.ordinal} emitted {produced}, expected {decoration.weight}") + + +def runs(cells: Iterable[int]) -> tuple[Run, ...]: + result: list[Run] = [] + for color in cells: + if result and result[-1][0] == color: + result[-1] = color, result[-1][1] + 1 + else: + result.append((color, 1)) + return tuple(result) + + +def fixture( + decoration: Decoration, + q_words: tuple[tuple[int, ...], tuple[int, ...], tuple[int, ...]], +) -> tuple[tuple[int, int, int, int], tuple[Source, ...], tuple[tuple[int, ...], ...]]: + edge = decoration.edge + sources: tuple[Source, ...] = ( + (edge.bad[0], edge.bad[1]), + *((edge.q_color, cap) for cap in edge.q_caps), + ) + words: tuple[tuple[int, ...], ...] = ( + (edge.bad[2],) * (HEIGHT - edge.bad[1]), + *q_words, + ) + used = Counter(color for word in words for color in word) + hidden = tuple(HEIGHT - count for count in exposed_counts(edge.parent)) + require(tuple(used[color] for color in range(COLORS)) == hidden, + "fixture inventory does not realize its checkpoint") + for source, word in zip(sources, words): + require(len(word) == HEIGHT - source[1], "fixture column length drifted") + require(word and word[-1] != source[0], "fixture merged into current top") + return state_debts(edge.parent), sources, words + + +def solve_fixture( + debts: tuple[int, int, int, int], + sources: tuple[Source, ...], + words_bottom_to_top: tuple[tuple[int, ...], ...], +) -> tuple[bool, int, str]: + columns: Columns = tuple( + (source[0], source[1], runs(reversed(word))) + for source, word in zip(sources, words_bottom_to_top) + ) # type: ignore[assignment] + + def step( + current_debts: tuple[int, int, int, int], + exhausted: int, + current_columns: Columns, + source_index: int, + ) -> tuple[tuple[int, int, int, int], int, Columns] | None: + column = current_columns[source_index] + if column is None: + return None + top, cap, future = column + if not future or not source_legal(current_debts, exhausted, top, cap): + return None + next_color, length = future[0] + require(next_color != top and length > 0, "fixed chain contains a merged edge") + child_debts = list(current_debts) + child_debts[top] += cap + child_columns = list(current_columns) + child_exhausted = exhausted + if len(future) == 1: + require(cap + length == HEIGHT, "final run misses height seven") + child_debts[next_color] += length + child_columns[source_index] = None + child_exhausted += 1 + else: + require(cap + length < HEIGHT, "nonfinal run reaches height seven") + child_debts[next_color] -= cap + child_columns[source_index] = (next_color, cap + length, future[1:]) + return ( + tuple(child_debts), # type: ignore[arg-type] + child_exhausted, + tuple(child_columns), # type: ignore[arg-type] + ) + + @lru_cache(maxsize=None) + def win( + current_debts: tuple[int, int, int, int], + exhausted: int, + current_columns: Columns, + ) -> bool: + if exhausted >= EMPTY: + return True + return any( + child is not None and win(*child) + for source_index in range(COLORS) + for child in (step(current_debts, exhausted, current_columns, source_index),) + ) + + solvable = win(debts, 0, columns) + mask = 0 + for source_index in range(COLORS): + child = step(debts, 0, columns, source_index) + if child is not None and win(*child): + mask |= 1 << source_index + path: list[int] = [] + current = (debts, 0, columns) + if solvable: + while current[1] < EMPTY: + advanced = False + for source_index in range(COLORS): + child = step(*current, source_index) + if child is not None and win(*child): + path.append(source_index) + current = child + advanced = True + break + require(advanced, "winning fixture has no replayable successor") + require(bool(mask) == solvable, "safe mask disagrees with fixed-future outcome") + if solvable: + require(current[1] >= EMPTY and path, "winning path did not reach the goal") + else: + require(mask == 0 and not path, "local NO has a winning witness") + return solvable, mask, "".join(str(source) for source in path) + + +def fnv_row(hash_value: int, row: str) -> int: + for value in (row + "\n").encode("ascii"): + hash_value ^= value + hash_value = (hash_value * FNV_PRIME) & ((1 << 64) - 1) + return hash_value + + +def sample( + future_index: int, + decoration: Decoration, + words: tuple[tuple[int, ...], ...], + solvable: bool, + mask: int, + path: str, +) -> dict[str, object]: + return { + "future_index": future_index, + "decoration_index": decoration.ordinal, + "bridge_edge": decoration.edge.ordinal, + "local_status": "YES" if solvable else "NO", + "safe_source_mask": mask, + "escape_columns": path, + "hidden_words_bottom_to_top": [ + "".join(str(color) for color in word) for word in words + ], + } + + +def production_no_object( + row_sample: dict[str, object], decoration: Decoration +) -> dict[str, object]: + edge = decoration.edge + return { + "future_index": row_sample["future_index"], + "decoration_index": decoration.ordinal, + "bridge_edge": edge.ordinal, + "parent_debts": list(state_debts(edge.parent)), + "bad_source": list(edge.bad), + "q_color": edge.q_color, + "q_caps": list(edge.q_caps), + "cards": [list(card) for card in decoration.chosen], + "hidden_words_bottom_to_top": row_sample["hidden_words_bottom_to_top"], + "local_status": "NO", + "safe_source_mask": 0, + } + + +def independent_no_object( + row_sample: dict[str, object], decoration: Decoration +) -> dict[str, object]: + return { + **production_no_object(row_sample, decoration), + "scope": "nonzero_debt_parent_checkpoint_fixed_future", + "zero_debt_past_restored": False, + "global_counterexample": False, + } + + +class ProductionRows: + def __init__(self, tsv_path: Path | None, local_no_path: Path | None): + self.tsv: TextIO | None = None + self.local_no: TextIO | None = None + if tsv_path is not None: + self.tsv = tsv_path.open("r", encoding="utf-8", newline="") + require(self.tsv.readline().rstrip("\r\n") == TSV_HEADER, + "production TSV header drifted") + if local_no_path is not None: + self.local_no = local_no_path.open("r", encoding="utf-8") + + def compare_row(self, expected: str) -> None: + if self.tsv is None: + return + actual = self.tsv.readline() + require(actual != "", "production TSV ended before the independent universe") + require(actual.rstrip("\r\n") == expected, + f"production fixed-future row differs:\nactual={actual.rstrip()}\nexpected={expected}") + + def compare_local_no(self, expected: dict[str, object]) -> None: + if self.local_no is None: + return + raw = self.local_no.readline() + require(raw != "", "production local-NO ledger ended early") + actual = json.loads(raw) + require(actual == expected, + f"production local-NO row differs: {actual} != {expected}") + + def finish(self) -> None: + if self.tsv is not None: + require(self.tsv.readline() == "", "production TSV has unverified extra rows") + self.tsv.close() + if self.local_no is not None: + require(self.local_no.readline() == "", + "production local-NO ledger has unverified extra rows") + self.local_no.close() + + +def audit_status(complete: bool, local_no: int) -> str: + if not complete: + return "INCOMPLETE" + if local_no: + return "LOCAL_NO_RESIDUALS_EXPORTED" + return "THREE_SOURCE_D2_CHECKPOINT_FAMILY_ELIMINATED" + + +def audit( + target: int, + production_rows: ProductionRows | None = None, + independent_local_no: Path | None = None, +) -> dict[str, object]: + require(0 < target <= EXPECTED_FIXED_FUTURES, + "fixed-future limit is outside the exact universe") + bridge, decorations = derive_decorations() + expected_by_edge = {edge: (count, weight) + for edge, count, weight in EXPECTED_EDGE_ROWS} + per_edge: dict[int, dict[str, object]] = { + edge: { + "bridge_edge": edge, + "decorations": count, + "fixed_futures_expected": weight, + "fixed_futures_checked": 0, + "local_yes": 0, + "local_no": 0, + "safe_mask_distribution": Counter(), + } + for edge, (count, weight) in expected_by_edge.items() + } + local_output: TextIO | None = None + if independent_local_no is not None: + independent_local_no.parent.mkdir(parents=True, exist_ok=True) + local_output = independent_local_no.open("w", encoding="utf-8", newline="\n") + + checked = local_yes = local_no = replayed = 0 + first_yes: dict[str, object] | None = None + first_no: dict[str, object] | None = None + hash_value = FNV_OFFSET + try: + for decoration in decorations: + if checked >= target: + break + emitted = 0 + for q_words in fixed_futures(decoration): + if checked >= target: + break + emitted += 1 + debts, sources, words = fixture(decoration, q_words) + solvable, mask, path = solve_fixture(debts, sources, words) + row_sample = sample( + checked, decoration, words, solvable, mask, path + ) + cards_text = ",".join( + f"{color}:{endpoint}" for color, endpoint in decoration.chosen + ) + words_text = ",".join(row_sample["hidden_words_bottom_to_top"]) + row = ( + f"{checked}\t{decoration.ordinal}\t{decoration.edge.ordinal}\t" + f"{cards_text}\t{words_text}\t" + f"{'YES' if solvable else 'NO'}\t{mask}\t{path}" + ) + if production_rows is not None: + production_rows.compare_row(row) + hash_value = fnv_row(hash_value, row) + edge_row = per_edge[decoration.edge.ordinal] + edge_row["fixed_futures_checked"] += 1 # type: ignore[operator] + masks: Counter[int] = edge_row["safe_mask_distribution"] # type: ignore[assignment] + masks[mask] += 1 + if solvable: + local_yes += 1 + replayed += 1 + edge_row["local_yes"] += 1 # type: ignore[operator] + if first_yes is None: + first_yes = row_sample + else: + local_no += 1 + edge_row["local_no"] += 1 # type: ignore[operator] + if first_no is None: + first_no = row_sample + production_object = production_no_object(row_sample, decoration) + if production_rows is not None: + production_rows.compare_local_no(production_object) + if local_output is not None: + local_output.write(json.dumps( + independent_no_object(row_sample, decoration), + sort_keys=True, + ) + "\n") + checked += 1 + if checked % 100_000 == 0: + print( + f"independent progress fixed_futures={checked}/{target} " + f"local_no={local_no}", + flush=True, + ) + if checked < target: + require(emitted == decoration.weight, + f"decoration {decoration.ordinal} coverage drifted") + finally: + if local_output is not None: + local_output.close() + require(checked == target, "independent audit stopped before its limit") + require(local_yes + local_no == checked, "local YES/NO partition drifted") + require(replayed == local_yes, "a local YES path was not replayed") + if production_rows is not None: + production_rows.finish() + + edge_rows: list[dict[str, object]] = [] + for edge, _count, _weight in EXPECTED_EDGE_ROWS: + row = per_edge[edge] + masks: Counter[int] = row["safe_mask_distribution"] # type: ignore[assignment] + row["safe_mask_distribution"] = { + str(mask): count for mask, count in sorted(masks.items()) + } + edge_rows.append(row) + complete = checked == EXPECTED_FIXED_FUTURES + return { + "schema_version": 1, + "experiment": "independent_c4_h7_d2_three_source_checkpoint_audit", + "production_experiment": EXPERIMENT, + "scope": { + "parent_checkpoint_only": True, + "fixed_hidden_futures": True, + "zero_debt_past_restored": False, + "global_counterexamples_claimed": False, + }, + "bridge_reconstruction": { + "tq_terminals": bridge.terminal_count, + "labeled_candidates": bridge.labelled_count, + "canonical_parents": bridge.parent_count, + "canonical_edges": bridge.canonical_edge_count, + "sibling_edges": len(bridge.edges), + }, + "universe": { + "selected_edges": len(EXPECTED_EDGE_ROWS), + "decorations": len(decorations), + "labeled_fixed_futures": sum(item.weight for item in decorations), + }, + "run": { + "universe_complete": complete, + "fixed_futures_checked": checked, + "local_yes": local_yes, + "local_no": local_no, + "winning_paths_replayed": replayed, + }, + "status": audit_status(complete, local_no), + "result_rows_fnv1a64": f"{hash_value:016x}", + "first_local_yes": first_yes, + "first_local_no": first_no, + "per_edge": edge_rows, + "claim_boundary": ( + "A local NO is only a nonzero-debt parent-checkpoint residual; " + "no zero-debt past or balanced initial-layout NO is asserted." + ), + } + + +def load_report(path: Path) -> dict[str, object]: + value = json.loads(path.read_text(encoding="utf-8")) + require(isinstance(value, dict), "production report root is not an object") + return value + + +def compare_report(report: dict[str, object], independent: dict[str, object]) -> None: + require(report.get("experiment") == EXPERIMENT, "production experiment drifted") + for field in ("bridge_reconstruction", "universe", "first_local_yes", "first_local_no"): + require(report.get(field) == independent.get(field), + f"production {field} differs from the independent audit") + independent_run = independent["run"] + production_run = report.get("run") + require(isinstance(independent_run, dict) and isinstance(production_run, dict), + "run section is not an object") + for field in ( + "universe_complete", "fixed_futures_checked", "local_yes", + "local_no", "winning_paths_replayed", + ): + require(production_run.get(field) == independent_run.get(field), + f"production run.{field} differs") + require(report.get("status") == independent.get("status"), + "production status differs from the conservative independent status") + ledgers = report.get("ledgers") + require(isinstance(ledgers, dict), "production ledgers section is missing") + require(ledgers.get("result_rows_fnv1a64") == independent.get("result_rows_fnv1a64"), + "production fixed-future ledger hash differs") + actual_edges = report.get("per_edge") + expected_edges = independent.get("per_edge") + require(isinstance(actual_edges, list) and isinstance(expected_edges, list) + and len(actual_edges) == len(expected_edges), "per-edge rows drifted") + for actual, expected in zip(actual_edges, expected_edges): + require(isinstance(actual, dict) and isinstance(expected, dict), + "per-edge row is not an object") + for field in ( + "bridge_edge", "decorations", "fixed_futures_expected", + "fixed_futures_checked", "local_yes", "local_no", + "safe_mask_distribution", + ): + require(actual.get(field) == expected.get(field), + f"edge {expected.get('bridge_edge')} field {field} differs") + scope = report.get("scope") + claims = report.get("claims") + require(scope == { + "parent_checkpoint_only": True, + "fixed_hidden_futures": True, + "zero_debt_past_restored": False, + "full_h7_theorem": False, + }, "production scope overclaims coverage") + require(isinstance(claims, dict) + and claims.get("zero_debt_initial_family_eliminated") is False + and claims.get("universal_c4_h7_solvability") is False, + "production claims turn a checkpoint result into a global theorem") + + +def production_paths(report_path: Path) -> tuple[Path, Path]: + report = load_report(report_path) + ledgers = report.get("ledgers") + require(isinstance(ledgers, dict), "report does not name its ledgers") + tsv = ledgers.get("fixed_future_results") + local_no = ledgers.get("local_no") + require(isinstance(tsv, str) and isinstance(local_no, str), + "report ledger names are invalid") + return report_path.parent / tsv, report_path.parent / local_no + + +def run_program(program: Path, limit: int) -> tuple[dict[str, object], dict[str, object]]: + with tempfile.TemporaryDirectory(prefix="c4-h7-d2-three-source-") as directory: + output = Path(directory) + subprocess.run( + [str(program), "--limit", str(limit), "--output-dir", str(output)], + check=True, + ) + report_path = output / "report.json" + report = load_report(report_path) + tsv, local_no = production_paths(report_path) + rows = ProductionRows(tsv, local_no) + independent = audit(limit, rows) + compare_report(report, independent) + return report, independent + + +def parse_args() -> argparse.Namespace: + parser = argparse.ArgumentParser(description=__doc__) + source = parser.add_mutually_exclusive_group() + source.add_argument("--program", type=Path, + help="production executable for a bounded row differential") + source.add_argument("--report", type=Path, + help="existing production report and ledgers to compare") + parser.add_argument("--limit", type=int, + help="fixed futures to inspect; required with --program") + parser.add_argument("--json", type=Path, help="write the independent report") + parser.add_argument("--local-no-ledger", type=Path, + help="write explicitly local-only independent NO rows") + return parser.parse_args() + + +def main() -> int: + args = parse_args() + production: dict[str, object] | None = None + if args.program is not None: + require(args.limit is not None and args.limit > 0, + "--program requires a positive --limit") + production, independent = run_program(args.program, args.limit) + elif args.report is not None: + production = load_report(args.report) + run_section = production.get("run") + require(isinstance(run_section, dict), "production run section is missing") + target = run_section.get("fixed_futures_checked") + require(isinstance(target, int) and not isinstance(target, bool) and target > 0, + "production checked count is invalid") + tsv, local_no = production_paths(args.report) + independent = audit( + target, + ProductionRows(tsv, local_no), + args.local_no_ledger, + ) + compare_report(production, independent) + else: + require(args.limit is not None and args.limit > 0, + "standalone audit requires an explicit positive --limit") + independent = audit(args.limit, independent_local_no=args.local_no_ledger) + + encoded = json.dumps(independent, indent=2, sort_keys=True) + "\n" + if args.json is not None: + args.json.parent.mkdir(parents=True, exist_ok=True) + args.json.write_text(encoded, encoding="utf-8") + elif production is None: + print(encoded, end="") + run_section = independent["run"] + print( + "independent three-source checkpoint audit: " + f"checked={run_section['fixed_futures_checked']}/" + f"{independent['universe']['labeled_fixed_futures']} " + f"local_yes={run_section['local_yes']} local_no={run_section['local_no']} " + f"status={independent['status']}" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) From e2104c8581a19eca7bb2c10adad772b718f248a5 Mon Sep 17 00:00:00 2001 From: lieoric <129092606+lieoric@users.noreply.github.com> Date: Tue, 11 Aug 2026 07:38:31 +1000 Subject: [PATCH 3/6] Audit anchor pair switch saturation --- .github/workflows/c4-h7-global-bypass.yml | 12 +- docs/c4-h7-anchor-pair-graph.md | 399 ++++++++++++ tests/check_c4_h7_anchor_pair_graph.py | 740 ++++++++++++++++++++++ 3 files changed, 1149 insertions(+), 2 deletions(-) create mode 100644 docs/c4-h7-anchor-pair-graph.md create mode 100644 tests/check_c4_h7_anchor_pair_graph.py diff --git a/.github/workflows/c4-h7-global-bypass.yml b/.github/workflows/c4-h7-global-bypass.yml index 26d2767..3bda5eb 100644 --- a/.github/workflows/c4-h7-global-bypass.yml +++ b/.github/workflows/c4-h7-global-bypass.yml @@ -28,6 +28,7 @@ jobs: tests/check_c4_h7_critical_pair_bypass.py tests/check_c4_h7_rainbow_lift.py tests/check_c4_h7_anchor_pair_potential.py + tests/check_c4_h7_anchor_pair_graph.py - name: Build the certified first-exhaustion census producer run: | cmake -S . -B build \ @@ -60,14 +61,21 @@ jobs: python tests/check_c4_h7_anchor_pair_potential.py \ --report out/anchor/report.json 2>&1 \ | tee out/anchor/potential-audit.json + - name: Check anchor-pair switching and the height-seven saturation cut + run: | + mkdir -p out/anchor-graph + set -o pipefail + python tests/check_c4_h7_anchor_pair_graph.py 2>&1 \ + | tee out/anchor-graph/audit.log - name: Record the exact claim boundary run: | cat >> "$GITHUB_STEP_SUMMARY" <<'EOF' These checks certify three mathematical reductions: the exact critical-pair disable formula plus the past/future bypass, the two-anchor vector potential and first-sweep inequalities, and the - rainbow-transversal/token-error formula. They deliberately do not - claim universal c4/k2/h7 solvability. + rainbow-transversal/token-error formula. It also checks the clean + two-switch return saturation cut. They deliberately do not claim + universal c4/k2/h7 solvability. EOF - name: Hash the complete audit bundle if: always() diff --git a/docs/c4-h7-anchor-pair-graph.md b/docs/c4-h7-anchor-pair-graph.md new file mode 100644 index 0000000..5bd7a14 --- /dev/null +++ b/docs/c4-h7-anchor-pair-graph.md @@ -0,0 +1,399 @@ +# The charged anchor-pair graph at `c=4, h=7, k=2` + +## Scope and claim boundary + +At a zero-exhaustion border checkpoint with exactly two positive debts, the +other two colors form an **anchor pair**. There are six such pairs. This +note organizes them as the octahedral graph `J(4,2)` and proves two facts. + +1. A color which enters the anchor pair must receive a new exposed run. + Therefore the six-vertex graph becomes acyclic after it is lifted by the + four-color exposure vector. +2. In the clean two-switch rotor realized by the committed four-lock + example, a return to the original anchor pair which is also a `D2` + terminal saturates one anchor color at height seven. + +The unweighted six-vertex graph is **not** acyclic. The height-seven +four-lock layout has a legal projected two-cycle, and the cycle ends with +seven, not eight, exposed items of one color. Thus neither + +- "an anchor-pair cycle is impossible at height seven", nor +- "one projected cycle already charges an eighth item" + +is true. The correct statement is that a later entry of a color already at +exposure seven would require an eighth item. This is a well-foundedness and +saturation lemma, not a proof of universal height-seven solvability. In +particular, it does not prove that every unresolved `D2` admits the clean +switch used in Section 4. + +## 1. Exact anchor checkpoints + +For a color `c`, write + +\[ + d_c=F_c-G_c, +\] + +where `F_c` is exposed inventory and `G_c` is the sum of active host caps +currently topped by `c`. Before the first exhaustion, + +\[ + \sum_c d_c=0, + \qquad |\operatorname{Pos}(d)|\le2. \tag{1} +\] + +A source of top color `x` and cap `s` is legal exactly when + +\[ + |\operatorname{Pos}(d+s e_x)|\le2. \tag{2} +\] + +A live border event + +\[ + x_s\longrightarrow y_R, + \qquad x\ne y,quad s0` and `d_c(T)<=0`. Exhausting +events never decrease a debt coordinate, and in (3) the only way to +decrease `d_c` is for `c` to be the destination of a live event. At least +one event + +\[ + u_s\longrightarrow c_R, + \qquad R>s, +\] + +must therefore occur between `S` and `T`. It newly exposes the positive +length `R-s` run of `c`, so `F_c` increases by at least one. Exposure never +decreases later. This proves (6). \(\square\) + +For a sequence of exact checkpoints `S_0,...,S_m`, put `A_i=A(S_i)` and + +\[ + N_c=\#\{i:c\in A_{i+1}\setminus A_i\}. \tag{7} +\] + +Summing (6) over the disjoint time segments gives the vector inequality + +\[ + F_c(S_m)-F_c(S_0)\ge N_c. \tag{8} +\] + +Consequently + +\[ + \sum_{i=0}^{m-1}|A_{i+1}\setminus A_i| + \le \sum_c (h-F_c(S_0)). \tag{9} +\] + +The left side is the octahedral path length, counting a jump to the opposite +pair with cost two. The residual-inventory potential + +\[ + \Phi(F)=\sum_c(h-F_c) \tag{10} +\] + +decreases on every nonconstant pair transition. Thus the lifted graph + +\[ + (A,F)\longrightarrow(B,F') \tag{11} +\] + +is acyclic, even though its projection to the six values of `A` need not be. + +For a closed projected walk `A_m=A_0`, entries and exits balance separately +for every color. Every nonconstant closed walk charges at least two colors, +and a fixed cyclic word can be repeated at most + +\[ + \min_{c:N_c>0} + \left\lfloor\frac{h-F_c(S_0)}{N_c}\right\rfloor + \tag{12} +\] + +times along one coherent history. In particular, if `F_c=7` at height +seven, any transition with `c in B\A` would require `F_c>=8` by (6) and is +impossible. + +This last statement is the precise "eighth item" obstruction. Charges +cannot be added across counterfactual branches: all checkpoints in (8) must +belong to the same legal history and the same fixed layout. + +## 3. A projected cycle at height seven + +The committed balanced four-lock layout, with colors `(q,f,g,h)` encoded as +`(0,1,2,3)`, is written bottom to top as + +```text +2221032 +3321023 +3321003 +1111000 +``` + +The legal column sequence + +```text +0,0,1,0,2,1 +``` + +contains the following exact checkpoints. + +| prefix length | debt `(q,f,g,h)` | anchor pair | exposure `(Fq,Ff,Fg,Fh)` | +|---:|---|---|---| +| 2 | `(-2,0,1,1)` | `{q,f}` | `(4,0,1,3)` | +| 4 | `(1,-3,0,2)` | `{f,g}` | `(4,1,2,3)` | +| 6 | `(-2,-3,2,3)` | `{q,f}` | `(7,1,2,3)` | + +Thus the projected graph has the two-cycle + +\[ + \{q,f\}\longrightarrow\{f,g\} + \longrightarrow\{q,f\}. \tag{13} +\] + +The first edge charges the new anchor `g` once. The second charges the new +anchor `q` three times, stronger than the one-item lower bound in (6). The +return is not a lifted cycle because exposure has changed from +`(4,0,1,3)` to `(7,1,2,3)`. Its final checkpoint is a `3+1` `D2` terminal +with three `q_3` tops and one `f_4` top. A second traversal of the same +projected cycle would eventually have to re-enter `q` and expose an eighth +`q`, so that repetition is excluded, but the first terminal traversal is +real. + +The complete layout is nevertheless YES. One winning column sequence is + +```text +0,0,1,0,2,2,0,1,1,1,1,2,2,3 +``` + +Therefore a projected cycle neither implies NO nor can simply be deleted +from the proof. It records a bad scheduling choice in a solvable layout. + +## 4. Clean two-switch return saturation + +The same example belongs to a more rigid normal form. This is the part of +the graph idea that uses height seven sharply. + +Use four distinct colors `(x,b,y,p)`. Start at an exact checkpoint with + +\[ + d=(-A,0,X,Y), + \qquad X,Y\ge1, + \qquad A=X+Y, \tag{14} +\] + +and top multiset + +\[ + x_t,\ x_c,\ p_s,\ p_u. \tag{15} +\] + +The zero in (14) is forced: `b` is an anchor with no current host, hence +`d_b=F_b` is both nonnegative and nonpositive. Balance then gives +`A=X+Y`. + +Consider the four live events + +\[ + \begin{aligned} + p_s&\longrightarrow y_r, & X&\le sA,\\ + p_u&\longrightarrow x_w, & u&\ge t-A,\quad u