theorem proved term proof

`phi_lt_two`

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

formal statement (Lean)

 168theorem phi_lt_two : phi < 2 := by

proof body

Term-mode proof.

 169  linarith [Constants.phi_lt_onePointSixTwo]
 170
 171/-- e > φ: Euler's number exceeds the golden ratio. -/

used by (23)

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

ml_from_phi_tier_structure in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
ml_matches_stellar_observations in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
ml_geometric_bounds in IndisputableMonolith.Astrophysics.ObservabilityLimits decl_use
high_tc_superconductivity_structure in IndisputableMonolith.CondensedMatter.HighTcSuperconductivityStructure decl_use
phi_lt_two in IndisputableMonolith.Constants decl_use
vev_phi_window in IndisputableMonolith.Constants.ElectroweakVEVStructure decl_use
delta_w0_max_lt_one in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use
Jcost_phi_bounds in IndisputableMonolith.Cosmology.Sigma8Suppression decl_use
phi_lt_two in IndisputableMonolith.Derivations.MassToLight decl_use
log_phi_lt_one in IndisputableMonolith.Ecology.BiodiversityScalingFromJCost decl_use
log_phi_lt_sevenTenths in IndisputableMonolith.Ecology.BiodiversityScalingFromJCost decl_use
spacing_below_two in IndisputableMonolith.Education.PedagogyOptimalRateFromGap45 decl_use
phi_lt_two in IndisputableMonolith.Foundation.PhiForcing decl_use
phi_perturbation_bounded in IndisputableMonolith.Foundation.StillnessGenerative decl_use
rung_slope_lt_log_two in IndisputableMonolith.Geology.GutenbergRichterFromLedger decl_use
rungPhaseDelay_band in IndisputableMonolith.Gravity.BlackHoleEchoesFromBounce decl_use
C_kernel_pos in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
Omega_0_pos in IndisputableMonolith.Gravity.Inflation decl_use
phi_bit_more_efficient in IndisputableMonolith.Information.RecognitionEntropy decl_use
phi_lt_two in IndisputableMonolith.Information.RecognitionEntropy decl_use
e_gt_phi in IndisputableMonolith.Mathematics.Euler decl_use
ew_scale_structure in IndisputableMonolith.QFT.ElectroweakScaleStructure decl_use
deltaCP_prediction_matches in IndisputableMonolith.StandardModel.PMNSMatrix decl_use

depends on (6)

Lean names referenced from this declaration's body.

phi_lt_onePointSixTwo in IndisputableMonolith.Constants decl_use
phi_lt_two in IndisputableMonolith.Constants decl_use
Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
phi_lt_two in IndisputableMonolith.Derivations.MassToLight decl_use
phi_lt_two in IndisputableMonolith.Foundation.PhiForcing decl_use
phi_lt_two in IndisputableMonolith.Information.RecognitionEntropy decl_use