theorem proved term proof

`ew_scale_structure`

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

formal statement (Lean)

  44theorem ew_scale_structure : scale_from_ledger := by

proof body

Term-mode proof.

  45  constructor
  46  · exact ⟨one_lt_phi, phi_lt_two⟩
  47  · intro r
  48    exact no_fine_tuning r
  49
  50/-- Electroweak-scale structure implies the phi-window input. -/

used by (2)

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

vev_not_free_parameter in IndisputableMonolith.Constants.ElectroweakVEVStructure decl_use
has_ew_scale_structure in IndisputableMonolith.Cosmology.WMassAnomalyStructure decl_use

depends on (13)

Lean names referenced from this declaration's body.

one_lt_phi in IndisputableMonolith.Constants decl_use
phi_lt_two in IndisputableMonolith.Constants decl_use
no_fine_tuning in IndisputableMonolith.Cosmology.DarkEnergy decl_use
scale in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS decl_use
phi_lt_two in IndisputableMonolith.Derivations.MassToLight decl_use
no_fine_tuning in IndisputableMonolith.Experimental.UltraDiffuseGalaxies decl_use
phi_lt_two in IndisputableMonolith.Foundation.PhiForcing decl_use
phi_lt_two in IndisputableMonolith.Information.RecognitionEntropy decl_use
phi_lt_two in IndisputableMonolith.Mathematics.Euler decl_use
one_lt_phi in IndisputableMonolith.PhiSupport decl_use
one_lt_phi in IndisputableMonolith.PhiSupport.Lemmas decl_use
no_fine_tuning in IndisputableMonolith.QFT.ElectroweakScaleStructure decl_use
scale_from_ledger in IndisputableMonolith.QFT.ElectroweakScaleStructure decl_use