physicsCost
plain-language theorem explainer
Equality cost on physics states returns zero when the states coincide and one when they differ. Researchers constructing minimal LogicRealization instances for the Universal Forcing chain cite this definition to equip the PhysicsState carrier with a discrete cost. The definition is realized by a direct conditional on equality of the input states.
Claim. For physics states $x$ and $y$, the cost is $0$ if $x = y$ and $1$ otherwise.
background
PhysicsState is a structure with a single field tick of type LogicNat and decidable equality. It supplies the minimal carrier for recognition states indexed by identity ticks. The module supplies a lightweight interface for Universal Forcing that treats identity ticks as the step action and equality cost as the minimal realization of physical tick arithmetic, avoiding fragile imports from the full forcing chain. The definition depends directly on this PhysicsState structure.
proof idea
The definition is a direct if-then-else expression that tests equality of the two states and returns the corresponding Nat value.
why it matters
This definition supplies the compare operation for physicsRealization, which instantiates LogicRealization with PhysicsState as carrier and Nat as cost. It enables the downstream self-cost and symmetry theorems. In the Recognition framework it furnishes the stable minimal hook for tick arithmetic in the physics logic realization module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.