embed_le_iff_of_one_lt
Embedding monotonicity for generators exceeding one shows that the orbit map from logic naturals to positive reals preserves order. Researchers deriving arithmetic from the Law of Logic cite it to confirm that inequalities on the orbit lift correctly. The term proof reduces both sides to powers of the generator value and applies the standard power comparison on natural numbers.
claimLet $a, b$ be elements of the logic naturals and let $γ$ be a generator with value greater than 1. Then the orbit embedding satisfies $ι_γ(a) ≤ ι_γ(b)$ if and only if $a ≤ b$.
background
In ArithmeticFromLogic the logic naturals are the inductive type with constructors identity (the zero-cost multiplicative identity) and step (one further multiplication by the generator). A generator is a positive real distinct from 1, extracted from the non-triviality clause of the Law of Logic. The orbit embedding maps identity to 1 and each step recursively to multiplication by the generator value, which equals that value raised to the corresponding natural-number index.
proof idea
One-line wrapper that rewrites both embeddings via embed_eq_pow, applies pow_le_pow_iff_of_one_lt under the hypothesis that the generator value exceeds 1, and finishes with the order equivalence supplied by toNat_le.
why it matters in Recognition Science
The result secures order preservation for the orbit embedding, a prerequisite for consistent arithmetic derivations from the functional equation. It supports later constructions that rely on monotonicity of the phi-ladder and mass formulas, even though no direct downstream use is recorded in the current graph. In the Recognition chain it completes the arithmetic layer that precedes Hamiltonian emergence and spin-statistics statements.
scope and limits
- Does not apply when the generator value is at most 1.
- Does not separate the strict-inequality case.
- Does not extend the order comparison beyond the induced Nat order.
- Does not address embeddings into structures other than the positive reals.
formal statement (Lean)
674theorem embed_le_iff_of_one_lt (γ : Generator) (hγ : 1 < γ.value) (a b : LogicNat) :
675 embed γ a ≤ embed γ b ↔ a ≤ b := by
proof body
Term-mode proof.
676 rw [embed_eq_pow, embed_eq_pow, pow_le_pow_iff_of_one_lt hγ, ← LogicNat.toNat_le]
677
678/-- **Embedding strict monotonicity (γ > 1)**. -/