PositiveRatio

formal source

 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