Finite Runtime Reduction with Online State Extension

Abstract

A fixed finite-precision runtime is finite, and online learning requires an expanded state.

Theorem 1.1 (Finite-precision runtime reduction with online state extension).

$$\forall C,K,R,M,S,O,Theta,Optimizer:\mathrm{Type},[\mathrm{Fintype}(C)],[\mathrm{Fintype}(K)],[\mathrm{Fintype}(R)],[\mathrm{Fintype}(M)],[\mathrm{Fintype}(S)],[\mathrm{Finite}(O)],[\mathrm{Fintype}(Theta)],[\mathrm{Fintype}(Optimizer)],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),onlineUpdate:\mathrm{LearningState}(C,K,R,M,S,Theta,Optimizer)\to \mathrm{LearningState}(C,K,R,M,S,Theta,Optimizer),onlineReadout:\mathrm{LearningState}(C,K,R,M,S,Theta,Optimizer)\to O,\exists system:\mathrm{ObservationSystem}(\mathrm{RuntimeState}(C,K,R,M,S),O),\mathrm{transition}(system)=\mathrm{Apply}(update,theta)\wedge \mathrm{readout}(system)=\mathrm{Apply}(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 (\mathrm{onlineLearningOccurred}(onlineUpdate,onlineReadout)\Rightarrow ((\exists onlineSystem:\mathrm{ObservationSystem}(\mathrm{LearningState}(C,K,R,M,S,Theta,Optimizer),O),\mathrm{transition}(onlineSystem)=onlineUpdate\wedge \mathrm{readout}(onlineSystem)=onlineReadout\wedge \mathrm{card}(\mathrm{LearningState}(C,K,R,M,S,Theta,Optimizer))=\mathrm{card}(\mathrm{RuntimeState}(C,K,R,M,S))\times \mathrm{card}(Theta)\times \mathrm{card}(Optimizer)\wedge \exists state,(onlineUpdate(state).2.1\ne state.2.1\vee onlineUpdate(state).2.2\ne state.2.2))\wedge \neg \exists fixedReadout:\mathrm{RuntimeState}(C,K,R,M,S)\to O,\forall state,fixedReadout(state.1)=onlineReadout(state))).$$

Proof. Machine-checked in Lean as D5/S3/QuantumStates/FiniteRuntimeReductionOnline.finite_precision_runtime_reduction_online (✓ 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; no uncounted input appears in either function’s domain.

The public conclusion includes the exact product cardinality and the injective b-bit parameter bound. Its online clause constructs the expanded runtime state, records an actual parameter or optimizer mutation, and rules out collapse to a fixed runtime when that mutation changes the readout against frozen old values.

Repository search found no exact packaged theorem. 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/FiniteRuntimeReductionOnline.finite_precision_runtime_reduction_online