Internal zeros and literal seam safety

Abstract

A zero inside each complete word controls the inherited run across its next seam.

Theorem 1.1 (Internal zero execution).

$$\forall k\in \mathbb{N},\forall m\in \mathbb{N},\forall w\in \mathrm{Fin}\left(m\right)\to Bool,\forall i\in \mathrm{Fin}\left(m\right),\forall v\in \mathrm{ZMod}\left(2\right),\forall phase\in \mathrm{ZMod}\left(k+1\right),\forall s\in \mathbb{N},\left(\left(\left(\left(2\le k\wedge m<k\right)\wedge w\left(i\right)=false\right)\wedge s<k\right)\wedge \left(s+\mathrm{val}\left(i\right)<k\vee w\left(⟨0{⟩}_m\right)=false\right)\right)\Rightarrow \left(\mathrm{runBits}\left(k,w,\mathrm{some}\left(⟨v,phase,s⟩\right)\right)=\mathrm{some}\left(⟨v+\mathrm{wordIncrement}\left(k,phase,w\right),phase+m,\mathrm{tailAfter}\left(0,w\right)⟩\right)\wedge \mathrm{tailAfter}\left(0,w\right)\le m-1-\mathrm{val}\left(i\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/InternalZeroSafety.internal_zero_execution (✓ std3). ∎

Source. Repository-derived.

Commentary.

The word has m<k bits and a marked zero at position i. If the incoming tail plus i is below k, every bit before that mark is safe. Alternatively a zero at the first position clears any legal inherited tail. The marked zero makes the terminal tail independent of the incoming tail and bounds it by m-1-i. The scalar and phase are those of the original literal executor. The bound uses the mark, so later seams may have two adjacent one bits. It does not require a zero at either block boundary.

Subtraction in the tail bound is natural subtraction. The index i:Fin(m) already implies m>0. Only the complete endpoint is observed; the internal zero is a literal bit of the paid word.

Theorem 1.2 (One common literal suffix).

$$\forall k\in \mathbb{N},\forall m\in \mathbb{N},\forall alphabet\in Bool,\forall marked\in \mathrm{List}\left((\mathbb{N}\to \mathrm{ZMod}\left(2\right))\times \mathrm{Fin}\left(m\right)\right),\forall v\in \mathrm{ZMod}\left(2\right),\forall j\in \mathrm{ZMod}\left(k+1\right),\forall s\in \mathbb{N},\left(\left(\left(\left(\left(\left(\left(\left(3\le k\wedge 1\le m\right)\wedge m<k\right)\wedge \left(\forall e\in (\mathbb{N}\to \mathrm{ZMod}\left(2\right))\times \mathrm{Fin}\left(m\right),e\in marked\Rightarrow \sum _{h\in \mathrm{range}\left(m+1\right)}\mathrm{row}\left(e\right)\left(h\right)=0\right)\right)\wedge \left(\forall e\in (\mathbb{N}\to \mathrm{ZMod}\left(2\right))\times \mathrm{Fin}\left(m\right),e\in marked\Rightarrow \mathrm{prefixWord}\left(m,\mathrm{row}\left(e\right)\right)\left(\mathrm{second}\left(e\right)\right)=false\right)\right)\wedge \mathrm{IsChain}\left((\lambda (a:(\mathbb{N}\to \mathrm{ZMod}\left(2\right))\times \mathrm{Fin}\left(m\right)),(\lambda (b:(\mathbb{N}\to \mathrm{ZMod}\left(2\right))\times \mathrm{Fin}\left(m\right)),m+\mathrm{mark}\left(b\right)\le k+\mathrm{mark}\left(a\right))),marked\right)\right)\wedge s<k\right)\wedge \left(\forall e\in (\mathbb{N}\to \mathrm{ZMod}\left(2\right))\times \mathrm{Fin}\left(m\right),e\in \mathrm{headOption}\left(marked\right)\Rightarrow \left(s+\mathrm{mark}\left(e\right)<k\vee \mathrm{row}\left(e\right)\left(0\right)=0\right)\right)\right)\wedge \gcd \left(m,k+1\right)\mid \mathrm{val}\left(-j\right)\right)\Rightarrow \left(\left(\left(\left(\mathrm{length}\left(\mathrm{chargeBlocks}\left(k,m,alphabet,\mathrm{mapFirst}\left(marked\right)\right)\right)=\mathrm{length}\left(marked\right)\wedge \mathrm{fixedBlockArchive}\left(\mathrm{chargeBlocks}\left(k,m,alphabet,\mathrm{mapFirst}\left(marked\right)\right),\mathrm{some}\left(⟨v,-j,s⟩\right)\right)=\mathrm{chargeArchive}\left(k,m,\mathrm{mapFirst}\left(marked\right),v,j\right)\right)\wedge \mathrm{length}\left(\mathrm{fixedBlockArchive}\left(\mathrm{chargeBlocks}\left(k,m,alphabet,\mathrm{mapFirst}\left(marked\right)\right),\mathrm{some}\left(⟨v,-j,s⟩\right)\right)\right)=\mathrm{length}\left(marked\right)\right)\wedge \left(\neg none\in \mathrm{fixedBlockArchive}\left(\mathrm{chargeBlocks}\left(k,m,alphabet,\mathrm{mapFirst}\left(marked\right)\right),\mathrm{some}\left(⟨v,-j,s⟩\right)\right)\right)\right)\wedge \left(\exists N\in \mathbb{N},\exists source\in \mathrm{Fin}\left(N\right)\to Bool,\left(\left(\left(\left(\left(m\mid N\wedge \mathrm{DBonacciAdmissible}\left(k,N,source\right)\right)\wedge \mathrm{runBits}\left(k,source,\mathrm{some}\left(⟨0,0,0⟩\right)\right)=\mathrm{some}\left(⟨v,-j,s⟩\right)\right)\wedge \mathrm{originalWordValue}\left(k,source\right)=v\right)\wedge \mathrm{tailAfter}\left(0,source\right)=s\right)\wedge \left(\forall b\in \mathbb{N},\left(b+1\right)\cdot m\le N\Rightarrow \mathrm{DBonacciAdmissible}\left(k,m,(\lambda (i:\mathrm{Fin}\left(m\right)),source\left(⟨b\cdot m+\mathrm{val}\left(i\right){⟩}_N\right))\right)\right)\right)\wedge \mathrm{fixedBlockArchive}\left(\mathrm{chargeBlocks}\left(k,m,alphabet,\mathrm{mapFirst}\left(marked\right)\right),\mathrm{runBits}\left(k,source,\mathrm{some}\left(⟨0,0,0⟩\right)\right)\right)=\mathrm{chargeArchive}\left(k,m,\mathrm{mapFirst}\left(marked\right),v,j\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/InternalZeroSafety.actual_internal_zero_charge_suffix (✓ std3). ∎

Source. Repository-derived.

Commentary.

An entry is a pair consisting of an ordered charge row and a marked Fin(m) position. Here row(e) is its first projection, second(e) its second projection, mark(e) the natural value of that position, and mapFirst(marked)=marked.map(Prod.fst). chargeBlocks omits the proof arguments 2<=k and m<k in the display. IsChain applies the displayed relation only to consecutive entries. headOption denotes List.head?.

Every row is even and its prefix-parity word is zero at the marked position. For adjacent marks a,b the gap bound m+mark(b)<=k+mark(a) makes the outgoing tail from a safe up to b. The first word also satisfies the stated incoming condition. Thus the one common list of words gives exactly chargeArchive, with one completed live reading for every issued block. Its relative phase changes by minus m each time, so the charge windows follow their actual chronology.

The source witness realizes the value, phase and inherited tail jointly using original weights and legal complete history blocks. The same suffix works in either alphabet. This uses D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/LiteralModel and the row inverse in D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/WindowChargeInverse. The theorem supplies physical safety and the whole archive. It does not construct the charge rows, distinguish phase labels, synthesize stopping or decoding, or establish an adaptive-to-preset price inequality.

References

• Truth anchor: D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/InternalZeroSafety.actual_internal_zero_charge_suffix
• Truth anchor: D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/InternalZeroSafety.internal_zero_execution
• Dependency: D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/WindowChargeInverse
• Narrative reference: D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/LiteralModel
• Narrative reference: D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/WindowChargeInverse