Prove sharp one-pass child batching storage (no new κ)

research/low-type-stream-buffer/PROOF.md

@@ -0,0 +1,138 @@
+# Sharp one-pass storage for whole-high child batches
+
+This scoped proof was produced by Nick Petalas. Apache-2.0.
+
+## Contract
+
+Let n,L,s be positive integers. An input stream consists of independent
+symbols x[u,l,a], in lexicographic order (u,l,a), where 0<=u<n,
+0<=l<L and 0<=a<s. A dispatcher must emit exactly those symbols in
+lexicographic order (l,u,a). It has one forward input pass and one
+append-only output. It may pause either stream, and may pass an arriving
+symbol directly to output. Emitted output cannot be read, overwritten,
+or used as scratch. There is no other external storage or side channel.
+
+Fix any finite alphabet Sigma with cardinality A>=2. Storage means retained
+payload information. Every payload-dependent buffer, register, control state,
+cursor or address is charged. Fixed schedule counters carry no payload
+information and are separate overhead. At a fixed input cut, a retained-state
+family of cardinality A^b requires at least b alphabet-symbol equivalents,
+or b*log2(A) bits. An unbounded integer cell does not have unit capacity here.
+This convention permits arbitrary lossless encodings; it does not assume
+that the dispatcher stores literal symbols. Timing is not an external channel.
+
+## Theorem
+
+The least possible worst-cut retained payload capacity is exactly
+
+    B = (n-1)(L-1)s.
+
+A fixed schedule attains B with B literal symbol slots and deterministic
+address/control overhead. Thus the result also gives the exact slot bound
+in the usual indivisible-record buffer model. It is not a physical tape-time
+bound, a native-cell bound for infinite alphabets, or a supplier theorem.
+
+## Lower bound
+
+Consider the cut after the first n-1 complete input cycles, immediately
+before reading the final cycle. The n=1 or L=1 case has B=0 and needs
+only the nonnegativity bound, so assume n,L>=2.
+
+The dispatcher has not seen x[n-1,0,0]. Correctness for every independent
+payload prevents it from emitting that symbol before reading it. Since
+output order is fixed, no symbol with l>0 has been emitted yet.
+
+Fix every l=0 symbol and every final-cycle symbol to one alphabet element.
+Vary independently the B symbols with u<n-1 and l>0. There are A^B such
+inputs. All already emitted output symbols have the same value. The
+output length can vary, but any payload-dependent output cursor is part
+of the charged retained state.
+
+Two different choices cannot give the same retained state at this input cut.
+Otherwise the unread suffix is identical, as are the already emitted output
+and its cursor. Determinism would give identical remaining output. Correct
+outputs differ at an l>0 symbol, a contradiction. Consequently at least
+A^B retained states are required. This counts compressed representations
+and payload-dependent control as well as explicit buffers.
+
+The statement is for exact deterministic dispatch. It does not assert a
+bound for randomized approximate recovery or a write-only output channel
+that also communicates hidden timing information to another controller.
+
+## Attaining schedule
+
+During the first n-1 cycles, emit the l=0 chunk as it arrives and retain
+every l>0 chunk. The retained size after k whole cycles is k(L-1)s,
+so it never exceeds B. On the final cycle, emit its l=0 chunk directly.
+For l=1,...,L-1 in order, first emit and release all retained chunks of
+that type in increasing u order, then read and directly emit its final-cycle
+chunk. No new retained symbols are required. The buffer ends empty.
+
+There are nLs input reads and nLs output writes. This counts stream
+events only. Accessing the retained chunks in the required order may
+require physical movement, indexing or extra tapes, which are unpriced.
+For n=1 or L=1, input already has the required order and direct bypass
+uses zero payload slots.
+
+## Delayed-cover substitution
+
+Ali Romman's PR #5829 at f1e522fc26371617ed60dea3c4609d422d491d2e supplies
+the declared whole-high batch address contract. We cite that contract; we
+do not replay its address proof. In its notation, at depth j<D the parent
+row index is b=U*H^j+A, with U=U'*(L*H)+l*H+h. Include the complete
+body index r of size R. Reading the canonical parent order means reading
+
+    (U', l, h, A, r).
+
+Emitting each complete child in its declared b' order means emitting
+
+    (l, U', h, A, r).
+
+The theorem applies with
+
+    n_j = T*(L*H)^(D-j-1),
+    s_j = H^(j+1)*R,
+    V_j = n_j*L*s_j = T*(L*H)^D*R/L^j.
+
+Its exact payload capacity is therefore
+
+    B_j = (T*(L*H)^(D-j-1)-1)*(L-1)*H^(j+1)*R
+        = ((L-1)/L)*(1-1/n_j)*V_j.
+
+The high fields remain in s_j. They are not discarded or treated as fixed
+payloads. With L=2,H=2,T=1,D=2,j=0,R=1, the parent has 16 symbols
+and the exact buffer is 6 symbols. For fixed L>1 and increasing n_j,
+the buffer fraction tends to (L-1)/L. A sublinear buffer in V_j cannot
+implement this particular one-pass, sequential-child interface in that limit.
+
+This does not refute #5829's O(V_j) local-space premise. It supplies a
+necessary term for one implementation of its still-open dispatcher. Multiple
+independently writable child streams, another input pass, random access,
+interleaved child execution or a changed parent order can evade the contract.
+No assertion is made that the current caller requires this interface.
+
+## Finite evidence and implementation limits
+
+The verifier executes literal streams, an independent output-prefix cut
+oracle and a minimax dynamic program over every legal read/emit interleaving
+for every permutation through length seven. It checks the closed form on
+all n,L,s in {1,...,8}, actual binary payloads on a declared complete small
+domain, injective binary cut states, algebraic cover substitutions, and
+subcritical and malformed-input rejection. The universal claim follows
+from the preceding proof, not from the finite bounds.
+
+The Python code is a simulator, not a measured physical buffer implementation.
+Its input, output log and optional snapshots are checker instrumentation.
+Only the simulated retained dictionary contributes to its reported payload
+peak. It deliberately contains no predecessor imports or scientific replay.
+
+Power-of-ten rule 3 deviation: CPython and its standard library allocate
+managed objects dynamically, including integers and checker logs. Streams
+are validated at at most 4096 symbols with signed 64-bit payloads. Production
+simulation dictionaries, logs and snapshots have at most 4096 entries each;
+the scheduling oracle is called only through size seven, with at most 64
+cells. Cut-state sets have at most 1024 states of at most ten pairs each.
+All search loops have explicit finite ranges, functions are below 60 lines,
+and checks raise normally under optimized Python. Warning-strict normal and
+optimized runs provide the available interpreter diagnostics. A physical
+fixed-capacity implementation and its allocator diagnostics remain future work.

research/low-type-stream-buffer/README.md

@@ -0,0 +1,73 @@
+# Exact payload storage for one-pass child batching
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+For n repeated input cycles, L low types and s symbols per type per cycle,
+one forward input pass that emits complete child batches sequentially needs
+exactly
+
+    (n-1)(L-1)s
+
+alphabet-symbol equivalents of retained payload information. The lower bound
+permits arbitrary lossless encodings and charges payload-dependent controller
+state. An explicit schedule attains it with literal symbol slots. Claim type:
+scoped written proof with finite corroboration. See [PROOF.md](PROOF.md).
+
+This answers one restricted version of the physical-dispatcher question in
+[Ali Romman's PR #5829](https://github.com/CrocSwap/integer-mult-bounds/pull/5829),
+at head f1e522fc26371617ed60dea3c4609d422d491d2e. Its whole-high batch address
+contract is the cited predecessor, not an audited deliverable. At its depth j,
+put n_j=T*(L*H)^(D-j-1) and s_j=H^(j+1)*R. The new storage term is
+((L-1)/L)*(1-1/n_j)*V_j. The L=2,H=2,T=1,D=2,j=0,R=1 fixture
+requires exactly six retained symbols for a sixteen-symbol parent.
+
+This is an explicit linear-storage term for the stated interface. It does
+not refute the predecessor's O(V_j) premise or prove that a physical caller
+must use this interface. Multiple writable child streams, rereads, random
+access and changed traversal orders are outside scope. Unbounded integer
+or exact-complex cells do not have unit information capacity in this model.
+Physical movement, numerical precision, native execution, cleanup and the
+complete supplier bill remain open. No new kappa or frontier change is claimed.
+
+## Reproduction
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/low-type-stream-buffer/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/low-type-stream-buffer/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/low-type-stream-buffer
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/low-type-stream-buffer --check-source-history
+```
+
+Any CPython 3.12 path can replace the local interpreter path. Direct success
+prints PASS_LOW_TYPE_STREAM_BUFFER. The verifier checks complete domains
+declared in its functions, independent prefix and scheduling oracles, actual
+payload outputs, cut-state injectivity and rejection controls. It can write
+a generated receipt with --receipt /absolute/path/outside/package.json;
+the receipt binds all six package files by SHA256. No generated evidence
+is stored in this package. Independent human and formal proof-kernel review
+are unclaimed.
+
+The source manifest pins the task and selected record as historical provenance.
+The PR #5829 contract is a cited mathematical premise, recorded separately
+with its exact head, paths and hashes; it is not a runtime or Git-history
+dependency. No pending predecessor code is imported or fetched during replay.
+
+## Open next questions
+
+- Can the final compiled template emit into multiple independently writable
+  child streams while retaining complete arbitrary-input return and a smaller
+  local buffer? Start with the sixteen-symbol fixture. Physical stream count,
+  head placement, return order and a complete movement bill are the blockers.
+- What time and storage bill does a literal fixed-tape implementation of the
+  attaining one-pass schedule incur? Start by charging the six-slot fixture's
+  retained-chunk reads and releases. A source-bound dispatcher and its cleanup
+  contract are still required.
+
+Credit Ali Romman for PR #5829's whole-high batch address contract and open
+dispatcher question, Mason Hale for its recursive-allocation predecessor,
+and the retained BIT/compiler/cover authors credited there. Streaming
+permutation cuts and the elementary information-counting method are classical.
+The new contribution is the sharp buffering result for this declared interface,
+its delayed-cover substitution, attaining schedule and standalone corroboration.

research/low-type-stream-buffer/SOURCES.json

@@ -0,0 +1,35 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ],
+  "cited_mathematical_contract": {
+    "pr": 5829,
+    "author": "Ali Romman",
+    "head": "f1e522fc26371617ed60dea3c4609d422d491d2e",
+    "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5829",
+    "role": "Cited address contract and open dispatcher question; no runtime dependency, imported code, or predecessor verification claim.",
+    "documents": [
+      {
+        "path": "research/delayed-cover-batch-allocation/README.md",
+        "sha256": "559bee7010e02a436a67528a1b2580881e1d5b7567a66cceb7fe86ae9ba3c557"
+      },
+      {
+        "path": "research/delayed-cover-batch-allocation/PROOF.md",
+        "sha256": "adab55de97f1336a58922b2fc92782af335a94a36cbaae34d6d3314d18a882ea"
+      }
+    ]
+  }
+}

research/low-type-stream-buffer/TASK.json

@@ -0,0 +1,102 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Sharp retained payload storage for a one-pass parent stream emitting complete low-type child batches sequentially, with the delayed-cover address substitution.",
+  "scope_change_reason": "The donor requests original work rather than another audit. The formal-interface card is changed to a scoped written dispatcher-storage theorem, not proof-assistant formalization or predecessor verification.",
+  "bottleneck_link": "Prices one missing local-space term in the delayed-cover physical dispatcher; it does not discharge the full precision_tape assumption.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first sharp buffer bound with an attaining schedule and independent finite checks; do not extend the model.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and verify.py; generated receipts live outside the checkout.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can multiple independently writable child streams reduce this buffer with complete return?",
+      "why_it_matters": "The sharp bound depends on one sequential child-output stream.",
+      "first_step": "Implement the sixteen-symbol, six-buffer fixture with two writable child streams.",
+      "blocked_by": "Physical stream count, head placement, source binding and full movement/return bill."
+    },
+    {
+      "question": "What literal fixed-tape cost realizes the attaining one-pass schedule?",
+      "why_it_matters": "An information bound is not a complete time or physical storage implementation.",
+      "first_step": "Charge all reads and releases for the six-slot fixture.",
+      "blocked_by": "A source-bound dispatcher, head movement and cleanup contract."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216164"
+}

research/low-type-stream-buffer/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Literal batches, all permutations through length seven, independent prefix/minimax scheduling oracles, binary payloads, information-cut injection and rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same full finite evidence with interpreter assertions disabled."
+    }
+  ]
+}