PositiveRatio
plain-language theorem explainer
PositiveRatio defines the subtype of strictly positive reals that serves as carrier for the continuous Law-of-Logic realization. Researchers deriving arithmetic equivalences between positive-ratio and Boolean realizations cite this carrier when constructing StrictLogicRealization.arith. The definition is a direct subtype construction requiring no lemmas or proof steps beyond the subtype predicate.
Claim. $P := {x : ℝ | 0 < x}$ is the positive-ratio carrier on which the continuous realization of the laws of logic is defined.
background
In the module NonTrivialityFromDistinguishability the positive-ratio carrier replaces the non_trivial field of SatisfiesLawsOfLogic with distinguishability. The module shows that under Identity, Non-Contradiction, Scale Invariance and Route Independence the existence of at least one pair of distinct positive quantities with non-zero comparison cost is equivalent to the original non-triviality predicate. This shifts the residual posit from an algebraic statement about the derived cost to an Aristotelian statement about comparison.
proof idea
The declaration is a direct subtype abbreviation: PositiveRatio := {x : ℝ // 0 < x}. No upstream lemmas are invoked; the construction is primitive and carries no proof obligations.
why it matters
PositiveRatio supplies the carrier for SatisfiesLawsOfLogicAbsoluteFloor and for the two strict equivalence theorems strictPositiveRatio_arith_equiv_strictBoolean and positiveRatio_strict_equiv_existing. These theorems establish that the forced arithmetic is identical across the positive-ratio and Boolean realizations, closing the loop from the functional equation to Peano arithmetic without reference to the derived-cost definition. It anchors the positive ratios on which J acts in the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.