diff --git a/research/outer-ledger-kappa-region/PROOF.md b/research/outer-ledger-kappa-region/PROOF.md new file mode 100644 index 0000000000..300f2dd0dc --- /dev/null +++ b/research/outer-ledger-kappa-region/PROOF.md @@ -0,0 +1,89 @@ +# Proof: exact κ region of the selected outer ledger + +## Setting + +The selected #5599 result (`research/p104-helper-subspace-splits/pricing.py`) +calls `ledger(params)` from +`research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py`. That +function recomputes zxv's PR4359 outer parameter ledger: 54 strict checks and +3 functional checks. `pricing.py` adds a fourth functional check, +`β(1-atom)` with `atom=1/250`. Call the 58 expressions *the ledger*; it is +satisfied when every expression is strictly positive. + +Inputs: κ, the complex uniform saving U, and the admitted BIT saving B. +Free parameters: b, a, q, ε, β, r0, stop, layout. (`tested_saving` and `d` +are passed through but no check reads them.) Write OLD for the ledger constant +`OLD_BASELINE = 0.001730970419199163702738` and M = min(U, B, 1/32). + +**Theorem.** Some choice of the free parameters satisfies the ledger if and +only if OLD < κ < M. + +## Necessity + +Nine checks give the chain. Each name is the ledger's own key; `verify.py` +checks every closed form against the loaded function on random exact inputs. + +| Check | Expression > 0 | +|---|---| +| `improvement_over_user_baseline` | κ − OLD | +| `main_transform_above_kappa` | εq − κ | +| `epsilon_below_one` | 1 − ε | +| `q_positive` | q | +| `q_below_effective` | a − q | +| `actual_bit_above_effective` | B − a | +| `complex_above_effective` | b − a | +| `new_complex_uniform_saving_above_b` | U − b | +| `complex_below_one_over_32` | 1/32 − b | + +From q > 0 and ε < 1, εq < q, so κ < εq < q < a. Then a < B, and +a < b < min(U, 1/32). Hence κ < min(U, B, 1/32), and κ > OLD directly. ∎ + +## Sufficiency + +Let OLD < κ < M and d = (M − κ)/7 > 0. Take PR4359's own `family` shape: + + q = κ+3d, a = κ+4d, b = κ+5d, + ε = 1−d, β = 1−3d, r0 = d/10, stop = layout = d. + +Then 0 < κ < q < a < b < M ≤ min(U, B, 1/32), and d < 1/224. Write +σ = 1−b, τ = 1−a, λ = 1−(q+a)/2, c = 3/32, ξ = ε(1+q) − c + layout, +key = β+1−ε. Since σ−τ = a−b < 0, internal = τ; leaf = σ + d·b. + +- Ordering rows: B−a, b−a, U−b, 1/32−b, a−q, b−q and q are positive by + construction. `leaf_saving_above_effective` = (1−d)b − a = d − d(κ+5d) > 0 + because κ+5d < 1. `q_below_leaf` = (1−d)b − q exceeds it. +- λ rows: λ−τ = (a−q)/2, λ−σ = b−(q+a)/2, λ−internal = (a−q)/2, + 1−q−λ = (a−q)/2, 1−internal−q = a−q, 1−q−leaf = (1−d)b − q. All positive. +- ε, β rows: 1−ε = d, ε−β = 2d, 1−β = 3d, 1−ε−r0 = 9d/10, + 1−key = 2d, 1−β−2(1−ε) = d, ε−a > 0, β > 0, 80−β > 0, r0, stop, + 1−stop and layout are positive. +- ξ rows: ξ − 1/2 = ε(1+q) + d − 19/32 > 0 since ε > 1 − 1/224. + ε − ξ = 3/32 − εq − d > 0 since q < 1/32 and d < 1/224. 2 − ξ > 0. + 3 − 2ξ − β − r0 > 0 and 3 − 2ξ − β > 0 since ξ < ε < 1 and β+r0 < 1. +- Main row: εq − κ = (1−d)(κ+3d) − κ = d(3 − κ − 3d) > 0. +- Other margins above κ: a − κ = 4d; fused = 1−ε+qβ = εq + d(1−2q) > εq; + group BIT router = 1−ε+aβ = a + d(1−3a) > a; group scans = 1−ε+β ≈ 1; + boundary matrix = c+ξ−ε = εq + d > εq; sparse union = εq + d + 13/32; + polynomial = ε; microbox = 79−ε−β. Each exceeds κ < 1/32. + `gaussian_above_main` = d(1−2q) > 0. +- Constant rows: 2^45 − 7^16, 2, 5 and 7/2 are positive. +- Functional rows: 1−β, β(1−3/1000), 79−ε−β and β(1−1/250) are positive. ∎ + +## Consequences + +1. The 58 outer checks lose only strict slack: the supremum of admissible κ + is exactly min(U, B, 1/32), and it is never attained. +2. At the selected values U = 21703153/7000000000 and B = 17/5000, the + supremum is U. The selected κ = 62009/20000000 sits 3/7000000000 below it. +3. At the selected κ, the ledger accepts any admitted BIT saving B > κ. + The admitted .0034 has 5991/20000000 of headroom. The PR4359 negative + control B = .0027 fails only because .0027 < κ. +4. For any target κ > .01, the ledger requires exactly U > κ and B > κ. + It rules out κ ≥ 1/32 for every pair of suppliers. + +## Scope + +This is a scoped proof about the ledger's parameter arithmetic. It does not +prove the outer theorems the ledger encodes, the five inherited framework +assumptions, native or compiler costs, or any supplier admission. It changes +no κ and no selected frontier. diff --git a/research/outer-ledger-kappa-region/README.md b/research/outer-ledger-kappa-region/README.md new file mode 100644 index 0000000000..e7750a0100 --- /dev/null +++ b/research/outer-ledger-kappa-region/README.md @@ -0,0 +1,94 @@ +# Exact κ region of the selected outer ledger + +**Scoped written proof with exact finite corroboration; no new κ.** + +The selected #5599 result passes its supplier savings through one outer +ledger: zxv's PR4359 parameter ledger, recomputed by +`research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py` and +called by `research/p104-helper-subspace-splits/pricing.py`. It has 54 strict +checks and 4 functional checks over the free parameters +b, a, q, ε, β, r0, stop and layout. + +**Theorem.** For complex uniform saving U and admitted BIT saving B, the +58 checks are jointly satisfiable at κ exactly when + + OLD_BASELINE < κ < min(U, B, 1/32), + +where OLD_BASELINE = 0.001730970419199163702738 is the ledger's constant. + +Necessity is a chain through nine named checks: κ < εq < q < a < B and +a < b < min(U, 1/32). Sufficiency uses PR4359's own `family` shape with +d = (min(U, B, 1/32) − κ)/7. [PROOF.md](PROOF.md) checks all 58 rows. + +## What this tells the next contributor + +- The outer rows lose nothing beyond strict slack. Revision 8's "work + backward from the nine outer rows" step for κ > .01 reduces to U > κ and + B > κ. These rows impose no other condition. +- κ ≥ 1/32 is excluded for every supplier pair. The cap comes from the + `complex_below_one_over_32` row. +- At the selected values, U = 21703153/7000000000 binds. The selected + κ = 62009/20000000 is 3/7000000000 below the ledger supremum U. +- At the selected κ, any admitted BIT saving above κ passes. The admitted + 17/5000 has 5991/20000000 of headroom. The historical .0027 control fails + only because .0027 < κ. + +## Evidence + +`verify.py` loads the ledger unchanged and checks: + +- inventory: 54 strict plus 3 functional checks in the ledger, and the fourth + functional check and the ledger call in the selected `pricing.py`; +- the closed form of each of the nine chain checks on 400 random exact inputs; +- the explicit witness at 528 points: a 9×9 grid of (U, B) with three κ per + admissible pair, including κ = OLD + 10⁻³⁰ and κ = M − 10⁻³⁰, plus random + pairs; +- 4,000 random perturbations of witnesses. The 58 that satisfy every check + all lie inside the region. This is corroboration, not the proof; +- controls: κ = B fails `actual_bit_above_effective`; κ = OLD fails only the + baseline row; b > 1/32 fails `complex_below_one_over_32`; ε > 1 fails + `epsilon_below_one`; +- the selected corollary from `certificates/frontier5599/CLAIM.json`. + +## Reproduce + +From the repository root with CPython 3.12 and only the standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/outer-ledger-kappa-region +python3.12 -B scripts/check_research_commit.py --package research/outer-ledger-kappa-region --check-source-history +python3.12 -I -W error -B research/outer-ledger-kappa-region/verify.py +python3.12 -I -O -W error -B research/outer-ledger-kappa-region/verify.py +``` + +Success prints `PASS_OUTER_LEDGER_KAPPA_REGION`. The run takes under a +second and writes no files. Inputs are pinned in [SOURCES.json](SOURCES.json). + +## Limitations + +This is about the ledger's parameter arithmetic only. It does not prove the +outer theorems the ledger encodes, the five inherited framework assumptions, +native, compiler or stock costs, or any supplier admission. Other outer +assemblies in the repository are not covered. No κ or selected frontier +changes. + +## Open next questions + +1. **Which proof obligation behind the 1/32 row binds first?** The row + `complex_below_one_over_32` is the only supplier-independent cap. An older + assembly audit (`research/format-limits-corrected`) calls its 1/32 domain + cap conservative. First step: trace the row to its PR4359 source lemma and + find whether a larger domain is provable. Blocker: the lemma is an + inherited framework premise, not re-proved here. +2. **Does a joint supplier change cost the ledger anything?** The region + depends only on min(U, B). A change trading complex for BIT saving gains + κ only while U < B. First step: state any proposed trade as (ΔU, ΔB) and + apply the min. Blocker: no such joint supplier exists yet. + +## Credit + +Produced by Nick Petalas. The ledger and its `family` shape are zxv's PR4359 +outer parameters, as retained in `research/pr4359-p7-padding`; the selected +call and fourth functional check are from the #5599 package +`research/p104-helper-subspace-splits` and its contributor lineage. New work +is Apache-2.0. diff --git a/research/outer-ledger-kappa-region/SOURCES.json b/research/outer-ledger-kappa-region/SOURCES.json new file mode 100644 index 0000000000..056b4ee3d5 --- /dev/null +++ b/research/outer-ledger-kappa-region/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/frontier5599/CLAIM.json", + "usage": "input", + "git_blob": "3a8673160d129f0bec6aacf3ff2c2cf693839221", + "sha256": "66fbb5b21f32f1c4ba544c20d5a44ebcdfd11bce2bfa2d609c656ae520d3b21e" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-helper-subspace-splits/pricing.py", + "usage": "input", + "git_blob": "0b54ad3f16e3c1068e9e36ee83187e150325a791", + "sha256": "637c8b0eea8bf870d866707de8230aa8ddd0c7401b56153f65b60913b025000b" + }, + { + "path": "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py", + "usage": "input", + "git_blob": "340e1f0ffb8a1a9c38fbbd9119580b6d23e01b59", + "sha256": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15" + } + ] +} diff --git a/research/outer-ledger-kappa-region/TASK.json b/research/outer-ledger-kappa-region/TASK.json new file mode 100644 index 0000000000..db1b9eba78 --- /dev/null +++ b/research/outer-ledger-kappa-region/TASK.json @@ -0,0 +1,97 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "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": "changed", + "actual_scope": "Exact set of kappa for which the selected #5599 outer ledger (PR4359 54 strict checks plus 4 functional checks, as called by research/p104-helper-subspace-splits/pricing.py) is satisfiable, as a function of the complex uniform saving U and admitted BIT saving B.", + "scope_change_reason": "Original target chosen at the open-question checkpoint. Instead of auditing one changed supplier, this settles the outer-admission step that every changed supplier must pass: it gives the exact supplier conditions the selected outer ledger imposes, which revision 8 asks contributors aiming at kappa > .01 to work out.", + "bottleneck_link": "Revision 8 says to work backward from the nine outer rows for kappa > .01. This proves those rows require exactly U > kappa and B > kappa (and kappa < 1/32), so supplier savings, not the outer ledger, are the binding constraint.", + "budget_minutes": 60, + "stop_rule": "Stop after the written proof, exact corroboration and one focused PR.", + "outcome": "completed", + "evidence": "PROOF.md and verify.py (PASS_OUTER_LEDGER_KAPPA_REGION).", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which proof obligation behind the complex_below_one_over_32 row binds first, and can its 1/32 domain be enlarged?", + "why_it_matters": "It is the only supplier-independent cap in the selected outer ledger.", + "first_step": "Trace the row to its PR4359 source lemma and identify where 1/32 enters.", + "blocked_by": "The lemma is an inherited framework premise, not re-proved here." + }, + { + "question": "Does any proposed joint complex/BIT supplier trade improve kappa under this ledger?", + "why_it_matters": "The admissible region depends only on min(U, B), so a trade helps only while U < B.", + "first_step": "State the trade as (delta U, delta B) and apply the min.", + "blocked_by": "No such joint supplier exists yet." + } + ] +} diff --git a/research/outer-ledger-kappa-region/VERIFY.json b/research/outer-ledger-kappa-region/VERIFY.json new file mode 100644 index 0000000000..b6e7aee5b4 --- /dev/null +++ b/research/outer-ledger-kappa-region/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/frontier5599/CLAIM.json", + "research/p104-helper-subspace-splits/pricing.py", + "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Ledger inventory and selected call; closed forms of the nine necessity-chain checks; explicit witness at 528 points including both region endpoints; random feasible points inside the region; boundary and 1/32 controls; selected corollary." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Ledger inventory and selected call; closed forms of the nine necessity-chain checks; explicit witness at 528 points including both region endpoints; random feasible points inside the region; boundary and 1/32 controls; selected corollary." + } + ] +} diff --git a/research/outer-ledger-kappa-region/verify.py b/research/outer-ledger-kappa-region/verify.py new file mode 100644 index 0000000000..70fd93fb1e --- /dev/null +++ b/research/outer-ledger-kappa-region/verify.py @@ -0,0 +1,235 @@ +#!/usr/bin/env python3 +"""Exact kappa region of the selected outer transfer ledger. + +Nick Petalas. Apache-2.0. The ledger is zxv's PR4359 outer parameter ledger as +recomputed in research/pr4359-p7-padding endpoint.py and called by the selected +research/p104-helper-subspace-splits/pricing.py; it is loaded unchanged. + +Claim checked: for supplier savings U (complex uniform) and B (admitted BIT), +some choice of the free parameters makes all 54 strict and 4 functional checks +positive iff OLD_BASELINE < kappa < min(U, B, 1/32). PROOF.md gives the proof; +this script binds every named check used by the proof to the loaded ledger, +evaluates the explicit witness, and runs failure controls. +""" +from fractions import Fraction as Q +from hashlib import sha256 +from pathlib import Path +import importlib.util +import json +import random +import sys + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +LEDGER = ROOT/'research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py' +PRICING = ROOT/'research/p104-helper-subspace-splits/pricing.py' +CLAIM = ROOT/'certificates/frontier5599/CLAIM.json' +CAP = Q(1, 32) +ATOM = Q(1, 250) +FREE = ('b', 'a', 'q', 'epsilon', 'beta', 'r0', 'stop', 'layout') +# Checks used by the necessity chain, with their closed forms. +CHAIN = { + 'improvement_over_user_baseline': lambda p, old: p['kappa']-old, + 'main_transform_above_kappa': lambda p, old: p['epsilon']*p['q']-p['kappa'], + 'epsilon_below_one': lambda p, old: 1-p['epsilon'], + 'q_positive': lambda p, old: p['q'], + 'q_below_effective': lambda p, old: p['a']-p['q'], + 'actual_bit_above_effective': lambda p, old: p['bit_saving']-p['a'], + 'complex_above_effective': lambda p, old: p['b']-p['a'], + 'new_complex_uniform_saving_above_b': lambda p, old: p['complex_uniform_saving']-p['b'], + 'complex_below_one_over_32': lambda p, old: CAP-p['b'], +} + + +def need(value, message): + if not value: + raise AssertionError(message) + + +def load_ledger(): + spec = importlib.util.spec_from_file_location('selected_outer_ledger', LEDGER) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def evaluate(module, p): + out = module.ledger(p) + values = dict(out['strict_checks']) + values.update(out['functional_checks']) + values['actual_new_BIT_stock_sublinear'] = p['beta']*(1-ATOM) + return values + + +def feasible_predicted(old, U, B, kappa): + return old < kappa < min(U, B, CAP) + + +def witness(U, B, kappa): + """The PR4359 family shape with d=(min(U,B,1/32)-kappa)/7.""" + d = (min(U, B, CAP)-kappa)/7 + return {'kappa': kappa, 'complex_uniform_saving': U, 'bit_saving': B, + 'b': kappa+5*d, 'a': kappa+4*d, 'q': kappa+3*d, + 'epsilon': 1-d, 'beta': 1-3*d, 'r0': d/10, 'stop': d, 'layout': d} + + +def all_positive(values): + return all(v > 0 for v in values.values()) + + +def check_inventory(module): + probe = witness(Q('.004'), Q('.005'), Q('.003')) + values = evaluate(module, probe) + need(len(values) == 58, 'Inventory: 54 strict plus 4 functional checks') + out = module.ledger(probe) + need(len(out['strict_checks']) == 54 and len(out['functional_checks']) == 3, + 'Ledger supplies 54 strict and 3 functional; pricing.py adds the fourth') + need(set(probe) == set(FREE)|{'kappa', 'complex_uniform_saving', 'bit_saving'}, + 'Witness sets exactly the ledger inputs') + text = PRICING.read_text() + need('outer_module.ledger(params)' in text and "'p104_productive_outer'" in text, + 'Selected pricing calls this ledger') + need("params['beta']*(1-atom)" in text, 'Selected fourth functional check') + return values + + +def check_chain_bindings(module, rng): + """Each chain check equals its closed form on random exact inputs.""" + old = module.OLD_BASELINE + for _ in range(400): + p = {k: Q(rng.randint(-50, 2000), rng.randint(1, 4000)) for k in FREE} + p.update(kappa=Q(rng.randint(1, 900), 10**5), + complex_uniform_saving=Q(rng.randint(1, 900), 10**5), + bit_saving=Q(rng.randint(1, 900), 10**5)) + values = evaluate(module, p) + for name, form in CHAIN.items(): + need(values[name] == form(p, old), 'Chain binding '+name) + return len(CHAIN) + + +def check_witnesses(module, rng): + old = module.OLD_BASELINE + count = 0 + grid = [Q('.0025'), Q('.0031'), Q('.0034'), Q('.01'), Q('.02'), Q('.03'), + Q(1, 32), Q('.05'), Q('.2')] + for U in grid: + for B in grid: + top = min(U, B, CAP) + for kappa in (old+Q(1, 10**30), (old+top)/2, top-Q(1, 10**30)): + if not feasible_predicted(old, U, B, kappa): + continue + need(all_positive(evaluate(module, witness(U, B, kappa))), + 'Witness passes every check') + count += 1 + for _ in range(300): + U = Q(rng.randint(1, 10**6), 10**7) + B = Q(rng.randint(1, 10**6), 10**7) + top = min(U, B, CAP) + if top <= old: + continue + kappa = old+(top-old)*Q(rng.randint(1, 10**6-1), 10**6) + need(all_positive(evaluate(module, witness(U, B, kappa))), 'Random witness') + count += 1 + return count + + +def check_necessity_samples(module, rng): + """Random feasible points never exceed the predicted region.""" + old = module.OLD_BASELINE + hits = 0 + for _ in range(4000): + U = Q(rng.randint(1, 4*10**5), 10**7) + B = Q(rng.randint(1, 4*10**5), 10**7) + top = min(U, B, CAP) + kappa = Q(rng.randint(1, 4*10**5), 10**7) + base = witness(max(U, kappa*2), max(B, kappa*2), kappa) + p = {k: base[k]*(1+Q(rng.randint(-20, 20), 1000)) for k in FREE} + p.update(kappa=kappa, complex_uniform_saving=U, bit_saving=B) + if all_positive(evaluate(module, p)): + need(old < kappa < top, 'Feasible point inside region') + hits += 1 + need(hits > 0, 'Necessity sampling found feasible points') + return hits + + +def check_controls(module): + old = module.OLD_BASELINE + U, B = Q('.02'), Q('.012') + rows = {} + for name, kappa in (('kappa_equals_BIT', B), ('kappa_at_baseline', old)): + p = witness(U, B, kappa) if kappa < B else witness(U, B+Q(1, 10**9), kappa) + p['bit_saving'] = B + rows[name] = sorted(k for k, v in evaluate(module, p).items() if v <= 0) + need('actual_bit_above_effective' in rows['kappa_equals_BIT'], 'BIT boundary rejects') + need(rows['kappa_at_baseline'] == ['improvement_over_user_baseline'], 'Baseline rejects') + p = witness(Q('.04'), Q('.04'), Q('.03')) + p['b'] = Q('.0313') + p['complex_uniform_saving'] = Q('.04') + rows['b_above_one_over_32'] = sorted(k for k, v in evaluate(module, p).items() if v <= 0) + need('complex_below_one_over_32' in rows['b_above_one_over_32'], '1/32 row rejects') + p = witness(Q('.004'), Q('.005'), Q('.003')) + p['epsilon'] = 1+Q(1, 10**6) + rows['epsilon_one_or_more'] = sorted(k for k, v in evaluate(module, p).items() if v <= 0) + need('epsilon_below_one' in rows['epsilon_one_or_more'], 'epsilon row rejects') + # Old PR4359 control: BIT .0027 fails at the selected kappa. + claim = json.loads(CLAIM.read_text()) + kappa = Q(claim['kappa']) + U = {t['family']: Q(t['saving']) for t in claim['uniform_templates']}['complex'] + rows['selected_kappa_BIT_0027'] = 'kappa >= B, so actual_bit_above_effective fails' + need(not feasible_predicted(old, U, Q('.0027'), kappa), 'Old .0027 control excluded') + return rows + + +def selected_corollary(module): + claim = json.loads(CLAIM.read_text()) + kappa = Q(claim['kappa']) + templates = {t['family']: Q(t['saving']) for t in claim['uniform_templates']} + U = templates['complex'] + B = Q(claim['admitted_BIT_saving']) + top = min(U, B, CAP) + need(top == U, 'Complex supplier binds the selected ledger') + need(feasible_predicted(module.OLD_BASELINE, U, B, kappa), 'Selected kappa inside region') + need(all_positive(evaluate(module, witness(U, B, kappa))), 'Selected witness') + need(module.OLD_BASELINE < B, 'Admitted BIT above baseline') + return {'U_complex_uniform': U, 'B_admitted_BIT': B, 'kappa_selected': kappa, + 'ledger_supremum': top, 'selected_gap_to_supremum': top-kappa, + 'BIT_headroom_over_selected_kappa': B-kappa, + 'BIT_threshold_at_selected_kappa': 'any B > kappa'} + + +def encode(value): + if isinstance(value, Q): + return str(value) + if isinstance(value, dict): + return {k: encode(v) for k, v in value.items()} + if isinstance(value, list): + return [encode(v) for v in value] + return value + + +def main(): + module = load_ledger() + rng = random.Random(20261027) + check_inventory(module) + result = { + 'theorem': 'feasible iff OLD_BASELINE < kappa < min(U, B, 1/32)', + 'OLD_BASELINE': module.OLD_BASELINE, + 'checks_total': 58, + 'chain_checks_bound': check_chain_bindings(module, rng), + 'witnesses_passed': check_witnesses(module, rng), + 'random_feasible_points_inside_region': check_necessity_samples(module, rng), + 'controls': check_controls(module), + 'selected': selected_corollary(module), + } + digest = sha256() + for path in sorted(HERE.iterdir()): + if path.is_file() and path.suffix in {'.py', '.md', '.json'}: + digest.update(path.name.encode()+b'\0'+path.read_bytes()) + print('RESULT '+json.dumps(encode(result), sort_keys=True)) + print('PACKAGE_SHA256 '+digest.hexdigest()) + print('PASS_OUTER_LEDGER_KAPPA_REGION') + + +if __name__ == '__main__': + main()