lemma proved term proof

`lambdaA_ne_zero`

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

formal statement (Lean)

 100lemma lambdaA_ne_zero : lambdaA ≠ 0 := by

proof body

Term-mode proof.

 101  have hpos : 0 < Constants.phi := Constants.phi_pos
 102  have hne1 : Constants.phi ≠ 1 := Constants.phi_ne_one
 103  simpa [lambdaA] using Real.log_ne_zero_of_pos_of_ne_one hpos hne1
 104

depends on (4)

Lean names referenced from this declaration's body.

phi_ne_one in IndisputableMonolith.Constants decl_use
Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
phi_ne_one in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
lambdaA in IndisputableMonolith.RecogSpec.Scales decl_use