Finite-Precision Runtime Reduction

Abstract

A fixed finite-precision runtime is a finite deterministic observation system.

Theorem 1.1 (Finite-precision runtime reduction).

$$\forall C,K,R,M,S,O,Theta,External:\mathrm{Type},[\mathrm{Fintype}(C)],[\mathrm{Fintype}(K)],[\mathrm{Fintype}(R)],[\mathrm{Fintype}(M)],[\mathrm{Fintype}(S)],[\mathrm{Fintype}(O)],[\mathrm{Fintype}(Theta)],[\mathrm{IsEmpty}(External)],theta:Theta,update:Theta\to \mathrm{RuntimeState}(C,K,R,M,S)\to \mathrm{RuntimeState}(C,K,R,M,S),readout:Theta\to \mathrm{RuntimeState}(C,K,R,M,S)\to O,Nb:\mathbb{N},parameterEncoding:Theta\to \mathrm{ParameterSlots}(N,b),hParameterInjective:\mathrm{Injective}(parameterEncoding),onlineLearning:Prop,\exists system:\mathrm{ObservationSystem}(\mathrm{RuntimeState}(C,K,R,M,S),O),\mathrm{transition}(system)=update(theta)\wedge \mathrm{readout}(system)=readout(theta)\wedge \mathrm{card}(\mathrm{RuntimeState}(C,K,R,M,S))=\mathrm{card}(C)\times \mathrm{card}(K)\times \mathrm{card}(R)\times \mathrm{card}(M)\times \mathrm{card}(S)\wedge \mathrm{card}(Theta)\le 2^{b\times N}\wedge (onlineLearning\Rightarrow \forall Optimizer:\mathrm{Type}[\mathrm{Fintype}(Optimizer)],\mathrm{card}(\mathrm{Prod}(\mathrm{Prod}(\mathrm{RuntimeState}(C,K,R,M,S),Theta),Optimizer))=\mathrm{card}(\mathrm{RuntimeState}(C,K,R,M,S))\times \mathrm{card}(Theta)\times \mathrm{card}(Optimizer)).$$

Proof. Machine-checked in Lean as D5/S3/QuantumStates/FiniteRuntimeReduction.finite_precision_runtime_reduction (✓ std3). ∎

Source. Repository-derived.

Commentary.

The complete runtime state is constructed as the product of the five finite source components C, K, R, M, and S. Fixed parameters make the update and readout deterministic maps on that product, while the empty external-input type records the absence of uncounted inputs.

The public conclusion includes the exact product cardinality, an injective b-bit encoding bound for N parameter slots, and the expanded product cardinality when online learning carries parameters and optimizer state.

Repository search found no packaged theorem with this complete reduction. Pinned Mathlib supplies and is applied through Fintype.card_prod, Fintype.card_fun, Fintype.card_fin, and Fintype.card_le_of_injective.

References

• Truth anchor: D5/S3/QuantumStates/FiniteRuntimeReduction.finite_precision_runtime_reduction