PositiveRatio
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 in Recognition Science
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.
scope and limits
- Does not define any comparison operator or cost function.
- Does not prove equivalence between distinguishability and non-triviality.
- Does not constrain constants such as phi or the alpha band.
- Does not address discrete or Boolean realizations directly.
formal statement (Lean)
130abbrev PositiveRatio := {x : ℝ // 0 < x}
proof body
Definition body.
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. -/