pow_le_pow_iff_of_one_lt
plain-language theorem explainer
For real γ > 1 and natural numbers n, m the power inequality γ^n ≤ γ^m holds exactly when n ≤ m. The embedding monotonicity result in the same module cites this fact to establish order preservation under the power-based map from LogicNat. The proof splits the biconditional, derives a contradiction via the strict power lemma for the forward direction, and applies the standard monotonicity lemma for the reverse.
Claim. Let γ be a real number with γ > 1 and let n, m be natural numbers. Then γ^n ≤ γ^m if and only if n ≤ m.
background
The module ArithmeticFromLogic derives basic arithmetic on LogicNat from the functional equation in LogicAsFunctionalEquation. LogicNat is the inductive type with zero and succ constructors equipped with an embedding into the reals via repeated multiplication by a generator γ. The present theorem supplies the order comparison for that embedding when γ exceeds 1.
proof idea
Constructor splits the biconditional. The forward direction assumes γ^n ≤ γ^m, negates n ≤ m to obtain m < n, invokes pow_lt_pow_right₀ to produce the strict reverse inequality γ^m < γ^n, and closes with linarith. The reverse direction applies pow_le_pow_right₀ directly to the assumption γ > 1 and the inequality n ≤ m.
why it matters
The result is invoked by embed_le_iff_of_one_lt, whose doc-comment states it establishes that the embedding is order-preserving. This step is required to transfer the order on LogicNat into the reals while constructing arithmetic from the Recognition functional equation, supporting later comparisons on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.