logicNatCost_symm
plain-language theorem explainer
Symmetry of the binary cost function on the LogicNat carrier follows directly from case analysis on argument equality. Researchers establishing strict categorical realizations of arithmetic in Recognition Science cite this to confirm invariance of the compare operation. The proof splits on whether the inputs coincide, substitutes in the equal branch, derives the swapped inequality in the unequal branch, and simplifies using the definition in both cases.
Claim. For all $a, b$ in the LogicNat type, the cost function satisfies cost$(a, b) =$ cost$(b, a)$, where cost$(a, b)$ equals 0 if $a = b$ and 1 otherwise.
background
LogicNat is the inductive type whose constructors identity and step generate the multiplicative orbit starting at 1, serving as the canonical Peano surface for arithmetic realized from logic. The logicNatCost function is the binary compare operation that returns 0 on equal arguments and 1 on unequal arguments. The module supplies the strict categorical/Lawvere-style hook whose carrier is this LogicNat NNO surface; the theorem depends on the definition of logicNatCost together with the canonical arithmetic object and the LogicNat inductive type.
proof idea
The proof opens with by_cases on whether a equals b. The equal branch substitutes and simplifies both sides to 0. The unequal branch first constructs the symmetric inequality b ≠ a, then simplifies both sides of the goal to 1 using the definition of logicNatCost.
why it matters
The result supplies the symmetry needed for the compare field inside strictCategoricalRealization, the definition that assembles the full StrictLogicRealization structure with Carrier := LogicNat and Cost := Nat. It closes a basic invariance check for the canonical arithmetic object in the Recognition Science foundation, ensuring the cost operation is well-defined as a symmetric relation before any further composition or realization steps are taken.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.