gap_sync_unique
plain-language theorem explainer
The theorem shows that for dimensions d from 1 to 8, the equality lcm(2^d, 45) = 360 holds only when d equals 3. Recognition Science researchers working on spectral emergence from the Q3 cube would cite it to lock in the uniqueness of D=3 before deriving gauge groups and generations. The proof is a direct decidable computation that exhaustively checks the numerical condition over the finite range.
Claim. For every integer $d$ with $1 ≤ d ≤ 8$, if lcm$(2^d, 45) = 360$ then $d = 3$.
background
The module SpectralEmergence derives the Standard Model and consciousness structures from the single datum D=3 (T8). It starts from the binary cube Q3 with 8 vertices, whose automorphism group has order 48 and decomposes into SU(3) × SU(2) × U(1) sectors. Face pairs count the opposite-face axes; one sibling definition sets this equal to D while the module version uses D(D-1)/2, both yielding 3 when D=3. The gap-45 synchronization condition appears via upstream Gap45.Derivation.gap and Masses.AnchorPolicy.gap, which tie the lcm identity to the phi-ladder mass formula and the eight-tick octave (T7).
proof idea
The proof is a one-line wrapper that applies decidable equality checking. Lean evaluates the universal quantifier over the finite type Fin 8 by direct computation of Nat.lcm for each possible D.val + 1 and confirms the implication holds exactly when the dimension equals 3.
why it matters
This declaration closes the uniqueness argument inside the spectral emergence module, ensuring no other dimension in 1..8 satisfies the gap synchronization that feeds the phi-ladder and three-generation structure. It directly supports the module claim that D=3 is the unique spectral emergence dimension and aligns with T8 forcing D=3 together with the Recognition Composition Law. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.