equality_cost_satisfies_definitional
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish that the cost satisfies Composition Consistency.
- Does not prove continuity, scale invariance, or non-triviality.
- Does not apply to costs that are not equality-induced.
- Does not constrain the numerical value of the weight parameter.
formal statement (Lean)
294theorem equality_cost_satisfies_definitional
295 (weight : ℝ) :
296 Identity (hammingCostOnReal weight) ∧
297 NonContradiction (hammingCostOnReal weight) := by
proof body
Term-mode proof.
298 refine ⟨?_, ?_⟩
299 · intro x _
300 exact identity_from_equality ℝ weight x
301 · intro x y _ _
302 exact non_contradiction_from_equality ℝ weight x y
303
304/-! ## Summary
305
306The four Aristotelian conditions of Logic_FE are not seven independent
307axioms. Three of them (Identity, Non-Contradiction, Totality) are
308definitional facts forced by the type signature of an equality-induced
309cost. Only the fourth (Composition Consistency) is a genuinely
310substantive structural condition.
311
312The rigidity theorem of Logic_FE therefore rests on:
313
314* **One substantive structural condition** (Composition Consistency):
315 the cost respects the carrier's composition.
316* **Three regularity / structural hypotheses** (Continuity, Scale
317 Invariance, Polynomial-degree-2 closure of the combiner): the cost
318 has the analytic regularity required for the d'Alembert classification
319 to apply.
320* **One existence assumption** (Non-Triviality): the cost is not
321 identically zero.
322* **Three definitional facts** (Identity, Non-Contradiction, Totality):
323 forced by the type signature of the equality-induced cost.
324
325This is the deepest structural decomposition of the Aristotelian
326foundations of comparison-based rigidity that the present framework
327admits.
328-/
329
330end PrimitiveDistinction
331end Foundation
332end IndisputableMonolith