[JoyboyBrian]

Result

This PR adds a source-impact audit of the #2973 bit-0 word-census error across the whole tree, in research/census-prune-source-impact. It adds no new κ and no new f(7) bound, and it changes no frozen package or the selected frontier.

• The pruning rule is disproved. The rule groups prefix states by bit 0 and applies the balanced L/2 budget. It lives in the Research: seven-source singleton universal path — length 18 excluded, f(7) >= 20 (no new kappa) #2542 cyclic_census bytes (SHA-256 82e4c407…), which are byte-identical in the Research: seven-source singleton universal path — length 18 excluded, f(7) >= 20 (no new kappa) #2542, KB3b: seven-source singleton f(7) continued - parity closes L=19, beating templates closed, cover/walk dichotomy, resumable 20-cycle census (no new kappa) #2634 and KB3c: 17-point cover audit - PR 2542's 'no 17-point set covers F2^7' against its own lemma table (no new kappa) #2773 vendor copies, and in Independent audit of PR2634 census + completion of the (10,10) exclusion at L=20 #2691's f7_census.c (nq & 1, BUDGET 27).
  • On 01021323, the weight-parity excess is 0 against a budget of 5. The bit-0 excess is 8, against the balanced budget 5 and the actual-size budget 9.
  • The faulty engine was loaded from authenticated bytes and compared with an independent oracle on the complete n=4, L=8 simple domain. It falsely prunes exactly 6 of the 22 universal words. The weight-parity rule prunes 0.
• No final bound is disproved. No exclusion the current f(7) line relies on uses the faulty bytes, cyclic_census or nq & 1 grouping. The replacement sources checked are Correct word-census parity budgets; 22 <= f(7) <= 24 in the PR943 model #2973, Independently corroborate the corrected seven-label word exclusion #3005, Research: independently replay corrected f7 length-20 census #3333, Strengthen the length-22 seven-label census with a union-support budget; exclude the (9,9) split (no new kappa) #3818/Close the length-22 seven-label word census: all splits excluded, f(7) = 24 in the prefix-walk model (no new κ) #4221 and Research: exact seven-source singleton minimum f(7) = 24 #3058 §1–2.
• Whole-tree classification at base cef4b52. verify.py --rescan scanned 90,399 files. Every file containing the faulty bytes, a cyclic_census definition or call, the native rule, the old L18/L20 receipts or a 20 <= f(7) statement falls under one of 21 classified prefixes. There are 0 unclassified files and 0 stale prefixes.
• Downstream exclusions that need revalidation: exactly three, and all three already have merged replacement evidence. They are the Research: seven-source singleton universal path — length 18 excluded, f(7) >= 20 (no new kappa) #2542 L18, KB3b: seven-source singleton f(7) continued - parity closes L=19, beating templates closed, cover/walk dichotomy, resumable 20-cycle census (no new kappa) #2634 partial L20 and Independent audit of PR2634 census + completion of the (10,10) exclusion at L=20 #2691 (10,10) L20 word exclusions.
  • The set-level packages KB3c: 17-point cover audit - PR 2542's 'no 17-point set covers F2^7' against its own lemma table (no new kappa) #2773–KB3h: (12,6) A-vanish (5,1) PROVEN impossible; (4,2)/(3,3) reduced to exact walkable forms (outcome=partial; no new kappa) #3023 split by weight parity, so this error does not affect them.
  • KB3c: 17-point cover audit - PR 2542's 'no 17-point set covers F2^7' against its own lemma table (no new kappa) #2773, KB3d: (11,6)/(6,11) remainder rows (5,1),(6,0) of the 17-point cover question impossible by an exact Fourier/Parseval identity (no new kappa) #2870, KB3e: the 18-point cover question for F2^7 narrowed to an exact finite remainder (outcome=partial, no new kappa) #2911 and KB3f: the vanishing-character restriction on the 18-point cover question for F2^7 (outcome=partial, no new kappa) #2933 carry L18 universal=0 anchors produced by the unsound filter, and KB3c: 17-point cover audit - PR 2542's 'no 17-point set covers F2^7' against its own lemma table (no new kappa) #2773–KB3h: (12,6) A-vanish (5,1) PROVEN impossible; (4,2)/(3,3) reduced to exact walkable forms (outcome=partial; no new kappa) #3023 cite 20 <= f(7). These need a reading note, not revalidation. Whether to add one is left to maintainers (open question 1).

Task and overlap

• Card: census-pruning-audit (adversarial-audit track), scope refined.
• Already merged: the card's calibration and the Research: seven-source singleton universal path — length 18 excluded, f(7) >= 20 (no new kappa) #2542 trace (Record the bit-0 census false prune on 01021323 #3096, Record the prefix-budget counterexample #3821), a six-file inventory (Research: audit PR #2542's set/word pruning and refute its minimum-length degree-filter justification #3215) and the corrected replays (Correct word-census parity budgets; 22 <= f(7) <= 24 in the PR943 model #2973, Independently corroborate the corrected seven-label word exclusion #3005, Research: independently replay corrected f7 length-20 census #3333). Research: audit PR #2542's set/word pruning and refute its minimum-length degree-filter justification #3215 states that its inventory is "not a whole-repository dependency proof", so this PR takes that remaining step. It is the card's allowed "one downstream dependency audit" variation.
• Repetition: the calibration is repeated only to bind the hash to the defect.
• Overlap check: scripts/find_overlap.py --task census-pruning-audit, a grep of research/ for Correct word-census parity budgets; 22 <= f(7) <= 24 in the PR943 model #2973/Research: seven-source singleton universal path — length 18 excluded, f(7) >= 20 (no new kappa) #2542/KB3b: seven-source singleton f(7) continued - parity closes L=19, beating templates closed, cover/walk dichotomy, resumable 20-cycle census (no new kappa) #2634/Independent audit of PR2634 census + completion of the (10,10) exclusion at L=20 #2691, and the open PRs. research: independently audit L22 union prune on tiny domain #3899, an L22 union-prune audit, is adjacent but does not overlap.
• Claim: Handoffs and requests for independent checks #1166 (comment)
• Base: cef4b52f2a59009865bf8eabde1be3f159063703

Test plan

All of the following passed:

• python3.12 -B research/census-prune-source-impact/verify.py → PASS_CENSUS_PRUNE_SOURCE_IMPACT pinned=26 false_prunes_n4L8=6/22 controls=7 no_new_kappa
• The same command under -O and under -I -W error.
• python3.12 -B research/census-prune-source-impact/verify.py --rescan → ... rescan_files=90399 ..., which takes about 40 s and is bound to the base commit.
• python3 scripts/research_package.py --package research/census-prune-source-impact --check-only → PASS_PACKAGE_METADATA_AND_PINS
• python3.12 -B scripts/research_package.py --package research/census-prune-source-impact → PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=completed
• python3.12 -B scripts/check_research_commit.py --package research/census-prune-source-impact --check-source-history → PASS_RESEARCH_COMMIT_BYTES
• python3.12 -W error -B -m unittest discover -s tests -p 'test_research_onboarding.py' → 26 tests OK.
• In-verifier controls: all 7 fail as required.
  • An audit caller relabelled as a replacement.
  • The native rule relabelled as a replacement.
  • A tampered pin.
  • The Research: exact seven-source singleton minimum f(7) = 24 #3058 evidence weakened to f(7) >= 20.
  • Planted unclassified consumers.
  • The balanced bit-0 budget applied to 01021323.
  • Bit-0 grouping substituted into the corrected rule.
• Separate source mutation run: 7 of 7 mutants were killed.
  • An off-by-one budget.
  • Weight parity replaced by bit 0.
  • A changed calibration word.
  • A stale citation relabelled as a replacement.
  • A faulty engine relabelled as an audit caller. This mutant survived the first run, so a faulty-bytes role invariant was added.
  • A removed intake prefix.
  • A changed recorded result.

Not run: no Lean, Docker or seven-label census, and no replay of the replacement censuses. Whether #2973, #3058 and #4221 are scientifically correct is outside this PR. The scan is syntactic, and phrase-level citations would be missed (open question 3).

Open next questions

1. Should the frozen L18 anchors (KB3c: 17-point cover audit - PR 2542's 'no 17-point set covers F2^7' against its own lemma table (no new kappa) #2773 verify.py, and the KB3d: (11,6)/(6,11) remainder rows (5,1),(6,0) of the 17-point cover question impossible by an exact Fourier/Parseval identity (no new kappa) #2870, KB3e: the 18-point cover question for F2^7 narrowed to an exact finite remainder (outcome=partial, no new kappa) #2911 and KB3f: the vanishing-character restriction on the 18-point cover question for F2^7 (outcome=partial, no new kappa) #2933 receipts) get a reading note or a successor entry point? That is a maintainer decision.
2. Can Independently corroborate the corrected seven-label word exclusion #3005's census be extended past L=20, to give the single-engine L22 exclusions (Strengthen the length-22 seven-label census with a union-support budget; exclude the (9,9) split (no new kappa) #3818, Close the length-22 seven-label word census: all splits excluded, f(7) = 24 in the prefix-walk model (no new κ) #4221) a second implementation?
3. Can the rescan detect phrase-level citations of the old exclusions?

Credit

• Ross Richardson: the PR943 model.
• Aaron Wang (navinor): Research: seven-source singleton universal path — length 18 excluded, f(7) >= 20 (no new kappa) #2542 and KB3b: seven-source singleton f(7) continued - parity closes L=19, beating templates closed, cover/walk dichotomy, resumable 20-cycle census (no new kappa) #2634, and the set-level chain KB3c: 17-point cover audit - PR 2542's 'no 17-point set covers F2^7' against its own lemma table (no new kappa) #2773–KB3h: (12,6) A-vanish (5,1) PROVEN impossible; (4,2)/(3,3) reduced to exact walkable forms (outcome=partial; no new kappa) #3023.
• Nicholas Stone: Independent audit of PR2634 census + completion of the (10,10) exclusion at L=20 #2691, and the Correct word-census parity budgets; 22 <= f(7) <= 24 in the PR943 model #2973 correction and 01021323.
• Nick Petalas: Independently corroborate the corrected seven-label word exclusion #3005, Derive the complete length-22 parity-split domain at seven labels (no census, no f(7)) #3708, Strengthen the length-22 seven-label census with a union-support budget; exclude the (9,9) split (no new kappa) #3818 and Close the length-22 seven-label word census: all splits excluded, f(7) = 24 in the prefix-walk model (no new κ) #4221.
• conorholds: Research: exact seven-source singleton minimum f(7) = 24 #3058.
• jwr404: Record the bit-0 census false prune on 01021323 #3096 and Record the prefix-budget counterexample #3821.
• commdata2338: Research: audit PR #2542's set/word pruning and refute its minimum-length degree-filter justification #3215 and Research: audit connector-covering-code's parity-capacity filter and its simple-word boundary #3224.
• 1337isnot1337: Research: independently replay corrected f7 length-20 census #3333.
• Douglas Colkitt: the package framework.

Prepared by JoyboyBrian with substantial assistance from Anthropic Claude (Claude Code, Opus 5.5). No independent human review is claimed.

🤖 Generated with Claude Code