positiveRatio_faithful
plain-language theorem explainer
The positive-ratio realization embeds the forced LogicNat arithmetic injectively into the positive reals when the comparison operator satisfies the laws of logic. Researchers tracing the Universal Forcing program would cite this result to confirm no collapse occurs in the continuous carrier. The proof constructs the FaithfulArithmeticInterpretation by invoking the dedicated injectivity lemma for positive ratios and reducing the non-collapse condition to the upstream Peano axiom via that injectivity.
Claim. Let $C$ be a comparison operator on positive reals that satisfies the laws of logic. Then the logic realization constructed from $C$ via positive ratios is a faithful arithmetic interpretation: its interpretation function is injective, and the image of the identity element is distinct from the image of any successor in the forced natural numbers.
background
The module supplies a setting-independent interface for realizations of the laws of logic. A LogicRealization packages a carrier type, a cost type with zero, a comparison map, and a zero element together with structural propositions. FaithfulArithmeticInterpretation requires that the interpretation of the forced arithmetic (the inductive type with identity and step constructors mirroring the orbit under multiplication by the generator) into the carrier is injective and that the zero element remains distinct from all its successors. Upstream, the inductive type encodes the orbit generated by repeated application of the non-trivial generator starting from the multiplicative identity. The theorem zero_ne_succ asserts that this identity is distinguishable from any successor. SatisfiesLawsOfLogic collects the four Aristotelian constraints, scale invariance, and non-triviality for the comparison operator. The positive-ratio realization uses the positive reals as carrier with the cost derived from the comparison operator under scale invariance.
proof idea
The proof is a direct tactic construction of the two fields of FaithfulArithmeticInterpretation. The injective field is discharged by applying the sibling lemma on positive-ratio interpretation injectivity to the assumed equality of interpretations. The zero_step_noncollapse field reduces the assumed collapse to an equality in the forced natural numbers and invokes the upstream theorem zero_ne_succ after transporting via the injectivity map.
why it matters
This result places the continuous positive-ratio realization on the same footing as the abstract forcing chain by guaranteeing faithful embedding of the arithmetic. It supports the downstream development of the J-cost function and the Recognition Composition Law by ensuring the orbit distinctions survive the interpretation. Within the T0-T8 chain, it secures the base for deriving D=3 and the phi-ladder without arithmetic degeneracy. The module creates the common object into which different Law-of-Logic settings can be mapped, and this theorem discharges the faithfulness obligation for the continuous case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.