positiveRatioOrbitInterpret_val
plain-language theorem explainer
The theorem equates the value component of the positive-ratio orbit interpretation of any LogicNat element to the arithmetic embedding of the generator extracted from a comparison operator satisfying the laws of logic. Researchers building setting-independent realizations for the Universal Forcing program cite it when embedding continuous positive-ratio models into the common arithmetic interface. The proof is a direct induction on the LogicNat structure that reduces via the definitions of embed and generatorOfLawsOfLogic.
Claim. Let $C$ be a comparison operator and $h$ a proof that $C$ satisfies the laws of logic. For any $n$ in the natural numbers generated by the law of logic, the first component of the positive-ratio orbit interpretation of $n$ equals the embedding into the positive reals of the generator derived from $h$ applied to $n$.
background
The LogicRealization module supplies a setting-independent interface for the Universal Forcing program. Different Law-of-Logic realizations (continuous positive ratios, discrete propositions, categorical settings) map into a common object that can be compared and composed. LogicNat is the inductive type whose constructors identity and step generate the orbit {1, γ, γ², …} under multiplication by a positive generator γ. generatorOfLawsOfLogic extracts an explicit generator from any proof that a comparison operator satisfies the laws of logic, using the non-triviality witness to guarantee a value strictly greater than 1. embed maps LogicNat into the positive reals by sending identity to 1 and each step to multiplication by the generator value.
proof idea
The proof is by induction on n. The identity case is immediate by reflexivity. The step case applies simplification using the definitions of positiveRatioOrbitInterpret, embed, generatorOfLawsOfLogic, and the inductive hypothesis on the predecessor.
why it matters
The result is invoked by positiveRatio_interpret_injective to obtain injectivity of the orbit map. It supplies the concrete embedding of continuous positive-ratio realizations into the generator-based arithmetic interface, completing one direction of the setting-independent mapping required by the LogicRealization module for the Universal Forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.