IndisputableMonolith.Foundation.NonTrivialityFromDistinguishability

   1import Mathlib
   2import IndisputableMonolith.Foundation.LogicAsFunctionalEquation
   3import IndisputableMonolith.Foundation.AbsoluteFloorClosure
   4
   5/-!
   6  NonTrivialityFromDistinguishability.lean
   7
   8  Move 1: promote `NonTrivial` from a posit to a corollary.
   9
  10  In `Foundation.LogicAsFunctionalEquation`, `SatisfiesLawsOfLogic`
  11  carries a `non_trivial` field stating that the derived cost function
  12  is not identically zero on the positive ratios. The reason it was
  13  posited at all is that the constant-zero comparison operator
  14  vacuously satisfies the four Aristotelian conditions; without an
  15  extra commitment we cannot rule it out.
  16
  17  This module replaces `non_trivial` with the more natural Aristotelian
  18  content: **distinguishability**, the claim that comparison is not
  19  vacuous, i.e. there exists at least one pair of distinct positive
  20  quantities whose comparison cost is non-zero.
  21
  22  We then prove the equivalence: under Identity + Non-Contradiction +
  23  Scale Invariance, distinguishability is equivalent to the original
  24  `NonTrivial` predicate. So distinguishability is the canonical
  25  Aristotelian content; `NonTrivial` is an algebraic reformulation of
  26  the same fact.
  27
  28  This makes the framework slightly more fundamental: the residual
  29  posit in `SatisfiesLawsOfLogic` is now stated in genuinely
  30  Aristotelian language, with no reference to the derived-cost
  31  definition.
  32-/
  33
  34namespace IndisputableMonolith
  35namespace Foundation
  36namespace LogicAsFunctionalEquation
  37
  38open Real
  39
  40/-- **Distinguishability**: comparison is operative, i.e. there exists
  41at least one pair of positive quantities whose comparison is not
  42vacuous. This is the operative Aristotelian content of comparison. -/
  43def Distinguishability (C : ComparisonOperator) : Prop :=
  44  ∃ x y : ℝ, 0 < x ∧ 0 < y ∧ C x y ≠ 0
  45
  46/-- **Equivalence (forward)**: distinguishability implies the algebraic
  47non-triviality predicate, given Scale Invariance. -/
  48theorem nonTrivial_of_distinguishability
  49    (C : ComparisonOperator)
  50    (hSI : ScaleInvariant C)
  51    (hDist : Distinguishability C) :
  52    NonTrivial C := by
  53  obtain ⟨x, y, hx, hy, hxy⟩ := hDist
  54  -- Use scale invariance with λ = y⁻¹ to get C(x/y, 1) = C(x, y) ≠ 0.
  55  have hyinv : (0 : ℝ) < y⁻¹ := inv_pos.mpr hy
  56  have hxoverypos : (0 : ℝ) < x / y := div_pos hx hy
  57  have hkey : C (y⁻¹ * x) (y⁻¹ * y) = C x y := hSI x y y⁻¹ hx hy hyinv
  58  have hyne : (y : ℝ) ≠ 0 := ne_of_gt hy
  59  have hyinv_y : y⁻¹ * y = 1 := inv_mul_cancel₀ hyne
  60  have hyinv_x : y⁻¹ * x = x / y := by
  61    field_simp
  62  rw [hyinv_y, hyinv_x] at hkey
  63  refine ⟨x / y, hxoverypos, ?_⟩
  64  show derivedCost C (x / y) ≠ 0
  65  unfold derivedCost
  66  rw [hkey]
  67  exact hxy
  68
  69/-- **Equivalence (backward)**: the algebraic non-triviality predicate
  70implies distinguishability. -/
  71theorem distinguishability_of_nonTrivial
  72    (C : ComparisonOperator)
  73    (hNT : NonTrivial C) :
  74    Distinguishability C := by
  75  obtain ⟨x, hx, hxne⟩ := hNT
  76  refine ⟨x, 1, hx, one_pos, ?_⟩
  77  show C x 1 ≠ 0
  78  exact hxne
  79
  80/-- **Equivalence theorem**: under scale invariance, distinguishability
  81and non-triviality are the same condition. -/
  82theorem nonTrivial_iff_distinguishability
  83    (C : ComparisonOperator) (hSI : ScaleInvariant C) :
  84    NonTrivial C ↔ Distinguishability C :=
  85  ⟨distinguishability_of_nonTrivial C, nonTrivial_of_distinguishability C hSI⟩
  86
  87/-! ## A canonical form of `SatisfiesLawsOfLogic` using distinguishability -/
  88
  89/-- The canonical Aristotelian form of the Law of Logic, with
  90distinguishability replacing the algebraic non-triviality predicate. -/
  91structure SatisfiesLawsOfLogicCanonical (C : ComparisonOperator) : Prop where
  92  identity            : Identity C
  93  non_contradiction   : NonContradiction C
  94  excluded_middle     : ExcludedMiddle C
  95  scale_invariant     : ScaleInvariant C
  96  route_independence  : RouteIndependence C
  97  distinguishability  : Distinguishability C
  98
  99/-- The canonical form is equivalent to the existing form. -/
 100theorem canonical_iff_existing (C : ComparisonOperator) :
 101    SatisfiesLawsOfLogicCanonical C ↔ SatisfiesLawsOfLogic C := by
 102  constructor
 103  · intro h
 104    refine
 105      { identity := h.identity
 106      , non_contradiction := h.non_contradiction
 107      , excluded_middle := h.excluded_middle
 108      , scale_invariant := h.scale_invariant
 109      , route_independence := h.route_independence
 110      , non_trivial := nonTrivial_of_distinguishability C h.scale_invariant h.distinguishability }
 111  · intro h
 112    refine
 113      { identity := h.identity
 114      , non_contradiction := h.non_contradiction
 115      , excluded_middle := h.excluded_middle
 116      , scale_invariant := h.scale_invariant
 117      , route_independence := h.route_independence
 118      , distinguishability := distinguishability_of_nonTrivial C h.non_trivial }
 119
 120/-! ## Absolute-floor supplied canonical form
 121
 122The structure above still stores `distinguishability` directly for
 123backward compatibility. The absolute-floor route below supplies that
 124field from a non-trivial specifiability witness on the positive-ratio
 125carrier, together with the statement that the comparison operator detects
 126the resulting carrier-level distinction.
 127-/
 128
 129/-- Positive-ratio carrier used by the continuous Law-of-Logic realization. -/
 130abbrev PositiveRatio := {x : ℝ // 0 < x}
 131
 132/-- Law-of-Logic data with distinguishability supplied by the absolute-floor
 133closure: a non-trivial specification of the positive-ratio carrier plus a
 134comparison operator that detects distinct specified carrier points. -/
 135structure SatisfiesLawsOfLogicAbsoluteFloor (C : ComparisonOperator) : Prop where
 136  identity            : Identity C
 137  non_contradiction   : NonContradiction C
 138  excluded_middle     : ExcludedMiddle C
 139  scale_invariant     : ScaleInvariant C
 140  route_independence  : RouteIndependence C
 141  floor               : AbsoluteFloorClosure.AbsoluteFloorWitness PositiveRatio
 142  detects_floor       : ∀ x y : PositiveRatio, x ≠ y → C x.1 y.1 ≠ 0
 143
 144/-- Absolute-floor Law-of-Logic data supplies ordinary distinguishability. -/
 145theorem distinguishability_of_absoluteFloor
 146    (C : ComparisonOperator) (h : SatisfiesLawsOfLogicAbsoluteFloor C) :
 147    Distinguishability C := by
 148  obtain ⟨x, y, hxy⟩ :=
 149    AbsoluteFloorClosure.bare_distinguishability_of_absolute_floor h.floor
 150  exact ⟨x.1, y.1, x.2, y.2, h.detects_floor x y hxy⟩
 151
 152/-- The absolute-floor form induces the canonical Law-of-Logic form. -/
 153theorem canonical_of_absoluteFloor
 154    (C : ComparisonOperator) (h : SatisfiesLawsOfLogicAbsoluteFloor C) :
 155    SatisfiesLawsOfLogicCanonical C where
 156  identity := h.identity
 157  non_contradiction := h.non_contradiction
 158  excluded_middle := h.excluded_middle
 159  scale_invariant := h.scale_invariant
 160  route_independence := h.route_independence
 161  distinguishability := distinguishability_of_absoluteFloor C h
 162
 163/-- The absolute-floor form induces the existing algebraic form used by
 164downstream modules. -/
 165theorem existing_of_absoluteFloor
 166    (C : ComparisonOperator) (h : SatisfiesLawsOfLogicAbsoluteFloor C) :
 167    SatisfiesLawsOfLogic C :=
 168  (canonical_iff_existing C).mp (canonical_of_absoluteFloor C h)
 169
 170/-! ## The constant-zero exclusion
 171
 172The constant-zero comparison operator `C ≡ 0` satisfies Identity,
 173Non-Contradiction, Excluded Middle, Scale Invariance, and a vacuous
 174form of Route Independence. The reason it does not satisfy the Law of
 175Logic is precisely that it fails distinguishability — comparison
 176collapses, so reality on this operator has no operative content.
 177
 178This is the structural reason why distinguishability is a genuine
 179Aristotelian content rather than an external assumption: an operator
 180satisfying every other condition but failing distinguishability is
 181the constant-zero operator, which is the formal expression of "no
 182comparison is operative." -/
 183
 184/-- The constant-zero comparison operator. -/
 185def constZero : ComparisonOperator := fun _ _ => 0
 186
 187/-- Constant zero satisfies identity. -/
 188theorem constZero_identity : Identity constZero := by
 189  intro x _; rfl
 190
 191/-- Constant zero satisfies non-contradiction. -/
 192theorem constZero_nonContradiction : NonContradiction constZero := by
 193  intro x y _ _; rfl
 194
 195/-- Constant zero is continuous on the positive quadrant. -/
 196theorem constZero_continuous : ExcludedMiddle constZero := by
 197  unfold ExcludedMiddle
 198  exact continuousOn_const
 199
 200/-- Constant zero is scale-invariant. -/
 201theorem constZero_scaleInvariant : ScaleInvariant constZero := by
 202  intro _ _ _ _ _ _; rfl
 203
 204/-- Constant zero fails distinguishability. -/
 205theorem constZero_not_distinguishable : ¬ Distinguishability constZero := by
 206  intro ⟨_, _, _, _, h⟩
 207  exact h rfl
 208
 209/-- Constant zero fails non-triviality. -/
 210theorem constZero_not_nonTrivial : ¬ NonTrivial constZero := by
 211  intro ⟨_, _, h⟩
 212  exact h rfl
 213
 214/-! ## Summary
 215
 216Move 1 closure: distinguishability is an Aristotelian content, the
 217algebraic `NonTrivial` predicate is one of its consequences under
 218scale invariance, and the only operator that satisfies all the other
 219laws but fails distinguishability is the constant-zero operator. The
 220residual posit in `SatisfiesLawsOfLogic` is therefore reducible to a
 221genuinely Aristotelian commitment, and the framework can be stated
 222canonically using `SatisfiesLawsOfLogicCanonical`. -/
 223
 224end LogicAsFunctionalEquation
 225end Foundation
 226end IndisputableMonolith
 227