pith. machine review for the scientific record. sign in
theorem proved term proof

log_generator_ne_zero

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 608private theorem log_generator_ne_zero (γ : Generator) :
 609    Real.log γ.value ≠ 0 := by

proof body

Term-mode proof.

 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 ℝ₊. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.