Independently join the selected #4470 p16 invoice to its moment bill: exact agreement, surplus below one rank-one job (no new κ)

research/pr4470-invoice-join/PROOF.md

@@ -0,0 +1,81 @@
+# Join and enclosure argument
+
+## 1. Charging model (taken from #4440 PROOF.md sections 1-2, not re-derived)
+
+Complex controller with p = 16 pairs and prefix a = 7, so there are 2p+1 = 33 local stages.
+The thick stages are S = {0, 2p} ∪ {1, 3, ..., 2p-1}, which gives |S| = 18. The model has
+112 ports and fresh block rank d = 8. Events are charged as follows:
+
+- `LOCAL(stage, pair, backward)`: one full native call. It charges one fresh copy of the local
+  helper targets and one copy of the local paid unit for that orientation.
+- `QUERY_SHEAR(stage, ...)`: 112 paid rank-one jobs, one per port. No productive credit.
+- `IDLE(pair, stages)`: both lines of the pair on every port. This is 2·112 paid jobs of rank
+  d·|stages|.
+- `ADD`, `SIGNED_SWAP`: scalar bridges with no rank charge. They sit under the nonrecursive allowance
+  of #4470, which is not checked here.
+- Diagonal output `(c, e_0, ..., e_32)`: c is ±1, the central Gaussian (rank 1). The term gives
+  112 productive targets of rank 1 + d·|{s : e_s = 1}|.
+
+The verifier checks the structural conditions that make this model applicable to the
+committed word:
+
+- one full call per thick stage;
+- one query per thin stage;
+- idle stages are distinct and thick;
+- outputs have 0/1 exponents, support inside S, and c = ±1.
+
+The verifier does not prove that the word realizes the advertised operator. That is the
+Laurent factorization of `research/pr4470-controller-replay`, and both packages pin the same
+`CONTROLLER.json` bytes.
+
+## 2. Join and cross-bindings
+
+T is the sum of the main targets plus 18 helper copies. P is the sum of:
+
+- the idle charges;
+- 112·15 rank-one queries;
+- the forward unit, once per forward call;
+- the backward unit, once per backward call.
+
+The units are read from #4504's committed `RESULT.json`, `profiles.new`. Both orientations are
+required to carry the same paid unit with eight rank-8 center jobs.
+
+The #4440 closed form gives a second derivation that does not use the event word:
+
+- 2·112 targets of rank 1 + d(p+2);
+- for j in 1..a and in 1..p-1-a: 2·112 targets of rank 1 + d(j+1) and 2·112 paid jobs of rank d(j+1);
+- (p+2) units;
+- 112(p-1) queries.
+
+The event-word join and the closed form agree exactly. Their common value equals:
+
+- `RESULT.json` targets/paid;
+- `NATIVE.json.gz` helpers/paid, times the call counts;
+- `CONTROLLER.json`'s embedded invoice after replacing 18 THREE-base units by 18 new units;
+- #4478's literals `T` and `P`.
+
+## 3. Enclosure
+
+For integer k ≥ 1 and rational t ≥ 0, k^t = exp(t ln k). Decimal `ln` and `exp` are documented
+as correctly rounded at the working precision (60 digits). Each returned value v is widened to
+[v - |v|·10⁻²⁰, v + |v|·10⁻²⁰]. Rationals are converted to [floor, ceiling] decimal quotients.
+Products of nonnegative intervals, sums and quotients are rounded outward with `ROUND_FLOOR` /
+`ROUND_CEILING` contexts. exp is increasing, so exp evaluated at the interval endpoints encloses
+the image.
+
+Then M_H(t) = Σ n_k k^t is enclosed for each histogram H. The surplus lower bound is
+M_T,lo − M_P,hi, and the upper bound is M_T,hi − M_P,lo. The tails are enclosed from above by
+using upper bounds in numerators and lower bounds in denominators:
+
+- α = M_P(t)/M_T(t);
+- γ = M_P(t+1/5)/(20^{1/5} M_T(t));
+- δ = 21·|T|/(20^{C} M_T(t)), where t = 1 − C and C = 0.003020155.
+
+The exact rational facts (97/100)^128 < 1/16 and 1/(1 + 1024·10⁻⁹) + 4/2³² < 1 are checked in
+`Fraction`.
+
+## 4. Sharpness
+
+The rank-one moment is 1^t = 1 for every t. The certified upper bounds of the raw surplus at
+κ and at the tested saving are below 1. Adding any single rank-one paid job therefore makes
+both surpluses negative, and the verifier asserts this bound.

research/pr4470-invoice-join/README.md

@@ -0,0 +1,152 @@
+# Independent join of the selected #4470 p16 invoice to its moment bill
+
+**Independent verification; no new κ.** This covers the selected record,
+[#4470](https://github.com/CrocSwap/integer-mult-bounds/pull/4470) (Cinna Davis / 1337isnot1337,
+conditional κ = 60403/20000000 = 0.00302015). It joins two parts that were already independently
+derived, the per-call local unit and the p16 controller word, into the complete target/paid histogram.
+It then checks that histogram against the moment and tail inequalities at the selected κ, using a
+different enclosure method. The verifier is separately written and imports no checker.
+
+Base `cef4b52f2a59009865bf8eabde1be3f159063703`, priority revision 7.
+Claim: [#1166 comment 19137480](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19137480).
+
+## Coverage before this package
+
+| Piece of #4470's changed ledger | Independent coverage |
+| --- | --- |
+| Local unit: helpers `{4:28, 7:7, 8:47, 9:326}`, paid `{1:2237, 2:388, 3:494, 4:147, 5:36, 8:8}` | #4504 frame audit (Mihir Srivastava), both orientations |
+| p16 Laurent factorization and main/idle/thin charges | `research/pr4470-controller-replay` (Ryanson Jonathan) |
+| Changed transport recipes | `research/pr4470-coverage-join` (Clear1nsight) |
+| Root, tails, compiler and outer rows **on a hard-coded histogram** | #4478 (Ryanson Jonathan), whose `T`/`P` literals are "as printed in #4470" |
+| **Complete p16 histogram = controller bill + 18 local units** | author code only (`joint-helper-lattice/verify.py`) |
+| **Moment/tail inequalities on a source-derived histogram** | author code only |
+
+The two bold rows are the gap. #4478 never reads `CONTROLLER.json` or the local unit.
+`CONTROLLER.json`'s own `invoice` uses the older THREE-base unit (69,012 jobs). Only the
+author's substitution step produced the 64,620-job histogram that everyone evaluates.
+
+## Result
+
+**A. Join (exact).** One pass over the 154 committed events gives the following. Full native calls sit
+at exactly the 18 thick stages `{0, 32, 1, 3, …, 31}`: 2 forward and 16 backward. Paid query shears sit
+at exactly the 15 thin stages. The 15 IDLE windows multiply only distinct thick stages. The 32 diagonal
+outputs have central exponent ±1 and no thin-stage credit. The bill is charged as follows:
+
+- each full call gets #4504's unit for its own orientation, plus one fresh copy of the 408 helpers;
+- each query shear gets 112 rank-one jobs;
+- each IDLE window gets 2·112 jobs of rank 8·|stages|;
+- each diagonal output gets 112 targets of rank 1 + 8·|stages|.
+
+The result is:
+
+```text
+targets {4:504, 7:126, 8:846, 9:5868, 17..65 step 8: 448 each, 73:224, 145:224}   10,928 fields, mass 239,886
+paid    {1:41946, 2:6984, 3:8892, 4:2646, 5:648, 8:144, 16..64 step 8: 448 each, 72:224}  64,620 jobs, mass 239,134
+```
+
+The same histogram comes out of all six sources below, exactly:
+
+1. this event-word join;
+2. the #4440 closed form (PROOF.md §2, with no event word);
+3. `RESULT.json`;
+4. `NATIVE.json.gz`'s unit, times the call counts;
+5. `CONTROLLER.json`'s embedded invoice, with the THREE-base unit replaced by the new one;
+6. #4478's `T`/`P` literals (read with `ast`, never executed).
+
+**B. Moment and tails (second method).** The verifier uses Python `decimal` at 60 digits with
+directed rounding. It widens every correctly rounded `ln`/`exp` by 10⁻²⁰ relative, which is far
+more than one ulp. This is a different method from the Fraction atanh/Taylor series used by #4470
+and #4478. Let `T_t − P_t` be the raw surplus, with `t = 1 − saving`. The results:
+
+| Check | Enclosure | Stated limit |
+| --- | --- | --- |
+| raw surplus at κ = 0.00302015 | ≥ 0.00395201766 | > 0 |
+| raw surplus at tested 0.003020155 | ≥ 0.00271523544 | > 0 |
+| root bracket (0.0030201659770, 0.0030201659771) | ≥ 3.86e-9 / ≤ −2.09e-8 | sign change |
+| α = P_t/T_t | ≤ 0.999999988558808 | < 1 − 10⁻⁹ |
+| γ = P_{t+1/5}/(20^{1/5} T_t) | ≤ 0.956176646498 | < 97/100 |
+| δ = 21·10928/(20^{0.003020155} T_t) | ≤ 0.958284435309 | < 97/100 |
+
+These agree with #4470's and #4478's printed values. **No discrepancy was found.**
+
+**Sharpness (new observation).** The whole raw surplus at κ (0.00395) and at the tested saving
+(0.00272) is **below the moment of one rank-one paid job** (1ᵗ = 1). The verifier asserts this.
+Each of the following single-job edits flips the selected κ by itself:
+
+- one extra rank-one paid job;
+- one rank-one job promoted to rank two;
+- one rank-9 helper demoted to rank 8.
+
+The selected record is therefore correct only if the complete p16 invoice is exact at
+single-job resolution. This is not a defect. It does mean an omitted charge of even one query,
+copy or erase would invalidate κ = 0.00302015.
+
+## Controls
+
+The 15 controls below all reject, and the verifier fails if any one passes:
+
+- **Moment controls:** one extra rank-one job; 1→2 promotion; 9→8 helper demotion; κ moved to the
+  root's upper end; the #4447 local unit placed in the p16 word; the predecessor p17 invoice at κ.
+- **Structural controls:** query shear dropped; query shear promoted to a full call; full call demoted
+  to a query; one IDLE stage removed; a diagonal output credited with a thin stage; central exponent 0.
+- **Binding controls:** one backward-unit job shifted; one helper rank lowered; tampered pinned bytes.
+
+All 8 of 8 hand mutants of the verifier's sharp constants fail:
+
+- job count; α limit; port count; κ; thin charge; idle line count; γ limit; and the root upper end
+  moved below the root.
+
+## Not covered
+
+This package does not cover:
+
+- the native word, phases or helper boundaries (#4504, the coverage join and the maintainer review cover these);
+- the Laurent factorization (pr4470-controller-replay covers this);
+- the compiler, BIT admission, the outer ledger rows and their parameters (#4478 covers these from printed parameters);
+- the physical query/owned-stream protocol.
+
+The cost model is taken as stated in #4440 PROOF.md §1–2 and is not re-derived:
+
+- 112 ports;
+- fresh block rank 8;
+- one unit per full call;
+- a query costs one rank-one job per port;
+- idle costs 2·112 jobs of rank 8·|stages|;
+- a main output has rank 1 + 8·|stages|.
+
+The decimal enclosure assumes Python's documented correct rounding of `Decimal.ln`/`exp`, with
+10²⁰-ulp slack. This is a finite certificate for one fixed histogram. It is not a theorem about
+the multiplication algorithm and not a new κ.
+
+## Reproduce
+
+```sh
+python3 scripts/research_package.py --package research/pr4470-invoice-join --check-only
+python3.12 -B scripts/research_package.py --package research/pr4470-invoice-join
+python3.12 -O -B research/pr4470-invoice-join/verify.py
+python3.12 -I -W error -B research/pr4470-invoice-join/verify.py
+```
+
+The verifier prints `PASS_PR4470_INVOICE_JOIN` in under a second, using only the standard library.
+`PROOF.md` states the charging rules and the enclosure argument.
+
+## Open next questions
+
+1. **Single-job completeness of the p16 invoice.** The surplus at κ is below one rank-one job, so is
+   every paid operation of a thin query shear and an IDLE window charged exactly once?
+   *First step:* enumerate one query shear's per-port copy/query/add/erase steps from #4440's protocol.
+   Match each step to a histogram entry or to an explicit nonrecursive allowance.
+2. **Stage-zero unit.** All 18 full calls, including stage 0 (multiplier F9·Q⁻¹), are charged the same
+   #4504 unit, following #4440/#4470. *First step:* compare the stage-zero call's frame audit with the
+   generic unit.
+
+Structured versions are in `TASK.json`.
+
+## Credit
+
+- Construction and claim: Cinna Davis / 1337isnot1337 (#4470, #4440, #4441, #4447). zxv supplied the native/controller lineage.
+- Local unit audit: Mihir Srivastava (#4504). Arithmetic audit and controller replay: Ryanson Jonathan (#4478, pr4470-controller-replay). Coverage join: Clear1nsight.
+- Maintainer review: docs/research/pr-intake-evidence/pr4470/PROOF-REVIEW.md.
+
+Prepared by JoyboyBrian with substantial assistance from Anthropic Claude (Claude Code, Opus 5.5).
+This is not independent human or formal review. Apache-2.0.

research/pr4470-invoice-join/SOURCES.json

@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "input",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/joint-helper-lattice/CONTROLLER.json",
+      "usage": "input",
+      "git_blob": "49a2f0675819f9deeea27ed77be2c2b6ff2e87e5",
+      "sha256": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f"
+    },
+    {
+      "path": "research/joint-helper-lattice/NATIVE.json.gz",
+      "usage": "input",
+      "git_blob": "0910f74138decf498e7fc445cc2daff4390169d6",
+      "sha256": "74582cce642c80f0235be7fcbce3716174666326ac6a1d46d02a62a75d7be4c6"
+    },
+    {
+      "path": "research/joint-helper-lattice/RESULT.json",
+      "usage": "input",
+      "git_blob": "edf41a49a0350862c23378f837c7397fc5dc7596",
+      "sha256": "c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21"
+    },
+    {
+      "path": "research/missing-join-frame/RESULT.json",
+      "usage": "input",
+      "git_blob": "e653fb4358ded67ff1539151f4b670ad9a242fb1",
+      "sha256": "25f2cbcde988847ff86f44e804982069863ec99ff68097f16e9bb7a1a17c4cd0"
+    },
+    {
+      "path": "research/pr4470-arithmetic-check/verify.py",
+      "usage": "input",
+      "git_blob": "629964628fdf5d5695cfd56e0c7bdd69beea5010",
+      "sha256": "eefdc2a1b6ca98d04ecd543428231d2a6ca48090477068d76d5038ea3bd5a09d"
+    },
+    {
+      "path": "research/pr4470-controller-replay/SOURCES.json",
+      "usage": "input",
+      "git_blob": "3df53e9984de185eae263858196da6ecba3e38ca",
+      "sha256": "5d00952f3c969027a04ebcf912d18cc32644e885e39361b00c3d367c21b2dc44"
+    },
+    {
+      "path": "research/pr4470-frame-audit/RESULT.json",
+      "usage": "input",
+      "git_blob": "423d1bbe38023d34419082492bac38b29a80850c",
+      "sha256": "9eae5428e0d083a80c4771439b888f8e559624754be71bb80c2a610ff54c10b7"
+    },
+    {
+      "path": "research/pr4470-frame-audit/SOURCES.json",
+      "usage": "input",
+      "git_blob": "9124bb10fe889a583982b0f5228776c779f092bf",
+      "sha256": "0b2b3bebb675855bb87d2cf6318fcc45c46d2c3f23064a9e765847991bf4ce5f"
+    }
+  ]
+}