theorem proved term proof

`cube_uniqueness`

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

formal statement (Lean)

 136theorem cube_uniqueness :
 137    ∀ D : ℕ, (linkingNumber D ≠ 0) ↔ D = 3 := by

proof body

Term-mode proof.

 138  intro D
 139  constructor
 140  · intro h
 141    unfold linkingNumber at h
 142    split_ifs at h with hD
 143    · exact hD
 144    · contradiction
 145  · intro h
 146    rw [h]
 147    unfold linkingNumber
 148    simp
 149
 150/-! ## 8-Tick Uniqueness -/
 151
 152/-- A Gray code cycle of length T on D dimensions. -/

depends on (15)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
T in IndisputableMonolith.Foundation.Breath1024 decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
Tick in IndisputableMonolith.Foundation.TimeEmergence decl_use
T in IndisputableMonolith.Gap45.SyncMinimization decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
Tick in IndisputableMonolith.Masses.Ribbons decl_use
Tick in IndisputableMonolith.Masses.Ribbons.Tick decl_use
Tick in IndisputableMonolith.Measurement.RSNative.Core decl_use
linkingNumber in IndisputableMonolith.Meta.LedgerUniqueness decl_use
A in IndisputableMonolith.Modal.Actualization decl_use