SectorGauge
plain-language theorem explainer
SectorGauge packages the three real parameters that set the multiplicative amplitude and additive offset for aligning the phi-ladder inside each fermionic sector. Mass-spectrum calculations that start from the eight-tick octave and cube-derived r0 values cite this record when tabulating concrete yardsticks. The declaration is a plain structure definition whose three fields carry no computational content or proof obligations.
Claim. A sector gauge is a triple $(B_B, r_0, m) $ with $B_B, r_0, m : ℝ$, where $B_B$ is the multiplicative amplitude, $r_0$ is the additive rung offset (including global phase), and $m$ is the empirical mismatch percentage.
background
The module formalizes sector-global gauge parameters that align the phi-ladder across fermionic sectors. The inductive type Sector distinguishes Lepton, UpQuark, DownQuark and Electroweak, while the upstream r0 definition supplies the derived integer offsets (62 for leptons, 35 for up-quarks, -5 for down-quarks, 55 for electroweak) obtained from wallpaper and cube geometry. Additional upstream material includes the rung function, the eight-tick phase map kπ/4, and the Lepton inductive type.
proof idea
Record definition that simply declares the three fields B_B, r0 and mismatch; no tactics or lemmas are applied.
why it matters
SectorGauge supplies the common type instantiated by the four concrete gauges (lepton_gauge, up_quark_gauge, down_quark_gauge, ew_vector_gauge) that feed the mass formula yardstick · φ^(rung-8+gap(Z)). It therefore bridges the abstract T5 J-uniqueness and T7 eight-tick octave to numerical sector predictions inside the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.