pith. machine review for the scientific record. sign in
theorem

embed_injective

proved
show as:
view math explainer →
module
IndisputableMonolith.Foundation.ArithmeticFromLogic
domain
Foundation
line
620 · github
papers citing
139 papers (below)

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.ArithmeticFromLogic on GitHub at line 620.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 617/-- **Embedding injectivity**: distinct natural numbers map to distinct
 618points in the orbit. This closes the bridge from the abstract `LogicNat`
 619to the concrete orbit `{1, γ, γ², ...}` in ℝ₊. -/
 620theorem embed_injective (γ : Generator) : Function.Injective (embed γ) := by
 621  intro a b hab
 622  -- Translate to powers.
 623  rw [embed_eq_pow, embed_eq_pow] at hab
 624  -- Take logs.
 625  have hpos_a : 0 < γ.value ^ (LogicNat.toNat a) := pow_pos γ.pos _
 626  have hpos_b : 0 < γ.value ^ (LogicNat.toNat b) := pow_pos γ.pos _
 627  have hlog : Real.log (γ.value ^ (LogicNat.toNat a))
 628              = Real.log (γ.value ^ (LogicNat.toNat b)) := by
 629    exact congrArg Real.log hab
 630  rw [Real.log_pow, Real.log_pow] at hlog
 631  -- Cancel the non-zero log γ.value.
 632  have hne := log_generator_ne_zero γ
 633  have hcast : ((LogicNat.toNat a : ℝ)) = ((LogicNat.toNat b : ℝ)) := by
 634    have := mul_right_cancel₀ hne hlog
 635    exact this
 636  have h_nat : LogicNat.toNat a = LogicNat.toNat b := by exact_mod_cast hcast
 637  -- Lift back to LogicNat via the equivalence.
 638  have := congrArg LogicNat.fromNat h_nat
 639  rw [LogicNat.fromNat_toNat, LogicNat.fromNat_toNat] at this
 640  exact this
 641
 642/-! ## Order via the Embedding (γ > 1 case)
 643
 644When `γ > 1`, the orbit is strictly increasing under multiplication
 645by `γ`, and `embed γ` is a strictly monotone embedding of the Peano
 646order on `LogicNat` into `(ℝ, ≤)`. This is the analytic counterpart
 647of the abstract Peano order from Section 5b. -/
 648
 649/-- For `γ > 1`, `γⁿ ≤ γᵐ ↔ n ≤ m` on `Nat`. -/
 650private theorem pow_le_pow_iff_of_one_lt {γ : ℝ} (hγ : 1 < γ) (n m : Nat) :