Audit the relay premise in the P104 carrier-merge bound (no new κ)

research/carrier-merge-relay-premise/INDEPENDENT-REVIEW.md

@@ -0,0 +1,102 @@
+# Independent review: carrier merging and relay premises
+
+Prepared for @CubeJerry with substantial OpenAI Codex assistance by worker D.
+Apache-2.0. The review concerns #6315 at
+`3667554dab1bf08bb9ce6c267b6047fdc9978498` and worker B's scoped application audit.
+
+## Verdict
+
+The missing-premise finding is valid. The Lean lemmas retain explicit hypotheses
+that the broader prose application does not establish for its allowed shrinking
+steps. This is an application gap, not a flaw in the Lean theorem and not a
+physical counterexample with cost below fourteen for a pair.
+
+Direct source inspection establishes:
+
+- `sup_top_of_cover` requires `G ≤ Z` and a full-span hypothesis for `G` together
+  with the receiver set.
+- `merge_count` explicitly assumes `Z c ⊔ T = ⊤` for every carrier.
+- `pair_merge` explicitly assumes both full-span conditions and `G ≤ W`.
+- The information-walk definition allows a free step to a strict subspace of
+  an earlier node. Therefore the terminal common dual frame need not retain
+  source-normal directions previously visited.
+
+For a fixed carrier c, set H_c=l_c^perp. The walk
+
+    <g_c> -> H_c -> {0}
+
+is an allowed growth followed by shrink in that abstract model. Its paid amount
+is seven, and its union span is H_c. Every receiver in R_c is visited at H_c.
+All carriers can finish at the same W={0}; taking no nontrivial common tail gives
+T={0}. Thus H_c+T has dimension eight, not nine. A pair pays fourteen, violating
+the unqualified proposed intermediate count sixteen, while attaining rather
+than violating the claimed final pair floor fourteen. The formal theorem is
+not contradicted because its full-span hypothesis is false.
+
+The independent finite check uses the pinned predecessor's eight normals/lines
+and all 104 ports from the selected word. For each carrier it enumerates all
+512 binary vectors, the 256-element H_c, its 52 receiver ports, and the entire
+XOR span of <g_c> with those receivers. This verifies all eight witnesses and
+the off-diagonal pairing g_a·l_c=1. It imports neither worker B's executable nor
+the predecessor executable. It does not independently rederive carrier contents
+from the full chronological word; that identification remains an inherited,
+pinned predecessor fact in both this review and worker B's package.
+
+## Repaired count
+
+Under only receiver coverage, let Z_c denote each premerge walk's union span,
+T the common tail union, and W their common starting tail dual frame. Suppose
+W⊆Z_c∩T, pay_c≥dim Z_c−1 and tail≥dim T−dim W. Since
+H_c=<g_c>+span(R_c)⊆Z_c+T, define η_c=dim(Z_c+T)−8∈{0,1}. The modular identity
+gives
+
+    pay_c + tail
+      ≥ dim Z_c + dim T − dim W − 1
+      = dim(Z_c+T) + dim(Z_c∩T) − dim W − 1
+      ≥ 7 + η_c.
+
+Summing yields
+
+    total + (k−1) tail ≥ 7k + Σ_c η_c,
+    total = Σ_c pay_c + tail.
+
+The displayed witness attains this weaker count with η_c=0 and tail=0.
+If a shared premise guarantees every other source normal remains in W, the
+off-diagonal pairing forces η_c=1 for k≥2, recovering the predecessor's stronger
+count. That premise must be supplied; free shrinking does not preserve it.
+
+For pairs with hypothetical total≤13, the repaired inequality only forces
+dim Z_a≤7−η_b and dim Z_b≤7−η_a. Without the missing full-span conditions this
+can be seven, rather than the dimension-six range covered by the predecessor's
+finite `nocover` certificate. This is a scope diagnosis, not evidence that a
+cheaper pair program exists.
+
+An independent exact arithmetic enumeration checked the modular inequality on
+all 383 feasible integer dimension tuples with union dimension eight or nine.
+The displayed symbolic proof establishes the general statement; finite dimension
+checks are corroboration, not a substitute for it.
+
+## Physical scope and remaining obligations
+
+The walk records movement of an information contribution. It does not supply
+the actual public relay roles, isolate pure carriers from arbitrary dirty public
+inputs, restore those inputs, or price the complete physical program. The
+countermodel establishes that the stated abstract walk premises do not imply
+the hypotheses used by the merge argument. The physical pair floor may still
+be true after a different proof or additional realizability restriction.
+
+No new κ, supplier, selected-frontier change, theorem-kernel replay or complete
+multiplier is claimed. Matarener retains credit for #6315's model, valid
+conditional Lean lemmas and finite facts; the selected P104 word, DreamingOfClouds,
+#6166 code identification and retained predecessor lineage keep their credit.
+
+## Addendum: nonzero common merge dual
+
+Reviewer D separately checked the final strengthening by reading the selected
+word directly: carriers {0,1} have 22 common receiver ports and carriers {0,1,2}
+have seven; port 11 lies in both intersections. The listed basis of Y112's
+final frame 128 enumerates exactly 11^perp. Consequently replacing the terminal
+zero in those paths by W=T=<11> preserves valid shrinking steps, path unions,
+paid cost seven per carrier, and failure of both missing hypotheses. This
+confirms availability of an actual selected endpoint chart, without supplying
+the pure-carrier dirty-relay program. No additional code dependency is needed.

research/carrier-merge-relay-premise/PREDECESSOR.json

@@ -0,0 +1,51 @@
+{
+  "files": [
+    {
+      "git_blob": "dddca6c30a16aed2298762ee24fcc98fa9586dee",
+      "retained_path": "research/carrier-merge-relay-premise/inputs/pr6315-PROOF.md",
+      "sha256": "bb760bce0f08006b18996ac8e52ead47cb65f47aa39d582151dbe7a73d4bfa58",
+      "source_head": "3667554dab1bf08bb9ce6c267b6047fdc9978498",
+      "source_path": "research/p104-network-coded-carriers/PROOF.md",
+      "source_pr": 6315,
+      "source_repository": "CrocSwap/integer-mult-bounds"
+    },
+    {
+      "git_blob": "487a2efd9734f258c5c219e5247df1b436060b17",
+      "retained_path": "research/carrier-merge-relay-premise/inputs/pr6315-README.md",
+      "sha256": "8ca925faaa503aeea5832b51d60901c136674455777d17d2d97e57f0aeb0a69b",
+      "source_head": "3667554dab1bf08bb9ce6c267b6047fdc9978498",
+      "source_path": "research/p104-network-coded-carriers/README.md",
+      "source_pr": 6315,
+      "source_repository": "CrocSwap/integer-mult-bounds"
+    },
+    {
+      "git_blob": "03840be5de5acc12aae343fe7d2da24e26feaf91",
+      "retained_path": "research/carrier-merge-relay-premise/inputs/pr6315-RESULT.json",
+      "sha256": "6db1b3fadd64f643731879ec4fdb661e36da97e5969424e6364628b5f2e3780d",
+      "source_head": "3667554dab1bf08bb9ce6c267b6047fdc9978498",
+      "source_path": "research/p104-network-coded-carriers/RESULT.json",
+      "source_pr": 6315,
+      "source_repository": "CrocSwap/integer-mult-bounds"
+    },
+    {
+      "git_blob": "3616ecd1ae4d7c6d076e9eb8a3a5f38c3f7a7e8c",
+      "retained_path": "research/carrier-merge-relay-premise/inputs/pr6315-Walk.lean",
+      "sha256": "95a7b2d39e4ba52a5a2c4018a3ddc2d3335ef099b9757e314d9af9031dc1a28b",
+      "source_head": "3667554dab1bf08bb9ce6c267b6047fdc9978498",
+      "source_path": "research/p104-network-coded-carriers/lean/NetCode/Walk.lean",
+      "source_pr": 6315,
+      "source_repository": "CrocSwap/integer-mult-bounds"
+    },
+    {
+      "git_blob": "cf52884d41030feeb6bf9d49a5c360fd7ecad428",
+      "retained_path": "research/carrier-merge-relay-premise/inputs/pr6315-verify.py",
+      "sha256": "c57cb4123060530161364ca5ed996132cd2a06d3665f79018348d08a1a708aaf",
+      "source_head": "3667554dab1bf08bb9ce6c267b6047fdc9978498",
+      "source_path": "research/p104-network-coded-carriers/verify.py",
+      "source_pr": 6315,
+      "source_repository": "CrocSwap/integer-mult-bounds"
+    }
+  ],
+  "schema": "retained-source-copies-v1",
+  "scope": "Original Git objects authenticated locally before publication; replay checks retained exact bytes without requiring pending commit history."
+}

research/carrier-merge-relay-premise/PROOF.md

@@ -0,0 +1,214 @@
+# A source-normal premise for relay-enabled carrier merges
+
+## Result and classification
+
+At the exact source head of CrocSwap/integer-mult-bounds#6315, the application of
+the merge lemmas to public-relay walks needs an additional argument. Common-frame
+merging does not, by itself, retain every source normal in the merge dual. The
+Lean theorem statements retain the required hypotheses explicitly. This audit
+identifies a missing application implication, not a false Lean theorem and not
+a physical counterexample to the pair cost floor 14 or the owned cost floor 56.
+
+The exact countermodels below satisfy the declared **abstract dual-frame walk**
+rules, source origins, common merge, and coverage of every required receiver.
+They do not supply scalar decoding coefficients, a pure-carrier public relay,
+or restoration of arbitrary public dirt. Those obligations can obstruct these
+walks and might support a corrected physical theorem.
+
+The repaired invariant is
+
+\[
+ \operatorname{total}+(k-1)\tau\ \ge\ 7k+\sum_{c=1}^k\eta_c,
+ \qquad \eta_c\in\{0,1\}.
+\]
+
+Here \(\eta_c\) records whether the carrier's pre-merge and tail union escapes
+its eight-dimensional receiver hyperplane. An explicit source-normal retention
+condition recovers the predecessor's \(8k\) right-hand side. **No new κ.**
+
+## 1. Exact source and missing implication
+
+The audited head is `3667554dab1bf08bb9ce6c267b6047fdc9978498`, by Matarener.
+The five relevant source files are retained verbatim under `inputs/`, with
+original repository/head/path, SHA-256 and Git-blob pins in `PREDECESSOR.json`.
+The metadata manifest is itself pinned by the verifier. The original Git bytes
+were compared before publication; portable replay needs no pending Git history.
+All line numbers below refer to those unchanged files.
+
+| Source | Hypothesis or application |
+|---|---|
+| `pr6315-PROOF.md`, lines 13–20 | Public ascents may shrink duals freely; information walks permit such steps. |
+| `pr6315-PROOF.md`, lines 43–50 | Uses the other carrier's normal to conclude \(Z_c+T=\mathbb F_2^9\). |
+| `pr6315-Walk.lean`, lines 152–153 | `sup_top_of_cover` requires the supplied subspace `G` to lie in `Z`. |
+| `pr6315-Walk.lean`, lines 173–175 | `merge_count` assumes `htop`: every \(Z_c+T\) is the full space. |
+| `pr6315-Walk.lean`, lines 205–207 | `pair_merge` additionally assumes `hG : G ≤ W`. |
+| `pr6315-Walk.lean`, line 217 | `hG` supplies the common source subspace to the finite no-cover predicate. |
+
+The finite fact \(\langle g_a,g_c\rangle+\operatorname{span}R_c=V\) is not the
+missing implication. To use it, the application must place \(g_a\) in the
+relevant union, or prove an equivalent full-span condition. A common merge
+frame only places its own dual \(W\) in each path union; it does not prove
+\(g_a\in W\), or even \(g_a\in Z_c+T\), after arbitrary shrinking steps.
+
+For two carriers, the formal sufficient condition is
+\(\langle g_a,g_b\rangle\subseteq W\). A weaker repair might suffice for the
+application, but it must also establish the source-subspace inclusions used by
+the finite no-cover check. This audit does not re-audit that finite search or
+the separate decoder coefficient argument.
+
+## 2. Concrete selected geometry
+
+Work in \(V=\mathbb F_2^9\), with the standard binary dot product. The selected
+#6030 word supplies its 104 port vectors \(P\). The #6315 receipt supplies these
+paired delivery lines and source normals:
+
+| c | \(\ell_c\) | \(g_c\) |
+|---|---:|---:|
+| 0 | 7 | 104 |
+| 1 | 25 | 162 |
+| 2 | 52 | 266 |
+| 3 | 67 | 97 |
+| 4 | 82 | 289 |
+| 5 | 137 | 127 |
+| 6 | 448 | 42 |
+| 7 | 491 | 76 |
+
+Integers encode nine binary coordinates. For
+\(R_c=\{p\in P:p\cdot\ell_c=0\}\) and \(H_c=\ell_c^\perp\), the independent
+checker verifies directly from these inputs that
+
+\[
+ |R_c|=52,\quad
+ H_c=\langle g_c\rangle+\operatorname{span}R_c,\quad
+ \dim H_c=8,\quad
+ g_a\cdot\ell_c=[a\ne c].
+\]
+
+It does not import the predecessor interpreter. The identity of the source
+receipt's eight carriers with the complete scalar program is inherited; the
+specific geometric facts used here are independently checked against the
+selected port list. No full selected word or decoder replay is claimed.
+
+## 3. Receiver-covering walk countermodels
+
+For any subset \(U\subseteq\{0,\ldots,7\}\) with \(k=|U|\ge2\), take the
+following pre-merge dual walk for every \(c\in U\):
+
+\[
+ \langle g_c\rangle\ \longrightarrow\ H_c\ \longrightarrow\ \{0\}.
+\]
+
+The first step is growth from dimension one to eight, paid at seven. The
+second is a free shrink under the declared information-walk rules. All 52
+receivers lie in the visited node \(H_c\). Set the common merge dual and the
+tail union to \(W=T=\{0\}\), with tail cost \(\tau=0\). The path union is
+exactly \(Z_c=H_c\), and the total frame-walk price is \(7k\).
+
+Thus all source roots, nested steps, receiver coverage, common-merge conditions
+and walk-union price inequalities hold, while
+
+\[
+ \langle g_a:a\in U\rangle\not\subseteq W,
+ \qquad Z_c+T=H_c\ne V.
+\]
+
+For example, \(g_1=162\notin H_0=7^\perp\), because \(162\cdot7=1\).
+The common merge therefore does not force carrier 0's union to contain the
+other source normal. The countermodel exists already for the pair \(\{0,1\}\)
+and the triple \(\{0,1,2\}\). The verifier checks all 247 subsets of sizes two
+through eight, including all 28 pairs and all 56 triples.
+
+In primal frames the walk is
+\(g_c^\perp\to\langle\ell_c\rangle\to V\): an owned descent followed by the
+frame pattern of a public ascent. This is a countermodel to the proposed
+**frame-only implication**. Reading into an arbitrary public helper can add
+its dirt. No pure scalar relay, its dirty restoration, or the resulting full
+physical invoice is constructed here. In particular the pair example costs
+14, so it is not even an abstract witness below the pair floor 14.
+
+The gap does not require a zero-dimensional merge dual. For the pair
+\(\{0,1\}\) and triple \(\{0,1,2\}\), the selected port \(p=11\) lies in every
+required \(H_c\). Replace the final zero by \(W=T=\langle11\rangle\).
+All unions and paid costs remain unchanged, and both missing hypotheses still
+fail. The common primal chart is the actual final chart 128 of selected
+register Y112, whose basis is `(3,4,9,16,32,64,128,256)`; the checker verifies
+that this is exactly \(11^\perp\). There are 22 common selected receiver ports
+for this pair and seven for this triple. These fixtures establish availability
+of an actual endpoint chart; they still do not install multiple pure carriers
+and arbitrary dirty relays into a complete scalar program.
+
+## 4. Repaired invariant
+
+Choose \(1\le k\le8\) distinct carriers from the fixed selected code. For each
+chosen carrier \(c\), assume:
+
+1. Its pre-merge union \(Z_c\) contains \(g_c\), and its paid cost \(p_c\)
+   satisfies \(\dim Z_c\le p_c+1\).
+2. Every required receiver lies in \(Z_c\cup T\).
+3. The merge dual obeys \(W\subseteq Z_c\cap T\), and tail cost satisfies
+   \(\dim T\le\tau+\dim W\).
+
+Since \(H_c=\langle g_c\rangle+\operatorname{span}R_c\), the first two
+conditions give \(H_c\subseteq Z_c+T\). Define
+
+\[
+ \eta_c=\begin{cases}0,&Z_c+T\subseteq H_c,\\1,&\text{otherwise.}\end{cases}
+\]
+
+The hyperplane has dimension eight, hence \(\dim(Z_c+T)=8+\eta_c\).
+The subspace dimension identity and \(W\subseteq Z_c\cap T\) give
+
+\[
+ 8+\eta_c+\dim W
+ \le \dim Z_c+\dim T
+ \le p_c+1+\tau+\dim W.
+\]
+
+Therefore \(p_c+\tau\ge7+\eta_c\). Sum over \(c\), and put
+\(\operatorname{total}=\sum_c p_c+\tau\), to obtain
+
+\[
+ \operatorname{total}+(k-1)\tau\ge7k+\sum_c\eta_c.
+\]
+
+This proof is a dimension argument for arbitrary walks of those chosen
+carriers in the stated relaxation, not an inference from the finite checks. The countermodels attain
+equality with every \(\eta_c=0\), so replacing \(7k\) universally by \(8k\)
+under just these hypotheses is impossible.
+
+If \(k\ge2\) and every source normal is retained in \(W\), choose \(a\ne c\).
+Then \(g_a\in W\subseteq Z_c+T\) and \(g_a\cdot\ell_c=1\), forcing
+\(\eta_c=1\). The predecessor's \(8k\) inequality follows. In particular,
+pre-merge walks consisting only of owned descents preserve their root normals;
+more generally it suffices that every pre-merge step retains its own normal.
+Arbitrary public-relay shrinking is the boundary that still needs a proof.
+
+## 5. Consequence and remaining obligation
+
+The repaired inequality also exposes the finite pair check's scope. If a
+hypothetical pair has `total <= 13`, then
+\(p_b+\tau\ge7+\eta_b\) implies
+\(\dim Z_a\le p_a+1\le7-\eta_b\), and symmetrically
+\(\dim Z_b\le7-\eta_a\). The predecessor's six-dimensional no-cover
+domain is recovered when both indicators are one. Without full-span it can
+instead require dimension-seven coverage, which that finite certificate does
+not establish. This consequence was identified independently by reviewer D;
+it is a scope diagnosis, not evidence of a cheaper physical pair.
+
+The predecessor's Lean statements can remain unchanged. Its general walk and
+single-carrier statements are not contradicted. To apply the stronger merge
+floor to relay-enabled physical programs, supply a source-bound theorem that
+either retains the required normals, establishes the necessary full-span and
+no-cover hypotheses another way, or charges the extra work needed to erase and
+restore those directions. An explicit purity/restoration theorem could resolve
+this gap; its absence is not a physical counterexample.
+
+Until then, an extension to three-carrier merges cannot simply inherit the
+stronger \(8k\) premise from a common merge frame. No triple-merger exclusion,
+native implementation, complete signed supplier invoice, or improvement to the
+multiplication bound is established here. All five selected assumptions remain.
+
+Prepared for @CubeJerry with substantial OpenAI Codex assistance. Credit
+Matarener for #6315 and #6267; DreamingOfClouds for the selected #6030 word;
+the carrier uniqueness, fragmentation and owned-boundary predecessors cited in
+the retained source; and the classical subspace dimension identity.