physicsRealization
plain-language theorem explainer
physicsRealization supplies the concrete LogicRealization instance whose carrier is the set of tick-indexed physics states and whose orbit is the logic naturals. Workers on the universal forcing chain cite it to obtain a minimal stable physics tick model that sidesteps fragile imports. The body is a direct record construction that delegates axioms to ArithmeticFromLogic lemmas and local cost functions.
Claim. Let LogicRealization be the structure whose fields include Carrier, Cost, compare, zero, step, Orbit, interpret, and the listed axioms. Then physicsRealization is the instance with Carrier equal to the set of physics states (tick-indexed recognition states), Cost equal to the naturals, compare equal to the equality cost on states, step equal to the tick step, Orbit equal to the logic naturals, interpret equal to the physics interpretation map, and the remaining axioms satisfied by reflexivity or by the corresponding lemmas on logic naturals.
background
PhysicsState is the minimal recognition-state skeleton indexed by identity ticks. LogicNat is the inductive type forced by the Law of Logic, with constructors identity (zero-cost element) and step (one more iteration of the generator), mirroring the orbit closed under multiplication by the generator and containing the multiplicative identity. The module supplies a lightweight physics realization hook for Universal Forcing that uses identity ticks as the step action and equality cost as the minimal realization of physical tick arithmetic.
proof idea
The definition constructs the LogicRealization record by direct field assignment: Carrier to PhysicsState, Cost to Nat, compare to physicsCost, zero to LogicNat.zero, step to tickStep, Orbit to LogicNat, interpret to physicsInterpret. The required properties are discharged by rfl for interpret_zero and interpret_step, by direct appeal to ArithmeticFromLogic.zero_ne_succ and succ_injective for the orbit axioms, by LogicNat.induction for orbit_induction, and by setting the remaining logical axioms to True.
why it matters
This definition supplies the concrete physics model on which physics_faithful (tick interpretation is faithful) and physics_arithmetic_invariant (invariant extracted arithmetic) are built. It fills the stable interface slot in the universal forcing chain, realizing the identity-tick step and recognition-state carrier while avoiding build fragility in the full physics forcing chain. It directly supports the identity-tick and recognition-state conventions stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.