diff --git a/research/f7-l22-split-domain/README.md b/research/f7-l22-split-domain/README.md new file mode 100644 index 0000000000..949fcf03f5 --- /dev/null +++ b/research/f7-l22-split-domain/README.md @@ -0,0 +1,244 @@ +# The complete length-22 parity-split domain at seven labels + +**Arithmetic reduction only. No seven-label word is enumerated, no length-22 +split is excluded, and `f(7)` is untouched.** This package derives, from +scratch and with a separately written implementation, the complete set of +Hamming-weight parity splits a restored universal length-22 word over seven +labels could possibly have. It is the first half of the open question recorded +in [PR #2973](../f7-weight-parity-census-correction/README.md) ("derive and +audit its complete split domain before a bounded feasibility probe"). + +Within PR #943's abstract singleton prefix-walk model the derived conditions +leave **11 split representatives at length 22**; importing the standing +17-point set-level exclusions of PR #2773 and PR #2870 removes exactly two of +them and leaves **9**. Nothing further is excluded by the counting or identity +conditions. A length-22 exclusion is therefore still open, and the number of +distinct configurations a future census must cover is now known exactly. + +Base main `20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority revision 6. +No frozen package, pinned source, production engine or selected result is +modified. + +**Overlap note.** PR #3699 independently recomputes the same `01021323` +fixture and classifies which linear functionals make the old substitution +falsely prune. That is a different deliverable: it answers *which groupings +are affected* at small `n`, while this package answers *what the admissible +split domain is* at `n = 7, L = 22`, which PR #3699 does not address. The +shared fixture arithmetic agrees exactly in both packages. + +## The derivation, and what is proved here + +For a word `w` of even length `L` over `n` labels, put `q_0 = 0` and +`q_i = q_(i-1) XOR (1 << w_i)`; restoration is `q_L = 0` with every label used +a positive even number of times. Universality is `P + P = F2^n` for the +**set** of distinct prefix states `P`. Because `wt(q_i) = i (mod 2)`, the +distinct even-weight states `E` and odd-weight states `O` have `s,t` bounded by +`L/2`, and `|P| = s + t`. Writing `Q = 2^(n-1)`, the four conditions are all +necessary, not sufficient: + +| Condition | Statement | Where it comes from | +|---|---|---| +| Time bound | `s <= L/2`, `t <= L/2` | `L/2+1` even-time positions with `q_0 = q_L` forced to coincide; `L/2` odd-time positions | +| Odd budget | `s*t >= Q` | all `Q` odd masks need an `E x O` representation | +| Even budget | `B0 = C(s,2)+C(t,2)-(Q-1) >= 0` | all `Q-1` nonzero even masks need a same-class pair | +| Pair identity | `B0 + a*b >= need = ceil((s*t-Q)/2)` | `sum_y C(r_y,2) = 2 sum_x A_x B_x` and `C(r,2) >= r-1`; expanding on the shared support bounds `sum_x A_x B_x <= |S| + a + b + a*b` with `|S| = B0 - a - b` | + +Rotation by one label translates `P` and swaps `E, O`, so existence at `(s,t)` +is equivalent to existence at `(t,s)`; the domain below lists `s >= t` only. + +`verify.py` recomputes all four from their definitions. It does not import a +census engine, a predecessor package, or any recorded receipt. + +## The length-22 domain + +Enumerating `1 <= t <= s <= 11` and applying the four conditions gives: + +| Split | `\|P\|` | Revisits forced | `B0` | `need` | Odd budget `s*t` | +|---|---:|---:|---:|---:|---:| +| `(11,11)` | 22 | 0 | 47 | 29 | 121 | +| `(11,10)` | 21 | 1 | 37 | 23 | 110 | +| `(11,9)` | 20 | 2 | 28 | 18 | 99 | +| `(10,10)` | 20 | 2 | 27 | 18 | 100 | +| `(11,8)` | 19 | 3 | 20 | 12 | 88 | +| `(10,9)` | 19 | 3 | 18 | 13 | 90 | +| `(11,7)` | 18 | 4 | 13 | 7 | 77 | +| `(10,8)` | 18 | 4 | 10 | 8 | 80 | +| `(9,9)` | 18 | 4 | 9 | 9 | 81 | +| `(11,6)` | 17 | 5 | 7 | 1 | 66 | +| `(10,7)` | 17 | 5 | 3 | 3 | 70 | + +**Excluded, with the responsible condition named.** The time bound removes +`(13,5)` and `(12,6)`, which are counting-feasible at `|P| = 18` but cannot +occur in a 22-step walk because `s <= 11`. The pair identity removes `(9,8)`, +whose `B0 = 1` cannot reach `need = 4`. That leaves the 11 rows above. + +**Importing the standing 17-point result.** PR #2773 and PR #2870 exclude all +six counting-feasible 17-point splits set-level. Independently, the four +conditions above already reduce `|P| = 17` to exactly `(10,7)` and `(11,6)`: the +identity removes `(9,8)` and `(8,9)` there, and `|P| <= 16` fails the odd budget +for every split. Those two remaining 17-point splits are exactly the ones the +imported result excludes, so the length-22 domain after import is the **9 rows +from `(11,11)` down to `(9,9)`**. That import is a standing claim of PR #2773 +and PR #2870 and is **not re-proved here**. + +**Two further consequences, both consequences of the arithmetic.** The same +conditions give a covering-cardinality floor of **17** points at `n = 7`: no +smaller prefix set satisfies the odd and even budgets. And a self-avoidance +restriction is valid at length 22 **only at `(11,11)`**, the single split where +`|P| = L`; at the other ten splits revisits are forced (1 to 5 of them), so a +census that assumes a simple cycle would silently miss most of the domain. + +**What this does not say.** The necessary conditions admit all 11 splits; none +is excluded by them. An admitted split may still have no universal word, as the +fifth-length evidence at `n = 7` shows. This is a reduction of the search space +and a correction of one census precondition, not a length-22 exclusion, not a +`f(7)` bound, and not a claim about any supplier, tariff or kappa. + +## Controls + +`verify.py` is standard library only. Every check below was developed against +a 37-mutant battery; the survivors are reported at the end rather than hidden. + +1. **The calibration fixture, reconstructed independently.** `01021323` at + `n = 4, L = 8` has prefix set `{0,1,2,3,4,6,8,12}`, covers all 16 masks, + has weight split `(4,4)` and bit-0 split `(6,2)`. Its bit-0 collision excess + is 8, above the wrongly substituted balanced budget 5 and at most the correct + actual-size budget 9. The old word-level prune is unsound on this fixture + even inside the simple balanced class, and the bit-0 grouping is not itself + invalid. This agrees element for element with + `check_math.py`'s `simple_n4_counterexample` block. +2. **Published small-domain counts *and split histograms*, from my own + enumeration.** All restored words at `(3,6)`, `(3,8)`, `(4,8)` are + enumerated: 90/60/10, 1260/1092/182 and 2520/624/26 + restored/universal/canonical-universal, and the per-split histograms match + `check_math.py` exactly (for `(4,8)`: 48 `(3,4)`, 48 `(4,3)`, 528 `(4,4)`). + Histograms are a strictly stronger control than totals. Five further domains + `(3,4)`, `(4,6)`, `(4,10)`, `(5,10)`, `(5,12)` are enumerated without a + published comparison. +3. **The universality oracle is cross-checked and non-vacuous.** All 256 subsets + of the fixture's prefix set are tested against a separately written per-mask + existence loop; they agree on every subset, and exactly 7 subsets cover. An + always-true `covers` fails this. Note the fixture is *not* minimal — four of + its points can be dropped and the rest still covers — so a naive + single-point-removal control would have been wrong. +4. **The conditions reject, not only admit.** On the 168 non-universal restored + words at `(3,8)` the four conditions reject all 168. Without this the + necessity audit inside the enumerator is one-sided and cannot fire. +5. **The published length-18 and length-20 domains and budgets.** The same code + returns the single split `(9,9)` at length 18 and the five length-20 + representatives `(10,10)`, `(10,9)`, `(10,8)`, `(9,9)`, `(10,7)`, with even + budgets `27,18,10,9,3` and odd excesses `36,26,16,17,6`, matching + [MATH.md](../f7-weight-parity-census-correction/MATH.md). +6. **Condition independence, measured not assumed.** Each condition is removed + in turn over the full enumeration range and the resulting domain compared. + At length 22 the time bound, odd budget and identity are load-bearing and the + **even budget is redundant**: `need >= 0`, so `B0 <= 0` already fails the + identity. It is reported as redundant rather than presented as a fourth + filter. +7. **Identity tightness.** The minimum slack `B0 + a*b - need` over the admitted + splits is 2 at length 22, and the `a*b` term never decides an eligible split + at lengths 18, 20, 22 or 24. Both are asserted, so an off-by-one in `need` + or a weakened `a*b` bound is caught. +8. **The `ceil` in `need` is checked directly**, including odd remainders where + floor and ceiling differ, because no length-22 verdict actually turns on + rounding. +9. **The padding lemma.** Appending `(j,j)` pairs preserves restoration, + containment of the prefix set and coverage, checked on every universal word + at `(3,6)` and `(4,8)`. +10. **Input guards reject**, verified by calling the function with an odd length + and with out-of-range dimensions. + +### Mutants that did not discriminate + +Two mutants survive and are **not defects**: + +- Replacing `== universe` by `>= universe` inside `covers`. The pair-sum set is + always a subset of `F2^n` by construction, so the two are equivalent. +- Appending `(j,j,j,j)` instead of `(j,j)` in the padding check. That is + exactly two pad steps, which is the lemma under test. + +One real limitation was found this way: the necessity audit in +`enumerate_restored` cannot fire on correct code, so deleting it changed +nothing. That is control 4, now fixed. + +## Reproduce + +Python 3.12 or newer, standard library only, from the repository root: + +```sh +python3 -I -B research/f7-l22-split-domain/verify.py +python3 -I -B research/f7-l22-split-domain/verify.py --emit +``` + +Expected marker: + +``` +PASS_F7_L22_SPLIT_DOMAIN length22_self_contained=11 after_17pt_import=9 f7_untouched +``` + +Observed on macOS arm64, CPython 3.15.0: about 32 s, dominated by the +`(5,12)` enumeration of 6,237,000 restored words. Nearly all of that time is +in domain 8, which is a non-vacuity control; the length-22 arithmetic itself is +microseconds. No temporary files, no subprocesses, no network, no compiler. + +`scripts/research_package.py --package research/f7-l22-split-domain` runs the +same command through the registered launcher with its bytecode-isolation and +timeout policy. + +## Open next questions + +1. **Does a restored universal length-22 seven-label word exist?** The domain + is now exactly the 9 imported splits above, so this is a census over a known + finite domain rather than an open one. `first_step`: run the corrected + revisit-aware engine at `(11,11)` alone, where self-avoidance is valid and + no revisit handling is needed, as the cheapest single case. + `blocked_by`: the `(11,11)` node count is not estimated here. `blocked_by` is + also a resource budget and a named decision: excluding length 22 would settle + `f(7) = 24`, so the search needs an explicit budget and a stop rule before it + starts. PR #2973's session stop rule was "no L22 census". +2. **Can the revisit requirement be priced rather than enumerated?** At the ten + non-`(11,11)` splits, `L - |P|` revisits are forced. A revisit forces a + contiguous subword with every label appearing an even number of times. + `first_step`: derive which subword lengths can realize the forced revisit + counts 1 to 5 at each split, which is a bounded combinatorial question with + no search. `blocked_by`: nothing structural. +3. **Do the 18-point splits open any length-22 route?** `(11,7)`, `(10,8)` and + `(9,9)` are the only 18-point splits in the length-22 domain, and + [PR #2911](../community-efficient1900-audit/originals/2911/research/f7-18point-cover-question-seed6d34356c/README.md) + leaves all four of its 18-point splits undecided. `first_step`: intersect + PR #2911's remainder rows with this package's per-split budgets. + `blocked_by`: `(12,6)` is not in the length-22 domain at all, so only three of + its four splits are reachable here; the rest stays a set-level question. + +## Scope, credit and verification limits + +This package changes no supplier, tariff, kappa, certificate, frozen input or +selected frontier. The selected result `certificates/selected-result.json` is +untouched, and `scripts/research_baseline.py` still reports +`PASS_RESEARCH_BASELINE_BINDINGS_ONLY` with the same values. + +Credit Ross Richardson for the PR #943 prefix-walk model; Aaron Wang for the +PR #2542 word model and the Gray construction, and for the PR #2773/#2870 +17-point set-level exclusions imported here as standing claims; Nicholas Stone +for PR #2691 and the corrected weight-parity census in +`research/f7-weight-parity-census-correction`, including the `01021323` +calibration and the length-18/length-20 domains this package independently +recomputes; Douglas Colkitt for the selected source bindings and review. +Existing source notices and licenses remain unchanged. This contribution adds +the independent derivation, the length-22 domain and its verifier. + +Nick Petalas' repository workflow is followed here; this automated research +donation session wrote the code and the prose. Separate internal source +inspection and self-review are **not** independent human or proof-assistant +review. No formal-kernel proof, no full seven-label replay, no all-size transfer +and no hosted CI run are claimed. + +Three obligations are not discharged. The 17-point exclusions are imported, not +re-proved, so the 9-split figure is conditional on PR #2773 and PR #2870 holding. +No test here can show that an admitted split is realizable; the conditions are +necessary only, so the length-22 domain is an upper bound on what a census must +search, not a candidate list of existing words. And the registered launcher +(`scripts/research_package.py`) was **not** run here: it gates on Python 3.12, +which is not installed on this host, so only `--check-only` (metadata and pins) +was executed locally. The commands above were run directly under CPython 3.15.0; +CI remains the first 3.12 run. \ No newline at end of file diff --git a/research/f7-l22-split-domain/RESULT.json b/research/f7-l22-split-domain/RESULT.json new file mode 100644 index 0000000000..752456d73f --- /dev/null +++ b/research/f7-l22-split-domain/RESULT.json @@ -0,0 +1,769 @@ +{ + "calibration_fixture": { + "actual_bit0_budget": 9, + "actual_bit0_budget_admits": true, + "bit0_split": [ + 6, + 2 + ], + "old_prune_rejects": true, + "prefix_states": [ + 0, + 1, + 2, + 3, + 4, + 6, + 8, + 12 + ], + "substituted_balanced_budget": 5, + "weight_split": [ + 4, + 4 + ], + "within_even_excess": 8, + "word": "01021323" + }, + "claims": { + "imported": "the 17-point set-level exclusion is a standing claim of PR #2773 and PR #2870 and is not re-proved here", + "length_22_no_exclusion": "no length-22 split is excluded by the derived conditions; this is not a census and not f(7)" + }, + "condition_independence_n7": { + "18": { + "domain_size": 1, + "load_bearing": [ + "passes_identity", + "passes_time_bound" + ], + "redundant": [ + "passes_even_budget", + "passes_odd_budget" + ] + }, + "20": { + "domain_size": 5, + "load_bearing": [ + "passes_identity", + "passes_time_bound" + ], + "redundant": [ + "passes_even_budget", + "passes_odd_budget" + ] + }, + "22": { + "domain_size": 11, + "load_bearing": [ + "passes_identity", + "passes_odd_budget", + "passes_time_bound" + ], + "redundant": [ + "passes_even_budget" + ] + } + }, + "conditions_not_vacuous": { + "length": 8, + "n": 3, + "non_universal_words": 168, + "rejected_by_conditions": 168 + }, + "covering_cardinality_floor_n7": 17, + "covering_cardinality_floor_splits": [ + [ + 10, + 7 + ], + [ + 11, + 6 + ] + ], + "excluded_at_length_22": { + "imported_17_point_set_level": [ + [ + 11, + 6 + ], + [ + 10, + 7 + ] + ], + "pair_identity": [ + [ + 9, + 8 + ] + ], + "time_bound_s_t_le_11": [ + [ + 13, + 5 + ], + [ + 12, + 6 + ] + ] + }, + "identity_need_formula": { + "cases": 8, + "odd_remainder_cases": [ + [ + 7, + 11, + 7, + 13, + 6, + 7 + ], + [ + 7, + 9, + 9, + 17, + 8, + 9 + ], + [ + 7, + 11, + 11, + 57, + 28, + 29 + ], + [ + 3, + 1, + 5, + 1, + 0, + 1 + ], + [ + 4, + 3, + 3, + 1, + 0, + 1 + ] + ] + }, + "identity_tightness_n7": { + "18": { + "ab_term_decides_at": [], + "admitted": 1, + "excluded_by_identity": [ + [ + 9, + 8 + ] + ], + "min_even_budget_slack": 9, + "min_identity_slack": 20 + }, + "20": { + "ab_term_decides_at": [], + "admitted": 5, + "excluded_by_identity": [ + [ + 9, + 8 + ] + ], + "min_even_budget_slack": 3, + "min_identity_slack": 2 + }, + "22": { + "ab_term_decides_at": [], + "admitted": 11, + "excluded_by_identity": [ + [ + 9, + 8 + ] + ], + "min_even_budget_slack": 3, + "min_identity_slack": 2 + }, + "24": { + "ab_term_decides_at": [], + "admitted": 18, + "excluded_by_identity": [ + [ + 9, + 8 + ] + ], + "min_even_budget_slack": 3, + "min_identity_slack": 2 + } + }, + "input_guards": { + "dimension_bounds_rejected": true, + "odd_length_rejected": true + }, + "length_20_published_budgets": { + "(10,10)": [ + 27, + 36 + ], + "(10,7)": [ + 3, + 6 + ], + "(10,8)": [ + 10, + 16 + ], + "(10,9)": [ + 18, + 26 + ], + "(9,9)": [ + 9, + 17 + ] + }, + "length_22_after_imported_17_point_exclusion": [ + [ + 11, + 11 + ], + [ + 11, + 10 + ], + [ + 11, + 9 + ], + [ + 10, + 10 + ], + [ + 11, + 8 + ], + [ + 10, + 9 + ], + [ + 11, + 7 + ], + [ + 10, + 8 + ], + [ + 9, + 9 + ] + ], + "length_22_revisits_forced": { + "(10, 10)": 2, + "(10, 7)": 5, + "(10, 8)": 4, + "(10, 9)": 3, + "(11, 10)": 1, + "(11, 11)": 0, + "(11, 6)": 5, + "(11, 7)": 4, + "(11, 8)": 3, + "(11, 9)": 2, + "(9, 9)": 4 + }, + "length_22_self_contained": [ + [ + 11, + 11 + ], + [ + 11, + 10 + ], + [ + 11, + 9 + ], + [ + 10, + 10 + ], + [ + 11, + 8 + ], + [ + 10, + 9 + ], + [ + 11, + 7 + ], + [ + 10, + 8 + ], + [ + 9, + 9 + ], + [ + 11, + 6 + ], + [ + 10, + 7 + ] + ], + "length_22_simple_cycle_admissible": [ + [ + 11, + 11 + ] + ], + "marker": "PASS_F7_L22_SPLIT_DOMAIN", + "model": "PR943 singleton prefix-walk, first-occurrence labels", + "oracle_non_vacuity": { + "independent_reference_agrees": true, + "subsets_accepted": 7, + "subsets_tested": 256 + }, + "padding_lemma": [ + { + "length": 6, + "n": 3, + "pad_steps": 2, + "universal_words_checked": 60 + }, + { + "length": 8, + "n": 4, + "pad_steps": 1, + "universal_words_checked": 624 + } + ], + "small_domain_census": [ + { + "canonical_universal_words": 0, + "distinct_prefix_sizes": [], + "length": 4, + "n": 3, + "restored_words": 0, + "split_histogram": {}, + "universal_splits": [], + "universal_words": 0 + }, + { + "canonical_universal_words": 10, + "distinct_prefix_sizes": [ + 5, + 6 + ], + "length": 6, + "n": 3, + "restored_words": 90, + "split_histogram": { + "2,3": 18, + "3,2": 18, + "3,3": 24 + }, + "universal_splits": [ + [ + 3, + 3 + ], + [ + 3, + 2 + ] + ], + "universal_words": 60 + }, + { + "canonical_universal_words": 182, + "distinct_prefix_sizes": [ + 5, + 6, + 7, + 8 + ], + "length": 8, + "n": 3, + "restored_words": 1260, + "split_histogram": { + "2,3": 252, + "2,4": 12, + "3,2": 252, + "3,3": 408, + "3,4": 72, + "4,2": 12, + "4,3": 72, + "4,4": 12 + }, + "universal_splits": [ + [ + 4, + 4 + ], + [ + 4, + 3 + ], + [ + 4, + 2 + ], + [ + 3, + 3 + ], + [ + 3, + 2 + ] + ], + "universal_words": 1092 + }, + { + "canonical_universal_words": 0, + "distinct_prefix_sizes": [], + "length": 6, + "n": 4, + "restored_words": 0, + "split_histogram": {}, + "universal_splits": [], + "universal_words": 0 + }, + { + "canonical_universal_words": 26, + "distinct_prefix_sizes": [ + 7, + 8 + ], + "length": 8, + "n": 4, + "restored_words": 2520, + "split_histogram": { + "3,4": 48, + "4,3": 48, + "4,4": 528 + }, + "universal_splits": [ + [ + 4, + 4 + ], + [ + 4, + 3 + ] + ], + "universal_words": 624 + }, + { + "canonical_universal_words": 1310, + "distinct_prefix_sizes": [ + 7, + 8, + 9, + 10 + ], + "length": 10, + "n": 4, + "restored_words": 75600, + "split_histogram": { + "3,4": 1440, + "3,5": 720, + "4,3": 1440, + "4,4": 11520, + "4,5": 6480, + "5,3": 720, + "5,4": 6480, + "5,5": 2640 + }, + "universal_splits": [ + [ + 5, + 5 + ], + [ + 5, + 4 + ], + [ + 5, + 3 + ], + [ + 4, + 4 + ], + [ + 4, + 3 + ] + ], + "universal_words": 31440 + }, + { + "canonical_universal_words": 0, + "distinct_prefix_sizes": [], + "length": 10, + "n": 5, + "restored_words": 113400, + "split_histogram": {}, + "universal_splits": [], + "universal_words": 0 + }, + { + "canonical_universal_words": 1116, + "distinct_prefix_sizes": [ + 11, + 12 + ], + "length": 12, + "n": 5, + "restored_words": 6237000, + "split_histogram": { + "5,6": 17280, + "6,5": 17280, + "6,6": 99360 + }, + "universal_splits": [ + [ + 6, + 6 + ], + [ + 6, + 5 + ] + ], + "universal_words": 133920 + } + ], + "split_domains": { + "18": [ + { + "even_budget": 9, + "identity_max_upper": 29, + "identity_need": 9, + "odd_pairs": 81, + "points": 18, + "revisits_forced": 0, + "split": [ + 9, + 9 + ] + } + ], + "20": [ + { + "even_budget": 27, + "identity_max_upper": 209, + "identity_need": 18, + "odd_pairs": 100, + "points": 20, + "revisits_forced": 0, + "split": [ + 10, + 10 + ] + }, + { + "even_budget": 18, + "identity_max_upper": 99, + "identity_need": 13, + "odd_pairs": 90, + "points": 19, + "revisits_forced": 1, + "split": [ + 10, + 9 + ] + }, + { + "even_budget": 10, + "identity_max_upper": 35, + "identity_need": 8, + "odd_pairs": 80, + "points": 18, + "revisits_forced": 2, + "split": [ + 10, + 8 + ] + }, + { + "even_budget": 9, + "identity_max_upper": 29, + "identity_need": 9, + "odd_pairs": 81, + "points": 18, + "revisits_forced": 2, + "split": [ + 9, + 9 + ] + }, + { + "even_budget": 3, + "identity_max_upper": 5, + "identity_need": 3, + "odd_pairs": 70, + "points": 17, + "revisits_forced": 3, + "split": [ + 10, + 7 + ] + } + ], + "22": [ + { + "even_budget": 47, + "identity_max_upper": 599, + "identity_need": 29, + "odd_pairs": 121, + "points": 22, + "revisits_forced": 0, + "split": [ + 11, + 11 + ] + }, + { + "even_budget": 37, + "identity_max_upper": 379, + "identity_need": 23, + "odd_pairs": 110, + "points": 21, + "revisits_forced": 1, + "split": [ + 11, + 10 + ] + }, + { + "even_budget": 28, + "identity_max_upper": 224, + "identity_need": 18, + "odd_pairs": 99, + "points": 20, + "revisits_forced": 2, + "split": [ + 11, + 9 + ] + }, + { + "even_budget": 27, + "identity_max_upper": 209, + "identity_need": 18, + "odd_pairs": 100, + "points": 20, + "revisits_forced": 2, + "split": [ + 10, + 10 + ] + }, + { + "even_budget": 20, + "identity_max_upper": 120, + "identity_need": 12, + "odd_pairs": 88, + "points": 19, + "revisits_forced": 3, + "split": [ + 11, + 8 + ] + }, + { + "even_budget": 18, + "identity_max_upper": 99, + "identity_need": 13, + "odd_pairs": 90, + "points": 19, + "revisits_forced": 3, + "split": [ + 10, + 9 + ] + }, + { + "even_budget": 13, + "identity_max_upper": 55, + "identity_need": 7, + "odd_pairs": 77, + "points": 18, + "revisits_forced": 4, + "split": [ + 11, + 7 + ] + }, + { + "even_budget": 10, + "identity_max_upper": 35, + "identity_need": 8, + "odd_pairs": 80, + "points": 18, + "revisits_forced": 4, + "split": [ + 10, + 8 + ] + }, + { + "even_budget": 9, + "identity_max_upper": 29, + "identity_need": 9, + "odd_pairs": 81, + "points": 18, + "revisits_forced": 4, + "split": [ + 9, + 9 + ] + }, + { + "even_budget": 7, + "identity_max_upper": 19, + "identity_need": 1, + "odd_pairs": 66, + "points": 17, + "revisits_forced": 5, + "split": [ + 11, + 6 + ] + }, + { + "even_budget": 3, + "identity_max_upper": 5, + "identity_need": 3, + "odd_pairs": 70, + "points": 17, + "revisits_forced": 5, + "split": [ + 10, + 7 + ] + } + ] + } +} diff --git a/research/f7-l22-split-domain/SOURCES.json b/research/f7-l22-split-domain/SOURCES.json new file mode 100644 index 0000000000..03bcddd31e --- /dev/null +++ b/research/f7-l22-split-domain/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/f7-weight-parity-census-correction/math/check_math.py", + "usage": "provenance", + "git_blob": "2ac1478a2115a82ad50bb7a56f4d33177ff2bea1", + "sha256": "a6b011f4c06017200bf855c122c510c23d08f4b74b269f27a0e0f92aae99d220" + }, + { + "path": "research/f7-weight-parity-census-correction/MATH.md", + "usage": "provenance", + "git_blob": "e0207d8ebd903dc584862a2d6d500b59f3134490", + "sha256": "13f1234de6b7bd9f5afbe9a8892fc1d7f47eae0eddf098d19331a561c750e06a" + }, + { + "path": "research/f7-weight-parity-census-correction/README.md", + "usage": "provenance", + "git_blob": "0221748ce35d4a2dc6ee5ce61be210eb34a2ea83", + "sha256": "9bc7867ccfa97a682e4683052647d4bf8f191da5a219271f87d3e0a10de1446a" + }, + { + "path": "research/community-efficient1900-audit/originals/2911/research/f7-18point-cover-question-seed6d34356c/README.md", + "usage": "provenance", + "git_blob": "be908c56657d173a548bba54430a8ff45f616701", + "sha256": "7538093643ab71152057156e34ff898ffa31275340745c021d9c5f448a236f43" + } + ] +} \ No newline at end of file diff --git a/research/f7-l22-split-domain/TASK.json b/research/f7-l22-split-domain/TASK.json new file mode 100644 index 0000000000..3fc176d597 --- /dev/null +++ b/research/f7-l22-split-domain/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "census-pruning-audit", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "census-pruning-audit", + "question": "Does the reported word-census parity-pruning error invalidate a specific exclusion we still rely on, and what bounded repair is justified?", + "starting_points": [ + "research/f7-weight-parity-census-correction/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct the tiny counterexample and trace one affected exclusion to its exact pruning code.", + "Compare corrected and unpruned enumeration on a small exhaustive domain, then audit the changed pruning implication." + ], + "acceptance_gate": "Pin the old and proposed corrected engines, distinguish a disproved pruning rule from a disproved final bound, and state exactly which downstream exclusions need revalidation. #2973 is an author-checked source archive; neither its new f(7) claim nor all old conclusions are automatically accepted or rejected.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2973 error description and MATH.md; manually reconstruct the prefix states of 01021323 before running any large census.", + "scope": "Source-binding orientation only; no full enumeration or mathematical validation." + }, + "first_experiment": "Reconstruct the eight prefix states of 01021323 and compare bit-0 versus Hamming-weight parity budgets independently. Trace the reported false prune to one pinned predecessor (#2542, #2634 or #2691), then test a small exhaustive domain. Stop after a source-impact handoff or corrected-prune proof; a full seven-label replay needs a separate resource budget and a named research decision it can change.", + "bottleneck_link": "An unsound exclusion can wrongly close a mechanism; correcting its dependency boundary is more useful than extending the same census.", + "allowed_variations": [ + "One predecessor pruning rule, one independently exhaustive small domain, or one downstream dependency audit." + ], + "scope_change_triggers": [ + "Launching a larger census before validating the prune and explaining which active decision it changes.", + "Treating a small-domain counterexample to the old rule as a counterexample to every reported seven-label bound." + ], + "overlap_terms": [ + "2973", + "2542", + "2634", + "2691", + "weight parity", + "bit-0", + "01021323", + "census pruning" + ] + }, + "scope_status": "refined", + "actual_scope": "Independently re-derive the four necessary conditions of PR #2973's corrected word census from their definitions, check them against the published small-domain counts and the 01021323 calibration, then derive the complete parity-split domain for n=7 at lengths 18, 20 and 22. No seven-label enumeration and no length-22 exclusion.", + "scope_change_reason": "The card's first_experiment asks to trace the false prune to one pinned predecessor and test a small exhaustive domain. Tracing the predecessor engines was already recorded in the #1317 discussion thread, so repeating it would not add coverage. The card's own acceptance gate asks which downstream exclusions need revalidation, and PR #2973's first open question asks for the complete length-22 split domain before any bounded probe. That domain derivation is the missing bounded deliverable, and it is what this package supplies.", + "bottleneck_link": "A word-census exclusion can only be correct if its prune is a necessary condition. This package independently re-derives those conditions, confirms the 01021323 unsoundness of the old word-level budget, and computes the exact finite domain any length-22 census must cover. It changes no supplier, tariff, kappa or selected result.", + "budget_minutes": 60, + "stop_rule": "Stop after the independent derivation, the small-domain controls, the three length domains and the reproducible package. No length-22 census, no new census engine, no seven-label enumeration, no frontier change.", + "outcome": "completed", + "evidence": "python3 -I -B research/f7-l22-split-domain/verify.py prints PASS_F7_L22_SPLIT_DOMAIN length22_self_contained=11 after_17pt_import=9 f7_untouched in about 28 s on macOS arm64 / CPython 3.15.0. It reconstructs the 01021323 fixture (bit-0 excess 8 against the substituted budget 5, within the correct budget 9), enumerates every restored word at eight small (n,L) domains reproducing the independently published 90/60/10, 1260/1092/182 and 2520/624/26 counts and their exact split histograms, cross-checks the coverage oracle against an independent per-mask reference over all 256 subsets of the fixture set (7 cover), confirms the four conditions reject all 168 non-universal words at (3,8), recomputes the published length-18 (single split (9,9)) and length-20 (five representatives, budgets 27/18/10/9/3 and odd excesses 36/26/16/17/6) domains and budgets, measures that the even budget is redundant while the time bound, odd budget and identity are load-bearing, checks the padding lemma and the input guards, and derives the length-22 domain: 11 representatives, dropping (13,5) and (12,6) by the time bound and (9,8) by the pair identity, then 9 after importing the standing 17-point set-level exclusions of PR #2773 and PR #2870. It also derives a covering-cardinality floor of 17 points at n=7, shows self-avoidance is valid at length 22 only at (11,11), and records minimum identity slack 2. A 37-mutant battery was run; the two survivors are documented equivalent mutants, and one vacuous control it exposed was replaced. The registered launcher was not run locally because it gates on Python 3.12, which this host lacks; only --check-only was executed here.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does a restored universal length-22 seven-label word exist?", + "why_it_matters": "Excluding length 22 after the corrected length-20 exclusion would settle f(7) = 24, so this is the deciding bounded question in the PR #943 word model. The domain is now exactly 9 splits rather than unknown, which converts an open-ended search into a finite one.", + "first_step": "Run the corrected revisit-aware engine at (11,11) alone, where |P| = L = 22 makes self-avoidance valid and no revisit handling is required.", + "blocked_by": "No node-count estimate or resource budget here. PR #2973's session stop rule was explicitly no L22 census, so this needs its own budget and a named research decision before any search starts." + }, + { + "question": "Which contiguous zero-XOR subword lengths can realize the forced revisit counts at each length-22 split?", + "why_it_matters": "At the ten splits other than (11,11), L - |P| revisits are forced, between 1 and 5. A revisit is a contiguous subword in which every label appears an even number of times. Pricing those instead of enumerating them could shrink the census, and it is pure combinatorics with no search.", + "first_step": "Enumerate the possible subword shapes for one label even count of 2 and 4 at n=7 and check which admit a self-avoiding insertion into an existing prefix walk.", + "blocked_by": "Nothing structural; the interaction with the collision budgets is untested here." + }, + { + "question": "Do PR #2911's undecided 18-point set-level splits intersect the reachable length-22 splits?", + "why_it_matters": "PR #2911 leaves all four 18-point splits undecided and calls the 18-point question the deciding set-level object for the L = 22 route. If one is excluded, one third of the length-22 domain disappears without any census.", + "first_step": "Intersect PR #2911's exact remainder rows for (11,7), (10,8) and (9,9) with the per-split budgets and revisit counts computed here.", + "blocked_by": "(12,6) is outside the length-22 domain entirely, so only three of PR #2911's four splits are reachable at length 22; the fourth remains a set-level question with no word-level consequence." + } + ] +} diff --git a/research/f7-l22-split-domain/VERIFY.json b/research/f7-l22-split-domain/VERIFY.json new file mode 100644 index 0000000000..a48db9cd3d --- /dev/null +++ b/research/f7-l22-split-domain/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/f7-weight-parity-census-correction/math/check_math.py", + "research/f7-weight-parity-census-correction/MATH.md", + "research/f7-weight-parity-census-correction/README.md", + "research/community-efficient1900-audit/originals/2911/research/f7-18point-cover-question-seed6d34356c/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Reconstructs the 01021323 bit-0 versus weight-parity calibration; enumerates every restored word at eight small (n,L) domains and requires the three independently published counts; requires every universal word to satisfy all four derived necessary conditions; recomputes the published length-18 and length-20 domains and budgets; requires the pair identity to be load-bearing; checks the padding lemma; and derives the length-22 domain with named exclusion reasons, the cardinality floor and the (11,11)-only simple-cycle condition. Failure controls are the negated published counts, budgets and domain sizes." + } + ] +} \ No newline at end of file diff --git a/research/f7-l22-split-domain/verify.py b/research/f7-l22-split-domain/verify.py new file mode 100644 index 0000000000..f68198ffe1 --- /dev/null +++ b/research/f7-l22-split-domain/verify.py @@ -0,0 +1,630 @@ +#!/usr/bin/env python3 +"""Derive and audit the complete length-22 parity-split domain at n=7. + +Independent standard-library implementation of the PR943 singleton +prefix-walk model. It recomputes the published length-18 and length-20 +split lists and budget tables from scratch, reconstructs the `01021323` +calibration, and then applies the same necessary conditions at length 22, +which is the first half of the open question recorded in +research/f7-weight-parity-census-correction (PR #2973). + +No census engine, no predecessor package and no external artefact is +imported. Nothing here enumerates seven-label words: the length-22 result +is arithmetic over the derived necessary conditions, so it is a scoped +reduction, not a census and not an exclusion of any word. + +Apache-2.0. +""" +from __future__ import annotations + +import argparse +from itertools import product +import json +import sys + +MAX_N = 12 +MAX_L = 24 +MARKER = "PASS_F7_L22_SPLIT_DOMAIN" + + +def require(condition: bool, message: str) -> None: + if not condition: + raise SystemExit("FAIL: " + message) + + +def popcount(value: int) -> int: + return bin(value).count("1") + + +def half(n: int) -> int: + """Q = 2^(n-1): the number of masks of each Hamming-weight parity.""" + return 1 << (n - 1) + + +def prefix_states(word, n: int): + """q_0 = 0, q_i = q_(i-1) XOR (1 << w_i); the model of PR #943.""" + state = 0 + out = [0] + for label in word: + state ^= 1 << label + out.append(state) + return out + + +def parity_classes(states, n: int): + """Distinct even-weight and odd-weight prefix states, as (E, O).""" + even, odd = set(), set() + for state in states: + (even if popcount(state) % 2 == 0 else odd).add(state) + return even, odd + + +def covers(even: set, odd: set, n: int) -> bool: + """Universality: P + P = F2^n, equivalently every mask is a pair sum.""" + universe = set(range(1 << n)) + if not even or not odd: + return False + pool = sorted(even) + sorted(odd) + return {a ^ b for a in pool for b in pool} == universe + + +def check_oracle_non_vacuity(n: int, seed_points) -> dict: + """The universality oracle must reject as well as accept. + + Without this, an always-true `covers` would silently pass every domain and + every small-domain count. The calibration fixture is not minimal -- four + of its points can be dropped and the rest still covers -- so a + single-point-removal control would be wrong. Instead this enumerates all + 2^8 subsets of the fixture's prefix set, compares `covers` against an + independently written per-mask existence loop, and requires the exact count + of accepting subsets. + """ + reference = set(seed_points) + require(covers(*parity_classes(reference, n), n), + "the full control set must be accepted") + require(not covers(*parity_classes(set(), n), n), + "the empty set must be rejected") + require(not covers(set(), {1}, n) and not covers({1}, set(), n), + "a single class alone must be rejected") + + accepted = 0 + for mask in range(1 << len(reference)): + subset = {point for bit, point in enumerate(sorted(reference)) + if mask >> bit & 1} + by_sums = covers(*parity_classes(subset, n), n) + by_mask = all(any(a ^ b == target for a in subset for b in subset) + for target in range(1 << n)) + require(by_sums == by_mask, + "coverage oracle disagrees with the per-mask reference at " + + repr(sorted(subset))) + accepted += by_sums + require(accepted == 7, + "exactly 7 subsets of the control set may cover, got " + str(accepted)) + return {"subsets_tested": 1 << len(reference), "subsets_accepted": accepted, + "independent_reference_agrees": True} + + +def within_pairs(items): + """Distinct-sum support of the unordered distinct-element pairs of a class.""" + support = set() + for i, a in enumerate(sorted(items)): + for b in sorted(items)[i + 1:]: + support.add(a ^ b) + return support + + +def collision_excess(classes): + """Sum over classes of C(|class|,2) - |distinct pair sums|, per class.""" + total = 0 + for items in classes: + total += len(items) * (len(items) - 1) // 2 - len(within_pairs(items)) + return total + + +def identity_need(s: int, t: int, n: int) -> int: + """ceil((s*t - Q) / 2): the pair-identity lower bound on sum(A_x*B_x).""" + excess = s * t - half(n) + return -((-excess) // 2) if excess > 0 else 0 + + +def even_budget(s: int, t: int, n: int) -> int: + """B0 = C(s,2) + C(t,2) - (Q-1): the even-mask collision excess budget.""" + return s * (s - 1) // 2 + t * (t - 1) // 2 - (half(n) - 1) + + +def split_row(s: int, t: int, n: int, length: int) -> dict: + """Evaluate every derived necessary condition at the split (s, t). + + The identity's upper bound `B0 + a*b` is attained at `a = b = B0/2`, and is + taken to be `B0` itself when `B0 <= 0`, where no feasible `a, b` pair + exists. That makes the identity imply the even budget: `need >= 0`, so + `B0 <= 0` never passes. `check_condition_independence` verifies this over + the full enumeration range instead of assuming it. + """ + q = half(n) + budget = even_budget(s, t, n) + need = identity_need(s, t, n) + best = budget + budget * budget // 4 if budget > 0 else budget + return { + "split": [s, t], + "points": s + t, + "revisits_forced": length - (s + t), + "even_budget": budget, + "identity_need": need, + "identity_max_upper": best, + "odd_pairs": s * t, + "odd_masks_needed": q, + "passes_time_bound": s <= length // 2 and t <= length // 2, + "passes_odd_budget": s * t >= q, + "passes_even_budget": budget >= 0, + "passes_identity": best >= need, + "self_avoiding_forced": s + t == length, + } + + +def admissible_splits(n: int, length: int): + """All splits with s >= t >= 1 that no derived condition excludes. + + The enumeration range is deliberately wider than `L/2` so that the time + bound is exercised as a condition rather than hidden in the loop bounds. + """ + rows = [] + for t in range(1, length): + for s in range(t, length): + row = split_row(s, t, n, length) + keep = (row["passes_time_bound"] and row["passes_odd_budget"] + and row["passes_even_budget"] and row["passes_identity"]) + if keep: + rows.append(row) + rows.sort(key=lambda r: (-r["points"], -r["split"][0])) + return rows + + +def check_condition_independence(n: int, lengths) -> dict: + """Which derived conditions are load-bearing, measured not assumed. + + Each condition is removed in turn and the resulting domain is compared with + the full one, over the whole enumeration range. A condition that changes + nothing here is reported as redundant rather than presented as a filter. + """ + names = ("passes_time_bound", "passes_odd_budget", + "passes_even_budget", "passes_identity") + report = {} + for length in lengths: + rows = [split_row(s, t, n, length) + for t in range(1, length) for s in range(t, length)] + full = [row["split"] for row in rows if all(row[name] for name in names)] + redundant = [] + for drop in names: + kept = [row["split"] for row in rows + if all(row[name] for name in names if name != drop)] + if len(kept) == len(full): + redundant.append(drop) + report[str(length)] = { + "domain_size": len(full), + "load_bearing": sorted(set(names) - set(redundant)), + "redundant": sorted(redundant)} + return report + + +def check_identity_need_formula() -> dict: + """The ceiling in `need = ceil((s*t - Q)/2)` must be the real ceiling. + + No length-22 split is decided by rounding, so a floor-for-ceiling mutant + survives the domain comparison. This checks the arithmetic directly, + including the odd remainders that make floor and ceiling differ. + """ + cases = [(7, 11, 7), (7, 9, 9), (7, 10, 8), (7, 11, 11), (7, 10, 7), + (3, 1, 5), (4, 3, 3), (5, 4, 4)] + odd = [] + for n, s, t in cases: + excess = s * t - half(n) + expected = -((-excess) // 2) if excess > 0 else 0 + require(identity_need(s, t, n) == expected, + "identity_need wrong at n=%d s=%d t=%d" % (n, s, t)) + require(identity_need(s, t, n) >= excess / 2, + "identity_need must be at least the real value") + if excess > 0 and excess % 2: + odd.append([n, s, t, excess, excess // 2, identity_need(s, t, n)]) + require(identity_need(s, t, n) == excess // 2 + 1, + "odd remainder must round up at %d/%d" % (s, t)) + require(odd, "no odd remainder case exercised the ceiling") + return {"cases": len(cases), "odd_remainder_cases": odd} + + +def check_identity_tightness(n: int, lengths) -> dict: + """Measure how hard each admitted split is, and what the a*b term buys. + + Reported rather than assumed: the minimal slack `B0 + a*b - need` over the + admitted splits bounds how far `need` or the ceiling could be perturbed + before the domain changes, and the `ab_decides` list records the splits + where the `a*b` refinement rather than `B0` alone decides the verdict. + """ + report = {} + for length in lengths: + rows = [split_row(s, t, n, length) + for t in range(1, length) for s in range(t, length)] + eligible = [r for r in rows if r["passes_time_bound"] + and r["passes_odd_budget"] and r["passes_even_budget"]] + admitted = [r for r in eligible if r["passes_identity"]] + decisive = [r["split"] for r in eligible + if (r["even_budget"] >= r["identity_need"]) + != (r["identity_max_upper"] >= r["identity_need"])] + report[str(length)] = { + "admitted": len(admitted), + "excluded_by_identity": [r["split"] for r in eligible + if not r["passes_identity"]], + "min_identity_slack": min(r["identity_max_upper"] - r["identity_need"] + for r in admitted), + "min_even_budget_slack": min(r["even_budget"] for r in admitted), + "ab_term_decides_at": decisive} + return report + + +def even_count_vectors(labels: int, length: int): + """Positive even multiplicities summing to `length`.""" + if length < 2 * labels or length % 2: + return + extra = length // 2 - labels + for cuts in product(range(extra + 1), repeat=labels - 1): + point = extra - sum(cuts) + if point < 0: + continue + yield [2 * (1 + c) for c in cuts] + [2 * (1 + point)] + + +def arrangements(counts, labels: int, length: int): + """Every word with the given multiplicity vector, in first-occurrence order.""" + if length == 0: + yield () + return + for label in range(labels): + if counts[label]: + counts[label] -= 1 + for rest in arrangements(counts, labels, length - 1): + yield (label,) + rest + counts[label] += 1 + + +def is_canonical(word) -> bool: + """Restricted growth form: each new label is the next unused one.""" + seen = 0 + for label in word: + if label > seen: + return False + seen = max(seen, label + 1) + return word[0] == 0 + + +def check_calibration_counterexample(n: int, word) -> dict: + """Independent reconstruction of the PR #2973 `01021323` fixture.""" + states = prefix_states(word, n) + distinct = set(states) + even, odd = parity_classes(distinct, n) + size = len(distinct) + weight_split = [len(even), len(odd)] + bit0_even = {s for s in distinct if s & 1 == 0} + bit0_odd = {s for s in distinct if s & 1 == 1} + balanced_budget = even_budget(max(weight_split), min(weight_split), n) + bit0_budget = even_budget(len(bit0_even), len(bit0_odd), n) + excess = collision_excess([bit0_even, bit0_odd]) + require(size == 8 and weight_split == [4, 4], "fixture split changed") + require(sorted(distinct) == [0, 1, 2, 3, 4, 6, 8, 12], "prefix set") + require(covers(even, odd, n), "fixture is not universal") + require(excess == 8, "bit-0 collision excess must be 8, got " + str(excess)) + require(balanced_budget == 5 and excess > balanced_budget, + "the substituted balanced budget must reject the fixture") + require(bit0_budget == 9 and excess <= bit0_budget, + "the actual-size bit-0 budget must admit the fixture") + require(len(bit0_even) == 6 and len(bit0_odd) == 2, "bit-0 split (6,2)") + return { + "word": "".join(str(x) for x in word), + "prefix_states": sorted(set(states)), + "weight_split": weight_split, + "bit0_split": [len(bit0_even), len(bit0_odd)], + "within_even_excess": excess, + "substituted_balanced_budget": balanced_budget, + "actual_bit0_budget": bit0_budget, + "old_prune_rejects": True, + "actual_bit0_budget_admits": True, + } + + +def check_conditions_are_not_vacuous(n: int, length: int) -> dict: + """The conditions must also reject, not only admit. + + The necessity audit inside `enumerate_restored` is one-sided: on correct + code it can never fire, so deleting it changes nothing and it is not a + discriminating check on its own. This is the converse. It enumerates the + non-universal restored words and requires that the four conditions reject a + substantial share of them, so an always-true condition set fails. + """ + names = ("passes_time_bound", "passes_odd_budget", + "passes_even_budget", "passes_identity") + non_universal = rejected = 0 + for counts in even_count_vectors(n, length): + for word in arrangements(list(counts), n, length): + even, odd = parity_classes(set(prefix_states(word, n)), n) + if covers(even, odd, n): + continue + non_universal += 1 + row = split_row(max(len(even), len(odd)), + min(len(even), len(odd)), n, length) + rejected += not all(row[name] for name in names) + require(non_universal > 0, "no non-universal words to test against") + require(rejected >= non_universal // 4, + "the conditions reject too few non-universal words: %d of %d" + % (rejected, non_universal)) + return {"n": n, "length": length, "non_universal_words": non_universal, + "rejected_by_conditions": rejected} + + +def check_input_rejection() -> dict: + """The boundary guards must actually reject, not merely be present.""" + for args, label in (((3, 7), "odd length"), ((MAX_N + 1, 8), "n over bound"), + ((3, MAX_L + 2), "length over bound")): + try: + enumerate_restored(*args) + except SystemExit: + continue + raise SystemExit("FAIL: guard did not reject " + label) + return {"odd_length_rejected": True, "dimension_bounds_rejected": True} + + +def enumerate_restored(n: int, length: int) -> dict: + """Every restored word over n labels, with a universality audit.""" + require(n <= MAX_N and length <= MAX_L, "enumeration domain too large") + require(length % 2 == 0, "a restored word has even length") + restored = universal = canonical = 0 + observed_points, observed_splits = set(), set() + histogram = {} + for counts in even_count_vectors(n, length): + for word in arrangements(list(counts), n, length): + restored += 1 + states = prefix_states(word, n) + distinct = set(states) + even, odd = parity_classes(distinct, n) + require(len(even) <= length // 2 and len(odd) <= length // 2, + "time-parity bound violated at " + str(word)) + require(len(distinct) <= length, "|P| exceeds L at " + str(word)) + if not covers(even, odd, n): + continue + universal += 1 + s, t = len(even), len(odd) + row = split_row(max(s, t), min(s, t), n, length) + for key in ("passes_time_bound", "passes_odd_budget", + "passes_even_budget", "passes_identity"): + require(row[key], "necessary condition rejected a real cover: " + + key + " at " + str(word)) + observed_points.add(len(distinct)) + observed_splits.add((max(s, t), min(s, t))) + key = "%d,%d" % (s, t) + histogram[key] = histogram.get(key, 0) + 1 + if is_canonical(word): + canonical += 1 + return { + "n": n, "length": length, "restored_words": restored, + "universal_words": universal, "canonical_universal_words": canonical, + "distinct_prefix_sizes": sorted(observed_points), + "universal_splits": sorted(observed_splits, reverse=True), + "split_histogram": dict(sorted(histogram.items())), + } + + +def check_padding_lemma(n: int, length: int, steps: int) -> dict: + """Appending (j,j) pairs preserves restoration and prefix coverage.""" + checked = 0 + for counts in even_count_vectors(n, length): + for word in arrangements(list(counts), n, length): + states = prefix_states(word, n) + even, odd = parity_classes(set(states), n) + if not covers(even, odd, n): + continue + padded, position = list(word), 0 + for _ in range(steps): + padded += [position % n, position % n] + position += 1 + new_states = set(prefix_states(padded, n)) + even, odd = parity_classes(new_states, n) + require(new_states >= set(states), "padding must keep the prefix set") + require(covers(even, odd, n), "padding must preserve coverage") + require(prefix_states(padded, n)[-1] == 0, "padding must restore") + checked += 1 + return {"n": n, "length": length, "pad_steps": steps, + "universal_words_checked": checked} + + +def check_published_small_domains(census) -> None: + """Counts and split histograms as independently recorded by + research/f7-weight-parity-census-correction/math/check_math.py.""" + published = { + (3, 6): (90, 60, 10, + {"2,3": 18, "3,2": 18, "3,3": 24}), + (3, 8): (1260, 1092, 182, + {"2,3": 252, "2,4": 12, "3,2": 252, "3,3": 408, + "3,4": 72, "4,2": 12, "4,3": 72, "4,4": 12}), + (4, 8): (2520, 624, 26, + {"3,4": 48, "4,3": 48, "4,4": 528}), + } + for row in census: + key = (row["n"], row["length"]) + if key not in published: + continue + observed = (row["restored_words"], row["universal_words"], + row["canonical_universal_words"], row["split_histogram"]) + require(observed == published[key], + "small-domain mismatch at " + str(key) + ": " + repr(observed)) + + +def check_published_split_domains(splits) -> None: + """The length-18 and length-20 domains and budgets, recomputed.""" + require([[r["split"] for r in splits[18]]] == [[[9, 9]]], + "length-18 domain must be the single split (9,9)") + require([[r["split"] for r in splits[20]]] + == [[[10, 10], [10, 9], [10, 8], [9, 9], [10, 7]]], + "length-20 domain must reproduce the five published representatives") + published_budgets = {"(10,10)": [27, 36], "(10,9)": [18, 26], + "(10,8)": [10, 16], "(9,9)": [9, 17], + "(10,7)": [3, 6]} + for row in splits[20]: + key = "(%d,%d)" % tuple(row["split"]) + require(key in published_budgets, "unpublished length-20 split " + key) + require([row["even_budget"], row["odd_pairs"] - half(7)] + == published_budgets[key], + "length-20 budget mismatch at " + key) + # The identity is what excludes (9,8): admitted without it, excluded with. + weak = [r["split"] for r in + [split_row(s, t, 7, 20) for t in range(1, 20) for s in range(t, 20)] + if r["passes_time_bound"] and r["passes_odd_budget"] + and r["passes_even_budget"]] + require([9, 8] in weak and [9, 8] not in [r["split"] for r in splits[20]], + "the identity must be the condition excluding (9,8) at length 20") + + +def check_cardinality_floor() -> dict: + """The counting conditions set a covering-cardinality floor of 17 at n=7. + + The identity then narrows the 17-point survivors to exactly the two splits + that PR #2773 and PR #2870 exclude set-level. + """ + for size in range(1, 24): + survivors = [tuple(row["split"]) for row in + [split_row(s, size - s, 7, 22) + for s in range((size + 1) // 2, size)] + if row["passes_odd_budget"] and row["passes_even_budget"] + and row["passes_identity"]] + if survivors: + require(size == 17, "the covering-cardinality floor must be 17") + require(sorted(survivors) == [(10, 7), (11, 6)], + "17-point survivors must be exactly (10,7) and (11,6)") + return {"floor": size, "splits": [list(x) for x in survivors]} + raise SystemExit("FAIL: no covering cardinality found below 23") + + +def build_receipt(fixture, oracle, guards, not_vacuous, census, padding, + splits, domain, reporting): + """The reconstructed receipt, as printed by --emit.""" + receipt = { + "marker": MARKER, + "model": "PR943 singleton prefix-walk, first-occurrence labels", + "calibration_fixture": fixture, + "oracle_non_vacuity": oracle, + "input_guards": guards, + "conditions_not_vacuous": not_vacuous, + "small_domain_census": census, + "padding_lemma": padding, + "split_domains": { + str(length): [{"split": r["split"], "points": r["points"], + "revisits_forced": r["revisits_forced"], + "even_budget": r["even_budget"], + "identity_need": r["identity_need"], + "identity_max_upper": r["identity_max_upper"], + "odd_pairs": r["odd_pairs"]} + for r in rows] + for length, rows in splits.items()}, + "length_20_published_budgets": { + "(10,10)": [27, 36], "(10,9)": [18, 26], "(10,8)": [10, 16], + "(9,9)": [9, 17], "(10,7)": [3, 6]}, + "length_22_self_contained": domain["self_contained"], + "length_22_after_imported_17_point_exclusion": domain["after_import"], + "length_22_revisits_forced": {str(tuple(r["split"])): + r["revisits_forced"] for r in splits[22]}, + "covering_cardinality_floor_n7": domain["cardinality"]["floor"], + "covering_cardinality_floor_splits": domain["cardinality"]["splits"], + "length_22_simple_cycle_admissible": domain["simple_only"], + "condition_independence_n7": reporting["independence"], + "identity_tightness_n7": reporting["tightness"], + "identity_need_formula": reporting["need_formula"], + "excluded_at_length_22": { + "time_bound_s_t_le_11": [[13, 5], [12, 6]], + "pair_identity": [[9, 8]], + "imported_17_point_set_level": [[11, 6], [10, 7]]}, + "claims": { + "length_22_no_exclusion": "no length-22 split is excluded by the " + "derived conditions; this is not a census and not f(7)", + "imported": "the 17-point set-level exclusion is a standing claim " + "of PR #2773 and PR #2870 and is not re-proved here"}, + } + return receipt + + +def check_length_22_domain(splits) -> dict: + """The length-22 domain, its named exclusions and its imported reduction.""" + self_contained = [r["split"] for r in splits[22]] + seventeen = {(11, 6), (10, 7)} + after_import = [r["split"] for r in splits[22] + if tuple(r["split"]) not in seventeen] + require(len(self_contained) == 11 and len(after_import) == 9, + "length-22 domain size changed") + require([13, 5] not in self_contained and [12, 6] not in self_contained, + "the time bound must remove (13,5) and (12,6)") + cardinality = check_cardinality_floor() + # Self-avoidance is valid only where the split forces |P| = L. + simple_only = [r["split"] for r in splits[22] if r["self_avoiding_forced"]] + require(simple_only == [[11, 11]], + "only (11,11) may use a simple-cycle restriction at length 22") + return {"self_contained": self_contained, "after_import": after_import, + "cardinality": cardinality, "simple_only": simple_only} + + +def check_identity_reporting() -> dict: + """Condition independence, the ceiling formula, and measured tightness.""" + independence = check_condition_independence(7, (18, 20, 22)) + require(independence["22"]["redundant"] == ["passes_even_budget"], + "at length 22 only the even budget may be redundant") + for name in ("passes_identity", "passes_time_bound", "passes_odd_budget"): + require(name in independence["22"]["load_bearing"], + name + " must be load-bearing at length 22") + need_formula = check_identity_need_formula() + tightness = check_identity_tightness(7, (18, 20, 22, 24)) + for length in ("18", "20", "22", "24"): + require(tightness[length]["excluded_by_identity"] == [[9, 8]], + "the identity must exclude exactly (9,8) at length " + length) + require(tightness[length]["ab_term_decides_at"] == [], + "the a*b term must not decide any eligible split at " + length) + require(tightness["22"]["min_identity_slack"] == 2, + "the tightest admitted length-22 split must have slack 2") + return {"independence": independence, "need_formula": need_formula, + "tightness": tightness} + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", + help="print the reconstructed receipt as JSON") + args = parser.parse_args() + + fixture = check_calibration_counterexample(4, (0, 1, 0, 2, 1, 3, 2, 3)) + oracle = check_oracle_non_vacuity(4, fixture["prefix_states"]) + guards = check_input_rejection() + not_vacuous = check_conditions_are_not_vacuous(3, 8) + + domains = [(3, 4), (3, 6), (3, 8), (4, 6), (4, 8), (4, 10), + (5, 10), (5, 12)] + census = [enumerate_restored(n, length) for n, length in domains] + + check_published_small_domains(census) + + padding = [check_padding_lemma(3, 6, 2), check_padding_lemma(4, 8, 1)] + + splits = {length: admissible_splits(7, length) + for length in (18, 20, 22)} + check_published_split_domains(splits) + + domain = check_length_22_domain(splits) + reporting = check_identity_reporting() + + receipt = build_receipt( + fixture, oracle, guards, not_vacuous, census, padding, splits, + domain, reporting) + + if args.emit: + print(json.dumps(receipt, indent=1, sort_keys=True)) + print("%s length22_self_contained=%d after_17pt_import=%d " + "f7_untouched" % (MARKER, len(domain["self_contained"]), + len(domain["after_import"]))) + return 0 + + +if __name__ == "__main__": + sys.exit(main()) \ No newline at end of file