diff --git a/research/g20-second-after-cover-obstruction/PROOF.md b/research/g20-second-after-cover-obstruction/PROOF.md new file mode 100644 index 0000000000..e82ef9af34 --- /dev/null +++ b/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`. diff --git a/research/g20-second-after-cover-obstruction/README.md b/research/g20-second-after-cover-obstruction/README.md new file mode 100644 index 0000000000..d4853bf272 --- /dev/null +++ b/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. diff --git a/research/g20-second-after-cover-obstruction/SOURCES.json b/research/g20-second-after-cover-obstruction/SOURCES.json new file mode 100644 index 0000000000..0f41f96a19 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/g20-second-after-cover-obstruction/TASK.json b/research/g20-second-after-cover-obstruction/TASK.json new file mode 100644 index 0000000000..576a52db42 --- /dev/null +++ b/research/g20-second-after-cover-obstruction/TASK.json @@ -0,0 +1,97 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 8, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Does one changed supplier have complete source-bound native, caller, ordinary and outer admission coverage?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one latest uncovered candidate and build a delta coverage map against the selected review. For P104, #5717 changes owned-lifetime assumptions and #5719 covers exact #5713 causal premises; neither automatically transfers to #5718. For BIT, #5679/#5708 need component admission and compatible outer use. Check controls and exact source identity before reuse; stop with one resolved gap or explicit remaining obligation. A heavy full replay requires a separate serial resource budget.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "supplier admission", + "5717", + "5719", + "5708", + "owned lifetime" + ], + "existing_checks": [ + { + "scope": "PR #4088: author-checked local words, native receipts, owner/phase fill and exact moment.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Rebind and validate ordinary/outer admission with all four providers; full mixed release not established.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3801: successor scatter-boundary decision package.", + "evidence": "research/scatter-boundary-decision/README.md", + "remaining": "Consult its exact acceptance scope before any new exporter audit; not proof of a selected failure.", + "status": "author-checked", + "source_commit": "911f8800ba7a4b03603ef62c5ffc6240e53cb5fd", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Whether a second source assignment to after_cover can make the selected ordinary formula equal the recorded PR5679 component 3507410738409/1000000000000000 while the thinned controller's one-weight delayed-cover proof is kept.", + "scope_change_reason": "The card asks for one resolved gap on a latest BIT component. Merged #6957 already censused the single emitted after-cover. This package answers only the remaining question: authenticate the retained bridge's separate after-cover assignment, then decide whether a second emission can keep the one-weight proof and hit the component. Native, caller, compiler, tape, analytic recovery, and the outer ledger are not rerun.", + "bottleneck_link": "Complex currently binds and BIT is the next cap. The selected ordinary formula reads one after-cover. A second cover that the one-weight proof does not allow cannot change that formula, and every cover the proof's positive gap does allow stays strictly below the component. Matching ordinary to the component would still leave bit_saving equal to admitted, not ordinary, so it would not change kappa.", + "budget_minutes": 60, + "stop_rule": "Stop once the named bridge assignment is authenticated and the positive-gap obstruction is proved. Do not search for an odd prime, edit the controller, or replay the ledger.", + "outcome": "negative-result", + "evidence": "verify.py receipt and PROOF.md", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance for the source authentication, the gap proof, the verifier, and the write-up.", + "open_questions": [ + { + "question": "Does any odd prime above 2^26*N^5 avoid the fixed denominators and rank witnesses at the kept gap 9/1000000?", + "why_it_matters": "The controller's prime rule includes that avoidance clause. It is not the blocker of the second-cover obstruction: every cover strictly below C0 already misses the PR5679 component, and the preimage is not below C0.", + "first_step": "Name one such prime and the denominator list it avoids. Do not start from the preimage, where C0-C1 is negative.", + "blocked_by": "The controller's compiled N is enormous, and this package does not search primes." + }, + { + "question": "If before > after and 256/(C0-C1) are dropped, does the unique preimage make the selected ordinary formula equal the PR5679 component while bit_saving remains the recorded admitted value?", + "why_it_matters": "That preimage is the only rational solution of the formula. Using it drops the one-weight delayed-cover proof rather than keeping it, and equality of ordinary with the component would still leave this assembly's bit_saving equal to 17/5000.", + "first_step": "Write the replacement for those two sentences, then read the pricing assignment of bit_saving. Do not treat the result as a kappa change.", + "blocked_by": "This package keeps both sentences. It does not retake the caller census of #6958." + } + ] +} diff --git a/research/g20-second-after-cover-obstruction/VERIFY.json b/research/g20-second-after-cover-obstruction/VERIFY.json new file mode 100644 index 0000000000..838d16c478 --- /dev/null +++ b/research/g20-second-after-cover-obstruction/VERIFY.json @@ -0,0 +1,47 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/frontier6030/CLAIM.json", + "certificates/selected-result.json", + "research/g20-helper-split/ORDINARY-RESULT.json", + "research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json", + "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md", + "research/kappa-rebuild/bit/bit_allsize_parameters.py", + "research/p104-helper470-twin-rung-removal/pricing.py", + "research/query-thinned-controllers/PROOF.md", + "research/query-thinned-controllers/RESULT.json", + "research/query-thinned-controllers/SOURCES.json", + "research/query-thinned-controllers/controller.py", + "research/query-thinned-controllers/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Hash-bind the controller's single after_cover writer and the retained bridge's C1_after_cover assignment before arithmetic. Every cover strictly below the controller C0 misses the PR5679 component, and the unique preimage lies above C0. A second key, a renamed bridge key, a second C1 sentence, and a second writer fail closed. No prime search and no kappa change." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same proof and controls pass with assertions removed, because every check raises SystemExit." + } + ] +} diff --git a/research/g20-second-after-cover-obstruction/verify.py b/research/g20-second-after-cover-obstruction/verify.py new file mode 100644 index 0000000000..feda5c7d11 --- /dev/null +++ b/research/g20-second-after-cover-obstruction/verify.py @@ -0,0 +1,393 @@ +#!/usr/bin/env python3 +"""The one-weight proof admits no second after-cover equal to the PR5679 component. + +Authenticate the controller's single writer and the retained bridge's separate +C1 assignment before any Fraction arithmetic. The selected ordinary formula is +then shown to miss that component on every cover the positive-gap hypothesis +allows. This does not search for a prime, run the outer ledger, or change kappa. +""" +from fractions import Fraction +import ast +import hashlib +import json +import re +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +Q = Fraction + +CONTROLLER_RESULT = "research/query-thinned-controllers/RESULT.json" +CONTROLLER_VERIFY = "research/query-thinned-controllers/verify.py" +CONTROLLER_PROOF = "research/query-thinned-controllers/PROOF.md" +CONTROLLER_SOURCES = "research/query-thinned-controllers/SOURCES.json" +CONTROLLER_CODE = "research/query-thinned-controllers/controller.py" +PRICING = "research/p104-helper470-twin-rung-removal/pricing.py" +COMPONENT = "research/g20-helper-split/ORDINARY-RESULT.json" +BRIDGE_JSON = "research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json" +BRIDGE_PROSE = "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md" +BRIDGE_WRITER = "research/kappa-rebuild/bit/bit_allsize_parameters.py" +CLAIM = "certificates/frontier6030/CLAIM.json" +SELECTED = "certificates/selected-result.json" + +ONE_WEIGHT = "Keep one external cover weight throughout the entire finite BIT compilation" +C1_SENTENCE = "Use C0=0.003459 before covering and C1=0.00345" +GAP_PHRASE = "exceeds 256/(C0-C1)*N^5" +WRITER = "before, after, atom, old = Q('.003459'), Q('.00345'), Q('.004'), Q('.0000384599')" +GAP_NEED = "need(before > after and atom > ordinary > admitted and atom < 1-ordinary, 'Complete ordinary BIT conversion')" +PRIME_NEED = "need(Q('.003') < ordinary and 2**26 > 256/(before-after), 'Old atom rejected and finite prime bound')" +FORMULA = "ordinary=(1-atom)*Q(bit['after_cover'])+atom*Q('.0000384599')" +READER = "bit = L.read(L.ROOT/'research/query-thinned-controllers/RESULT.json')['ordinary_BIT']" +ATOM_LINE = "atom = Q(bit['atom'])" +ADMITTED_LINE = "admitted=Q(bit['admitted'])" +BRIDGE_ASSIGNMENT = "before,after=Q(69,25000),Q(11,4000)" +BRIDGE_GAP = "B.need(gap==Q(1,100000) and before>after>0,'Strict precompile-to-cover gap')" +BRIDGE_SENTENCE = "C1=11/4000=0.00275" +EMITTED_SPELLING = '"after_cover": "69/20000"' +RETAINED_BRIDGE_INPUTS = (BRIDGE_JSON, BRIDGE_PROSE) + + +def need(ok, message): + if not ok: + raise SystemExit("FAIL: " + message) + + +class Authenticated: + """Spellings checked against pinned bytes. Arithmetic must receive this.""" + + def __init__(self, spellings): + self.authenticated = True + self.spellings = spellings + + +def git_blob_sha1(raw): + header = b"blob " + str(len(raw)).encode("ascii") + b"\0" + return hashlib.sha1(header + raw).hexdigest() + + +def bind_sources(): + manifest = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8")) + files = {} + seen = [] + for row in manifest["files"]: + if row["usage"] != "input": + continue + path = row["path"] + raw = (ROOT / path).read_bytes() + need(hashlib.sha256(raw).hexdigest() == row["sha256"], "sha256 pin " + path) + need(git_blob_sha1(raw) == row["git_blob"], "git blob pin " + path) + need(b"\0" not in raw, "source is text " + path) + files[path] = raw.decode("utf-8") + seen.append(path) + need(len(seen) == len(set(seen)), "duplicate source pin") + required = { + CONTROLLER_RESULT, CONTROLLER_VERIFY, CONTROLLER_PROOF, CONTROLLER_SOURCES, + CONTROLLER_CODE, PRICING, COMPONENT, BRIDGE_JSON, BRIDGE_PROSE, BRIDGE_WRITER, + CLAIM, SELECTED, + } + need(required <= set(seen), "missing second-cover input") + return files + + +def walk_keys(value, key, prefix="$"): + found = [] + if isinstance(value, dict): + for name, child in value.items(): + path = prefix + "." + name + if name == key: + found.append((path, child)) + found.extend(walk_keys(child, key, path)) + elif isinstance(value, list): + for index, child in enumerate(value): + found.extend(walk_keys(child, key, prefix + "[" + str(index) + "]")) + return found + + +def tuple_assignments(source, names): + tree = ast.parse(source) + matches = [] + for node in ast.walk(tree): + if not isinstance(node, ast.Assign) or len(node.targets) != 1: + continue + target = node.targets[0] + if not isinstance(target, ast.Tuple): + continue + if not all(isinstance(item, ast.Name) for item in target.elts): + continue + got = [item.id for item in target.elts] + if got == names: + matches.append(ast.get_source_segment(source, node)) + return matches + + +def name_assignments(source, name): + tree = ast.parse(source) + matches = [] + for node in ast.walk(tree): + if not isinstance(node, ast.Assign) or len(node.targets) != 1: + continue + target = node.targets[0] + if isinstance(target, ast.Name) and target.id == name: + matches.append(ast.get_source_segment(source, node)) + return matches + + +def authenticate(files): + """Name both source assignments. No rational arithmetic in this function.""" + proof = files[CONTROLLER_PROOF] + verify = files[CONTROLLER_VERIFY] + result = files[CONTROLLER_RESULT] + code = files[CONTROLLER_CODE] + pricing = files[PRICING] + bridge_json_text = files[BRIDGE_JSON] + bridge_prose = files[BRIDGE_PROSE] + bridge_writer = files[BRIDGE_WRITER] + component_text = files[COMPONENT] + claim_text = files[CLAIM] + selected_text = files[SELECTED] + controller_sources = json.loads(files[CONTROLLER_SOURCES]) + + need(proof.count(ONE_WEIGHT) == 1, "one external cover-weight sentence") + need(proof.count(C1_SENTENCE) == 1, "one controller C1 sentence") + need(proof.count("C1=") == 1, "one C1 literal in the controller proof") + need(proof.count(GAP_PHRASE) == 1, "one positive-gap prime comparison") + need("11/4000" not in proof and BRIDGE_SENTENCE not in proof, + "the bridge weight is not copied into the controller C1 sentence") + + writers = tuple_assignments(verify, ["before", "after", "atom", "old"]) + need(writers == [WRITER], "one controller cover assignment") + need(verify.count(WRITER) == 1, "writer text occurs once") + need(verify.count("'after_cover'") == 1, "controller writes one after_cover key") + need(verify.count(GAP_NEED) == 1, "one strict before-after gate") + need(verify.count(PRIME_NEED) == 1, "one numerical prime-coefficient comparison") + need("11/4000" not in verify, "controller verifier does not assign the bridge weight") + + need(result.count(EMITTED_SPELLING) == 1, "one raw after_cover spelling") + need(result.count('"after_cover"') == 1, "one after_cover key in the controller receipt") + receipt = json.loads(result) + found = walk_keys(receipt, "after_cover") + need(len(found) == 1 and found[0] == ("$.ordinary_BIT.after_cover", "69/20000"), + "parsed controller after_cover") + bit = receipt["ordinary_BIT"] + need(bit["before_cover"] == "3459/1000000", "controller before-cover spelling") + need(bit["atom"] == "1/250", "controller atom spelling") + need(bit["admitted"] == "17/5000", "controller admitted spelling") + need("odd q > 2^26*N^5" in bit["prime_rule"], "prime rule is recorded, not evaluated") + need("after_cover" not in code and "11/4000" not in code and ".00345" not in code, + "controller.py does not assign a cover weight") + + retained = {row["path"]: row["usage"] for row in controller_sources["files"]} + for path in RETAINED_BRIDGE_INPUTS: + need(retained.get(path) == "input", "controller package retains " + path) + need(BRIDGE_WRITER not in retained, "controller pins the bridge receipt, not its writer script") + + need(bridge_prose.count(BRIDGE_SENTENCE) == 1, "one bridge C1 sentence") + need('"after_cover"' not in bridge_prose and "'after_cover'" not in bridge_prose, + "bridge prose does not name the formula key") + bridge_writers = tuple_assignments(bridge_writer, ["before", "after"]) + need(bridge_writers == [BRIDGE_ASSIGNMENT], "one bridge after-cover assignment") + need(bridge_writer.count(BRIDGE_ASSIGNMENT) == 1, "bridge assignment text occurs once") + need(bridge_writer.count(BRIDGE_GAP) == 1, "bridge gap predicate") + need(bridge_writer.count("'C1_after_cover'") == 2, "bridge stores and prints C1_after_cover") + need("'after_cover'" not in bridge_writer and '"after_cover"' not in bridge_writer, + "bridge writer does not store the formula key") + bridge = json.loads(bridge_json_text) + need(walk_keys(bridge, "after_cover") == [], "bridge receipt has no after_cover key") + bridge_covers = walk_keys(bridge, "C1_after_cover") + need(bridge_covers == [("$." + "C1_after_cover", "11/4000")], "bridge C1_after_cover spelling") + need(bridge["C0_before_cover"] == "69/25000", "bridge before-cover is not the controller C0") + need(bridge["C0_minus_C1"] == "1/100000", "bridge's own gap spelling") + need(bridge_json_text.count('"after_cover"') == 0, "bridge receipt text has no after_cover key") + need(bridge_json_text.count('"C1_after_cover"') == 1, "one bridge C1_after_cover key") + + need(pricing.count(FORMULA) == 1, "one selected ordinary formula") + need(pricing.count(READER) == 1, "formula reads the thinned-controller receipt") + need(pricing.count(ATOM_LINE) == 1 and pricing.count(ADMITTED_LINE) == 1, "atom and admitted reads") + need(name_assignments(pricing, "ordinary") == [FORMULA], "formula AST") + need(name_assignments(pricing, "admitted") == [ADMITTED_LINE], "admitted is not ordinary") + need(pricing.count("'bit_saving':admitted") == 1, "bit_saving is the name admitted") + need("ordinary_saving" not in pricing and "C1_after_cover" not in pricing, + "pricing does not read a stored ordinary or the bridge weight") + need("kappa-rebuild/bit" not in pricing, "pricing does not read the bridge") + + component = json.loads(component_text) + claim = json.loads(claim_text) + selected = json.loads(selected_text) + need(component["admitted"] == "3507410738409/1000000000000000", "recorded PR5679 component spelling") + need(component["whole_kappa"] is None, "component receipt claims no whole kappa") + need(claim["kappa"] == selected["kappa"] == "781451/250000000", "selected kappa spelling") + need(selected["decimal"] == "0.003125804", "selected decimal spelling") + need(claim["ordinary_BIT_saving"] == "8590884599/2500000000000", "selected ordinary spelling") + + return Authenticated({ + "emitted": bit["after_cover"], + "before": bit["before_cover"], + "atom": bit["atom"], + "admitted": bit["admitted"], + "bridge": bridge["C1_after_cover"], + "bridge_before": bridge["C0_before_cover"], + "component": component["admitted"], + "claim_ordinary": claim["ordinary_BIT_saving"], + "kappa": claim["kappa"], + "texts": files, + }) + + +def ordinary(atom, cover, epsilon): + return (1 - atom) * cover + atom * epsilon + + +def absent_token(text, token): + return re.search(r"(? emitted > bridge > 0, "both named covers sit strictly below controller C0") + need(before - emitted == Q(9, 1000000), "controller gap") + + slope = 1 - atom + need(slope == Q(249, 250) and slope > 0, "ordinary is strictly increasing in the cover") + at_emitted = ordinary(atom, emitted, epsilon) + at_before = ordinary(atom, before, epsilon) + at_bridge = ordinary(atom, bridge, epsilon) + need(at_emitted == Q(spell["claim_ordinary"]) == Q(8590884599, 2500000000000), + "ordinary at the emitted cover reproduces the selected claim") + need(at_before == Q(8613294599, 2500000000000), "ordinary at controller C0") + need(at_bridge == Q(6847884599, 2500000000000), "ordinary at the bridge weight") + need(at_bridge < at_emitted < at_before, "the two named covers sit below the C0 image") + + preimage = (recorded - atom * epsilon) / slope + need(preimage == Q(3507256898809, 996000000000000), "reduced preimage") + need(ordinary(atom, preimage, epsilon) == recorded, "preimage reproduces the component") + need(preimage > before, "the preimage is not strictly below C0") + need(before - preimage == Q(-62092898809, 996000000000000), "negative gap at the preimage") + need(recorded - at_before == slope * (preimage - before) == Q(62092898809, 1000000000000000), + "component stays above ordinary at C0") + need(recorded - at_emitted == slope * (preimage - emitted) == Q(71056898809, 1000000000000000), + "component stays above ordinary at the emitted cover") + need(at_before < recorded and at_emitted < recorded and at_bridge < recorded, + "C0, the emitted cover, and the bridge weight all miss the component") + + def misses(cover): + need(cover < before, "gap-feasible covers are strictly below C0") + image = ordinary(atom, cover, epsilon) + need(image < at_before < recorded, "a gap-feasible cover stays strictly below the component") + return image + + need(misses(emitted) == at_emitted and misses(bridge) == at_bridge, + "both named assignments are gap-feasible and miss the component") + try: + misses(preimage) + except SystemExit as exc: + need(str(exc) == "FAIL: gap-feasible covers are strictly below C0", + "the preimage is rejected by the gap hypothesis") + else: + need(False, "the preimage was treated as gap-feasible") + need(2**26 > 256 / (before - emitted), "kept positive gap meets the recorded coefficient comparison") + need(before - preimage < 0, "the same comparison has no positive denominator at the preimage") + + preimage_token = str(preimage.numerator) + for path, body in spell["texts"].items(): + need(absent_token(body, preimage_token), "preimage numerator is not a source constant in " + path) + need(str(preimage) not in body, "preimage fraction is not written in " + path) + + return { + "status": "PASS_G20_SECOND_AFTER_COVER_OBSTRUCTION", + "claim_type": "scoped-proof", + "kappa": spell["kappa"], + "kappa_changed": False, + "ledger_executed": False, + "controller_replayed": False, + "prime_searched": False, + "odd_prime_avoidance_executed": False, + "admission_verdict": "not claimed", + "bit_saving_expression": "admitted", + "admitted_BIT": spell["admitted"], + "hypotheses": [ + "one external cover-weight sentence", + "one controller C1 sentence C1=0.00345", + "one writer of after_cover from that C1", + "before > after, so every kept cover is strictly below 3459/1000000", + ], + "controller_after_cover": str(emitted), + "bridge_C1_after_cover": str(bridge), + "bridge_key_is_after_cover": False, + "second_after_cover_assignment_named": "research/kappa-rebuild/bit/bit_allsize_parameters.py", + "controller_C0": str(before), + "slope": str(slope), + "ordinary_at_emitted_cover": str(at_emitted), + "ordinary_at_controller_C0": str(at_before), + "ordinary_at_bridge_weight": str(at_bridge), + "pr5679_component": str(recorded), + "component_minus_ordinary_at_C0": str(recorded - at_before), + "unique_preimage": str(preimage), + "preimage_below_C0": False, + "positive_gap_at_preimage": False, + "every_gap_feasible_cover_misses_component": True, + "domain": "all rationals strictly below the controller C0; proved by a positive slope, not enumerated", + } + + +def reject(label, callback): + try: + callback() + except SystemExit as exc: + need(str(exc).startswith("FAIL:"), label + " did not fail closed") + return + need(False, label + " returned") + + +def controls(files): + reject("unbound arithmetic", lambda: arithmetic(object())) + + second_key = dict(files) + second_key[CONTROLLER_RESULT] = files[CONTROLLER_RESULT].replace( + EMITTED_SPELLING, + EMITTED_SPELLING + ', "nested": {"after_cover": "11/4000"}', + 1, + ) + need(second_key[CONTROLLER_RESULT] != files[CONTROLLER_RESULT], "second-key mutation") + reject("second after_cover key", lambda: authenticate(second_key)) + + renamed = dict(files) + renamed[BRIDGE_JSON] = files[BRIDGE_JSON].replace('"C1_after_cover"', '"after_cover"', 1) + need('"after_cover"' in renamed[BRIDGE_JSON], "renamed bridge key") + reject("bridge weight stored as after_cover", lambda: authenticate(renamed)) + + duplicated = dict(files) + duplicated[CONTROLLER_PROOF] = files[CONTROLLER_PROOF].replace( + C1_SENTENCE, C1_SENTENCE + "\n" + C1_SENTENCE, 1) + reject("second C1 sentence", lambda: authenticate(duplicated)) + + second_writer = dict(files) + second_writer[CONTROLLER_VERIFY] = files[CONTROLLER_VERIFY].replace( + WRITER, WRITER + "\n " + WRITER, 1) + reject("second controller writer", lambda: authenticate(second_writer)) + + +def main(): + files = bind_sources() + controls(files) + bound = authenticate(files) + receipt = arithmetic(bound) + print("PASS_G20_SECOND_AFTER_COVER_OBSTRUCTION") + print(json.dumps(receipt, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()