tickStep
plain-language theorem explainer
The definition supplies the successor operation on physics states by advancing the tick index one step in the LogicNat orbit. Researchers constructing discrete-time models in the Recognition Science framework cite it when realizing the physics carrier from the logic structure. It is realized as a direct one-line wrapper applying the succ constructor to the tick field of the input state.
Claim. Let $x$ be a physics state whose tick component is an element $n$ of LogicNat. Then tickStep$(x)$ is the physics state whose tick component is succ$(n)$, where succ is the step constructor that adds one iteration of the generator.
background
PhysicsState is the structure carrying a single tick field of type LogicNat, serving as the minimal recognition-state skeleton indexed by identity ticks. LogicNat is the inductive type with constructors identity (the zero-cost multiplicative identity) and step, forming the smallest orbit closed under the generator. The module provides a stable lightweight interface for the universal forcing chain, realizing physical tick arithmetic via identity ticks as the step action and equality cost as the minimal carrier.
proof idea
One-line wrapper that applies ArithmeticFromLogic.LogicNat.succ to the tick field of the input PhysicsState and repackages the result as a new PhysicsState.
why it matters
This definition supplies the successor needed by the downstream physicsRealization skeleton, which sets the carrier to PhysicsState and the zero element via LogicNat.zero. It completes the identity-tick step action in the foundation module, enabling the minimal realization of physical tick arithmetic without pulling in fragile modules from the full forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.