theorem
proved
vev_not_free_parameter
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.ElectroweakVEVStructure on GitHub at line 27.
browse module
All declarations in this module, on Recognition.
explainer page
Derivations using this theorem
depends on
used by
formal source
24/-! ## Structural Statement -/
25
26/-- The electroweak scale is ledger-determined in RS. -/
27theorem vev_not_free_parameter : scale_from_ledger :=
28 ew_scale_structure
29
30/-- A minimal structural placeholder for the derived VEV relation. -/
31def vev_from_ledger : Prop := scale_from_ledger
32
33/-- **C-020 Structural**: the electroweak VEV belongs to the same
34ledger-fixed scale hierarchy rather than being an unconstrained
35input parameter. -/
36theorem vev_structure : vev_from_ledger := vev_not_free_parameter
37
38/-- Electroweak-VEV structure implies electroweak-scale structural input. -/
39theorem vev_implies_scale (h : vev_from_ledger) : scale_from_ledger :=
40 h
41
42/-- The VEV structural scale is pinned to the same phi interval. -/
43theorem vev_phi_window : 1 < Constants.phi ∧ Constants.phi < 2 :=
44 ⟨Constants.one_lt_phi, Constants.phi_lt_two⟩
45
46/-- Electroweak-VEV structure implies `phi ≠ 1` via the inherited scale window. -/
47theorem vev_implies_phi_ne_one (_h : vev_from_ledger) : Constants.phi ≠ 1 := by
48 exact ne_of_gt Constants.one_lt_phi
49
50/-! ## Enhanced C-020 Derivation Framework -/
51
52/-- **THEOREM**: The VEV v ≈ 246 GeV sits at a specific rung on the φ-ladder.
53
54 The ladder position is determined by:
55 - Base rung: r_vev = r_e + Δr
56 - where r_e is the electron rung (from T9)
57 - and Δr is the electroweak symmetry breaking step