[petalas]

Summary

Scoped algebraic proof with exact finite corroboration: frozen live snapshots of rational rank r can remove at most r dyadic unit channels. Every permitted loss is attained while rational pairing rank stays unchanged.

D = Z[1/2]
Q = full saturated D-basis of ker(C)
c_C(K) = max { t : X K Y = I_t, C Y = 0 } = c(K Q)
max(0,c(K)-rank_Q(C)) <= c_C(K) <= c(K)

K = [1 0], C = [1 3]
unconstrained capacity 1; constrained capacity 0; rational pairing rank 1

This supplies the frozen-copy insertion restriction and its sharp envelope. Credit woklerx / #1437 for the chronological snapshot condition and Ali Romman / #5615 for unconstrained dyadic unit capacity, with their retained R439/helper/native lineage. Their results are cited rather than audited or replayed. Saturation, Smith reduction and module splitting are classical. This contribution was produced by Nick Petalas. No new kappa or selected-frontier change is claimed.

Evidence

• Before: positive rational pairing rank and an eventual identity endpoint do not establish an admissible dyadic insertion preserving a live copied value. After: the proof gives the exact constrained pairing, sharp all-size loss bound, attaining family and an eight-ADD arbitrary-dirty realization at its declared comparison boundaries.
• Exact finite checks pass for 4,096 one-snapshot pairs and 6,561 two-snapshot pairs. In the first domain, 2,100 pairs lose capacity and 108 retain rational pairing rank. All 69 sharp fixtures, 343 dirty inputs, 2,744 literal ADD updates and eleven controls pass.
• Warning-strict normal and optimized direct runs pass on CPython 3.12.15, with identical complete stdout. The two registered checks took 0.632 and 0.632 seconds locally, below their separate 120-second limits. These timings establish timeout headroom, not a performance comparison.
• Registered replay, metadata/source pins, whitespace and exact committed-byte/source-history checks pass at d4ccb392103ab3ec89228a6fec99251a3cc19e75. The generated stdout receipt binds results to every package file hash. No receipt was hand-written.

Reproduce from the worktree root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/frozen-snapshot-channel-capacity/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/frozen-snapshot-channel-capacity/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/frozen-snapshot-channel-capacity
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/frozen-snapshot-channel-capacity --check-source-history

Any CPython 3.12 interpreter may replace the local path. The standard-library verifier writes no files. Expected markers are PASS_FROZEN_SNAPSHOT_CHANNEL_CAPACITY, PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES.

Limitations and unrun obligations

This freezes copied slots and restricts additive insertion directions in fixed eligible modules. It does not classify arbitrary helper/snapshot rebasing or supply a physical P104 split. No source-bound physical L0,R0,S, carrier, native chart, productive target, copy tariff, basis-synthesis invoice, complete consumer or supplier admission is supplied. Dirty cancellation, intermediate comparison legality, growth, precision/tape, compiler and outer obligations remain. The finite census is exactly the stated integer domain; the arbitrary-size dyadic theorem has a written proof using the cited capacity criterion.

Selected cold replay, Lean, Docker, independent human review and formal proof-kernel validation are unrun or unclaimed. The five selected framework assumptions retain their status.

Open next questions

1. Extract L0,R0 and every unchanged snapshot map S for one nominated physical live cut, then compute the saturated kernel of S R0. A concrete changed word and its eligible modules are missing here.
2. Specify a legal copied-slot update and inverse that escape the restriction, with all COPY/ERASE, native and target charges. A complete producer/consumer and tariff are missing here.

Related open work

• Prove sharp one-channel capacity change for paired cut edits (no κ) #6462 studies the same dyadic unit-capacity quantity under a paired prefix ADD and inverse suffix update. This instead holds the pairing fixed and restricts insertion directions by frozen snapshot equations. No common physical instance is computed or compared.
• Conditional κ = 0.003287014 (+1.65e-7 over #6417): a third group-1091 anchor on the clean mixed root #6453 changes an actual P104 helper trajectory and mixed-root invoice. This proof supplies no edit or kappa value for that word and does not validate its construction.
• Conditional κ = 0.00328637739144124222748802 (+1.626e-7 over #6398): a third group-1091 anchor #6436 studies another actual P104 anchor and paid/target invoice. This provides a live-boundary screening lemma without computing that invoice or its reported saving.

The completion refresh inspected all twelve other open account PRs created since the advance CLAIM. PR6462 studies the same unit-capacity quantity and is listed above; none of the other inspected submissions computes this frozen-snapshot contract or a conflicting common value. No extra computations audited another contribution. Historical sparse notes and unpublished work remain overlap limits.

CI notes

Both hosted checks passed at exact head d4ccb392103ab3ec89228a6fec99251a3cc19e75 in run 41550752751: plan and replay (research/frozen-snapshot-channel-capacity). The completed checks were read once and both report pass; the PR has the matching head.

Hosted replay certifies execution of the two registered normal and optimized finite checks at this commit. All local checks listed above also passed. This does not supply independent human or formal proof-kernel acceptance of the universal written proof or discharge the physical/supplier obligations. No CI failure remains.

Advance CLAIM.

Merge Danger

Door: two-way.

Blast radius: isolated. Five new files in one opt-in research package. Shared code, frozen sources and selected-result records are unchanged.