Independent replay, invoice, native and funding audit of #5827 and #5907 (no new κ)

research/p104-unread-rung-independent-audit/PROOF.md

@@ -0,0 +1,90 @@
+# Proof notes for the PR5827 / PR5907 audit
+
+All statements concern the fixed P104 local words on canonical main `19fdb086ea96af9a9f87936a2b888e10af4ed810`:
+`research/p104-unread-path-resynthesis/inputs/pr5811-WORD.json.gz` (PR5811),
+`research/p104-unread-path-resynthesis/WORD.json.gz` (PR5827) and
+`research/p104-helper468-rung-removal/WORD.json.gz` (PR5907), with the complete invoices in each package's `RESULT.json`.
+
+## Layer 0: sources
+
+PR5907 pins a tar archive of the PR5827 package and runs its chain from there. Every archive member is compared
+with the file at the same path on canonical main and must be equal byte for byte, so the PR5907 chain runs the
+canonical PR5827 code. PR5907's own `construct.py` then regenerates its word from the pinned PR5827 word and
+`EDIT.json.gz`. The decompressed payload must equal the shipped word. The two gzip containers may differ only in
+header byte 9 (the OS code), and that byte is reported. That byte is why PR5907's own byte-for-byte check fails
+on Linux.
+
+## Layer 1: replay and deltas
+
+`replay()` imports nothing from the packages. Frames are bases of subspaces of F2^9, and their spans are built as
+sets. For every event it checks:
+
+- MOVE: the register is in the source frame and its ownership flag is correct. The target span strictly contains
+  the source span (public) or is strictly contained in it (owned). The paid rank is the dimension gap.
+- ADD, COPY, SCALE: the coefficient is a nonzero dyadic rational, and the destination and source registers are in
+  the event's frame, so the scalar operation runs in a common chart. COPY writes only into a cleared owned field.
+- INIT and CLEAR: owned lifetimes, erasure in the declared frame.
+
+At the end every public register is in its final frame and no owned field is live. The 770 + 29 rational rows must
+equal the identity on public registers, plus X added into Y = X + 112 for the 104 live ports. Owned rows must be
+zero. For each helper (a public register that is not a main port) the initial span must lie strictly inside the
+final span. Its credited target rank is the dimension gap.
+
+PR5811 → PR5827: the programs agree outside one window of seven events starting at index 13815. The paid multisets
+differ by −H1 − H4 + H5. Boundaries, frames, ports and the helper profile are equal. The identity of the window is
+implied by the full endpoint check on both words.
+
+PR5827 → PR5907: frames, live ports and port frames are equal. The boundary charts differ in exactly five entries:
+initial 557 (3→105) and 765 (245→263), final 455 (105→925), 557 (105→925) and 765 (127→742). The helper ranks of
+455, 557 and 765 become 7, 6 and 3 (from 1 each). The paid delta is −4H1 + H4 + H6 + H7 and the target delta is
+−3H1 + H3 + H6 + H7. The paid and target rank masses both rise by 13, so the surplus is unchanged. Per local call
+the moment margin changes by H1 + H3 − H4. That is positive for 0 < t < 1, because 4^t < 1 + 3^t.
+
+## Layer 2: invoice
+
+The invoice is rebuilt from `research/p104-productive-controller/CONTROLLER.json`. Each LOCAL event adds the local
+paid and helper profiles. Each QUERY_SHEAR adds 104·H1. Each IDLE over L blocks adds 208·H_{8L}. Each diagonal term
+adds 104·H_{1+8s}. The same totals are then built from the closed formula
+
+    P = 18 P_local + 1560 H1 + 208 Σ_{L∈{7,8}} Σ_{j=1..L} H_{8(j+1)}
+    T = 18 T_local + 208 H145 + 208 Σ_{L∈{7,8}} Σ_{j=1..L} H_{1+8(j+1)}
+
+The two must agree with each other and with the author's `complete_cost`.
+
+## Layer 3: native maps
+
+For a MOVE from frame A to frame B the native operator is chart(A)⁻¹ chart(B). The canonical compiler
+`clifford_exact.lower_child` lowers it to a recipe. The literal definition is `adjoint(frame(A)) + frame(B)`
+from `native_verify.py`. PR5548's dense interpreter evaluates both circuits exactly, with Gaussian-dyadic
+integers, on each of the 512 basis inputs. We require
+
+1. exact equality of every column, including absolute phase;
+2. squared norm one for every column;
+3. exactly 2^rank nonzero entries in every column, where rank is the paid rank of that transition.
+
+The same check runs for each distinct helper pair (chart(initial)⁻¹ chart(final), credited rank
+dim final − dim initial). The 208 intrinsic main adapters must lower at rank zero. The inventory is the union over
+PR5827 and PR5907 of 3,163 operators. Seven of them are new in PR5907: MOVE 3→712, 3→925, 105→925, 712→127 and
+helper pairs 3→925, 105→925, 263→742. One is used only by PR5827: MOVE 593→859. A phase-only fault (same signed
+tableau) and a flipped child sign on map 3→712 are both rejected.
+
+## Layer 4: funding
+
+The moment margin at κ is Σ_targets n·r^(1−κ) − Σ_paid n·r^(1−κ). Each power is exp((1−κ)·ln r), computed with 80
+significant digits and widened by a relative 10⁻⁷⁰. Bisection on the grid 10⁻¹⁴ gives the largest grid point with
+a certified positive margin and the next one with a certified negative margin. These must equal each author's
+`raw_root_interval`.
+
+At the tested saving s the decimal engine also checks the three charged tail ratios, with cutoff 16, floor 17 and
+offset 1/7:
+α = M_P(1−s)/M_T(1−s) < 1 − 10⁻¹², γ = M_P(1−s+1/7)/(16^{1/7} M_T(1−s)) < 125/128 and
+δ = 17·|T|/(16^s M_T(1−s)) < 125/128.
+
+The derivative of the margin in κ is −Σ_T n ln r · r^{1−κ} + Σ_P n ln r · r^{1−κ}. It is bounded above on
+[0, .0034] by taking target terms at exponent 1 − .0034 and paid terms at exponent 1. The bound is negative, so
+each crossing is unique there. The engine shares no code with the authors' two moment engines.
+
+## Not covered
+
+The uniform compiler for all recursion levels, owned erasure, precision and tape costs and analytic recovery are
+inherited premises. The compiler threshold and the outer conjunction are checked only by the authors' verifiers.

research/p104-unread-rung-independent-audit/README.md

@@ -0,0 +1,77 @@
+# Independent replay, invoice, native and funding audit of PR5827 and PR5907
+
+**Result (scoped audit, no new κ).** An independent check of the two latest conditional P104 words finds no
+error. It covers [PR #5827](https://github.com/CrocSwap/integer-mult-bounds/pull/5827) (Ali Romman, unread-path
+resynthesis, κ 0.00312476680) and [PR #5907](https://github.com/CrocSwap/integer-mult-bounds/pull/5907)
+(DreamingOfClouds, helper 468 rung removal, κ 0.003125282). For both words, an own exact replay, an own invoice
+recount, a dense all-column native check with absolute phase and an own decimal funding engine reproduce the
+authors' claims. That includes the exact raw crossings (.00312476681507, .00312476681508) and
+(.00312528909884, .00312528909885). One reproducibility defect was found: PR5907's `verify.py` fails on Linux
+(see below). Its mathematical content is unaffected.
+
+Base: canonical main `19fdb086ea96af9a9f87936a2b888e10af4ed810`, which contains both packages
+(`research/p104-unread-path-resynthesis`, head `05cd36e5`, and `research/p104-helper468-rung-removal`, head
+`c1cbd9e3`). The intake ledger records both as `partially_reviewed`, with "independent scientific review and
+source-bound replay remain open". This package supplies that review for the finite local words and their
+complete invoices. Live inputs are pinned in [SOURCES.json](SOURCES.json).
+
+## What is checked
+
+| Layer | Check | Result |
+|---|---|---|
+| Author verifiers | `verify.py` of PR5827 and PR5907, Python 3.12.3 on Linux, zlib 1.3 | PR5827 PASS (5.4 min). PR5907 stops at `Entire regenerated WORD.json.gz, byte for byte`. The two containers differ only in gzip header byte 9 (OS code 0x13 in the shipped file, 0x03 from Linux zlib) and the payloads are equal. With that one comparison made on the decompressed payload (as CONTRIBUTING.md asks), the complete PR5907 chain passes, including its committed RESULT.json (5.5 min) |
+| 0. Sources | PR5827 archive pinned inside PR5907 against the canonical PR5827 package; PR5907 `construct.py` | all archive members equal canonical main byte for byte; regenerated PR5907 word equals the shipped word after decompression |
+| 1. Own replay, importing nothing from the packages | PR5811, PR5827 and PR5907 words: strict span nesting of every MOVE, common chart of every ADD/COPY/SCALE, dyadic coefficients, owned INIT/CLEAR lifetimes, all 799 endpoint rows (identity on public registers plus X into Y for the 104 live ports), strict nesting of every helper's initial span in its final span | PASS on all three words: 770 public, 29 owned labels, 31 lifetimes, peak 13 |
+| | PR5811 → PR5827 | exactly the seven events from index 13815 change; paid delta −H1 − H4 + H5; boundaries and helper profile unchanged; one ADD added |
+| | PR5827 → PR5907 | exactly the five declared boundary changes (initial 557: 3→105, 765: 245→263; final 455, 557: 105→925, 765: 127→742); helper ranks 1→7, 1→6, 1→3; paid delta −4H1 + H4 + H6 + H7; target delta −3H1 + H3 + H6 + H7; one MOVE fewer, 15 ADDs more; 25,998 events ≤ 26,000 |
+| 2. Invoice | own recount from the 51 physical caller events (18 LOCAL, 15 QUERY_SHEAR, 15 IDLE, diagonal terms) and separately from the closed formula in PR5827 PROOF.md | equal to each author `complete_cost`: 66,870 / 13,444 (PR5827) and 66,852 / 13,444 (PR5907); rank-mass surplus 760 |
+| 3. Dense native inventory | PR5548's credited exact Gaussian-dyadic interpreter compares the lowered recipe with the literal frame circuit on all 512 columns: exact equality, norm, support size 2^rank | PASS on the union of both inventories: 3,163 operators (2,918 and 2,921 distinct signed maps, matching the authors, plus 208 main adapters), 8.3·10⁸ complex entries. A phase-only fault with an unchanged signed tableau and a flipped child sign on the new map 3 → 712 are both rejected |
+| 4. Own funding engine | 80-digit decimal ln/exp with 10⁻⁷⁰ relative padding, bisection on a 10⁻¹⁴ grid | both raw crossings equal the author intervals; tested savings .003124766805 and .0031252870 positive; the tail ratios α < 1 − 10⁻¹², γ, δ < 125/128 hold at the tested savings; the margin derivative is negative on [0, .0034], so each crossing is unique there |
+
+The gain of PR5907 over PR5827 per local call is H1 + H3 − H4 in the moment margin. It is positive for every t in (0, 1).
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3.12 -B research/p104-unread-rung-independent-audit/verify.py
+```
+
+The default run is serial and takes about three minutes. It checks layers 0, 1, 2 and 4 completely. For layer 3 it
+checks a fixed subset: all seven maps new in PR5907, every helper pair, every 8th main adapter and every 64th MOVE
+map. Each digest must equal [FULL-CHECK.json](FULL-CHECK.json). The complete inventory runs with
+
+```sh
+python3.12 -B research/p104-unread-rung-independent-audit/verify.py --full --jobs 4
+```
+
+in about 15 minutes on four cores. It recomputes all 3,163 digests. The marker is
+`PASS_P104_5827_5907_INDEPENDENT_AUDIT`. [PROOF.md](PROOF.md) explains each layer.
+
+## Scope and limits
+
+This audits the finite 9-qubit local words and their complete invoices. The five inherited framework assumptions
+remain: native_all_columns for the uniform word, owned_erasure, compiler, precision_tape and analytic_recovery.
+The physical caller (`research/p104-productive-controller`, unchanged since its admission in `e2a6cce2f`) is
+recounted, not re-derived. The compiler threshold and the 54 strict and 4 functional outer conditions are checked
+only by the authors' code, which passes here. This is an agent check, not human or proof-kernel acceptance. It does
+not change the selected record.
+
+## Open next questions
+
+- Should PR5907's verifier compare the decompressed word? A one-line change makes it pass on Linux hosts, and
+  hosted CI is likely to hit the same failure. First step: replace the byte comparison in `verify.py` line 55 by
+  a payload comparison, as in this audit's layer 0.
+- Can maintainers admit PR5827 and PR5907 on this evidence, with the inherited premises unchanged? First step:
+  intake review of this package against the ledger entries for #5827 and #5907.
+- Do the uniform-compiler premises bind to the FULL-CHECK.json digests, so that the finite native check carries
+  to every recursion level? This is still blocked by the inherited native_all_columns premise.
+
+## Credit
+
+Ali Romman (PR5827 word, verifier and lineage, with OpenAI Codex assistance) and DreamingOfClouds (PR5907 edit
+and packaging). Mason Hale (PR5811). Chris R / Clear1nsight (PR5548 dense interpreter, imported unchanged).
+unpaidmoon (frame-rank correction of the PR5827 early read). The P104 native, Clifford, controller, 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.