physicsCost_symm
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not assign numerical values to the cost beyond the binary indicator.
- Does not extend the cost function to states outside the PhysicsState structure.
- Does not interact with the full eight-tick octave or spatial dimension forcing steps.
- Does not prove that this cost is the unique minimal realization.
formal statement (Lean)
30theorem physicsCost_symm (x y : PhysicsState) : physicsCost x y = physicsCost y x := by
proof body
Tactic-mode proof.
31 by_cases h : x = y
32 · subst h
33 simp [physicsCost]
34 · have h' : y ≠ x := by intro hyx; exact h hyx.symm
35 simp [physicsCost, h, h']
36
37/-- Identity-tick successor. -/