pith. machine review for the scientific record. sign in
def definition def or abbrev

strictPositiveRatioRealization

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)

  19noncomputable def strictPositiveRatioRealization
  20    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
  21    StrictLogicRealization where
  22  Carrier := {x : ℝ // 0 < x}

proof body

Definition body.

  23  Cost := ℝ
  24  zeroCost := inferInstance
  25  compare := fun x y => C x.1 y.1
  26  compose := fun x y => ⟨x.1 * y.1, mul_pos x.2 y.2⟩
  27  one := ⟨1, one_pos⟩
  28  generator :=
  29    let γ : ℝ := Classical.choose h.non_trivial
  30    ⟨γ, (Classical.choose_spec h.non_trivial).1⟩
  31  identity_law := by
  32    intro x
  33    exact h.identity x.1 x.2
  34  non_contradiction_law := by
  35    intro x y
  36    exact h.non_contradiction x.1 y.1 x.2 y.2
  37  excluded_middle_law := ExcludedMiddle C
  38  composition_law := RouteIndependence C
  39  invariance_law := ScaleInvariant C
  40  nontrivial_law := by
  41    exact (Classical.choose_spec h.non_trivial).2
  42
  43/-- Strict positive-ratio forced arithmetic is canonically `LogicNat`. -/

used by (3)

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

depends on (19)

Lean names referenced from this declaration's body.