diff --git a/research/f7-l22-receipt-domain/README.md b/research/f7-l22-receipt-domain/README.md new file mode 100644 index 0000000000..2346bd0100 --- /dev/null +++ b/research/f7-l22-receipt-domain/README.md @@ -0,0 +1,273 @@ +# Bind the length-22 acceptance domain to the recorded census receipts + +**Scoped successor to #4221 Open next question 2. No new census, no new kappa, +no newly proved `f(7) = 24`.** This package replaces trust in a copied split +list with an independent arithmetic reimplementation of the credited #3708 +mathematics and an exact acceptance adapter. It leaves every predecessor package, +engine, selected record and ledger intact. + +## Result and evidence status + +The supplied checker derives **eleven** representatives `s >= t` at `n=7, L=22` +from four necessary conditions, before any 17-point exclusion. It compares every +arithmetic row with #3708's retained pre-import result, including revisits and +self-avoidance. It then requires the four completed #3818 receipts and seven +completed #4221 receipts to form an exact partition of that domain. Duplicate +split rows are rejected before constructing a mapping; coverage cannot be +silently narrowed by deleting a domain entry and its receipt together. + +**Completed scoped acceptance adapter; author-checked/orchestrator-replayed.** +On 2026-10-22, the orchestrator observed metadata validation and both registered +normal and `-O` replays pass under **CPython 3.12.13**. Both replays emitted +`PASS_F7_L22_RECEIPT_DOMAIN domain=11 prior=4 deep=7 controls=30 no_census_replay`. +The emitted `recorded_deep_nodes=173808188827` is the sum of authenticated +historical receipt counts, **not nodes executed by this adapter**. Read-only +Git-object extraction and standard hashing also found all twelve declared +source files equal to their package-base working bytes. A completed independent, +read-only AI review found no blocking mathematical or acceptance defect; the +reviewer performed no execution. Neither that review nor the replay receipts +constitute independent human review, formal verification or scientific endorsement. + +This is an **authenticated-recorded-counts adapter**, not independent census +replay. Its finite controls test the acceptance boundary; they do not manufacture +mathematical novelty or establish the correctness of the full enumeration. + +## Exact scope and source lineage + +Package base: `b58ad9ef4d4e861b0eaa5dba41742bdc072dca51`, priority revision 7. +The selected conditional kappa at this base is `0.00302015`, unchanged. + +- [#4221](https://github.com/CrocSwap/integer-mult-bounds/pull/4221), Nick + Petalas, head `9d21222c67ecd40f49935a1e56b11f2b50d54613`: + [deep-shard census](../f7-l22-deep-shard-census/README.md), especially + `verify.py`'s `check_receipt()` and + [Open next questions](../f7-l22-deep-shard-census/README.md#open-next-questions), + question 2, “Recompute the domain inside the verifier.” Its receipt, engine + manifest and cover generator are retained unchanged. +- [#3708](https://github.com/CrocSwap/integer-mult-bounds/pull/3708), head + `ba1aff20ee3ce3dce35e4978feab0b6be08c7168`: + [split-domain proof](../f7-l22-split-domain/README.md#the-derivation-and-what-is-proved-here) + and [length-22 domain](../f7-l22-split-domain/README.md#the-length-22-domain), + arithmetic in `verify.py`'s `identity_need()`, `even_budget()`, `split_row()` + and `admissible_splits()`, and the pre-import `RESULT.json` rows. +- [#3818 union census](../f7-l22-union-census/README.md): retained `RESULT.json` + and unchanged `engine/union_census.c`. The latter is hashed, never compiled. + +All `SOURCES.json` source pins resolve at the package base, so every source +commit is an ancestor of the base (the base itself). The two historical PR heads +above identify attribution and review context, not extra unmerged dependencies. +The originating catalogue card and selected record are Git provenance; the ten +research inputs are live and all are listed in `VERIFY.json`. The original card +was copied from the committed base object, not from a mutable task-picker result. + +The catalogue's `census-pruning-audit` card is **refined** to one downstream +acceptance-boundary audit. This answers the explicit retained open question +rather than repeating a tiny-domain prune audit or launching a larger search. +No pruning implementation changes. The scoped budget is 60 minutes; registered +replay is bounded by two 30-second command timeouts, without compilation or +enumeration of length-22 words. + +Final local overlap intake on **2026-10-22** covered **299 open PRs** at +**19:49:07Z** and **3,721 Discussion records** at **19:49:40Z**, with complete +pagination, plus all **5,860 tracked local notes** and two other new package +notes. Exact phrase searches found predecessor/own-note references only. This +is not a novelty proof, an arbitrary-diff search or an exhaustive search of +closed remote PRs. Coordination is local-only; no public Discussion claim is +asserted. Canonical refresh `624de9dc66858af0945e5f8a0942488d62280d43` left +the guidance, catalogue, selected record and all source packages unchanged +relative to the pinned scientific base; the original base and card pins remain. + +## Derivation and proof boundary + +Let `q_0,...,q_22=q_0` be the restored singleton prefix walk in `F_2^7` and let +`P` be its distinct prefix states. Write `E,O` for their Hamming-weight parity +classes and `s=|E|, t=|O|`. A universal prefix set has `P+P=F_2^7`. The following +are necessary conditions, **not sufficient conditions for a word to exist**. + +1. **Time:** parity alternates with step number. Among positions `0,...,21` + there are eleven of each parity; `q_22=q_0` supplies no new state. Thus + `s,t <= 11`. +2. **Odd budget:** each of the 64 odd masks needs an `E x O` pair, so + `s*t >= 64`. +3. **Even budget:** the 63 nonzero even masks need unordered, distinct same-class + pairs. Thus `B = C(s,2)+C(t,2)-63 >= 0`. +4. **Pair identity:** let `A_x,B_x` be unordered pair multiplicities at nonzero + even mask `x` within `E,O`, and let `r_y` count cross pairs at odd `y`. + Counting four-cycles gives + `sum_y C(r_y,2) = 2 sum_x A_x B_x`. + Since every odd mask occurs and `C(r,2) >= r-1`, the right sum is at least + `ceil((s*t-64)/2)`, denoted `need`. Let `a,b >= 0` be the collision excesses + within the two same-class supports. Their intersection has size `B-a-b`. + Expanding `A_x B_x` on that intersection bounds its sum by + `(B-a-b)+a+b+a*b = B+a*b`. In particular `a+b <= B` and + `a*b <= floor(B^2/4)`. Hence `need <= B+floor(B^2/4)` is necessary. + +At `L=22`, the even-budget condition is redundant once the identity-bound check +is enforced: the adapter makes its identity upper bound negative when `B < 0`, +whereas `need >= 0`. These are four stated necessary conditions, not four +separately load-bearing acceptance controls. + +A one-step rotation translates the restored prefix set by an odd state and +swaps its parity classes, preserving universality. Therefore `s >= t` is a +complete quotient of the ordered split problem. This written implication and +the underlying singleton prefix-walk interpretation are inherited from #3708; +they are not re-proved by the finite controls or checked in a formal kernel. + +`verify.py` enumerates all positive `1 <= t <= s <= 22`, deliberately beyond the +time bound, and applies the four conditions using only integer arithmetic. +This is an independent arithmetic reimplementation of #3708's mathematics, +not an independent discovery or proof of those necessary conditions. There is +no acceptance-domain table in the adapter. The recorded table is used **only as +a comparison oracle after recomputation**, not as the source of accepted splits. +The integer product bound is also checked by direct maximization over +`a+b <= B` for `B=0,...,47`; the ceiling check includes the odd excess 57. + +| Split | Distinct points | Revisits among cyclic positions | `B` | `need` | +|---|---:|---:|---:|---:| +| (11,11) | 22 | 0 | 47 | 29 | +| (11,10) | 21 | 1 | 37 | 23 | +| (11,9) | 20 | 2 | 28 | 18 | +| (10,10) | 20 | 2 | 27 | 18 | +| (11,8) | 19 | 3 | 20 | 12 | +| (10,9) | 19 | 3 | 18 | 13 | +| (11,7) | 18 | 4 | 13 | 7 | +| (10,8) | 18 | 4 | 10 | 8 | +| (9,9) | 18 | 4 | 9 | 9 | +| (11,6) | 17 | 5 | 7 | 1 | +| (10,7) | 17 | 5 | 3 | 3 | + +Here revisits count `22-|P|` among `q_0,...,q_21`, excluding the mandatory final +return. Only `(11,11)` forces a simple cycle; all other representatives require +revisits. `(9,8)` passes time and both budgets but has `B=1, need=4`, so the +identity excludes it. `(11,6)` and `(10,7)` remain in the acceptance domain: +**no #2773/#2870 17-point exclusion is imported**. + +## Receipt binding, controls and inherited guarantees + +The adapter first authenticates every live source byte against both SHA256 and +Git blob pins. It parses JSON with duplicate-key rejection. It imports no old +Python helper and launches no subprocess; source closure therefore does not +silently depend on those helpers' imports or runtime-generated artifacts. +The fixed `n=7, L=22` interpretation is inherited from the exact authenticated +source context; these are not parameter fields read from either census receipt. + +From the authenticated #3818 receipt it records each original completion state. +A capped row is never promoted to complete by changing its flags. At the semantic +boundary it checks strict Boolean completion, exclusion-flag consistency, zero +hits, recorded count types, the global depth-four prefix inventory and cap +consistency where recorded. Its four completed splits are +`(9,9), (10,8), (11,7), (11,8)`. Among those four, only `(9,9)` records +`shards_recorded=15` and `capped_shards=[]`. The other three are `source:control` +unsharded runs without `shards_recorded` or `capped_shards` fields. The global +depth-four inventory does not establish individual shard evidence for those +three rows, and their recorded `sharded_nodes` fields do not supply shard logs. + +For the deep receipt it independently generates restricted-growth words over +seven labels: 203 depth-six prefixes, replacing `012345` by its 49 depth-eight +extensions, yielding 251 entries. Every depth-eight restricted-growth word must +have exactly one cover prefix. It requires the recorded cover metadata, exact +ordered per-shard keys, nonnegative integer counts, total equality, strict +`complete=true`, zero hits and empty hit-word arrays on all seven deep rows. +The deep receipt's engine hash explicitly covers these seven deep rows and must +agree with the actual engine bytes, the new manifest and #4221's unchanged +manifest. The prior receipt has no engine hash: its same-engine provenance rests +on retained history, not an authenticated runtime engine field. Finally the +deep keys must equal **derived domain minus prior completed keys**, not merely +contain some claimed remainder. + +Controls operate on deep copies of the **actual authenticated receipts**. They +require positive acceptance of the original pair and reversed split-row order, +then rejection of: + +- each of the eleven individual admissible-row omissions; +- duplicate deep and predecessor rows, and duplicate JSON member names; +- incomplete deep rows, truthy non-Boolean completion, false predecessor + incompletion, and a capped predecessor falsely marked complete with its + exclusion/cap fields changed consistently; +- positive hits in either receipt and hidden hit words despite a zero hit count; +- an unexpected `(9,8)` row; +- a narrowed domain alone, and a co-mutated domain **and actual receipt** removing + both 17-point rows (an imported-exclusion-shaped mutant); +- a missing shard, wrong total, negative shard count, changed engine identity, + omitted cover entry and overlapping cover prefix. + +These controls run through the real acceptance adapter, with reason-checked +rejections. They cannot pass just because a generic parser crashes or an +always-rejecting adapter rejects everything. Explicit exceptions, not `assert`, +enforce all obligations under normal Python and `-O`. + +| Boundary | Added or preserved here | Not discharged here | +|---|---|---| +| Domain arithmetic | Independently reimplement credited #3708 arithmetic for eleven pre-import rows, compare all row fields, classify revisits | Formal necessity/rotation proof; realizability of any admitted split; `n=7,L=22` inherited from authenticated source context, not receipt fields | +| Receipt acceptance | Exact partition, unique split identity, completion/hit rejection | Fresh completion of any census process | +| Deep sharding | Independent 251-prefix partition, per-shard keys, integer totals | Raw shard logs, engine traversal/pruning correctness | +| Engine identity | Hash exact unchanged C source; compare #4221 manifest and engine hash covering seven deep rows | Prior receipt has no engine hash; its same-engine provenance is retained history, not a runtime field; no compilation, independent engine or giant replay | +| Historical predecessor totals | Authenticate recorded bytes and check count types; `(9,9)` records 15 shards, three other completed rows are unsharded controls | No individual shard evidence for `(10,8), (11,7), (11,8)`; global depth-four inventory does not supply it | +| Theorem/frontier | No altered source, selected kappa, tariff or supplier | New `f(7)=24` proof, formal kernel certificate or multiplication theorem | + +In particular the deep aggregate receipt records one completion flag per split, +not raw per-shard completion/exit logs. Authentication preserves that historical +claim; this adapter does not invent missing logs. Balanced changes to counts and +totals are excluded by source authentication, not by arithmetic total checks +alone. Recorded cover sums repeat prefix nodes across shards; they must not be +compared with differently sharded or unsharded counts as though identical. + +## Reproduction + +From the repository root, using CPython 3.12 (observed: 3.12.13): + +```sh +python3.12 -I -B research/f7-l22-receipt-domain/verify.py --emit +python3.12 -I -B -O research/f7-l22-receipt-domain/verify.py +python3.12 -B scripts/research_package.py --package research/f7-l22-receipt-domain --check-only +python3.12 -B scripts/research_package.py --package research/f7-l22-receipt-domain +``` + +The first two commands are the registered bounded replays; metadata validation +(`--check-only`) and invocation of both registered commands through +`scripts/research_package.py` passed on 2026-10-22 under CPython 3.12.13. +The observed marker from each replay was: + +```text +PASS_F7_L22_RECEIPT_DOMAIN domain=11 prior=4 deep=7 controls=30 no_census_replay +``` + +`--emit` printed deterministic derived rows, receipt partition, +`recorded_deep_nodes=173808188827` and names of rejected controls. That count +comes from recorded census receipts; no census nodes were executed. All source +inputs are read-only and the adapter creates no files. Normal and optimized +replays each have a 30-second manifest timeout. The orchestrator reported +1.13 seconds for the combined shell command including environment setup and +metadata validation; this is **not a precise adapter benchmark**. These are +orchestrator replay receipts, not contributor-run checks. The completed read-only +AI review is separate evidence, with no reviewer execution and no human or formal +endorsement. + +## Open next questions + +The structured questions and blockers are also in `TASK.json`. + +1. **Can an independent engine reproduce the seven deep exclusions?** This would + address the single-engine dependency that no receipt adapter removes. First + separately scope lifting #3005's `L<=20` C++ gate, then compare one split + shard-by-shard. Blockers: explicit compute authorization, extension review and + unknown length-22 throughput; this is not an instruction to run it here. +2. **Can a proof kernel check the pair-identity necessity and rotation quotient?** + Exact finite arithmetic does not formalize the universal-walk implication. + First formalize the four-cycle double-counting identity and one-step rotation. + Blocker: a separately scoped formal model and proof-assistant contribution. + +## Attribution and license + +Nick Petalas's #4221 deep census, #3708 split-domain work and #3005/#3731/#3818 +union-budget/census lineage are the direct predecessors; the existing source +notices remain unchanged. Retain Ross Richardson's PR943 prefix-walk model, +Aaron Wang's PR2542/PR2634 word-model contributions, and Nicholas Stone's #2973 +corrected Hamming-weight-parity engine and calibration. The historical 17-point +line #2773/#2870 is credited in predecessor sources to Aaron Wang / `navinor`; +its exclusions are not dependencies of this adapter. Douglas Colkitt's source +binding, package registration and review conventions are retained. + +This user-authorized contribution was prepared with substantial OpenAI Astra +assistance in code, controls and prose. Internal source inspection is not an +independent human review. Apache-2.0; no predecessor attribution is replaced. diff --git a/research/f7-l22-receipt-domain/SOURCES.json b/research/f7-l22-receipt-domain/SOURCES.json new file mode 100644 index 0000000000..64c27bf345 --- /dev/null +++ b/research/f7-l22-receipt-domain/SOURCES.json @@ -0,0 +1,79 @@ +{ + "schema_version": 1, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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-l22-deep-shard-census/verify.py", + "usage": "input", + "git_blob": "8f3b0e68ffb546fddb7f96d1fc565369291b1b71", + "sha256": "fa35dc13d0ad60f3ca29c2aa1283cda3e98b9be3aa3461d3731e8e2c2c61fa06" + }, + { + "path": "research/f7-l22-deep-shard-census/README.md", + "usage": "input", + "git_blob": "073e240af36bdd9ecf3ba5b7ab7bf6f1d3f933fc", + "sha256": "abc753bb54116e2ab5d65a1aae952a694766860f93115c63ea08152eddca68ec" + }, + { + "path": "research/f7-l22-deep-shard-census/RESULT.json", + "usage": "input", + "git_blob": "baf89975f1e7821ad37c952a234801092f37de8d", + "sha256": "a50770ce1c7de12438c0463bc2d2d47bbabfddfa9b3a0ec76bb60bdbf5b320ea" + }, + { + "path": "research/f7-l22-deep-shard-census/SOURCES.json", + "usage": "input", + "git_blob": "2b613280d67f03f233d564c4d11959c1ba0b8455", + "sha256": "b89052c91f341eb770fa0d1eb9c1284400310e9f7c11da76abb5d39dc2f58e7f" + }, + { + "path": "research/f7-l22-deep-shard-census/deep_census.py", + "usage": "input", + "git_blob": "ad980727381fe15ec3ac32991ded97fbbef403a0", + "sha256": "9a63bed90a4ea0e1254bdd43fd35b0d4a846f71c1ad2feb7ae166e8a2082b690" + }, + { + "path": "research/f7-l22-split-domain/verify.py", + "usage": "input", + "git_blob": "f68198ffe1338dc44b95c0431aa8f62d3bc34da9", + "sha256": "71e0035e7bb4a072a93b8b4ca4d0b7f5d4c7d03b8cd77e6d2cef4126cba6a0dc" + }, + { + "path": "research/f7-l22-split-domain/README.md", + "usage": "input", + "git_blob": "949fcf03f5d59fae90d26f5dca44c597d920d9ab", + "sha256": "d503e26c0d3bcbf09c66c0e4ff689382717e1c1c5b67cc98923394173a26a9b5" + }, + { + "path": "research/f7-l22-split-domain/RESULT.json", + "usage": "input", + "git_blob": "752456d73f7fba700796b3271d847f0e7fdf4d5f", + "sha256": "43b662bb27f6140dd1cfa23704f87c527f8dbd9aaa60256fb899a534a21598fa" + }, + { + "path": "research/f7-l22-union-census/RESULT.json", + "usage": "input", + "git_blob": "e845a493dbedb7556658a1f05e7f3d5b8652ecac", + "sha256": "292277ff25d6c63f2443b65aa2f6955d35beb116b0984a5457a1a8fa82633533" + }, + { + "path": "research/f7-l22-union-census/engine/union_census.c", + "usage": "input", + "git_blob": "b2742d3f711b468b287acb3fb65e8d27938e448f", + "sha256": "d34a322fc6c9fd41bc9dae337d3e84923f9dfb938c1af42de491cf536fe3cabe" + } + ], + "notes": "All pins resolve at the package base; no unmerged PR head is required. PR #4221 head 9d21222c67ecd40f49935a1e56b11f2b50d54613 and PR #3708 head ba1aff20ee3ce3dce35e4978feab0b6be08c7168 are attribution/context, not additional Git source dependencies." +} diff --git a/research/f7-l22-receipt-domain/TASK.json b/research/f7-l22-receipt-domain/TASK.json new file mode 100644 index 0000000000..9af604c77e --- /dev/null +++ b/research/f7-l22-receipt-domain/TASK.json @@ -0,0 +1,108 @@ +{ + "schema_version": 1, + "task_id": "census-pruning-audit", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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 reimplement the credited #3708 arithmetic for the eleven pre-import n=7,L=22 parity representatives from time, odd-budget, even-budget and pair-identity conditions; the even-budget condition is redundant at L=22 when the identity-bound check is enforced, not a fourth separately load-bearing control. Bind the exact completed predecessor/deep receipts to that domain with duplicate, omission, false completion, positive-hit and narrowed-domain rejection. Independent acceptance adapter only: no census replay, engine import or compilation. Fixed n=7,L=22 is inherited from exact authenticated source context, not parameter fields read from the receipts.", + "scope_change_reason": "This is the downstream dependency-audit variation of the card and directly answers #4221 Open next question 2. The predecessor receipt checker trusts a static DOMAIN and silently overwrites duplicate split keys. The corrected engine is unchanged; the repair is the exact acceptance-domain-to-receipt boundary, not another prune or a new f(7) proof.", + "bottleneck_link": "An unsound exclusion can wrongly close a mechanism; correcting its dependency boundary is more useful than extending the same census. No supplier, tariff, selected frontier or kappa changes; selected conditional kappa remains 0.00302015.", + "budget_minutes": 60, + "stop_rule": "Stop at a five-file standalone arithmetic/receipt adapter and source-bound handoff; reject any discrepancy without changing frozen pins. No compilation, large census, publication, commits or selected-frontier changes. Bounded metadata validation and registered normal/-O replay are the execution boundary.", + "outcome": "completed", + "evidence_status": "author-checked/orchestrator-replayed", + "evidence": "Completed scoped acceptance adapter. On 2026-10-22 the orchestrator observed CPython 3.12.13 metadata validation and registered normal/-O replays pass, each with PASS_F7_L22_RECEIPT_DOMAIN domain=11 prior=4 deep=7 controls=30 no_census_replay. Emitted recorded_deep_nodes=173808188827 is an authenticated historical count, not executed census nodes. Combined shell time was 1.13 seconds including setup and metadata, not a precise adapter benchmark. Read-only immutable Git source extraction and standard hashes found all twelve source working files equal to base objects. No contributor-run gates are claimed. Completed independent read-only AI review found no blocking mathematical or acceptance defect; the reviewer performed no execution. No independent human review, formal verification or scientific endorsement, new theorem or selected-frontier change is claimed.", + "author": "User-authorized Astra research contribution", + "ai_assistance": "Substantial OpenAI Astra assistance wrote the new adapter, controls, proof explanation and package metadata. No independent human or formal-kernel review is claimed.", + "overlap": { + "checked_at": "2026-10-22T19:49:40Z", + "source": "Final local overlap intake with complete remote pagination", + "open_prs": 299, + "open_prs_snapshot_at": "2026-10-22T19:49:07Z", + "discussion_records": 3721, + "discussion_snapshot_at": "2026-10-22T19:49:40Z", + "local_notes": 5860, + "additional_new_package_notes": 2, + "canonical_refresh": "624de9dc66858af0945e5f8a0942488d62280d43", + "base_pin_status": "Guidance, catalogue, selected record and all source packages unchanged relative to the pinned scientific base. Original base and card pins retained.", + "finding": "Exact phrase searches found predecessor/own-note references only; no novelty proof, arbitrary-diff search or exhaustive search of closed remote PRs. All tracked local notes were covered. Work is local-only; no public Discussion claim is asserted." + }, + "boundary_obligation_ledger": [ + { + "boundary": "Necessary-condition domain", + "discharged_by_artifact": "Independent arithmetic reimplementation of credited #3708 mathematics and comparison with all eleven pre-import rows; only (11,11) permits a simple cycle. The even-budget condition is redundant at L=22 when the identity-bound check is enforced; four stated conditions are not four separately load-bearing controls.", + "remaining": "Written necessity and rotation proofs are inherited, not formalized; n=7,L=22 comes from exact authenticated source context, not receipt parameter fields. Bounded arithmetic and controls were orchestrator-replayed; completed read-only AI review found no blocking mathematical or acceptance defect, with no reviewer execution or human/formal endorsement." + }, + { + "boundary": "Completed-receipt partition", + "discharged_by_artifact": "Four authenticated completed predecessor splits plus seven deep splits must partition the derived eleven; no 17-point import.", + "remaining": "Receipt flags and counts are historical evidence, not freshly enumerated words. Among the four completed prior rows, only (9,9) records shards_recorded=15 and capped_shards=[]. The (10,8), (11,7), (11,8) rows are source:control unsharded runs without shards_recorded or capped_shards; neither the global depth-four inventory nor their sharded_nodes fields establish individual shard evidence." + }, + { + "boundary": "Shard/engine binding", + "discharged_by_artifact": "Generated restricted-growth prefix cover, every deep shard key and integer total, zero-hit/completion fields, and an engine hash explicitly covering the seven deep rows, compared with exact engine bytes and #4221's manifest pin.", + "remaining": "The prior receipt has no engine hash; its same-engine provenance rests on retained history, not an authenticated runtime engine field. No raw per-shard completion logs in the deep aggregate receipt; engine pruning soundness, process exit history and full census remain inherited." + }, + { + "boundary": "Production theorem/frontier", + "discharged_by_artifact": "No production or selected record edits.", + "remaining": "No new kappa, no newly proved f(7)=24, no supplier or multiplication-theorem admission." + } + ], + "open_questions": [ + { + "question": "Can an independent engine reproduce the seven deep length-22 exclusions?", + "why_it_matters": "This adapter authenticates recorded counts; it cannot remove dependence on one census engine and its pruning proofs.", + "first_step": "Separately budget and audit lifting the #3005 C++ engine L<=20 gate, then compare one split shard-by-shard with #4221.", + "blocked_by": "An explicit resource budget, engine extension review, and measured length-22 throughput; no giant replay is authorized here." + }, + { + "question": "Can the pair-identity necessity and rotation quotient be checked in a proof kernel?", + "why_it_matters": "The finite arithmetic reimplementation is exact but still credits and inherits #3708's written implication from universal prefix walks to four necessary conditions; the even-budget condition is redundant at L=22 when the identity-bound check is enforced.", + "first_step": "Formalize the four-cycle double-counting identity sum_y C(r_y,2)=2 sum_x A_x B_x and one-step rotation of a restored walk.", + "blocked_by": "A separately scoped formalization task and formal model; no proof assistant or environment setup is included here." + } + ] +} diff --git a/research/f7-l22-receipt-domain/VERIFY.json b/research/f7-l22-receipt-domain/VERIFY.json new file mode 100644 index 0000000000..cb4beff297 --- /dev/null +++ b/research/f7-l22-receipt-domain/VERIFY.json @@ -0,0 +1,63 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/f7-l22-deep-shard-census/verify.py", + "research/f7-l22-deep-shard-census/README.md", + "research/f7-l22-deep-shard-census/RESULT.json", + "research/f7-l22-deep-shard-census/SOURCES.json", + "research/f7-l22-deep-shard-census/deep_census.py", + "research/f7-l22-split-domain/verify.py", + "research/f7-l22-split-domain/README.md", + "research/f7-l22-split-domain/RESULT.json", + "research/f7-l22-union-census/RESULT.json", + "research/f7-l22-union-census/engine/union_census.c" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "--emit" + ], + "timeout_seconds": 30, + "checks": "Authenticate all live inputs; independently reimplement credited #3708 arithmetic and compare eleven pre-import rows; classify revisits; regenerate the deep prefix partition; bind exact four-prior/seven-deep completion coverage and zero hits; check deep shard totals and engine hash covering seven deep rows; check prior global depth-four inventory and recorded count/cap fields without asserting individual shard evidence for its three unsharded control rows; reject actual-receipt mutants and require positive acceptance." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Repeat all acceptance and mutation controls under -O, ensuring fail-closed checks do not depend on assert." + } + ], + "evidence_status": "author-checked/orchestrator-replayed", + "replay_evidence": { + "date": "2026-10-22", + "python": "CPython 3.12.13", + "metadata_validation": "passed", + "registered_normal_replay": "passed", + "registered_optimized_replay": "passed", + "observed_marker": "PASS_F7_L22_RECEIPT_DOMAIN domain=11 prior=4 deep=7 controls=30 no_census_replay", + "recorded_deep_nodes": 173808188827, + "count_scope": "Authenticated historical receipt count, not census nodes executed by this adapter.", + "timing_scope": "Orchestrator reported 1.13 seconds for the combined shell command including environment setup and metadata validation; not a precise adapter benchmark.", + "review_scope": "Completed independent read-only AI review found no blocking mathematical or acceptance defect. The reviewer performed no execution. No independent human review, formal verification or scientific endorsement is claimed." + }, + "evidence_limits": { + "arithmetic": "Independent arithmetic reimplementation of credited #3708 mathematics, not an independent discovery or formal necessity proof. At L=22 the even-budget condition is redundant when the identity-bound check is enforced; four stated necessary conditions are not four separately load-bearing controls.", + "parameters": "Fixed n=7,L=22 is inherited from exact authenticated source context, not parameter fields read from either census receipt.", + "engine": "The engine hash explicitly covers the seven deep rows and is compared with exact engine bytes and #4221's manifest. The prior receipt has no engine hash; same-engine provenance for its rows rests on retained history, not an authenticated runtime engine field.", + "prior_shards": "Among the four completed prior rows, only (9,9) records shards_recorded=15 and capped_shards=[]. The (10,8), (11,7), (11,8) rows are source:control unsharded runs without shards_recorded or capped_shards. The global depth-four prefix inventory and their sharded_nodes fields do not assert individual shard evidence for these three rows.", + "historical_counts": "The eleven-row domain remains partitioned into four prior and seven deep completed rows, with 30 adapter controls. Recorded deep nodes are authenticated historical counts, not newly enumerated nodes; aggregate receipts do not supply raw per-shard completion/exit logs." + }, + "notes": "Ready denotes registered replay commands; their observed outcomes are recorded above. Standard library only, no subprocesses, imports of predecessor helpers, compiler, network, word census or writes. Only retained input bytes are read. Catalogue and selected record are Git provenance, not live inputs. The completed outcome covers only the scoped acceptance adapter: no new census, theorem, kappa or selected-frontier change. No contributor-run gates are claimed." +} diff --git a/research/f7-l22-receipt-domain/verify.py b/research/f7-l22-receipt-domain/verify.py new file mode 100755 index 0000000000..bad0b4eed0 --- /dev/null +++ b/research/f7-l22-receipt-domain/verify.py @@ -0,0 +1,485 @@ +#!/usr/bin/env python3 +"""Source-bound domain/receipt adapter; never imports or executes census engines. + +Prepared with OpenAI Astra assistance. Predecessors: Nick Petalas (#4221, +#3708), the #3818 union census, and the attributed PR943 word-model lineage. +Apache-2.0. Runtime evidence is emitted only when this command is executed. +""" + +from __future__ import annotations + +import argparse +import hashlib +import json +import sys +from copy import deepcopy +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +DEEP = "research/f7-l22-deep-shard-census/" +DOMAIN = "research/f7-l22-split-domain/" +PRIOR = "research/f7-l22-union-census/" +ENGINE = PRIOR + "engine/union_census.c" +INPUTS = ( + DEEP + "verify.py", + DEEP + "README.md", + DEEP + "RESULT.json", + DEEP + "SOURCES.json", + DEEP + "deep_census.py", + DOMAIN + "verify.py", + DOMAIN + "README.md", + DOMAIN + "RESULT.json", + PRIOR + "RESULT.json", + ENGINE, +) + + +class Rejected(ValueError): + """A failed acceptance obligation, also active under python -O.""" + + +def require(condition, message): + if not condition: + raise Rejected(message) + + +def expect_rejected(label, action, reason): + try: + action() + except Rejected as error: + require(reason in str(error), f"{label}: wrong rejection: {error}") + return label + raise Rejected(f"control survived: {label}") + + +def controls(prior, deep, domain, trusted_status, engine_hash, keys): + """Mutate actual loaded receipts, not invented one-row success fixtures.""" + rejected = [] + + def exercise(label, change, reason): + p, d, requested = deepcopy(prior), deepcopy(deep), set(domain) + change(p, d, requested) + rejected.append( + expect_rejected( + label, + lambda: bind_receipts( + p, d, requested, trusted_status, engine_hash, keys + ), + reason, + ) + ) + + # Positive acceptance is mandatory; an always-rejecting adapter fails here. + bind_receipts(prior, deep, domain, trusted_status, engine_hash, keys) + p, d = deepcopy(prior), deepcopy(deep) + p["probes"].reverse() + d["splits"].reverse() + bind_receipts(p, d, domain, trusted_status, engine_hash, keys) + + for split in sorted(domain): + target = ( + "deep" + if any(tuple(r["split"]) == split for r in deep["splits"]) + else "prior" + ) + + def omit(p, d, requested, split=split, target=target): + rows = d["splits"] if target == "deep" else p["probes"] + rows[:] = [r for r in rows if tuple(r["split"]) != split] + + exercise(f"omit-{split}", omit, "coverage") + + exercise( + "duplicate-deep", + lambda p, d, q: d["splits"].append(deepcopy(d["splits"][0])), + "duplicate split", + ) + exercise( + "duplicate-prior", + lambda p, d, q: p["probes"].append(deepcopy(p["probes"][0])), + "duplicate split", + ) + exercise( + "deep-incomplete", + lambda p, d, q: d["splits"][0].update(complete=False), + "deep completion", + ) + exercise( + "truthy-completion", + lambda p, d, q: d["splits"][0].update(complete=1), + "deep completion", + ) + exercise( + "prior-false-incomplete", + lambda p, d, q: p["probes"][0].update(complete=False), + "recorded completion", + ) + + def false_complete(p, d, requested): + row = next(r for r in p["probes"] if r["complete"] is False) + row.update(complete=True, finite_split_exclusion=True, capped_shards=[]) + + exercise("prior-false-complete", false_complete, "recorded completion") + exercise( + "deep-positive-hit", + lambda p, d, q: d["splits"][0].update(hits=1, hit_words=["01021323"]), + "hits", + ) + exercise( + "prior-positive-hit", lambda p, d, q: p["probes"][0].update(hits=1), "hits" + ) + exercise( + "hidden-hit-word", + lambda p, d, q: d["splits"][0].update(hit_words=["01021323"]), + "hits", + ) + exercise( + "unexpected-split", + lambda p, d, q: d["splits"][0].update(split=[9, 8]), + "unexpected split", + ) + exercise( + "narrowed-domain-only", lambda p, d, q: q.discard((11, 6)), "derived domain" + ) + + def narrow_both(p, d, requested): + requested.difference_update({(11, 6), (10, 7)}) + d["splits"][:] = [r for r in d["splits"] if sum(r["split"]) != 17] + + exercise("narrowed-domain-and-receipts", narrow_both, "derived domain") + exercise( + "missing-shard", + lambda p, d, q: d["splits"][0]["per_shard_nodes"].pop(keys[0]), + "shard keys", + ) + exercise( + "wrong-total", + lambda p, d, q: d["splits"][0].update(nodes=d["splits"][0]["nodes"] + 1), + "node total", + ) + exercise( + "negative-node", + lambda p, d, q: d["splits"][0]["per_shard_nodes"].update({keys[0]: -1}), + "node count", + ) + exercise("wrong-engine", lambda p, d, q: d.update(engine_sha256="0" * 64), "engine") + rejected.append( + expect_rejected("omitted-cover", lambda: check_cover(keys[:-1]), "partition") + ) + rejected.append( + expect_rejected( + "overlapping-cover", lambda: check_cover(keys + ["0123456"]), "partition" + ) + ) + rejected.append( + expect_rejected( + "duplicate-json-key", + lambda: load_json('{"split": [11,6], "split": [10,7]}'), + "duplicate JSON key", + ) + ) + return rejected + + +def unique_object(pairs): + result = {} + for key, value in pairs: + require(key not in result, f"duplicate JSON key: {key}") + result[key] = value + return result + + +def load_json(text): + return json.loads(text, object_pairs_hook=unique_object) + + +def authenticate_inputs(): + sources = load_json((PACKAGE / "SOURCES.json").read_bytes()) + live = [r for r in sources["files"] if r["usage"] == "input"] + require( + len(live) == len(INPUTS) and {r["path"] for r in live} == set(INPUTS), + "live input inventory differs from the adapter contract", + ) + payloads = {} + for row in live: + payload = (ROOT / row["path"]).read_bytes() + require( + hashlib.sha256(payload).hexdigest() == row["sha256"], + "source SHA256 mismatch: " + row["path"], + ) + header = f"blob {len(payload)}\0".encode("ascii") + require( + hashlib.sha1(header + payload).hexdigest() == row["git_blob"], + "source Git blob mismatch: " + row["path"], + ) + payloads[row["path"]] = payload + return payloads + + +def arithmetic(s, t): + """Four necessary conditions at n=7, L=22; no set-level imports.""" + budget = s * (s - 1) // 2 + t * (t - 1) // 2 - 63 + need = max(0, (s * t - 64 + 1) // 2) + upper = budget + budget * budget // 4 if budget >= 0 else budget + return { + "split": [s, t], + "points": s + t, + "revisits_forced": 22 - s - t, + "even_budget": budget, + "identity_need": need, + "identity_max_upper": upper, + "odd_pairs": s * t, + }, (s <= 11 and t <= 11, s * t >= 64, budget >= 0, upper >= need) + + +def derive_domain(): + # A prefix set has at most L distinct positions. The deliberately wider + # range exercises the time condition rather than building it into a table. + rows = [] + for s in range(1, 23): + for t in range(1, s + 1): + row, conditions = arithmetic(s, t) + if all(conditions): + rows.append(row) + return sorted(rows, key=lambda r: (-r["points"], -r["split"][0])) + + +def check_domain(record): + rows = derive_domain() + require( + rows == record["split_domains"]["22"], "pre-import arithmetic rows disagree" + ) + require( + [r["split"] for r in rows] == record["length_22_self_contained"], + "pre-import representatives disagree", + ) + require(len(rows) == 11, "expected eleven independently derived representatives") + domain = {tuple(r["split"]) for r in rows} + require({(11, 6), (10, 7)} <= domain, "17-point import leaked into derivation") + simple = [r["split"] for r in rows if r["points"] == 22] + require( + simple == [[11, 11]] == record["length_22_simple_cycle_admissible"], + "self-avoidance classification", + ) + revisits = {str(tuple(r["split"])): r["revisits_forced"] for r in rows} + require(revisits == record["length_22_revisits_forced"], "revisit classification") + row, conditions = arithmetic(9, 8) + require( + conditions == (True, True, True, False) + and row["even_budget"] == 1 + and row["identity_need"] == 4, + "(9,8) must fail only the identity", + ) + require(not arithmetic(12, 6)[1][0], "time condition is not active") + require(not arithmetic(8, 8)[1][2], "even-budget condition is not active") + require(not arithmetic(11, 5)[1][1], "odd-budget condition is not active") + require( + arithmetic(11, 11)[0]["identity_need"] == 29, + "odd excess 57 must round up, not down", + ) + # Independently optimize over integer a+b<=B, rather than repeating B^2//4. + for budget in range(48): + best = max(a * b for a in range(budget + 1) for b in range(budget - a + 1)) + require(best == budget * budget // 4, "integer identity maximization") + return rows, domain + + +def growth_words(depth): + words = [""] + for _ in range(depth): + words = [ + word + str(label) + for word in words + for label in range(min(7, max(map(int, word), default=-1) + 2)) + ] + return words + + +def make_cover(): + extensions = [w for w in growth_words(8) if w.startswith("012345")] + base = growth_words(6) + require(len(base) == 203 and len(extensions) == 49, "cover construction") + return [ + key + for prefix in base + for key in (extensions if prefix == "012345" else [prefix]) + ] + + +def check_cover(keys): + require(len(keys) == len(set(keys)), "duplicate cover prefix") + require(all(1 <= len(key) <= 8 for key in keys), "cover partition depths") + words = growth_words(8) + require( + all(any(word.startswith(key) for word in words) for key in keys), + "cover partition contains invalid prefix", + ) + for word in words: + require( + sum(word.startswith(key) for key in keys) == 1, + "cover partition missing or overlapping at " + word, + ) + + +def index_splits(rows): + require(type(rows) is list, "split rows must be a list") + indexed = {} + for row in rows: + split = row["split"] + require( + type(split) is list + and len(split) == 2 + and all(type(v) is int for v in split), + "invalid split", + ) + key = tuple(split) + require(key not in indexed, f"duplicate split: {key}") + indexed[key] = row + return indexed + + +def nonnegative_integer(value): + return type(value) is int and value >= 0 + + +def bind_receipts(prior, deep, requested_domain, trusted_status, engine_hash, keys): + # Re-derive at the acceptance boundary: even a domain+receipt co-mutation + # cannot turn exact coverage into coverage of a caller-selected subset. + domain = {tuple(r["split"]) for r in derive_domain()} + require(requested_domain == domain, "requested domain differs from derived domain") + p = index_splits(prior["probes"]) + d = index_splits(deep["splits"]) + require(set(p) <= domain and set(d) <= domain, "unexpected split") + require(set(p) == set(trusted_status), "predecessor coverage changed") + require( + prior["shard_depth"] == 4 and prior["shard_prefixes"] == growth_words(4), + "predecessor shard coverage", + ) + complete = set() + for split, row in p.items(): + require( + type(row["complete"]) is bool and row["complete"] is trusted_status[split], + f"{split}: recorded completion changed", + ) + require( + row["finite_split_exclusion"] is row["complete"], + f"{split}: inconsistent exclusion flag", + ) + require(type(row["hits"]) is int and row["hits"] == 0, f"{split}: prior hits") + require(nonnegative_integer(row["sharded_nodes"]), "prior node count") + if "shards_recorded" in row: + require(row["shards_recorded"] == 15, "prior shard coverage") + if row["complete"]: + require( + not row.get("capped_shards", []), "complete prior has capped shards" + ) + require( + nonnegative_integer(row["unsharded_nodes"]), + "prior unsharded node count", + ) + complete.add(split) + else: + capped = row["capped_shards"] + require( + capped + and len(capped) == len(set(capped)) + and set(capped) <= set(prior["shard_prefixes"]), + "prior capped coverage", + ) + require( + deep["engine"] == ENGINE and deep["engine_sha256"] == engine_hash, + "receipt engine identity", + ) + require( + deep["base_depth"] == 6 + and deep["cover_size"] == 251 + and deep["expanded"] == {"012345": 8}, + "deep cover metadata", + ) + for split, row in d.items(): + require(row["complete"] is True, f"{split}: deep completion") + require( + type(row["hits"]) is int and row["hits"] == 0 and row["hit_words"] == [], + f"{split}: deep hits", + ) + require( + row["shards"] == 251 and list(row["per_shard_nodes"]) == keys, + f"{split}: shard keys differ", + ) + counts = row["per_shard_nodes"].values() + require( + all(nonnegative_integer(n) for n in counts), f"{split}: invalid node count" + ) + require( + nonnegative_integer(row["nodes"]) and sum(counts) == row["nodes"], + f"{split}: node total", + ) + require( + set(d) == domain - complete, + "deep coverage must equal derived domain minus prior complete", + ) + require( + not (set(d) & complete) and complete | set(d) == domain, + "completed receipt coverage is not an exact partition", + ) + return { + "prior_complete": sorted(complete), + "deep_complete": sorted(d), + "recorded_deep_nodes": sum(row["nodes"] for row in d.values()), + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "--emit", + action="store_true", + help="print deterministic arithmetic and control details", + ) + args = parser.parse_args() + payloads = authenticate_inputs() + prior = load_json(payloads[PRIOR + "RESULT.json"]) + deep = load_json(payloads[DEEP + "RESULT.json"]) + record = load_json(payloads[DOMAIN + "RESULT.json"]) + old_sources = load_json(payloads[DEEP + "SOURCES.json"]) + engine_pins = [r for r in old_sources["files"] if r["path"] == ENGINE] + engine_hash = hashlib.sha256(payloads[ENGINE]).hexdigest() + require( + len(engine_pins) == 1 and engine_pins[0]["sha256"] == engine_hash, + "predecessor engine source guarantee", + ) + rows, domain = check_domain(record) + keys = make_cover() + check_cover(keys) + # These completion states come only from the authenticated original bytes; + # controls cannot make a capped run complete by changing both of its flags. + trusted_status = { + key: row["complete"] for key, row in index_splits(prior["probes"]).items() + } + summary = bind_receipts(prior, deep, domain, trusted_status, engine_hash, keys) + rejected = controls(prior, deep, domain, trusted_status, engine_hash, keys) + if args.emit: + print( + json.dumps( + { + "derived_rows": rows, + "binding": summary, + "rejected_controls": rejected, + "evidence_kind": "authenticated recorded counts; no census replay", + }, + indent=2, + sort_keys=True, + ) + ) + print( + f"PASS_F7_L22_RECEIPT_DOMAIN domain=11 prior=4 deep=7 controls={len(rejected)} no_census_replay" + ) + + +if __name__ == "__main__": + try: + main() + except (Rejected, KeyError, TypeError, ValueError, OSError) as error: + print(f"FAIL_F7_L22_RECEIPT_DOMAIN: {error}", file=sys.stderr) + sys.exit(1)