def
definition
NonTrivial
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.LogicAsFunctionalEquation on GitHub at line 142.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
all -
all -
of -
bridge -
scale -
all -
of -
one -
A -
ComparisonOperator -
derivedCost -
cost -
cost -
is -
of -
from -
one -
is -
of -
is -
of -
A -
is -
A -
all -
and -
that -
one -
two -
one -
comparison
used by
formal source
139/-- A comparison operator is **non-trivial** if there exists at least one
140positive ratio with non-zero cost. (Without this assumption the constant zero
141function vacuously satisfies all the constraints.) -/
142def NonTrivial (C : ComparisonOperator) : Prop :=
143 ∃ x : ℝ, 0 < x ∧ derivedCost C x ≠ 0
144
145/-- A comparison operator **satisfies the laws of logic** if all four
146Aristotelian constraints hold, together with scale invariance (the bridge
147from two-argument to one-argument form) and non-triviality (so that the
148derived cost is not vacuously zero). -/
149structure SatisfiesLawsOfLogic (C : ComparisonOperator) : Prop where
150 identity : Identity C
151 non_contradiction : NonContradiction C
152 excluded_middle : ExcludedMiddle C
153 scale_invariant : ScaleInvariant C
154 route_independence : RouteIndependence C
155 non_trivial : NonTrivial C
156
157/-! ## Translation Lemmas
158
159The four Aristotelian constraints, applied to the derived cost function
160F(r) := C(r, 1), produce the hypotheses of the d'Alembert Inevitability
161Theorem.
162-/
163
164/-- **Translation lemma 1 (Identity ⇒ Normalization)**: If a comparison
165operator satisfies Identity, then the derived cost function takes value
166zero at the multiplicative identity. -/
167theorem identity_implies_normalized (C : ComparisonOperator)
168 (hId : Identity C) :
169 IsNormalized (derivedCost C) := by
170 unfold IsNormalized derivedCost
171 exact hId 1 one_pos
172