theorem proved term proof

`dimension_forced`

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

formal statement (Lean)

 383theorem dimension_forced : ∃! D : Dimension, RSCompatibleDimension D := by

proof body

Term-mode proof.

 384  use 3
 385  constructor
 386  · exact D3_compatible
 387  · intro D hD
 388    exact dimension_unique D hD
 389
 390/-! ## Physical Interpretation -/
 391
 392/-- The spatial dimension of the physical world. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

why_D_equals_3 in IndisputableMonolith.Foundation.DimensionForcing decl_use
physical_derivation_cert in IndisputableMonolith.Gap45.PhysicalMotivation decl_use
PhysicalDerivationCert in IndisputableMonolith.Gap45.PhysicalMotivation decl_use

depends on (11)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
Physical in IndisputableMonolith.Bridge.DataCore decl_use
Dimension in IndisputableMonolith.Constants.Dimensions decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
D3_compatible in IndisputableMonolith.Foundation.DimensionForcing decl_use
Dimension in IndisputableMonolith.Foundation.DimensionForcing decl_use
dimension_unique in IndisputableMonolith.Foundation.DimensionForcing decl_use
RSCompatibleDimension in IndisputableMonolith.Foundation.DimensionForcing decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use