PhysicsState
plain-language theorem explainer
The minimal recognition-state skeleton indexed by identity ticks supplies the carrier for physics realizations of the forcing chain. Researchers constructing the stable interface for Universal Forcing cite this definition when building tick arithmetic interpretations. It is introduced by a direct structure declaration with a single field and decidable equality.
Claim. A recognition state in the physics realization consists of an element of the logic natural numbers (the smallest subset of positive reals closed under multiplication by the generator and containing the multiplicative identity), equipped with decidable equality.
background
This module supplies a lightweight hook for realizing physics within the Universal Forcing framework. Identity ticks act as the step action, recognition states serve as the carrier, and equality cost provides the minimal realization of physical tick arithmetic. The fundamental time quantum is one tick, denoted τ₀.
proof idea
The declaration is a direct structure definition introducing the tick field of type the logic natural numbers and deriving decidable equality. No lemmas or tactics are applied.
why it matters
This definition provides the carrier for downstream constructions including the equality cost function on states, the interpretation map from logic natural numbers to states, and the full physics realization object. It realizes the minimal skeleton for identity-tick states in the forcing chain, supporting faithful arithmetic interpretations. It connects to the fundamental time quantum in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.