Prove sharp clean storage for reversible Gaussian overwrite (no κ)

research/gaussian-smith-reversible-capacity/PROOF.md

@@ -0,0 +1,128 @@
+# Sharp clean capacity for reversible Gaussian overwrite
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Contract and predecessor results
+
+Let pi=1+i, R_P=Z[i]/(pi^P), N=2^n, and
+F(x)=C tensor n times x over R_P, where C=[[i,1],[1,i]].
+Both n and P are nonnegative integers. R_0 is the singleton ring.
+
+Ali Romman's [PR #5821](https://github.com/CrocSwap/integer-mult-bounds/pull/5821),
+head `c137f338117e8a88816ce254efe3b1494809711f`, proves the response-image
+information formula
+
+    D(n,P) = sum_(j=0)^n binom(n,j) max(P-2j,0).
+
+It leaves reversible truncation and cleanup explicitly open in README question 4.
+Its source is Dugongue's [PR #5815](https://github.com/CrocSwap/integer-mult-bounds/pull/5815),
+head `f0fcda576df410dc15cd5b8183d4f74d284eba2b`, which supplies
+
+    C = S diag(1,pi^2) T,
+    T(a,b) = (a-i*b,b),    S(a,b) = (i*a,a+b).
+
+These are cited predecessor results, not claims of this contribution. Their
+tensor factors T_n and S_n are permutations of R_P^N. The diagonal factor at
+label u is multiplication by pi^(2|u|). The new result below concerns a
+destructive reversible interface, unlike the predecessor's source-preserving
+array computation. No predecessor census, precision theorem or invoice is
+replayed as the deliverable.
+
+## Theorem
+
+Consider any permutation on a public field R_P^N, c initially zero bits, and
+an arbitrary finite borrowed dirty field B. For every x and every initial
+dirty value b, require the final public field to equal F(x). All auxiliary
+outputs must stay within those c bits and B. Allow arbitrary reversible
+mixing, nonlinear operations, and changes to the dirty field.
+
+The exact minimum c is
+
+    K(n,P) = NP - D(n,P)
+           = sum_(j=0)^n binom(n,j) min(2j,P).
+
+A permutation attaining c=K can return B unchanged. This is a logical
+reversible-encoding theorem, without a gate-count, running-time or tape claim.
+The initially zero bits become retained output information. They are not
+promised clean again at the end.
+
+### Necessity, including arbitrary dirty workspace
+
+Restrict the permutation to the allowed input slice where the c bits are zero.
+There are 2^(NP)|B| distinct inputs in that slice. The required output field
+has 2^D possibilities by the cited theorem. The remaining fields have at most
+2^c|B| possibilities. Injectivity therefore requires
+
+    2^(NP)|B| <= 2^D 2^c |B|,
+
+and hence c>=NP-D. This argument permits the borrowed field to change. Requiring
+its restoration cannot weaken the bound. It also permits an arbitrary finite
+nonbinary B. Arbitrary initially unknown states do not supply clean capacity.
+
+### Sufficiency by explicit permutation
+
+Every element of R_P has a unique P-bit pi-adic representation
+
+    z = sum_(t=0)^(P-1) d_t pi^t,    d_t in {0,1}.
+
+Successive reduction modulo pi and exact division by pi prove uniqueness.
+For a diagonal exponent 2|u|, put e=min(2|u|,P), q=P-e.
+Write its P input bits as a q-bit low part l and an e-bit high part h.
+Allocate e initially zero bits a. Apply the bit permutation
+
+    (l,h,a) -> (a,l,h),
+
+where the first e+q=P output bits are the public coordinate and the last e
+bits are the auxiliary coordinate. When a=0, the public coordinate represents
+pi^e*l modulo pi^P, exactly pi^(2|u|)*z. The high part h retains the lost
+information. For arbitrary a, this remains a permutation, with literal inverse
+
+    (a,l,h) -> (l,h,a).
+
+If e=P, the entire public coordinate is swapped with its clean field. If e=0,
+the step is the identity. Thus zero raw precision and zero tensor depth also
+have valid endpoints.
+
+First apply T_n to the public field. Apply these disjoint coordinate
+permutations, using a total of sum_u min(2|u|,P)=K clean bits. Finally apply
+S_n to the public field. Tensoring the cited factorization proves that a zero
+auxiliary input gives F(x). Composition proves a permutation on every public
+and auxiliary state, not just on the allowed zero slice. Leave B untouched.
+To invert, apply S_n inverse, the inverse coordinate permutations, and T_n
+inverse. This construction attains the lower bound.
+
+## Consequences and scope
+
+For normalized precision p with the predecessor's raw exponent P=p+n,
+
+    K = sum_j binom(n,j) min(2j,p+n).
+
+In particular, if p>=n, all exponents are unsaturated and
+
+    K = sum_j binom(n,j) 2j = n 2^n.
+
+At p=n>0, the sharp initially clean capacity is half the public raw input
+bit count, since that input has 2n 2^n bits. The attaining auxiliary output
+retains those n 2^n bits.
+
+For n>0 and P>0, K>0. A reversible host cannot complete this overwrite and
+reset all nonpublic fields while retaining only the rounded modular response.
+If the c clean bits must finish zero, the output-count bound has factor one
+in place of 2^c, and contradicts injectivity whenever K>0. Even allowing the
+dirty field to change cannot repair that deficit.
+Restoring the auxiliary to zero requires preserving or recovering additional
+input information, changing the output contract, or permitting irreversible
+erasure. An exact unrounded invertible response is a different contract.
+
+The predecessor preserves the original source. That source already retains
+the information lost by F, so this overwrite lower bound does not apply to
+its source-preserving compute-copy-uncompute route. This result neither
+invalidates that route nor prices its additional passes.
+
+The all-size statement rests on this written argument and the cited Smith
+and image theorems. The checker verifies new finite reversible augmentations,
+including nonzero auxiliary states, inverse recovery, every individual lost
+bit, and dirty-capacity inequalities. It does not reestablish the predecessor's
+image theorem by counting its outputs. Physical reversible primitives, their
+gate and tape costs, reusable clean restoration, the five selected framework
+assumptions and any kappa improvement remain open here.

research/gaussian-smith-reversible-capacity/README.md

@@ -0,0 +1,113 @@
+# Sharp clean storage for reversible Gaussian overwrite
+
+The exact initially clean storage for destructively overwriting
+`C tensor n times x modulo pi^P`, with `C=[[i,1],[1,i]]` and `pi=1+i`, is
+
+```text
+K(n,P) = sum_j binom(n,j) min(2j,P) bits.
+```
+
+This minimum allows arbitrary reversible mixing and arbitrary finite borrowed
+dirty workspace, even if the dirty field may change. An explicit bit permutation
+through the cited Smith factors attains it while leaving dirty workspace alone.
+The retained auxiliary output cannot then be erased reversibly from the modular
+response alone. This answers the destructive-overwrite portion of Open next
+question 4 in [Ali Romman's PR #5821](https://github.com/CrocSwap/integer-mult-bounds/pull/5821).
+
+At normalized precision `p>=n`, raw precision is `P=p+n` and the sharp clean
+capacity is `n*2^n` bits. At `p=n>0`, that is half the public raw input size.
+These are storage bounds, without a time or kappa improvement.
+
+## Claim and evidence
+
+This is a scoped written mathematical proof with exact finite corroboration.
+[PROOF.md](PROOF.md) states the contract, counting lower bound, attaining
+permutation, inverse and cleanup consequence. The predecessor's image theorem
+and Smith factors are cited; its image census and precision/cost replays are
+not this contribution. The new verifier checks the augmented reversible map.
+
+The finite checks enumerate 17,898 full public/auxiliary states in 14 complete
+permutations, including 646 clean-input endpoints. They also check 432 larger
+interfaces, 272 clean endpoints, 1,492 individual retained-bit witnesses,
+216 dirty-undercapacity comparisons, ten invalid-input controls and four
+semantic controls. The verifier emits a generated SHA256-bound receipt to
+stdout and writes no files. No receipt is hand-authored or stored in this package.
+
+The original `uniform-transfer-audit` card is explicitly changed to this
+successor-interface result. It concerns `owned_erasure` and `precision_tape`
+boundaries, but does not discharge an assumption of selected #5599. The source
+preserving array contract remains different: retaining the original source
+already retains the lost information. Physical reversible gates, tape routing,
+operation costs, reusable clean restoration and independent human/formal
+proof-kernel review remain unclaimed. The selected frontier is unchanged.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+PY=/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12
+"$PY" -W error -B research/gaussian-smith-reversible-capacity/verify.py
+"$PY" -O -W error -B research/gaussian-smith-reversible-capacity/verify.py
+"$PY" -B scripts/research_package.py --package research/gaussian-smith-reversible-capacity
+"$PY" -B scripts/check_research_commit.py --package research/gaussian-smith-reversible-capacity --check-source-history
+```
+
+The last command checks publication bytes after committing. Both registered
+commands have 30-second timeouts. Normal and optimized verification use explicit
+exceptions, so optimization cannot remove the checks. A Git-free exported copy
+can run the direct verifier from any working directory. Source history is
+required only for metadata provenance and publication checks. No predecessor
+code, Git object from a pending PR, network access or dependency installation
+is needed by the scientific replay.
+
+## Execution bounds and implementation decisions
+
+Only `overwrite` and `dimensions` are the executable interface; arithmetic and
+chart helpers receive validated internal values. The implementation caps depth
+at 8 and raw precision at 16, hence 256 public coordinates and 4,096 bits in
+each public/auxiliary field. This bound restricts the executable corroboration,
+not the all-size written theorem. Exhaustive enumeration is separately capped
+at 14 total bits. Larger fixtures use `n<=5`, `P<=8` and eight patterns per case.
+
+The implementation uses bounded loops without recursion, direct calls and no
+generated code. Every function is under 60 physical lines. Runtime contracts
+and verifier failures use exceptions that remain active under optimization.
+Python requires dynamic object allocation, a Power of Ten rule 3 deviation.
+Its scope is this bounded offline model. Fixed dimension limits, a maximum
+16,384-entry exhaustive state set and the registered timeout bound resources;
+no host-memory or physical-tape bound is inferred from Python execution.
+A lower-level physical implementation would need its own allocation and
+operation ledger. Warning-strict normal/optimized replay is the available
+diagnostic check; separate Python static analyzers are unavailable on PATH.
+
+## Open next questions
+
+1. Implement the attaining pi-adic permutation on one permitted reversible
+   native/tape host. The clean-capacity optimum alone gives no operation bill.
+   Start with the one-axis map and charge chart conversion and each bit move;
+   the physical gate alphabet and representation contract are blockers.
+2. Price source-preserving compute-copy-uncompute against destructive overwrite
+   plus retained kernel information for one real caller. Start by listing exactly
+   which source or kernel information the caller retains at its next cut.
+   Caller lifetimes and a complete paid bill are required before comparing routes.
+
+## Credit and provenance
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Credit Ali Romman #5821 for the explicit open question and image-information
+theorem; Dugongue #5815 for the Smith circuit and Gaussian correction context;
+and the classical finite-ring cardinality and reversible-embedding arguments.
+The Gaussian/native/controller/compiler lineage retained by those sources,
+including Cinna Davis, Cao Yifan and the credited predecessor contributors,
+remains theirs. Their files and credit lines are unchanged.
+
+The exact predecessor heads are recorded in [PROOF.md](PROOF.md) and
+[TASK.json](TASK.json). They are literature references, not runtime dependencies.
+[SOURCES.json](SOURCES.json) pins the task catalogue and selected-record
+provenance at main `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8.
+Live overlap checks included the handoff board, open PRs, this account's recent
+PRs, concurrent reservations, exact main-text searches and merged-PR searches.
+The cached helper searched 426 open PRs and 5,331 discussion records; its sparse
+local notes covered 200 of 7,845 paths. Direct Git searches supplemented that
+incomplete local coverage. No global literature-priority claim follows.

research/gaussian-smith-reversible-capacity/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "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"
+    }
+  ]
+}

research/gaussian-smith-reversible-capacity/TASK.json

@@ -0,0 +1,118 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?",
+    "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"
+    ],
+    "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": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "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": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "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": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "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": "Sharp initially clean bit capacity and attaining reversible permutation for destructive raw Gaussian tensor overwrite, with arbitrary finite dirty workspace.",
+  "scope_change_reason": "The user requests a new result rather than an audit. Answer PR5821 README Open next question 4 at the successor modular overwrite interface; do not claim to discharge a selected assumption.",
+  "bottleneck_link": "A source-preserving array reset does not supply a reversible destructive overwrite. The result prices the lost-information capacity exactly and identifies when retained source information is necessary; native and tape costs remain open.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship this first sharp scoped capacity theorem and attaining interface once bounded local package and publication checks pass; do not extend to a physical implementation.",
+  "outcome": "completed",
+  "evidence": "Written lower bound and explicit all-state inverse; generated source-bound stdout receipt from normal/optimized finite replay. No predecessor image census is rerun.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Implement the attaining permutation on a permitted reversible native/tape host.",
+      "why_it_matters": "Logical clean capacity does not bound physical operations or movement.",
+      "first_step": "Implement and price the one-axis chart and bit permutation.",
+      "blocked_by": "Physical gate alphabet, representation and tape contract."
+    },
+    {
+      "question": "Compare source-preserving cleanup with destructive overwrite plus retained kernel data at one real caller.",
+      "why_it_matters": "These interfaces retain different information and cannot share a cleanup invoice without justification.",
+      "first_step": "List the caller source/kernel information and lifetimes at its next cut.",
+      "blocked_by": "Actual caller schedule and complete paid-operation bill."
+    }
+  ],
+  "predecessors": [
+    {
+      "pr": 5821,
+      "author": "Ali Romman",
+      "head": "c137f338117e8a88816ce254efe3b1494809711f",
+      "role": "README Open next question 4 and cited response-image theorem",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5821"
+    },
+    {
+      "pr": 5815,
+      "author": "Dugongue",
+      "head": "f0fcda576df410dc15cd5b8183d4f74d284eba2b",
+      "role": "Cited Gaussian Smith factorization and retained construction lineage",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5815"
+    }
+  ],
+  "overlap": {
+    "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19214971",
+    "checked_at_utc": "2026-10-27T10:38:47Z",
+    "source": "PR #5821",
+    "scope": "Live handoffs and open PRs; recent own PRs; concurrent reservations; main text and merged title/body searches. Sparse helper local coverage is incomplete.",
+    "open_related_prs": [
+      5813,
+      5815,
+      5821,
+      5825,
+      5780
+    ]
+  }
+}