embed_le_iff_of_one_lt
plain-language theorem explainer
The orbit embedding of LogicNat into positive reals is order-preserving precisely when the generator exceeds one: embed(γ, a) ≤ embed(γ, b) holds if and only if a ≤ b in the LogicNat order. Researchers deriving arithmetic from the Recognition Science functional equation cite this when lifting the induced partial order on the generator orbit. The proof is a one-line rewrite that converts both embeddings to natural-number powers of γ.value and invokes the power-order equivalence together with the Nat-LogicNat order isomorphism.
Claim. Let γ be a generator with γ > 1. For a, b in LogicNat, embed(γ, a) ≤ embed(γ, b) if and only if a ≤ b, where embed maps identity to 1 and step n to γ ⋅ embed(γ, n).
background
Generator is the structure of a positive real value ≠ 1, obtained as the non-trivial witness from SatisfiesLawsOfLogic. LogicNat is the inductive type whose constructors identity and step generate the orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by γ and containing the multiplicative identity. The embed function is defined recursively by embed(γ, identity) = 1 and embed(γ, step n) = γ.value ⋅ embed(γ, n). Upstream, embed_eq_pow shows this equals γ.value raised to the underlying Nat index, while toNat_le recovers the LogicNat partial order from the standard Nat order. The local setting is ArithmeticFromLogic, which extracts Peano arithmetic and order directly from the Law of Logic functional equation.
proof idea
One-line wrapper that rewrites both sides via embed_eq_pow, applies pow_le_pow_iff_of_one_lt under the hypothesis 1 < γ.value, and finishes with the backward direction of toNat_le to equate the LogicNat order with the Nat order.
why it matters
This monotonicity result is required to recover ordered arithmetic inside the Recognition framework before lifting to HamiltonianEmergence and SpinStatistics constructions. It directly supports the chain from the functional equation through the generator orbit to integer inequalities, consistent with the T0–T8 forcing sequence that extracts spatial dimensions and constants from the same logic. No downstream uses are recorded yet, but the lemma closes an essential order-recovery step in the arithmetic foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.