positiveRatioOrbitInterpret
plain-language theorem explainer
The definition maps the inductive type of naturals generated by identity and step under the laws of logic into positive reals, sending identity to 1 and each step to multiplication by the positive generator chosen from the non-triviality condition. Researchers constructing continuous realizations cite this map to populate the carrier object in the setting-independent interface. It is defined by recursion on the two constructors, selecting the generator once via classical choice and propagating positivity.
Claim. Let $C$ be a comparison operator satisfying the laws of logic. Define the map from the inductive type of naturals generated by the laws of logic to positive reals by sending the base element to $1$ and each successor to multiplication by the generator $γ > 0$ selected from the non-triviality axiom.
background
The inductive type of naturals generated by the laws of logic consists of an identity constructor representing the zero-cost multiplicative identity and a step constructor representing iteration of a generator, forming the orbit {1, γ, γ², …} in positive reals. As described upstream, identity represents the zero-cost element (the multiplicative identity in the orbit) while step represents one more iteration of the generator. A comparison operator assigns a real-valued cost to pairs of positive quantities, and the structure requiring it to satisfy the laws of logic includes axioms for identity, non-contradiction, excluded middle, scale invariance, and route independence, along with non-triviality.
proof idea
The definition is given explicitly by cases on the constructors of the inductive type. The identity case returns the positive real 1. The step case selects the generator γ using classical choice from the non-triviality field, recurses to obtain the value for the predecessor, and returns their product while proving positivity from the product of positives.
why it matters
This definition provides the embedding of the forced arithmetic into the positive-ratio carrier, which is used to construct the LogicRealization instance via the embedding function. It supports the injectivity theorem and the valuation theorem that relate the interpretation back to the arithmetic embedding. Within the Recognition Science framework, it realizes one concrete model of the logic-forced naturals in the continuous setting, contributing to the interface that allows different logic settings to feed into the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.