Prove a 120N-bit complete-caller retention floor (no κ)

research/rounded-read-caller-fiber/PROOF.md

@@ -0,0 +1,153 @@
+# A 120N-bit complete-caller fiber from silent rounded reads
+
+This scoped proof concerns the same-grid stochastic numerical ABI of Ali
+Romman's [PR6546](https://github.com/CrocSwap/integer-mult-bounds/pull/6546)
+at `ff038070b8d122a43993f2b2524154323cc6b4d7`, on the selected PR6030 word.
+It builds on the complete-caller fiber argument in his
+[PR6547](https://github.com/CrocSwap/integer-mult-bounds/pull/6547), exact head
+`317e4a099488794c372f8a4ad1e70deef3626bbf`. That predecessor's every-seed
+86N-bit family is cited, not independently verified here.
+
+The new step permits fractional reads before erasure. One explicit seed
+schedule makes 39 such reads of 17 additional fields silent. The resulting
+60-field family strengthens the worst-case retained-capacity lower bound to
+120N bits. The seed quantifier is weaker than the predecessor's: this proof
+constructs one schedule, rather than treating every schedule.
+
+## Contract and theorem
+
+There are 770 arbitrary public fields, each with N complex coordinates in
+`h Z[i]`, for fixed h>0 and N=512^f. Initial owned fields are zero and obey
+the source INIT instructions. Work in integer coordinates in units h.
+For a scalar coefficient q=p/D in lowest terms, D>0, the retained scalar
+seed u belongs to {0,...,D-1}. Its component map is
+
+```text
+Q(q,x,u) = floor((p*x+u)/D).
+```
+
+ADD adds this rounded source product to the destination; SCALE replaces
+its destination. COPY has the literal source/destination read set. Native
+MOVE accesses only its declared field and sends the all-zero field to zero
+for each fixed legal native seed. Records do not feed the forward data path.
+These are hypotheses inherited from PR6546 and PR6547, not new native claims.
+
+Fix the scalar schedule
+
+```text
+u(p,D) = 0 if p>0; D-1 if p<0.
+```
+
+The schedule depends only on the instruction coefficient, not the input,
+coordinate, or a previous output. It is a legal fixed realization of the
+stochastic ABI. Fix any legal native seeds satisfying the zero contract.
+
+**Theorem.** The fixed complete map has a displayed family of
+`2^(120N)` distinct public inputs with identical all-zero complete data
+output. Exact recovery from that output and the unchanged seed needs at
+least 120N bits of additional retained capacity. At f=1 this is 61,440 bits,
+or 7,680 bytes. This exceeds the predecessor's reported worst-case floor
+by 34N bits, or 2,176 bytes at f=1.
+
+The theorem is for unrestricted public same-grid inputs. It does not assert
+a new bound under an even-coordinate entrance promise, correlations imposed
+by multiplication, or another word/output/seed interface.
+
+## Silent source reads
+
+If b is either zero or one and 0<|p|<D, then
+
+```text
+Q(p/D,b,u(p,D)) = 0.
+```
+
+For p>0, both possible numerators lie in [0,D-1]. For p<0, they are D-1 and
+D-1+p, again in [0,D-1]. Also Q(q,0,u)=0 for every legal seed. Thus a
+fractional read of an unmodified binary input can reveal no information
+through the rounded increment, even though it is a genuine data read.
+An integer source coefficient has no such guarantee and is excluded.
+
+## The 60-field witness
+
+Independently choose a bit for each real and imaginary coordinate of each
+of these public fields; set every other public input component to zero:
+
+```text
+118 119 120 121 122 123 126 130 134 135 137 139
+140 141 143 150 152 156 157 158 159 160 161 162
+163 165 167 168 172 176 177 179 180 181 182 184
+186 188 191 194 196 200 202 204 205 207 210 211
+214 215 216 218 219 222 223 259 289 369 506 734
+```
+
+The source-bound certificate records each field's first SCALE, which is a
+signed half. Before that SCALE there is no other SCALE, MOVE, COPY, INIT or
+CLEAR accessing that field, and every ADD source read has 0<|q|<1. ADDs
+may use the field as a destination. The per-field scan and a separate
+whole-word active-label check agree on every erasure event.
+
+There are exactly 39 ADD source reads before erasure, across 17 fields.
+Their full list and all 60 erasure cuts are emitted by verify.py, bound to
+the compressed source hash and verifier hash. The last erasure is event
+10447, so no bit survives after cut 10448. Event indices are zero based.
+No claim of a maximum fiber or an exhaustive classification is made.
+
+## Complete chronological induction
+
+At every cut, each not-yet-erased witness field contains only its original
+independent binary coordinates. Every other live data field is zero.
+This holds at entry.
+
+- An ADD source is zero or an active witness field. A zero source gives
+  zero increment. An active source has 0<|q|<1 by the certificate, so the
+  silent-read identity gives zero increment for both possible bits. The
+  destination is unchanged, preserving the invariant even when active.
+- A SCALE on an active witness is its certified first signed half. It
+  maps both bits to zero and erases that label. A SCALE on any other field
+  preserves its zero value.
+- A COPY, INIT or CLEAR touches no active witness. All of its data are zero.
+- Every MOVE operand is zero. The stipulated native zero contract preserves
+  it. No hidden read of another field is permitted by this contract.
+
+The checker traverses all 22,803 source events, including all 3,453 MOVEs.
+The last erasure occurs after native calls have begun. After cut 10448 all
+data are zero, and the remaining instructions preserve zero. The induction
+holds componentwise for arbitrary N; it does not enumerate 2^(120N) inputs.
+
+## Retained capacity and a matching family code
+
+The input bits give exactly 2^(60*2*N) distinct public inputs, since they
+occupy distinct initial coordinates. The output and complete fixed seed
+are identical. A b-bit retained record allows at most 2^b distinct inverse
+states, hence b>=120N. Original input copies or changed seed contents that
+carry these distinctions count as retained information.
+
+An arbitrary dirty bank with Q possible initial states does not remove the
+obligation if its original state must remain recoverable. Injectivity on
+the product family requires 2^(120N)*Q <= 2^b*Q, giving the same bound.
+This is an information-capacity result, not an initially clean hardware
+storage minimum.
+
+Packing the original 120N bits gives a matching code on this displayed
+family. More concretely, each erasing signed half has residue
+`(p*b+u) mod 2`, equal to b for p=1 and to 1-b for p=-1. The 60 such residue
+fields therefore also encode every original bit bijectively. This uses
+the literal retained residue ABI; it is not a full-input recovery schedule
+or an assertion that other records are redundant on general inputs.
+
+## Limits
+
+The every-seed statement of PR6547 remains distinct. This new family uses
+one coefficient-sign-dependent scalar schedule. A wrong seed can make a
+negative fractional read nonzero, and changing an input bit to two can
+survive a positive half; the checker computes both boundary witnesses.
+
+The finite replays corroborate the written induction. They do not run
+compiled native operators, establish a global fiber maximum, prove physical
+randomness/routing/restoration costs, discharge the five selected assumptions,
+or supply a complete multiplication theorem or a new kappa.
+
+This contribution was produced by Nick Petalas. Credit Ali Romman for the
+same-grid caller, zero-fiber method and question; DreamingOfClouds for PR6030
+and its retained P104 lineage; zxv for the signed-half residue interface in
+PR6066. Pigeonhole counting and chronological induction are classical.

research/rounded-read-caller-fiber/README.md

@@ -0,0 +1,111 @@
+# A 120N-bit complete-caller fiber from rounded reads
+
+This contribution was produced by Nick Petalas.
+
+Claim type: scoped written proof with exact finite corroboration. On the
+unchanged selected PR6030 word, one explicit legal scalar seed schedule
+maps 2^(120N) distinct same-grid public inputs to zero, where N=512^f.
+Exact input recovery needs at least 120N additional retained bits. At width
+one this is 61,440 bits or 7,680 bytes.
+
+Ali Romman's [PR6547](https://github.com/CrocSwap/integer-mult-bounds/pull/6547)
+already supplies an 86N-bit complete-caller family for every seed. It and
+his [PR6546](https://github.com/CrocSwap/integer-mult-bounds/pull/6546)
+complete same-grid stochastic caller are cited predecessors, not audit
+targets. The new construction permits 39 fractional reads of 17 additional
+fields before their bits disappear. A coefficient-sign-dependent seed
+makes those reads silent. This raises the worst-case floor by 34N bits,
+with a weaker seed quantifier. The selected frontier is unchanged.
+
+[PROOF.md](PROOF.md) gives the precise ABI, all 60 witness fields, the
+componentwise all-width induction and information-capacity argument.
+The runtime input is pinned at main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`. The predecessor proof is pinned
+by citation to `317e4a099488794c372f8a4ad1e70deef3626bbf`.
+
+## Reproduction
+
+From the worktree root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/rounded-read-caller-fiber/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rounded-read-caller-fiber
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rounded-read-caller-fiber --check-source-history
+```
+
+The direct command emits a deterministic JSON receipt containing source
+and verifier SHA256 hashes, every silent read and erasure event, then
+`PASS_ROUNDED_READ_CALLER_FIBER`. It writes no files.
+
+Local validation used CPython 3.12.15. Both registered commands pass with
+warnings treated as errors, including the optimized run.
+
+The per-field scan and separate whole-word active-label pass agree on
+60 fields and cut 10448. All 3,453 native operands are checked through
+the zero contract. There are 129 complete literal integer replays,
+including all 120 individual real/imaginary generators and nine simultaneous
+patterns at 1, 4 and 512 complex coordinates. Nine actual rejection controls
+and two computed boundary witnesses cover source corruption, leaking reads,
+native access, copying, wrong scaling, owned access, surviving or duplicate
+labels, invalid labels, wrong seeds and outside-family values.
+
+These are checks of the new family. No predecessor scientific suite, native
+implementation, full selected replay, Lean or Docker run is required or
+claimed. The native zero contract and declared read sets remain hypotheses.
+
+## Scope and limitations
+
+The public domain is arbitrary h-grid data, without an even-coordinate or
+actual multiplication-encoding promise. The result applies to the displayed
+fixed scalar schedule. It does not improve the predecessor's every-seed
+bound, find the global maximum fiber, price physical retained storage, or
+discharge any selected assumption. A matching 120N-bit code is supplied only
+on the displayed family by its erasing half residues. All five framework
+assumptions and the selected kappa remain unchanged.
+
+## Engineering bounds
+
+The verifier authenticates the fixed source before parsing it, with 22,803
+events, 770 public and 799 total labels. The largest data replay has 799*1024
+integer slots; on these fixtures every slot is zero or one. Loops are bounded
+by those dimensions, 129 cases, 60 labels, or the nine rejection controls.
+Functions are under 60 lines. Runtime checks use explicit exceptions and
+remain enabled under optimized Python. No global framework or predecessor
+code is imported.
+
+Power-of-Ten deviations are limited to these offline verification mechanisms.
+
+```text
+Rule: 3, fixed memory after initialization
+Location: verify.py, JSON parsing and integer data replay
+Reason: Python allocates managed objects during arithmetic and parsing.
+Scope: The authenticated fixed source and sequential bounded fixtures only.
+Compensating control: Fixed dimensions, bounded coefficients and masks,
+  799*1024 maximum data slots, and one data replay live at a time.
+Verification: Strict normal and optimized registered replays.
+Follow-up: Use fixed arrays if ported to a constrained runtime component.
+
+Rule: 9, indirect calls
+Location: verify.py, expect_rejection and controls
+Reason: Rejection checks must invoke an operation and observe its exception.
+Scope: The nine explicit local test callbacks only.
+Compensating control: No external callback or dynamic code is accepted.
+Verification: Every callback must raise its specific expected exception.
+Follow-up: Replace callbacks with explicit variants in a constrained port.
+```
+
+## Open next questions
+
+- Can a larger seed-uniform family be found? First inspect whether the 39
+  rounded-read constraints have two common integer solutions for arbitrary
+  seeds. Conflicting read intervals are the blocker.
+- Can correlated input variations enlarge this fixed-schedule family?
+  First allow one exact source read and solve its joint cancellation
+  constraints. A complete causal proof must prevent leakage into native inputs.
+- Which of these inputs are reachable under an actual multiplication entrance
+  contract? Bind one concrete encoding before transferring the capacity bound.
+
+The first verified improvement was packaged without extending these questions.
+Credit Ali Romman for the caller and fiber predecessors, DreamingOfClouds and
+the full retained PR6030 lineage for the word, and zxv for PR6066's residue
+interface. No independent human or formal proof-kernel acceptance is claimed.

research/rounded-read-caller-fiber/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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"
+    }
+  ]
+}