physicsRealization
The physics realization supplies a concrete LogicRealization instance with PhysicsState as carrier and LogicNat ticks as orbit for the forcing chain. Workers on Universal Forcing cite it as the stable minimal interface that realizes identity ticks via equality cost. The definition assembles the record by direct field assignment from ArithmeticFromLogic constructors and local helpers.
claimThe physics realization is the LogicRealization whose carrier is the set of states each carrying one LogicNat tick index, whose cost is the natural-number equality cost, whose step action is the tick successor, whose orbit is the LogicNat type with its identity and successor constructors, and whose interpretation and orbit axioms hold by reflexivity together with the inductive properties of LogicNat.
background
PhysicsLogicRealization supplies the stable interface for the physics side of Universal Forcing. Its carrier is PhysicsState, the structure whose single field is a tick of type LogicNat. LogicNat is the inductive type generated by identity and step, serving as the orbit forced by the Law of Logic and mirroring the multiplicative orbit closed under the generator.
proof idea
The definition constructs the LogicRealization record by explicit field assignment. Carrier and Cost are set to PhysicsState and Nat. Step uses tickStep, orbit uses LogicNat with its zero and succ, and interpret uses physicsInterpret. Orbit axioms are discharged by zero_ne_succ, succ_injective and induction from ArithmeticFromLogic; nontriviality applies succ to zero and simplifies the cost.
why it matters in Recognition Science
This definition supplies the concrete carrier that physics_faithful and physics_arithmetic_invariant depend on. It realizes identity ticks as the step action inside the forcing chain and closes the lightweight hook described in the module. It connects to the eight-tick octave through the imported tick constants and provides the arithmetic orbit for downstream physics invariants.
scope and limits
- Does not embed the full physics forcing chain or its build dependencies.
- Does not compute explicit state transitions beyond single tick steps.
- Does not prove faithfulness of the interpretation; that is handled separately.
- Does not define the cost function beyond reference to the sibling physicsCost.
Lean usage
theorem example : LogicRealization.FaithfulArithmeticInterpretation physicsRealization := physics_faithfulformal statement (Lean)
46def physicsRealization : LogicRealization where
47 Carrier := PhysicsState
proof body
Definition body.
48 Cost := Nat
49 zeroCost := inferInstance
50 compare := physicsCost
51 zero := ⟨ArithmeticFromLogic.LogicNat.zero⟩
52 step := tickStep
53 Orbit := ArithmeticFromLogic.LogicNat
54 orbitZero := ArithmeticFromLogic.LogicNat.zero
55 orbitStep := ArithmeticFromLogic.LogicNat.succ
56 interpret := physicsInterpret
57 interpret_zero := rfl
58 interpret_step := by intro n; rfl
59 orbit_no_confusion := by
60 intro n h
61 exact ArithmeticFromLogic.LogicNat.zero_ne_succ n h
62 orbit_step_injective := ArithmeticFromLogic.LogicNat.succ_injective
63 orbit_induction := by
64 intro P h0 hs n
65 exact ArithmeticFromLogic.LogicNat.induction (motive := P) h0 hs n
66 orbitEquivLogicNat := Equiv.refl ArithmeticFromLogic.LogicNat
67 orbitEquiv_zero := rfl
68 orbitEquiv_step := by intro n; rfl
69 identity := physicsCost_self
70 nonContradiction := physicsCost_symm
71 excludedMiddle := True
72 composition := True
73 actionInvariant := True
74 nontrivial := by
75 refine ⟨⟨ArithmeticFromLogic.LogicNat.succ ArithmeticFromLogic.LogicNat.zero⟩, ?_⟩
76 simp [physicsCost]
77
78/-- Physics tick interpretation is faithful. -/