D4_fails_sync
plain-language theorem explainer
The theorem shows that dimension 4 violates a synchronization condition by yielding lcm(16,45) = 720 rather than 360. Researchers deriving gauge groups and fermion counts from the binary cube Q3 would cite it to exclude D=4. The proof is a direct native computation of the inequality on natural numbers.
Claim. The least common multiple of $2^4$ and 45 is not equal to 360.
background
The Spectral Emergence module starts from T8 forcing D=3, which produces the binary cube Q3 with 8 vertices and automorphism group of order 48. This group matches the 48 chiral fermion states in the Standard Model and decomposes into SU(3) x SU(2) x U(1) sectors. The synchronization condition with 45 appears as a numerical requirement tied to the eight-tick octave period and the phi-ladder mass hierarchy.
proof idea
The proof is a one-line term that applies native_decide to evaluate the inequality directly on the natural numbers.
why it matters
This result closes one escape route in the forcing chain by showing D=4 fails the synchronization test required for Q3 structure. It supports the module claim that only D=3 produces the observed gauge content, three generations, and 48 fermionic degrees of freedom. The parent results are the derivations of SU(3) x SU(2) x U(1) and the phi-ladder from the same cube.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.