diff --git a/research/p104-source-lifetime-216-review/FINITE-RESULTS.json b/research/p104-source-lifetime-216-review/FINITE-RESULTS.json new file mode 100644 index 0000000000..7127a8b62c --- /dev/null +++ b/research/p104-source-lifetime-216-review/FINITE-RESULTS.json @@ -0,0 +1,15 @@ +{ + "schema_version": 1, + "source_commit": "743640530229e1821ae11dc104798871272d6f00", + "census": { + "targets": 104, + "certified_targets": 84, + "permissive_targets": 20, + "exempt_target_ids": [1, 3, 6, 7, 12, 14, 41, 46, 54, 74, 81, 83], + "Tprime_pairs_full": 1038, + "both_halves_Tprime_full_good_targets": 12 + }, + "arrival_floor": 208, + "proof_formula": "E >= ceil((certified - exemptions - 2*permissive)/4)", + "evidence_status": "selected fields transcribed from the exact upstream verifier output; see UPSTREAM-PINS.json for the full replay command and source hashes" +} diff --git a/research/p104-source-lifetime-216-review/PROOF-REVIEW.md b/research/p104-source-lifetime-216-review/PROOF-REVIEW.md new file mode 100644 index 0000000000..ba40182fff --- /dev/null +++ b/research/p104-source-lifetime-216-review/PROOF-REVIEW.md @@ -0,0 +1,110 @@ +# Proof review: the 216-lifetime floor + +## Statement and model + +For the frozen 104-source / 104-target P104 paths from the PR1972/PR1991 +native-channel inputs, every complete X-only monotone correction word for +`C = I - G/2` needs `L ≥ 216` lifetimes in the widened grammar `G′` defined by +the upstream proof. The proof permits arbitrary rational mixing at an equal +frame, even singular mixing; each lifetime grows through nested frames. It +allows source-independent helper births and helper ends at any frame. There +are no reads from Y, the root code, or original helpers. + +The source-lifetime claim is not the 208-flag geometric certificate. Its base +is a program-level arrival count; the extra eight come from the shared-half +count below. The bound does not require restoration or a particular cut +ordering. + +## Counting proof audit + +Let `B_t` be the lifetimes whose nested paths pass through target hyperplane +`H_t`, and let `b_t = |B_t|`. The exact finite census has 104 distinct target +hyperplanes. A strictly nested lifetime can pass through at most one such +8-dimensional hyperplane, so if `J` lifetimes pass through none, + +```text +L = Σ_t b_t + J = 208 + E, +E = Σ_t (b_t - 2) + J ≥ 0. +``` + +The upstream proof establishes `b_t ≥ 2` for every target: with no source read +at `H_t`, target writes there are spanned by the entering helper values; one +entering value would have to support the entire residual row inside one +hyperplane, contradicted by the checked one-cover fact. + +For the full model, the replay classifies 84 targets as certified (“good”): +their intermediate-source counts are in `{0,1,2,4}`. The other 20 are treated +permissively. For a tight certified target (`b_t = 2`), its two helper paths +must pass through complementary 7-dimensional halves. The proof's +singular-mixing lemma says two such tight targets can share both halves only +if the exact pair test `T′` holds on each. The finite `F8′` census finds 12 +certified targets that can have both complementary halves paired under `T′`; +these are the only exemptions in this model. + +Let `m_c` be the number of non-tight certified targets, `m_p` the number of +non-tight permissive targets, `X = Σ_{non-tight t}(b_t - 2)`, and `J` the junk +lifetimes above. Set + +```text +c = 84, π = 20, e = 12, A = c - e - 2π = 32. +``` + +Every tight certified non-exempt target has at least one imperfect half, so +there are at least `c - m_c - e` imperfect halves. They must be witnessed by: + +- a junk lifetime (`γ`), which can witness at most two such halves because a + 7-frame lies in at most two target hyperplanes; +- a lifetime belonging to a non-tight target (`δ`), with at most `X + 2m` + witnesses, where `m = m_c + m_p`; +- a lifetime belonging to a tight permissive target (`ε`), with at most + `2(π - m_p)` witnesses. + +Subtracting the latter two capacities gives +`h_γ ≥ A - 3m_c - X`. Thus `J ≥ max(0, ceil(h_γ/2))` and `E = X+J` satisfies +both `E ≥ X ≥ m_c` and `E ≥ A/2 - m_c`. Adding these two inequalities gives +`2E ≥ A/2`, hence the integer bound `E ≥ ceil(A/4) = 8`. Therefore +`L ≥ 208 + 8 = 216`. + +The proof audit checked the charging cases against the nested-frame contract: +a lifetime crosses at most one 7-frame; any 7-frame is in at most two target +hyperplanes; and a tight target cannot have two lifetimes entering from the +same 7-frame because that would place its full residual support in one +hyperplane. The singular case of the mixing lemma is also handled: a rank-one +mixing matrix makes the two target rows proportional on the shared support, +so `B` is one ratio class and satisfies `T′` by definition. + +The row counts `84`, `20`, the 12 exception IDs, and the `T′` pair census are +finite source facts, not consequences of the counting proof. The pinned +two-implementation replay reproduces them. The mathematical argument remains +a written proof, not a machine-checked proof. + +## Exact inputs and reproduced values + +The replay used the following frozen canonical inputs: + +| Input | SHA-256 | +|---|---| +| `research/p104-native-channel/inputs/LOWRANK-WITNESS.json` | `0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e` | +| `research/p104-native-channel/inputs/P104-FIXTURE.json` | `516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4` | +| `research/complex-local-word-ceiling/ceiling.py` | `86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc` | + +The exact upstream source hashes are in [UPSTREAM-PINS.json](UPSTREAM-PINS.json). +The replay output includes `good_targets=84`, `floor_full_singular_mixing=216`, +`pairs_passing_Tprime_full=1038`, and `both_halves_Tprime_full_good_targets=12` +with IDs `[1,3,6,7,12,14,41,46,54,74,81,83]`. The baseline selected-result +binding check passed at base `20ecf2891d80b5acf18d980b2164fb44ea7faa90`. + +## Limits and provenance + +The replay checks finite geometry and the encoded complete demo word using two +separate implementations plus the vendored published relay checker. The proof +review here independently follows the written counting argument; it does not +constitute independent human review or formal verification. The grammar is +still restricted to its frozen paths and X-only reads. New frames, new source +access, a changed target contract, or a new correlated source state can fall +outside `G′`. + +The result does not show that a word with 216 lifetimes exists. It also does +not price lower-dimensional gathering, primitive count, dirty restoration, +physical hosting or a consumer. The original source handoff pauses this line +unless a sub-7-frame charge is supplied. diff --git a/research/p104-source-lifetime-216-review/README.md b/research/p104-source-lifetime-216-review/README.md new file mode 100644 index 0000000000..ba22a3c15b --- /dev/null +++ b/research/p104-source-lifetime-216-review/README.md @@ -0,0 +1,87 @@ +# P104 source-lifetime floor: 216 in the widened X-only model + +**Result.** The source-bound proof review and pinned replay support the claim +that a complete word correcting all 104 rows of `C = I - G/2` needs at least +216 helper lifetimes in the stated widened grammar `G′`. This grammar permits +arbitrary rational linear mixing among helpers at the same frame, including +singular maps. The bound is conditional on the frozen P104 source and target +frame paths and the X-only monotone access rules below. + +This is the lower-bound lane assigned to macbook-04. It studies the complete +104-row side-correction matrix. It does not construct a word for the other +worker's named 208-flag endpoint collection and does not repeat its static +matching. + +## Proof and evidence + +The mathematical argument and finite census are reviewed in +[PROOF-REVIEW.md](PROOF-REVIEW.md). The exact upstream proof source is +[commit `743640530229e1821ae11dc104798871272d6f00`](https://github.com/thakrarsagar/integer-mult-bounds/tree/743640530229e1821ae11dc104798871272d6f00/research/p104-rank1-mixer-correction). +The source-package file hashes are recorded in [UPSTREAM-PINS.json](UPSTREAM-PINS.json). + +The pinned upstream replay was run from an isolated copy with the canonical +P104 inputs. It ended with: + +```text +PASS_P104_RANK1_MIXER_TOP floor_full=219 floor_final_frame=234 floor_full_singular_mixing=216 pairs_passing_T_final_frame=288 pairs_passing_T_full=414 both_halves_T=0 demo_lifetimes=4974 controls=7 lemma_max_ST=48 +``` + +The replay reports 84 certified targets, 20 permissive targets, and 12 +full-model singular-mixing exceptions (target IDs 1, 3, 6, 7, 12, 14, 41, 46, +54, 74, 81, 83). It reports 1,038 pairs satisfying the singular-mixing test +and no geometric full-model pair passing that test for both complementary +halves outside those 12 targets. + +To reproduce the complete upstream replay, retrieve the package files at the +pinned commit, stage them as `research/p104-rank1-mixer-correction/`, and stage +the two frozen inputs and `ceiling.py` at the paths and hashes in +[SOURCES.json](SOURCES.json). Then run, from the staged repository root: + +```sh +flock /home/user/int-bounds-pass/20261018-luna-xhigh/compute.lock \ + python3.12 -I -B research/p104-rank1-mixer-correction/verify.py +``` + +The package-local `verify.py` checks the fixed source hashes and recomputes +the integer floor from the recorded replay counts. It is an arithmetic check, +not a replacement for the upstream geometric replay or the written proof. +From the repository root, run it with: + +```sh +python3.12 scripts/research_package.py --package research/p104-source-lifetime-216-review +``` + +## Scope limits + +`G′` uses the PR1972/PR1991 P104 source and target paths, X-only source reads, +monotone helper lifetimes, and target writes to the frozen Y paths. It permits +arbitrary rational operations among helpers sharing one frame, including +copies, clears, rescalings, source-independent helper births and early helper +ends. It has no Y reads, root-code reads, or original-helper reads. The proof +does not use dirty restoration or cut order, so it also holds when those are +relaxed within this grammar. + +The result does not establish an executable correction, a physical hosting +bill, a supplier, an all-size theorem, or a new `κ`. The floor is below the +source handoff's first decision-relevant threshold of 333 lifetimes and below +its fixed-template allowances 431, 478 and 482. The two-history relaxation +therefore still passes its optimistic screen; this review changes no budget or +frontier decision. See [PR #2924](https://github.com/CrocSwap/integer-mult-bounds/pull/2924) +for the price under the imported floor. + +## Open next questions + +No next construction or larger census is justified by this floor alone. The +upstream proof identifies a concrete reopening condition: a source-bound +gathering or mixing charge below seven-dimensional frames that could raise the +floor past 333. Until such a charge or a changed source/consumer contract is +available, stop this line. + +## Credit + +The 216/219/234 theorem and checker are by Sagar Thakrar, with substantial +Claude assistance, at the pinned upstream commit. Retain Philippe Van Velzen's +relay grammar and geometry contributions, PR #2353 and its predecessors, and +the Rohan Arun / Chafik Boukhalfa / Adam Gall P104 native-channel lineage. This +review was prepared by GPT-6 Luna xhigh (macbook-04) with substantial OpenAI +Codex assistance. No independent human or proof-assistant review is claimed. diff --git a/research/p104-source-lifetime-216-review/SOURCES.json b/research/p104-source-lifetime-216-review/SOURCES.json new file mode 100644 index 0000000000..ab5c66709c --- /dev/null +++ b/research/p104-source-lifetime-216-review/SOURCES.json @@ -0,0 +1,36 @@ +{ + "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/complex-local-word-ceiling/ceiling.py", + "usage": "input", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + }, + { + "path": "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "usage": "input", + "git_blob": "86beaf424e9f0f800ae3a62797d94ec9386b7706", + "sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e" + }, + { + "path": "research/p104-native-channel/inputs/P104-FIXTURE.json", + "usage": "input", + "git_blob": "2e16f99b295bb386fd13bd8fbd57b42ef54143a9", + "sha256": "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4" + } + ] +} diff --git a/research/p104-source-lifetime-216-review/TASK.json b/research/p104-source-lifetime-216-review/TASK.json new file mode 100644 index 0000000000..07e9caff2b --- /dev/null +++ b/research/p104-source-lifetime-216-review/TASK.json @@ -0,0 +1,82 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "p104-side-correction", + "question": "Can the proposed P104 joint endpoint flags be realized by a chronological correction program with coefficients, dirty restoration and an affordable complete bill?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/p104-native-channel/README.md", + "research/p104-native-channel/PROOF.md", + "docs/research/community-efficient1000-review.md", + "research/p104-joint-unit-flags/README.md" + ], + "methods": [ + "Construct one side-correction word at an explicit chronological cut with the needed frames still available.", + "Derive a lower bound on the side correction and hosting costs that decides whether this channel can beat the selected budget." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the revision-6 family record and #2981 static joint flags, alongside the reviewed #1991 channel. #2981 is an author-checked source archive, not an independently validated executable correction or a refutation of program-level lifetime floors.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "After checking live handoffs, pin one named collection from #2981 and attach acquisition/delivery times, source dependencies and coefficient requirements. Test legal access and arbitrary dirty restoration; price any completion against the full channel/endpoint/hosting allowance. Stop with the exact missing implication or a scoped counterexample rather than expanding the static cover census.", + "bottleneck_link": "Completing an already realized changed channel tests a concrete construction opportunity, instead of refining the incumbent packing. A positive local result still needs global and all-size admission.", + "allowed_variations": [ + "One correction factorization, one chronological cut, or one explicit hosting obstruction.", + "A changed correction schedule with an updated full bill and native frame contract." + ], + "scope_change_triggers": [ + "Recompiling the already certified low-rank channel without closing a new obligation.", + "Treating a pending ancestor, local histogram or unpriced side correction as an admitted global supplier.", + "Repeating a correction or physical conversion already supplied by a pending follow-up without adding independent coverage or a different unresolved obligation.", + "Repeating the 208-flag static matching or calling a static nested cover a chronological correction program. Independent audit of that certificate is distinct and remains useful." + ], + "overlap_terms": [ + "P104", + "I-G/2", + "side correction", + "native channel", + "1972", + "1991", + "2586", + "endpoint transport", + "physical dual", + "relay composition", + "2981", + "joint unit flags", + "acquisition delivery", + "static nesting" + ], + "existing_checks": [ + { + "scope": "PR #2981 reports static joint endpoint flags and a matching of 208 departure and arrival flags; archival intake is not independent verification.", + "evidence": "research/p104-joint-unit-flags/README.md", + "remaining": "Independent flag check and a chronological coefficient program with dirty restoration and a complete cost.", + "status": "author-checked", + "source_commit": "3d24b92d8ba057b57cb2d480170ec407520e6882", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Audit the reported 216-lifetime lower bound for the full 104-row P104 side-correction matrix C = I - G/2 under the widened X-only monotone helper grammar G-prime. This is distinct from constructing a chronological word for one named 208-flag endpoint collection.", + "scope_change_reason": "The macbook-04 assignment is the complementary lower-bound lane. It checks one existing source-lifetime floor for the all-target correction matrix instead of constructing or re-counting the 208 matched endpoint flags assigned to the constructive worker.", + "bottleneck_link": "The floor tests a program-level necessary condition for correcting the P104 native channel after the 208 static endpoint flags. It confirms a real lifetime cost but does not reject the currently priced two-history relaxation.", + "budget_minutes": 60, + "stop_rule": "Stop after replaying the exact source-bound census and auditing the written counting proof. Do not launch another construction or lifetime census unless a changed source/consumer contract or a decision-relevant budget makes this floor insufficient.", + "outcome": "completed", + "evidence": "See README.md and PROOF-REVIEW.md. The exact upstream handoff commit 743640530229e1821ae11dc104798871272d6f00 was replayed with its primary, second, and vendored relay checkers against the frozen P104 input hashes. The checked finite facts give 84 certified targets, 20 permissive targets and 12 G-prime exceptions; the written charging argument then gives A=32, E>=8, L>=216.", + "author": "GPT-6 Luna xhigh (macbook-04)", + "ai_assistance": "Substantial OpenAI Codex assistance (GPT-6 Luna xhigh). The source replay and proof audit were performed by this agent; no human or formal-kernel review is claimed.", + "open_questions": [], + "no_open_questions_reason": "The floor is 216, below the 333-lifetime first decision threshold cited by the source handoff and below the 431/478/482 fixed-template allowances. The source proof itself says the next useful step requires a concrete sub-7-frame gathering charge. No such charge was established in this session, so extending the census would not change a decision." +} diff --git a/research/p104-source-lifetime-216-review/UPSTREAM-PINS.json b/research/p104-source-lifetime-216-review/UPSTREAM-PINS.json new file mode 100644 index 0000000000..212d7dd7dc --- /dev/null +++ b/research/p104-source-lifetime-216-review/UPSTREAM-PINS.json @@ -0,0 +1,26 @@ +{ + "schema_version": 1, + "repository": "https://github.com/thakrarsagar/integer-mult-bounds", + "commit": "743640530229e1821ae11dc104798871272d6f00", + "base_main": "d9b24831174325cad2e04e34da2068d7acb02938", + "priority_revision_at_source": 5, + "files": { + "research/p104-rank1-mixer-correction/README.md": "c3d18662146bfcf35ed519d54169790cdf2e8392f7a8dffccdb7638c376c17a3", + "research/p104-rank1-mixer-correction/PROOF.md": "cd7160916a0881528a679d487b51ed8b26eebd4384fb6b08e4cd0555cb47c537", + "research/p104-rank1-mixer-correction/SOURCES.json": "0722fc23d6b93d68583add6feb1fd0fe9dbacb9ded97a9ef420de0341a0a2630", + "research/p104-rank1-mixer-correction/TASK.json": "40178fc989fa2a1484c8f6cdcf0422061562f1cca1f24871830a80582105dfb8", + "research/p104-rank1-mixer-correction/VERIFY.json": "2670526cf82df4fa863f261edfea23e1a4611bb07a17a5380af300d0844c2ec5", + "research/p104-rank1-mixer-correction/EXPECTED.json": "6b3ad2936578d8da217b37fe0ce7789981db7a69279cbed95bf3cd59f104516c", + "research/p104-rank1-mixer-correction/build_demo.py": "c524b8579c3aef8352b2f43b31a0468ec4668a167fbdb7dd68cfbdde94a04207", + "research/p104-rank1-mixer-correction/independent.py": "40c554719bec44a23c3624f0f7e844555b9f112c3ec904d97eb03edd2c57d9b3", + "research/p104-rank1-mixer-correction/top_primary.py": "aaad5ea11a70b6e240c68ed39972dc29e26dcffb2f63572874df2b25d02ed66f", + "research/p104-rank1-mixer-correction/verify.py": "fe1cecca76207055acbd17ab1a7bc666862ec33ad70b0992c186d081f9dc2800", + "research/p104-rank1-mixer-correction/vendor/check_p104_relay_construction.py": "b808e70129fc2c01fbead974c770e0a39245f3a3968c53bcd1f49fb1972e865d" + }, + "replay": { + "command": "python3.12 -I -B research/p104-rank1-mixer-correction/verify.py", + "environment": "CPython 3.12.3; standard library only; single-threaded under the host-wide compute lock", + "result": "PASS_P104_RANK1_MIXER_TOP floor_full=219 floor_final_frame=234 floor_full_singular_mixing=216 pairs_passing_T_final_frame=288 pairs_passing_T_full=414 both_halves_T=0 demo_lifetimes=4974 controls=7 lemma_max_ST=48", + "status": "replayed locally from exact handoff commit; no hosted CI or independent human review claimed" + } +} diff --git a/research/p104-source-lifetime-216-review/VERIFY.json b/research/p104-source-lifetime-216-review/VERIFY.json new file mode 100644 index 0000000000..ced012daf9 --- /dev/null +++ b/research/p104-source-lifetime-216-review/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/complex-local-word-ceiling/ceiling.py", + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "research/p104-native-channel/inputs/P104-FIXTURE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Checks the declared frozen-input hashes and recomputes the exact integer implication A=32, E>=8, L>=216 from the finite census recorded from the pinned upstream replay. This local arithmetic verifier does not replace the full upstream geometric replay; its exact commit and replay result are documented in README.md." + } + ] +} diff --git a/research/p104-source-lifetime-216-review/verify.py b/research/p104-source-lifetime-216-review/verify.py new file mode 100644 index 0000000000..c657ee3e4e --- /dev/null +++ b/research/p104-source-lifetime-216-review/verify.py @@ -0,0 +1,59 @@ +#!/usr/bin/env python3 +"""Check the P104 lifetime-floor arithmetic and frozen input hashes. + +The geometric census and proof are upstream and are not reimplemented here. +""" +import hashlib +import json +from pathlib import Path + + +ROOT = Path(__file__).resolve().parents[2] +HERE = Path(__file__).resolve().parent +LOCAL_PINS = { + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json": + "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e", + "research/p104-native-channel/inputs/P104-FIXTURE.json": + "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4", + "research/complex-local-word-ceiling/ceiling.py": + "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc", +} + + +def require(condition, message): + if not condition: + raise SystemExit("FAIL_P104_LIFETIME_FLOOR_216: " + message) + + +def main(): + for rel, expected in LOCAL_PINS.items(): + actual = hashlib.sha256((ROOT / rel).read_bytes()).hexdigest() + require(actual == expected, "frozen input hash mismatch: " + rel) + + facts = json.loads((HERE / "FINITE-RESULTS.json").read_text()) + upstream = json.loads((HERE / "UPSTREAM-PINS.json").read_text()) + require(upstream["commit"] == facts["source_commit"], + "finite census is not bound to the recorded upstream commit") + require(upstream["replay"]["result"].startswith("PASS_P104_RANK1_MIXER_TOP "), + "upstream replay receipt is missing its pass marker") + census = facts["census"] + require(census["targets"] == 104, "wrong target count") + require(census["certified_targets"] + census["permissive_targets"] == 104, + "certified/permissive split does not cover all targets") + exempt = census["exempt_target_ids"] + require(len(exempt) == census["both_halves_Tprime_full_good_targets"] == 12, + "wrong singular-mixing exception count") + require(census["Tprime_pairs_full"] == 1038, "wrong singular-mixing pair census") + + a = (census["certified_targets"] - len(exempt) + - 2 * census["permissive_targets"]) + excess = (a + 3) // 4 + floor = facts["arrival_floor"] + excess + require(a == 32 and excess == 8 and floor == 216, + "the exact integer floor does not reproduce") + print("PASS_P104_LIFETIME_FLOOR_216_ARITHMETIC certified=84 permissive=20 " + "exempt=12 A=32 excess=8 floor=216") + + +if __name__ == "__main__": + main()