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
depends on (26)
Lean names referenced from this declaration's body.