continuousRealization
ContinuousRealization re-exports the positive-ratio model of the laws of logic as a concrete LogicRealization instance for the universal forcing program. Researchers tracing the continuous-to-discrete arithmetic equivalence cite it when instantiating an abstract ComparisonOperator that obeys the Aristotelian constraints. The definition is a one-line wrapper delegating construction to ofPositiveRatioComparison.
claimLet $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator satisfying identity, non-contradiction, excluded middle, scale invariance and route independence. The continuous realization is the LogicRealization whose carrier is the positive reals, whose cost type is ℝ, and whose comparison map is given by $C$.
background
ComparisonOperator is the abbreviation for a map ℝ → ℝ → ℝ that returns the cost of comparing two positive quantities; the four Aristotelian constraints plus scale invariance turn it into a well-defined function on positive ratios. SatisfiesLawsOfLogic is the structure asserting that a given operator obeys identity, non-contradiction, excluded middle, scale invariance and route independence, ensuring the derived cost is non-vacuous and independent of path. LogicRealization packages a carrier, a cost type with zero, a compare operation and a distinguished zero element, supplying the minimal interface required by the forcing program. The module simply re-exports the existing ofPositiveRatioComparison construction under the UniversalForcing namespace so that downstream invariance statements can refer to the continuous model without importing the LogicRealization file directly.
proof idea
one-line wrapper that applies ofPositiveRatioComparison
why it matters in Recognition Science
This definition supplies the continuous positive-ratio instance required by the two invariance theorems that equate continuous and discrete arithmetic. It is used directly by continuous_arith_equiv_logicNat to extract the Peano carrier equivalence to LogicNat and by arith_continuous_equiv_arith_discrete to produce the canonical isomorphism between the continuous and discrete Peano carriers. In the Recognition framework the construction closes the loop from the functional equation through the laws of logic to a scale-invariant arithmetic that is independent of the chosen realization, supporting the claim that the forced arithmetic is unique up to equivalence.
scope and limits
- Does not construct the carrier or cost type from scratch; delegates entirely to ofPositiveRatioComparison.
- Does not verify the Aristotelian constraints; assumes they are supplied by the SatisfiesLawsOfLogic hypothesis.
- Does not address discrete realizations or other comparison operators.
- Does not prove any equivalence or invariance statement; only provides the instance used by those statements.
Lean usage
noncomputable def continuous_arith_equiv_logicNat (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) : (arithmeticOf (continuousRealization C h)).peano.carrier ≃ ArithmeticFromLogic.LogicNat := (continuousRealization C h).orbitEquivLogicNatformal statement (Lean)
19noncomputable def continuousRealization
20 (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
21 LogicRealization :=
proof body
Definition body.
22 LogicRealization.ofPositiveRatioComparison C h
23
24/-- The continuous realization carries the universal forced arithmetic. -/