gap_sync_unique
plain-language theorem explainer
The theorem shows that for D ranging from 1 to 8, the condition lcm(2^D, 45) equals 360 forces D to equal 3. Recognition Science researchers deriving spatial dimensions from the forcing chain cite this to lock in uniqueness of three dimensions before building the Q3 cube structure. The proof reduces to a single decidable check over the finite Fin 8 domain.
Claim. For every integer $D$ with $1 ≤ D ≤ 8$, if lcm($2^D$, 45) = 360 then $D$ = 3.
background
The SpectralEmergence module starts from the forced datum D = 3 in the UnifiedForcingChain and constructs the binary cube Q3 with 8 vertices. Face pairs count the opposite-face axes on the D-cube; one sibling definition sets this equal to D while another uses D(D-1)/2. The gap-45 synchronization enters via upstream results from Gap45.Derivation.gap and Masses.AnchorPolicy.gap, which supply the integer 45 appearing in the lcm argument.
proof idea
The proof is a one-line wrapper that invokes the decidable tactic on the finite quantification over Fin 8, evaluating the lcm predicate for each candidate D and confirming the implication holds only at D = 3.
why it matters
This declaration completes the uniqueness step for D = 3 inside the T8 forcing chain, ensuring the eight-tick octave and subsequent Q3 symmetry (order 48) are the only structures compatible with gap synchronization. It directly supports the module's derivation of SU(3) × SU(2) × U(1) gauge content and three particle generations from face-pair count. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.