Bind P104 outgoing ports to recipient histories and input admission

research/p104-external-port-closure/PROOF.md

@@ -0,0 +1,110 @@
+# Conditional dependency, admission and endpoint proof
+
+Hiroki Kumazaki with substantial OpenAI Codex assistance. Apache-2.0.
+
+## 1. Literal closure
+
+Give every initial bank a distinct state version. Each transport/sign depends
+on its preceding bank version; ADD depends on both the preceding target and
+current source; zero has no value predecessors; erase depends on its current
+private value. The least predecessor-closed set containing an observation is
+its graph ancestor set. This proves the SSA algorithm's literal minimality.
+
+For any touched private lifetime, also require its matching erase. Iterate
+predecessor closure and this requirement to a fixed point. Each iteration only
+adds vertices in a finite graph, so it terminates. Any legal set satisfying
+these two conditions contains every iteration, hence contains the result.
+This minimality is graph-theoretic, not a lower bound against cancellation or
+alternative schedules. The independent reverse scan propagates live demands
+through precisely the same literal instructions without constructing this DAG.
+
+The 675 observations use the exact published PR3423 port-index hash. At an ADD
+observation, predecessor closure retains both the current recipient history and
+the actual source history. Running retained instructions in their original
+order therefore yields each observed ideal value, by induction. Private erase
+checks prove exact zero scalar rows, rather than silently discarding dirt.
+
+The original 146 endpoint observations require 265 inputs. Requesting the
+original endpoints of those 265 inputs adds 215 events and no new inputs.
+This is a selected-output projection. Other outgoing effects are not implied
+by preserving its selected endpoints; they are explicitly listed separately.
+
+## 2. Native premise and normalized rows
+
+Assume the relevant initial and current chart maps `A_H` are unitary
+automorphisms of `B9`, and every used native transport has its archived operator
+`T_(H->K) = A_K A_H^-1`, and that each complete native primitive is unitary,
+preserves `B9 = E Z[i]^512`, and is exact for the admitted module on the common
+grid. These are the existing chart/module implications, not consequences of
+our file hashes. The new check binds all used occurrences to their source data.
+
+Put `z_s = A_initial(s)^-1 v_s(0)`. Induction gives
+
+`v_b(t) = A_frame(b,t) sum_s r[b,s,t] z_s`.
+
+Transport changes the outer frame only. Common-frame ADD performs the literal
+rational row addition. Sign negates a row. Private zero creates the zero row;
+erase is allowed only for the zero row. These arguments quantify over arbitrary
+independent dirty initial arrays, not just the three numerical fixtures.
+The final formula keeps both frame factors; neither initial X frames nor final
+Y frames can be dropped.
+
+The exact retained matrix shows normalized restoration of 213 non-X banks and
+an identity X diagonal plus a rank-9 Y map on the 52 X endpoints. The rank is
+computed by corrected rational pivot elimination, with duplicate/dependent-row
+regressions. A separate explicit factorization expresses all 52 rows using
+nine named rows and verifies every coefficient; a 9-by-9 minor of those rows
+has determinant `-1/128`. These give the matching upper and lower rank bounds. The separate literal fixture interpreter
+checks projection/full ideal-word agreement but is not the universal proof;
+the induction and complete exact rows provide that statement.
+
+## 3. Minimal independent dyadic product entrance
+
+Restrict each independent initial bank to `2^k_s B9`, `k_s >= 0` an integer.
+The chart automorphism premise makes each normalized `z_s` independently
+arbitrary in that same module. For any one row, its output lies in `B9` for all
+such inputs if and only if `r[b,s] 2^k_s` is an integer for every source s.
+
+Sufficiency follows from integer linear closure of B9. For necessity, set every
+other input to zero and choose `z_s = 2^k_s E e_0`. Applying `E^-1` to that row
+leaves its nonintegral scalar coefficient in the zeroth coordinate. The outer
+chart is an automorphism, so it cannot repair nonmembership. All coefficients
+are real dyadic rationals; the maximum reduced-denominator exponent over every
+retained row is consequently the coordinatewise-minimal k_s.
+
+The computed maxima are two for all 104 Y inputs, one for the 38 listed N
+inputs, and zero for the other 123. Reducing any positive exponent by one is
+rejected using its actual coefficient witness (142 cases). This is a condition
+for the retained *prefix invariant*. It does not characterize correlated inputs
+or domains admitting only the final cut. N33/N34's omitted full-word half-reads
+are not licensed by this projection's weaker entrance.
+
+Every retained ADD includes its before and after rows. Under this entrance both
+are in B9, hence their difference—the actual increment—is also in B9. Thus
+rational coefficient divisions are exact on the common grid. Native prefix
+exactness uses the separate inherited module premise; scalar rows alone do not
+verify a native circuit's phase or intermediate rounding.
+
+The event-312 witness is stronger than an odd-integer half: `N100(x)=2*x_0`
+is in B9 because its only nonzero Newton coefficient is `2/(1+i)=1-i`.
+No instruction has touched N100 before its half-read. All other banks remain
+zero beforehand. Its arithmetically exact half `x_0` has coefficient
+`1/(1+i)=(1-i)/2`, outside the Gaussian integers. `4*x_0` is the positive
+2B9 control. This satisfies every original 63-bank entrance assumption and
+exhibits an independent external admission obligation.
+
+## 4. Conditional payload width
+
+Let H bound each real and imaginary physical input component across the 265
+inputs. Each 512-entry complex vector has Euclidean norm at most `32H`.
+Unitary initial chart normalization preserves this norm. Triangle inequality
+and the exact row identity give `||v_b||_2 <= 32H sum_s |r[b,s]|`.
+The retained maximum is `127/2`, first at event 3589, so `2032H` bounds each
+payload component. Unitary complete native prefixes preserve the entrance norm;
+partially written disjoint components inherit a bound from their before/after
+stage. This reproduces the retained norm estimate on the actual recipient
+slice, not a new global estimate or a physical storage theorem.
+
+H itself, initial domain preparation, physical allocation, scratch layout,
+movement, controls, exposed codecs and recursive interfaces still need a paid
+caller. The unchanged-profile `599/584` stop is unaffected.

research/p104-external-port-closure/README.md

@@ -0,0 +1,160 @@
+# Closing the P104 open program's external recipient histories
+
+This answers [PR3423's 675-port handoff][handoff] at
+`15d28c4de37dc47ea07cd7173c8b318fca7a4d75`, using the unchanged literal PR2586
+word retained on canonical main `6f100d4bb5083f8c35d96fd95a539811c62f245c`.
+The result is a source-bound dependency and conditional numerical interface,
+not a physical supplier or a new multiplication exponent.
+
+## Result
+
+The 63-bank open program's 675 outgoing ADDs reach 83 distinct recipient banks.
+Their actual histories require substantially more inputs:
+
+| Observations required | Events with private cleanup | Initial banks |
+| --- | ---: | ---: |
+| All 675 recipient states immediately after their port ADD | 2,907 | 263 |
+| Final endpoints of the 83 recipients and 63 original banks | 3,812 | 265 |
+| Also preserve the original endpoint histories of all 265 dependencies | 4,027 | 265 |
+
+A state-version dependency graph and a separately written reverse-liveness
+scan agree on the exact event and input sets. These are least closures in the
+literal read/write graph with all touched private lifetimes closed. They are
+not minima over algebraic cancellations, rewritten programs or different
+implementations. Merely adding the eight erases is insufficient: their forty
+cleanup predecessors must be included too.
+
+The final 4,027-event projection has 2,310 ADDs, 1,597 native transports,
+104 signs, eight private allocations and eight zero-checked erasures.
+It reaches all 265 original endpoints without introducing more inputs.
+It omits 1,371 word events and 93 initial banks. **696 omitted outgoing ADDs** to those 93 banks
+are explicitly inventoried in [SUMMARY.json](SUMMARY.json); this projection
+is not a replacement for the whole word on those omitted banks.
+
+## Additional admission and an exact-half counterexample
+
+Conditional on the inherited native chart identities and Gaussian Newton
+module invariance, the coordinatewise-minimal independent dyadic product
+entrance for **every retained atomic state** is:
+
+- All 104 initial Y banks in `4B9`.
+- The following 38 N banks in `2B9`:
+  `2,4,7,9,18,20,27,29,35,36,40,44,45,46,48,49,50,54,58,59,64,65,66,70,74,75,79,80,81,83,84,85,87,88,89,92,98,100`.
+- The other 123 dependencies in `B9`: 52 X, 32 D, 29 G, eight Q, and N33/N34.
+
+Here `B9 = E Z[i]^512`, with
+`E = [[1,0],[1,1+i]] tensor ... tensor [[1,0],[1,1+i]]` (nine factors).
+One common grid `2^-f` can scale every displayed module.
+Relative to PR3423 this adds 202 initial banks: 52 more strengthened Y inputs,
+38 half-read N inputs, two ordinary N inputs, 52 X, 27 D, seven Q and 24 G.
+It does not claim that correlated final-cut domains require these individual
+scales; PR3426 studies such cancellations separately. The whole-word product
+theorem of PR3406 is credited, not rediscovered: this result specializes the
+entrance to the actual recipient closure, where N33/N34 need only `B9`.
+
+The first added incoming boundary is event **312**, `X100 += N100/2` at the
+empty frame. Set `N100(x)=2*x_0` on the 512 binary addresses, and all other
+initial banks to zero. Every input belongs to `B9`, and all PR3423 63-bank
+admissions hold. The division is exact in Gaussian integers, but its output
+`X100(x)=x_0` has Newton coefficient `(1-i)/2` at index one, outside `Z[i]`.
+The source coefficient is `1-i`. Amplitude four is the positive control.
+This exposes an additional recipient admission obligation; it is not a defect
+in PR3423, which explicitly left recipient histories open.
+
+## Composed endpoints and widths
+
+Write `A_F = Delta_F`, with the empty-frame map equal to identity. Under the
+native covariance premise, at every retained state the exact physical value is
+
+```
+v_b(t) = A_frame(b,t) * sum_s r[b,s,t] * A_initial(s)^(-1) * v_s(0).
+```
+
+The certificate retains the complete rational rows, actual initial frames and
+actual final frames. Initial X banks are not at the empty frame. Final frames
+also vary; using PR3423's common frame at event 4516 for the later endpoints
+would be incorrect.
+
+All 213 non-X banks in the 265-bank projection return their normalized initial
+rows. Each of the 52 X endpoints has its own initial X coefficient one, only Y
+increments, and no residual N/D/Q/G dirt. The actual complete 52-by-104 Y map
+has rational rank 9: every row has a retained nine-row factorization and a
+9-by-9 minor has determinant `-1/128`. This is a different, larger operator from PR3423's
+rank-one **subset of port increments**; the remaining histories are included
+here. [CERTIFICATE.json.gz](CERTIFICATE.json.gz) provides every endpoint row
+and the before/increment/after rows for all 675 ports.
+
+If every initial real/imaginary component of the 265 physical inputs is bounded
+by `H`, unitary chart maps give `32 H * ||r||_1` as a payload bound. The maximum
+row norm is `127/2`, at event 3589 on X46, giving **2032 H**. This is the retained
+whole-word norm bound, now bound to the recipient histories; no sharper global
+width claim is made. Native prefix unitarity extends it to complete native
+stages. Physical storage, temporary layout, caller heights, ownership, routing,
+control, exposed representation conversions and recursive charges remain unpaid.
+
+The inherited unchanged-profile `599/584` stopping decision remains. This
+interface certificate does not justify another supplier-construction round.
+
+## Evidence and reproduction
+
+The checker imports no predecessor executable. It binds the unchanged WORD and
+NATIVE files and all native occurrence/frame/rank records. Native operator
+semantics are **assumed**, not proved by matching those records. PR3382's module
+theorem and PR3416's broader native-covariance certificate are credited external
+premises; PR3423's 392-occurrence check alone does not cover this larger slice.
+
+The bounded check includes eight structural/semantic rejection groups, 142
+one-bit-weaker input-scale controls, two dependent-row rank regression cases,
+an exact rank factorization/minor, three independent literal scalar fixtures
+comparing the projection with the full ideal word, and the exact-array Newton
+counterexample/positive control. The full-word comparison is scalar algebra
+under the chart premise, not a rounded native execution on unadmitted inputs.
+
+```sh
+python3.12 -B scripts/research_package.py --package research/p104-external-port-closure
+python3.12 -I -O -B research/p104-external-port-closure/verify.py
+```
+
+Runtime uses only the standard library. `verify.py --emit` prints the complete
+certificate; `verify.py --summary` prints its summary.
+`oracle.py --full` prints the independently reconstructed closure.
+[SUMMARY.json](SUMMARY.json) is the readable summary; [PROOF.md](PROOF.md) states
+the conditional implications. Exact base, source hashes, context heads, overlap
+coverage, environment and command outcomes are in SOURCES.json and TASK.json.
+No heavy native replay, Lean check or selected-frontier replay is claimed.
+
+## Open next questions
+
+1. Can a paid caller supply this 265-bank entrance and physical layout, including
+   the 52 additional `4B9` and 38 `2B9` admissions? Start with the explicit input
+   list and event-312 witness; stop at any unproved divisibility or ownership
+   premise. Current H and input modules are assumptions, not preparation costs.
+2. If using the projection inside the original word, how will its omitted
+   outgoing effects be supplied and paid? Start with the exact omitted-ADD list
+   in SUMMARY.json. The selected endpoints alone do not preserve those effects.
+   Any changed supplier/profile must first pass a compatible full cost screen.
+
+## Credit and scope history
+
+Hiroki Kumazaki, with substantial OpenAI Codex assistance for analysis, code,
+execution, writing and separate AI-agent review. No independent human or
+formal proof-kernel review is claimed. Apache-2.0.
+
+Credit Clear1nsight (PR3423/3382 and the explicit handoff), ywz65 (PR2586 word
+and native recipes), Arham Tahir (PR2665 binding and PR2674 atomic row/grid
+bounds), Tekalign (PR3025 literal wrapper/ledger), Ross Richardson (PR3068
+period domain), Nick Petalas (PR3406 product domain, PR3416 native covariance,
+PR3426 correlated entrance), and the original geometry/native/compiler lineage.
+Jose Manuel's unchanged-profile stop and Vasek's PR2744 audit remain credited.
+The main `p104-whole-word-internal-grid` package already proves the whole-word
+row norm and an alternative sufficient enlarged fixed grid.
+
+This refines the current P104 producer/consumer question by taking the released
+PR3423 handoff, rather than repeating the preceding PR3044 audit or reopening
+fixed-cover matching searches. Entry overlap covered 353 open PRs and 2,277
+Discussion records with complete pagination; literal numeric searches have
+false-positive matches. Focused PR3423/675-port and canonical-thread checks
+found no other published closure for this handoff. Coverage excludes unpublished
+work and exhaustive historical diffs. The canonical claim is recorded in TASK.
+
+[handoff]: https://github.com/CrocSwap/integer-mult-bounds/discussions/2750#discussioncomment-19009429

research/p104-external-port-closure/SOURCES.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "6f100d4bb5083f8c35d96fd95a539811c62f245c",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    },
+    {
+      "path": "research/p104-rounded-collector/inputs/NATIVE.json.gz",
+      "usage": "input",
+      "git_blob": "04f2877aa5444948b7ae37efd267745af82cb34d",
+      "sha256": "ab91c78835c3e10cf3b2cb8a5d4e0b7cfc3df1ae5a811298d27842f2193e1e3d"
+    },
+    {
+      "path": "research/p104-rounded-collector/inputs/WORD.json",
+      "usage": "input",
+      "git_blob": "93acaabc0a523789ef2f1b06f6eeeefed5551397",
+      "sha256": "cec1fb3fbd0067b500ad5119a62ba60685be718e769374d7ec8abdd2beaa7e50"
+    }
+  ],
+  "context_sources": [
+    {
+      "pr": 3423,
+      "head": "15d28c4de37dc47ea07cd7173c8b318fca7a4d75",
+      "path": "research/p104-newton-interfaces/RECEIPT.json",
+      "sha256": "fbc444897b13be5973c92ecfa5de67a8efae13b1aca0d8181bd430e2cffba1d3",
+      "usage": "Inspected published port boundary;675eventindices authenticate to04b3a0bc022c336c9b177eeed49036f1257ab81ea9d0459b8170075b002a24a4. No executable import or Git fetch required."
+    },
+    {
+      "pr": 3406,
+      "head": "18a054fd585ab4b2010770ec83cba0c9f28184e3",
+      "usage": "Credited wholewordproductdomain, not rerun or imported."
+    },
+    {
+      "pr": 3416,
+      "head": "f1112560883a5e81b1a29c37c81a79a20be31fe3",
+      "usage": "Native covariance external mathematical premise, not rerun or imported."
+    },
+    {
+      "pr": 3426,
+      "head": "ce2221dddab6efd3027c09269765dd7eb45f2877",
+      "usage": "Distinct correlated finalcut result, not rerun or imported."
+    }
+  ]
+}