[JosieElliston]

Summary

Navigation index plus a partial finite replay; no new bound, no κ, no supplier or frontier change. Card scope-navigation (consolidation), base 721c03822c421b7f7fcbb2598993b947c4d88419, priority revision 8. New package research/f7-record-map; no other file changes.

Question. Item 5 of petalas's consolidation handoff says the records disagree on f(7). #3058 says f(7) = 24, and research/f7-independent-full-replay (#3333) says {22,24}.

Answer: they agree. #3333 is a length-20 replay. It says it "does not decide whether length 22 is attainable". Length 22 is excluded on main by two routes that share no search code:

• Research: exact seven-source singleton minimum f(7) = 24 #3058's covering-code argument, audited piecewise by Research: audit connector-covering-code's parity-capacity filter and its simple-word boundary #3224, Research: audit singleton connector path-domain propagation #3244, Audit complete candidate representation in the seven-source search #3261, Audit seven-source search completeness and interruption #3276, Audit seven-source gap traversal and caller exhaustion #3287, Certify four seven-source B exclusions with checked SAT proofs #3360 and Audit the 20-prefix confinement step of the length-22 exclusion (no new kappa) #3728.
• The census chain Correct word-census parity budgets; 22 <= f(7) <= 24 in the PR943 model #2973 → Derive the complete length-22 parity-split domain at seven labels (no census, no f(7)) #3708/Eleven length-22 splits survive, and nine survive the 17-point import #3712 → Bounded length-22 census probe: exclude splits (11,7), (10,8), (11,8); measure the rest (answers #3708 OQ1's blocker; no new kappa) #3731/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, bound to its domain by Bind length-22 census receipts to the derived split domain #4871.

The README's record map lists, for each length step, the route, the records, the independent coverage and what is still open. Every one of those records is partially_reviewed in the ledger.

Second engine at length 22. #4221's first open question, which #4871 repeats, is that every census-route L = 22 exclusion rests on one engine. The recorded blocker was that #3005's separately written engine "is gated at L <= 20 and its throughput at length 22 is unmeasured". The gate is one constant. verify.py rebuilds #3005's census.cpp from the pinned bytes with exactly two lines changed (max_length and its error message) and runs it at n = 7, L = 22:

Split	Entered nodes (this engine)	Hits	Prior engine nodes
(11,9)	11,942,611,230	0	#4221 14,058,107,415
(10,9)	6,624,261,154	0	#4221 7,027,617,655
(11,8)	973,631,241	0	#3731 1,349,702,650
(9,9)	386,427,869	0	#3818 388,563,293
(10,8)	238,010,457	0	#3731 597,933,297
(11,7)	8,613,944	0	#3731 8,784,744
(10,7)	699,412	0	#4221 700,909
(11,6)	1,020	0	#4221 2,247
(11,11)	37,567,052,539	0	#4221 55,385,607,437
(11,10)	40,743,043,536	0	#4221 52,957,641,635
(10,10)	37,400,857,165	0	#4221 44,378,511,529

All 11 splits close on the second engine with zero hits, all complete and uncapped. The three heaviest took 3,751 to 4,188 s each and were added in a follow-up commit. Every census-route L = 22 exclusion now rests on two separately written engines. The two engines are separately written, but #3818's engine ports #3005's union-support bound. The proof of that bound is therefore a premise of both; the code is not shared.

Controls:

• At L = 18 and L = 20, every summary field equals Independently corroborate the corrected seven-label word exclusion #3005's FULL.json.
• A capped n = 6, L = 22 run finds hits, and each one is checked by direct XOR coverage.
• A capped n = 7 run exits 2.
• Four tamper controls are rejected: a changed quote, a changed node count, a dropped domain split and a changed engine digest.

Entered-node counts track #3731/#3818: (9,9) gives 386,427,869 here against 388,563,293.

Scope and limits

• The census route still imports Derive the complete length-22 parity-split domain at seven labels (no census, no f(7)) #3708's four split conditions and its rotation symmetry, so only s >= t runs. It also relies on the pruning proofs of Independently corroborate the corrected seven-label word exclusion #3005 (this engine) and Strengthen the length-22 seven-label census with a union-support budget; exclude the (9,9) split (no new kappa) #3818 (the other engine).
• Research: exact seven-source singleton minimum f(7) = 24 #3058 §3, the 21-distinct-prefix case, has no independent audit that I found on main. Certify four seven-source B exclusions with checked SAT proofs #3360 lists it as out of scope. Pattern A and 73 of the 77 pattern-B cases rest on the native search only.
• Consumers (Prove an eight-source singleton floor of 28 calls (no new κ) #5234, Research: projection matching obstruction for eight-source singleton lifts (partial result) #5430, Construct 21- and 20-call seven-source DUO connector words, beating (22, 24) (no new κ) #6005) cite only Research: exact seven-source singleton minimum f(7) = 24 #3058. They use only the value, so the census route serves as well.
• The L = 22 runs are LOCAL-ONLY receipts (macOS arm64, Apple clang 21). CI replays (11,6), (10,7) and (11,7) by default, and (9,9) and (10,8) in a second registered command.

Reproduce

python3 -I -B research/f7-record-map/verify.py
python3 -I -B research/f7-record-map/verify.py --splits 9:9,10:8 --workers 2
python3 -I -B research/f7-record-map/verify.py --full --workers 8   # all completed splits, ~1.5 CPU-hours
python3 scripts/research_package.py --package research/f7-record-map --check-only

Open next questions

1. research: independently audit L22 union prune on tiny domain #3899's tiny-domain audit of the union-support prune (open). Both engines depend on that bound.

The other two are #3058 §3 and pattern A plus the remaining B cases; details are in the README.

Overlap and credit

• Overlap: find_overlap.py, PR and Discussion searches for f(7)/length-22/seven-label, and the ledger. research: independently audit L22 union prune on tiny domain #3899 is the only open f7 PR, and it is a tiny-domain audit of the union prune, disjoint from this.
• Claim: Handoffs and requests for independent checks #1166 (reply in thread)
• Codex adversarial review (read-only): it found the lift sound (iteration bound 9.12e18 < 2^64, 11 slots per side, convention s = |E| matching Derive the complete length-22 parity-split domain at seven labels (no census, no f(7)) #3708) and corrected two map overstatements. Research: exact seven-source singleton minimum f(7) = 24 #3058 has its own Python port for pattern A and two checkers for §3. Both corrections are applied.
• Credit: petalas for the question. Nick Petalas for the engine (Independently corroborate the corrected seven-label word exclusion #3005) and much of the L = 22 chain. The routes belong to conorholds (Research: exact seven-source singleton minimum f(7) = 24 #3058), Nicholas Stone (Correct word-census parity budgets; 22 <= f(7) <= 24 in the PR943 model #2973), James Reed (Eleven length-22 splits survive, and nine survive the 17-point import #3712, Record the confinement multiplicity sums #3732), codyw912 (Bind length-22 census receipts to the derived split domain #4871), 1337isnot1337 (Research: independently replay corrected f7 length-20 census #3333), commdata2338 (Research: audit connector-covering-code's parity-capacity filter and its simple-word boundary #3224), krzysztofwojt (Audit complete candidate representation in the seven-source search #3261), JoyboyBrian (Classify every consumer of the bit-0 census prune: no relied exclusion affected (no new κ) #4946), Douglas Colkitt (Research: six-source universal dirty-connector boundary, f(6)=16 (no new kappa) #1185) and Ross Richardson (Research: sharp four/five-source dirty-connector boundary (no new kappa) #943).
• Prepared by Claude Opus 5.5 for JosieElliston in an unattended session. Codex was used only for a read-only adversarial review. No human review.

Workflow feedback: find_overlap.py did not connect the two f(7) records because #3333 never cites #3058. A per-family index such as this README is cheaper than re-deriving the map each time.

🤖 Generated with Claude Code