Prove no second after-cover keeps the one-weight gap and equals C (no κ)

research/g20-second-after-cover-obstruction/PROOF.md

@@ -0,0 +1,142 @@
+# No second after-cover keeps the one-weight proof and hits C
+
+## Claim type
+
+This is a scoped proof. It is not an exhaustive census of every file that
+contains the string `after_cover`, not a heuristic search, and not an
+admission verdict. The selected conditional exponent stays
+**781451/250000000**. Nothing here changes `certificates/selected-result.json`.
+
+## What was authenticated before arithmetic
+
+Two source assignments were named and hash-bound before any `Fraction`
+evaluation.
+
+1. **The controller's only writer.** `research/query-thinned-controllers/verify.py`
+   contains one assignment
+
+        before, after, atom, old = Q('.003459'), Q('.00345'), Q('.004'), Q('.0000384599')
+
+   and stores `after` once under the key `after_cover`. The receipt spells
+   that field `69/20000`. `controller.py` contains neither the key nor the
+   literal. `PROOF.md` contains one sentence, "Keep one external cover weight
+   throughout the entire finite BIT compilation," and one C1 sentence,
+   "Use C0=0.003459 before covering and C1=0.00345".
+
+2. **The retained bridge's other after-cover weight.** The controller package
+   pins `research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md` and
+   `research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json` as inputs. It does
+   not pin the writer script. That script assigns
+
+        before, after = Q(69, 25000), Q(11, 4000)
+
+   and stores the second name as `C1_after_cover`, spelled `11/4000`. The
+   bridge prose states `C1=11/4000=0.00275` once. None of those three files
+   contains the key `after_cover`. The controller proof does not contain
+   `11/4000`.
+
+The selected formula, in `research/p104-helper470-twin-rung-removal/pricing.py`,
+is the single assignment
+
+    ordinary = (1 - atom) * Q(bit['after_cover']) + atom * Q('.0000384599')
+
+where `bit` is `ordinary_BIT` from the thinned-controller receipt. The same
+file passes `bit_saving = admitted`. It does not read `C1_after_cover`.
+
+The component is the top-level `admitted` value of
+`research/g20-helper-split/ORDINARY-RESULT.json`,
+
+    C = 3507410738409/1000000000000000,
+
+with `whole_kappa = null`.
+
+## Hypotheses kept
+
+A changed thinned-controller contract keeps the one-weight delayed-cover proof
+only when all four of the following remain true of that contract.
+
+- **(H-one)** There is one external cover weight, the sentence quoted above.
+- **(H-writer)** `after_cover` is written once, from the single assignment of
+  `after`.
+- **(H-C1)** That assignment is the single sentence `C1=0.00345`.
+- **(H-gap)** The verifier's gate `before > after` remains, and the proof's
+  comparison `256/(C0-C1)` remains a comparison across a positive denominator.
+  The recorded coefficient check is `2**26 > 256/(before-after)`.
+
+(H-one) and (H-writer) forbid a second stored `after_cover`. (H-C1) fixes the
+one stored value at `69/20000`. (H-gap) is the reason the algebraic preimage
+cannot be substituted for that value either.
+
+## Argument
+
+The pinned spellings give `atom = 1/250` and `epsilon = 384599/10000000000`.
+The slope `1 - atom = 249/250` is positive, so the formula is strictly
+increasing and injective in the cover. Its only solution of `ordinary = C` is
+
+    (C - atom * epsilon) / (249/250) = 3507256898809/996000000000000.
+
+The controller's before-cover is `C0 = 3459/1000000`. The same identity gives
+
+    preimage - C0 = 62092898809/996000000000000 > 0,
+
+so the preimage fails `before > after`. At that preimage the denominator
+`C0 - C1` is negative, and the proof's positive-gap comparison does not apply.
+No odd prime was tested there. The failure is the sign of the gap, not an
+incomplete search.
+
+The image of the kept gap is strictly below the component, not merely at the
+emitted point. Because the slope is positive,
+
+    ordinary(x) < ordinary(C0) for every rational x < C0,
+
+and
+
+    ordinary(C0) = 8613294599/2500000000000,
+    C - ordinary(C0) = 62092898809/1000000000000000 > 0.
+
+Thus every cover that keeps (H-gap) misses `C`. This is a proof about an
+infinite rational ray. It does not list the ray.
+
+The two named assignments both lie on that ray and both miss `C`:
+
+    ordinary(69/20000) = 8590884599/2500000000000,
+    ordinary(11/4000) = 6847884599/2500000000000.
+
+The first is the selected claim. The second is what the formula would return
+if it were pointed at the bridge weight. The pricing does not do that, and
+storing the bridge weight under `after_cover` would be a second external
+weight, dropping (H-one) or (H-writer). The bridge's own atom is `3/1000` and
+its own before-cover is `69/25000`; that other formula is not the selected
+formula.
+
+Therefore no second source assignment to `after_cover` makes the selected
+formula equal `C` while (H-one), (H-writer), (H-C1) and (H-gap) are kept.
+Under (H-writer) and (H-C1) there is no second assignment at all. Under the
+weaker requirement that a changed single weight still obey (H-gap), the
+formula still misses `C`, and the bridge weight is one authenticated example.
+
+## The odd-prime rule
+
+The controller records `odd q > 2^26*N^5`, avoiding fixed denominators and
+rank witnesses, and says that such a prime exceeds `256/(C0-C1)*N^5`. The
+coefficient comparison `2**26 > 256/(C0-C1)` holds at the kept gap
+`9/1000000`. That is rational arithmetic on the pinned literals. It is not a
+search for a prime, and the avoidance clause was not executed. At the
+preimage the same comparison has a negative denominator, so the rule's
+positive-gap hypothesis is false before any prime is chosen. The avoidance
+clause remains unrun. It is not the blocker of this negative result.
+
+## What this does not say
+
+`ordinary(69/20000) ≠ C` was already the census in
+`research/g20-source-bound-cover-census`. The new statement is that the whole
+positive-gap ray misses `C`, and that the retained bridge weight is not a
+second `after_cover` which repairs that miss.
+
+This note does not census other filenames, does not replay `verify.py` or the
+bridge script, does not execute the outer ledger, and does not replace
+`admitted` by `C` or by `ordinary`. The pricing still feeds
+`bit_saving = admitted = 17/5000` to the ledger. A contract that drops
+`before > after`, or that changes the formula, is outside the hypotheses.
+Equality of `ordinary` with `C` would still leave this assembly's
+`bit_saving` equal to `17/5000`.

research/g20-second-after-cover-obstruction/README.md

@@ -0,0 +1,115 @@
+# No second after-cover keeps the one-weight proof and equals C
+
+**Scoped proof. No new κ.** The selected conditional exponent stays
+**781451/250000000** (`0.003125804`).
+
+The selected ordinary formula reads one field, `ordinary_BIT.after_cover`.
+The thinned controller writes that field once, from `C1=0.00345`, spelled
+`69/20000`. The one-weight delayed-cover proof keeps a positive gap:
+`before > after`, with before-cover `C0=3459/1000000`. The formula is
+strictly increasing, and
+
+    ordinary(C0) = 8613294599/2500000000000
+
+is still strictly below the recorded PR5679 component
+
+    C = 3507410738409/1000000000000000.
+
+Every rational cover strictly below `C0` therefore misses `C`. The unique
+cover that hits `C` is `3507256898809/996000000000000`, and that rational is
+strictly above `C0`, so the positive-gap comparison does not apply to it.
+
+The second source assignment named here is the retained delayed-cover
+bridge, not a second write of `after_cover`. Its writer assigns
+`after = Q(11, 4000)` and stores `C1_after_cover`. Those bytes were
+authenticated before the arithmetic. The bridge key is not `after_cover`.
+Pointing the selected formula at `11/4000` still misses `C`. Emitting it
+beside `69/20000` would be a second external weight and would drop the
+one-weight sentence.
+
+## Scope
+
+Base commit `17469fff78c22941280f04d39dc5a1faee09c840` 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. Merged
+PR #6957, `research/g20-source-bound-cover-census`, already showed that the
+one emitted after-cover misses `C`. This package takes only open question 1
+of that note: a changed contract that emits a second after-cover while
+keeping the one-weight delayed-cover proof. The argument is in
+[PROOF.md](PROOF.md). The family-status expansion gate was not opened. This
+package does not extend a construction.
+
+Overlap recheck on 2026-11-10, after fetching canonical main at the base
+commit: 339 open upstream PR bodies and 7,007 discussion records. The
+preimage occurs in discussion
+[#1166 comment 19492491](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19492491)
+and in the #6957 finding
+[#1166 comment 19507126](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19507126),
+and in no open upstream PR body. The phrase "second after-cover" occurs only
+in the #6957 package's open question. No match is a novelty certificate.
+Question 2 of that package, the caller outside this pricing assembly, is
+merged #6958 and is not retaken. The PR5708 preimage remains with
+`research/g20-component-stock-gate`.
+
+## Validation
+
+Environment: Python 3.12, standard library only. From the repository root:
+
+```sh
+python3 -B research/g20-second-after-cover-obstruction/verify.py
+python3 -O -B research/g20-second-after-cover-obstruction/verify.py
+python3 -B scripts/research_package.py --package research/g20-second-after-cover-obstruction
+```
+
+The verifier prints `PASS_G20_SECOND_AFTER_COVER_OBSTRUCTION`. 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 bridge assignment is named and authenticated in that step.
+Controls reject an unbound arithmetic call, a second `after_cover` key, a
+bridge receipt whose key has been renamed to `after_cover`, a second C1
+sentence, and a second controller writer.
+
+Not run: the controller replay, the bridge script, the outer ledger, either
+component caller, native maps, a search for an odd prime, the odd-prime
+avoidance of denominators and rank witnesses, Lean, Docker, and
+`make frontier6030-verify`. The coefficient comparison
+`2**26 > 256/(C0-C1)` is evaluated only at the kept gap `9/1000000`. At the
+preimage the denominator is negative, so that rule is not a remaining
+search. The domain of the gap statement is every rational below `C0`; the
+verifier checks the slope and the image of `C0`, and does not enumerate the
+ray.
+
+## 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
+bridge weight is the retained source in `research/kappa-rebuild/bit`. The
+single-emission census that left this question open is merged PR #6957.
+The outside-pricing caller census is merged PR #6958 and is not retaken.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+
+## Open next questions
+
+1. The odd-prime rule also says the prime must avoid the fixed denominators
+   and rank witnesses. That avoidance list was not executed. It is not the
+   blocker of this negative result: every cover strictly below `C0` already
+   misses `C`, and the preimage is not below `C0`. First step, for a later
+   single cover that restores a positive gap and is being checked only for
+   the fallback surcharge: name one odd prime above `2^26*N^5` and the
+   denominator list it avoids. Blocked by the size of the controller's
+   compiled `N` and by this package not searching primes.
+2. If `before > after` and `256/(C0-C1)` are dropped, the unique preimage
+   makes this formula equal `C`. That drops the one-weight delayed-cover
+   proof rather than keeping it. First step: write the replacement for those
+   two sentences, then say whether `bit_saving` is still `admitted`.
+   Blocked here because both sentences are kept. Equality of `ordinary` with
+   `C` would still leave this assembly's `bit_saving` equal to `17/5000`.
+   This package does not retake the caller census of #6958.

research/g20-second-after-cover-obstruction/SOURCES.json

@@ -0,0 +1,84 @@
+{
+  "schema_version": 1,
+  "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840",
+  "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-helper-split/ORDINARY-RESULT.json",
+      "usage": "input",
+      "git_blob": "bfe417c5cca5227714238c80d65700e3f6a2e8d8",
+      "sha256": "382ca0d6c763dd26e12cac2e490eb1ecd8d40f1a1501b0e059aacc04fe7528de"
+    },
+    {
+      "path": "research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json",
+      "usage": "input",
+      "git_blob": "fbe6da7241357d89cf5c55b2e7ce2d0d046be32a",
+      "sha256": "edb273f59a27356ad89f38791590c3c806b228c3510eb508e01e89f2caba95ef"
+    },
+    {
+      "path": "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md",
+      "usage": "input",
+      "git_blob": "a58774e237c9362869a60a22bda35be09fb85872",
+      "sha256": "9731b93026717f5fa15851e3633cbb4bdc76eba2bffb9d6b4a3b69f7dd502443"
+    },
+    {
+      "path": "research/kappa-rebuild/bit/bit_allsize_parameters.py",
+      "usage": "input",
+      "git_blob": "aee5c2b85a96c7309d1dfec97c19b45d1bb9bbd3",
+      "sha256": "59f92cf44019c27bde3db2f4482f2b5fcf25f0c3dcf071319d46b041f7b6a821"
+    },
+    {
+      "path": "research/p104-helper470-twin-rung-removal/pricing.py",
+      "usage": "input",
+      "git_blob": "65bb723f8558dc60ff92764db1a43d8bf438aa09",
+      "sha256": "3c6cf2966ccfe5a5fb6c90f89f46ac224ea455127e35dd34975683c68c36d710"
+    },
+    {
+      "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/SOURCES.json",
+      "usage": "input",
+      "git_blob": "0f061c87ff87c43ff1ea0fc418582e9ccea3bc1d",
+      "sha256": "74b73563d9f78a4562d376b6f33528d652e41097f65747667f112a3e1fa81d29"
+    },
+    {
+      "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"
+    }
+  ]
+}