log_generator_ne_zero

formal source

 605here. -/
 606
 607/-- Logarithm of a non-trivial generator is non-zero. -/
 608private theorem log_generator_ne_zero (γ : Generator) :
 609    Real.log γ.value ≠ 0 := by
 610  intro h
 611  -- Real.log_eq_zero_iff: log x = 0 ↔ x = 0 ∨ x = 1 ∨ x = -1
 612  rcases (Real.log_eq_zero.mp h) with h0 | h1 | hneg
 613  · exact (lt_irrefl (0 : ℝ)) (h0 ▸ γ.pos)
 614  · exact γ.nontrivial h1
 615  · linarith [γ.pos]
 616
 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