physicsCost
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not assign graded costs based on tick differences.
- Does not incorporate J-cost, defect distance, or phi-ladder structure.
- Does not extend to continuous or non-discrete state spaces.
formal statement (Lean)
24def physicsCost (x y : PhysicsState) : Nat :=
proof body
Definition body.
25 if x = y then 0 else 1
26