diff --git a/research/f7-four-stay-pruning/README.md b/research/f7-four-stay-pruning/README.md new file mode 100644 index 0000000000..3521be1e9e --- /dev/null +++ b/research/f7-four-stay-pruning/README.md @@ -0,0 +1,172 @@ +# Sharp high-weight excess at four labels and length ten + +This contribution is produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +**Claim type: scoped combinatorial proof with exact finite corroboration.** +For every simple restored singleton-prefix walk of length ten on `F_2^4`, +each weight-three functional has within-class pair-sum excess at most **11**. +The bound is attained by a universal walk for each such functional. The +all-ones functional has excess exactly **6**. Thus the fixed substituted +budget **13** is sound throughout this domain. + +This proves the `(4,10)` case explicitly left unproved in unpaidmoon's +[PR #4148](https://github.com/CrocSwap/integer-mult-bounds/pull/4148), +Open next question 3. Earlier work measured soundness on this domain. The new +contribution is a structural proof, the sharp cap and its equality condition. +No predecessor executable is imported or replayed. + +## Definitions + +A word `w` of length `L` moves by `q_(i+1)=q_i+e_(w_i)` over `F_2`. +Restoration means `q_L=q_0=0`. Simplicity means the `L` nonclosing prefix +states are distinct. For a nonzero label-basis functional `f`, let `E,O` +be its two classes in the prefix set, of sizes `s,t`. Put + +```text +D(A) = {x+y : x,y in A, x != y} +excess(A) = C(|A|,2) - |D(A)| +X_f = excess(E) + excess(O) +base(4,10) = 2 C(5,2) - (2^3-1) = 13. +``` + +This is the separate-class excess used in #4148. A vector occurring in +both `D(E)` and `D(O)` is counted once in each support. Universality means +the entire prefix set has difference set `F_2^4`. +Every coordinate is active here: ten distinct states cannot fit inside a +proper coordinate subcube, which has at most eight states. + +## Proof + +**Matching balance lemma.** In any simple hypercube cycle of length at least +four, a functional +omitting exactly one coordinate has class sizes satisfying +`max(s,t) <= 2 min(s,t)`. + +Only edges in the omitted coordinate preserve the functional. Those +hypercube edges form a matching, so their endpoints in the cycle are +disjoint. Let `a,b` count preserving edges inside the respective classes, +and let `c` count edges crossing between them. Counting cycle degrees gives + +```text +2s = 2a+c, 2t = 2b+c, s-t = a-b. +2a <= s, 2b <= t. +``` + +If `s>=t`, then `s-t=a-b<=a<=s/2`, hence `s<=2t`. Interchange the +classes for the other case. Simplicity is used when the preserving edges +are treated as a matching on distinct cycle vertices. + +At `L=10`, this gives `s,t>=4`. The unordered split is therefore `(5,5)` +or `(6,4)`. This conclusion uses no universality assumption. + +Translate either functional coset into its kernel `F_2^3`; translation +preserves pair sums. Every subset of this eight-point space having at +least five points realizes every nonzero difference. Otherwise, for a +missed nonzero `v`, it contains at most one point from each of the four +pairs `{x,x+v}`, a contradiction. Every four-point subset realizes at +least three differences, obtained by adding a fixed point to the other +three. + +For split `(5,5)`, both supports have size seven, so +`X_f=2 C(5,2)-14=6`. For split `(6,4)`, their sizes are seven and at least +three, so `X_f<=C(6,2)+C(4,2)-7-3=11`. + +Equality in the latter case holds exactly when the four-point class is +an affine two-dimensional plane. Indeed, translate a point to zero. If +there are only three nonzero differences, the three remaining points +`u,v,z` must obey `u+v=z`, and conversely such a plane has exactly three +nonzero differences. This also proves the equality characterization. + +The all-ones functional flips on every edge. Its split is `(5,5)` and +its excess is exactly six by the same support argument. + +**Sharpness.** The word `0102301023` and functional mask `0111` have split +`(6,4)`, excess eleven and a full sixteen-element difference set. The +verifier checks this literal witness. Permuting coordinates sends its +omitted coordinate to any chosen coordinate and preserves all properties, +so every weight-three functional attains eleven. The verifier also emits +one literal witness for each mask. This completes the proof. + +## Reproduction and evidence + +Use CPython 3.12 and its standard library from the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/f7-four-stay-pruning +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/f7-four-stay-pruning/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/f7-four-stay-pruning/verify.py +``` + +The standalone verifier freshly enumerates all `4^9` labeled prefixes. +Restoration uniquely determines the tenth edge when the ninth endpoint +is a unit vector. Exactly **2,640** simple restored cycles survive, and +all **13,200** high-weight functional cases satisfy the theorem and the +degree/matching identities. No first-occurrence normalization is used. + +A separate set-level calculation uses all `C(16,10)=8,008` ten-point +subsets and all five high-weight functionals. It checks the same envelope +on every split admitted by the matching lemma, using ordered differences +instead of the walk checker's unordered pairs. It also checks the +affine-plane equality characterization. This is corroboration of the +proof's set argument, not another implementation of a predecessor census. + +Nine controls reject a nonsimple word, a nonrestoring word, an out-of-range +label, a Boolean label, three invalid functionals, cap ten, and removal of +the functional-weight restriction. The last control is the universal word +`0102131213` at mask `0001`, whose excess is **21 > 13**. + +The verifier prints a fresh JSON receipt bound to SHA256 of all five +package files. `--output /absolute/external/new.json` creates it exclusively +outside the checkout. `--check-receipt /absolute/external/new.json` +recomputes and compares the full payload. No receipt is hand-written or +stored in the checkout. The verifier and registered checks write no files +by default and need no Git or network access. + +## Scope and credit + +The catalogue's `census-pruning-audit` card changes scope to a new theorem +answering #4148. The selected-source orientation command passed with +`PASS_RESEARCH_BASELINE_BINDINGS_ONLY`. The package changes no engine, +seven-label exclusion, supplier, selected record or kappa. The theorem's +cycle and weight hypotheses are explicit; its proof makes no claim for +other lengths or dimensions. + +Credit unpaidmoon for #4148's open question, double-transversal theorem +and excess convention. Nick Petalas's #3699/#3733 supply the earlier +measured functional classifications. Nicholas Stone's #2973 supplies the +parity correction, James Reed's #3096 the bit-0 boundary work, and Ross +Richardson's #943 the singleton-prefix model. The source documents are +pinned as provenance in `SOURCES.json`; they are not runtime inputs. + +Overlap checks covered live open PR titles and relevant bodies, recent +account submissions, the latest handoff claims and active discussions, +distinctive all-main README terms and merged-title searches. The cached +refresh covered 411 open PRs and 3,925 Discussion records; its local scan +covered 133 of 6,319 tracked notes. The omitted notes, arbitrary diffs and +unpublished work are coverage limits. Direct Git searches covered the +relevant omitted f7 README paths. Search coverage is not a novelty proof. + +The verifier uses bounded Python collections and iterator allocations. +This is a managed-runtime deviation from Power of Ten rule 3. There are +at most ten live walk states, sixteen difference values per set and five +histogram rows; the `4^9` prefix and `8,008` subset domains are streamed. +Receipt files are limited to one MiB. Python runtime allocations are not +instrumented. A future expansion must retain explicit domain and memory +bounds. Functions stay below sixty lines, there is no recursion or dynamic +code execution, and explicit exceptions keep checks active under `-O`. +Registered commands enable warning errors. No separate static type checker +is configured for this standalone standard-library script. + +## Open next questions + +- Does a structural argument settle the `(5,12)` high-weight case in + #4148 Open next question 3? It would extend a proved soundness boundary. + Start by applying the matching balance lemma and analyzing the remaining + `(8,4)` split. The three-dimensional support argument here does not + settle the four-dimensional kernel case. +- Can a pruning engine profitably use the matching balance constraint at + a partial chronological prefix? A stronger sound prune could reduce + future searches. First specify remaining-edge capacities and prove that + every possible completion satisfies the proposed bound. No engine change + or performance measurement is supplied here. diff --git a/research/f7-four-stay-pruning/SOURCES.json b/research/f7-four-stay-pruning/SOURCES.json new file mode 100644 index 0000000000..2add2c7dde --- /dev/null +++ b/research/f7-four-stay-pruning/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/f7-codim-one-substitution-soundness/PROOF.md", + "usage": "provenance", + "git_blob": "0df5ca372839f27f1dc6c3b953c8766fde510ac7", + "sha256": "1f5b5fc5706a428411908db87cb6ff553d98afdbfda7bd95df6d4a4d9d855037" + }, + { + "path": "research/f7-codim-one-substitution-soundness/README.md", + "usage": "provenance", + "git_blob": "4abeb11e029017d6d9815cba0728fc65bfa2a5f2", + "sha256": "634d348ebc54fcf9437dc7844a70d6b56c68eb7b61990fb028f3ea6e0710f50c" + } + ] +} diff --git a/research/f7-four-stay-pruning/TASK.json b/research/f7-four-stay-pruning/TASK.json new file mode 100644 index 0000000000..c6a8abcc3c --- /dev/null +++ b/research/f7-four-stay-pruning/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "census-pruning-audit", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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": "changed", + "actual_scope": "Prove the sharp weight-three and weight-four within-class excess bounds for simple restored length-ten walks on F_2^4, answering PR4148 Open next question 3 at (4,10).", + "scope_change_reason": "The explicit assignment requires an original result rather than auditing a predecessor. This changes the audit card to a new structural theorem beyond the predecessor double-transversal proof.", + "bottleneck_link": "A structural soundness boundary can justify future pruning decisions without relying on measured regularity. This small interface theorem does not improve the multiplication bound.", + "budget_minutes": 60, + "stop_rule": "Stop at the first new proved case and exact finite corroboration; do not extend to (5,12) or run a seven-label census.", + "outcome": "completed", + "evidence": "README proof: preserving-coordinate matching forces splits (5,5) or (6,4); exact class supports give sharp cap 11 versus budget 13. Standalone enumeration, set envelope and rejection controls corroborate it.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the (5,12) high-weight case in PR4148 be proved structurally?", + "why_it_matters": "It would extend the proved soundness boundary beyond the present four-dimensional walk.", + "first_step": "Apply matching balance and analyze the (8,4) split in the four-dimensional functional kernel.", + "blocked_by": "The present three-dimensional support lemma does not settle that split." + }, + { + "question": "Can a sound partial-prefix prune use the preserving-edge matching constraint?", + "why_it_matters": "It may reduce future word searches without the unsound fixed-size substitution.", + "first_step": "Specify remaining-edge capacities and prove a bound valid for every chronological completion.", + "blocked_by": "No partial-prefix completion lemma or engine integration is provided." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134279", + "overlap_coverage": { + "open_prs": 411, + "discussion_records": 3925, + "local_notes": 133, + "head_notes": 6319, + "limits": "Sparse local notes, arbitrary diffs and unpublished work; relevant omitted f7 READMEs searched directly at origin/main." + } +} diff --git a/research/f7-four-stay-pruning/VERIFY.json b/research/f7-four-stay-pruning/VERIFY.json new file mode 100644 index 0000000000..2364c46bbe --- /dev/null +++ b/research/f7-four-stay-pruning/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Fresh labeled cycle enumeration, preserving-edge degree/matching identities, sharp excess witnesses, independent set envelope and nine boundary controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The identical mathematical and boundary checks with Python assertions disabled." + } + ] +} diff --git a/research/f7-four-stay-pruning/verify.py b/research/f7-four-stay-pruning/verify.py new file mode 100644 index 0000000000..0f259c459b --- /dev/null +++ b/research/f7-four-stay-pruning/verify.py @@ -0,0 +1,214 @@ +#!/usr/bin/env python3 +"""Exact corroboration of the length-ten codimension-one excess theorem.""" + +import argparse +import hashlib +import json +from itertools import combinations, product +from pathlib import Path + + +MASKS = (7, 11, 13, 14, 15) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def cycle_states(word): + require(len(word) == 10, "the word must have length ten") + require(all(type(j) is int and 0 <= j < 4 for j in word), "invalid label") + states = [] + q = 0 + for label in word: + require(q not in states, "the cycle must be simple") + states.append(q) + q ^= 1 << label + require(q == 0, "the cycle must restore every coordinate") + return tuple(states) + + +def pair_sums(cell): + return {x ^ y for x, y in combinations(cell, 2)} + + +def statistics(states, mask): + require(type(mask) is int and 1 <= mask < 16, "invalid functional") + require(len(states) == len(set(states)) == 10, "ten distinct states required") + require(all(type(x) is int and 0 <= x < 16 for x in states), "invalid state") + cells = tuple(tuple(x for x in states if (x & mask).bit_count() % 2 == p) + for p in (0, 1)) + supports = tuple(pair_sums(cell) for cell in cells) + slots = sum(len(cell) * (len(cell) - 1) // 2 for cell in cells) + excess = slots - sum(len(support) for support in supports) + return cells, supports, excess + + +def matching_check(states, mask): + """Check the degree identity and matching premise, without assuming balance.""" + colors = tuple((x & mask).bit_count() % 2 for x in states) + internal = [0, 0] + endpoints = set() + for i in range(10): + j = (i + 1) % 10 + if colors[i] == colors[j]: + require(i not in endpoints and j not in endpoints, "not a matching") + endpoints.update((i, j)) + internal[colors[i]] += 1 + s = colors.count(0) + t = 10 - s + require(s - t == internal[0] - internal[1], "degree identity failed") + require(2 * internal[0] <= s and 2 * internal[1] <= t, "matching capacity") + require(max(s, t) <= 2 * min(s, t), "matching balance failed") + + +def exact_walks(): + """At most 4**9 prefixes; restoration uniquely determines the last edge.""" + for prefix in product(range(4), repeat=9): + states = [] + q = 0 + for label in prefix: + if q in states: + break + states.append(q) + q ^= 1 << label + else: + if q not in states and q.bit_count() == 1: + yield prefix + (q.bit_length() - 1,) + + +def walk_corroboration(): + maxima = {mask: -1 for mask in MASKS} + witnesses = {} + histogram = {mask: {} for mask in MASKS} + count = 0 + for word in exact_walks(): + states = cycle_states(word) + count += 1 + for mask in MASKS: + matching_check(states, mask) + cells, supports, excess = statistics(states, mask) + split = tuple(sorted(map(len, cells))) + require(split in ((4, 6), (5, 5)), "unexpected split") + if mask == 15: + require(split == (5, 5) and excess == 6, "parity endpoint") + require(excess <= 11, "sharp cap failed") + key = str(excess) + histogram[mask][key] = histogram[mask].get(key, 0) + 1 + if excess > maxima[mask]: + maxima[mask] = excess + witnesses[mask] = "".join(map(str, word)) + if split == (4, 6): + small = 0 if len(cells[0]) == 4 else 1 + require((excess == 11) == (len(supports[small]) == 3), + "equality characterization failed") + require(count == 2640, "incomplete walk enumeration") + require(maxima == {7: 11, 11: 11, 13: 11, 14: 11, 15: 6}, "maxima failed") + return {"labeled_cycles": count, "functional_checks": count * len(MASKS), + "maxima": {str(mask): maxima[mask] for mask in MASKS}, + "witnesses": {str(mask): witnesses[mask] for mask in MASKS}, + "histogram": {str(mask): histogram[mask] for mask in MASKS}} + + +def subset_envelope(): + """Independent set-level envelope; this does not enumerate walks.""" + checked = 0 + equalities = 0 + for states in combinations(range(16), 10): + for mask in MASKS: + # Count ordered nonzero differences directly, independently of pair_sums. + cells = [[x for x in states if (x & mask).bit_count() % 2 == p] + for p in (0, 1)] + sizes = sorted(map(len, cells)) + if sizes not in ([4, 6], [5, 5]): + continue + excess = 0 + for cell in cells: + support = {x ^ y for x in cell for y in cell if x != y} + excess += len(cell) * (len(cell) - 1) // 2 - len(support) + if len(cell) >= 5: + require(len(support) == 7, "large-set lemma failed") + if len(cell) == 4: + affine_plane = 0 + for x in cell: + affine_plane ^= x + require((len(support) == 3) == (affine_plane == 0), + "affine-plane equality failed") + require(excess <= 11, "set envelope failed") + if sizes == [5, 5]: + require(excess == 6, "balanced set value failed") + checked += 1 + equalities += excess == 11 + require(checked > 0 and equalities > 0, "empty set corroboration") + return {"admitted_set_functional_pairs": checked, "equalities": equalities} + + +def controls(): + for word in ((0,) * 10, tuple(map(int, "0102301022")), + (0, 1, 0, 2, 3, 0, 1, 0, 2, 4), + (False, 1, 0, 2, 3, 0, 1, 0, 2, 3)): + try: + cycle_states(word) + except ValueError: + pass + else: + raise ValueError("invalid word was accepted") + sharp = cycle_states(tuple(map(int, "0102301023"))) + require(statistics(sharp, 7)[2] == 11, "cap-ten mutation not detected") + require(len({x ^ y for x in sharp for y in sharp}) == 16, + "sharp witness must be universal") + for mask in (0, 16, True): + try: + statistics(sharp, mask) + except ValueError: + pass + else: + raise ValueError("invalid functional was accepted") + low = cycle_states(tuple(map(int, "0102131213"))) + require(statistics(low, 1)[2] == 21 > 13, "weight restriction control") + require(len({x ^ y for x in low for y in low}) == 16, "control universality") + return 9 + + +def receipt(): + root = Path(__file__).resolve().parent + hashes = {} + for name in ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py"): + path = root / name + require(path.stat().st_size <= 1_048_576, "oversize package source") + hashes[name] = hashlib.sha256(path.read_bytes()).hexdigest() + return {"schema": "f7-four-stay-pruning/v1", "claim_type": "scoped proof", + "source_sha256": hashes, "walks": walk_corroboration(), + "sets": subset_envelope(), "controls": controls()} + + +def root_outside_package(path): + checkout = Path(__file__).resolve().parents[2] + return not path.resolve().is_relative_to(checkout) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="create a fresh external JSON receipt") + parser.add_argument("--check-receipt", type=Path, help="compare with a prior receipt") + args = parser.parse_args() + result = receipt() + payload = json.dumps(result, sort_keys=True, indent=2) + "\n" + if args.check_receipt is not None: + require(args.check_receipt.stat().st_size <= 1_048_576, "oversize receipt") + supplied = json.loads(args.check_receipt.read_text(encoding="utf-8")) + require(json.dumps(supplied, sort_keys=True, indent=2) + "\n" == payload, + "receipt does not match this replay and its source hashes") + if args.output is not None: + require(root_outside_package(args.output), "receipt must be outside the checkout") + with args.output.open("x", encoding="utf-8") as stream: + written = stream.write(payload) + require(written == len(payload), "incomplete receipt write") + print("PASS_F7_FOUR_STAY_PRUNING labeled_cycles=2640 functional_checks=13200 " + "max_weight3=11 max_weight4=6 substituted_budget=13 controls=9") + print(payload, end="") + + +if __name__ == "__main__": + main()