physicsRealization
plain-language theorem explainer
The definition supplies the concrete LogicRealization for physics, taking recognition states indexed by ticks as carrier and the logic naturals as orbit under step. Researchers on the universal forcing chain cite it as the stable hook avoiding build fragility in the full physics module. The construction is a direct record filling that delegates arithmetic properties to the inductive naturals from logic and cost to the equality function on states.
Claim. A logic realization for physics is the structure whose carrier is the set of states each indexed by an identity tick, whose cost takes values in the natural numbers under equality comparison, whose orbit is the inductive type with identity element and successor generator, whose step advances by one tick, and whose interpretation maps the orbit to states while satisfying the zero, step, injectivity, induction, and non-contradiction axioms by direct assignment.
background
PhysicsState is the minimal recognition-state skeleton indexed by identity ticks, consisting of a single field holding a value from the logic naturals. LogicNat is the inductive type forced by the law of logic, with constructors identity (the zero-cost multiplicative identity) and step (one more application of the generator), mirroring the orbit closed under the generator and containing the identity. The module supplies a lightweight hook for universal forcing that uses identity ticks as the step action, recognition states as carrier, and equality cost as the minimal realization of physical tick arithmetic; it imports the ordered logic realization interface and depends on the arithmetic-from-logic module for the Peano structure together with the constants module for the fundamental tick quantum.
proof idea
The definition is a direct record construction. Carrier is set to the physics states, Cost to the naturals, compare to the equality cost function, zero and step to the corresponding logic-naturals elements, interpret to the physics interpretation map, and the axioms are discharged by reflexivity or by direct appeal to the successor injectivity, zero-not-successor, and induction lemmas from the arithmetic-from-logic module; the nontrivial witness is constructed explicitly as a successor state with positive cost.
why it matters
This supplies the stable interface for the physics realization inside the universal forcing chain, directly feeding the downstream results that establish faithful arithmetic interpretation and invariant extracted arithmetic. It realizes the tick-based evolution and eight-tick octave of the T0-T8 forcing chain while providing the minimal model before the full physics forcing module is integrated. It touches the open question of embedding the complete physics module without introducing unrelated build fragility.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.