aristotelian_decomposition

formal source

 259theorem from "seven independent axioms" to "four substantive
 260structural conditions plus three definitional facts."
 261-/
 262theorem aristotelian_decomposition (weight : ℝ) (hw : weight ≠ 0) :
 263    -- Definitional: L1, L2, L3a hold for the equality-induced cost.
 264    (∀ x : ℝ, equalityCost ℝ weight x x = 0) ∧
 265    (∀ x y : ℝ, equalityCost ℝ weight x y = equalityCost ℝ weight y x) ∧
 266    (∀ x y : ℝ, ∃ c : ℝ, equalityCost ℝ weight x y = c) ∧
 267    -- Substantive: L4 fails for the equality-induced cost, demonstrating
 268    -- that L4 is not a type-theoretic consequence.
 269    ¬ CompositionConsistency (hammingCostOnReal weight) := by
 270  refine ⟨?_, ?_, ?_, ?_⟩
 271  · exact identity_from_equality ℝ weight
 272  · exact non_contradiction_from_equality ℝ weight
 273  · exact totality_from_function_type ℝ weight
 274  · exact composition_consistency_not_definitional weight hw
 275
 276/-! ## Bridge to Logic_FE
 277
 278Here we connect the new framework to the existing
 279`SatisfiesLawsOfLogic` predicate. The bridge says: if a comparison
 280operator on `ℝ_{>0}` is derived from an equality cost, then it
 281automatically satisfies the Identity and Non-Contradiction conditions
 282of Logic_FE, and the rigidity theorem of Logic_FE reduces to imposing
 283the substantive conditions (Composition Consistency, Continuity, Scale
 284Invariance, polynomial closure, Non-Triviality) on the cost.
 285-/
 286
 287open IndisputableMonolith.Foundation.LogicAsFunctionalEquation
 288
 289/-- **Bridge theorem.** The Identity and Non-Contradiction conditions
 290of `SatisfiesLawsOfLogic` are automatic for any equality-induced cost.
 291The remaining four conditions of `SatisfiesLawsOfLogic` (excluded
 292middle as continuity, scale invariance, route independence, and