strictPositiveRatioRealization
plain-language theorem explainer
strictPositiveRatioRealization constructs a StrictLogicRealization whose carrier is the positive reals, with comparison costs supplied by any C that satisfies the laws of logic. Researchers tracing the forcing chain from logic to arithmetic cite it to obtain a concrete positive-ratio model. The definition is a direct structure instantiation that populates fields via multiplication for composition and appeals to the input laws plus lemmas such as ExcludedMiddle and RouteIndependence for the required properties.
Claim. Let $C$ be a comparison operator on positive reals that satisfies the laws of logic. The strict positive-ratio realization is the structure with carrier the set of positive reals, cost function given by $C$, composition by multiplication, generator chosen from the non-triviality axiom, and all required laws (identity, non-contradiction, excluded middle, route independence, scale invariance) holding by direct transfer from $C$.
background
ComparisonOperator is an abbreviation for a map from pairs of positive reals to reals that returns the cost of comparing them. SatisfiesLawsOfLogic bundles the structural constraints: identity (zero cost on the multiplicative identity), non-contradiction, excluded middle (continuity and totality), route independence (the d'Alembert polynomial form), scale invariance, and non-triviality (existence of a generator). StrictLogicRealization is the record type whose fields encode a carrier set, cost type, comparison map, composition, unit, generator, and the six laws that any such realization must obey. LogicNat is the inductive type with constructors identity and step that models the orbit generated by repeated multiplication by the generator, as forced by the same laws.
proof idea
The definition is a direct structure construction. Carrier is set to the subtype of positive reals. Cost is the reals. Compare delegates to C. Compose uses multiplication and preserves positivity. One is the real number 1. Generator is obtained by choice from the non-triviality field of h. The six laws are discharged by direct appeal to the corresponding fields of h or by the lemmas ExcludedMiddle C, RouteIndependence C, and ScaleInvariant C.
why it matters
This definition supplies the strict positive-ratio model used by positiveRatio_arith_equiv_logicNat to identify its induced arithmetic with LogicNat and by strictPositiveRatio_arith_equiv_strictBoolean to equate it with the Boolean realization. It therefore closes one concrete instance of the universal forcing claim that every realization obeying the laws of logic forces the same Peano arithmetic. The construction sits inside the strict layer of UniversalForcing and relies on the functional-equation package to guarantee the eight-tick octave and three-dimensional spatial structure downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.