From f3bebf8236dec18dea8ec6b714a12dda6cf25243 Mon Sep 17 00:00:00 2001 From: CubeJerry <80299683+CubeJerry@users.noreply.github.com> Date: Sat, 31 Oct 2026 11:05:08 +0800 Subject: [PATCH] Audit the relay premise in the P104 carrier-merge bound --- .../INDEPENDENT-REVIEW.md | 102 ++++++ .../PREDECESSOR.json | 51 +++ research/carrier-merge-relay-premise/PROOF.md | 214 +++++++++++ .../carrier-merge-relay-premise/README.md | 100 ++++++ .../carrier-merge-relay-premise/RESULT.json | 215 +++++++++++ .../carrier-merge-relay-premise/SOURCES.json | 24 ++ .../carrier-merge-relay-premise/TASK.json | 90 +++++ .../VALIDATION.json | 126 +++++++ .../carrier-merge-relay-premise/VALIDATION.md | 53 +++ .../carrier-merge-relay-premise/VERIFY.json | 69 ++++ .../independent.py | 95 +++++ .../inputs/pr6315-PROOF.md | 80 +++++ .../inputs/pr6315-README.md | 62 ++++ .../inputs/pr6315-RESULT.json | 124 +++++++ .../inputs/pr6315-Walk.lean | 220 ++++++++++++ .../inputs/pr6315-verify.py | 335 ++++++++++++++++++ .../carrier-merge-relay-premise/verify.py | 273 ++++++++++++++ 17 files changed, 2233 insertions(+) create mode 100644 research/carrier-merge-relay-premise/INDEPENDENT-REVIEW.md create mode 100644 research/carrier-merge-relay-premise/PREDECESSOR.json create mode 100644 research/carrier-merge-relay-premise/PROOF.md create mode 100644 research/carrier-merge-relay-premise/README.md create mode 100644 research/carrier-merge-relay-premise/RESULT.json create mode 100644 research/carrier-merge-relay-premise/SOURCES.json create mode 100644 research/carrier-merge-relay-premise/TASK.json create mode 100644 research/carrier-merge-relay-premise/VALIDATION.json create mode 100644 research/carrier-merge-relay-premise/VALIDATION.md create mode 100644 research/carrier-merge-relay-premise/VERIFY.json create mode 100644 research/carrier-merge-relay-premise/independent.py create mode 100644 research/carrier-merge-relay-premise/inputs/pr6315-PROOF.md create mode 100644 research/carrier-merge-relay-premise/inputs/pr6315-README.md create mode 100644 research/carrier-merge-relay-premise/inputs/pr6315-RESULT.json create mode 100644 research/carrier-merge-relay-premise/inputs/pr6315-Walk.lean create mode 100644 research/carrier-merge-relay-premise/inputs/pr6315-verify.py create mode 100644 research/carrier-merge-relay-premise/verify.py diff --git a/research/carrier-merge-relay-premise/INDEPENDENT-REVIEW.md b/research/carrier-merge-relay-premise/INDEPENDENT-REVIEW.md new file mode 100644 index 0000000000..2cca97b712 --- /dev/null +++ b/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 + + -> 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 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=+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. diff --git a/research/carrier-merge-relay-premise/PREDECESSOR.json b/research/carrier-merge-relay-premise/PREDECESSOR.json new file mode 100644 index 0000000000..86a7fc97ef --- /dev/null +++ b/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." +} diff --git a/research/carrier-merge-relay-premise/PROOF.md b/research/carrier-merge-relay-premise/PROOF.md new file mode 100644 index 0000000000..14cf611ae6 --- /dev/null +++ b/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. diff --git a/research/carrier-merge-relay-premise/README.md b/research/carrier-merge-relay-premise/README.md new file mode 100644 index 0000000000..4c3bb27d56 --- /dev/null +++ b/research/carrier-merge-relay-premise/README.md @@ -0,0 +1,100 @@ +# Audit the source-normal premise in relay-enabled carrier merges + +The merge lemmas in CrocSwap/integer-mult-bounds#6315 explicitly require source +subspace retention and/or full union span. Its broad abstract information-walk +model permits public-relay shrinking, which does not imply those hypotheses. +Using the actual selected #6030 geometry, this package gives receiver-covering +countermodels to that **frame-only implication**, and proves the corrected bound + +`total + (k-1)*tail >= 7k + sum(eta_c)`. + +Each `eta_c` is zero or one according to whether that carrier's union escapes +its receiver hyperplane. Source-normal retention recovers the predecessor's +`8k` right-hand side. **No new κ.** + +This is a precise missing-application-lemma audit, not a false Lean theorem, +a cheaper physical network, a counterexample to the pair floor 14 or owned +floor 56, or an exclusion of triple merges. All five selected framework +assumptions remain. A pure-carrier relay with arbitrary dirty restoration is +not constructed or assumed free. + +## Evidence and reproduction + +Canonical base: `2485805a6d47f36ea83ddde6327d453ac82d44dc`. +Audited #6315 head: `3667554dab1bf08bb9ce6c267b6047fdc9978498`. +Base sources are pinned in [SOURCES.json](SOURCES.json); the exact predecessor +head, original Git paths and retained-byte hashes are in +[PREDECESSOR.json](PREDECESSOR.json), itself pinned by the verifier. +Five relevant predecessor files are retained verbatim under `inputs/`; their +authors and notices are unchanged. The selected word is a declared live input. + +From the repository root, with CPython 3.12 and the standard library: + +```sh +python3 -B scripts/research_package.py --package research/carrier-merge-relay-premise +``` + +Expected: `PASS_CARRIER_MERGE_RELAY_PREMISE subsets=247 controls=11` in both +normal and optimized modes, followed by `PASS_REGISTERED_RESEARCH_PACKAGE`. + +[PROOF.md](PROOF.md) identifies the exact Lean hypotheses and gives the general +repaired proof. [RESULT.json](RESULT.json) is the exact replay receipt. The +independent implementation uses finite sets of binary vectors and imports no +predecessor executable. It checks: + +- All eight source-normal/receiver hyperplanes against the 104 selected ports. +- Every one of 247 carrier subsets, including 28 pairs and 56 triples, with + source roots, nested moves, all 52 receivers per carrier, common merge, + paid growth seven, and explicit failure of `hG` and `htop`. Two further pair/triple + fixtures use the actual selected Y112 endpoint chart with nonzero merge dual `<11>`. +- Seven source-normal-preserving controls that attain the `8k` dimension count; + these controls also test only the frame-walk algebra, not scalar decoding. +- All 2,457 applicable tuples in the enumerated 16-subspace lattice of + `F2^3`, corroborating both values of the repaired excess indicator. +- Eleven rejection controls: wrong paid amount, missing source, illegal nonnested + step, missing receiver growth, false pair/triple hypotheses, unjustified + `8k`, an invalid merge line, and a Boolean disguised as an integer cost. + +To regenerate the canonical receipt without changing repository files: + +```sh +python3 -I -W error -B research/carrier-merge-relay-premise/verify.py --output /absolute/new/external/result.json +``` + +The output path must be new and outside the checkout. Finite replay corroborates +the written dimension argument; it is not a proof-kernel verification of it. + +## Scope and limitations + +The exact countermodel is `line(g_c) -> H_c -> 0` in dual frames. It grows at +cost seven, serves every receiver in `H_c`, then shrinks freely to the common +merge. Such a frame path does not specify how to remove a public helper's +arbitrary dirt. Its scalar feasibility, decoding and restoration invoice are +deliberately unresolved. A physical purity/restoration theorem might supply +the missing implication even though the frame rules alone cannot. + +The correspondence of the source receipt's carrier code with the complete +selected word is inherited; the geometric facts used here are freshly checked. +The predecessor's pair-cover census, Lean build, full selected scalar/native/ +caller replay and complete supplier invoice are not run as this deliverable. +No formal-kernel or human acceptance, supplier admission, or complete +multiplication theorem is claimed. See `VALIDATION.md` for executed release +checks and the independent review. + +## Open next questions + +The structured questions are in [TASK.json](TASK.json). The next useful task +is a physical relay with arbitrary-input purity and restoration, or a proof +that every admissible such relay satisfies the needed source-normal/full-span +conditions after all costs are charged. Only then should the broader +three-carrier search inherit those conditions. The corrected `eta_c` invariant +can be used immediately when the actual unions are known. + +## Credit + +Prepared for @CubeJerry with substantial OpenAI Codex assistance: worker B, +independent mathematical/source reviewer D, and lead review. Credit Matarener +for #6315, #6267 and the question; DreamingOfClouds for #6030; the fragmentation, +owned-boundary and carrier-uniqueness lineage retained in the source files; and +the classical subspace dimension identity. Apache-2.0. No predecessor result +is presented as a new theorem of this package. diff --git a/research/carrier-merge-relay-premise/RESULT.json b/research/carrier-merge-relay-premise/RESULT.json new file mode 100644 index 0000000000..8ddfbab6d7 --- /dev/null +++ b/research/carrier-merge-relay-premise/RESULT.json @@ -0,0 +1,215 @@ +{ + "countermodel_subsets": 247, + "countermodels": [ + { + "eta_sum": 0, + "k": 2, + "missing_htop": 2, + "paid": 14, + "subsets": 28 + }, + { + "eta_sum": 0, + "k": 3, + "missing_htop": 3, + "paid": 21, + "subsets": 56 + }, + { + "eta_sum": 0, + "k": 4, + "missing_htop": 4, + "paid": 28, + "subsets": 70 + }, + { + "eta_sum": 0, + "k": 5, + "missing_htop": 5, + "paid": 35, + "subsets": 56 + }, + { + "eta_sum": 0, + "k": 6, + "missing_htop": 6, + "paid": 42, + "subsets": 28 + }, + { + "eta_sum": 0, + "k": 7, + "missing_htop": 7, + "paid": 49, + "subsets": 8 + }, + { + "eta_sum": 0, + "k": 8, + "missing_htop": 8, + "paid": 56, + "subsets": 1 + } + ], + "geometry": { + "H_dimensions": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + "carrier_lines": [ + 7, + 25, + 52, + 67, + 82, + 137, + 448, + 491 + ], + "ports": 104, + "receivers_each": 52, + "source_normals": [ + 104, + 162, + 266, + 97, + 289, + 127, + 42, + 76 + ] + }, + "negative_controls": [ + "underpriced growth", + "missing source root", + "nonnested step", + "omitted growth", + "pair false hG", + "pair false htop", + "triple false hG", + "triple false htop", + "unjustified 8k", + "invalid merge line", + "boolean paid value" + ], + "new_kappa": false, + "nonzero_merge_examples": [ + { + "carrier_subset": [ + 0, + 1 + ], + "common_receiver_count": 22, + "eta": [ + 0, + 0 + ], + "merge_dual_generator": 11, + "merge_primal_frame": 128, + "path_dimensions": [ + 8, + 8 + ], + "selected_receiver_register": 112, + "total": 14 + }, + { + "carrier_subset": [ + 0, + 1, + 2 + ], + "common_receiver_count": 7, + "eta": [ + 0, + 0, + 0 + ], + "merge_dual_generator": 11, + "merge_primal_frame": 128, + "path_dimensions": [ + 8, + 8, + 8 + ], + "selected_receiver_register": 112, + "total": 21 + } + ], + "schema": "carrier-merge-relay-premise-v1", + "scope": "abstract dual-frame walks; no scalar decoder or dirty restoration verified", + "small_lattice": { + "admissible_tuples": 2457, + "ambient_dimension": 3, + "eta_counts": [ + 294, + 2163 + ], + "subspaces": 16 + }, + "source_preserving_controls": [ + { + "eta_sum": 2, + "k": 2, + "prefix_paid": 2, + "tail_paid": 7, + "total": 9 + }, + { + "eta_sum": 3, + "k": 3, + "prefix_paid": 6, + "tail_paid": 6, + "total": 12 + }, + { + "eta_sum": 4, + "k": 4, + "prefix_paid": 12, + "tail_paid": 5, + "total": 17 + }, + { + "eta_sum": 5, + "k": 5, + "prefix_paid": 20, + "tail_paid": 4, + "total": 24 + }, + { + "eta_sum": 6, + "k": 6, + "prefix_paid": 30, + "tail_paid": 3, + "total": 33 + }, + { + "eta_sum": 7, + "k": 7, + "prefix_paid": 42, + "tail_paid": 2, + "total": 44 + }, + { + "eta_sum": 8, + "k": 8, + "prefix_paid": 56, + "tail_paid": 1, + "total": 57 + } + ], + "source_sha256": { + "research/carrier-merge-relay-premise/inputs/pr6315-PROOF.md": "bb760bce0f08006b18996ac8e52ead47cb65f47aa39d582151dbe7a73d4bfa58", + "research/carrier-merge-relay-premise/inputs/pr6315-README.md": "8ca925faaa503aeea5832b51d60901c136674455777d17d2d97e57f0aeb0a69b", + "research/carrier-merge-relay-premise/inputs/pr6315-RESULT.json": "6db1b3fadd64f643731879ec4fdb661e36da97e5969424e6364628b5f2e3780d", + "research/carrier-merge-relay-premise/inputs/pr6315-Walk.lean": "95a7b2d39e4ba52a5a2c4018a3ddc2d3335ef099b9757e314d9af9031dc1a28b", + "research/carrier-merge-relay-premise/inputs/pr6315-verify.py": "c57cb4123060530161364ca5ed996132cd2a06d3665f79018348d08a1a708aaf", + "research/p104-helper470-twin-rung-removal/WORD.json.gz": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f" + } +} diff --git a/research/carrier-merge-relay-premise/SOURCES.json b/research/carrier-merge-relay-premise/SOURCES.json new file mode 100644 index 0000000000..0e8987f7f6 --- /dev/null +++ b/research/carrier-merge-relay-premise/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "usage": "input", + "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760", + "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f" + } + ] +} diff --git a/research/carrier-merge-relay-premise/TASK.json b/research/carrier-merge-relay-premise/TASK.json new file mode 100644 index 0000000000..044c2b1853 --- /dev/null +++ b/research/carrier-merge-relay-premise/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Audit the source-normal retention premise when applying the #6315 merge lemmas to public-relay information walks; give receiver-covering countermodels and an exact repaired dimension invariant.", + "scope_change_reason": "The assigned three-carrier merge extension depended on source-normal retention. Exact-source inspection found that the Lean theorem assumes this premise whereas the broad abstract walk model permits free shrinking. The lead approved resolving this dependency before any triple census.", + "bottleneck_link": "A false universal transfer of the merge bound would prematurely exclude network-coded complex-supplier mechanisms. The audit separates a missing physical application lemma from a false cost-floor theorem.", + "budget_minutes": 60, + "stop_rule": "Stop after the exact premise discrepancy, all actual carrier subsets, repaired proof and independent review; do not enumerate triple merges under an unproved premise.", + "outcome": "completed", + "evidence": "PROOF.md; RESULT.json; verify.py. Exact source frame geometry, 247 receiver-covering subset countermodels, seven source-normal-preserving positive controls, 2457 small-lattice instances and eleven rejection controls.", + "author": "@CubeJerry", + "ai_assistance": "Substantial OpenAI Codex assistance: research worker B; separate worker D source/mathematical verification; lead review.", + "open_questions": [ + { + "question": "Does every admissible dirty-restored physical relay imply the source-normal/full-span inclusions needed by the merge lemmas, after charging all additional work?", + "why_it_matters": "This determines whether the stronger pair and short-tail bounds extend from source-normal-preserving merges to the public-relay scope.", + "first_step": "Give one exact public-relay scalar program with arbitrary dirty inputs and annotate each retained/lost source normal, compensation and restoration cost.", + "blocked_by": "No physical purity/restoration lemma is supplied by this frame-only audit." + }, + { + "question": "Can three-carrier merges improve the complete paid moment under a valid strengthened boundary contract?", + "why_it_matters": "This remains the original complex-supplier search direction once its imported premises are justified.", + "first_step": "Choose source-normal-preserving walks or prove a different corrected physical interface, then optimize the full paid and target invoice.", + "blocked_by": "The broad public-relay application and a complete scalar decoder/caller are not established here." + } + ], + "track_seed": 44, + "claim_status": "LOCAL-ONLY: Discussion posting tool unavailable; no reservation issue created.", + "coordination": { + "base": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "priority_revision": 8, + "source_pr": 6315, + "source_head": "3667554dab1bf08bb9ce6c267b6047fdc9978498", + "overlap": "Lead inspected recent PR bodies, targeted all-status carrier/merge searches and accessible newest handoffs; public Discussion coverage is partial. No exhaustive novelty claim. Scope pivot approved by lead." + } +} diff --git a/research/carrier-merge-relay-premise/VALIDATION.json b/research/carrier-merge-relay-premise/VALIDATION.json new file mode 100644 index 0000000000..c3691838d2 --- /dev/null +++ b/research/carrier-merge-relay-premise/VALIDATION.json @@ -0,0 +1,126 @@ +{ + "environment": { + "python": "3.12.14 (main, Aug 25 2026, 14:00:49) [Clang 22.1.3 ]", + "platform": "linux" + }, + "tested_content_commit": "12a3e8bdaaea3da7a423e7fbb4d0c1a6c8c31760", + "readonly_gitfree_commands": [ + { + "optimized": false, + "script": "verify.py", + "exit": 0, + "stdout_sha256": "d65aa476de984a7d4589137e9f69479f250fbb2db2b8a7228fab310c52c57844" + }, + { + "optimized": false, + "script": "independent.py", + "exit": 0, + "stdout_sha256": "4fb9c514f4e10084c62f8cf7ff939d1a7cca6797f2f6fc1f8094d304325fd671" + }, + { + "optimized": true, + "script": "verify.py", + "exit": 0, + "stdout_sha256": "d65aa476de984a7d4589137e9f69479f250fbb2db2b8a7228fab310c52c57844" + }, + { + "optimized": true, + "script": "independent.py", + "exit": 0, + "stdout_sha256": "4fb9c514f4e10084c62f8cf7ff939d1a7cca6797f2f6fc1f8094d304325fd671" + } + ], + "readonly_files_unchanged": 18, + "actual_corruption_rejections": [ + { + "file": "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "optimized": false, + "exit": 1 + }, + { + "file": "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "optimized": true, + "exit": 1 + }, + { + "file": "research/carrier-merge-relay-premise/inputs/pr6315-PROOF.md", + "optimized": false, + "exit": 1 + }, + { + "file": "research/carrier-merge-relay-premise/inputs/pr6315-PROOF.md", + "optimized": true, + "exit": 1 + }, + { + "file": "research/carrier-merge-relay-premise/inputs/pr6315-README.md", + "optimized": false, + "exit": 1 + }, + { + "file": "research/carrier-merge-relay-premise/inputs/pr6315-README.md", + "optimized": true, + "exit": 1 + }, + { + "file": "research/carrier-merge-relay-premise/inputs/pr6315-RESULT.json", + "optimized": false, + "exit": 1 + }, + { + "file": "research/carrier-merge-relay-premise/inputs/pr6315-RESULT.json", + "optimized": true, + "exit": 1 + }, + { + "file": "research/carrier-merge-relay-premise/inputs/pr6315-Walk.lean", + "optimized": false, + "exit": 1 + }, + { + "file": "research/carrier-merge-relay-premise/inputs/pr6315-Walk.lean", + "optimized": true, + "exit": 1 + }, + { + "file": "research/carrier-merge-relay-premise/inputs/pr6315-verify.py", + "optimized": false, + "exit": 1 + }, + { + "file": "research/carrier-merge-relay-premise/inputs/pr6315-verify.py", + "optimized": true, + "exit": 1 + }, + { + "file": "research/carrier-merge-relay-premise/PREDECESSOR.json", + "optimized": false, + "exit": 1 + }, + { + "file": "research/carrier-merge-relay-premise/PREDECESSOR.json", + "optimized": true, + "exit": 1 + }, + { + "file": "research/carrier-merge-relay-premise/RESULT.json", + "optimized": false, + "exit": 1 + }, + { + "file": "research/carrier-merge-relay-premise/RESULT.json", + "optimized": true, + "exit": 1 + } + ], + "original_source_git_authentication_files": 5, + "source_history_preflight": "not run; shallow checkout; original relevant source bytes independently authenticated", + "tested_scientific_files_sha256": { + "verify.py": "24ba9bfeedd0b5543d11fc9559e88436dde90516b12b43806d106270de38296e", + "independent.py": "c0c271d2fa0e0d27560cdb62e481a288970f687be0741995077b89bec82e12b4", + "RESULT.json": "a713a1db74756cde14e4d011ec09bfdc0981c46b9afa6876494d3d8a20dae1a8", + "PREDECESSOR.json": "10fe4a63096ea0e0e5b71322061f2903ad02f117fef44fda0b17fbfa6e334faf", + "SOURCES.json": "19d50b5838ef6327e3f9edd1a24d8328d6938626432abacf5ada97c247dd0d0d", + "VERIFY.json": "476814e92789c84190a8d175e6dae7e95f3af175bec97e7021449fabe7b44637" + } +} diff --git a/research/carrier-merge-relay-premise/VALIDATION.md b/research/carrier-merge-relay-premise/VALIDATION.md new file mode 100644 index 0000000000..42674384e3 --- /dev/null +++ b/research/carrier-merge-relay-premise/VALIDATION.md @@ -0,0 +1,53 @@ +# Validation scope + +Environment: Linux, CPython 3.12.14, standard library only. + +The written result is an application-premise audit and a dimension proof. +[INDEPENDENT-REVIEW.md](INDEPENDENT-REVIEW.md) records reviewer D's separate +source reading and derivation, including the pair-dimension consequence. +`independent.py` was written without importing the primary or predecessor +executables. It corroborates all eight geometric witnesses, 383 dimension +tuples and three rejecting geometry controls. Chronological carrier +identification remains inherited in both implementations. + +## Executed checks + +- All four registered commands passed: primary and independent checks in + normal and optimized Python. Primary coverage is 247 subset countermodels, + two nonzero endpoint-chart examples, seven source-preserving controls, + 2,457 small-lattice instances and eleven rejecting controls. The independent + checker covers all eight carrier fixtures, 383 dimension tuples and three + geometry mutants. Reviewer D separately checked the nonzero endpoint chart. +- Every one of the five retained predecessor files was compared byte for byte + with `git show 3667554dab1bf08bb9ce6c267b6047fdc9978498:`; + SHA-256 and Git blob identities agreed with `PREDECESSOR.json`. +- `scripts/check_research_commit.py --package research/carrier-merge-relay-premise + --check-modes` passed. The official exporter and export-integrity checker + passed. No omitted sparse files were staged as deletions. +- From the official export, all four direct registered scientific commands + passed with no Git checkout, an empty `PATH`, source files mode 0444 and + directories mode 0555. All 18 exported files then present, including the + export inventory, retained their exact bytes and modes. This is a no-write + integrity observation; execution as the container user is not an OS security + isolation claim. +- In private copies, actual byte corruption of each of six source files, the + predecessor manifest and the exact result receipt was rejected in both + normal and optimized modes: sixteen rejecting executions. The preserved + source tree was not mutated. + +The final scientific-code validation occurred at local content commit +`12a3e8bdaaea3da7a423e7fbb4d0c1a6c8c31760`. Subsequent changes only clarify the +written fixed-eight-carrier scope and record validation; no scientific code, +input or receipt changes follow those tests. Final committed-byte/mode and +official export-integrity checks are repeated after these documentation edits. + +The reproducible registered command is in `README.md`; the direct commands are +exactly the four arrays in `VERIFY.json`. The final test receipt in +`VALIDATION.json` records output digests and the actual corrupted paths. The +validation receipt is evidence, not an additional mathematical premise. + +No hosted CI, Lean build, full selected replay or full Git ancestry check is +claimed. The checkout is deliberately shallow and sparse; relevant original +source bytes were independently authenticated. Runtime metadata uses only +base-pinned Git sources plus exact retained copies, so portable replay does +not require the pending predecessor commit in the local Git history. diff --git a/research/carrier-merge-relay-premise/VERIFY.json b/research/carrier-merge-relay-premise/VERIFY.json new file mode 100644 index 0000000000..4ce2acd8b6 --- /dev/null +++ b/research/carrier-merge-relay-premise/VERIFY.json @@ -0,0 +1,69 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper470-twin-rung-removal/WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate exact sources; all 247 actual-source frame-walk countermodels; repaired invariant; source-preserving positive controls; small-lattice corroboration; eleven meaningful failure controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same checks with optimized Python; scientific checks do not rely on assert." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/independent.py", + "--word", + "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "--facts", + "{package}/inputs/pr6315-RESULT.json" + ], + "timeout_seconds": 30, + "checks": "Independent geometry reconstruction, symbolic-dimension corroboration on383 tuples, three corrupted-geometry controls; no author/predecessor executable imports." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/independent.py", + "--word", + "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "--facts", + "{package}/inputs/pr6315-RESULT.json" + ], + "timeout_seconds": 30, + "checks": "Independent geometry reconstruction, symbolic-dimension corroboration on383 tuples, three corrupted-geometry controls; no author/predecessor executable imports." + } + ] +} diff --git a/research/carrier-merge-relay-premise/independent.py b/research/carrier-merge-relay-premise/independent.py new file mode 100644 index 0000000000..8bca1e341b --- /dev/null +++ b/research/carrier-merge-relay-premise/independent.py @@ -0,0 +1,95 @@ +#!/usr/bin/env python3 +"""Independent finite geometry check for the carrier relay-premise audit. + +Prepared for @CubeJerry with substantial OpenAI Codex assistance. Apache-2.0. +Only pinned input data is read; no predecessor/author executable is imported. +""" +import argparse +import gzip +import hashlib +import json +from pathlib import Path + +WORD_SHA = "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f" +FACTS_SHA = "6db1b3fadd64f643731879ec4fdb661e36da97e5969424e6364628b5f2e3780d" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def dot(a, b): + return (a & b).bit_count() % 2 + + +def closure(values): + result = {0} + for value in values: + result |= {entry ^ value for entry in tuple(result)} + return result + + +def check(ports, normals, lines): + need(len(ports) == len(set(ports)) == 104, "104 distinct ports") + need(len(normals) == len(lines) == 8, "eight carriers") + facts = [] + for c, (g, line) in enumerate(zip(normals, lines)): + hyperplane = {x for x in range(512) if not dot(x, line)} + receivers = {x for x in ports if not dot(x, line)} + start = {0, g} + need(len(hyperplane) == 256 and len(receivers) == 52, "hyperplane and receiver sizes") + need(start < hyperplane and {0} < hyperplane, "strict grow then shrink") + need(closure([g, *receivers]) == hyperplane, "receiver span identity") + need(all(dot(other, line) == (a != c) for a, other in enumerate(normals)), + "cross-normal pairing") + need(receivers <= hyperplane, "all receivers served") + need(len(hyperplane | {0}) != 512, "full-span hypothesis fails") + facts.append({"carrier": c, "normal_g": g, "line": line, + "receiver_count": len(receivers), "walk_dimensions": [1, 8, 0], + "paid": 7, "union_dimension": 8, "eta": 0}) + count = 0 + for z in range(1, 10): + for t in range(10): + for intersection in range(min(z, t) + 1): + union = z + t - intersection + if union not in (8, 9): + continue + for w in range(intersection + 1): + need((z - 1) + (t - w) >= 7 + union - 8, "repaired modular inequality") + count += 1 + need(count == 383, "dimension-domain coverage") + return {"carriers": facts, "dimension_tuples": count, + "two_carrier_paid": 14, "unqualified_stronger_rhs": 16, + "scope": "abstract dual-subspace walk; not a pure-carrier physical program"} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--word", type=Path, required=True) + parser.add_argument("--facts", type=Path, required=True) + args = parser.parse_args() + word_bytes, facts_bytes = args.word.read_bytes(), args.facts.read_bytes() + need(hashlib.sha256(word_bytes).hexdigest() == WORD_SHA, "word source bytes") + need(hashlib.sha256(facts_bytes).hexdigest() == FACTS_SHA, "predecessor fact bytes") + word = json.loads(gzip.decompress(word_bytes)) + facts = json.loads(facts_bytes)["carriers"] + result = check(word["ports"], facts["normals_g"], facts["lines"]) + rejected = 0 + for normals, lines in [([0] + facts["normals_g"][1:], facts["lines"]), + (facts["normals_g"], [0] + facts["lines"][1:]), + (facts["normals_g"], facts["lines"][::-1])]: + try: + check(word["ports"], normals, lines) + except ValueError: + rejected += 1 + else: + raise ValueError("mutated geometry accepted") + need(rejected == 3, "three negative controls") + result["negative_controls"] = rejected + print(json.dumps(result, sort_keys=True)) + print("PASS_INDEPENDENT_CARRIER_PREMISE") + + +if __name__ == "__main__": + main() diff --git a/research/carrier-merge-relay-premise/inputs/pr6315-PROOF.md b/research/carrier-merge-relay-premise/inputs/pr6315-PROOF.md new file mode 100644 index 0000000000..dddca6c30a --- /dev/null +++ b/research/carrier-merge-relay-premise/inputs/pr6315-PROOF.md @@ -0,0 +1,80 @@ +# Proofs: network-coded owned carriers on P104 + +Tags: **PROVED-LEAN** = `lean/NetCode/Walk.lean` (Lean 4 + Mathlib, no `sorry`, axioms `propext`, +`Classical.choice`, `Quot.sound`); **CHECKED-EXACT** = `verify.py` on the PR6030 word (exact rationals and F2). + +## 0. Model + +Frames are subspaces of F2^9. A public role only ascends (strict inclusion), an owned role only descends and pays +the dimension drop, and arithmetic happens in a common frame. This is the verifier contract replayed by `verify.py`. +Content is not tied to the frame. A public role may hold coordinates whose ports lie outside its frame, as long as +they arrived through owned descents. + +Pass to duals. A frame C corresponds to C^perp. An ascent shrinks the dual for free. An owned descent C -> C' +grows it and costs `dim C - dim C' = dim C'^perp - dim C^perp` (`descent_cost_dual`, PROVED-LEAN). +In PR6030, X_j starts on the line and Y_j ends in p_j^perp with p_j . p_j = 1 (CHECKED-EXACT). So a receiver +Y_j can use only frames C with p_j in C^perp, and X_j and Y_j never share a frame. + +An **information walk** is a sequence of dual subspaces Z_0, Z_1, ... Each node k >= 1 comes from an earlier +node par(k), either by shrinking (free) or by growing (paid). This covers stops, copies, branches and relays +through public helpers: a helper reads at one frame and ascends, and that is a shrink. + +## 1. Walk bound and Lemma S (PROVED-LEAN `union_bound`, `lemma_S`) + +The union span of the visited nodes has dimension at most `dim Z_0` plus the total paid amount. +*Proof.* A free step adds a subspace of its parent, which is already inside the union. A paid step adds Z_k ⊇ Z_par. +By the modular law, `dim(U ⊔ Z_k) = dim U + dim Z_k - dim(U ⊓ Z_k) <= dim U + dim Z_k - dim Z_par`. + +**Lemma S.** Suppose a carrier holding t.x is collected in G = span of its source ports, so Z_0 = G^perp. Suppose +it must reach every receiver j in R. Then it pays at least `dim(G^perp + span p_R) - dim G^perp`, whatever its stops, +branches and relays. This number is the binary rank of the pairing [p_j . p_i] (j in R, i in S), the repository's +COPY cost. One chain attains it. So stops do not make a single carrier cheaper. +On PR6030 both sides equal 7 for each of the 8 carriers (CHECKED-EXACT). + +## 2. Lemma A: additions and shedding along one path (PROVED-LEAN `lemma_A`, `lemma_A_rows`) + +Let a port p_i lie in C. Let a receiver read at a frame C' ⊇ C, so that p_j ∈ C'^perp. Then p_j . p_i = 0. +Hence content added at C from ports of C changes no costly pair (p_j . p_i = 1) of any receiver served higher on the +same path. It can be loaded at the top instead, so a path with additions or shedding is one term with stops +(Lemma S). + +## 3. Lemma M: merges + +Carriers c in U merge in a frame with dual W, with combination lambda. Path c has union span Z_c ⊇ W and starts on +the line , so it pays at least `dim Z_c - 1` (walk bound). The common tail has union span T ⊇ W and pays at +least `dim T - dim W`. Every receiver of c reads c-content on path c or on the tail, so its port lies in Z_c ∪ T. + +*Finite facts (CHECKED-EXACT).* +(i) + span p_{R_c} = l_c^perp, of dimension 8. +(ii) g_a . l_c = 1 for a ≠ c. +Hence + span p_{R_c} = F2^9 for a ≠ c, and Z_c ⊔ T = F2^9 (`sup_top_of_cover`). + +**General count (PROVED-LEAN `merge_count`).** +`dim Z_c + dim T >= 9 + dim W` (`path_dim`), so `pay_c + tail >= 8` for each c. Therefore +`total + (k-1) tail >= 8k`. A merge with tail <= 1 never beats the 7k of separate carriers, for any k. + +**Pairs (PROVED-LEAN `pair_merge` + CHECKED-EXACT `nocover`).** +Suppose two merged carriers pay at most 13. Combining the bounds gives `dim Z_a, dim Z_b <= 6`. +Let N be the receivers of a or b whose need (d_ja, d_jb) is not proportional to lambda. +`must_read_path` (PROVED-LEAN) shows that each such receiver must read a pure path, so N ⊆ Z_a ∪ Z_b. +The exhaustive check is over all 28 pairs, both ratios, and all 11,811 six-dimensional subspaces containing +(WLOG dim Z_a = 6). It finds no cover with the remainder in a subspace of dimension <= 6. So every pair merge costs +at least 14 = 7 + 7. + +The decoder rows are unique: on the costly pairs of every port, the 8 carrier rows have rank 8 (CHECKED-EXACT). +So the needs d_j are forced, and d_jc = ±2 exactly when j ∈ R_c. + +## 4. Scope + +Covered: the unique 8-carrier code of the P104 local word (PR6030 contents, unique up to sign by PR6166). +Covered mechanisms: stops, copies, branches, public relays, additions and shedding along a path, any single merge +with a tail of length <= 1, and every single merge of two carriers. + +Not covered: +- merges of three or more carriers with a tail of length >= 2; +- multi-stage merge trees; +- codes with 9 or more carriers, which is the open masked floor C(P104) >= 56 beyond rank 8; +- decoders that read X directly (P-ATOM), and different words or boundaries. + +The cut profile of PR6030 is tight: 8 crossings on each level 2..8 of the seven dimension cuts of +`p104-owned-coding-boundaries` (CHECKED-EXACT). diff --git a/research/carrier-merge-relay-premise/inputs/pr6315-README.md b/research/carrier-merge-relay-premise/inputs/pr6315-README.md new file mode 100644 index 0000000000..487a2efd97 --- /dev/null +++ b/research/carrier-merge-relay-premise/inputs/pr6315-README.md @@ -0,0 +1,62 @@ +# Network-coded owned carriers on P104: stops, shedding and pair merges do not go below 56 + +`research/fragmentation-ceiling/PROOF.md` §6.7 lists "network-coded carriers with stops and shedding" as one door +outside the A30-CUT scope. This package tests that door on the selected PR6030 local word and its 8-carrier code, +which PR6166 shows is unique up to sign. + +**Scoped negative result. No new word or kappa is claimed.** + +## Result + +| Mechanism | Result | Evidence | +|---|---|---| +| stops, copies, branches, relays through public helpers | a carrier pays at least its COPY cost (the F2 pairing rank) | Lemma S, PROVED-LEAN | +| additions and shedding along one path | equivalent to loading at the top | Lemma A, PROVED-LEAN | +| any merge of k carriers with a tail of length <= 1 | costs more than 7k | `merge_count`, PROVED-LEAN + finite facts | +| any merge of two carriers | costs at least 14 = 7 + 7 | `pair_merge`, PROVED-LEAN + exhaustive check | + +The proofs use a dual picture. A frame C is replaced by C^perp. Public ascents shrink the dual for free, and owned +descents grow it at their price. The union span of every visited dual grows by at most the paid amount. With this +one inequality, stops, copies, branches and relays reduce to the COPY cost. For merges, each carrier must also +reach the other carrier's normal g_a. Since g_a . l_c = 1 for a ≠ c, each content tree then spans all of F2^9. + +The PR6030 word already uses a coded owned network. It has 31 owned lifetimes, 14 owned-to-owned additions and +owned reads at frame dimensions 0-8. It is tight against the seven dimension cuts of +[p104-owned-coding-boundaries](../p104-owned-coding-boundaries/JOINT-BOUNDARY.md), with exactly 8 crossings on +every level 2..8 (owned paid 56). + +## Reproduce + +```sh +python3 -B research/p104-network-coded-carriers/verify.py +``` + +The check uses the standard library only and takes about 17 s. Expected marker: `PASS_P104_NETWORK_CODED_CARRIERS`. +It replays the PR6030 word exactly and checks the Y/X frame facts and the 8 carriers. It extracts the delivery lines +(removed E8 root lines), the normals g_c and the receivers R_c. It checks the Lemma S equality (dual walk cost = +pairing rank = 7), the unique masked decoder (d_jc = ±2) and the `merge_count` spanning facts. It runs the +exhaustive pair `nocover` check (28 pairs × 2 ratios × 11,811 subspaces) and compares the result with +[RESULT.json](RESULT.json). + +Lean (optional, not run by `verify.py`): `cd lean && lake exe cache get && lake build && lake env lean Audit.lean`. +Every theorem prints only `propext`, `Classical.choice` and `Quot.sound`. The Mathlib pin is the one used by +`p104-carrier-code-uniqueness`. + +## Relation to existing work + +- `fragmentation-ceiling` §6.4 (single-commodity lemma) and §6.7 (the door). Lemma S is the P104 form of the + single-commodity statement, with arbitrary stops and public relays. +- `p104-owned-coding-boundaries`: its seven cuts close arbitrary sharing for a fixed public boundary with + dimension-1 deliveries. This package removes the boundary premise for stops, shedding and pair merges. +- Matarener's open PR6267 (owned-lineage factorization) asks whether its floor extends to merges. Pair merges are + answered here. +- `p104-signed-mixed-carrier-bank` builds mixed carriers in a relaxed frame model. Here the actual frame rules are + used, and pair mixing does not pay. + +## Open next questions + +- Merges of 3 or more carriers with tails of length >= 2, and multi-stage merge trees. +- Codes with 9 or more carriers (masked floor beyond rank 8). +- Decoders reading X (P-ATOM). + +Prepared for Matarener with Claude (Anthropic), via Claude Code. Apache-2.0. diff --git a/research/carrier-merge-relay-premise/inputs/pr6315-RESULT.json b/research/carrier-merge-relay-premise/inputs/pr6315-RESULT.json new file mode 100644 index 0000000000..03840be5de --- /dev/null +++ b/research/carrier-merge-relay-premise/inputs/pr6315-RESULT.json @@ -0,0 +1,124 @@ +{ + "carriers": { + "g_dot_l_is_offdiagonal_one": true, + "lines": [ + 7, + 25, + 52, + 67, + 82, + 137, + 448, + 491 + ], + "normals_g": [ + 104, + 162, + 266, + 97, + 289, + 127, + 42, + 76 + ], + "receivers": [ + 52, + 52, + 52, + 52, + 52, + 52, + 52, + 52 + ], + "support_sizes": [ + 52, + 52, + 52, + 52, + 52, + 52, + 52, + 52 + ] + }, + "decoder": { + "carriers_per_port": { + "2": 12, + "3": 24, + "4": 32, + "5": 24, + "6": 12 + }, + "support_equals_receivers": true, + "unique_rows": 104, + "values": [ + -2, + 2 + ] + }, + "frames": { + "X_start_is_p_line": 104, + "Y_final_is_p_perp": 104, + "p_dot_p_is_1": 104 + }, + "lemma_S": { + "dual_walk_cost": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "pairing_rank": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ] + }, + "merge_count_htop": { + "pairs": 56 + }, + "pair_nocover": { + "feasible_covers": 0, + "max_N": 75, + "min_N": 49, + "pairs": 28, + "ratios": 2, + "six_dim_subspaces_tested_each": 11811 + }, + "word": { + "cut_crossings_levels_1_to_9": [ + 0, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 0 + ], + "owned_lifetimes": 31, + "owned_paid": 56, + "owned_reads_by_frame_dim": { + "0": 4, + "1": 25, + "2": 1, + "3": 10, + "4": 14, + "5": 17, + "7": 6, + "8": 8 + }, + "owned_to_owned_adds": 14 + } +} diff --git a/research/carrier-merge-relay-premise/inputs/pr6315-Walk.lean b/research/carrier-merge-relay-premise/inputs/pr6315-Walk.lean new file mode 100644 index 0000000000..3616ecd1ae --- /dev/null +++ b/research/carrier-merge-relay-premise/inputs/pr6315-Walk.lean @@ -0,0 +1,220 @@ +import Mathlib + +/-! +# Network-coded carriers on P104: the dual-span walk bound (Lemmas S, A, M of PROOF.md) + +Frames are subspaces `C` of `F₂⁹`. We work with their orthogonal complements (`C^⊥` for the dot product). +A public ascent `C ≤ C'` shrinks the dual (free), an owned descent `C' ≤ C` grows it and costs +`dim C - dim C' = dim C'^⊥ - dim C^⊥` (`descent_cost_dual`). A receiver whose final frame is `p^⊥` can read +only in a frame `C` with `p ∈ C^⊥`. + +An information walk is a sequence of dual subspaces `Z 0, Z 1, …`; node `k ≥ 1` is produced from an earlier node +`par k` (a copy, a stop, a relay through public helpers or a branch) either by shrinking (free) or by growing (paid). +The union span of all visited nodes grows by at most the paid amount (`union_bound`). +-/ + +namespace NetCode + +open Module + +abbrev V := Fin 9 → ZMod 2 +abbrev Sub := Submodule (ZMod 2) V + +/-- The dot-product form on `F₂⁹`. -/ +def dotForm : LinearMap.BilinForm (ZMod 2) V := Matrix.toBilin' 1 + +theorem dotForm_apply (x y : V) : dotForm x y = x ⬝ᵥ y := by + simp [dotForm, Matrix.toBilin'_apply', dotProduct] + +/-- The dual of a frame. -/ +def orth (C : Sub) : Sub := dotForm.orthogonal C + +theorem mem_orth {C : Sub} {p : V} : p ∈ orth C ↔ ∀ x ∈ C, x ⬝ᵥ p = 0 := by + simp [orth, LinearMap.BilinForm.mem_orthogonal_iff, dotForm_apply] + +/-- `dim C + dim C^⊥ = 9`. -/ +theorem finrank_add_orth (C : Sub) : finrank (ZMod 2) C + finrank (ZMod 2) (orth C) = 9 := by + have h := dotForm.finrank_add_finrank_orthogonal' C + have hker : LinearMap.ker dotForm = ⊥ := by + rw [eq_bot_iff] + intro x hx + rw [Submodule.mem_bot] + funext i + have := congrArg (fun f => f (Pi.single i 1)) (LinearMap.mem_ker.mp hx) + simp only [dotForm_apply, LinearMap.zero_apply] at this + simpa [dotProduct_single] using this + rw [show (dotForm.ker : Submodule (ZMod 2) V) = LinearMap.ker dotForm from rfl, hker, inf_bot_eq, + finrank_bot, add_zero, Module.finrank_fin_fun] at h + exact h + +theorem orth_anti {C C' : Sub} (h : C' ≤ C) : orth C ≤ orth C' := by + intro p hp + rw [mem_orth] at hp ⊢ + exact fun x hx => hp x (h hx) + +/-- An owned descent `C → C'` (`C' ≤ C`) costs exactly the growth of the dual. -/ +theorem descent_cost_dual {C C' : Sub} (_h : C' ≤ C) : + finrank (ZMod 2) C - finrank (ZMod 2) C' = + finrank (ZMod 2) (orth C') - finrank (ZMod 2) (orth C) := by + have := finrank_add_orth C + have := finrank_add_orth C' + omega + +/-! ## The walk bound (Lemma S) -/ + +attribute [local instance] Classical.propDecidable + +/-- Paid amount of step `k`: zero for a shrinking (free) step, the dimension growth otherwise. -/ +noncomputable def cost (Z : ℕ → Sub) (par : ℕ → ℕ) (k : ℕ) : ℕ := + if Z k ≤ Z (par k) then 0 else finrank (ZMod 2) (Z k) - finrank (ZMod 2) (Z (par k)) + +/-- Union span of the first `n + 1` nodes. -/ +def U (Z : ℕ → Sub) : ℕ → Sub + | 0 => Z 0 + | n + 1 => U Z n ⊔ Z (n + 1) + +theorem le_U (Z : ℕ → Sub) : ∀ {i n : ℕ}, i ≤ n → Z i ≤ U Z n + | i, 0, h => by + rw [Nat.le_zero.mp h]; exact le_rfl + | i, n + 1, h => by + rcases Nat.lt_or_eq_of_le h with h | h + · exact le_trans (le_U Z (Nat.lt_succ_iff.mp h)) le_sup_left + · rw [h]; exact le_sup_right + +/-- **Walk bound.** If every step shrinks or grows its (earlier) parent, the union span of all visited dual subspaces +has dimension at most `dim Z 0` plus the total paid amount. -/ +theorem union_bound (Z : ℕ → Sub) (par : ℕ → ℕ) (hpar : ∀ k, 0 < k → par k < k) + (hstep : ∀ k, 0 < k → Z k ≤ Z (par k) ∨ Z (par k) ≤ Z k) : + ∀ n, finrank (ZMod 2) (U Z n) ≤ + finrank (ZMod 2) (Z 0) + ∑ k ∈ Finset.Icc 1 n, cost Z par k + | 0 => Nat.le_add_right _ _ + | n + 1 => by + have ih := union_bound Z par hpar hstep n + have hp : par (n + 1) ≤ n := Nat.lt_succ_iff.mp (hpar (n + 1) (Nat.succ_pos n)) + have hparU : Z (par (n + 1)) ≤ U Z n := le_U Z hp + rw [Finset.sum_Icc_succ_top (by omega : 1 ≤ n + 1)] + show finrank (ZMod 2) ((U Z n ⊔ Z (n + 1) : Sub)) ≤ _ + by_cases hfree : Z (n + 1) ≤ Z (par (n + 1)) + · have hc : cost Z par (n + 1) = 0 := by simp [cost, hfree] + have : (U Z n ⊔ Z (n + 1) : Sub) = U Z n := sup_eq_left.mpr (le_trans hfree hparU) + rw [this, hc] + omega + · have hgrow : Z (par (n + 1)) ≤ Z (n + 1) := (hstep (n + 1) (Nat.succ_pos n)).resolve_left hfree + have hc : cost Z par (n + 1) = + finrank (ZMod 2) (Z (n + 1)) - finrank (ZMod 2) (Z (par (n + 1))) := by simp [cost, hfree] + have hmod := Submodule.finrank_sup_add_finrank_inf_eq (U Z n) (Z (n + 1)) + have hinf : finrank (ZMod 2) (Z (par (n + 1))) ≤ finrank (ZMod 2) ((U Z n ⊓ Z (n + 1) : Sub)) := + Submodule.finrank_mono (le_inf hparU hgrow) + have hmono := Submodule.finrank_mono hgrow + rw [hc] + omega + +/-- **Lemma S.** A walk starting at `Z 0` that visits, for every receiver vector `p ∈ R`, some node containing `p` +pays at least `dim (Z 0 ⊔ span R) - dim Z 0`. With `Z 0 = (span S)^⊥` this is the binary rank of the pairing between +the receivers and the sources (`verify.py` checks the equality), so stops, branches, copies and relays through public +helpers never make one carrier cheaper than its COPY cost. -/ +theorem lemma_S (Z : ℕ → Sub) (par : ℕ → ℕ) (hpar : ∀ k, 0 < k → par k < k) + (hstep : ∀ k, 0 < k → Z k ≤ Z (par k) ∨ Z (par k) ≤ Z k) (n : ℕ) (R : Set V) + (hR : ∀ p ∈ R, ∃ i ≤ n, p ∈ Z i) : + finrank (ZMod 2) ((Z 0 ⊔ Submodule.span (ZMod 2) R : Sub)) ≤ + finrank (ZMod 2) (Z 0) + ∑ k ∈ Finset.Icc 1 n, cost Z par k := by + have hle : Z 0 ⊔ Submodule.span (ZMod 2) R ≤ U Z n := by + refine sup_le (le_U Z (Nat.zero_le n)) (Submodule.span_le.mpr ?_) + intro p hp + obtain ⟨i, hi, hpi⟩ := hR p hp + exact le_U Z hi hpi + exact le_trans (Submodule.finrank_mono hle) (union_bound Z par hpar hstep n) + +/-! ## Lemma A: free additions along one path touch only free pairs -/ + +/-- If a port `pi` lies in a frame `C` and a receiver `pj` reads in a frame `C' ⊇ C` (so `pj ∈ C'^⊥`), the pair is +free: `pj · pi = 0`. Hence content added at `C` from ports of `C` changes no costly pair of any receiver served higher +on the same path, and could have been loaded at the top. -/ +theorem lemma_A {C C' : Sub} (h : C ≤ C') {pi pj : V} (hi : pi ∈ C) (hj : pj ∈ orth C') : + pj ⬝ᵥ pi = 0 := by + rw [mem_orth] at hj + rw [dotProduct_comm] + exact hj pi (h hi) + +/-- Content form of Lemma A: an addition `f` supported on ports of `C` vanishes on every costly pair +(`port j · port i = 1`) of a receiver `j` reading in a frame containing `C`. -/ +theorem lemma_A_rows {L K : Type*} [Zero K] (port : L → V) (f : L → K) {C C' : Sub} (h : C ≤ C') + (hf : ∀ i, f i ≠ 0 → port i ∈ C) (j : L) (hj : port j ∈ orth C') (i : L) + (hcost : port j ⬝ᵥ port i = 1) : f i = 0 := by + by_contra hne + have := lemma_A h (hf i hne) hj + rw [this] at hcost + exact zero_ne_one hcost + +/-! ## Lemma M: merging carriers -/ + +/-- If the receivers `S` of a carrier lie in `Z ∪ T`, `G ≤ Z` and `G ⊔ span S = ⊤`, then `Z ⊔ T = ⊤`. -/ +theorem sup_top_of_cover {Z T G : Sub} {S : Set V} (hS : ∀ p ∈ S, p ∈ Z ∨ p ∈ T) (hG : G ≤ Z) + (htop : G ⊔ Submodule.span (ZMod 2) S = ⊤) : Z ⊔ T = ⊤ := by + rw [eq_top_iff, ← htop] + refine sup_le (le_trans hG le_sup_left) (Submodule.span_le.mpr ?_) + intro p hp + rcases hS p hp with h | h + · exact (le_sup_left : Z ≤ Z ⊔ T) h + · exact (le_sup_right : T ≤ Z ⊔ T) h + +/-- Dimension count behind Lemma M: if `Z ⊔ T = ⊤` and `W ≤ Z ⊓ T` then `dim Z ≥ 9 - (dim T - dim W)`. -/ +theorem path_dim {Z T W : Sub} (htop : Z ⊔ T = ⊤) (hW : W ≤ Z ⊓ T) : + 9 + finrank (ZMod 2) W ≤ finrank (ZMod 2) Z + finrank (ZMod 2) T := by + have hmod := Submodule.finrank_sup_add_finrank_inf_eq Z T + rw [htop, finrank_top, Module.finrank_fin_fun] at hmod + have := Submodule.finrank_mono hW + omega + +/-- **Lemma M, general count.** Carriers `c ∈ Fin k` merge in a frame with dual `W`; path `c` has union span `Z c` +(from a line, so it pays at least `dim Z c - 1`), the common tail has union span `T ⊇ W` and pays at least +`dim T - dim W`. If every carrier's content tree spans everything (`Z c ⊔ T = ⊤`), then +`total + (k - 1)·tail ≥ 8 k`. Short tails therefore never beat `7 k`. -/ +theorem merge_count (k : ℕ) (Z : Fin k → Sub) (T W : Sub) (hW : ∀ c, W ≤ Z c ⊓ T) + (htop : ∀ c, Z c ⊔ T = ⊤) (pay : Fin k → ℕ) (hpay : ∀ c, finrank (ZMod 2) (Z c) ≤ pay c + 1) + (tail : ℕ) (htail : finrank (ZMod 2) T ≤ tail + finrank (ZMod 2) W) : + 8 * k ≤ (∑ c, pay c) + tail + (k - 1) * tail := by + have h : ∀ c, 8 ≤ pay c + tail := by + intro c + have := path_dim (htop c) (hW c) + have := hpay c + omega + have hsum : ∑ _c : Fin k, 8 ≤ ∑ c, (pay c + tail) := Finset.sum_le_sum fun c _ => h c + simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, smul_eq_mul, + Finset.sum_add_distrib] at hsum + rcases k with _ | k + · simp + · simp only [Nat.add_sub_cancel] + nlinarith + +/-- A receiver whose need is not proportional to the merged ratio must read some pure path. -/ +theorem must_read_path {K : Type*} [Field K] {k : ℕ} (lam d : Fin k → K) (μ : K) (ν : Fin k → K) + (hd : d = μ • lam + ν) (hnot : ∀ μ' : K, d ≠ μ' • lam) : ∃ c, ν c ≠ 0 := by + by_contra h + push Not at h + apply hnot μ + rw [hd] + funext c + simp [h c] + +/-- **Lemma M for pairs.** Two carriers whose paths start on lines merge; the network pays +`pay a + pay b + tail` with the bounds of `merge_count`. A network cheaper than 14 forces both path unions to have +dimension at most 6. If no two subspaces containing `G`, each of dimension at most 6, cover the non-proportional +receivers `N` (the finite fact checked by `verify.py`), the merged network costs at least 14, the price of the two +separate carriers. -/ +theorem pair_merge (Za Zb T W G : Sub) (hG : G ≤ W) (hWa : W ≤ Za ⊓ T) (hWb : W ≤ Zb ⊓ T) + (hta : Za ⊔ T = ⊤) (htb : Zb ⊔ T = ⊤) (N : Set V) (hN : ∀ p ∈ N, p ∈ Za ∨ p ∈ Zb) + (nocover : ∀ A B : Sub, G ≤ A → G ≤ B → + finrank (ZMod 2) A ≤ 6 → finrank (ZMod 2) B ≤ 6 → ¬ ∀ p ∈ N, p ∈ A ∨ p ∈ B) + (pa pb tail : ℕ) (hpa : finrank (ZMod 2) Za ≤ pa + 1) (hpb : finrank (ZMod 2) Zb ≤ pb + 1) + (htail : finrank (ZMod 2) T ≤ tail + finrank (ZMod 2) W) : + 14 ≤ pa + pb + tail := by + have h1 := path_dim hta hWa + have h2 := path_dim htb hWb + by_contra hlt + have ha6 : finrank (ZMod 2) Za ≤ 6 := by omega + have hb6 : finrank (ZMod 2) Zb ≤ 6 := by omega + exact nocover Za Zb (le_trans hG (le_trans hWa inf_le_left)) (le_trans hG (le_trans hWb inf_le_left)) + ha6 hb6 hN + +end NetCode diff --git a/research/carrier-merge-relay-premise/inputs/pr6315-verify.py b/research/carrier-merge-relay-premise/inputs/pr6315-verify.py new file mode 100644 index 0000000000..cf52884d41 --- /dev/null +++ b/research/carrier-merge-relay-premise/inputs/pr6315-verify.py @@ -0,0 +1,335 @@ +#!/usr/bin/env python3 +"""Network-coded owned carriers on the PR6030 P104 word: finite facts for the Lean lemmas. Apache-2.0. + +Prepared for Matarener with Claude (Anthropic), via Claude Code. Python 3.12, standard library only. + +Checks: + 1. exact replay of the PR6030 word: frame rules (public ascents, owned strict descents, common-chart arithmetic), + endpoint rows, owned lifetimes, owned-to-owned transfers, read dimensions, and the crossing profile of the seven + dimension cuts of p104-owned-coding-boundaries (8 crossings on every level 2..8, owned paid 56); + 2. Y_j final frame = p_j^perp with p_j . p_j = 1, so X_j and Y_j never share a frame; + 3. the eight dimension-1 delivery lines l_c are the eight removed E8 root lines that carry deliveries; carrier + contents s_c (52 live coordinates, +-1/4) are collected in G_c = span of their ports (dimension 8, normal g_c); + receivers R_c = {j : p_j . l_c = 0} (52 each); + span p_{R_c} = l_c^perp; g_a . l_c = [a != c]; + 4. Lemma S equality: dual walk cost dim( + span p_{R_c}) - 1 = binary rank of the pairing [p_j . p_i] = 7; + 5. the masked decoder: on the costly pairs of every port j (p_i . p_j = 1, i = j included) the eight carrier + rows have rank 8, so d_j is unique; d_jc = +-2 exactly on the carriers with j in R_c; + 6. htop facts of Lean `merge_count`: + span p_{R_c} = F2^9 for every a != c; + 7. Lean `pair_merge` finite fact `nocover`: for every pair {a, b} and ratio +-1, no two subspaces containing + , each of dimension <= 6, cover the non-proportional receivers N; + 8. the computed record equals RESULT.json. +""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +from pathlib import Path +import gzip, itertools, json, sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORD = 'research/p104-helper470-twin-rung-removal/WORD.json.gz' + + +def need(ok, why): + if not ok: + raise SystemExit('FAIL ' + why) + + +def log(kind, **data): + print(kind, json.dumps(data, sort_keys=True, default=str)[:300], flush=True) + + +def dot(a, b): + return bin(a & b).count('1') & 1 + + +def rank(vs): + b = [] + for v in vs: + for x in b: + v = min(v, v ^ x) + if v: + b.append(v) + return len(b) + + +def span(basis): + s = {0} + for v in basis: + s |= {x ^ v for x in s} + return frozenset(s) + + +def normals(vs): + return [u for u in range(1, 512) if all(dot(u, v) == 0 for v in vs)] + + +def qrank(rows): + m = [list(r) for r in rows] + r = 0 + for c in range(len(m[0]) if m else 0): + p = next((i for i in range(r, len(m)) if m[i][c] != 0), None) + if p is None: + continue + m[r], m[p] = m[p], m[r] + for i in range(len(m)): + if i != r and m[i][c] != 0: + f = m[i][c] / m[r][c] + m[i] = [x - f * y for x, y in zip(m[i], m[r])] + r += 1 + return r + + +def qsolve(A, b): + """Unique exact solution of A x = b (A has full column rank), else None.""" + n = len(A[0]) + m = [list(r) + [bb] for r, bb in zip(A, b)] + r = 0 + piv = [] + for c in range(n): + p = next((i for i in range(r, len(m)) if m[i][c] != 0), None) + if p is None: + return None + m[r], m[p] = m[p], m[r] + inv = 1 / m[r][c] + m[r] = [x * inv for x in m[r]] + for i in range(len(m)): + if i != r and m[i][c] != 0: + f = m[i][c] + m[i] = [x - f * y for x, y in zip(m[i], m[r])] + piv.append(c) + r += 1 + if any(m[i][n] != 0 for i in range(r, len(m))): + return None + return [m[i][n] for i in range(n)] + + +def replay(w): + S = [span(b) for b in w['frames']] + dims = [len(b) for b in w['frames']] + n, m = w['public'], w['owned_fields'] + live = list(w['live']) + lset = set(live) + cur = list(w['initial']) + [None] * m + rows = [{r: Q(1)} for r in range(n + m)] + owned = set() + lifetimes, life = [], {} + deliveries = {} + reads = Counter() + o2o = 0 + for e in w['program']: + op, r = e[0], e[1] + if op == 'MOVE': + a, b, private = e[2], e[3], e[4] + need(cur[r] == a and (r in owned) == private, 'move source') + need(S[b] < S[a] if private else S[a] < S[b], 'strict nesting') + cur[r] = b + if private: + life[r]['path'].append(dims[b]) + continue + if op == 'INIT': + need(r >= n and r not in owned, 'init') + owned.add(r) + cur[r] = e[2] + rows[r] = {} + life[r] = {'path': [dims[e[2]]]} + lifetimes.append(life[r]) + continue + if op == 'CLEAR': + need(r in owned and cur[r] == e[2], 'clear') + owned.discard(r) + cur[r] = None + rows[r] = {} + continue + q, f = Q(e[-2]), e[-1] + need(q != 0 and cur[r] == f, 'destination chart') + if op == 'SCALE': + rows[r] = {k: q * v for k, v in rows[r].items()} + continue + s = e[2] + need(cur[s] == f, 'common chart') + if s >= n and r >= n: + o2o += 1 + if s >= n and r < n: + reads[dims[f]] += 1 + if dims[f] == 1: + line = min(v for v in S[f] if v) + vec = {k: v for k, v in rows[s].items() if k in lset} + deliveries.setdefault(line, []).append(vec) + if op == 'COPY': + need(r in owned and not rows[r], 'copy') + rows[r] = {k: q * v for k, v in rows[s].items()} + else: + need(op == 'ADD', 'opcode') + t = dict(rows[r]) + for k, v in rows[s].items(): + x = t.get(k, 0) + q * v + if x: + t[k] = x + else: + t.pop(k, None) + rows[r] = t + need(not owned and cur[:n] == w['final'], 'exits') + for r in range(n): + exp = {r: Q(1)} + if r - 112 in lset: + exp[r - 112] = Q(1) + need(rows[r] == exp, 'endpoint row %d' % r) + return lifetimes, deliveries, reads, o2o + + +def subspaces(nn, d): + out = [] + for piv in itertools.combinations(range(nn), d): + free = [(r, c) for r in range(d) for c in range(piv[r] + 1, nn) if c not in piv] + for bits in range(1 << len(free)): + rows = [1 << piv[r] for r in range(d)] + for t, (r, c) in enumerate(free): + if bits >> t & 1: + rows[r] |= 1 << c + out.append(span(rows)) + return out + + +def main(): + src = json.loads((HERE / 'SOURCES.json').read_text()) + for row in src['files']: + if row['usage'] == 'input': + need(sha256((ROOT / row['path']).read_bytes()).hexdigest() == row['sha256'], 'source pin ' + row['path']) + w = json.loads(gzip.decompress((ROOT / WORD).read_bytes())) + P = w['ports'] + live = list(w['live']) + lidx = {r: k for k, r in enumerate(live)} + res = {} + + # 1. replay and cut profile + lifetimes, deliveries, reads, o2o = replay(w) + cross = Counter() + paid = 0 + for L in lifetimes: + for a, b in zip(L['path'], L['path'][1:]): + paid += a - b + for k in range(b + 1, a + 1): + cross[k] += 1 + res['word'] = {'owned_lifetimes': len(lifetimes), 'owned_to_owned_adds': o2o, 'owned_paid': paid, + 'cut_crossings_levels_1_to_9': [cross[k] for k in range(1, 10)], + 'owned_reads_by_frame_dim': {str(k): v for k, v in sorted(reads.items())}} + need(paid == 56 and all(cross[k] == 8 for k in range(2, 9)), 'cut profile') + log('REPLAY', **res['word']) + + # 2. Y_j final frame + S = [span(b) for b in w['frames']] + yn = [] + for k, r in enumerate(live): + nv = normals([v for v in S[w['final'][r + 112]] if v]) + need(len(nv) == 1 and nv[0] == P[k] and dot(P[k], P[k]) == 1, 'Y final = p^perp') + need(min(v for v in S[w['initial'][r]] if v) == P[k] and len(S[w['initial'][r]]) == 2, 'X start =

') + yn.append(nv[0]) + res['frames'] = {'Y_final_is_p_perp': 104, 'X_start_is_p_line': 104, 'p_dot_p_is_1': 104} + + # 3. carriers + lines = sorted(deliveries) + need(len(lines) == 8, 'eight delivery lines') + carriers = [] + for l in lines: + vecs = {json.dumps(sorted((lidx[k], str(v)) for k, v in d.items())) for d in deliveries[l]} + need(len(vecs) == 1, 'one content per line') + d0 = deliveries[l][0] + carriers.append({lidx[k]: v for k, v in d0.items()}) + weight3or7 = [q for q in range(512) if bin(q).count('1') in (3, 7)] + removed = [q for q in weight3or7 if q not in P] + need(len(removed) == 16 and all(l in removed for l in lines), 'lines are removed root lines') + g, R = [], [] + for c, l in enumerate(lines): + s = carriers[c] + need(len(s) == 52 and set(abs(v) for v in s.values()) == {Q(1, 4)}, 'carrier content') + ports = [P[i] for i in s] + need(rank(ports) == 8, 'G_c dim 8') + nv = normals(ports) + need(len(nv) == 1, 'normal') + g.append(nv[0]) + R.append([j for j in range(104) if dot(P[j], l) == 0]) + need(len(R[c]) == 52, '52 receivers') + need(rank([g[c]] + [P[j] for j in R[c]]) == 8 and all(dot(v, l) == 0 for v in [g[c]] + [P[j] for j in R[c]]), + ' + p_R = l^perp') + gl = [[dot(g[a], lines[c]) for a in range(8)] for c in range(8)] + need(all(gl[c][a] == (a != c) for a in range(8) for c in range(8)), 'g_a . l_c = [a != c]') + res['carriers'] = {'lines': lines, 'normals_g': g, 'support_sizes': [len(s) for s in carriers], + 'receivers': [len(r) for r in R], 'g_dot_l_is_offdiagonal_one': True} + log('CARRIERS', lines=lines, g=g) + + # 4. Lemma S equality: dual walk cost = F2 pairing rank = 7 + walk = [rank([g[c]] + [P[j] for j in R[c]]) - 1 for c in range(8)] + pair = [rank([sum(dot(P[j], P[i]) << t for t, i in enumerate(sorted(carriers[c]))) for j in R[c]]) + for c in range(8)] + need(walk == [7] * 8 and pair == [7] * 8, 'Lemma S equality') + res['lemma_S'] = {'dual_walk_cost': walk, 'pairing_rank': pair} + + # 5. masked decoder + D = [] + for j in range(104): + costly = [i for i in range(104) if dot(P[i], P[j]) == 1] + A = [[carriers[c].get(i, Q(0)) for c in range(8)] for i in costly] + need(qrank(A) == 8, 'unique decoder row') + x = qsolve(A, [Q(1) if i == j else Q(0) for i in costly]) + need(x is not None, 'decoder solvable') + need(all((x[c] != 0) == (j in R[c]) for c in range(8)) and all(v in (0, 2, -2) for v in x), 'decoder support') + D.append(x) + res['decoder'] = {'unique_rows': 104, 'values': [-2, 2], 'support_equals_receivers': True, + 'carriers_per_port': dict(sorted(Counter(sum(1 for v in d if v) for d in D).items()))} + + # 6. htop facts + for a in range(8): + for c in range(8): + if a != c: + need(rank([g[a], g[c]] + [P[j] for j in R[c]]) == 9, 'htop') + res['merge_count_htop'] = {'pairs': 56} + + # 7. pair nocover + S4 = subspaces(7, 4) + need(len(S4) == 11811, 'subspace count') + rows = [] + for a, b in itertools.combinations(range(8), 2): + G = [g[a], g[b]] + Gb = [] + for v in sorted(G, reverse=True): + for x in Gb: + v = min(v, v ^ x) + Gb.append(v) + Gb.sort(reverse=True) + + def red(v): + for x in Gb: + v = min(v, v ^ x) + return v + comp = [] + for e in range(9): + if rank([red(c) for c in comp] + [red(1 << e)]) > len(comp): + comp.append(1 << e) + coord = {} + for mm in range(128): + x = 0 + for i in range(7): + if mm >> i & 1: + x ^= red(comp[i]) + coord[x] = mm + need(len(coord) == 128, 'quotient') + for lam in (1, -1): + N = [j for j in range(104) if (D[j][a] or D[j][b]) and not (D[j][a] and D[j][b] and D[j][b] == lam * D[j][a])] + Nq = [coord[red(P[j])] for j in N] + feas = sum(1 for Sx in S4 if rank([x for x in Nq if x not in Sx]) <= 4) + need(feas == 0, 'pair cover %s' % ((a, b, lam),)) + rows.append(len(N)) + res['pair_nocover'] = {'pairs': 28, 'ratios': 2, 'six_dim_subspaces_tested_each': 11811, + 'min_N': min(rows), 'max_N': max(rows), 'feasible_covers': 0} + log('PAIRS', **res['pair_nocover']) + + out = json.dumps(res, indent=1, sort_keys=True) + '\n' + if '--write' in sys.argv: + (HERE / 'RESULT.json').write_text(out) + need((HERE / 'RESULT.json').read_text() == out, 'RESULT.json') + print('PASS_P104_NETWORK_CODED_CARRIERS') + + +if __name__ == '__main__': + main() diff --git a/research/carrier-merge-relay-premise/verify.py b/research/carrier-merge-relay-premise/verify.py new file mode 100644 index 0000000000..487d3484d7 --- /dev/null +++ b/research/carrier-merge-relay-premise/verify.py @@ -0,0 +1,273 @@ +#!/usr/bin/env python3 +"""Independent exact frame-walk audit, not a restored circuit or decoder. + +Prepared for @CubeJerry with substantial OpenAI Codex assistance. Apache-2.0. +Geometry: DreamingOfClouds #6030. Audited theorem: Matarener #6315. +No predecessor executable is imported or executed. +""" +import argparse +import gzip +import hashlib +import itertools +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORD = "research/p104-helper470-twin-rung-removal/WORD.json.gz" +PREDECESSOR_SHA256 = "10fe4a63096ea0e0e5b71322061f2903ad02f117fef44fda0b17fbfa6e334faf" + + +class Rejected(ValueError): + pass + + +def need(condition, message): + if not condition: + raise Rejected(message) + + +def dot(x, y): + return (x & y).bit_count() % 2 + + +def space(vectors): + values = {0} + for vector in vectors: + values.update(x ^ vector for x in tuple(values)) + return frozenset(values) + + +def dim(s): + size = len(s) + need(size > 0 and size & (size - 1) == 0, "non-subspace cardinality") + return size.bit_length() - 1 + + +def join(*spaces): + return space(itertools.chain.from_iterable(spaces)) + + +def walk(nodes, root, claimed=None): + need(bool(nodes) and nodes[0] == root, "wrong source root") + paid = 0 + for a, b in zip(nodes, nodes[1:]): + if b <= a: + continue + need(a <= b, "nonnested step") + paid += dim(b) - dim(a) + if claimed is not None: + need(type(claimed) is int and paid == claimed, "wrong paid amount") + union = join(*nodes) + need(dim(union) <= dim(root) + paid, "walk union bound") + return paid, union + + +def check_model(carriers, selected, hG=False, htop=False, base=7, grow=True, merge_vector=0): + zero, full = frozenset({0}), frozenset(range(512)) + W = space([merge_vector]) + G = space(carriers[c]["g"] for c in selected) + paths, costs = [], [] + for c in selected: + item = carriers[c] + root = space([item["g"]]) + nodes = [root, item["H"], W] if grow else [root, W] + paid, Z = walk(nodes, root) + need(all(any(p in node for node in nodes) for p in item["receivers"]), "receiver coverage") + need(nodes[-1] == W, "common merge") + paths.append(Z) + costs.append(paid) + T = W + tail = 0 + need(all(W <= Z and W <= T for Z in paths), "merge inclusion") + if hG: + need(G <= W, "hG fails") + if htop: + need(all(join(Z, T) == full for Z in paths), "htop fails") + eta = [] + for c, Z, paid in zip(selected, paths, costs): + H = carriers[c]["H"] + U = join(Z, T) + need(H <= U, "H coverage") + e = int(not U <= H) + need(dim(U) == 8 + e, "eta dimension") + need(paid + tail >= base + e, "repaired individual inequality") + eta.append(e) + k = len(selected) + total = sum(costs) + tail + need(total + (k - 1) * tail >= base * k + sum(eta), "repaired sum") + return {"k": k, "total": total, "tail": tail, "eta": eta, + "path_dimensions": [dim(Z) for Z in paths], + "hG": G <= W, "htop": [join(Z, T) == full for Z in paths]} + + +def all_subspaces(n): + """Closure enumeration, independent of the predecessor RREF generator.""" + found = {frozenset({0})} + todo = list(found) + while todo: + s = todo.pop() + for v in range(1, 1 << n): + if v not in s: + enlarged = s | frozenset(x ^ v for x in s) + if enlarged not in found: + found.add(enlarged) + todo.append(enlarged) + return sorted(found, key=lambda s: (len(s), sorted(s))) + + +def tiny_check(): + subs = all_subspaces(3) + need(len(subs) == 16, "tiny lattice size") + counts = [0, 0] + for H in subs: + if dim(H) != 2: + continue + for g in H - {0}: + for Z in subs: + if g not in Z: + continue + for T in subs: + if not H <= Z | T: + continue + U = join(Z, T) + eta = int(not U <= H) + need(dim(U) == 2 + eta, "tiny eta") + for W in subs: + if W <= Z & T: + need(dim(Z) - 1 + dim(T) - dim(W) >= 1 + eta, "tiny repaired inequality") + counts[eta] += 1 + return {"ambient_dimension": 3, "subspaces": len(subs), "eta_counts": counts, + "admissible_tuples": sum(counts)} + + +def authenticate(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + pins = {} + retained_raw = (HERE / "PREDECESSOR.json").read_bytes() + need(hashlib.sha256(retained_raw).hexdigest() == PREDECESSOR_SHA256, + "predecessor manifest pin") + retained = json.loads(retained_raw) + rows = [row for row in manifest["files"] if row["usage"] == "input"] + rows += [dict(row, path=row["retained_path"]) for row in retained["files"]] + for row in rows: + raw = (ROOT / row["path"]).read_bytes() + digest = hashlib.sha256(raw).hexdigest() + need(digest == row["sha256"], "source SHA256 " + row["path"]) + blob = hashlib.sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() + need(blob == row["git_blob"], "source Git blob " + row["path"]) + pins[row["path"]] = digest + return pins + + +def result(): + pins = authenticate() + word = json.loads(gzip.decompress((ROOT / WORD).read_bytes())) + previous = json.loads((HERE / "inputs/pr6315-RESULT.json").read_text()) + ports = word["ports"] + need(len(ports) == len(set(ports)) == 104, "selected ports") + need(all(dot(p, p) == 1 for p in ports), "odd selected ports") + lines = previous["carriers"]["lines"] + normals = previous["carriers"]["normals_g"] + need(len(lines) == len(normals) == 8, "eight carriers") + carriers = [] + for c, (line, g) in enumerate(zip(lines, normals)): + need(line not in ports and 0 < line < 512 and 0 < g < 512, "carrier labels") + H = frozenset(p for p in range(512) if dot(p, line) == 0) + receivers = [p for p in ports if dot(p, line) == 0] + need(len(receivers) == 52 and dim(H) == 8, "receiver geometry") + need(join(space([g]), space(receivers)) == H, "H equals root plus receivers") + need(all(dot(normals[a], line) == int(a != c) for a in range(8)), "cross normal") + carriers.append({"g": g, "H": H, "receivers": receivers}) + need(dim(space(normals)) == 8, "independent normals") + summaries = [] + subsets = 0 + for k in range(2, 9): + count = 0 + for selected in itertools.combinations(range(8), k): + row = check_model(carriers, selected) + need(row["total"] == 7 * k and row["eta"] == [0] * k, "countermodel price") + need(not row["hG"] and row["htop"] == [False] * k, "missing premise") + count += 1 + subsets += count + summaries.append({"k": k, "subsets": count, "paid": 7 * k, + "eta_sum": 0, "missing_htop": k}) + need(subsets == 247, "subset coverage") + nonzero = [] + for selected in [(0, 1), (0, 1, 2)]: + common = sorted(set.intersection(*(set(carriers[c]["receivers"]) for c in selected))) + need(common and common[0] == 11, "nonzero common selected port") + row = check_model(carriers, selected, merge_vector=11) + need(not row["hG"] and not any(row["htop"]), "nonzero missing premises") + j = ports.index(11) + receiver = word["live"][j] + 112 + frame = word["final"][receiver] + primal = space(word["frames"][frame]) + need(primal == frozenset(x for x in range(512) if dot(x, 11) == 0), "actual endpoint chart") + need(dim(space(word["frames"][word["initial"][receiver]])) == 0, "actual receiver starts at zero") + need(all(lines[c] in primal for c in selected), "line-to-endpoint ascent") + nonzero.append({"carrier_subset": list(selected), "merge_dual_generator": 11, + "selected_receiver_register": receiver, "merge_primal_frame": frame, + "common_receiver_count": len(common), "total": row["total"], + "path_dimensions": row["path_dimensions"], "eta": row["eta"]}) + full = frozenset(range(512)) + positive = [] + for k in range(2, 9): + W = space(normals[:k]) + prefix = sum(walk([space([g]), W], space([g]))[0] for g in normals[:k]) + tail, T = walk([W, full], W) + need(join(W, T) == full, "source-preserving htop") + total = prefix + tail + need(total + (k - 1) * tail == 8 * k, "source-preserving equality") + positive.append({"k": k, "prefix_paid": prefix, "tail_paid": tail, + "total": total, "eta_sum": k}) + zero, root0, root1 = frozenset({0}), space([normals[0]]), space([normals[1]]) + H0 = carriers[0]["H"] + controls = [ + ("underpriced growth", lambda: walk([root0, H0, zero], root0, 6)), + ("missing source root", lambda: walk([zero, H0, zero], root0)), + ("nonnested step", lambda: walk([root0, root1], root0)), + ("omitted growth", lambda: check_model(carriers, (0, 1), grow=False)), + ("pair false hG", lambda: check_model(carriers, (0, 1), hG=True)), + ("pair false htop", lambda: check_model(carriers, (0, 1), htop=True)), + ("triple false hG", lambda: check_model(carriers, (0, 1, 2), hG=True)), + ("triple false htop", lambda: check_model(carriers, (0, 1, 2), htop=True)), + ("unjustified 8k", lambda: check_model(carriers, (0, 1), base=8)), + ("invalid merge line", lambda: check_model(carriers, (0, 1), merge_vector=normals[1])), + ("boolean paid value", lambda: walk([root0, H0, zero], root0, True)), + ] + for label, action in controls: + try: + action() + except Rejected: + continue + raise Rejected("negative control accepted: " + label) + return {"schema": "carrier-merge-relay-premise-v1", "source_sha256": pins, + "geometry": {"ports": 104, "carrier_lines": lines, "source_normals": normals, + "receivers_each": 52, "H_dimensions": [8] * 8}, + "countermodels": summaries, "countermodel_subsets": subsets, + "nonzero_merge_examples": nonzero, + "source_preserving_controls": positive, "small_lattice": tiny_check(), + "negative_controls": [x[0] for x in controls], + "scope": "abstract dual-frame walks; no scalar decoder or dirty restoration verified", + "new_kappa": False} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="write evidence to a new external file") + args = parser.parse_args() + actual = result() + serialized = json.dumps(actual, indent=2, sort_keys=True) + "\n" + if args.output: + destination = args.output.resolve() + need(destination != ROOT and ROOT not in destination.parents, "output must be outside checkout") + with destination.open("x") as stream: + stream.write(serialized) + else: + need((HERE / "RESULT.json").read_text() == serialized, "receipt disagreement") + print("PASS_CARRIER_MERGE_RELAY_PREMISE subsets=247 controls=11") + + +if __name__ == "__main__": + main()