diff --git a/research/complex-coverage-law-relief/README.md b/research/complex-coverage-law-relief/README.md new file mode 100644 index 0000000000..90977f7c65 --- /dev/null +++ b/research/complex-coverage-law-relief/README.md @@ -0,0 +1,266 @@ +# 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 +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 +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 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`. + +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`, 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) + +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: complex-unbinding (`a = 1733427039589844234749/(10^24 − 1)`) | T1: `a = 1/99` | +|---|---|---| +| 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`: + +- `(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 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 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 + +`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. + 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. 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. + +## Boundary with existing work + +- 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 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 + +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, 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; +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 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. + +## Credit + +Contributor: **Navinor**, with help from opencode. Apache-2.0. + +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 +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..fd5647b1bb --- /dev/null +++ b/research/complex-coverage-law-relief/SOURCES.json @@ -0,0 +1,36 @@ +{ + "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" + }, + { + "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-CARD.md b/research/complex-coverage-law-relief/TASK-CARD.md new file mode 100644 index 0000000000..4dca2ad5c9 --- /dev/null +++ b/research/complex-coverage-law-relief/TASK-CARD.md @@ -0,0 +1,92 @@ +# 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): +- 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). +- 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 (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 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 +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 +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 +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: +- 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 +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 (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 new file mode 100644 index 0000000000..3ddb52815d --- /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 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 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.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." + }, + { + "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 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." + }, + { + "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..fc104c42cb --- /dev/null +++ b/research/complex-coverage-law-relief/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/gauge44-slots-t16/README.md", + "research/community-frontier1094-audit/ASSEMBLY.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{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, 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 new file mode 100644 index 0000000000..ab287fa935 --- /dev/null +++ b/research/complex-coverage-law-relief/verify.py @@ -0,0 +1,516 @@ +#!/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 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): + + * 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 + 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 + 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. + +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, +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. +Contributor: Navinor, with help from opencode. Apache-2.0. +""" +import argparse +import json +from pathlib import Path +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 CrocSwap/integer-mult-bounds#1094 local word per call +WORD_MASS = sum(r * n for r, n in WORD.items()) # 5586 +# 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 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): + 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 + + +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 = [] + 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 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() + + # --- 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 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 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)} + + # --- 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_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 = {} + 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'], + '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'], + '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())