GenerationStructure
plain-language theorem explainer
GenerationStructure records the pair of real rung gaps separating the three fermion generations according to cubic voxel topology. Researchers assembling unified lepton and quark spectra in the Recognition Science ladder model cite this record when populating concrete hierarchies. It is introduced as a bare structure with two real fields and carries no proof obligations.
Claim. A generation structure is a pair of real numbers $(Δ_1, Δ_2)$ encoding the topological separations between consecutive fermion generations, where $Δ_1$ is the gap from the first to the second generation and $Δ_2$ from the second to the third (with values 11 and 6 for leptons).
background
The module unifies discrete ladder positions for all fermion sectors by placing particles on the phi-ladder whose steps follow from the Recognition Composition Law. Topological gaps are taken from the cubic voxel, supplying the fixed integers E_p = 11 and F = 6. The module note distinguishes the integer-rung lepton core from the quarter-ladder hypothesis lane used for quarks. Upstream, the Lepton inductive type enumerates the six lepton states whose mass ordering is governed by these gaps.
proof idea
The declaration is a pure structure definition that introduces the two real fields with no body, no tactics, and no proof obligations. It functions solely as the shared carrier type instantiated by the concrete hierarchy records defined later in the same module.
why it matters
GenerationStructure supplies the common type for lepton_hierarchy and quark_hierarchy, which together realize the three-generation model across fermion sectors. It directly encodes the Generation Torsion Universality claim that the gaps originate from cubic voxel topology (E_p = 11, F = 6). In the Recognition framework it supports the discrete mass formula on the phi-ladder and the forcing chain that fixes D = 3 dimensions. The quark portion remains provisional under the Gap 6 hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.