theorem proved decidable or rfl

`gap_sync_unique`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 420theorem gap_sync_unique :
 421    ∀ D : Fin 8, Nat.lcm (2 ^ (D.val + 1)) 45 = 360 → D.val + 1 = 3 := by

proof body

Decided by rfl or decide.

 422  decide
 423
 424/-- **THEOREM**: D = 3 is the unique spectral emergence dimension.
 425    For D ∈ {1,..,8}, only D = 3 satisfies gap-45 synchronization
 426    AND has face_pairs ≥ 3. -/

depends on (11)

Lean names referenced from this declaration's body.

has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
face_pairs in IndisputableMonolith.Foundation.ParticleGenerations decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
face_pairs in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
gap in IndisputableMonolith.Gap45.Derivation decl_use
gap in IndisputableMonolith.Masses.AnchorPolicy decl_use
gap in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
gap in IndisputableMonolith.RSBridge.Anchor decl_use