ofPositiveRatioComparison
plain-language theorem explainer
This definition constructs a LogicRealization whose carrier is the positive reals, comparison is supplied by a given operator obeying the laws of logic, and orbit is the inductive natural numbers generated from the identity. Universal forcing work cites it to embed the continuous positive-ratio model into the abstract interface shared by all realizations. The construction populates each structure field directly from the operator axioms and the LogicNat orbit.
Claim. Let $C$ be a comparison operator satisfying the laws of logic. The positive-ratio realization is the structure whose carrier is the positive reals, whose comparison function is $C$, whose zero element is $1$, whose step multiplies by a non-trivial positive real chosen from the non-triviality axiom, and whose orbit is the inductive type generated by an identity element and a successor operation.
background
LogicRealization is the common structure used by the Universal Forcing program. It consists of a carrier type, a cost type equipped with zero, a comparison map from carrier to cost, a distinguished zero element, a step map on the carrier, an orbit type with its own zero and step, and a collection of propositions that enforce the arithmetic laws extracted from any Law-of-Logic setting.
proof idea
The definition is a direct field-by-field construction of the LogicRealization structure. Carrier and Cost are set to the positive reals and the reals. The step field chooses a non-trivial multiplier via Classical.choose on the non_trivial hypothesis. The orbit fields are supplied by LogicNat together with its zero, succ, injectivity, and induction theorems. The remaining axioms are discharged by direct appeal to the corresponding fields of the SatisfiesLawsOfLogic hypothesis or by reflexivity.
why it matters
This supplies the concrete continuous positive-ratio model that continuous_positive_ratio_arithmetic_invariant uses to prove all realizations share the same forced arithmetic. It is wrapped by continuousRealization and shown faithful by positiveRatio_faithful. In the framework it realizes the continuous case of the Law-of-Logic interface, allowing extraction of the same Peano arithmetic that later feeds the phi-ladder and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.