pow_lt_pow_iff_of_one_lt
plain-language theorem explainer
The theorem asserts that for real γ strictly greater than 1, the inequality γ^n < γ^m holds exactly when the natural numbers n and m satisfy n < m. Researchers deriving order-preserving embeddings of LogicNat into the reals cite this result when establishing monotonicity of the power map. The argument splits the biconditional with constructor and invokes the library lemmas pow_le_pow_right₀ (via contradiction) and pow_lt_pow_right₀ (directly).
Claim. For real number $γ > 1$ and natural numbers $n, m$, we have $γ^n < γ^m$ if and only if $n < m$.
background
This result lives in the ArithmeticFromLogic module, which constructs natural-number arithmetic from the logic-as-functional-equation foundation imported from LogicAsFunctionalEquation. LogicNat is the inductive type built from zero and successor primitives; the embedding maps each LogicNat element to a real power of a generator γ. The theorem supplies the order-preservation step needed to translate inequalities between LogicNat values into inequalities between their real images.
proof idea
The term-mode proof begins with constructor to split the biconditional. The forward direction assumes γ^n < γ^m, negates n < m, applies pow_le_pow_right₀ to obtain a non-strict inequality, and closes with linarith. The reverse direction applies the library lemma pow_lt_pow_right₀ directly to the hypotheses 1 < γ and n < m.
why it matters
The lemma is invoked inside embed_lt_iff_of_one_lt to convert the order relation on LogicNat into the order relation on the embedded reals. It thereby completes a basic arithmetic fact required for later Recognition Science constructions such as the phi-ladder and the mass formula. The result sits downstream of the logic functional equation and upstream of embedding monotonicity statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.