generatorOfLawsOfLogic
plain-language theorem explainer
A comparison operator satisfying the laws of logic determines an explicit non-trivial generator in the positive reals. Foundation researchers building arithmetic from functional equations cite this to obtain the concrete starting point for the orbit embedding. The definition applies classical choice to the non-triviality witness and invokes the identity law to exclude the unit element.
Claim. Let $C$ be a comparison operator satisfying the laws of logic. Then the generator is the positive real $x$ extracted from the non-triviality condition such that the derived cost $C(x,1)neq 0$, with the structure record carrying $0<x$ and $xneq 1$.
background
The module constructs natural numbers and arithmetic from the laws of logic. A ComparisonOperator maps pairs of positive reals to a real-valued cost. SatisfiesLawsOfLogic encodes the four Aristotelian constraints plus scale invariance and non-triviality. The Generator structure is a positive real value distinct from one; its existence is guaranteed by the non_trivial field of SatisfiesLawsOfLogic. LogicNat is the inductive type whose constructors identity and step mirror the orbit under repeated multiplication by the generator. Upstream results include the definition of derivedCost as $C(r,1)$ and the identity law that forces derivedCost at one to vanish.
proof idea
The definition selects $x$ via Classical.choose on the non_trivial witness of hLaws, obtaining $0<x$ and derivedCost $C x neq 0$. It assembles the Generator record with this value and positivity proof. The nontrivial field is discharged by assuming equality to one, rewriting to show derivedCost $C 1=0$, and applying the identity law at one to reach a contradiction with the choice specification.
why it matters
This definition supplies the explicit generator required by downstream orbit interpretations in LogicRealization. It is invoked in positiveRatioOrbitInterpret_val to embed LogicNat via repeated multiplication and in positiveRatio_interpret_injective to establish injectivity of the embedding. Within the Recognition framework it closes the structural chain from SatisfiesLawsOfLogic to arithmetic generators, enabling the passage from the functional equation to the phi-ladder and subsequent forcing steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Intrinsic rewards must be strictly concave in reciprocal occupancy
"invariance under the agent-environment interaction and congruent Markov morphisms"