T_min_at_D3
plain-language theorem explainer
The declaration fixes the minimal Hamiltonian cycle period T_min at spatial dimension D=3 to the integer 8. Mass ladder constructions in Recognition Science cite this value to anchor the baseline rung on the phi-ladder before applying the yardstick scaling. The proof is a one-line native_decide evaluation that unfolds the definition of T_min as the vertex count of the 3-cube.
Claim. At spatial dimension $D=3$, the minimal Hamiltonian cycle period $T_min(D)$ equals 8, where $T_min(d)$ is the vertex count of the $d$-cube.
background
The module upgrades several boundary assumptions to derived status by applying standard cube combinatorics at fixed D=3. T_min(d) is defined as the Hamiltonian cycle period on the d-cube Q_d, which equals the vertex count 2^d. The local setting derives the octave offset B-15 as -T_min = -2^D = -8 together with neutrino baseline, lepton baseline, and generation ordering from the same geometric input.
proof idea
The proof is a one-line term that applies native_decide to the closed term T_min 3. This reduces directly to the definition cube_vertices 3 and evaluates the power of two without further lemmas.
why it matters
The result supplies the octave offset -8 that enters the mass formula yardstick * phi^(rung - 8 + gap(Z)). It closes derivation B-15 in the cube-geometry module and supports the eight-tick octave landmark T7 together with D=3 from T8. No open scaffolding remains for this evaluation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.