Prove the exact κ region of the selected outer ledger: min(U, B, 1/32) (no new κ)

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.

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.

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"
+    }
+  ]
+}

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."
+    }
+  ]
+}

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."
+    }
+  ]
+}