Record that the only emitted after-cover misses the PR5679 component.

research/g20-source-bound-cover-census/PROOF.md

@@ -0,0 +1,120 @@
+# Census: the emitted after-cover does not make ordinary equal C
+
+## Claim type
+
+This is an exhaustive finite census of one source field, plus the exact rational
+identity for the selected ordinary formula on that field. It is not a heuristic
+search, not an unrestricted nonexistence theorem, and not an admission verdict.
+
+## Hypotheses
+
+The selected conditional exponent stays **781451/250000000**. Nothing here
+changes `certificates/selected-result.json`.
+
+1. **Formula.** In `research/p104-helper470-twin-rung-removal/pricing.py` the
+   ordinary value is the single assignment
+
+        ordinary = (1 - atom) * Q(bit["after_cover"]) + atom * Q(".0000384599")
+
+   where `bit` is `ordinary_BIT` from
+   `research/query-thinned-controllers/RESULT.json` and
+   `atom = Q(bit["atom"])`. The same file sets `admitted = Q(bit["admitted"])`
+   and passes `bit_saving = admitted`. It never reads `ordinary_saving`.
+
+2. **Stock contract.** `research/query-thinned-controllers/PROOF.md` says to
+   keep one external cover weight, with `C0 = 0.003459` before covering and
+   `C1 = 0.00345` afterward. The controller verifier assigns that weight once:
+
+        before, after, atom, old = Q(".003459"), Q(".00345"), Q(".004"), Q(".0000384599")
+
+   and stores `after` as `after_cover`. The physical BIT word and
+   `controller.py` do not carry a second cover field.
+
+3. **Recorded component.** `C` is the top-level `admitted` value of
+   `research/g20-helper-split/ORDINARY-RESULT.json`,
+
+        C = 3507410738409/1000000000000000,
+
+   equal to that receipt's fifth finite level. The receipt has
+   `whole_kappa = null`. It is a component saving, not a selected exponent.
+
+A source-bound after-cover, under this contract, is a value of the single
+`ordinary_BIT.after_cover` field those bytes emit. A rational that does not
+appear there is not a source-bound cover for this formula, even if some other
+package records a different `C1`.
+
+## Census
+
+After the SHA256 and Git blob pins match, the receipt text contains the key
+`after_cover` once, spelled `69/20000`, at `ordinary_BIT.after_cover`. The
+controller verifier contains one writer of that key and one assignment of
+`after`. The proof contains one `C1 = 0.00345` sentence. The physical word has
+no `after_cover` key and neither cover literal. Therefore the emitted set is
+
+    { 69/20000 }.
+
+`Q(".00345")` equals that fraction, and `Q(".003459")` equals the separate
+before-cover field `3459/1000000`. The before-cover is the claim template
+named "BIT before cover". It is not the field the ordinary formula reads.
+
+The domain is finite because it is one parsed field written by one literal.
+The enumeration is complete because every pinned writer, stored key, and
+physical-word key was counted, and a second key, including a duplicate JSON
+key that a parser would collapse, is rejected by the text count. The controller
+program was not executed. The stored field and the writer literal were
+compared, and they are the same rational. A disagreement would have failed
+the census.
+
+## Arithmetic
+
+The pins give `atom = 1/250` and `epsilon = 384599/10000000000`. The slope
+
+    1 - atom = 249/250
+
+is positive, so the formula is injective in the cover. The emitted value
+reproduces the selected claim:
+
+    ordinary(69/20000) = 8590884599/2500000000000.
+
+The unique rational preimage of `C` is
+
+    (C - atom * epsilon) / (1 - atom) = 3507256898809/996000000000000.
+
+That preimage is not `69/20000`. The same identity gives
+
+    C - ordinary(69/20000) = 71056898809/1000000000000000 > 0.
+
+So the only emitted after-cover does not make the formula equal `C`, and there
+is no other emitted after-cover that could. The preimage numerator does not
+occur as a constant in the pinned controller, pricing, claim, or component
+files. This package does not write it into the controller.
+
+## What is outside the census
+
+The following rationals are recorded somewhere, and each fails the formula
+when substituted, but none of them is an emitted after-cover. They are
+controls, not extra census elements.
+
+- The before-cover `3459/1000000`.
+- PR5679's own cover `C1 = uniform - 1/10^14 = 350741073841/100000000000000`,
+  from `ordinary.py`, where the component formula is
+  `(1 - rho) * C1 + rho * backend` with `rho = 1/100`. That is not the
+  selected formula.
+- PR5708's receipt cover and the different preimage
+  `3507565220149/996000000000000` of its larger component. The odd-prime
+  question asked for that other preimage is not this census.
+
+The delayed-cover bridge's group fibers are not values of this scalar field
+and are not read by the formula.
+
+## What this does not say
+
+`ordinary(69/20000) ≠ C` is the statement that the emitted cover is not the
+preimage. It is not a new proof that `C` fails admission. The pricing still
+feeds `bit_saving = admitted = 17/5000` to the ledger. This note does not
+execute that ledger, does not replace `admitted` by `C` or by `ordinary`, and
+does not move κ.
+
+A cover the controller does not emit remains a changed stock contract. The
+odd-prime comparison at `3507256898809/996000000000000` was not run. A
+Gaussian caller outside this pricing assembly was not named or executed.

research/g20-source-bound-cover-census/README.md

@@ -0,0 +1,104 @@
+# The emitted after-cover does not make ordinary equal C
+
+**Exhaustive finite census. No new κ.** The selected conditional exponent stays
+**781451/250000000** (`0.003125804`).
+
+The selected ordinary formula reads one thinned-controller field,
+`ordinary_BIT.after_cover`. Under the controller's one-weight stock contract
+that field is only
+
+    69/20000.
+
+The formula is strictly increasing in the cover. The unique cover that would
+make it equal the recorded PR5679 component
+
+    C = 3507410738409/1000000000000000
+
+is
+
+    3507256898809/996000000000000.
+
+That rational is not emitted. The ordinary value at the emitted cover remains
+the selected claim `8590884599/2500000000000`, and
+
+    C - ordinary(69/20000) = 71056898809/1000000000000000 > 0.
+
+This identifies the preimage. It does not admit `C` as BIT and it does not
+change κ. The pricing passes `bit_saving = admitted = 17/5000`, not `ordinary`.
+
+## Scope
+
+Base commit `7c49fe32c55de02c2c873655c804b16e4c3fef0a` on canonical
+`CrocSwap/integer-mult-bounds` main. Priority revision 8. The live selected
+record, not the older κ quoted in `current-priorities.md`, supplies the
+exponent above. Catalogue card `supplier-boundary-audit`. Scope status:
+**refined**.
+
+The card asks for one resolved gap on a latest supplier candidate. The gap
+taken here is the cover field left open by the PR5679 stock-gate reading:
+read the thinned controller's cover before constructing one, then ask whether
+any emitted cover other than `69/20000` makes the selected formula equal `C`.
+The argument is in [PROOF.md](PROOF.md).
+
+Overlap recheck on 2026-11-10, after fetching canonical main at the base
+commit: 885 open upstream PR bodies and the discussion cache. The preimage
+numerator occurs in discussion
+[#1166 comment 19492491](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19492491)
+as an open question, and in no open upstream PR body. That comment's fork
+draft, PR 149, stops at the stock gate and does not census the cover field.
+`research/g20-component-stock-gate` asks the odd-prime question for the
+different PR5708 preimage `3507565220149/996000000000000`. No match is a
+novelty certificate. This package does not take the caller question and does
+not answer the odd-prime question.
+
+## Validation
+
+Environment: Python 3.12, standard library only. From the repository root:
+
+```sh
+python3 -B research/g20-source-bound-cover-census/verify.py
+python3 -O -B research/g20-source-bound-cover-census/verify.py
+python3 -B scripts/research_package.py --package research/g20-source-bound-cover-census
+```
+
+The verifier prints `PASS_G20_SOURCE_BOUND_COVER_CENSUS`. The launcher prints
+`PASS_REGISTERED_RESEARCH_PACKAGE` with outcome `negative-result`. Checks
+raise `SystemExit`, so `-O` does not disable them.
+
+Source hashes and Git blobs are checked before any scientific `Fraction`
+evaluation. The census counts the raw `after_cover` key, including a duplicate
+key a JSON parser would collapse. Controls reject an unbound call, a second
+nested key, and that duplicate key. The before-cover, PR5679's own `C1`, and
+PR5708's cover and preimage are substituted only as values outside the emitted
+set; none equals `C` under this formula, and none is added to the census.
+
+Not run: `scripts/research_selected_baseline.py`, the thinned-controller replay
+itself, the outer ledger, either component caller, native maps, the odd-prime
+rule at the missing preimage, Lean, Docker, and `make frontier6030-verify`.
+The cover is the source literal `Q('.00345')`, checked against the pinned
+receipt; it is not a value discovered by replaying the physical word.
+
+## Credit
+
+The component is Ali Romman's PR #5679, recorded in `research/g20-helper-split`.
+The selected pricing and claim are DreamingOfClouds' PR #6030. The one-weight
+cover contract is Cinna Davis's `research/query-thinned-controllers`. The
+PR5708 preimage question remains with `research/g20-component-stock-gate`.
+The stock-gate reading that left this cover field open is the predecessor
+package behind discussion comment 19492491.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+
+## Open next questions
+
+1. Can a changed thinned-controller contract that emits a second after-cover
+   make this formula equal `C` while keeping the one-weight delayed-cover
+   proof? The missing value is `3507256898809/996000000000000`. First step:
+   name a second source assignment to `after_cover` and authenticate it before
+   any arithmetic. Blocked by the single `C1` sentence and the single writer.
+   The odd-prime rule at that missing value was not run.
+2. Can a Gaussian caller that does not use this pricing assembly consume `C`?
+   First step: name that caller and the field it reads as `bit_saving`.
+   Blocked here because no such caller is identified. This package does not
+   take that question. Equality of `ordinary` with `C` would still leave this
+   assembly's `bit_saving` equal to `17/5000`.

research/g20-source-bound-cover-census/SOURCES.json

@@ -0,0 +1,78 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/frontier6030/CLAIM.json",
+      "usage": "input",
+      "git_blob": "f32ff3779274a349dc8af2e84a4c6234c6d62406",
+      "sha256": "9cee8a1304fa893be3d3b641eda42fdd9b2fd6a5ac2124fb891de7a1a5e8d92e"
+    },
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "input",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/g20-conjugation-admission/ORDINARY-RESULT.json",
+      "usage": "input",
+      "git_blob": "46308272ac871d5876406dbb59eb21f4035c3503",
+      "sha256": "3a379d5ba1e005ce57610d9a5954cce62f24939b7246bb785e76ff70f74c93fa"
+    },
+    {
+      "path": "research/g20-helper-split/ORDINARY-RESULT.json",
+      "usage": "input",
+      "git_blob": "bfe417c5cca5227714238c80d65700e3f6a2e8d8",
+      "sha256": "382ca0d6c763dd26e12cac2e490eb1ecd8d40f1a1501b0e059aacc04fe7528de"
+    },
+    {
+      "path": "research/g20-helper-split/ordinary.py",
+      "usage": "input",
+      "git_blob": "cb462e82c34237dc0ce1d761fef9097a175cd082",
+      "sha256": "a5783901f6de9428d257f661deb041705556c1f9ce75786afd311ae5484b4260"
+    },
+    {
+      "path": "research/p104-helper470-twin-rung-removal/pricing.py",
+      "usage": "input",
+      "git_blob": "65bb723f8558dc60ff92764db1a43d8bf438aa09",
+      "sha256": "3c6cf2966ccfe5a5fb6c90f89f46ac224ea455127e35dd34975683c68c36d710"
+    },
+    {
+      "path": "research/query-thinned-controllers/BIT-CONTROLLER.json",
+      "usage": "input",
+      "git_blob": "89c400d5970024b3debe870c36ce43889beed001",
+      "sha256": "39ac84fb848b908f7ba051fae4556d507900c421dc5d23501a9c0cb1d61fd08d"
+    },
+    {
+      "path": "research/query-thinned-controllers/PROOF.md",
+      "usage": "input",
+      "git_blob": "9068f429896112082664455ab00bab083c99d1d8",
+      "sha256": "5ade59641f2ed70d045d6f60e89db7d979b1d1e9967f3acbe5c56eac81312841"
+    },
+    {
+      "path": "research/query-thinned-controllers/RESULT.json",
+      "usage": "input",
+      "git_blob": "e0695152c98d727edfd0d2034b58a1c7e8682c0c",
+      "sha256": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f"
+    },
+    {
+      "path": "research/query-thinned-controllers/controller.py",
+      "usage": "input",
+      "git_blob": "d4557e08cfb9fe57cc1ae4024705a72dc95f3583",
+      "sha256": "8b462d660487b1be4940357c4c7522967b1bfaede3c02b1c66109b85acae0fd2"
+    },
+    {
+      "path": "research/query-thinned-controllers/verify.py",
+      "usage": "input",
+      "git_blob": "f1114036fff66f57014e5c1256141fb78ff4c4a9",
+      "sha256": "07dea601d6bbaa4d90e576f20c8607c37fb01e8778c798d919fa9df435049950"
+    }
+  ]
+}