lemma other other

`phi_ne_one`

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

formal statement (Lean)

  41lemma phi_ne_one : phi ≠ 1 := ne_of_gt one_lt_phi

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

Jcost_phi_pos in IndisputableMonolith.Constants decl_use
dmCrossSection_pos in IndisputableMonolith.Cosmology.DarkMatterXENONPrediction decl_use
hubble_tension_pos in IndisputableMonolith.Cosmology.HubbleTensionFromBIT decl_use
jcost_phi_pos in IndisputableMonolith.Cosmology.HubbleTensionFromBIT decl_use
J_phi_pos in IndisputableMonolith.Foundation.SpectralEmergence decl_use
phi_ne_one in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
Jcost_phi_pos in IndisputableMonolith.NumberTheory.UniformFailureFloor decl_use
phiSpacing_jcost_pos in IndisputableMonolith.Physics.PhiVsUniformPulseSpacingCert decl_use
lambdaA_ne_zero in IndisputableMonolith.RecogSpec.Scales decl_use

Lean names referenced from this declaration's body.