Finite original events and paused frame copies

Abstract

RarePriorLiteralController.EventFrames

The event representation records finite completion indices and preserves the original event block. Copy checkpoints specify every residual instruction cut, so frame decoding and lawful history replay refer to the same original fields and operations.

Theorem 1.1 (Exact original six-slot ROM).

$$\forall (f:\mathrm{FiniteFields}),\forall (\mathrm{op}:\mathrm{Operation}),(((\mathrm{eventBlock}(f,\mathrm{op})).\mathrm{length}\le 6)\wedge (((\forall (i:\mathbb{N}),\forall (b:\mathrm{Letter}),\mathrm{OriginalEvent}.\mathrm{completed}(i,b)\in \mathrm{eventBlock}(f,\mathrm{op})⟹i<4)\wedge (\mathrm{List}.\mathrm{map}(\mathrm{original},\mathrm{List}.\mathrm{filterMap}(\mathrm{id},\mathrm{List}.\mathrm{ofFn}(\mathrm{eventROM}(f,\mathrm{op}))))=\mathrm{eventBlock}(f,\mathrm{op})))))$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/EventFrames.six_slot_original_events (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every finite field state and operation, the original block has at most six events, every emitted completion index is below four, and the embedded present ROM slots equal that exact block.

Theorem 1.2 (Every paused tape transfer).

$$\forall (w:\mathbb{N}),\forall (\mathrm{rom}:\mathrm{Fin}(w)\to \mathrm{Bool}),((\forall (m:\mathbb{N}),\forall (\mathrm{hm}:m\le w),\forall (r:\mathbb{N}),((\mathrm{copyRun}(\mathrm{rom},\mathrm{copyEntry}(w),4\ast m+r)=\mathrm{copyRun}(\mathrm{rom},\mathrm{copyCheckpoint}(\mathrm{rom},m,\mathrm{hm}),r))\wedge (\mathrm{copyTrace}(\mathrm{rom},\mathrm{copyEntry}(w),4\ast m+r)=\mathrm{List}.\mathrm{ofFn}((\mathrm{fun}i:\mathrm{Fin}(m)\mapsto \mathrm{rom}(\mathrm{Fin}.\mathrm{castLE}(\mathrm{hm},i))))++\mathrm{copyTrace}(\mathrm{rom},\mathrm{copyCheckpoint}(\mathrm{rom},m,\mathrm{hm}),r))))\wedge ((((\mathrm{copyRun}(\mathrm{rom},\mathrm{copyEntry}(w),4\ast w)).\mathrm{tape}=\mathrm{rom})\wedge (\forall (n:\mathbb{N}),\mathrm{copyRun}(\mathrm{rom},\mathrm{copyEntry}(w),4\ast w+1+n)=\{\mathrm{copyCheckpoint}(\mathrm{rom},w,{\mathrm{le}}_{\mathrm{rfl}})\mathrm{with}\mathrm{pc}:=\mathrm{CopyPC}.\mathrm{halt}\}))))$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/EventFrames.paused_copy_refinement (✓ std3). ∎

Source. Repository-derived.

Commentary.

After m complete four-instruction transfers, all subsequent internal states and observations equal execution from the exact prefix checkpoint. At the full width the scratch equals the ROM, and the exhausted instruction halts permanently.

Theorem 1.3 (Current original frame output).

$$\forall (f:\mathrm{FiniteFields}),\forall (\mathrm{op}:\mathrm{Operation}),((\forall (\mathrm{slot}:\mathrm{Fin}(6)),((\mathrm{copyTrace}(\mathrm{frameTape}(\mathrm{eventROM}(f,\mathrm{op},\mathrm{slot})),\mathrm{renderFrame},4\ast \mathrm{frameWidth})=\mathrm{bitCode}(\mathrm{frameCodec}(\mathrm{eventROM}(f,\mathrm{op},\mathrm{slot}))))\wedge ((\mathrm{frameRun}(f,\mathrm{op},\mathrm{slot},4\ast \mathrm{frameWidth})).\mathrm{tape}=\mathrm{frameTape}(\mathrm{eventROM}(f,\mathrm{op},\mathrm{slot})))))\wedge (\mathrm{List}.\mathrm{map}(\mathrm{original},\mathrm{List}.\mathrm{filterMap}(\mathrm{id},\mathrm{List}.\mathrm{ofFn}((\mathrm{fun}\mathrm{slot}:\mathrm{Fin}(6)\mapsto \mathrm{decodeFrame}(\mathrm{copyTrace}(\mathrm{frameTape}(\mathrm{eventROM}(f,\mathrm{op},\mathrm{slot})),\mathrm{renderFrame},4\ast \mathrm{frameWidth}))))))=\mathrm{eventBlock}(f,\mathrm{op})))$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/EventFrames.streamed_original_events (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each actual copy trace emits the complete code of its selected finite frame and retains that tape. Decoding the six external frame traces gives exactly the original event block.

Theorem 1.4 (Charged installation and current frames).

$$\forall (s:\mathrm{RenderSnapshot}),((\mathrm{Function}.\mathrm{Injective}(\mathrm{snapshot}))\wedge (((\forall (q:\mathrm{RenderSnapshot}),(\mathrm{programImage}).\mathrm{length}+(\mathrm{snapshot}(q)).\mathrm{length}<\mathrm{rendererBound})\wedge (((\mathrm{installed}(s)=(\mathrm{installStep}{)}^{[4\ast \mathrm{programWidth}]}\{s\mathrm{with}\mathrm{installation}:=\mathrm{copyEntry}(\mathrm{programWidth})\})\wedge ((((((\mathrm{installStep}{)}^{[4\ast \mathrm{programWidth}]}\{s\mathrm{with}\mathrm{installation}:=\mathrm{copyEntry}(\mathrm{programWidth})\}).\mathrm{installation}).\mathrm{tape}=\mathrm{programTape})\wedge (((\forall (\mathrm{slot}:\mathrm{Fin}(6)),\forall (m:\mathbb{N}),\forall (\mathrm{hm}:m\le \mathrm{frameWidth}),\forall (r:\mathbb{N}),((\mathrm{frameStep}(\mathrm{slot}){)}^{[4\ast m+r]}\{\mathrm{installed}(s)\mathrm{with}\mathrm{frame}:=\mathrm{renderFrame}\}).\mathrm{frame}=\mathrm{copyRun}(\mathrm{frameTape}(\mathrm{eventROM}((((s).\mathrm{retained}).\mathrm{pre}).\mathrm{fields},((s).\mathrm{retained}).\mathrm{operation},\mathrm{slot})),\mathrm{copyCheckpoint}(\mathrm{frameTape}(\mathrm{eventROM}((((s).\mathrm{retained}).\mathrm{pre}).\mathrm{fields},((s).\mathrm{retained}).\mathrm{operation},\mathrm{slot})),m,\mathrm{hm}),r))\wedge (\mathrm{List}.\mathrm{map}(\mathrm{original},\mathrm{List}.\mathrm{filterMap}(\mathrm{id},\mathrm{List}.\mathrm{ofFn}((\mathrm{fun}\mathrm{slot}:\mathrm{Fin}(6)\mapsto \mathrm{decodeFrame}(\mathrm{copyTrace}(\mathrm{installedFrameROM}(\mathrm{installed}(s),\mathrm{slot}),\mathrm{renderFrame},4\ast \mathrm{frameWidth}))))))=\mathrm{eventBlock}((((s).\mathrm{retained}).\mathrm{pre}).\mathrm{fields},((s).\mathrm{retained}).\mathrm{operation})))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/EventFrames.charged_installed_frames (✓ std3). ∎

Source. Repository-derived.

Commentary.

The complete snapshot encoding is injective and every value fits the fixed budget. The loader installs the actual image tape. Current-frame instructions read that installed image, satisfy the paused invariant with retained context and emit the exact original block under finite macro addressing.

Theorem 1.5 (Original source-history replay).

$$\forall (c:\mathrm{AcquiredNativeState}),\forall (d:\mathrm{AcquiredNativeState}),\forall (\mathrm{omega}:\mathrm{Stream}),\forall (n:\mathbb{N}),\forall (k:\mathbb{N}),\forall (\mathrm{ops}:\mathrm{List}(\mathrm{Operation})),\mathrm{nativeDrive}(c,\mathrm{omega},n)=\mathrm{some}((\mathrm{ops},d,k))⟹((\mathrm{fullTranscript}(c,\mathrm{omega},n)=\mathrm{some}((\mathrm{ops},((d).\mathrm{source}).\mathrm{finiteFields},\mathrm{streamedBlocks}(((c).\mathrm{source}).\mathrm{finiteFields},\mathrm{ops}))))\wedge (\mathrm{List}.\mathrm{foldl}(\mathrm{replayBlock},((c).\mathrm{source}).\mathrm{finiteFields},\mathrm{streamedBlocks}(((c).\mathrm{source}).\mathrm{finiteFields},\mathrm{ops}))=((d).\mathrm{source}).\mathrm{finiteFields}))$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/EventFrames.streamed_original_history (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every lawful nativeDrive prefix, the streamed frame blocks reconstruct the original full output and replay to its actual finite fields. The operations and iteration indices are external proof coordinates, not retained machine inputs.

References

• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/EventFrames.charged_installed_frames
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/EventFrames.paused_copy_refinement
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/EventFrames.six_slot_original_events
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/EventFrames.streamed_original_events
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/EventFrames.streamed_original_history
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeFullResidual
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorResidentCode
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorSerialExecution