From 741d4fa5b60168bfd0b66de51d7b8b94324f402f Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Tue, 13 Oct 2026 19:11:44 -0400 Subject: [PATCH 1/3] Add coverage-law relief thresholds for the selected complex local word (no new kappa) --- .../complex-coverage-law-relief/README.md | 196 +++++++++ .../complex-coverage-law-relief/SOURCES.json | 24 ++ .../complex-coverage-law-relief/TASK-CARD.md | 79 ++++ .../complex-coverage-law-relief/TASK.json | 72 ++++ .../complex-coverage-law-relief/VERIFY.json | 21 + .../complex-coverage-law-relief/verify.py | 403 ++++++++++++++++++ 6 files changed, 795 insertions(+) create mode 100644 research/complex-coverage-law-relief/README.md create mode 100644 research/complex-coverage-law-relief/SOURCES.json create mode 100644 research/complex-coverage-law-relief/TASK-CARD.md create mode 100644 research/complex-coverage-law-relief/TASK.json create mode 100644 research/complex-coverage-law-relief/VERIFY.json create mode 100644 research/complex-coverage-law-relief/verify.py diff --git a/research/complex-coverage-law-relief/README.md b/research/complex-coverage-law-relief/README.md new file mode 100644 index 0000000000..45c6f94705 --- /dev/null +++ b/research/complex-coverage-law-relief/README.md @@ -0,0 +1,196 @@ +# Coverage-law relief thresholds for the selected complex local word + +**Scoped obstruction and exact threshold table under the optimistic relaxation. +No new kappa, no supplier admission; the selected record is unchanged.** + +## Scope + +Card `complex-new-helper-inventory` (complex-mechanisms track, chooser nonce +`6ddf1b6647d8c5131033b16d30f0045b`), scope **refined** to the card's first +experiment: the complete optimistic child histogram, used to reject interface +routes without headroom. The card asks for a new physically realizable helper +inventory; this package instead quantifies the screen itself on **changed +coverage-law interfaces**, answering the coverage-law half of +[PR #1240](https://github.com/CrocSwap/integer-mult-bounds/pull/1240)'s open +question. The full task card is in [TASK-CARD.md](TASK-CARD.md); structured +scope metadata is in [TASK.json](TASK.json). + +## Model and object + +The hosted nine-stage coverage law of the selected line (semantics follow +PR1012's coverage identity and PR #1240's moment model; the arithmetic here is +written independently): + +- width `m = 73`; per call `w = families/stages = 896/9` live data families; +- coverage identity: paid rank mass + idle mass = `(m − unpaid)·w + centre` + (selected line: `unpaid = 1`, `centre = 64`); deficit `D = unpaid·w − centre`; +- the selected #1094 local word per call is `{1:2412, 2:418, 3:432, 4:142, + 5:82, 8:8}` (paid mass 5586), recorded at `research/gauge44-slots-t16/README.md`; +- idle/remainder children have rank at most `R = 51` (halving guard `m² > 2R²`); + the optimistic relaxation allows fractional counts and puts all idle mass at `R`. + +Total mass per call is 7232 (idle 1646), reproduced exactly. The relaxation +moment `relax(a)` is increasing in the saving `a`; the packing ceiling `a*` +solves `relax(a*) = 1`. A failing relaxation (moment above one at a target) +falsifies **every** construction with those interface parameters; a passing one +is optimistic only. + +Two targets: + +- **T1 (headline):** `a = 1/99`, equivalently `κ = 0.01` under the retained + transfer `κ = a/(1+a)`. +- **T2 (unbinding):** `a = κ_bit/(1 − κ_bit)` with `κ_bit = + 1733427039589844234749/10^24`, the bit saving pinned by + `scripts/research_baseline.py` at the base commit. This is where the complex + side would stop binding over that bit supplier. The incumbent ceiling + `a* = 0.001690054109088696` (κ ≈ 0.00168720) is below T2, so **pure repacking + of the selected word cannot unbind the complex side**; an interface change is + required even for the near target. + +## Results (all brackets certified with exact rational intervals) + +Positive control: `a* = 0.001690054109088696` reproduces PR #1240's grid +ceiling `a < 0.001690054109089` to within one 1e-15 grid step. + +| Lever (others at the selected line) | T2: unbinding (`a = 0.001736437026484097`) | T1: `a = 1/99` | +|---|---|---| +| unpaid coordinates per family `u` | `u* ∈ (1.009826689, 1.009826689)`; least integer 2 | `u* ∈ (2.804078009, 2.804078010)`; least integer 3 | +| centre charge `c` (from 64) | `c* ∈ (63.021698514, 63.021698515)`: met iff `c ≤ c*` | **impossible**: sup `a* = 0.004711142955614` at `c = 0` | +| families per replica `F` (stages 9) | least met `F = 906` (905 fails) | least met `F = 3093` (3092 fails) | +| paid-word count scale `s` | met iff `s ≤ 0.969437086` | met iff `s ≤ 0.049110034` | + +Pair points at `F = 896`: + +- `(u=2, c=0)`: `a* = 0.009357801683738 < 1/99`. So unpaid relief up to 2 + combined with **any** centre charge fails T1 (the sup over `c ∈ [0, 64]` is at + `c = 0`; `relax` is strictly decreasing in `u` and strictly increasing in `c`). +- `(u=3, c=64)`: `a* = 0.011001994530886 > 1/99`. Keeping three unpaid + coordinates per family optimistically suffices at the unchanged centre charge. + +Reading the T1 column as an interface budget: the headline target needs one of +three large changes — every live family keeping at least 2.804 unpaid +coordinates (integer 3 at `c = 64`), or a 3.45× larger template (3093 families +per replica at 9 stages), or a paid word at most 4.911% of its current counts +(a 95.1% reduction, consistent with PR #1240's independently derived "about 95% +lower fully priced local excess spend"). Centre-charge relief alone cannot reach +T1 at any `c ≥ 0`. T2 is much nearer: about 1% more unpaid coordinates, or one +unit off the 64 centre charge, or 906 families, or a 3.06% paid-count cut. + +## D/E diagnostic + +`a* < D/E` holds strictly (convexity: `(r/m)^(1-a) ≥ (r/m)(1 + a ln(m/r))`), +checked at four points: + +| Point | `D` | `E = Σ n_r r ln(m/r)` | `D/E` | `a*` | +|---|---|---|---|---| +| incumbent | `320/9` | `20973.176117977` | 0.001695287130359 | 0.001690054109089 | +| `u=2, c=0` | `1792/9` | `20914.519566200` | 0.009520233562185 | 0.009357801683738 | +| `u=3, c=64` | `704/3` | `20901.768141900` | 0.011227120360035 | 0.011001994530886 | +| `c=0` | `896/9` | `20950.223554238` | 0.004752004449872 | 0.004711142955614 | + +The diagnostic tracks the exact ceiling within 0.4% here, but the exact moment +is the acceptance test. + +## What this does and does not establish + +- Necessity holds inside the stated model: any construction on this local word, + template and outer recipe whose interface parameters miss every threshold + fails the moment, however it packs, hosts or repacks. +- Sufficiency is **optimistic-relaxation only**: fractional idle, all idle at the + cheapest admissible rank, no added charges. No physical realizability, owner + map, finite invoice or cold replay is claimed. The card's acceptance gate (a + new physically realizable contract) is **not** met by this package. +- The `u`, `c` and pair thresholds are at `F = 896` families; the `F` and `s` + thresholds are at the selected `u = 1, c = 64`. Changing several levers at once + can meet a target below each single-lever threshold (see open questions). +- `u > 1` and any `c ≠ 64` are what-if coverage laws. PR1012's identity is + re-checked only at the selected point; a realized `u ≥ 3` would itself be a + changed interface contract needing its own admission. +- `κ = a/(1+a)` is the retained planning transfer, not a theorem; T2 uses the + bit supplier pinned at the base commit, and any bit-side improvement moves it. +- All inherited all-size/compiler, common-label/mutable-source, whole-call + hosting, precision/tape, analytic-transfer and bit H1–H5 assumptions remain. + This is not a full Lean multiplication theorem. + +## Boundary with existing work + +- [PR #1240](https://github.com/CrocSwap/integer-mult-bounds/pull/1240) + (Douglas Colkitt) derives the coverage-law moment model and the fixed-word + packing ceiling, and names the coverage-law change as open. This package + answers that question with independently written, code-disjoint exact + interval arithmetic; its `unpaid` what-if parameter is used here as a search + lever. +- The pending stacked branches of [PR #1240](https://github.com/CrocSwap/integer-mult-bounds/pull/1240) + and [PR #1272](https://github.com/CrocSwap/integer-mult-bounds/pull/1272) + carry a `levers.py` ideal-budget table (first-order multiples per lever) that + #1272's proposed `centre-path-sharing` and `coverage-law-change` cards cite. + This package is complementary: it certifies exact threshold brackets (not + first-order multiples) at two targets, adds the families and paid-word-scaling + levers, least-integer thresholds, the `(u=2, c=0)` pair obstruction and the + `a* < D/E` convexity margins, and ships as a package on the base commit. +- [PR #1264](https://github.com/CrocSwap/integer-mult-bounds/pull/1264) screens + 14 open claims at the **unchanged** coverage law; nothing there varies the + interface. +- [PR #1272](https://github.com/CrocSwap/integer-mult-bounds/pull/1272) + (pending) narrows this card with a ceiling screen; this package is that screen + applied to changed interfaces. +- Ali Romman's `research/heterogeneous-owner-assembly/` bounds every mixture of + the frozen catalogue's 25 cost interfaces and explicitly excludes new + helper-inventory interfaces such as PR1004/1005's R489/R480. The thresholds + here price what such a new interface would have to deliver. +- Distinct from discussion #1265 (within-group idle repartitions at a fixed + coverage law) and discussion #1315 (X2 acceptance boundary for the selected + owner map). + +## Reproduce + +Python 3.11+, standard library only, from the repository root: + +```sh +python3 -I -B research/complex-coverage-law-relief/verify.py +python3 scripts/research_package.py --package research/complex-coverage-law-relief --check-only +python3.12 scripts/research_package.py --package research/complex-coverage-law-relief +``` + +Expected final line: + +```text +PASS_COMPLEX_COVERAGE_LAW_RELIEF +``` + +Add `--out /new/file.json` for the complete certificate (model, targets, every +threshold bracket as exact fractions, pair points, D/E diagnostics, check log). +Failure controls: `unpaid = 0`, halving-guard `R = 52`, a negative centre charge +and an over-paid word are rejected; one extra rank-1 child lowers the ceiling; +nine extra families raise it. + +## Open next questions + +See [TASK.json](TASK.json) for the structured list: + +1. **Can any physically realizable helper inventory move a lever past a + threshold?** First step: map PR1004/1005's R489/R480 interfaces onto + `(u, c, F, s)` and price them here. Blocked on an admission proof that a known + interface change corresponds to a coverage-identity change rather than a + repacking. +2. **Thresholds for the #1148 joint-entrance words** (whose packing caps are + 0.17–0.21% below the selected word's). First step: pin one joint-entrance + profile from PR #1264's `SNAPSHOT.json` and rerun the table. Blocked on the + profile not being in the base tree. +3. **The exact combined `(u, c)` and `(F, s)` Pareto surface at 1/99.** First + step: a certified 2D grid in `verify.py`; not blocked, cheap. + +## Credit + +Contributor: **Navinor**, with help from opencode. Apache-2.0. + +Predecessors: PR1012's coverage identity; PR +https://github.com/CrocSwap/integer-mult-bounds/pull/1240 and +https://github.com/CrocSwap/integer-mult-bounds/pull/1264 (Douglas Colkitt) for +the moment model, the fixed-word ceiling and the open question; the selected +local word and its lineage (see `certificates/selected-result.json` and +`research/gauge44-slots-t16/README.md`); Ali Romman's +`research/heterogeneous-owner-assembly/` for the frozen-catalogue boundary. All +construction credit for the selected line stays with the authors listed in the +selected record's review. No human review or full formal verification is claimed +for this package. diff --git a/research/complex-coverage-law-relief/SOURCES.json b/research/complex-coverage-law-relief/SOURCES.json new file mode 100644 index 0000000000..abd5f6df21 --- /dev/null +++ b/research/complex-coverage-law-relief/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "research/gauge44-slots-t16/README.md", + "usage": "input", + "git_blob": "0262339347a739be25b24860e96b4a20dd774807", + "sha256": "e33534891b32397220d29cd60943a71b863b606e734d71902349e4cac78a1a35" + } + ] +} diff --git a/research/complex-coverage-law-relief/TASK-CARD.md b/research/complex-coverage-law-relief/TASK-CARD.md new file mode 100644 index 0000000000..0584fe0a30 --- /dev/null +++ b/research/complex-coverage-law-relief/TASK-CARD.md @@ -0,0 +1,79 @@ +# Local task card (autoresearch.md section 3) + +Task ID / proposed scope key: `complex-new-helper-inventory` / `5868e5281a1e63d41a22` +(chosen by `scripts/choose_research_task.py`, track `complex-mechanisms`, OS-random +nonce `6ddf1b6647d8c5131033b16d30f0045b`). + +Base commit: `bce54fb3f895cbe5cd4c0eb477c3afeed100190f`. + +Exact predecessors / dependency heads (read-only, not vendored): +- PR https://github.com/CrocSwap/integer-mult-bounds/pull/1240 head + `1e136b8c4a552050820334ad113628775182f08c` — coverage-law moment model and the + incumbent-word packing ceiling `a < 0.001690054109089` (semantics reference only; + this package's arithmetic is written independently). +- PR1012 coverage identity (via #1240 and `research/community-batch1099-audit`): + paid rank mass = `(m - unpaid) * W + centre * N` per template. +- `research/heterogeneous-owner-assembly/` (Ali Romman) — frozen provider-catalogue + mixture bound; its controls already reject the U10 delta (PR987) and the R489/R480 + helper-inventory changes (PR1004/1005), so new cost interfaces are outside it. + +Concrete object and question: +The hosted nine-stage coverage law of the selected line: width `m = 73`, +`w = families/stages = 896/9` live families per call, centre charge `64` per call, +`unpaid = 1` coordinate per family, halving-guard idle rank cap `R = 51`, with the +selected #1094 local word `{1:2412, 2:418, 3:432, 4:142, 5:82, 8:8}` (paid mass +5586 per call). Question: which changes of the local cost interface (unpaid +coordinates per family `u`, centre charge `c`, families per call `w`, and paid-word +excess spend `E`) are *necessary and which are sufficient* for the optimistic +whole-construction moment to admit saving `a >= 1/99`, and what are the exact +thresholds and trade-offs between them? + +Scope status: **refined**. The card asks for a new physically realizable helper +inventory; this session runs the card's stated first experiment (the complete +optimistic child histogram, rejecting routes without headroom) on *changed +coverage-law interfaces* instead of proposing a full new contract. Reason: the +optimistic screen is what decides whether any contract with given interface +parameters can have headroom at all, and #1240's open question asks for exactly +this quantification on the coverage-law side. + +Existing restriction being changed (or exact claim audited): +The coverage-law parameters `(unpaid=1, centre=64, families=896, stages=9)` and +the paid-word excess spend of the incumbent word; audited claim is the optimism +of the relaxation itself (fractional idle counts, all repackings allowed). + +Method; explicit parameter ranges / candidate alphabet: +Independent stdlib exact-rational interval moment (atanh-chain logarithm, Taylor +exponential with Lagrange remainder, outward rounding), bisection ceiling in `a`. +Domain: `u` in {1,...,12} integer and the exact continuous threshold in `(1, 12]`; +`c` in [0, 64] rational; `w` in [50, 2000] families per call at `stages = 9` +(families integer 450..18000); paid-word excess spend scaled continuously down +from the incumbent's. Positive control: reproduce #1240's incumbent ceiling. +Failure controls: mutated profile, halving-guard violation, over-paid word. + +Nearest overlapping PRs and why this adds something: +- #1240 screens one fixed word's repacking ceiling and states the coverage-law + change as an open direction; this package quantifies that direction exactly. +- #1264 screens 14 open claims' words at the *unchanged* coverage law; it does not + vary interface parameters. +- #1272 (director, pending) narrows this card with a ceiling screen; this package + is the screen applied to changed interfaces, consistent with that narrowing. +- Discussion #1265 covers within-group idle repartitions at fixed coverage law. + +Optimistic full cost budget; required observable improvement: +The relaxation already grants fractional idle, all idle at the cheapest admissible +rank and no extra charges; thresholds computed here are necessary conditions for +any realized construction (a failing relaxation falsifies the route) and optimistic +sufficiency only (a passing relaxation is not a contract). Observable improvement: +certified brackets showing `relax(1/99) < 1` or `> 1` at each named threshold. + +Success evidence; falsification test; time/compute cap: +Success = exact interval reproduction of the incumbent ceiling plus a threshold +table with certified brackets. Falsification = any control mutation accepted. +Compute cap: minutes of stdlib runtime; no network beyond the board/PR checks. + +Predecessor authors; intended artifact and reproduction command: +Douglas Colkitt (#1240/#1264/#1240's coverage-law model; PR1012 identity), +Ali Romman (heterogeneous-owner-assembly), the selected-line authors (see +`certificates/selected-result.json`). Artifact: `research/complex-coverage-law-relief/` +with `verify.py`; reproduction `python3 -I -B research/complex-coverage-law-relief/verify.py`. +Contributor: Navinor, with help from opencode. diff --git a/research/complex-coverage-law-relief/TASK.json b/research/complex-coverage-law-relief/TASK.json new file mode 100644 index 0000000000..2c1fc798fc --- /dev/null +++ b/research/complex-coverage-law-relief/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 2, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract, not another mixture already covered by the frozen catalogue.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the frozen catalogue bound exclusions and select one genuinely different helper endpoint inventory.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write the complete optimistic child histogram and reject it immediately if even the relaxation has insufficient headroom.", + "bottleneck_link": "Helper inventory changes can improve the moment; repacking a covered cost interface cannot evade its scoped bound.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "refined", + "actual_scope": "Exact relief thresholds and scoped obstructions for the hosted nine-stage coverage-law interface (unpaid coordinates per family u, centre charge c, families per call, paid-word excess spend) behind the selected #1094 complex local word, under the optimistic whole-construction moment; targets are a = 1/99 and the retained-transfer unbinding saving a = kappa_bit/(1-kappa_bit).", + "scope_change_reason": "The card asks for a new physically realizable helper inventory. This session runs the card's stated first experiment (the complete optimistic child histogram, rejecting routes without headroom) on changed coverage-law interfaces instead of proposing a full new contract, because the optimistic screen decides whether any contract with given interface parameters can have headroom at all, and PR #1240's open question asks for exactly this quantification on the coverage-law side. Necessity claims hold for every construction inside the model; sufficiency is optimistic-relaxation only.", + "bottleneck_link": "The card's question is whether a new local cost interface can change the deficit-to-recursive-cost ratio D/E beyond current packing. The thresholds quantify which interface levers move D/E past the binding complex budget: the deficit D = u*w - c and the recursive spend E both live in the coverage law, so a changed helper inventory can help only through one of these four levers.", + "budget_minutes": 60, + "stop_rule": "One bounded experiment: certified thresholds for the four levers plus the (u=2, c=0) and (u=3, c=64) pair points on the incumbent word; stop at the first table, no wider search without a physically realizable contract.", + "outcome": "completed", + "evidence": "PASS_COMPLEX_COVERAGE_LAW_RELIEF from research/complex-coverage-law-relief/verify.py: incumbent ceiling reproduced (a* = 0.0016900541090887 vs PR #1240's grid ceiling 0.001690054109089); T1 (1/99) needs u* in (2.804078009, 2.804078010) or F* = 3093 families or paid counts <= 4.911% of current, and centre relief alone is impossible (sup a* at c = 0 is 0.004711142955614 < 1/99; u <= 2 with any centre charge also fails: sup 0.009357801683738 at (u=2, c=0)); u = 3 at unchanged c = 64 optimistically suffices (a* = 0.011001994530886). T2 (unbinding) needs u* in (1.009826689, 1.009826689), or c <= 63.021698515, or F* = 906 families, or paid counts <= 96.9437086%. D/E diagnostic and eight failure controls pass; certificate in the verify --out JSON.", + "author": "Navinor", + "ai_assistance": "Substantial assistance from opencode (the OpenCode agent harness); contributor Navinor.", + "open_questions": [ + { + "question": "Can any physically realizable helper inventory move a coverage-law lever past a threshold: keep u >= 2.804 unpaid coordinates per family, cut the centre charge to <= 63.02, or shrink the paid word to <= 4.911% of its counts?", + "why_it_matters": "These are the only levers that move the binding complex budget inside this model; a contract that realizes one would change the frontier, and one that cannot is a closed route.", + "first_step": "Map the already-admitted helper-inventory changes PR1004/1005's R489/R480 (rejected by research/heterogeneous-owner-assembly's controls as outside the frozen catalogue) onto the (u, c, F, s) levers and price their endpoint with this verifier.", + "blocked_by": "No admission proof yet that any known interface change corresponds to a coverage-identity change rather than a repacking." + }, + { + "question": "What are the same thresholds for the #1148 joint-entrance local words, which #1264 shows have lower packing caps than the selected word?", + "why_it_matters": "The leading open claim line packs words with caps 0.17-0.21% below the selected word's; its relief thresholds may be worse or better than the selected word's, changing which line deserves construction effort.", + "first_step": "Pin one joint-entrance profile (e.g. from PR #1264's SNAPSHOT.json at head 1be64e9ef79fe11f24f05b62b0fd7d70be0b7b4c) and rerun this package's table with that profile as the word.", + "blocked_by": "The joint-entrance profiles are not in the base tree; a pinned PR blob or an in-tree package is needed as the word source." + }, + { + "question": "What is the exact combined Pareto surface of (u, c) and (F, s) at the 1/99 target, not just the single-lever thresholds and the two pair points?", + "why_it_matters": "A construction that can afford small relief on two levers may be easier to realize than one large single-lever change; the surface prices every combination exactly.", + "first_step": "Extend verify.py with a 2D grid over u in [1, 3] x c in [0, 64] at target 1/99 and certify each cell's sign; the machinery already exists and the run is minutes.", + "blocked_by": "Nothing; cheap follow-up." + } + ] +} diff --git a/research/complex-coverage-law-relief/VERIFY.json b/research/complex-coverage-law-relief/VERIFY.json new file mode 100644 index 0000000000..44a61877a4 --- /dev/null +++ b/research/complex-coverage-law-relief/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/gauge44-slots-t16/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Coverage identity (7232 total, 1646 idle), positive fixture reproducing PR #1240's incumbent grid ceiling, certified threshold brackets for the four interface levers at both targets, the (u=2, c=0) pair obstruction and (u=3, c=64) sufficiency point, the a* < D/E convexity margin at four points, and failure controls: unpaid=0, halving-guard R=52, negative centre, over-paid word, one-extra-rank-1 mutant, F+9 monotone control." + } + ] +} diff --git a/research/complex-coverage-law-relief/verify.py b/research/complex-coverage-law-relief/verify.py new file mode 100644 index 0000000000..176b337ac3 --- /dev/null +++ b/research/complex-coverage-law-relief/verify.py @@ -0,0 +1,403 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact relief thresholds for the coverage law behind the selected complex local word. + +Model (all inputs explicit; semantics follow PR1012's coverage identity and the +moment model of https://github.com/CrocSwap/integer-mult-bounds/pull/1240, whose +arithmetic is NOT imported here): + + * width m = 73; a call has w = families / stages live data families (selected + line: 896 families over 9 stages); + * coverage identity: paid rank mass + idle mass = (m - unpaid) * w + centre, + i.e. each live family keeps `unpaid` unpaid coordinates (1 on the selected + line) and each call pays a centre path of `centre` (64 on the selected line); + * the local word fixes its paid child profile per call (the selected #1094 word + is {1:2412, 2:418, 3:432, 4:142, 5:82, 8:8}, mass 5586, recorded at + research/gauge44-slots-t16/README.md and re-priced by PR #1240); + * all remaining mass is idle/remainder children of rank at most R, where the + outer halving guard m^2 > 2 R^2 gives R = 51 at m = 73. + +For a >= 0 a child of rank r costs (r/m)^(1-a); with idle mass M at fixed ranks +<= R the cheapest idle histogram puts all of M into (possibly fractional) rank-R +children, so the optimistic relaxation moment per call is + + relax(a) = [ sum_local n_r (r/m)^(1-a) + (M/R) (R/m)^(1-a) ] / w . + +relax is increasing in a; the packing ceiling a* solves relax(a*) = 1. A failing +relaxation (relax(a_t) > 1 at target a_t) falsifies every construction with those +interface parameters; a passing one is optimistic only (no realizability claim). + +This package computes certified brackets for a* and for the exact interface +thresholds that put a* above two targets: a = 1/99 (headline planning target) +and a = kappa_bit/(1 - kappa_bit) (the retained-transfer unbinding target where +the complex side would stop binding over the pinned bit supplier). + +Exact rational intervals: ln via atanh chains, exp by Taylor series with a +geometric tail bound, outward rounding to 2^-PREC. Standard library only. +Contributor: Navinor, with help from opencode. Apache-2.0. +""" +import argparse +import json +from fractions import Fraction as Q +from functools import lru_cache +from math import isqrt + +PREC = 256 + +M = 73 +STAGES = 9 +FAMILIES0 = 896 +CENTRE0 = 64 +UNPAID0 = 1 +WORD = {1: 2412, 2: 418, 3: 432, 4: 142, 5: 82, 8: 8} # selected #1094 local word per call +WORD_MASS = sum(r * n for r, n in WORD.items()) # 5586 +# PR #1240 reports the incumbent ceiling as a < 0.001690054109089 (positive control). +REF_CEILING = Q(1690054109089, 10 ** 15) +# scripts/research_baseline.py at the base commit: bit_saving = 1733427039589844234749/10^24. +KAPPA_BIT = Q(1733427039589844234749, 10 ** 24) +A_T1 = Q(1, 99) # headline target +A_T2 = KAPPA_BIT / (1 - KAPPA_BIT) # unbinding target, retained kappa = a/(1+a) + + +def require(ok, why): + if not ok: + raise ValueError(why) + + +def down(x): + return Q((x.numerator << PREC) // x.denominator, 1 << PREC) + + +def up(x): + return -down(-x) + + +@lru_cache(None) +def atanh(t): + """[lo, hi] enclosure of atanh(t) for rational 0 < t <= 1/3.""" + require(0 < t <= Q(1, 3), 'atanh range') + s, p, k = Q(0), t, 0 + while True: + term = p / (2 * k + 1) + s += term + p *= t * t + k += 1 + tail = p / ((2 * k + 1) * (1 - t * t)) + if tail < Q(1, 1 << (PREC + 8)): + return down(s), up(s + tail) + + +@lru_cache(None) +def ln_int(k): + """[lo, hi] enclosure of ln k for integer k >= 1: ln k = ln(k-1) + 2 atanh(1/(2k-1)).""" + require(isinstance(k, int) and k >= 1, 'ln domain') + if k == 1: + return Q(0), Q(0) + lo, hi = ln_int(k - 1) + a, b = atanh(Q(1, 2 * k - 1)) + return down(lo + 2 * a), up(hi + 2 * b) + + +def exp_pair(lo, hi): + """[lo', hi'] enclosure of exp([lo, hi]) for 0 <= lo <= hi <= 1/2.""" + require(0 <= lo <= hi <= Q(1, 2), 'exp range') + + def series(y, upper): + s, t, k = Q(1), Q(1), 0 + while True: + k += 1 + t = t * y / k + s += t + if t * y < Q(1, 1 << (PREC + 8)): + return up(s + 2 * t * y / (k + 1)) if upper else down(s) + + return series(lo, False), series(hi, True) + + +def child_cost(r, a): + """[lo, hi] enclosure of (r/m)^(1-a) = (r/m) * exp(a * ln(m/r)), 0 <= a <= 1/20.""" + require(0 <= a <= Q(1, 20) and 0 < r < M, 'child cost domain') + lm, um = ln_int(M) + lr, ur = ln_int(r) + e = exp_pair(a * max(Q(0), lm - ur), a * (um - lr)) + return down(Q(r, M) * e[0]), up(Q(r, M) * e[1]) + + +def max_idle_rank(m): + """Largest R with m^2 > 2 R^2 (outer halving guard).""" + r = isqrt((m * m - 1) // 2) + while 2 * (r + 1) ** 2 < m * m: + r += 1 + while 2 * r * r >= m * m: + r -= 1 + return r + + +R = max_idle_rank(M) + + +def model(local, unpaid=UNPAID0, centre=CENTRE0, families=FAMILIES0, stages=STAGES, rank_cap=R): + """Per-call coverage quantities; Fraction counts allowed.""" + require(2 * rank_cap * rank_cap < M * M, 'idle rank cap violates the halving guard') + require(1 <= unpaid < M, 'unpaid coordinates per family') + require(0 <= centre, 'centre charge') + require(stages >= 1 and families >= 1, 'template counts') + require(all(0 < r < M for r in local) and all(n >= 0 for n in local.values()), 'local profile') + w = Q(families) / stages + require(unpaid * w > centre, 'coverage deficit is not positive') + total = (M - unpaid) * w + centre + local_mass = sum(r * Q(n) for r, n in local.items()) + idle = total - local_mass + require(idle >= 0, 'local word pays more mass than the coverage law allows') + return dict(w=w, total=total, local_mass=local_mass, idle=idle, deficit=unpaid * w - centre) + + +def relax(local, a, unpaid=UNPAID0, centre=CENTRE0, families=FAMILIES0, stages=STAGES, rank_cap=R): + """[lo, hi] enclosure of the per-call relaxation moment at saving a.""" + q = model(local, unpaid, centre, families, stages, rank_cap) + lo = hi = Q(0) + for r, n in local.items(): + c = child_cost(r, a) + lo, hi = lo + Q(n) * c[0], hi + Q(n) * c[1] + c = child_cost(rank_cap, a) + k = q['idle'] / rank_cap + lo, hi = lo + k * c[0], hi + k * c[1] + return down(lo / q['w']), up(hi / q['w']) + + +def moment_sign(local, a, **kw): + """-1: moment below one at a; +1: above one. Raises if the enclosure straddles.""" + lo, hi = relax(local, a, **kw) + if hi < 1: + return -1 + if lo > 1: + return 1 + raise ValueError('moment enclosure straddles one') + + +def ceiling(local, grid=Q(1, 10 ** 18), **kw): + """Bracket [a_lo, a_hi] of the packing ceiling a*: relax(a_lo) < 1 < relax(a_hi).""" + lo, hi = Q(0), Q(1, 20) + require(moment_sign(local, hi, **kw) > 0, 'search window too small') + require(moment_sign(local, lo, **kw) < 0, 'relaxation has no positive saving') + while hi - lo > grid: + mid = (lo + hi) / 2 + if moment_sign(local, down(mid), **kw) < 0: + lo = down(mid) + else: + hi = up(mid) + return lo, hi + + +def target_met(local, a_t, **kw): + """True iff the relaxation admits saving >= a_t (moment below one at a_t).""" + return moment_sign(local, a_t, **kw) < 0 + + +def bisect_param(met, lo, hi, grid): + """Certified bracket [p_lo, p_hi] with met increasing in p: not met(p_lo), met(p_hi).""" + lo, hi = Q(lo), Q(hi) + require(met(hi) and not met(lo), 'parameter bracket does not straddle the threshold') + while hi - lo > grid: + mid = (lo + hi) / 2 + if met(mid): + hi = mid + else: + lo = mid + return lo, hi + + +def de_diagnostic(local, unpaid=UNPAID0, centre=CENTRE0, families=FAMILIES0, stages=STAGES): + """D = m*w - total mass (exact) and E = sum n_r r ln(m/r) over local + rank-R idle. + + First-order diagnostic: a* <= D/E (strict for a* > 0), from (r/m)^(1-a) >= + (r/m)(1 + a ln(m/r)) and relax(a*) = 1. + """ + q = model(local, unpaid, centre, families, stages) + d = M * q['w'] - q['total'] + lo = hi = Q(0) + counts = dict(local) + counts[R] = counts.get(R, Q(0)) + q['idle'] / R + for r, n in counts.items(): + lm, um = ln_int(M) + lr, ur = ln_int(r) + lo += Q(n) * r * down(lm - ur) + hi += Q(n) * r * up(um - lr) + return d, lo, hi + + +class Report: + def __init__(self): + self.lines = [] + self.cert = {} + + def check(self, ok, name, detail): + if not ok: + raise AssertionError('FAIL_' + name + ': ' + detail) + self.lines.append('PASS ' + name + ' ' + detail) + + +def frac_str(x): + return f'{x.numerator}/{x.denominator}' + + +def dec(x, digits=15): + return f'{float(x):.{digits}f}' + + +def run(out_path): + rep = Report() + + # --- model identity: coverage law reproduces the recorded 7232 total and 1646 idle. + q = model(WORD) + rep.check(q['total'] == Q(7232) and q['idle'] == Q(1646), 'COVERAGE_IDENTITY', + f"total={q['total']} idle={q['idle']} w={frac_str(q['w'])} deficit={frac_str(q['deficit'])}") + + # --- positive control: reproduce PR #1240's incumbent ceiling. + # #1240 reports the first 1e-15 grid point above a*, so its number is an upper + # bound; require our true bracket to sit within one grid step below it. + lo, hi = ceiling(WORD) + rep.check(hi - lo <= Q(2, 10 ** 18) and hi <= REF_CEILING and lo >= REF_CEILING - Q(1, 10 ** 15), + 'INCUMBENT_CEILING', + f'a* in [{dec(lo, 18)}, {dec(hi, 18)}] vs #1240 grid ceiling {dec(REF_CEILING, 15)}') + rep.cert['incumbent_ceiling'] = {'a_lo': frac_str(lo), 'a_hi': frac_str(hi), + 'decimal': dec(hi, 18), 'pr1240_reported': dec(REF_CEILING, 15)} + + # --- targets: T2 (unbinding) is the nearer goal, above the incumbent packing ceiling. + rep.check(0 < A_T2 < A_T1 and A_T2 > REF_CEILING, 'TARGETS', + f'a_T1=1/99={dec(A_T1)} a_T2={frac_str(A_T2)}={dec(A_T2, 18)}') + rep.cert['targets'] = {'a_T1': '1/99', 'a_T2': frac_str(A_T2), 'kappa_bit': frac_str(KAPPA_BIT)} + + # --- unpaid-coordinate threshold u* (continuous bracket + least integer). + u_res = {} + for tag, a_t in (('T1', A_T1), ('T2', A_T2)): + met = lambda u, a_t=a_t: target_met(WORD, a_t, unpaid=u) + ulo, uhi = bisect_param(met, Q(1), Q(12), Q(1, 10 ** 9)) + ints = [u for u in range(1, 13) if met(Q(u))] + least = ints[0] + rep.check(met(Q(least)) and (least == 1 or not met(Q(least - 1))), + f'UNPAID_THRESHOLD_{tag}', + f'u* in ({dec(ulo, 9)}, {dec(uhi, 9)}); least integer u = {least}') + u_res[tag] = {'u_lo': frac_str(ulo), 'u_hi': frac_str(uhi), 'least_integer': ints[0]} + rep.cert['unpaid_thresholds'] = u_res + + # --- centre-charge threshold c* (met for c <= c*). + c_res = {} + for tag, a_t in (('T1', A_T1), ('T2', A_T2)): + met = lambda c, a_t=a_t: target_met(WORD, a_t, centre=c) + try: + clo, chi = bisect_param(lambda c: not met(c), Q(0), Q(64), Q(1, 10 ** 9)) + c_res[tag] = {'c_lo': frac_str(clo), 'c_hi': frac_str(chi), 'met_at_zero': met(Q(0))} + rep.check(met(clo) and not met(chi), f'CENTRE_THRESHOLD_{tag}', + f'c* in ({dec(clo, 9)}, {dec(chi, 9)}); target met iff c <= c*') + except ValueError: + # Not met even at c = 0: certified obstruction for centre relief alone. + lo0, hi0 = ceiling(WORD, centre=Q(0)) + rep.check(hi0 < a_t, f'CENTRE_OBSTRUCTION_{tag}', + f'no c in [0,64] meets the target; sup a* at c=0 in ({dec(lo0, 15)}, {dec(hi0, 15)})') + c_res[tag] = {'obstruction': True, 'a_star_c0_lo': frac_str(lo0), 'a_star_c0_hi': frac_str(hi0)} + rep.cert['centre_thresholds'] = c_res + + # --- families-per-call threshold F* at stages = 9 (met for F >= F*). + # The floor 693 is the least families with total mass >= the word's 5586. + f_res = {} + for tag, a_t in (('T1', A_T1), ('T2', A_T2)): + met = lambda f, a_t=a_t: target_met(WORD, a_t, families=f) + flo, fhi = bisect_param(met, 693, 18000, Q(1)) + # integer tightening: scan down to the least integer families with the target met. + fmin = -(-fhi.numerator // fhi.denominator) + while fmin > 693 and met(fmin - 1): + fmin -= 1 + rep.check(met(fmin) and not met(fmin - 1), f'FAMILIES_THRESHOLD_{tag}', + f'F* in [{fmin - 1}+ , {fmin}] families per replica (w = F/9 per call)') + f_res[tag] = {'families_least': fmin, 'families_prev_not_met': fmin - 1, + 'w_at_threshold': frac_str(Q(fmin, STAGES))} + rep.cert['families_thresholds'] = f_res + + # --- paid-word scaling threshold s* (local counts * s, met for s <= s*). + s_res = {} + for tag, a_t in (('T1', A_T1), ('T2', A_T2)): + met = lambda s, a_t=a_t: target_met({r: n * s for r, n in WORD.items()}, a_t) + slo, shi = bisect_param(lambda s: not met(s), Q(0), Q(1), Q(1, 10 ** 9)) + rep.check(met(slo) and not met(shi), f'WORD_SCALING_{tag}', + f's* in ({dec(slo, 9)}, {dec(shi, 9)}); target met iff paid counts <= s* x current') + s_res[tag] = {'s_lo': frac_str(slo), 's_hi': frac_str(shi)} + rep.cert['word_scaling_thresholds'] = s_res + + # --- pair obstructions and sufficiency margins. + lo2, hi2 = ceiling(WORD, unpaid=2, centre=0) + rep.check(hi2 < A_T1, 'PAIR_UNPAID2_CENTRE0_OBSTRUCTION_T1', + f'sup a* at (u=2, c=0) in ({dec(lo2, 15)}, {dec(hi2, 15)}) < 1/99: unpaid relief up to 2 with any centre charge cannot reach T1') + lo3, hi3 = ceiling(WORD, unpaid=3, centre=CENTRE0) + rep.check(lo3 > A_T1, 'PAIR_UNPAID3_SUFFICIENCY_T1', + f'a* at (u=3, c=64) in ({dec(lo3, 15)}, {dec(hi3, 15)}) > 1/99 (optimistic sufficiency)') + rep.cert['pairs'] = {'u2_c0_T1': {'a_lo': frac_str(lo2), 'a_hi': frac_str(hi2)}, + 'u3_c64_T1': {'a_lo': frac_str(lo3), 'a_hi': frac_str(hi3)}} + + # --- D/E diagnostic and the convexity margin a* < D/E at named points. + de_res = {} + points = [('incumbent', {}), ('u2_c0', dict(unpaid=2, centre=0)), ('u3_c64', dict(unpaid=3)), + ('c0', dict(centre=0))] + for name, kw in points: + d, elo, ehi = de_diagnostic(WORD, **kw) + alo, ahi = ceiling(WORD, **kw) + # convexity: a* < D/E strictly, certified as a*_hi < (D/E)_lo = D/E_hi. + rep.check(d > 0 and ahi < d / ehi, f'DE_DIAGNOSTIC_{name}', + f'D={frac_str(d)} E in ({dec(elo, 9)}, {dec(ehi, 9)}) D/E ~ {dec(d / ehi, 15)} a* ~ {dec(ahi, 15)}') + de_res[name] = {'D': frac_str(d), 'E_lo': frac_str(elo), 'E_hi': frac_str(ehi), + 'a_star_lo': frac_str(alo), 'a_star_hi': frac_str(ahi)} + rep.cert['de_diagnostics'] = de_res + + # --- failure controls: each mutant must be rejected or strictly worse. + for bad, why in ((dict(unpaid=0), 'unpaid'), (dict(rank_cap=52), 'halving guard'), + (dict(centre=-1), 'negative centre')): + try: + model(WORD, **bad) + except ValueError: + rep.lines.append(f'PASS CONTROL_REJECT_{why.replace(" ", "_")}') + else: + raise AssertionError(f'FAIL_CONTROL_REJECT_{why}: accepted') + try: + model({1: WORD[1] + 2000, 2: 418, 3: 432, 4: 142, 5: 82, 8: 8}) + except ValueError: + rep.lines.append('PASS CONTROL_REJECT_over_paid_word') + else: + raise AssertionError('FAIL_CONTROL_REJECT_over_paid_word: accepted') + mutant = dict(WORD) + mutant[1] += 1 + mlo, mhi = ceiling(mutant) + rep.check(mhi < lo, 'CONTROL_MUTANT_ONE_EXTRA_RANK1_LOWERS_CEILING', + f'mutant a* ~ {dec(mhi, 15)} < incumbent ~ {dec(lo, 15)}') + m2lo, m2hi = ceiling(WORD, families=FAMILIES0 + 9) + rep.check(m2lo > hi, 'CONTROL_MONOTONE_FAMILIES', + f'F+9 raises a* to ~{dec(m2lo, 15)} > incumbent ~{dec(hi, 15)}') + + rep.cert['model'] = {'m': M, 'stages': STAGES, 'families': FAMILIES0, 'centre': CENTRE0, + 'unpaid': UNPAID0, 'idle_rank_cap': R, 'local_word': WORD, + 'local_mass': WORD_MASS} + rep.lines.append('PASS_COMPLEX_COVERAGE_LAW_RELIEF') + + print('\n'.join(rep.lines)) + if out_path: + with open(out_path, 'w', encoding='utf-8') as fh: + json.dump({'status': 'PASS_COMPLEX_COVERAGE_LAW_RELIEF', 'model': rep.cert['model'], + 'targets': rep.cert['targets'], 'incumbent_ceiling': rep.cert['incumbent_ceiling'], + 'unpaid_thresholds': rep.cert['unpaid_thresholds'], + 'centre_thresholds': rep.cert['centre_thresholds'], + 'families_thresholds': rep.cert['families_thresholds'], + 'word_scaling_thresholds': rep.cert['word_scaling_thresholds'], + 'pairs': rep.cert['pairs'], 'de_diagnostics': rep.cert['de_diagnostics'], + 'log': rep.lines}, fh, indent=2) + fh.write('\n') + return 0 + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument('--out', help='write the complete certificate JSON here') + args = ap.parse_args() + return run(args.out) + + +if __name__ == '__main__': + raise SystemExit(main()) From 6840924bf22523a9f0a965238a22cc3bcfc7297b Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Tue, 13 Oct 2026 19:19:32 -0400 Subject: [PATCH 2/3] Use full autolink citation forms in the coverage-law relief package --- .../complex-coverage-law-relief/README.md | 108 ++++++++++-------- .../complex-coverage-law-relief/TASK-CARD.md | 63 ++++++---- .../complex-coverage-law-relief/TASK.json | 12 +- .../complex-coverage-law-relief/VERIFY.json | 2 +- .../complex-coverage-law-relief/verify.py | 23 ++-- 5 files changed, 118 insertions(+), 90 deletions(-) diff --git a/research/complex-coverage-law-relief/README.md b/research/complex-coverage-law-relief/README.md index 45c6f94705..2702b3426f 100644 --- a/research/complex-coverage-law-relief/README.md +++ b/research/complex-coverage-law-relief/README.md @@ -11,21 +11,23 @@ experiment: the complete optimistic child histogram, used to reject interface routes without headroom. The card asks for a new physically realizable helper inventory; this package instead quantifies the screen itself on **changed coverage-law interfaces**, answering the coverage-law half of -[PR #1240](https://github.com/CrocSwap/integer-mult-bounds/pull/1240)'s open -question. The full task card is in [TASK-CARD.md](TASK-CARD.md); structured -scope metadata is in [TASK.json](TASK.json). +https://github.com/CrocSwap/integer-mult-bounds/pull/1240's open question. The +full task card is in [TASK-CARD.md](TASK-CARD.md); structured scope metadata is +in [TASK.json](TASK.json). ## Model and object The hosted nine-stage coverage law of the selected line (semantics follow -PR1012's coverage identity and PR #1240's moment model; the arithmetic here is +CrocSwap/integer-mult-bounds#1012's coverage identity and +CrocSwap/integer-mult-bounds#1240's moment model; the arithmetic here is written independently): - width `m = 73`; per call `w = families/stages = 896/9` live data families; - coverage identity: paid rank mass + idle mass = `(m − unpaid)·w + centre` (selected line: `unpaid = 1`, `centre = 64`); deficit `D = unpaid·w − centre`; -- the selected #1094 local word per call is `{1:2412, 2:418, 3:432, 4:142, - 5:82, 8:8}` (paid mass 5586), recorded at `research/gauge44-slots-t16/README.md`; +- the selected CrocSwap/integer-mult-bounds#1094 local word per call is + `{1:2412, 2:418, 3:432, 4:142, 5:82, 8:8}` (paid mass 5586), recorded at + `research/gauge44-slots-t16/README.md`; - idle/remainder children have rank at most `R = 51` (halving guard `m² > 2R²`); the optimistic relaxation allows fractional counts and puts all idle mass at `R`. @@ -49,8 +51,9 @@ Two targets: ## Results (all brackets certified with exact rational intervals) -Positive control: `a* = 0.001690054109088696` reproduces PR #1240's grid -ceiling `a < 0.001690054109089` to within one 1e-15 grid step. +Positive control: `a* = 0.001690054109088696` reproduces +https://github.com/CrocSwap/integer-mult-bounds/pull/1240's grid ceiling +`a < 0.001690054109089` to within one 1e-15 grid step. | Lever (others at the selected line) | T2: unbinding (`a = 0.001736437026484097`) | T1: `a = 1/99` | |---|---|---| @@ -71,10 +74,11 @@ Reading the T1 column as an interface budget: the headline target needs one of three large changes — every live family keeping at least 2.804 unpaid coordinates (integer 3 at `c = 64`), or a 3.45× larger template (3093 families per replica at 9 stages), or a paid word at most 4.911% of its current counts -(a 95.1% reduction, consistent with PR #1240's independently derived "about 95% -lower fully priced local excess spend"). Centre-charge relief alone cannot reach -T1 at any `c ≥ 0`. T2 is much nearer: about 1% more unpaid coordinates, or one -unit off the 64 centre charge, or 906 families, or a 3.06% paid-count cut. +(a 95.1% reduction, consistent with CrocSwap/integer-mult-bounds#1240's +independently derived "about 95% lower fully priced local excess spend"). +Centre-charge relief alone cannot reach T1 at any `c ≥ 0`. T2 is much nearer: +about 1% more unpaid coordinates, or one unit off the 64 centre charge, or 906 +families, or a 3.06% paid-count cut. ## D/E diagnostic @@ -103,9 +107,10 @@ is the acceptance test. - The `u`, `c` and pair thresholds are at `F = 896` families; the `F` and `s` thresholds are at the selected `u = 1, c = 64`. Changing several levers at once can meet a target below each single-lever threshold (see open questions). -- `u > 1` and any `c ≠ 64` are what-if coverage laws. PR1012's identity is - re-checked only at the selected point; a realized `u ≥ 3` would itself be a - changed interface contract needing its own admission. +- `u > 1` and any `c ≠ 64` are what-if coverage laws. + CrocSwap/integer-mult-bounds#1012's identity is re-checked only at the + selected point; a realized `u ≥ 3` would itself be a changed interface + contract needing its own admission. - `κ = a/(1+a)` is the retained planning transfer, not a theorem; T2 uses the bit supplier pinned at the base commit, and any bit-side improvement moves it. - All inherited all-size/compiler, common-label/mutable-source, whole-call @@ -114,33 +119,36 @@ is the acceptance test. ## Boundary with existing work -- [PR #1240](https://github.com/CrocSwap/integer-mult-bounds/pull/1240) - (Douglas Colkitt) derives the coverage-law moment model and the fixed-word - packing ceiling, and names the coverage-law change as open. This package - answers that question with independently written, code-disjoint exact - interval arithmetic; its `unpaid` what-if parameter is used here as a search - lever. -- The pending stacked branches of [PR #1240](https://github.com/CrocSwap/integer-mult-bounds/pull/1240) - and [PR #1272](https://github.com/CrocSwap/integer-mult-bounds/pull/1272) - carry a `levers.py` ideal-budget table (first-order multiples per lever) that - #1272's proposed `centre-path-sharing` and `coverage-law-change` cards cite. - This package is complementary: it certifies exact threshold brackets (not - first-order multiples) at two targets, adds the families and paid-word-scaling - levers, least-integer thresholds, the `(u=2, c=0)` pair obstruction and the - `a* < D/E` convexity margins, and ships as a package on the base commit. -- [PR #1264](https://github.com/CrocSwap/integer-mult-bounds/pull/1264) screens - 14 open claims at the **unchanged** coverage law; nothing there varies the - interface. -- [PR #1272](https://github.com/CrocSwap/integer-mult-bounds/pull/1272) - (pending) narrows this card with a ceiling screen; this package is that screen - applied to changed interfaces. +- https://github.com/CrocSwap/integer-mult-bounds/pull/1240 (Douglas Colkitt) + derives the coverage-law moment model and the fixed-word packing ceiling, and + names the coverage-law change as open. This package answers that question with + independently written, code-disjoint exact interval arithmetic; its `unpaid` + what-if parameter is used here as a search lever. +- The pending stacked branches of + https://github.com/CrocSwap/integer-mult-bounds/pull/1240 and + https://github.com/CrocSwap/integer-mult-bounds/pull/1272 carry a `levers.py` + ideal-budget table (first-order multiples per lever) that + CrocSwap/integer-mult-bounds#1272's proposed `centre-path-sharing` and + `coverage-law-change` cards cite. This package is complementary: it certifies + exact threshold brackets (not first-order multiples) at two targets, adds the + families and paid-word-scaling levers, least-integer thresholds, the + `(u=2, c=0)` pair obstruction and the `a* < D/E` convexity margins, and ships + as a package on the base commit. +- https://github.com/CrocSwap/integer-mult-bounds/pull/1264 screens 14 open + claims at the **unchanged** coverage law; nothing there varies the interface. +- https://github.com/CrocSwap/integer-mult-bounds/pull/1272 (pending) narrows + this card with a ceiling screen; this package is that screen applied to + changed interfaces. - Ali Romman's `research/heterogeneous-owner-assembly/` bounds every mixture of the frozen catalogue's 25 cost interfaces and explicitly excludes new - helper-inventory interfaces such as PR1004/1005's R489/R480. The thresholds - here price what such a new interface would have to deliver. -- Distinct from discussion #1265 (within-group idle repartitions at a fixed - coverage law) and discussion #1315 (X2 acceptance boundary for the selected - owner map). + helper-inventory interfaces such as the R489/R480 interfaces of + CrocSwap/integer-mult-bounds#1004 and CrocSwap/integer-mult-bounds#1005. The + thresholds here price what such a new interface would have to deliver. +- Distinct from + https://github.com/CrocSwap/integer-mult-bounds/discussions/1265 (within-group + idle repartitions at a fixed coverage law) and + https://github.com/CrocSwap/integer-mult-bounds/discussions/1315 (X2 + acceptance boundary for the selected owner map). ## Reproduce @@ -169,14 +177,16 @@ nine extra families raise it. See [TASK.json](TASK.json) for the structured list: 1. **Can any physically realizable helper inventory move a lever past a - threshold?** First step: map PR1004/1005's R489/R480 interfaces onto - `(u, c, F, s)` and price them here. Blocked on an admission proof that a known - interface change corresponds to a coverage-identity change rather than a - repacking. -2. **Thresholds for the #1148 joint-entrance words** (whose packing caps are - 0.17–0.21% below the selected word's). First step: pin one joint-entrance - profile from PR #1264's `SNAPSHOT.json` and rerun the table. Blocked on the - profile not being in the base tree. + threshold?** First step: map the R489/R480 interfaces of + CrocSwap/integer-mult-bounds#1004 and CrocSwap/integer-mult-bounds#1005 onto + `(u, c, F, s)` and price them here. Blocked on an admission proof that a + known interface change corresponds to a coverage-identity change rather than + a repacking. +2. **Thresholds for the CrocSwap/integer-mult-bounds#1148 joint-entrance words** + (whose packing caps are 0.17–0.21% below the selected word's). First step: + pin one joint-entrance profile from + https://github.com/CrocSwap/integer-mult-bounds/pull/1264's `SNAPSHOT.json` + and rerun the table. Blocked on the profile not being in the base tree. 3. **The exact combined `(u, c)` and `(F, s)` Pareto surface at 1/99.** First step: a certified 2D grid in `verify.py`; not blocked, cheap. @@ -184,7 +194,7 @@ See [TASK.json](TASK.json) for the structured list: Contributor: **Navinor**, with help from opencode. Apache-2.0. -Predecessors: PR1012's coverage identity; PR +Predecessors: CrocSwap/integer-mult-bounds#1012's coverage identity; https://github.com/CrocSwap/integer-mult-bounds/pull/1240 and https://github.com/CrocSwap/integer-mult-bounds/pull/1264 (Douglas Colkitt) for the moment model, the fixed-word ceiling and the open question; the selected diff --git a/research/complex-coverage-law-relief/TASK-CARD.md b/research/complex-coverage-law-relief/TASK-CARD.md index 0584fe0a30..4dca2ad5c9 100644 --- a/research/complex-coverage-law-relief/TASK-CARD.md +++ b/research/complex-coverage-law-relief/TASK-CARD.md @@ -7,34 +7,39 @@ nonce `6ddf1b6647d8c5131033b16d30f0045b`). Base commit: `bce54fb3f895cbe5cd4c0eb477c3afeed100190f`. Exact predecessors / dependency heads (read-only, not vendored): -- PR https://github.com/CrocSwap/integer-mult-bounds/pull/1240 head +- https://github.com/CrocSwap/integer-mult-bounds/pull/1240 head `1e136b8c4a552050820334ad113628775182f08c` — coverage-law moment model and the incumbent-word packing ceiling `a < 0.001690054109089` (semantics reference only; this package's arithmetic is written independently). -- PR1012 coverage identity (via #1240 and `research/community-batch1099-audit`): - paid rank mass = `(m - unpaid) * W + centre * N` per template. +- CrocSwap/integer-mult-bounds#1012 coverage identity (via + https://github.com/CrocSwap/integer-mult-bounds/pull/1240 and + `research/community-batch1099-audit`): paid rank mass = `(m - unpaid) * W + + centre * N` per template. - `research/heterogeneous-owner-assembly/` (Ali Romman) — frozen provider-catalogue - mixture bound; its controls already reject the U10 delta (PR987) and the R489/R480 - helper-inventory changes (PR1004/1005), so new cost interfaces are outside it. + mixture bound; its controls already reject the U10 delta (CrocSwap/integer-mult-bounds#987) + and the R489/R480 helper-inventory changes (CrocSwap/integer-mult-bounds#1004 and + CrocSwap/integer-mult-bounds#1005), so new cost interfaces are outside it. Concrete object and question: The hosted nine-stage coverage law of the selected line: width `m = 73`, `w = families/stages = 896/9` live families per call, centre charge `64` per call, `unpaid = 1` coordinate per family, halving-guard idle rank cap `R = 51`, with the -selected #1094 local word `{1:2412, 2:418, 3:432, 4:142, 5:82, 8:8}` (paid mass -5586 per call). Question: which changes of the local cost interface (unpaid -coordinates per family `u`, centre charge `c`, families per call `w`, and paid-word -excess spend `E`) are *necessary and which are sufficient* for the optimistic -whole-construction moment to admit saving `a >= 1/99`, and what are the exact -thresholds and trade-offs between them? +selected CrocSwap/integer-mult-bounds#1094 local word +`{1:2412, 2:418, 3:432, 4:142, 5:82, 8:8}` (paid mass 5586 per call). Question: +which changes of the local cost interface (unpaid coordinates per family `u`, +centre charge `c`, families per call `w`, and paid-word excess spend `E`) are +*necessary and which are sufficient* for the optimistic whole-construction moment +to admit saving `a >= 1/99`, and what are the exact thresholds and trade-offs +between them? Scope status: **refined**. The card asks for a new physically realizable helper inventory; this session runs the card's stated first experiment (the complete optimistic child histogram, rejecting routes without headroom) on *changed coverage-law interfaces* instead of proposing a full new contract. Reason: the optimistic screen is what decides whether any contract with given interface -parameters can have headroom at all, and #1240's open question asks for exactly -this quantification on the coverage-law side. +parameters can have headroom at all, and +https://github.com/CrocSwap/integer-mult-bounds/pull/1240's open question asks +for exactly this quantification on the coverage-law side. Existing restriction being changed (or exact claim audited): The coverage-law parameters `(unpaid=1, centre=64, families=896, stages=9)` and @@ -47,17 +52,22 @@ exponential with Lagrange remainder, outward rounding), bisection ceiling in `a` Domain: `u` in {1,...,12} integer and the exact continuous threshold in `(1, 12]`; `c` in [0, 64] rational; `w` in [50, 2000] families per call at `stages = 9` (families integer 450..18000); paid-word excess spend scaled continuously down -from the incumbent's. Positive control: reproduce #1240's incumbent ceiling. +from the incumbent's. Positive control: reproduce +https://github.com/CrocSwap/integer-mult-bounds/pull/1240's incumbent ceiling. Failure controls: mutated profile, halving-guard violation, over-paid word. Nearest overlapping PRs and why this adds something: -- #1240 screens one fixed word's repacking ceiling and states the coverage-law - change as an open direction; this package quantifies that direction exactly. -- #1264 screens 14 open claims' words at the *unchanged* coverage law; it does not - vary interface parameters. -- #1272 (director, pending) narrows this card with a ceiling screen; this package - is the screen applied to changed interfaces, consistent with that narrowing. -- Discussion #1265 covers within-group idle repartitions at fixed coverage law. +- https://github.com/CrocSwap/integer-mult-bounds/pull/1240 screens one fixed + word's repacking ceiling and states the coverage-law change as an open + direction; this package quantifies that direction exactly. +- https://github.com/CrocSwap/integer-mult-bounds/pull/1264 screens 14 open + claims' words at the *unchanged* coverage law; it does not vary interface + parameters. +- https://github.com/CrocSwap/integer-mult-bounds/pull/1272 (director, pending) + narrows this card with a ceiling screen; this package is the screen applied to + changed interfaces, consistent with that narrowing. +- https://github.com/CrocSwap/integer-mult-bounds/discussions/1265 covers + within-group idle repartitions at fixed coverage law. Optimistic full cost budget; required observable improvement: The relaxation already grants fractional idle, all idle at the cheapest admissible @@ -72,8 +82,11 @@ table with certified brackets. Falsification = any control mutation accepted. Compute cap: minutes of stdlib runtime; no network beyond the board/PR checks. Predecessor authors; intended artifact and reproduction command: -Douglas Colkitt (#1240/#1264/#1240's coverage-law model; PR1012 identity), -Ali Romman (heterogeneous-owner-assembly), the selected-line authors (see -`certificates/selected-result.json`). Artifact: `research/complex-coverage-law-relief/` -with `verify.py`; reproduction `python3 -I -B research/complex-coverage-law-relief/verify.py`. +Douglas Colkitt (https://github.com/CrocSwap/integer-mult-bounds/pull/1240, +https://github.com/CrocSwap/integer-mult-bounds/pull/1264 and the coverage-law +model; CrocSwap/integer-mult-bounds#1012 identity), Ali Romman +(heterogeneous-owner-assembly), the selected-line authors (see +`certificates/selected-result.json`). Artifact: +`research/complex-coverage-law-relief/` with `verify.py`; reproduction +`python3 -I -B research/complex-coverage-law-relief/verify.py`. Contributor: Navinor, with help from opencode. diff --git a/research/complex-coverage-law-relief/TASK.json b/research/complex-coverage-law-relief/TASK.json index 2c1fc798fc..69b9f5ade0 100644 --- a/research/complex-coverage-law-relief/TASK.json +++ b/research/complex-coverage-law-relief/TASK.json @@ -40,26 +40,26 @@ ] }, "scope_status": "refined", - "actual_scope": "Exact relief thresholds and scoped obstructions for the hosted nine-stage coverage-law interface (unpaid coordinates per family u, centre charge c, families per call, paid-word excess spend) behind the selected #1094 complex local word, under the optimistic whole-construction moment; targets are a = 1/99 and the retained-transfer unbinding saving a = kappa_bit/(1-kappa_bit).", - "scope_change_reason": "The card asks for a new physically realizable helper inventory. This session runs the card's stated first experiment (the complete optimistic child histogram, rejecting routes without headroom) on changed coverage-law interfaces instead of proposing a full new contract, because the optimistic screen decides whether any contract with given interface parameters can have headroom at all, and PR #1240's open question asks for exactly this quantification on the coverage-law side. Necessity claims hold for every construction inside the model; sufficiency is optimistic-relaxation only.", + "actual_scope": "Exact relief thresholds and scoped obstructions for the hosted nine-stage coverage-law interface (unpaid coordinates per family u, centre charge c, families per call, paid-word excess spend) behind the selected CrocSwap/integer-mult-bounds#1094 complex local word, under the optimistic whole-construction moment; targets are a = 1/99 and the retained-transfer unbinding saving a = kappa_bit/(1-kappa_bit).", + "scope_change_reason": "The card asks for a new physically realizable helper inventory. This session runs the card's stated first experiment (the complete optimistic child histogram, rejecting routes without headroom) on changed coverage-law interfaces instead of proposing a full new contract, because the optimistic screen decides whether any contract with given interface parameters can have headroom at all, and CrocSwap/integer-mult-bounds#1240's open question asks for exactly this quantification on the coverage-law side. Necessity claims hold for every construction inside the model; sufficiency is optimistic-relaxation only.", "bottleneck_link": "The card's question is whether a new local cost interface can change the deficit-to-recursive-cost ratio D/E beyond current packing. The thresholds quantify which interface levers move D/E past the binding complex budget: the deficit D = u*w - c and the recursive spend E both live in the coverage law, so a changed helper inventory can help only through one of these four levers.", "budget_minutes": 60, "stop_rule": "One bounded experiment: certified thresholds for the four levers plus the (u=2, c=0) and (u=3, c=64) pair points on the incumbent word; stop at the first table, no wider search without a physically realizable contract.", "outcome": "completed", - "evidence": "PASS_COMPLEX_COVERAGE_LAW_RELIEF from research/complex-coverage-law-relief/verify.py: incumbent ceiling reproduced (a* = 0.0016900541090887 vs PR #1240's grid ceiling 0.001690054109089); T1 (1/99) needs u* in (2.804078009, 2.804078010) or F* = 3093 families or paid counts <= 4.911% of current, and centre relief alone is impossible (sup a* at c = 0 is 0.004711142955614 < 1/99; u <= 2 with any centre charge also fails: sup 0.009357801683738 at (u=2, c=0)); u = 3 at unchanged c = 64 optimistically suffices (a* = 0.011001994530886). T2 (unbinding) needs u* in (1.009826689, 1.009826689), or c <= 63.021698515, or F* = 906 families, or paid counts <= 96.9437086%. D/E diagnostic and eight failure controls pass; certificate in the verify --out JSON.", + "evidence": "PASS_COMPLEX_COVERAGE_LAW_RELIEF from research/complex-coverage-law-relief/verify.py: incumbent ceiling reproduced (a* = 0.0016900541090887 vs CrocSwap/integer-mult-bounds#1240's grid ceiling 0.001690054109089); T1 (1/99) needs u* in (2.804078009, 2.804078010) or F* = 3093 families or paid counts <= 4.911% of current, and centre relief alone is impossible (sup a* at c = 0 is 0.004711142955614 < 1/99; u <= 2 with any centre charge also fails: sup 0.009357801683738 at (u=2, c=0)); u = 3 at unchanged c = 64 optimistically suffices (a* = 0.011001994530886). T2 (unbinding) needs u* in (1.009826689, 1.009826689), or c <= 63.021698515, or F* = 906 families, or paid counts <= 96.9437086%. D/E diagnostic and eight failure controls pass; certificate in the verify --out JSON.", "author": "Navinor", "ai_assistance": "Substantial assistance from opencode (the OpenCode agent harness); contributor Navinor.", "open_questions": [ { "question": "Can any physically realizable helper inventory move a coverage-law lever past a threshold: keep u >= 2.804 unpaid coordinates per family, cut the centre charge to <= 63.02, or shrink the paid word to <= 4.911% of its counts?", "why_it_matters": "These are the only levers that move the binding complex budget inside this model; a contract that realizes one would change the frontier, and one that cannot is a closed route.", - "first_step": "Map the already-admitted helper-inventory changes PR1004/1005's R489/R480 (rejected by research/heterogeneous-owner-assembly's controls as outside the frozen catalogue) onto the (u, c, F, s) levers and price their endpoint with this verifier.", + "first_step": "Map the already-admitted helper-inventory changes (the R489/R480 interfaces of CrocSwap/integer-mult-bounds#1004 and CrocSwap/integer-mult-bounds#1005, rejected by research/heterogeneous-owner-assembly's controls as outside the frozen catalogue) onto the (u, c, F, s) levers and price their endpoint with this verifier.", "blocked_by": "No admission proof yet that any known interface change corresponds to a coverage-identity change rather than a repacking." }, { - "question": "What are the same thresholds for the #1148 joint-entrance local words, which #1264 shows have lower packing caps than the selected word?", + "question": "What are the same thresholds for the CrocSwap/integer-mult-bounds#1148 joint-entrance local words, which CrocSwap/integer-mult-bounds#1264 shows have lower packing caps than the selected word?", "why_it_matters": "The leading open claim line packs words with caps 0.17-0.21% below the selected word's; its relief thresholds may be worse or better than the selected word's, changing which line deserves construction effort.", - "first_step": "Pin one joint-entrance profile (e.g. from PR #1264's SNAPSHOT.json at head 1be64e9ef79fe11f24f05b62b0fd7d70be0b7b4c) and rerun this package's table with that profile as the word.", + "first_step": "Pin one joint-entrance profile (e.g. from CrocSwap/integer-mult-bounds#1264's SNAPSHOT.json at head 1be64e9ef79fe11f24f05b62b0fd7d70be0b7b4c) and rerun this package's table with that profile as the word.", "blocked_by": "The joint-entrance profiles are not in the base tree; a pinned PR blob or an in-tree package is needed as the word source." }, { diff --git a/research/complex-coverage-law-relief/VERIFY.json b/research/complex-coverage-law-relief/VERIFY.json index 44a61877a4..34cdf7aa4c 100644 --- a/research/complex-coverage-law-relief/VERIFY.json +++ b/research/complex-coverage-law-relief/VERIFY.json @@ -15,7 +15,7 @@ "{package}/verify.py" ], "timeout_seconds": 120, - "checks": "Coverage identity (7232 total, 1646 idle), positive fixture reproducing PR #1240's incumbent grid ceiling, certified threshold brackets for the four interface levers at both targets, the (u=2, c=0) pair obstruction and (u=3, c=64) sufficiency point, the a* < D/E convexity margin at four points, and failure controls: unpaid=0, halving-guard R=52, negative centre, over-paid word, one-extra-rank-1 mutant, F+9 monotone control." + "checks": "Coverage identity (7232 total, 1646 idle), positive fixture reproducing CrocSwap/integer-mult-bounds#1240's incumbent grid ceiling, certified threshold brackets for the four interface levers at both targets, the (u=2, c=0) pair obstruction and (u=3, c=64) sufficiency point, the a* < D/E convexity margin at four points, and failure controls: unpaid=0, halving-guard R=52, negative centre, over-paid word, one-extra-rank-1 mutant, F+9 monotone control." } ] } diff --git a/research/complex-coverage-law-relief/verify.py b/research/complex-coverage-law-relief/verify.py index 176b337ac3..2524e70858 100644 --- a/research/complex-coverage-law-relief/verify.py +++ b/research/complex-coverage-law-relief/verify.py @@ -2,7 +2,8 @@ # SPDX-License-Identifier: Apache-2.0 """Exact relief thresholds for the coverage law behind the selected complex local word. -Model (all inputs explicit; semantics follow PR1012's coverage identity and the +Model (all inputs explicit; semantics follow CrocSwap/integer-mult-bounds#1012's +coverage identity and the moment model of https://github.com/CrocSwap/integer-mult-bounds/pull/1240, whose arithmetic is NOT imported here): @@ -11,9 +12,11 @@ * coverage identity: paid rank mass + idle mass = (m - unpaid) * w + centre, i.e. each live family keeps `unpaid` unpaid coordinates (1 on the selected line) and each call pays a centre path of `centre` (64 on the selected line); - * the local word fixes its paid child profile per call (the selected #1094 word + * the local word fixes its paid child profile per call (the selected + CrocSwap/integer-mult-bounds#1094 word is {1:2412, 2:418, 3:432, 4:142, 5:82, 8:8}, mass 5586, recorded at - research/gauge44-slots-t16/README.md and re-priced by PR #1240); + research/gauge44-slots-t16/README.md and re-priced by + CrocSwap/integer-mult-bounds#1240); * all remaining mass is idle/remainder children of rank at most R, where the outer halving guard m^2 > 2 R^2 gives R = 51 at m = 73. @@ -49,9 +52,10 @@ FAMILIES0 = 896 CENTRE0 = 64 UNPAID0 = 1 -WORD = {1: 2412, 2: 418, 3: 432, 4: 142, 5: 82, 8: 8} # selected #1094 local word per call +WORD = {1: 2412, 2: 418, 3: 432, 4: 142, 5: 82, 8: 8} # selected CrocSwap/integer-mult-bounds#1094 local word per call WORD_MASS = sum(r * n for r, n in WORD.items()) # 5586 -# PR #1240 reports the incumbent ceiling as a < 0.001690054109089 (positive control). +# CrocSwap/integer-mult-bounds#1240 reports the incumbent ceiling as +# a < 0.001690054109089 (positive control). REF_CEILING = Q(1690054109089, 10 ** 15) # scripts/research_baseline.py at the base commit: bit_saving = 1733427039589844234749/10^24. KAPPA_BIT = Q(1733427039589844234749, 10 ** 24) @@ -253,13 +257,14 @@ def run(out_path): rep.check(q['total'] == Q(7232) and q['idle'] == Q(1646), 'COVERAGE_IDENTITY', f"total={q['total']} idle={q['idle']} w={frac_str(q['w'])} deficit={frac_str(q['deficit'])}") - # --- positive control: reproduce PR #1240's incumbent ceiling. - # #1240 reports the first 1e-15 grid point above a*, so its number is an upper - # bound; require our true bracket to sit within one grid step below it. + # --- positive control: reproduce CrocSwap/integer-mult-bounds#1240's incumbent ceiling. + # CrocSwap/integer-mult-bounds#1240 reports the first 1e-15 grid point above + # a*, so its number is an upper bound; require our true bracket to sit within + # one grid step below it. lo, hi = ceiling(WORD) rep.check(hi - lo <= Q(2, 10 ** 18) and hi <= REF_CEILING and lo >= REF_CEILING - Q(1, 10 ** 15), 'INCUMBENT_CEILING', - f'a* in [{dec(lo, 18)}, {dec(hi, 18)}] vs #1240 grid ceiling {dec(REF_CEILING, 15)}') + f'a* in [{dec(lo, 18)}, {dec(hi, 18)}] vs CrocSwap/integer-mult-bounds#1240 grid ceiling {dec(REF_CEILING, 15)}') rep.cert['incumbent_ceiling'] = {'a_lo': frac_str(lo), 'a_hi': frac_str(hi), 'decimal': dec(hi, 18), 'pr1240_reported': dec(REF_CEILING, 15)} From 74768ab408b1ae2ce2c7094b49457a86fcb06e94 Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Wed, 14 Oct 2026 04:17:38 -0400 Subject: [PATCH 3/3] Re-derive the coverage-law T2 target from the coupled assembly binding step --- .../complex-coverage-law-relief/README.md | 100 +++++++++++--- .../complex-coverage-law-relief/SOURCES.json | 12 ++ .../complex-coverage-law-relief/TASK.json | 6 +- .../complex-coverage-law-relief/VERIFY.json | 5 +- .../complex-coverage-law-relief/verify.py | 128 ++++++++++++++++-- 5 files changed, 216 insertions(+), 35 deletions(-) diff --git a/research/complex-coverage-law-relief/README.md b/research/complex-coverage-law-relief/README.md index 2702b3426f..90977f7c65 100644 --- a/research/complex-coverage-law-relief/README.md +++ b/research/complex-coverage-law-relief/README.md @@ -39,15 +39,65 @@ is optimistic only. Two targets: -- **T1 (headline):** `a = 1/99`, equivalently `κ = 0.01` under the retained - transfer `κ = a/(1+a)`. -- **T2 (unbinding):** `a = κ_bit/(1 − κ_bit)` with `κ_bit = - 1733427039589844234749/10^24`, the bit saving pinned by - `scripts/research_baseline.py` at the base commit. This is where the complex - side would stop binding over that bit supplier. The incumbent ceiling - `a* = 0.001690054109088696` (κ ≈ 0.00168720) is below T2, so **pure repacking - of the selected word cannot unbind the complex side**; an interface change is - required even for the near target. +- **T1 (headline):** `a = 1/99`, a chosen planning target. Its `κ = 0.01` + caption is **defined** under the retained planning transfer `κ = a/(1+a)`, + not derived; the T1/coverage arithmetic below stands on its own either way. +- **T2 (complex-unbinding, re-derived from the coupled assembly):** + `a = c_bit/(1 − β) = 1733427039589844234749/(10^24 − 1)`, i.e. + `0.001733427039589844234749001733…`, where `c_bit = + 1733427039589844234749/10^24 = 0.001733427039589844234749` is the pinned + PR589 bit supplier's moment endpoint in `a`-units (`bit_saving` in + `scripts/research_baseline.py`, `bit_lower` in the pinned assembly + certificate — a supplier saving, **not** a kappa) and `β = 10^-24` is the + assembly's transfer factor on the complex endpoint. This is the point where + the assembly's binding step flips and the complex side stops binding over + that bit supplier; the exact conversion chain is in + [The T2 conversion chain](#the-t2-conversion-chain-coupled-assembly) below. + The retired pre-review value `a = κ_bit/(1 − κ_bit) = 0.001736437026484097` + applied a second `a = κ/(1−κ)` conversion to the `a`-unit bit endpoint; it is + defined, not derived, and overshoots the flip point by 0.1736%. The incumbent + ceiling `a* = 0.001690054109088696` is below the corrected T2, so **pure + repacking of the selected word cannot unbind the complex side**; an interface + change is required even for the near target. + +## The T2 conversion chain (coupled assembly) + +Pinned sources: the selected record's assembly certificate +`research/community-frontier1094-audit/ASSEMBLY.json` (the bit endpoint is the +PR589 supplier, cited unchanged) and the selected outer reduction +`research/pending-claims-independent-pricing/arith.py` (`kappa_from`), whose +`kappa_equals_record` gate in +`research/community-batch1099-audit/check_frontier1094.py` binds that assembly +to `certificates/selected-result.json`. This package re-implements the reduction +code-disjoint and reproduces the record exactly. + +1. Supplier endpoints in `a`-units (moment endpoints, certified per side: the + bit side carries its bad-residue surcharge inside the moment, the complex + side has no surcharge): complex `b = 67018507072324140917/(4·10^22) = + 0.001675462676808103522925` and bit `c_bit = + 1733427039589844234749/10^24 = 0.001733427039589844234749`. +2. Binding step: `s = min(c_bit, (1−β)·b) − 10^−27` with `β = η = 10^−24`; the + binding label is *bit* iff `c_bit ≤ (1−β)·b`, else *complex*. The selected + record takes the complex branch: `s = (1−β)·b − 10^−27`. +3. Bootstrap: `a ← s(1−s+a)` from `384599/10^10`, seven steps. The fixed point + is exactly `s` (the error contracts by the factor `s` per step; + `s − a₇ ≈ 6.07·10^−23`). +4. Outer reduction: `q = a₇(1−2η)`; `κ` is the largest `10^-18` grid point + strictly below `(1−η)·q/(1+q)`. This yields + `836330098538459/(5·10^17) = 0.001672660197076918`, the selected record's + kappa. + +The complex side unbinds exactly when the min in step 2 flips to the bit +branch: `(1−β)·b ≥ c_bit`, i.e. `b ≥ c_bit/(1−β)`. The `10^−27` shave, the +bootstrap, the `(1−2η)`/`(1−η)` factors and the grid floor all act strictly +after the min, so none of them moves the flip point. The threshold is +`c_bit/(1−β) = 1733427039589844234749/(10^24 − 1)`, whose decimal expansion is +the period-24 repeat `0.001733427039589844234749 001733427039589844234749 …`. +The retired double conversion +`κ_bit/(1−κ_bit) = 1733427039589844234749/998266572960410155765251 = +0.0017364370264840967545358…` treated the `a`-unit endpoint as a kappa and +inverted a second time; it is kept in the certificate as `retired_a_T2` for +traceability and is not used as a threshold. ## Results (all brackets certified with exact rational intervals) @@ -55,12 +105,12 @@ Positive control: `a* = 0.001690054109088696` reproduces https://github.com/CrocSwap/integer-mult-bounds/pull/1240's grid ceiling `a < 0.001690054109089` to within one 1e-15 grid step. -| Lever (others at the selected line) | T2: unbinding (`a = 0.001736437026484097`) | T1: `a = 1/99` | +| Lever (others at the selected line) | T2: complex-unbinding (`a = 1733427039589844234749/(10^24 − 1)`) | T1: `a = 1/99` | |---|---|---| -| unpaid coordinates per family `u` | `u* ∈ (1.009826689, 1.009826689)`; least integer 2 | `u* ∈ (2.804078009, 2.804078010)`; least integer 3 | -| centre charge `c` (from 64) | `c* ∈ (63.021698514, 63.021698515)`: met iff `c ≤ c*` | **impossible**: sup `a* = 0.004711142955614` at `c = 0` | -| families per replica `F` (stages 9) | least met `F = 906` (905 fails) | least met `F = 3093` (3092 fails) | -| paid-word count scale `s` | met iff `s ≤ 0.969437086` | met iff `s ≤ 0.049110034` | +| unpaid coordinates per family `u` | `u* ∈ (1.009188952, 1.009188953)`; least integer 2 | `u* ∈ (2.804078009, 2.804078010)`; least integer 3 | +| centre charge `c` (from 64) | `c* ∈ (63.085188751, 63.085188752)`: met iff `c ≤ c*` | **impossible**: sup `a* = 0.004711142955614` at `c = 0` | +| families per replica `F` (stages 9) | least met `F = 905` (904 fails) | least met `F = 3093` (3092 fails) | +| paid-word count scale `s` | met iff `s ≤ 0.971370799` | met iff `s ≤ 0.049110034` | Pair points at `F = 896`: @@ -76,9 +126,9 @@ coordinates (integer 3 at `c = 64`), or a 3.45× larger template (3093 families per replica at 9 stages), or a paid word at most 4.911% of its current counts (a 95.1% reduction, consistent with CrocSwap/integer-mult-bounds#1240's independently derived "about 95% lower fully priced local excess spend"). -Centre-charge relief alone cannot reach T1 at any `c ≥ 0`. T2 is much nearer: -about 1% more unpaid coordinates, or one unit off the 64 centre charge, or 906 -families, or a 3.06% paid-count cut. +Centre-charge relief alone cannot reach T1 at any `c ≥ 0`. T2 is nearer: +about 0.92% more unpaid coordinates, or one unit off the 64 centre charge +(`c* ≈ 63.085`), or 905 families, or a 2.86% paid-count cut. ## D/E diagnostic @@ -111,8 +161,17 @@ is the acceptance test. CrocSwap/integer-mult-bounds#1012's identity is re-checked only at the selected point; a realized `u ≥ 3` would itself be a changed interface contract needing its own admission. -- `κ = a/(1+a)` is the retained planning transfer, not a theorem; T2 uses the - bit supplier pinned at the base commit, and any bit-side improvement moves it. +- `κ = a/(1+a)` is the retained planning transfer, not a theorem. Only T1's + `κ = 0.01` caption uses it, as a defined label; T2 uses no κ-conversion at + all: it is the binding-flip point `c_bit/(1−β)` of the pinned assembly's + binding step (derived in + [The T2 conversion chain](#the-t2-conversion-chain-coupled-assembly)), and it + moves with any bit-side improvement to `c_bit` or change of `β`. +- The T2 derivation is exact under the pinned assembly's reduction + (`research/pending-claims-independent-pricing/arith.py`); a different coupling + or surcharge model would move the flip point. The threshold is on the + complex-side moment endpoint `a`, so reading the levers against it assumes the + levered call keeps the same endpoint semantics. - All inherited all-size/compiler, common-label/mutable-source, whole-call hosting, precision/tape, analytic-transfer and bit H1–H5 assumptions remain. This is not a full Lean multiplication theorem. @@ -166,7 +225,8 @@ Expected final line: PASS_COMPLEX_COVERAGE_LAW_RELIEF ``` -Add `--out /new/file.json` for the complete certificate (model, targets, every +Add `--out /new/file.json` for the complete certificate (model, the replayed +coupled-assembly chain, targets with the derived and retired T2 values, every threshold bracket as exact fractions, pair points, D/E diagnostics, check log). Failure controls: `unpaid = 0`, halving-guard `R = 52`, a negative centre charge and an over-paid word are rejected; one extra rank-1 child lowers the ceiling; diff --git a/research/complex-coverage-law-relief/SOURCES.json b/research/complex-coverage-law-relief/SOURCES.json index abd5f6df21..fd5647b1bb 100644 --- a/research/complex-coverage-law-relief/SOURCES.json +++ b/research/complex-coverage-law-relief/SOURCES.json @@ -19,6 +19,18 @@ "usage": "input", "git_blob": "0262339347a739be25b24860e96b4a20dd774807", "sha256": "e33534891b32397220d29cd60943a71b863b606e734d71902349e4cac78a1a35" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/pending-claims-independent-pricing/arith.py", + "usage": "provenance", + "git_blob": "b9e30144438b375ee999e53c5fe7051e381e4c6f", + "sha256": "1b4766610223bbf5e346d7cebc036eaeaedfa2f7200c075136bd750ab26ece88" } ] } diff --git a/research/complex-coverage-law-relief/TASK.json b/research/complex-coverage-law-relief/TASK.json index 69b9f5ade0..3ddb52815d 100644 --- a/research/complex-coverage-law-relief/TASK.json +++ b/research/complex-coverage-law-relief/TASK.json @@ -40,18 +40,18 @@ ] }, "scope_status": "refined", - "actual_scope": "Exact relief thresholds and scoped obstructions for the hosted nine-stage coverage-law interface (unpaid coordinates per family u, centre charge c, families per call, paid-word excess spend) behind the selected CrocSwap/integer-mult-bounds#1094 complex local word, under the optimistic whole-construction moment; targets are a = 1/99 and the retained-transfer unbinding saving a = kappa_bit/(1-kappa_bit).", + "actual_scope": "Exact relief thresholds and scoped obstructions for the hosted nine-stage coverage-law interface (unpaid coordinates per family u, centre charge c, families per call, paid-word excess spend) behind the selected CrocSwap/integer-mult-bounds#1094 complex local word, under the optimistic whole-construction moment; targets are a = 1/99 (chosen planning target) and the complex-unbinding saving a = c_bit/(1 - beta) = 1733427039589844234749/(10^24 - 1), re-derived as the binding-flip point of the pinned coupled assembly's binding step; the pre-review a = kappa_bit/(1-kappa_bit) double conversion is retired as defined-not-derived.", "scope_change_reason": "The card asks for a new physically realizable helper inventory. This session runs the card's stated first experiment (the complete optimistic child histogram, rejecting routes without headroom) on changed coverage-law interfaces instead of proposing a full new contract, because the optimistic screen decides whether any contract with given interface parameters can have headroom at all, and CrocSwap/integer-mult-bounds#1240's open question asks for exactly this quantification on the coverage-law side. Necessity claims hold for every construction inside the model; sufficiency is optimistic-relaxation only.", "bottleneck_link": "The card's question is whether a new local cost interface can change the deficit-to-recursive-cost ratio D/E beyond current packing. The thresholds quantify which interface levers move D/E past the binding complex budget: the deficit D = u*w - c and the recursive spend E both live in the coverage law, so a changed helper inventory can help only through one of these four levers.", "budget_minutes": 60, "stop_rule": "One bounded experiment: certified thresholds for the four levers plus the (u=2, c=0) and (u=3, c=64) pair points on the incumbent word; stop at the first table, no wider search without a physically realizable contract.", "outcome": "completed", - "evidence": "PASS_COMPLEX_COVERAGE_LAW_RELIEF from research/complex-coverage-law-relief/verify.py: incumbent ceiling reproduced (a* = 0.0016900541090887 vs CrocSwap/integer-mult-bounds#1240's grid ceiling 0.001690054109089); T1 (1/99) needs u* in (2.804078009, 2.804078010) or F* = 3093 families or paid counts <= 4.911% of current, and centre relief alone is impossible (sup a* at c = 0 is 0.004711142955614 < 1/99; u <= 2 with any centre charge also fails: sup 0.009357801683738 at (u=2, c=0)); u = 3 at unchanged c = 64 optimistically suffices (a* = 0.011001994530886). T2 (unbinding) needs u* in (1.009826689, 1.009826689), or c <= 63.021698515, or F* = 906 families, or paid counts <= 96.9437086%. D/E diagnostic and eight failure controls pass; certificate in the verify --out JSON.", + "evidence": "PASS_COMPLEX_COVERAGE_LAW_RELIEF from research/complex-coverage-law-relief/verify.py: incumbent ceiling reproduced (a* = 0.0016900541090887 vs CrocSwap/integer-mult-bounds#1240's grid ceiling 0.001690054109089); T1 (1/99) needs u* in (2.804078009, 2.804078010) or F* = 3093 families or paid counts <= 4.911% of current, and centre relief alone is impossible (sup a* at c = 0 is 0.004711142955614 < 1/99; u <= 2 with any centre charge also fails: sup 0.009357801683738 at (u=2, c=0)); u = 3 at unchanged c = 64 optimistically suffices (a* = 0.011001994530886). T2 is re-derived from the coupled assembly chain (research/community-frontier1094-audit/ASSEMBLY.json with research/pending-claims-independent-pricing/arith.py:kappa_from, replayed code-disjoint and reproducing the record kappa 0.001672660197076918): the complex side unbinds at a = c_bit/(1 - beta) = 1733427039589844234749/(10^24 - 1) = 0.001733427039589844234749001733..., the binding-flip point of s = min(c_bit, (1 - beta) b); the retired double conversion kappa_bit/(1-kappa_bit) = 0.001736437026484097 is kept as defined-not-derived and overshoots the flip by 0.1736%. At the corrected T2: u* in (1.009188952, 1.009188953), or c <= 63.085188752, or F* = 905 families, or paid counts <= 97.1370799% of current. D/E diagnostic, the T2 chain checks and the failure controls pass; certificate in the verify --out JSON.", "author": "Navinor", "ai_assistance": "Substantial assistance from opencode (the OpenCode agent harness); contributor Navinor.", "open_questions": [ { - "question": "Can any physically realizable helper inventory move a coverage-law lever past a threshold: keep u >= 2.804 unpaid coordinates per family, cut the centre charge to <= 63.02, or shrink the paid word to <= 4.911% of its counts?", + "question": "Can any physically realizable helper inventory move a coverage-law lever past a threshold: keep u >= 2.804 unpaid coordinates per family, cut the centre charge to <= 63.085, or shrink the paid word to <= 4.911% of its counts?", "why_it_matters": "These are the only levers that move the binding complex budget inside this model; a contract that realizes one would change the frontier, and one that cannot is a closed route.", "first_step": "Map the already-admitted helper-inventory changes (the R489/R480 interfaces of CrocSwap/integer-mult-bounds#1004 and CrocSwap/integer-mult-bounds#1005, rejected by research/heterogeneous-owner-assembly's controls as outside the frozen catalogue) onto the (u, c, F, s) levers and price their endpoint with this verifier.", "blocked_by": "No admission proof yet that any known interface change corresponds to a coverage-identity change rather than a repacking." diff --git a/research/complex-coverage-law-relief/VERIFY.json b/research/complex-coverage-law-relief/VERIFY.json index 34cdf7aa4c..fc104c42cb 100644 --- a/research/complex-coverage-law-relief/VERIFY.json +++ b/research/complex-coverage-law-relief/VERIFY.json @@ -4,7 +4,8 @@ "python": "3.12", "requirements": [], "inputs": [ - "research/gauge44-slots-t16/README.md" + "research/gauge44-slots-t16/README.md", + "research/community-frontier1094-audit/ASSEMBLY.json" ], "commands": [ { @@ -15,7 +16,7 @@ "{package}/verify.py" ], "timeout_seconds": 120, - "checks": "Coverage identity (7232 total, 1646 idle), positive fixture reproducing CrocSwap/integer-mult-bounds#1240's incumbent grid ceiling, certified threshold brackets for the four interface levers at both targets, the (u=2, c=0) pair obstruction and (u=3, c=64) sufficiency point, the a* < D/E convexity margin at four points, and failure controls: unpaid=0, halving-guard R=52, negative centre, over-paid word, one-extra-rank-1 mutant, F+9 monotone control." + "checks": "Coverage identity (7232 total, 1646 idle), positive fixture reproducing CrocSwap/integer-mult-bounds#1240's incumbent grid ceiling, code-disjoint replay of the pinned coupled-assembly chain (ASSEMBLY.json endpoints -> binding step -> bootstrap -> outer reduction) reproducing the record kappa and binding label, T2 re-derived as the binding-flip point a = c_bit/(1 - beta) with the retired double-conversion value recorded as defined-not-derived, certified threshold brackets for the four interface levers at both targets, the (u=2, c=0) pair obstruction and (u=3, c=64) sufficiency point, the a* < D/E convexity margin at four points, and failure controls: unpaid=0, halving-guard R=52, negative centre, over-paid word, one-extra-rank-1 mutant, F+9 monotone control." } ] } diff --git a/research/complex-coverage-law-relief/verify.py b/research/complex-coverage-law-relief/verify.py index 2524e70858..ab287fa935 100644 --- a/research/complex-coverage-law-relief/verify.py +++ b/research/complex-coverage-law-relief/verify.py @@ -31,9 +31,14 @@ interface parameters; a passing one is optimistic only (no realizability claim). This package computes certified brackets for a* and for the exact interface -thresholds that put a* above two targets: a = 1/99 (headline planning target) -and a = kappa_bit/(1 - kappa_bit) (the retained-transfer unbinding target where -the complex side would stop binding over the pinned bit supplier). +thresholds that put a* above two targets: a = 1/99 (headline planning target, +chosen; its kappa = 0.01 label is defined under the retained planning transfer +kappa = a/(1+a), not derived) and a = c_bit/(1 - beta), the complex-unbinding +threshold RE-DERIVED from the coupled assembly's binding step (see +assembly_reduction below): the complex side unbinds over the pinned bit +supplier exactly when the assembly's min flips to the bit branch. The retired +value kappa_bit/(1 - kappa_bit) applied a second a = kappa/(1-kappa) conversion +to the bit supplier's a-unit endpoint and is recorded here only as retired. Exact rational intervals: ln via atanh chains, exp by Taylor series with a geometric tail bound, outward rounding to 2^-PREC. Standard library only. @@ -41,6 +46,7 @@ """ import argparse import json +from pathlib import Path from fractions import Fraction as Q from functools import lru_cache from math import isqrt @@ -57,10 +63,33 @@ # CrocSwap/integer-mult-bounds#1240 reports the incumbent ceiling as # a < 0.001690054109089 (positive control). REF_CEILING = Q(1690054109089, 10 ** 15) -# scripts/research_baseline.py at the base commit: bit_saving = 1733427039589844234749/10^24. -KAPPA_BIT = Q(1733427039589844234749, 10 ** 24) -A_T1 = Q(1, 99) # headline target -A_T2 = KAPPA_BIT / (1 - KAPPA_BIT) # unbinding target, retained kappa = a/(1+a) +# scripts/research_baseline.py at the base commit exports bit_saving = +# 1733427039589844234749/10^24: the pinned PR589 bit supplier's moment endpoint +# in a-units (a supplier saving, NOT a kappa). +BIT_ENDPOINT = Q(1733427039589844234749, 10 ** 24) +# Coupled-assembly chain pinned by the selected record. The pinned assembly +# certificate research/community-frontier1094-audit/ASSEMBLY.json holds the two +# supplier moment endpoints and the assembled kappa; the selected outer +# reduction is research/pending-claims-independent-pricing/arith.py:kappa_from +# (gated on the record by +# research/community-batch1099-audit/check_frontier1094.py). It is pure +# rational arithmetic and is re-implemented code-disjoint in +# assembly_reduction() below, not imported. +ASSEMBLY = Path(__file__).resolve().parents[1] / 'community-frontier1094-audit' / 'ASSEMBLY.json' +BETA = Q(1, 10 ** 24) # transfer factor on the complex endpoint in the binding step +ETA = Q(1, 10 ** 24) # outer-reduction factors +SHAVE = Q(1, 10 ** 27) +BOOT_A0 = Q(384599, 10 ** 10) +BOOT_STEPS = 7 +A_T1 = Q(1, 99) # headline planning target (chosen; kappa = 0.01 only under the + # retained planning transfer kappa = a/(1+a), defined not derived) +# T2 re-derived from the assembly's binding step: the complex side unbinds iff +# c_bit <= (1 - BETA) b, i.e. at b = c_bit/(1 - BETA). No kappa conversion +# enters; the shave, bootstrap and outer factors act strictly after the min. +A_T2 = BIT_ENDPOINT / (1 - BETA) +# Retired pre-review value: a second a = kappa/(1-kappa) conversion applied to +# the a-unit bit endpoint. Not a derived unbinding threshold. +A_T2_RETIRED = BIT_ENDPOINT / (1 - BIT_ENDPOINT) def require(ok, why): @@ -230,6 +259,27 @@ def de_diagnostic(local, unpaid=UNPAID0, centre=CENTRE0, families=FAMILIES0, sta return d, lo, hi +def assembly_reduction(b, c, grid=Q(1, 10 ** 18)): + """Code-disjoint replay of the pinned selected outer reduction (arith.kappa_from). + + Binding step: s = min(c, (1 - BETA) b) - SHAVE, binding label 'bit' iff + c <= (1 - BETA) b (else 'complex'). Bootstrap: a <- s (1 - s + a) from + BOOT_A0 for BOOT_STEPS steps (fixed point is exactly s). Outer reduction: + q = a (1 - 2 ETA); kappa = the largest grid point strictly below + (1 - ETA) q / (1 + q). Returns (kappa, margin, binding). + """ + s = min(c, (1 - BETA) * b) - SHAVE + a = BOOT_A0 + for _ in range(BOOT_STEPS): + a = (1 - s) * s + s * a + q = a * (1 - 2 * ETA) + margin = (1 - ETA) * q / (1 + q) + t = margin / grid + k = (-((-t.numerator) // t.denominator) - 1) * grid + require(k < margin <= k + grid, 'grid reduction') + return k, margin, ('bit' if c <= (1 - BETA) * b else 'complex') + + class Report: def __init__(self): self.lines = [] @@ -249,6 +299,18 @@ def dec(x, digits=15): return f'{float(x):.{digits}f}' +def dec_exact(x, digits=30): + """First `digits` decimal digits of the nonnegative rational x (exact long division).""" + r = Q(x) + require(r >= 0, 'dec_exact domain') + out = [] + for _ in range(digits): + d = int(r * 10) + out.append(str(d)) + r = r * 10 - d + return '0.' + ''.join(out) + + def run(out_path): rep = Report() @@ -268,10 +330,55 @@ def run(out_path): rep.cert['incumbent_ceiling'] = {'a_lo': frac_str(lo), 'a_hi': frac_str(hi), 'decimal': dec(hi, 18), 'pr1240_reported': dec(REF_CEILING, 15)} - # --- targets: T2 (unbinding) is the nearer goal, above the incumbent packing ceiling. + # --- coupled-assembly chain: reproduce the pinned record kappa and binding label. + assembly = json.loads(ASSEMBLY.read_text(encoding='utf-8')) + b_complex = Q(assembly['complex_lower']) # complex endpoint, a-units (no surcharge) + c_bit = Q(assembly['bit_lower']) # bit endpoint, a-units (surcharge inside) + rep.check(c_bit == BIT_ENDPOINT, 'ASSEMBLY_BIT_PIN', + f'ASSEMBLY bit endpoint = research_baseline.py bit_saving = {frac_str(BIT_ENDPOINT)} (a-units, not a kappa)') + k_rec, _, bind_rec = assembly_reduction(b_complex, c_bit) + rep.check(k_rec == Q(assembly['kappa']) and bind_rec == assembly['binding'] == 'complex', + 'ASSEMBLY_CHAIN_REPLAY', + f'kappa {frac_str(k_rec)} = pinned record; binding {bind_rec}; s = (1-beta) b - 1e-27 (complex branch)') + rep.cert['assembly_chain'] = { + 'complex_endpoint': frac_str(b_complex), 'bit_endpoint': frac_str(c_bit), + 'beta': frac_str(BETA), 'eta': frac_str(ETA), 'shave': frac_str(SHAVE), + 'bootstrap_start': frac_str(BOOT_A0), 'bootstrap_steps': BOOT_STEPS, + 'record_kappa': frac_str(k_rec), 'binding': bind_rec, + 'chain': 's = min(c_bit,(1-beta)b) - shave; a <- s(1-s+a) x7 from 384599/10^10; ' + 'q = a(1-2 eta); kappa = largest 1e-18 grid point below (1-eta) q/(1+q)', + } + + # --- T2 re-derived from the binding step: the complex side unbinds iff + # c_bit <= (1 - BETA) b, i.e. at b = c_bit/(1 - BETA). The shave, bootstrap + # and outer factors act strictly after the min and do not move the flip point. + rep.check((1 - BETA) * A_T2 == BIT_ENDPOINT, 'T2_BINDING_FLIP_IDENTITY', + f'(1-beta) * a_T2 = c_bit exactly: a_T2 = {frac_str(A_T2)}') + _, _, bind_lo = assembly_reduction(A_T2 - Q(1, 10 ** 18), c_bit) + _, _, bind_hi = assembly_reduction(A_T2, c_bit) + rep.check(bind_lo == 'complex' and bind_hi == 'bit', 'T2_BINDING_FLIP_POINT', + f'binding flips between a_T2 - 1e-18 ({bind_lo}) and a_T2 ({bind_hi})') + rep.check(A_T2 < A_T2_RETIRED and (1 - BETA) * A_T2_RETIRED != BIT_ENDPOINT, + 'T2_RETIRED_DOUBLE_CONVERSION', + f'retired a = kappa_bit/(1-kappa_bit) = {frac_str(A_T2_RETIRED)} overshoots the flip by ' + f'{dec_exact((A_T2_RETIRED / A_T2 - 1) * 100, 6)}% (second conversion on an a-unit endpoint)') + + # --- targets: T2 (complex-unbinding, derived) is the nearer goal, above the incumbent packing ceiling. rep.check(0 < A_T2 < A_T1 and A_T2 > REF_CEILING, 'TARGETS', - f'a_T1=1/99={dec(A_T1)} a_T2={frac_str(A_T2)}={dec(A_T2, 18)}') - rep.cert['targets'] = {'a_T1': '1/99', 'a_T2': frac_str(A_T2), 'kappa_bit': frac_str(KAPPA_BIT)} + f'a_T1=1/99={dec(A_T1)} a_T2={frac_str(A_T2)}={dec_exact(A_T2, 18)}') + rep.cert['targets'] = { + 'a_T1': '1/99', + 'a_T1_label': 'chosen planning target; kappa = 0.01 only under the retained planning transfer ' + 'kappa = a/(1+a) (defined, not derived)', + 'a_T2': frac_str(A_T2), 'a_T2_decimal': dec_exact(A_T2, 30), + 'a_T2_derivation': 'c_bit/(1-beta): flip of the coupled assembly binding step ' + 's = min(c_bit, (1-beta) b); the complex side unbinds iff (1-beta) b >= c_bit. ' + 'Derived from the pinned chain, not a kappa conversion', + 'bit_endpoint': frac_str(BIT_ENDPOINT), 'beta': frac_str(BETA), + 'retired_a_T2': frac_str(A_T2_RETIRED), 'retired_a_T2_decimal': dec_exact(A_T2_RETIRED, 18), + 'retired_note': 'pre-review value applied a second a = kappa/(1-kappa) conversion to the a-unit ' + 'bit endpoint; defined-not-derived and superseded', + } # --- unpaid-coordinate threshold u* (continuous bracket + least integer). u_res = {} @@ -386,6 +493,7 @@ def run(out_path): if out_path: with open(out_path, 'w', encoding='utf-8') as fh: json.dump({'status': 'PASS_COMPLEX_COVERAGE_LAW_RELIEF', 'model': rep.cert['model'], + 'assembly_chain': rep.cert['assembly_chain'], 'targets': rep.cert['targets'], 'incumbent_ceiling': rep.cert['incumbent_ceiling'], 'unpaid_thresholds': rep.cert['unpaid_thresholds'], 'centre_thresholds': rep.cert['centre_thresholds'],