embed_lt_iff_of_one_lt

formal source

 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)**. -/
 679theorem embed_lt_iff_of_one_lt (γ : Generator) (hγ : 1 < γ.value) (a b : LogicNat) :
 680    embed γ a < embed γ b ↔ a < b := by
 681  rw [embed_eq_pow, embed_eq_pow, pow_lt_pow_iff_of_one_lt hγ, ← LogicNat.toNat_lt]
 682
 683/-- **Embedding is strictly monotone for γ > 1**. -/
 684theorem embed_strictMono_of_one_lt (γ : Generator) (hγ : 1 < γ.value) :
 685    StrictMono (embed γ) :=
 686  fun _ _ h => (embed_lt_iff_of_one_lt γ hγ _ _).mpr h
 687
 688/-! ## Summary
 689
 690  Law of Logic (four Aristotelian conditions on a comparison operator)
 691        ↓  (forces, via Translation Theorem and Aczél)
 692  J(x) = ½(x + x⁻¹) − 1 with unique zero at x = 1, positive elsewhere
 693        ↓  (the orbit of any γ ≠ 1 under multiplication has Peano shape)
 694  LogicNat (zero, succ, induction)
 695        ↓  (recovery theorem, this module)
 696  Nat with addition and multiplication
 697
 698The Peano axioms are theorems. Addition and multiplication are forced
 699by the orbit structure. No positional representation is assumed. The
 700only structural choice is the generator γ ≠ 1, which exists by
 701non-triviality of the comparison operator.
 702
 703What this module establishes is the recovery of the abstract Peano
 704structure. What it does not yet establish (left for a follow-up
 705module) is:
 706
 707  - Injectivity of `embed γ` (forced by J-positivity off-identity)
 708  - Generator-free characterization of the orbit
 709  - Order on `LogicNat` (forced by the cost ordering on the orbit)