Audit #5561 free helper endpoints against the #5550 P104 endpoint contract (no new κ)

research/p104-free-endpoint-contract-audit/PROOF.md

@@ -0,0 +1,53 @@
+# Why free helper endpoints are the audited P104 contract
+
+## Setting
+A P104 local word has 735 public registers: 104 X sources r, 104 Y targets r+112, and 527 helpers.
+Frames are subspaces F of F_2^9 with native charts T_F. Each helper h has an initial frame A_h and a
+final frame B_h with A_h ⊂ B_h. A MOVE F → G applies T_G T_F⁻¹ and is paid at rank dim G − dim F. An
+ADD/COPY/SCALE requires its registers to sit in one common frame.
+
+## Lemma 1 (chart invariant)
+Let x_k be the independent inputs. If every register r starts with physical content T_{A_r}(x_r), then
+after every event its physical content is T_{cur(r)}(row_r · x). Here row_r is the exact rational row
+replayed by `local.replay`.
+
+*Proof.* MOVE: T_G T_F⁻¹ T_F(v) = T_G(v). Same-chart ADD: T_f(u) + q·T_f(v) = T_f(u + q v), by linearity of T_f.
+COPY and SCALE are the same. INIT/CLEAR of owned fields set the row and the content to zero. ∎
+
+## Lemma 2 (helper autonomy)
+`local.replay` requires every helper row to end as {h:1}, every main row to have the literal expected
+form, and every owned row to end at zero. By Lemma 1, the module therefore maps a helper input
+y = T_{A_h}(x_h) to T_{B_h}(x_h) = T_{B_h} T_{A_h}⁻¹ y. It does not contaminate any other output. ∎
+
+## Proposition (delivered target)
+`native()` lowers U_h = T_{B_h} T_{A_h}⁻¹ = M_left · G_r · M_right. Here M_left and M_right are Clifford
+monomials and G_r is the canonical rank-r native Gaussian with r = dim B_h − dim A_h. Exact signed-Pauli images and a dense
+phase anchor are checked; the independent #5550 checker repeats both checks. Feed the module M_right⁻¹ z for an
+arbitrary fresh z, and apply M_left⁻¹ to its helper output. The composite is then G_r z. So every helper
+delivers one productive rank-r Gaussian on an arbitrary fresh input. The two monomials are ordinary
+routes, priced in `local_routes` and bounded by #5550's ordinary census.
+
+The proposition does not depend on A_h being the zero frame. A higher start reduces the credited rank r
+by exactly the dimension of the removed climb. Nothing beyond the paid MOVEs and the two priced
+monomials enters the delivered target.
+
+## Consequence for #5561
+The #5561 words change only helper initial/final frames, frame labels and MOVE stops. Their legality
+against the #5551 word is #5561's own `retime.py`. The unmodified `local.py` replay and native maps
+accept them, and #5561's verifier passes. The #5550 checker, with only its input lines swapped, binds all 527
+helper endpoints by exact native checks. It reproduces the invoice from MOVEs and native ranks, and fits the
+ordinary census inside the retained allowance (`verify.py`). Hence hypothesis (c) adds nothing to the
+contract under which #5545 was audited.
+
+## Precedent
+- #5545 (audited by #5550): 192 nonzero helper starts and 65 below-FULL finals.
+- T74 entering helpers: S_E = T_FULL T_E⁻¹ = L_E (C_[w] ⊗ I) R_E, with paid wrappers (#458, Lemma A).
+- Hyperplane-ended helpers: residual T_U T_E⁻¹ with pair wrappers R_(E,U), L_(E,U) (#591 review).
+- The one recorded failure of an entering helper (PR2478 audit of T74) came from that emitter's separate
+  zero-frame precondition phase, which ran before the entry adapters. A P104 word is a single chronology
+  checked by Lemma 1, and it has no such phase.
+
+## Not covered
+Retime legality, pricing, strictification and outer funding of #5561. Validity of the #5551 parent.
+Inherited local all-input native semantics and the five framework assumptions. Human or proof-kernel
+acceptance.

research/p104-free-endpoint-contract-audit/README.md

@@ -0,0 +1,89 @@
+# Free helper endpoints of #5561 under the audited P104 endpoint contract
+
+**Result (scoped audit, no new κ).** The "free helper start and final frames" hypothesis (c) of
+[#5561](https://github.com/CrocSwap/integer-mult-bounds/pull/5561) is the general helper-endpoint
+contract that the unmodified P104 `local.py` already implements. Chris R's independent caller audit
+[#5550](https://github.com/CrocSwap/integer-mult-bounds/pull/5550) checked that contract on the
+[#5545](https://github.com/CrocSwap/integer-mult-bounds/pull/5545) word. The same checker passes on
+both #5561 words when only the word and its invoice are swapped in.
+
+Base: canonical main `5e0052ca0aa3036a3afa8b0438927377c8d97d53`. Audited source: #5561 head
+`452d27dde67ee9f772dbbd3be129db97a8ecb9c1`. The words are byte copies in `inputs/` (SHA-256 in SOURCES.json).
+
+## What is checked
+
+| Check | Result |
+|---|---|
+| #5545 word (audited by #5550) | 192 of 527 helpers start at a nonzero frame (dims 1, 4, 5); 65 end below FULL; 40 distinct endpoint pairs |
+| Positive control | The patched #5550 checker on the #5545 word and invoice reproduces #5550's complete frozen output, SHA-256 `b51a7d19c10faea7d569a48e9536db8ba1e7418f8dd8dfb25646cc87cc9c4009`, byte for byte |
+| #5561 headline word | PASS: 527 helper endpoints, 272 exact signed-Pauli and phase-anchor checks, invoice 66,852 paid / 12,814 productive, ordinary passes 124,232,680 ≤ 184,647,552 |
+| #5561 starts-only word | PASS: 278 exact checks, invoice 67,374 / 12,814, ordinary passes 124,754,680 ≤ 184,647,552 |
+| Negative controls | Changed helper endpoint rejected; changed invoice rejected; all ten #5550 controls reject on each word |
+
+For comparison, the #5561 headline word has fewer nonzero helper starts (58) than the already audited #5545 word (192).
+Its 44 below-FULL finals are also fewer than #5545's 65. The starts-only word has 59 and 65.
+
+## Why this is the existing contract
+
+`native()` in `research/p104-productive-controller/local.py` credits each helper with the rank of
+`chart(initial)⁻¹·chart(final)` for any nested pair of frames. It also charges two normalizers per helper as
+ordinary routes. #5550 ([PROOF.md](../p104-caller-independent-audit/PROOF.md), "Helpers, scratch and
+paid jobs") makes the mechanism explicit. Each endpoint lowers to U = M_left·G_r·M_right. M_right⁻¹ acts on the
+fresh helper input before its LOCAL call and M_left⁻¹ after it. This relies on the local all-input ABI, which
+`replay()` checks row by row. A helper from E to B therefore delivers the native Gaussian G_r, with
+r = dim B − dim E, on an arbitrary fresh input. Only r is credited. Starting higher lowers the credited rank by
+exactly the climb it removes.
+
+The same wrapper mechanism appears in the T74 lineage. Entering helpers use paid residual wrappers
+R_E⁻¹/L_E⁻¹ (#458, Lemma A in `hpe_emit_local.py`). Hyperplane-ended helpers use pair wrappers R_(E,U), L_(E,U)
+([review](../../docs/research/community-hyperplane599-review.md)). The canonical start rule cited in #5561 belongs to the
+#4610/#5413 neutral caller, whose helper adapters J are pure coordinate permutations. It is not a
+predicate of the P104 contract. [PROOF.md](PROOF.md) gives the argument.
+
+## What the verifier changes
+
+`verify.py` copies the authenticated #5550 capsule to a temporary directory. It then replaces exactly four literal lines of
+its checker, each of which must occur once:
+
+1. Read the word from the given path, not the pinned #5545 word.
+2. Take the expected helper profile as a parameter, not the #5545 literal.
+3. Take the invoice from `inputs/INVOICE.json`, a byte extract of #5561's `RESULT.json`. The checker
+   recounts paid MOVEs and native target ranks and requires equality.
+4. Recompute `local_routes` from the MOVE count with the source formula (paid + 2·527 + 208 + 4·104 + 4·8)·1000.
+
+The canonical capsule is never edited. The positive control shows the four changes are faithful.
+
+## Reproduce
+
+Python 3.12+, standard library only:
+
+```sh
+python3 -B research/p104-free-endpoint-contract-audit/verify.py
+```
+
+The run takes about three minutes and should end with the marker `PASS_P104_FREE_ENDPOINT_CONTRACT_AUDIT`. `RESULT.json` holds the complete result.
+
+## Scope and limits
+
+This addresses only hypothesis (c) of #5561, and therefore also the mid-frame start hypothesis of
+[#5553](https://github.com/CrocSwap/integer-mult-bounds/pull/5553). It does not check the retime
+legality (#5561's own `retime.py`), the pricing or strictification, the outer conjunction, or the
+validity of the #5551 parent word. Those checks belong to #5561's verifier and the pending #5551 admission.
+The certified endpoints of the source are its checker constants KAPPA = .00308142 (headline) and
+.003076879 (starts-only), as noted in the intake record. Inherited local all-input native semantics,
+the five framework assumptions and maintainer acceptance remain. This is an agent check, not human
+or proof-kernel acceptance.
+
+## Open next questions
+
+- Admission of the #5551 parent word, on which #5561 and #5553 build (pending, with #5548/#5550/#5557 support).
+- Correction of #5561's claim lines to its certified endpoints .00308142 and .003076879.
+- A deterministic generator for the #5561 retime, so that a checker is not the only reproduction route.
+
+## Credit
+
+Chris R / Clear1nsight (#5550 checker, used unchanged except the four input lines). DreamingOfClouds
+(#5561, #5553). thu-nmrc (#5551). Ali Romman (#5544/#5545 and the P104 caller). chafreaky (#458
+wrappers). The P104 lineage (#2305, #2152, #2219) and all retained native, Clifford, compiler and analytic
+contributors are credited in the cited packages. This package was prepared for Matarener with Claude (Anthropic), via
+Claude Code. Apache-2.0.

research/p104-free-endpoint-contract-audit/RESULT.json

@@ -0,0 +1,77 @@
+{
+ "headline": {
+  "census": {
+   "below_full_finals": 44,
+   "distinct_endpoint_pairs": 32,
+   "final_dims": {
+    "4": 27,
+    "5": 5,
+    "8": 12,
+    "9": 483
+   },
+   "helpers": 527,
+   "nonzero_starts": 58,
+   "start_dims": {
+    "0": 469,
+    "1": 2,
+    "5": 56
+   }
+  },
+  "certified_kappa_of_source": "154071/50000000",
+  "exact_native_checks": 272,
+  "ordinary_allowance": 184647552,
+  "ordinary_passes": 124232680,
+  "output_sha256": "e7bc506894359007b38552e99c93346a67fc3c754b8982595c7ae79b678bb3f4",
+  "paid_jobs": 66852,
+  "productive_fields": 12814
+ },
+ "negative_controls": {
+  "changed_helper_endpoint": "rejected",
+  "changed_invoice": "rejected"
+ },
+ "pr5545_census": {
+  "below_full_finals": 65,
+  "distinct_endpoint_pairs": 40,
+  "final_dims": {
+   "4": 27,
+   "5": 4,
+   "8": 34,
+   "9": 462
+  },
+  "helpers": 527,
+  "nonzero_starts": 192,
+  "start_dims": {
+   "0": 335,
+   "1": 136,
+   "4": 32,
+   "5": 24
+  }
+ },
+ "starts_only": {
+  "census": {
+   "below_full_finals": 65,
+   "distinct_endpoint_pairs": 35,
+   "final_dims": {
+    "4": 27,
+    "5": 4,
+    "8": 34,
+    "9": 462
+   },
+   "helpers": 527,
+   "nonzero_starts": 59,
+   "start_dims": {
+    "0": 468,
+    "1": 2,
+    "4": 1,
+    "5": 56
+   }
+  },
+  "certified_kappa_of_source": "3076879/1000000000",
+  "exact_native_checks": 278,
+  "ordinary_allowance": 184647552,
+  "ordinary_passes": 124754680,
+  "output_sha256": "a4d61875640bad3ca3c82ea08c764381f275bb6fa798b5c2c6db3f4d80275e60",
+  "paid_jobs": 67374,
+  "productive_fields": 12814
+ }
+}

research/p104-free-endpoint-contract-audit/SOURCES.json

@@ -0,0 +1,87 @@
+{
+  "schema_version": 1,
+  "base_commit": "5e0052ca0aa3036a3afa8b0438927377c8d97d53",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446",
+      "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/p104-caller-independent-audit/CAPSULE-INVENTORY.json",
+      "usage": "input",
+      "git_blob": "07c7b818f02c2aabab4798c3e8203ffd2fe1e827",
+      "sha256": "c3e525f5d42ad5b274b039db42f97a2b6e372b583d382c73f59dcb3142f1960d"
+    },
+    {
+      "path": "research/p104-caller-independent-audit/expected/caller.json.gz",
+      "usage": "input",
+      "git_blob": "812ef403ffb149c6230e4a58f29bea75c38f9ba2",
+      "sha256": "383509fce75e2d364138775a4fc96181c9c4cf2608eda0819a7c0c6236faa679"
+    },
+    {
+      "path": "research/p104-full-frame-contact/WORD.json.gz",
+      "usage": "input",
+      "git_blob": "1ce96b0130daeea46ef53fdbd32bca2727aa6b35",
+      "sha256": "a1e416add9d2bb44fce923111ebc50513e5d845e56aabe214f2f0bc7d5f2b45d"
+    },
+    {
+      "path": "research/p104-native-channel/vendor/clifford_exact.py",
+      "usage": "input",
+      "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2",
+      "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962"
+    },
+    {
+      "path": "research/p104-native-channel/vendor/native_verify.py",
+      "usage": "input",
+      "git_blob": "2c209dfa9cfade3bc20ac5fc9d876b433a147f8c",
+      "sha256": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38"
+    },
+    {
+      "path": "research/pr4359-p7-padding/native_inventory.py",
+      "usage": "input",
+      "git_blob": "8d2d96e3998254c2333c43fe47cdfd074cbd811e",
+      "sha256": "65539acaf45bdfe8c5aee6830f9c9b3d1107c442a60842ef803fdd7688de8f32"
+    },
+    {
+      "path": "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json",
+      "usage": "input",
+      "git_blob": "d9a4f84211182ca200c081ea061d724c8a2cfb70",
+      "sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa"
+    },
+    {
+      "path": "research/p104-caller-independent-audit/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "3a74b71a55753a6e7cb372d98b0074cf98dc8708",
+      "sha256": "d73ff9587a85db8063391919ffc4a17521ccd5759cdaf6338ba036703239d839"
+    },
+    {
+      "path": "research/p104-productive-controller/local.py",
+      "usage": "provenance",
+      "git_blob": "dbb3d56a4f5b733bb0c32a91249d1f6a7e1ab5d2",
+      "sha256": "878734dfd64c4b9d362d0ae476cc5c2a19fe93e48b7378763b23f3e0dd0a5a71"
+    }
+  ],
+  "package_inputs": {
+    "INVOICE.json": "703d91eb2bb19caa22367c3b84dc7f7c666b3b94341981284e46cf998bbe7d84",
+    "pr5561-WORD.json.gz": "b3701d78bee3661382ebe5414e678dfc9ee292e254cb9dc56339c2d2f45fdf44",
+    "pr5561-WORD-STARTS-ONLY.json.gz": "c9d978ba90a3ddf6d50529a010ddb5dadc56554c99a15c36378b999deb6d6a20"
+  },
+  "external_sources": {
+    "pr5561": {
+      "head": "452d27dde67ee9f772dbbd3be129db97a8ecb9c1",
+      "files": {
+        "research/p104-free-endpoint-retime/WORD.json.gz": "inputs/pr5561-WORD.json.gz",
+        "research/p104-free-endpoint-retime/WORD-STARTS-ONLY.json.gz": "inputs/pr5561-WORD-STARTS-ONLY.json.gz",
+        "research/p104-free-endpoint-retime/RESULT.json": "inputs/INVOICE.json (extract)"
+      }
+    }
+  }
+}