Independent verification: prove and certify the a < D/E diagnostic for the selected complex and bit ledgers (no new kappa)

research/selected-suppliers-de-diagnostic/README.md

@@ -0,0 +1,169 @@
+# selected-suppliers-de-diagnostic
+
+**Independent verification and diagnostic only. No new kappa; the selected
+record is unchanged.**
+
+Contributor: Navinor (with help from opencode). Apache-2.0. Task card:
+[TASK-CARD.md](TASK-CARD.md); structured metadata: [TASK.json](TASK.json).
+
+## What is checked
+
+One selected pricing claim and one prescribed diagnostic, for both supplier
+ledgers of the selected record
+([`certificates/selected-result.json`](../../certificates/selected-result.json)):
+
+1. **Moment acceptance of the whole completed construction.** The priced bill
+   of a ledger with width `m`, live stock `W`, histogram `n_r` and bad-residue
+   surcharge coefficient `c_s` is
+
+   `f(a) = (1/(mW)) · Σ_r n_r r (m/r)^a + c_s m^a`.
+
+   The exact moment is the acceptance test: the recorded endpoints must give
+   `f(a) < 1` strictly, and the next `10^-24` grid point must give `f(a) > 1`.
+   This package recomputes both signs for the complex k8/T16 gauge44 ledger
+   (`m = 73`, `W = 14,336`, `N = 144`, no surcharge) and the bit PR589
+   p111-tuned nine-stage ledger (`m = 64`, `W = 28,416`, surcharge
+   `c_s = 32·m·Σn_r / (10^16 W)`) with an implementation disjoint from the
+   retained engines.
+
+2. **The `a < D/E` small-saving diagnostic** of
+   [autoresearch.md](../../autoresearch.md) section 2, which the repository
+   states without an in-repo proof. With `D = mW − Σ n_r r` and
+   `E = Σ n_r r ln(m/r)` (and `D_eff = D − c_s mW`, `E_eff = E + c_s mW ln m`
+   when the surcharge is present) the diagnostic is rigorous:
+
+   **Lemma.** `f` is convex on `ℝ`, `f(0) = 1 − D_eff/(mW) < 1` and
+   `f'(0) = E_eff/(mW) > 0`. The tangent at `a = 0` reaches 1 at
+   `a = D_eff/E_eff`, and convexity gives `f(a) > f(0) + a f'(0)` for `a > 0`.
+   Hence the exact root `a*` satisfies **`a* < D_eff/E_eff` strictly** whenever
+   `D_eff > 0`. For `c_s = 0` this is exactly `a* < D/E`.
+
+   The lemma turns the diagnostic into a valid *screen*: a proposed histogram
+   whose `D/E` is below a target saving cannot reach it. The exact moment
+   remains the acceptance test.
+
+## Results
+
+| Ledger | recorded endpoint `a` | moment residual at `a` | at `a + 10^-24` | certified `D/E` ceiling | `D/E ÷ a` | screening extremum |
+|---|---|---|---|---|---|---|
+| complex (m=73, W=14336) | 0.001675462676808103522925 | −1.304215e-24 | +1.624723e-24 | **0.001680590709754321699421** | 1.003061 | 0.013708749 (cap 51) |
+| bit (m=64, W=28416) | 0.001733427039589844234749 | −1.598690e-24 | +1.669360e-24 | **0.001738557248401367986042** | 1.002960 | 0.016127138 (cap 45) |
+
+- The residual intervals agree with both recorded engines' residuals in
+  `research/community-frontier1094-audit/ASSEMBLY.json` (`mercator` and
+  `base_two`), and reproduce the accept/reject sharpness at the next grid
+  point. The complex values match the independently recorded
+  `moment_minus_one` of
+  `research/community-frontier1094-audit/INDEPENDENT1094.json` digit for digit.
+- The diagnostic overestimates the exact root by about **0.30%** on the
+  complex ledger and **0.29%** on the bit ledger at the current small savings:
+  it is nearly sharp here, and safe as a screen in this regime.
+- The ledger aggregates are reconstructed from the published histograms and
+  checked against the coverage identities: complex `D = 73W − Σ n_r r =
+  W − 64N = 5,120` (which also re-derives `W = 14,336` from the histogram and
+  `N = 144`), and bit `D = 64W − Σ n_r r = T(2Kv − L·cst) = 32(2·4·111 − 9·63)
+  = 10,272`.
+- **Screening extremum.** If a repacking kept `m`, `W` and the rank mass and
+  moved fractional rank mass up to the halving-guard cap (`m² > 2r²`, i.e.
+  `r ≤ 51` for `m = 73` and `r ≤ 45` for `m = 64`), `D/E` could rise to about
+  0.0137 (complex) and 0.0161 (bit). Both exceed the `1/99 ≈ 0.010101`
+  planning target, so the `D/E` screen alone does **not** exclude target-scale
+  gain from repacking; that needs the exact moment plus a coverage/realizability
+  argument. For the complex local word that argument exists: the packing
+  ceiling of
+  [PR #1240](https://github.com/CrocSwap/integer-mult-bounds/pull/1240)
+  (0.001690054109089 for the fixed local word, with idle-mass optimization)
+  supersedes the per-histogram ceiling above and already rules out the target
+  there. The bit word has no such realizability analysis; its question is open.
+
+## Method and independence
+
+`verify.py` imports nothing from the repository's retained engines
+(`moment.py`, `base_two_moment.py`, the atanh prime chain of
+`research/pending-claims-independent-pricing`, or the Mercator/base-two
+transcriptions in `research/community-batch970-audit/submitted/957/`). Exact
+rational arithmetic throughout; every enclosure comes from an explicit
+inequality, and no floating point is used.
+
+- `ln` is enclosed by **rational square-root bisection**: `x^(1/2^k)` is
+  bracketed by repeated integer square roots on a `2^-320` dyadic grid
+  (`k = 112`), then `ln(1+u)` is bracketed by `u − u²/2 ≤ ln(1+u) ≤ u`.
+  This shares no series with the three retained log engines.
+- Independent cross-check: `ln` by **bisection inverting a certified Taylor
+  exponential**. Both methods must agree on every `ln(m/r)` used.
+- `exp` is a Taylor partial sum with an explicit rational geometric tail bound
+  (order 48; the largest exponent used in the bill is `a·ln 73 < 0.0073`, tail
+  below `10^-150`). This matches the standard approach of the retained engines
+  and is disclosed as such.
+- Positive fixtures: the exactly solvable single-rank ledger `H={1:1},
+  m=2, W=1`, whose root is exactly `a* = 1 < 1/ln 2 = D/E`; agreement with the
+  recorded residual intervals; and the reconstructed ledger identities.
+- Semantic failure controls, each required to be rejected: tampered assembly
+  pin; bit ledger priced at the wrong width `m = 73`; a one-count histogram
+  mutation that breaks the complex coverage identity; a child rank outside
+  `(0, m)`; a zero-deficit ledger; claiming the endpoint two grid steps up as
+  accepting; doubling the bit surcharge (breaks acceptance); negative surcharge
+  in the diagnostic.
+
+## Limits
+
+- The paid profiles are taken from the published ledgers
+  (`ASSEMBLY.json` `complex_profile`; `EXPECTED.json` `nine.profile`, pinned by
+  the git blob recorded in the assembly's `bit_supplier` block). This package
+  does not rebuild either word from its original operations; that reconstruction
+  exists for the complex owner map through the audits composed in
+  `research/community-batch1099-audit/check_frontier1094.py`, but not in this
+  package.
+- The conservative (surcharge-on-complex) endpoints of `ASSEMBLY.json` are not
+  rechecked here.
+- `D/E` bounds the root of one fixed histogram. It is not a repacking bound and
+  not a realizability statement (see the screening extremum above).
+- Nothing here verifies the inherited all-size/compiler, common-label/
+  mutable-source realization, whole-call hosting, precision/tape, analytic
+  transfer or bit H1–H5 obligations. This is not a multiplication theorem.
+
+## Reproduce
+
+From the repository root (Python 3.10+, standard library only, seconds):
+
+```sh
+python3 -B research/selected-suppliers-de-diagnostic/verify.py
+python3 scripts/research_package.py --package research/selected-suppliers-de-diagnostic --check-only
+```
+
+Observed: `PASS_INDEPENDENT_DE_DIAGNOSTIC`, 12 controls. Machine-readable
+output: [RESULT.json](RESULT.json).
+
+## Open next questions
+
+- **Bit-word realizability ceiling.** Question: does any repacking of the
+  PR589 bit word's rank mass under its own coverage law stay below `1/99`?
+  Why it matters: the bit side is currently non-binding, but the screening
+  extremum (0.0161) shows the `D/E` screen alone cannot settle it. First step:
+  adapt the idle-mass/coverage-law argument of
+  [PR #1240](https://github.com/CrocSwap/integer-mult-bounds/pull/1240)
+  to the bit coverage identity `D = T(2Kv − L·cst)` and the 32-replica
+  template. Blocker: the bit word's admissible idle inventory and hosting
+  constraints are not yet written as a local profile law.
+- **Ledger reconstruction for the bit supplier.** Question: can `nine.profile`
+  be rebuilt from the original gate operations of the pinned
+  `tune/bitE8mut-p111-tuned.json.gz` word rather than taken from EXPECTED.json?
+  Why it matters: it would close the last aggregate the selected assembly
+  trusts without a from-operations audit. First step: compute the per-frame
+  transition ranks of the word file and compare against `word.local_histogram`
+  and `nine.profile`. Blocker: the paid-rank charging convention lives in the
+  supplier's own checker, so a code-disjoint restatement is a substantial
+  piece of work.
+
+## Credit
+
+Prepared by Navinor (with help from opencode). Predecessor credit: the pricing
+model and the `a < D/E` diagnostic are Douglas Colkitt's (autoresearch.md,
+`research/pending-claims-independent-pricing`); the complex ledger is Rohan
+Arun's #1094 construction on Jeremy Kothe's packing chain, audited by Josie
+Elliston and Sagar Thakrar; the bit supplier is the PR589/PR555 lineage
+(eumemic and predecessors, retained unchanged by the selected record); the
+fixed-word packing-ceiling lineage (including
+[PR #1240](https://github.com/CrocSwap/integer-mult-bounds/pull/1240)) is
+static44, PR525, PR643 and the author of that PR. Substantial AI assistance
+is disclosed: with help from opencode.

research/selected-suppliers-de-diagnostic/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "dadfea6e8a78ff6ba901705f87532a71c6f5bbb8",
+  "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/community-frontier1094-audit/ASSEMBLY.json",
+      "usage": "input",
+      "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0",
+      "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045"
+    },
+    {
+      "path": "research/community-frontier1094-audit/INDEPENDENT1094.json",
+      "usage": "input",
+      "git_blob": "009a385e26858058a18188364078d162aa6f9519",
+      "sha256": "301fb8a0e4ab7e3c383ff974c54c08178283b2a3453c5282757f692a3c7a4bfd"
+    },
+    {
+      "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json",
+      "usage": "input",
+      "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13",
+      "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4"
+    }
+  ]
+}

research/selected-suppliers-de-diagnostic/TASK-CARD.md

@@ -0,0 +1,88 @@
+# Local task card (autoresearch.md section 3)
+
+Task ID / proposed scope key: `independent-moment` / `c6f2494b197df3bc3591`
+(draw: track `independent-verification`, chooser seed
+`9246ead964f301161b3d7eec63704082`, OS-random assignment; refined below to the
+card's "certified enclosure with a different method" variation).
+
+Base commit; exact predecessor and dependency heads:
+`dadfea6e8a78ff6ba901705f87532a71c6f5bbb8` (origin/main at entry).
+Selected record `certificates/selected-result.json`
+(sha256 `10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`);
+selected assembly `research/community-frontier1094-audit/ASSEMBLY.json`
+(sha256 `1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045`);
+bit supplier pin `research/e8-bit-p111-tuned/tune/EXPECTED.json`
+(git blob `e293ddc557742637f9f679f083a1a282d87b1b13`, as recorded inside the
+selected assembly's `bit_supplier` block).
+
+Concrete object and question:
+The two supplier ledgers of the selected record: the complex k8/T16 gauge44
+hosted profile (`complex_profile` in ASSEMBLY.json, width m = 73, live stock
+W = 14,336, calls N = 144) and the bit PR589 p111-tuned nine-stage profile
+(`nine.profile` / `nine.bit.live` in EXPECTED.json, width m = 64, W = 28,416,
+bad-residue surcharge). Question: (1) can the recorded moment acceptance at the
+two certified endpoints be reproduced by a genuinely independent exact
+implementation; (2) what does the prescribed small-saving diagnostic
+`a < D/E` give exactly for each ledger, and is the inequality actually implied
+by the priced moment?
+
+Scope status: refined. The card's question and method are unchanged
+("certified moment inequalities through a different exact enclosure method");
+the refinement names the two ledgers, the endpoints, the widths/stocks and the
+diagnostic. The earlier note that the endpoint-moment card was already covered
+by three code-disjoint engines (Mercator, base-two, atanh prime chain) is why
+this session does not add a fourth series engine: the log enclosure here is by
+rational square-root bisection, the new content is the `a < D/E` lemma and its
+application, and the bit ledger is included (the packing ceiling of
+https://github.com/CrocSwap/integer-mult-bounds/pull/1240 covers the complex
+local word only).
+
+Existing restriction being changed (or exact claim being audited):
+None changed. Audited claims: the ASSEMBLY `moments` accept/reject decisions at
+the complex and bit endpoints (and their next 1e-24 grid points), the ledger
+aggregates `rank_mass`/deficit and their coverage identities, and the
+`a < D/E` diagnostic asserted in autoresearch.md section 2 without an in-repo
+proof.
+
+Method; explicit parameter ranges/candidate alphabet:
+Stdlib-only exact rationals plus outward-rounded dyadic interval arithmetic at
+2^-320. ln by rational square-root bisection (x^(1/2^k) by squaring bisection,
+ln(1+u) bracketed by u - u^2/2 <= ln(1+u) <= u); cross-checked against an
+independent alternating Leibniz enclosure. exp by Taylor partial sums with an
+explicit rational tail bound. Parameters are the fixed ledgers above; the only
+free integer is the bisection depth (k = 32) and Taylor order (48), both
+checked to move intervals by far less than 2^-200. No search domain.
+
+Nearest overlapping PRs and why this adds something:
+https://github.com/CrocSwap/integer-mult-bounds/pull/1240 (complex local-word
+packing ceiling via idle-mass optimization; no bit side, no D/E lemma),
+research/pending-claims-independent-pricing (atanh prime-chain endpoint
+certification for pending claims) and
+research/community-batch970-audit/submitted/957/.../audit_endpoint_reduction.py
+(Mercator/base-two endpoint audit, PR957 lineage). None of them proves or
+computes the `a < D/E` diagnostic or covers the bit ledger's D/E.
+
+Optimistic full cost budget; required observable improvement:
+Budget ~60 minutes total with the last quarter for verification and handoff;
+no kappa change is possible or claimed (this is verification/diagnostic work).
+Required observable: independent residual intervals agreeing with the recorded
+ASSEMBLY residuals and the same accept/reject signs, certified D/E bounds on
+both ledgers, and every semantic failure control rejected.
+
+Success evidence; falsification test; time/compute cap:
+Success = verify.py prints PASS with (i) both moment residuals negative at the
+recorded endpoints and positive at the next grid point, (ii) exact ledger
+identities reproduced, (iii) certified a* < D/E intervals containing decimal
+cross-checks. Falsification = the smallest failing instance: the sign flip of
+the residual at the next grid point, or any mutated ledger that is not
+rejected. Compute cap: seconds per run, stdlib only.
+
+Predecessor authors; intended artifact and reproduction command:
+Predecessors: Douglas Colkitt (repository pricing model, autoresearch
+diagnostic), Rohan Arun (#1094 complex ledger), the PR589 bit supplier lineage
+(eumemic/PR555/PR543 lineage per the selected record), Sagar Thakrar and
+Josie Elliston (independent audits), Jeremy Kothe (packing chain),
+static44/PR525/PR643 and the author of
+https://github.com/CrocSwap/integer-mult-bounds/pull/1240 (packing-ceiling
+lineage). Artifact: `research/selected-suppliers-de-diagnostic/`.
+Command: `python3 -B research/selected-suppliers-de-diagnostic/verify.py`.