embed_lt_iff_of_one_lt
plain-language theorem explainer
The result establishes that the orbit embedding of logic naturals into positive reals preserves and reflects strict order when the generator value exceeds 1. Workers deriving arithmetic from the Law of Logic would cite this to confirm monotonicity of the forced naturals. The proof is a direct term reduction that rewrites the embedding as a power and invokes the corresponding natural-number inequality.
Claim. Let $γ$ be a generator with value greater than 1. For any $a, b$ in the logic naturals, the orbit embedding satisfies $embed(γ, a) < embed(γ, b)$ if and only if $a < b$.
background
The module constructs arithmetic structures from the functional equation of logic. LogicNat is the inductive type with identity (zero-cost element) and step constructors, forming the smallest subset of positive reals closed under multiplication by the generator and containing 1. A Generator is any positive real other than 1, extracted via the non-triviality field of SatisfiesLawsOfLogic.
proof idea
The proof is a one-line term-mode wrapper. It rewrites both embeddings via embed_eq_pow to obtain powers of the generator value. It then applies pow_lt_pow_iff_of_one_lt to convert the real inequality into an exponent comparison. The final step uses toNat_lt to transfer the order back to the logic naturals.
why it matters
This supplies the order equivalence needed for the immediate downstream theorem embed_strictMono_of_one_lt, which asserts that the embedding is a strict monotone map. It advances the extraction of Peano arithmetic from the single functional equation without external number axioms. In the Recognition Science setting it supports the initial segment of the forcing chain by ensuring the discrete orbit respects order, a prerequisite for later steps such as the self-similar fixed point and emergence of spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.