vev_implies_phi_ne_one
plain-language theorem explainer
Electroweak VEV structure on the phi-ladder implies the golden ratio differs from one. Derivations of mass scales in Recognition Science cite this to rule out trivial fixed points. The argument reduces directly to the established inequality one less than phi.
Claim. If the electroweak vacuum expectation value belongs to the ledger-fixed scale hierarchy, then the golden ratio satisfies $phi neq 1$.
background
In the ElectroweakVEVStructure module the definition vev_from_ledger is the proposition that the VEV satisfies the same ledger-derived scale relation as other constants, rather than serving as a free input. This inherits the rung structure and phi-ladder positioning from upstream constants. The lemma one_lt_phi establishes $1 < phi$ via comparison of square roots of 5 and 1 together with algebraic bounds on the golden-ratio expression. The module addresses C-020 on the origin of $v approx 246$ GeV and notes that full numeric extraction remains blocked pending closure of the electron-mass derivation.
proof idea
Term-mode one-line wrapper. It applies the lemma one_lt_phi, which states that phi exceeds one, to obtain the required inequality under the vev_from_ledger hypothesis.
why it matters
The declaration supplies a consistency check inside the C-020 framework for the electroweak VEV. It guarantees that phi-ladder assumptions stay non-degenerate when mass scales are extracted from ledger rungs. It supports sibling results such as vev_implies_scale and vev_phi_window by preserving separation from the degenerate case phi = 1. The underlying landmark is the forcing of phi as the self-similar fixed point of the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.