pith. machine review for the scientific record. sign in
theorem proved term proof

laws_of_logic_imply_dalembert_hypotheses

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 270theorem laws_of_logic_imply_dalembert_hypotheses
 271    (C : ComparisonOperator) (hLaws : SatisfiesLawsOfLogic C) :
 272    IsNormalized (derivedCost C) ∧
 273    IsSymmetric (derivedCost C) ∧
 274    (∃ P : ℝ → ℝ → ℝ,
 275      (∃ a b c d e f : ℝ, ∀ u v, P u v = a + b*u + c*v + d*u*v + e*u^2 + f*v^2) ∧
 276      (∀ u v, P u v = P v u) ∧
 277      HasMultiplicativeConsistency (derivedCost C) P) ∧
 278    ContinuousOn (derivedCost C) (Set.Ioi 0) ∧
 279    (∃ x : ℝ, 0 < x ∧ derivedCost C x ≠ 0) := by

proof body

Term-mode proof.

 280  refine ⟨?_, ?_, ?_, ?_, ?_⟩
 281  · exact identity_implies_normalized C hLaws.identity
 282  · exact non_contradiction_and_scale_imply_reciprocal C
 283      hLaws.non_contradiction hLaws.scale_invariant
 284  · exact route_independence_implies_multiplicative_consistency C
 285      hLaws.route_independence
 286  · exact excluded_middle_implies_continuous C hLaws.excluded_middle
 287  · exact hLaws.non_trivial
 288
 289/-! ## Main Theorem: RCL is the Unique Functional Form of the Laws of Logic -/
 290
 291/-- **Main theorem (Logical Formalization Theorem)**: For a comparison
 292operator satisfying the four Aristotelian constraints with scale invariance
 293and non-triviality, the route-independence combiner is necessarily of the
 294Recognition Composition Law form: `P(u,v) = 2u + 2v + c·uv` for some
 295constant c ∈ ℝ.
 296
 297In other words: the unique functional form the laws of logic can take on
 298continuous comparisons of positive ratios, under the polynomial regularity
 299assumption, is the Recognition Composition Law.
 300
 301This is an immediate corollary of `laws_of_logic_imply_dalembert_hypotheses`
 302combined with `bilinear_family_forced` (Inevitability.lean), which has been
 303peer-reviewed in:
 304
 305  Washburn, Zlatanović, Allahyarov.
 306  "The d'Alembert Inevitability Theorem."
 307  Mathematics (MDPI), 2026.
 308-/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (32)

Lean names referenced from this declaration's body.

… and 2 more