diff --git a/research/c5-frozen-centre-gap/README.md b/research/c5-frozen-centre-gap/README.md new file mode 100644 index 0000000000..55579fe291 --- /dev/null +++ b/research/c5-frozen-centre-gap/README.md @@ -0,0 +1,315 @@ +# The characteristic-5 centre on `s + t = 33` freezes a coordinate, and that does not prove the depth-two exclusion + +**Partial obstruction. No new κ.** In the unchanged unsigned dirty connector, +classify the centre of `s + t = kc + 3` at characteristic `c = 5` and six +sources. Every legal centre is a weight-3 mask and freezes a coordinate sum +of 10. The same one-step move that froze 14 at `c = 7` then makes the whole +middle diagonal illegal. That is a human proof of one chain hypothesis. It is +not a human proof that no depth-two word exists. + +The selected conditional κ stays `781451/250000000`. This note does not rerun +a SAT solver, does not touch the DRAT certificate in open PR #6216, and does +not treat a solver UNSAT as a proof. + +## Proved statement + +Let a floor word of length 30 call each of six sources exactly five times. +Write `q_t` for the count vector of the first `t` letters, so `q_0 = 0` and +`q_30 = (5,5,5,5,5,5)`. Letters are `w_0,...,w_29`, with +`q_{t+1} = q_t + e_{w_t}`. For `s = 4,...,16` define + +```text +S(s) = q_s + q_{33-s}. +``` + +Let `A = {0,1,5,6,10}`. Call `S(s)` **legal** when every coordinate lies in +`A`. The chain hypothesis is: + +> **(H)** `S(s)` is legal for every `s = 4,...,16`. + +**Theorem.** No length-30 six-source floor word in characteristic 5 satisfies +(H). Every legal value of `S(16)` is a weight-3 mask with at least one +coordinate equal to 10, that coordinate is immovable by the diagonal step, +and `q_4` would then contain a 5. + +The domain of the centre census below is finite, and the type split itself is +the short arithmetic in the next section. The checker recounts the census; the +emptiness of (H) does not depend on the SAT encoding of PR #6141. + +## Interface, unchanged + +This is the depth-two interface of PR #4231 and PR #4248, as used by PR #6141. +A pair `(s, t)` with `0 ≤ s ≤ t ≤ 29` realizes a binary mask `m` when +`q_s + q_t ≡ m (mod 5)` coordinatewise. Each count is an integer in +`{0,...,5}`, so each coordinate sum lies in `{0,...,10}`. The sums in that +range congruent to 0 or 1 modulo 5 are exactly `A`: + +| residue modulo 5 | attainable sums | +|---|---| +| 0 | 0, 5, 10 | +| 1 | 1, 6 | + +A coordinate in `{1,6}` contributes a mask bit 1. A coordinate in `{0,5,10}` +contributes a mask bit 0. The coordinate sum of `q_s + q_t` is `s + t`, so a +legal pair of mask weight `w` satisfies `s + t ≡ w (mod 5)` (PR #6107). The +endpoint `t = 30` is dropped, because `q_30` is the all-fives vector and is +identified with `q_0` modulo 5. Nothing here adds a connector operation. + +## Centre classification + +The pair on `s + t = 33` nearest the middle is `(16, 17)`. These prefixes +differ by one letter: `q_17 = q_16 + e_w` with `w = w_16`. Write `r = q_16`. +Then `∑ r_j = 16`, every `r_j` lies in `{0,...,5}`, and `r_w ≤ 4`. + +The centre sum is `2r + e_w`. For a coordinate other than `w` the sum is the +even number `2r_j`. The values of `r_j` in `{0,...,5}` give + +| `r_j` | `2r_j` | in `A` | +|---:|---:|---| +| 0 | 0 | yes, mask bit 0 | +| 1 | 2 | no | +| 2 | 4 | no | +| 3 | 6 | yes, mask bit 1 | +| 4 | 8 | no | +| 5 | 10 | yes, mask bit 0 | + +For the centre letter the sum is `2r_w + 1`, and `r_w ≤ 4`: + +| `r_w` | `2r_w + 1` | in `A` | +|---:|---:|---| +| 0 | 1 | yes, mask bit 1 | +| 1 | 3 | no | +| 2 | 5 | yes, mask bit 0 | +| 3 | 7 | no | +| 4 | 9 | no | + +So a legal centre has non-centre coordinates of types `r ∈ {0,3,5}` only, and +the centre letter is type `r_w = 0` or `r_w = 2`. Let `n_0, n_3, n_5` count +the five non-centre coordinates. Then `n_0 + n_3 + n_5 = 5`. + +**Type `r_w = 0`.** The centre contributes mask bit 1 and count 0. Weight 3 +is not required for this case split: the count equation alone is +`3 n_3 + 5 n_5 = 16`. The nonnegative possibilities with `n_5 ≤ 3` are + +| `n_5` | remainder | solution | +|---:|---:|---| +| 0 | 16 | not divisible by 3 | +| 1 | 11 | not divisible by 3 | +| 2 | 6 | `n_3 = 2`, so `n_0 = 1` | +| 3 | 1 | not divisible by 3 | + +The only solution has mask weight `n_3 + 1 = 3` and two coordinates equal to +10. Each of those is a pair of fives on a source other than `w`. + +**Type `r_w = 2`.** The centre contributes count 2 and mask bit 0. The count +equation is `2 + 3 n_3 + 5 n_5 = 16`, so `3 n_3 + 5 n_5 = 14`. + +| `n_5` | remainder | solution | +|---:|---:|---| +| 0 | 14 | not divisible by 3 | +| 1 | 9 | `n_3 = 3`, so `n_0 = 1` | +| 2 | 4 | not divisible by 3 | + +`n_5 ≥ 3` gives at least 15. The only solution has mask weight `n_3 = 3` and +one coordinate equal to 10, again a pair of fives off `w`. + +These two rows are the whole legal centre. In particular there is no legal +centre of weight 0, 1, 2, 4, 5 or 6. Both legal types freeze at least one +coordinate at 10. + +The same arithmetic counts the realizations. Choose the centre coordinate in +6 ways. + +- Type `r_w = 0`: the other five coordinates are two 3s, two 5s and one 0. + `6 · C(5,2) · C(3,2) = 180`. +- Type `r_w = 2`: three 3s, one 5 and one 0. + `6 · C(5,3) · C(2,1) = 120`. + +That is 300 centres and `2·180 + 120 = 480` coordinates equal to 10. The +checker enumerates every vector in `{0,...,5}^6` of sum 16 and every legal +centre letter, and it finds the same two types with these counts. That +enumeration is an exhaustive finite census of a finite domain. It is a check +of the table above, not a solver verdict. + +## The frozen step, and why (H) is empty + +On this diagonal the prefixes obey + +```text +S(s) = S(s-1) + e_{w_{s-1}} - e_{w_{33-s}}. +``` + +Indeed `q_s = q_{s-1} + e_{w_{s-1}}` and +`q_{34-s} = q_{33-s} + e_{w_{33-s}}`, so + +```text +S(s-1) = q_{s-1} + q_{34-s} = S(s) - e_{w_{s-1}} + e_{w_{33-s}}. +``` + +For each step from `s = 16` down to `s = 5`, both letters lie in +`w_4,...,w_28`. If the two letters agree, `S` does not change. If they +differ, one coordinate increases by 1 and another decreases by 1. + +Inside `A`, the only `+1` moves are `0 → 1` and `5 → 6`. The only `-1` moves +are `1 → 0` and `6 → 5`. The value 10 meets neither list: `9` and `11` are +outside `A`. Therefore, whenever `S(s)` and `S(s-1)` are both legal and +`S(s)` has a coordinate 10, that same coordinate of `S(s-1)` is 10. + +Assume (H). The classification gives a source `j` with `S(16)_j = 10`. +Walking down to `s = 4` keeps coordinate `j` equal to 10. The only way to +write 10 as a sum of two integers in `{0,...,5}` is `5 + 5`, so `q_4[j] = 5`. +The coordinates of `q_4` sum to 4, so none of them is 5. + +This contradiction is the theorem. One index `s ∈ {4,...,16}` whose vector is +illegal stops the walk. The argument uses every index on this diagonal and no +pair with a different sum. + +## Scope of the obstruction + +The theorem is exactly the emptiness of (H). A depth-two word is a floor word +such that every nonzero mask in `{0,1}^6` is realized by some pair +`0 ≤ s ≤ t ≤ 29`. PR #6141 reports that no such word exists at `c = 5`, +including the relaxation to the 16 masks of weights 2 and 6, as output of +CaDiCaL and Glucose on one encoding. Open PR #6216 supplies a DRAT/LRAT +certificate of that same encoding. Those are solver artifacts. This note is +not a certificate, and a certificate is not this note. + +(H) does not follow from depth two. Two independent reasons: + +1. **Weights 2 and 6 never meet this diagonal.** A legal vector has coordinate + sum `w + 5λ`. If the sum is 33, then `w ≡ 3 (mod 5)`. The only Hamming + weight in `0..6` congruent to 3 is 3. Every pair with `s + t = 33`, + centre or not, is disjoint from the 16 masks certified by PR #6216. + Freezing a coordinate of `S(16)` does not mention those masks. + +2. **A weight-3 mask need not sit on `s + t = 33`.** The pairs + `0 ≤ s ≤ t ≤ 29` number `465`. Those with `s + t ≡ 3 (mod 5)` are the 93 + pairs on + + ```text + 3, 8, 13, 18, 23, 28, 33, 38, 43, 48, 53, 58 + ``` + + with raw slot counts + + ```text + 2, 5, 7, 10, 12, 15, 13, 11, 8, 6, 3, 1. + ``` + + Thirteen of the 93 lie on `s + t = 33`, namely `(s, 33-s)` for + `s = 4,...,16`. The other eighty are outside the walk. The witness below + realizes a weight-3 mask at sum 13 while `S(16)` is illegal, so a single + weight-3 realization does not force (H). + +The missing implication, and the whole remaining obligation of this method, is: + +> **(I)** every six-source depth-two floor word in characteristic 5 satisfies (H). + +Together with the theorem, (I) would be a human proof of the exclusion. This +package does not prove (I). No inequality here moves a weight-2 mask, a +weight-6 mask, or a pair with `s + t ≠ 33` onto the frozen coordinate. + +Nick Petalas's handoff already records a different, weaker counting +obstruction to the *restricted* model in which weight-3 masks may use only +`s + t ∈ {3, 33}`. That count is rechecked here and left at its original +strength. The raw pairs of sum 3 are `(0,3)` and `(1,2)`. The second is never +legal: the first letter `a` satisfies `q_2[a] ≥ 1`, so the sum on `a` is at +least 2, while a legal vector of total sum 3 can use only the values `{0,1}`. +Thus that restricted model has at most `1 + 13 = 14` slots and `C(6,3) = 20` +masks. Fourteen slots cannot cover twenty masks. That pigeonhole is not (H), +and it is not the depth-two exclusion: the other residue-3 sums remain +available. The frozen step does not close them. + +## Witness that (H) is stricter than one off-diagonal mask + +The length-30 word + +```text +000001231234512345123451234545 +``` + +calls each source five times. Its prefixes `q_5 = (5,0,0,0,0,0)` and +`q_8 = (5,1,1,1,0,0)` sum to `(10,1,1,1,0,0)`, a weight-3 mask on sources +1, 2 and 3, at `s + t = 13`. The centre is + +```text +q_16 = (5,3,3,3,1,1), q_17 = (5,3,3,3,2,1), +S(16) = (10,6,6,6,3,2). +``` + +The coordinates 3 and 2 lie outside `A`, so `S(16)` is illegal and (H) does +not apply. Across all 465 pairs this word realizes 8 nonzero masks: three of +weight 2, two of weight 3, one of weight 4 and two of weight 1. It realizes +no weight-6 mask. It is a floor word with an off-diagonal weight-3 pair. It +is not a depth-two word, and it is not a counterexample to PR #6141. + +## What was not rerun + +No SAT solver, no DRAT/LRAT check, no replay of PR #6216, and no search for a +depth-two word. The characteristic-6 centre is a different arithmetic: `c + 1` +is odd, so the doubled non-centre sum cannot hit `c + 1`. That classification +is not done here. The off-diagonal replacement question at `c = 7` is not +done here. The `c = 7` chain on `s + t = 45` is not rerun. + +No supplier, consumer, or selected frontier changes. The live selected record +at the base commit is κ `= 781451/250000000 = 0.003125804`. The priority note +on this same commit still quotes the older selected figure from PR #5599; +this package follows the selected record. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -I -W error -B research/c5-frozen-centre-gap/verify.py +python3.12 -I -O -W error -B research/c5-frozen-centre-gap/verify.py +python3.12 -B scripts/research_package.py --package research/c5-frozen-centre-gap --check-only +``` + +The marker is + +```text +PASS_C5_FROZEN_CENTRE_GAP centres=300 type_r0=180 type_r2=120 frozen_coordinates=480 moves=+[0, 5]/-[1, 6] residue3_pairs=93 middle_slots=13 early_realizable_slots=1 witness_masks=8 chain_H=empty controls=7 +``` + +The seven controls are the near-miss centre `(3,3,3,3,3,1)`, the absence of a +5 in every length-4 count, the weight identity on all `5^6` allowed tuples, +the pair census, the exhaustive failure of `(1,2)`, the positive `(0,3)` +pattern `(1,1,1,0,0,0)`, and the witness above. No Lean, Docker, or historical +suite was run. + +## Open next questions + +1. Does every six-source depth-two floor word in characteristic 5 satisfy (H)? + *Why:* the emptiness of (H) is proved for every floor word, so this + implication is a human proof of the exclusion. *First step:* derive + `S(16) ∈ A^6` from the sixteen masks of weights 2 and 6, or show that those + masks do not determine the sum-33 diagonal. *Blocked by:* the weight + identity places weights 2 and 6 on sums congruent to 2 and 1 modulo 5. + Sum 33 is congruent to 3. No transport lemma is proved here. +2. Can the adjacent centre on one other sum `σ ≡ 3 (mod 5)`, `σ ≠ 33`, freeze + a coordinate that meets a positive share of the twenty weight-3 masks? + *Why:* the witness realizes a weight-3 mask at sum 13, which the sum-33 + walk never sees. *First step:* classify the single adjacent pair on `σ = 13` + or on `σ = 28`, at characteristic 5 only. *Blocked by:* adjacency + `q_t = q_s + e_w` with `|t - s| = 1` forces the sum `2s + 1`, and that sum + is 33 only for `s = 16`. A different sum has a different count total. + +## Credit + +The depth-two interface is Nick Petalas's (PR #4231, PR #4248), with the Ross +Richardson PR #934 / PR #943 lineage. PR #6107 supplies the weight identity. +JosieElliston's PR #6141 is the solver exclusion at characteristics 5 and 6 +and leaves characteristic 7 open; its README states that no human proof is +given. queelius's open PR #6216 is a DRAT certificate of the characteristic-5 +encoding, a separate artifact, and it is not replayed or replaced here. +Nick Petalas's handoff of 2026-11-03 +([discussion comment 19384981](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19384981)) +records the diagonal move, the slot counts 14, 17, 20 and 23, and the c=7 +centre shape. The c=7 chain proof is the fork draft +[PR #156](https://github.com/unpaidmoon/integer-mult-bounds/pull/156) +and discussion comment 19493159; this note answers only the characteristic-5 +half of that draft's second open question. zxv's PR #6057 and JosieElliston's +PR #6061 supply words for every `c ≥ 8`, which are outside this obstruction. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. diff --git a/research/c5-frozen-centre-gap/SOURCES.json b/research/c5-frozen-centre-gap/SOURCES.json new file mode 100644 index 0000000000..594089b9c7 --- /dev/null +++ b/research/c5-frozen-centre-gap/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/c5-frozen-centre-gap/TASK.json b/research/c5-frozen-centre-gap/TASK.json new file mode 100644 index 0000000000..8a8e9bb6d8 --- /dev/null +++ b/research/c5-frozen-centre-gap/TASK.json @@ -0,0 +1,68 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Characteristic 5 only, six sources, unchanged unsigned dirty connector. Classify the centre of s+t=33 and decide whether the frozen-coordinate step yields a human proof that no length-30 floor word has depth two. The proved statement is the emptiness of the chain hypothesis that S(s)=q_s+q_{33-s} is legal for every s=4..16. The depth-two exclusion stays a solver verdict.", + "scope_change_reason": "The catalogue card asks for one new connector operation. This package keeps the alphabet fixed and answers the characteristic-5 half of open question 2 in unpaidmoon fork draft PR 156, which restates Nick Petalas's 2026-11-03 handoff (discussion comment 19384981). The missing step named there is the centre classification of s+t=kc+3 at c=5, not a new operation. Characteristic 6, the c=7 off-diagonal replacement, and the open DRAT certificate in PR 6216 are other questions.", + "bottleneck_link": "Side result on the recursive-interface schedule. It does not change a supplier, a consumer, or kappa. The centre classification removes one proposed human route from the characteristic-5 exclusion to a proved chain obstruction, and it leaves the transport implication unproved.", + "budget_minutes": 60, + "stop_rule": "Stop when the c=5 centre is classified and either the chain hypothesis is proved empty with the missing implication to the depth-two exclusion written down, or a legal centre with no frozen coordinate appears.", + "outcome": "partial", + "evidence": "Human type split: the only legal centres of q_16 are type r_w=0 (n0,n3,n5)=(1,2,2) and type r_w=2 (1,3,1). Both have a coordinate 10. The diagonal step cannot move 10 inside {0,1,5,6,10}, so hypothesis (H) forces a 5 in q_4. Exhaustive census of every sum-16 vector in {0,...,5}^6 agrees: 180 + 120 = 300 centres, all weight 3, 480 frozen coordinates. The 465-pair census gives 13 middle slots and 93 residue-3 pairs. The witness word 000001231234512345123451234545 realizes a weight-3 mask at s+t=13, has an illegal centre, and realizes 8 nonzero masks. No SAT run.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance: the centre classification, the chain argument, the witness, the checker, and the package text.", + "open_questions": [ + { + "question": "Does every six-source depth-two floor word in characteristic 5 satisfy the chain hypothesis (H) on s+t=33?", + "why_it_matters": "Emptiness of (H) is proved for every floor word, so this implication is a human proof of the depth-two exclusion.", + "first_step": "Derive S(16) in {0,1,5,6,10}^6 from the sixteen masks of weights 2 and 6, or show that those masks do not determine the sum-33 diagonal.", + "blocked_by": "The weight identity places weights 2 and 6 on sums congruent to 2 and 1 modulo 5. Sum 33 is congruent to 3. No transport lemma is proved here." + }, + { + "question": "Can the adjacent centre on one other sum sigma congruent to 3 modulo 5, sigma not 33, freeze a coordinate that meets a positive share of the twenty weight-3 masks?", + "why_it_matters": "The witness realizes a weight-3 mask at sum 13, which the sum-33 walk never sees.", + "first_step": "Classify the single adjacent pair on sigma=13 or on sigma=28, at characteristic 5 only.", + "blocked_by": "Adjacency q_t = q_s + e_w with |t-s|=1 forces the sum 2s+1, and that sum is 33 only for s=16. A different sum has a different count total." + } + ] +} diff --git a/research/c5-frozen-centre-gap/VERIFY.json b/research/c5-frozen-centre-gap/VERIFY.json new file mode 100644 index 0000000000..74dd20c89b --- /dev/null +++ b/research/c5-frozen-centre-gap/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exhaustive centre census at c=5: every q_16 in {0,...,5}^6 summing to 16, and every legal centre letter. Expect 300 weight-3 centres, 180 of type r=0 and 120 of type r=2, with 480 coordinates equal to 10. Move table keeps 10 fixed. Pair census of all 465 pairs 0<=s<=t<=29. Controls: near-miss centre, no length-4 prefix contains a 5, weight identity on every allowed 6-tuple, (1,2) never legal, (0,3) pattern (1,1,1,0,0,0) is weight 3, and one floor-word witness with an off-diagonal weight-3 mask, an illegal centre, and 8 nonzero masks." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same census under optimized Python. Failures are explicit exceptions, not assertions." + } + ] +} diff --git a/research/c5-frozen-centre-gap/verify.py b/research/c5-frozen-centre-gap/verify.py new file mode 100644 index 0000000000..164a154bb1 --- /dev/null +++ b/research/c5-frozen-centre-gap/verify.py @@ -0,0 +1,243 @@ +#!/usr/bin/env python3 +"""Finite census for the characteristic-5 centre on s + t = 33. + +The human argument is in README.md. This program exhausts three finite +domains and checks the witness word. It does not search for a depth-two +word and it does not call a SAT solver. +""" + +import itertools +import math + +K = 6 +C = 5 +LENGTH = K * C +CENTRE_S = 3 * C + 1 # 16; partner is 17, and 16 + 17 = 33 +SIGMA = K * C + 3 # 33 +ALLOWED = (0, 1, C, C + 1, 2 * C) +MASK_BIT = {0: 0, 1: 1, C: 0, C + 1: 1, 2 * C: 0} +WITNESS = (0, 0, 0, 0, 0, 1, 2, 3, 1, 2, 3, 4, 5, 1, 2, 3, 4, 5, + 1, 2, 3, 4, 5, 1, 2, 3, 4, 5, 4, 5) + + +def fail(msg): + raise SystemExit('FAIL: ' + msg) + + +def mask_weight(sum_vec): + """Return the mask weight, or None when a coordinate lies outside ALLOWED.""" + bits = 0 + for value in sum_vec: + bit = MASK_BIT.get(value) + if bit is None: + return None + bits += bit + return bits + + +def prefixes(word): + counts = [0] * K + out = [tuple(counts)] + for letter in word: + counts[letter] += 1 + out.append(tuple(counts)) + return out + + +def main(): + if CENTRE_S != 16 or SIGMA != 33 or ALLOWED != (0, 1, 5, 6, 10): + fail('pinned characteristic-5 constants changed') + if len(WITNESS) != LENGTH: + fail('witness length is not 30') + + # Local types are the integer r in 0..5 whose doubled sum lands in ALLOWED. + non_centre = [r for r in range(C + 1) if 2 * r in MASK_BIT] + centre_types = [r for r in range(C) if 2 * r + 1 in MASK_BIT] + if non_centre != [0, 3, 5] or centre_types != [0, 2]: + fail(f'local types changed: non-centre {non_centre}, centre {centre_types}') + + type_r0 = 6 * math.comb(5, 2) * math.comb(3, 2) + type_r2 = 6 * math.comb(5, 3) * math.comb(2, 1) + if type_r0 != 180 or type_r2 != 120: + fail(f'multinomial prediction changed: {type_r0}, {type_r2}') + + found_r0 = 0 + found_r2 = 0 + frozen = 0 + weights = {} + for counts in itertools.product(range(C + 1), repeat=K): + if sum(counts) != CENTRE_S: + continue + for centre in range(K): + if counts[centre] >= C: + continue + summed = tuple(2 * counts[j] + (1 if j == centre else 0) for j in range(K)) + weight = mask_weight(summed) + if weight is None: + continue + weights[weight] = weights.get(weight, 0) + 1 + n10 = 0 + for j, value in enumerate(summed): + if value != 10: + continue + n10 += 1 + frozen += 1 + if counts[j] != C or j == centre: + fail(f'10 is not a pair of fives off the centre letter: {counts} {centre}') + if counts[centre] == 0 and summed[centre] == 1 and n10 == 2 and weight == 3: + others = sorted(counts[j] for j in range(K) if j != centre) + if others != [0, 3, 3, 5, 5]: + fail(f'type r=0 shape changed: {counts}') + found_r0 += 1 + elif counts[centre] == 2 and summed[centre] == 5 and n10 == 1 and weight == 3: + others = sorted(counts[j] for j in range(K) if j != centre) + if others != [0, 3, 3, 3, 5]: + fail(f'type r=2 shape changed: {counts}') + found_r2 += 1 + else: + fail( + f'centre outside the two types: q={counts} centre={centre} ' + f'sum={summed} weight={weight} tens={n10}' + ) + + if weights != {3: type_r0 + type_r2}: + fail(f'legal centre weights are not exactly weight 3: {weights}') + if found_r0 != type_r0 or found_r2 != type_r2 or frozen != 2 * type_r0 + type_r2: + fail( + f'census/multinomial mismatch: found {found_r0}, {found_r2}, frozen {frozen}' + ) + + increments = [v for v in ALLOWED if v + 1 in MASK_BIT] + decrements = [v for v in ALLOWED if v - 1 in MASK_BIT] + if increments != [0, 5] or decrements != [1, 6]: + fail(f'move table changed: +{increments} -{decrements}') + if 10 in increments or 10 in decrements: + fail('10 is movable inside the allowed set') + + controls = 0 + + # A sum of 16 can still fail the allowed set. Five 3s and a 1 is one example. + near = (3, 3, 3, 3, 3, 1) + if sum(near) != CENTRE_S: + fail('near-miss no longer sums to 16') + near_sum = tuple(2 * near[j] + (1 if j == 5 else 0) for j in range(K)) + if mask_weight(near_sum) is not None: + fail('near-miss centre was accepted') + controls += 1 + + # Every length-4 count in {0,...,5}^6 is too small to contain a 5. + for prefix in itertools.product(range(C + 1), repeat=K): + if sum(prefix) == 4 and max(prefix) >= C: + fail('length-4 prefix contains a 5') + controls += 1 + + # Every allowed 6-tuple has coordinate sum congruent to its mask weight. + # Sum 33 therefore admits only weight 3, never weight 2 or 6. + for values in itertools.product(ALLOWED, repeat=K): + weight = mask_weight(values) + if sum(values) % C != weight % C: + fail(f'weight identity failed on {values}') + if 33 % C != 3: + fail('33 is not residue 3') + for weight in (0, 1, 2, 4, 5, 6): + if weight % C == 3: + fail('another weight in 0..6 is congruent to 3') + controls += 1 + + # Complete pair census: every 0 <= s <= t <= 29. + slot_counts = {} + pair_total = 0 + for s in range(LENGTH): + for t in range(s, LENGTH): + pair_total += 1 + slot_counts[s + t] = slot_counts.get(s + t, 0) + 1 + if pair_total != 465 or slot_counts[33] != 13 or slot_counts[3] != 2: + fail(f'pair census changed: total {pair_total}, 33={slot_counts.get(33)}, 3={slot_counts.get(3)}') + residue3 = sorted(sigma for sigma in slot_counts if sigma % C == 3) + expected_residue = [3, 8, 13, 18, 23, 28, 33, 38, 43, 48, 53, 58] + expected_counts = { + 3: 2, 8: 5, 13: 7, 18: 10, 23: 12, 28: 15, + 33: 13, 38: 11, 43: 8, 48: 6, 53: 3, 58: 1, + } + if residue3 != expected_residue: + fail(f'residue-3 sums changed: {residue3}') + for sigma, count in expected_counts.items(): + if slot_counts[sigma] != count: + fail(f'slot count at {sigma} is {slot_counts[sigma]}, expected {count}') + if sum(expected_counts.values()) != 93: + fail('residue-3 total is not 93') + middle = [s for s in range(4, 17) if s + (33 - s) == 33 and 33 - s <= 29] + if middle != list(range(4, 17)): + fail(f'middle indices changed: {middle}') + controls += 1 + + # (1, 2) never lands in the allowed set: the first letter is at least 2. + legal_12 = 0 + for first, second in itertools.product(range(K), repeat=2): + q1 = [0] * K + q1[first] = 1 + q2 = q1[:] + q2[second] += 1 + summed = [q1[j] + q2[j] for j in range(K)] + if mask_weight(summed) is not None: + legal_12 += 1 + if summed[first] < 2: + fail('first letter of (1, 2) dropped below 2') + if legal_12 != 0: + fail(f'(1, 2) realized a mask {legal_12} times') + controls += 1 + early = [1, 1, 1, 0, 0, 0] + if mask_weight(early) != 3: + fail('(0, 3) with three distinct letters was rejected') + controls += 1 + + # Witness: a floor word with one off-diagonal weight-3 mask and an illegal centre. + # It realizes 8 nonzero masks and is not a depth-two word. + counts = [0] * K + for letter in WITNESS: + if not 0 <= letter < K: + fail('witness letter out of range') + counts[letter] += 1 + if counts != [C] * K: + fail(f'witness is not a floor word: {counts}') + pref = prefixes(WITNESS) + pair_58 = tuple(pref[5][j] + pref[8][j] for j in range(K)) + if pref[5] != (5, 0, 0, 0, 0, 0) or pref[8] != (5, 1, 1, 1, 0, 0): + fail(f'witness prefixes changed: q5={pref[5]} q8={pref[8]}') + if pair_58 != (10, 1, 1, 1, 0, 0) or mask_weight(pair_58) != 3 or 5 + 8 != 13: + fail(f'witness off-diagonal pair changed: {pair_58}') + centre_sum = tuple(pref[16][j] + pref[17][j] for j in range(K)) + if pref[16] != (5, 3, 3, 3, 1, 1) or pref[17] != (5, 3, 3, 3, 2, 1): + fail(f'witness centre prefixes changed: {pref[16]} {pref[17]}') + if centre_sum != (10, 6, 6, 6, 3, 2) or mask_weight(centre_sum) is not None: + fail(f'witness centre became legal: {centre_sum}') + realized = set() + for s in range(LENGTH): + for t in range(s, LENGTH): + summed = tuple(pref[s][j] + pref[t][j] for j in range(K)) + weight = mask_weight(summed) + if weight is None: + continue + mask = tuple(MASK_BIT[value] for value in summed) + if any(mask): + realized.add(mask) + by_weight = {} + for mask in realized: + by_weight[sum(mask)] = by_weight.get(sum(mask), 0) + 1 + if len(realized) != 8 or by_weight.get(2) != 3 or by_weight.get(3) != 2 or by_weight.get(6, 0) != 0: + fail(f'witness mask census changed: {len(realized)} {by_weight}') + if len(realized) == (1 << K) - 1: + fail('witness is depth two') + controls += 1 + + print( + 'PASS_C5_FROZEN_CENTRE_GAP ' + f'centres={found_r0 + found_r2} type_r0={found_r0} type_r2={found_r2} ' + f'frozen_coordinates={frozen} moves=+{increments}/-{decrements} ' + f'residue3_pairs=93 middle_slots=13 early_realizable_slots=1 ' + f'witness_masks=8 chain_H=empty controls={controls}' + ) + + +if __name__ == '__main__': + main()