physicsCost_self
plain-language theorem explainer
The theorem shows that the equality cost between any physics state and itself is zero. Developers of the physics realization layer cite it to confirm the zero-cost axiom holds for the compare function in LogicRealization. The proof is a one-line simp wrapper that reduces directly from the definition of physicsCost.
Claim. For every physics state $x$, the equality cost satisfies $cost(x,x)=0$, where $cost$ returns $0$ on identical states and $1$ otherwise.
background
PhysicsState is the minimal recognition-state skeleton: a structure with a single field tick of type LogicNat equipped with decidable equality. The function physicsCost is defined to return $0$ precisely when its two arguments are equal and $1$ otherwise. The module supplies a stable interface for Universal Forcing by taking identity ticks as the step action and equality cost as the minimal realization of physical tick arithmetic.
proof idea
The proof is a one-line simp wrapper that unfolds the definition of physicsCost and reduces the identical-state case to zero.
why it matters
The result is used by physicsRealization to construct the LogicRealization instance with PhysicsState as carrier and physicsCost as compare. It supplies the zero-cost axiom required by that skeleton, closing the minimal arithmetic interface for the forcing chain without importing heavier physics modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.