PhysicsState
plain-language theorem explainer
PhysicsState supplies the carrier type for minimal recognition states in the physics realization, consisting of a single LogicNat tick field with decidable equality. Researchers constructing the lightweight physics forcing hook cite it as the state space for interpreting arithmetic orbits via identity ticks. The definition is a direct structure declaration with no proof obligations or additional axioms.
Claim. Let PhysicsState be the structure whose sole field is a LogicNat tick, where LogicNat is the inductive type of naturals forced by the Law of Logic (with identity as the zero-cost element and step as generator iteration), equipped with decidable equality.
background
The module supplies a stable interface for physics realizations under Universal Forcing by taking identity ticks as the step action and recognition states as the carrier, with equality cost as the minimal realization of physical tick arithmetic. LogicNat is the inductive type whose constructors identity and step mirror the multiplicative orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by the generator and containing 1. The constant tick is the fundamental RS-native time quantum τ₀ set to 1.
proof idea
The declaration is a direct structure definition. It introduces the type with one field of type LogicNat and derives DecidableEq, requiring no lemmas, tactics, or computational reduction.
why it matters
PhysicsState provides the carrier for the downstream physicsRealization instance of LogicRealization and for physicsCost (0 on equality, 1 otherwise). It anchors physics_faithful (injective interpretation) and physicsInterpret. In the Recognition Science framework it realizes the identity-tick step action inside the T0-T8 forcing chain, supplying the minimal state space for the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.