equality_cost_satisfies_definitional

formal source

 291The remaining four conditions of `SatisfiesLawsOfLogic` (excluded
 292middle as continuity, scale invariance, route independence, and
 293non-triviality) are the substantive structural axioms. -/
 294theorem equality_cost_satisfies_definitional
 295    (weight : ℝ) :
 296    Identity (hammingCostOnReal weight) ∧
 297    NonContradiction (hammingCostOnReal weight) := by
 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