eqCost_symm
plain-language theorem explainer
Symmetry of the two-valued equality cost holds for any carrier type equipped with decidable equality. Researchers constructing minimal LogicRealization instances from a single distinction cite this result to confirm that the comparison function is undirected before invoking the universal forcing interface. The proof unfolds the cost definition and splits into cases on whether the arguments are equal, applying substitution and simplification in each branch.
Claim. Let $K$ be any type with decidable equality. For elements $a,b$ in $K$, the two-valued equality cost satisfies $eqCost(a,b)=eqCost(b,a)$.
background
The module shows that any carrier with at least one named distinction $x≠y$ directly instantiates the LogicRealization interface on that carrier itself. The two-valued equality cost is the function that returns zero on equal inputs and one on distinct inputs. This supplies the comparison map required by the interface while keeping the construction minimal and free of any assumption that the carrier already carries a smooth real-valued J-cost. The upstream constant $K=ϕ^{1/2}$ is the dimensionless bridge ratio used elsewhere in the framework, but the type parameter here is simply the arbitrary carrier.
proof idea
The proof unfolds the definition of eqCost. It then applies by_cases on the proposition a=b. When the arguments are equal, substitution reduces both sides to zero. When they differ, the symmetric negation b≠a is derived by contradiction and both sides simplify to one.
why it matters
The lemma is invoked inside logicRealizationOfDistinction, the universal instantiation theorem that equips every non-singleton carrier with a LogicRealization structure whose carrier is exactly the given type. It thereby supplies the symmetry needed for the cost function to serve as a valid comparison in the interface, allowing Universal Forcing to apply uniformly. In the Recognition Science chain this closes the first universal step from a bare distinction to a full logic realization without presupposing a native J-cost on the carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.