positiveRatio_interpret_injective
The orbit interpretation map induced by any comparison operator satisfying the laws of logic is injective on the forced arithmetic. Researchers embedding logic into positive-real arithmetic cite this to secure distinctness of elements under realization. The proof is a one-line wrapper that reduces the claim to embed_injective after extracting the generator from the laws and projecting via Subtype.val.
claimLet $C$ be a comparison operator on positive reals that satisfies the laws of logic. Then the map sending each element of the forced arithmetic to its image in the positive-ratio orbit is injective.
background
The LogicRealization module supplies a setting-independent interface that maps distinct Law-of-Logic realizations (continuous positive ratios, discrete propositions, categorical settings) into a common object. A ComparisonOperator is a function ℝ → ℝ → ℝ that assigns a real-valued cost to any pair of positive quantities; SatisfiesLawsOfLogic packages the four Aristotelian constraints together with scale invariance and non-triviality. The positive-ratio orbit interpretation is the concrete map constructed from the generator extracted by generatorOfLawsOfLogic. Upstream, embed_injective states that distinct natural numbers map to distinct points in the orbit {1, γ, γ², …} inside ℝ₊.
proof idea
Term-mode proof. Introduce a and b with equal interpretations; obtain equality of underlying values by congrArg Subtype.val; rewrite both sides with positiveRatioOrbitInterpret_val; apply embed_injective to the generator produced by generatorOfLawsOfLogic h.
why it matters in Recognition Science
This injectivity result is invoked directly by positiveRatio_faithful to establish FaithfulArithmeticInterpretation for the positive-ratio realization. It completes the bridge from abstract logic to concrete positive reals inside the universal forcing program, ensuring that distinct logical elements remain distinct after realization and thereby supporting the chain from the functional equation to arithmetic.
scope and limits
- Does not prove surjectivity of the orbit map onto ℝ₊.
- Applies only when the comparison operator satisfies all laws of logic.
- Does not treat discrete or categorical realizations.
- Does not derive the explicit form of the positive-ratio orbit.
Lean usage
exact positiveRatio_interpret_injective C h habformal statement (Lean)
158theorem positiveRatio_interpret_injective
159 (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
160 Function.Injective (positiveRatioOrbitInterpret C h) := by
proof body
Term-mode proof.
161 intro a b hab
162 have hval := congrArg Subtype.val hab
163 rw [positiveRatioOrbitInterpret_val, positiveRatioOrbitInterpret_val] at hval
164 exact ArithmeticFromLogic.embed_injective
165 (ArithmeticFromLogic.generatorOfLawsOfLogic h) hval
166
167/-- The continuous positive-ratio realization interprets its forced arithmetic
168faithfully into the positive real carrier. -/