theorem
proved
aristotelian_decomposition
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.PrimitiveDistinction on GitHub at line 262.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
bridge -
scale -
Composition -
of -
Identity -
SatisfiesLawsOfLogic -
cost -
cost -
is -
of -
CompositionConsistency -
composition_consistency_not_definitional -
equalityCost -
from -
hammingCostOnReal -
identity_from_equality -
non_contradiction_from_equality -
totality_from_function_type -
as -
is -
of -
for -
is -
of -
is -
and -
that -
Bridge -
comparison
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