continuousRealization
plain-language theorem explainer
Continuous positive-ratio Law-of-Logic realization maps any comparison operator obeying the Aristotelian constraints and scale invariance to the standard LogicRealization interface on positive reals. Workers on the universal forcing chain cite it to obtain the continuous arithmetic model before proving equivalence to the discrete case. The definition is a one-line wrapper around ofPositiveRatioComparison.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator and let $h$ be a proof that $C$ satisfies identity, non-contradiction, excluded middle, scale invariance and route independence. Then continuousRealization$(C,h)$ is the LogicRealization whose carrier is the positive reals, whose cost type is ℝ, and whose compare operation is induced by $C$.
background
ComparisonOperator is the abbreviation ℝ → ℝ → ℝ that assigns a real-valued cost to any pair of positive quantities. SatisfiesLawsOfLogic is the structure requiring the four Aristotelian constraints together with scale invariance (which reduces the two-argument form to a one-argument cost on ratios) and non-triviality. LogicRealization is the lean interface structure that every realization must supply: a carrier type, a cost type with zero, a compare map, and a distinguished zero element; the invariant arithmetic object is extracted from these data alone. The module re-exports the positive-ratio construction under the Universal Forcing namespace so that downstream invariance statements can treat the continuous and discrete cases uniformly.
proof idea
one-line wrapper that applies ofPositiveRatioComparison
why it matters
This definition supplies the continuous positive-ratio case required by the Universal Forcing program. It is invoked directly by continuous_arith_equiv_logicNat to extract the Peano carrier and by arith_continuous_equiv_arith_discrete to obtain the canonical equivalence between continuous and discrete arithmetic. The construction therefore sits at the interface between the functional-equation axioms and the later steps that recover the eight-tick octave and the three-dimensional spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.