NativeSerialImage

Abstract

NativeSerialImage

Theorem 1.1 (Prefix-free terminal reply words).

$$\forall C,O:Type,(\forall delta:C\to \mathrm{Op}\left(C,O\right),(\forall c:C,(\forall N:Nat,(\forall u,v:Source,(\forall t,s:Trace,(\forall o,p:O,((\mathrm{Run}\left(delta,c,N,u,t,o\right))⟹((\mathrm{Run}\left(delta,c,N,v,s,p\right))⟹((\mathrm{IsPrefix}\left(\mathrm{answers}\left(t\right),\mathrm{answers}\left(s\right)\right))⟹((t=s)\wedge (o=p)))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/NativeSerialImage.terminal_prefix_free (✓ std3). ∎

Source. Repository-derived.

Commentary.

A terminal reply word cannot be a proper prefix of another terminal word for the same source-free control and initial epoch. A prefix relation forces equality of the entire physical action traces and complete outputs, including every silent step and update.

Definition 1.2 (Fixed-length reply padding).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/NativeSerialImage.pad

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeSerialImage.pad (✓ std3).

Source. Repository-derived.

Commentary.

Pad a bounded terminal reply word with absent symbols to length K. This is a proof construction on words, not a physical register operation. Prefix-freeness makes the padding injective on actual terminal words.

Theorem 1.3 (Sharp whole-output image bound).

$$\forall C,O:Type,(\forall delta:C\to \mathrm{Op}\left(C,O\right),(\forall c:C,(\forall N,K:Nat,(\forall U:\mathrm{Set}\left(Source\right),((\mathrm{Nonempty}\left(U\right))⟹(\forall F:Source\to O,((\forall u:Source,((u\in U)⟹(\exists t:Trace,((\mathrm{Run}\left(delta,c,N,\mathrm{iterate}\left(substitution,N,u\right),t,F\left(u\right)\right))\wedge (\mathrm{length}\left(\mathrm{answers}\left(t\right)\right)\le K)))))⟹(\exists labels:\mathrm{Finset}\left(O\right),((\mathrm{card}\left(labels\right)\le \mathrm{power}\left(4,K\right))\wedge (\forall u:Source,((u\in U)⟹(F\left(u\right)\in labels))))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/NativeSerialImage.bounded_serial_output_image (✓ std3). ∎

Source. Repository-derived.

Commentary.

The terminal words inject into the length-K four-valued words. The entire terminal output image therefore lies in a finite set of cardinality at most four to the power K. K equal to zero is included; repeated reads are counted separately. No finite source or output universe and no uniform runtime hypothesis is used.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeSerialImage.bounded_serial_output_image
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeSerialImage.pad
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeSerialImage.terminal_prefix_free
• Dependency: D5/S3/Arith/FibonacciAtomic/Observer/NativeSerialMachine