physicsCost_symm
plain-language theorem explainer
Symmetry of the equality cost on physics states follows from the binary definition of that cost. Workers on the minimal physics realization in the Recognition Science forcing chain cite it to confirm the compare operator meets the axioms required by LogicRealization. The proof is a short tactic script that splits on equality of the two states and simplifies each branch using the cost definition.
Claim. For all physics states $x$ and $y$, the equality cost satisfies $c(x,y)=c(y,x)$, where $c$ returns $0$ if the states are identical and $1$ otherwise.
background
The PhysicsLogicRealization module supplies a stable interface for the universal forcing chain: identity ticks serve as the step action and recognition states act as the carrier, with equality cost as the minimal realization of physical tick arithmetic. PhysicsState is the structure whose sole field is a LogicNat tick, equipped with decidable equality. The function physicsCost(x,y) is defined to return 0 precisely when x equals y and 1 otherwise. This construction rests on the upstream Identity property (comparison of a quantity with itself costs zero) and on the fundamental tick unit from Constants.
proof idea
The tactic proof opens with by_cases on whether x equals y. The equal case substitutes the hypothesis and simplifies directly against the definition of physicsCost. The unequal case first derives the symmetric inequality y ≠ x, then simplifies both cost expressions under the two distinctness hypotheses.
why it matters
The result is used by physicsRealization to equip the LogicRealization record with Carrier := PhysicsState, Cost := Nat, and compare := physicsCost. It supplies the symmetry half of the comparison operator axioms required by that skeleton, aligning with the non-contradiction clause already present in the upstream Identity definition. The lemma therefore closes a basic requirement in the lightweight physics hook without touching the larger T0-T8 chain or fragile imports.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.