EWBreakingChannel
plain-language theorem explainer
This definition enumerates the five electroweak symmetry breaking channels that locate the Higgs vacuum expectation value at the J-cost minimum. A physicist modeling Yukawa hierarchies or electroweak symmetry breaking in the Recognition Science framework cites the enumeration to fix the configuration dimension at five. The definition proceeds by direct inductive construction of the five cases with automatic derivation of decidable equality and finite-type instances.
Claim. The electroweak symmetry breaking channels consist of the top-quark loop, bottom-quark loop, tau-lepton loop, $W$-boson loop, and $Z$-boson loop.
background
The module derives the Higgs vacuum expectation value from the J-cost by modeling electroweak breaking through five canonical channels that set the configuration dimension to five. The J-cost is the recognition cost function applied to Yukawa ratios, with the minimum occurring when the top Yukawa is unity. The local setting states that $v_H$ approximately 246 GeV sits at this recognition minimum between the top Yukawa near one and the smaller charged-fermion Yukawas.
proof idea
The declaration is a direct inductive definition that lists the five constructors and derives the type-class instances for decidable equality, representation, boolean equality, and finite type in a single step.
why it matters
The enumeration supplies the five channels required by the cardinality theorem and the Higgs VEV certification structure. It fills the S1/A1 depth step in the Higgs vacuum expectation value derivation. Within the Recognition Science framework the five channels realize the J-cost minimum that fixes the scale near 246 GeV when the top Yukawa equals one.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.