hierarchy_coherence
plain-language theorem explainer
The theorem establishes that the lepton hierarchy begins with rung spacing 11 while the quark hierarchy begins with spacing 7.75. A physicist modeling fermion mass ladders inside the Recognition Science framework would cite it to confirm both sectors fit the same eight-tick recognition cycle. The proof is a one-line wrapper that applies reflexivity to the lepton definition and normalizes the numerical value of the top-to-bottom step after unfolding the quark definition.
Claim. $Δ_1 = 11$ for the lepton hierarchy and $Δ_1 = 7.75$ for the quark hierarchy, where each $Δ_1$ is the first spacing entry in the respective GenerationStructure record.
background
The module unifies discrete ladder positions across fermion sectors under the eight-tick recognition cycle. Lepton hierarchy is the GenerationStructure record with first spacing 11 and second spacing 6. Quark hierarchy is the GenerationStructure record whose first spacing is taken from the top-to-bottom step, defined as the rational 31/4 in MixingGeometry.
proof idea
The proof is a one-line wrapper. Constructor splits the conjunction; reflexivity matches the lepton definition directly; unfolding the quark definition together with step_top_bottom exposes the rational 31/4, which norm_num reduces to the decimal 7.75.
why it matters
The declaration confirms structural coherence of the three-generation model by placing both hierarchies inside the same 8-tick cycle (T7). It fills the Hierarchy Coherence step of the Unified Generation Hierarchy module. The result touches the open question of reconciling integer-rung core spectra with quarter-ladder quark coordinates noted in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.