equality_cost_satisfies_definitional
plain-language theorem explainer
Any equality-induced cost on the reals satisfies the Identity and Non-Contradiction conditions of the logic functional equation for arbitrary real weight. Foundation researchers cite this when decomposing SatisfiesLawsOfLogic into definitional versus substantive axioms. The proof is a term-mode pairing that applies the lemmas identity_from_equality and non_contradiction_from_equality directly to the reals and the given weight.
Claim. For every real number $w$, let $C_w$ denote the Hamming cost function on the reals with weight $w$. Then $C_w$ satisfies the identity law and the non-contradiction law.
background
In the PrimitiveDistinction module, equalityDistinction and equalityCost construct costs directly from the equality relation on a carrier type. The concrete function hammingCostOnReal weight realizes this construction on the reals by scaling a Hamming-style distinction measure by the supplied weight. Upstream, LogicAsFunctionalEquation defines Identity and NonContradiction as two of the four Aristotelian conditions inside SatisfiesLawsOfLogic; the module summary states that these three conditions (Identity, Non-Contradiction, Totality) are forced by the type signature of any equality-induced cost while only Composition Consistency remains substantive.
proof idea
The proof is a term-mode wrapper. It uses refine to build the conjunction, then discharges the Identity subgoal by applying identity_from_equality to the reals, the weight, and the element x, and discharges the NonContradiction subgoal by applying non_contradiction_from_equality to the reals, the weight, and the pair x, y.
why it matters
The result isolates the definitional facts among the logic laws, confirming the module summary that the rigidity theorem of Logic_FE rests on one substantive structural condition (Composition Consistency) plus three definitional facts. It aligns with the Recognition Science forcing chain by separating automatic consistency properties from the RCL (T5 J-uniqueness) and the eight-tick octave (T7). No downstream uses are recorded yet, so the declaration currently serves as a bridge lemma inside the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.