vev_phi_window
The declaration establishes that the structural scale parameter phi lies strictly between 1 and 2. Physicists modeling electroweak symmetry breaking within Recognition Science cite this to confirm the vacuum expectation value is pinned by the same interval that governs the phi-ladder rather than treated as a free input. The proof is a one-line term that pairs the two inequalities already established for phi in the Constants module.
claim$1 < phi < 2$, where $phi$ is the self-similar fixed point of the Recognition Composition Law that sets the structural scale for the electroweak vacuum expectation value.
background
The module formalizes C-020, which asks what determines the electroweak VEV near 246 GeV. Recognition Science replaces parameter tuning with ledger rung structure on the phi-ladder, where mass scales are given by yardstick times phi to a power determined by rung and gap(Z). The upstream lemma one_lt_phi proves 1 < phi by comparing sqrt(5) to 1 and 2, while phi_lt_two proves phi < 2 by showing sqrt(5) < 3. The definition scale(k) := phi^k supplies the exponential growth along the ladder used in LargeScaleStructureFromRS.
proof idea
The proof is a term-mode constructor that directly supplies the pair of lemmas one_lt_phi and phi_lt_two. No further tactics or reductions are applied; the result simply inherits the two inequalities already shown for phi.
why it matters in Recognition Science
This theorem supplies the interval constraint required by the VEV structural framework in C-020. It supports the broader claim that mass scales arise from ledger rung structure rather than naturalness tuning, consistent with the eight-tick octave and D=3 spatial dimensions forced in the UnifiedForcingChain. Full numeric extraction of the laboratory VEV remains blocked per the module documentation.
formal statement (Lean)
43theorem vev_phi_window : 1 < Constants.phi ∧ Constants.phi < 2 :=
proof body
Term-mode proof.
44 ⟨Constants.one_lt_phi, Constants.phi_lt_two⟩
45
46/-- Electroweak-VEV structure implies `phi ≠ 1` via the inherited scale window. -/