def definition def or abbrev

`dim`

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

formal statement (Lean)

  70def dim : ℕ := D

proof body

Definition body.

  71
  72/-! ## The Coefficient Derivation -/
  73
  74/-- The Tau Step Coefficient derived from W and D.
  75    Formula: C_tau = W + D/2 -/

used by (27)

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

DimensionedQuantity in IndisputableMonolith.Constants.Dimensions decl_use
DimensionedQuantity in IndisputableMonolith.Constants.Dimensions decl_use
DimensionedQuantity in IndisputableMonolith.Constants.Dimensions decl_use
DimensionedQuantity in IndisputableMonolith.Constants.Dimensions decl_use
robotic_has_6 in IndisputableMonolith.CrossDomain.CubeFaceUniversality decl_use
future_slot_realised in IndisputableMonolith.CrossDomain.ParadigmShiftLattice decl_use
G3 in IndisputableMonolith.CrossDomain.RecognitionGenerators decl_use
conjugate_dim_forced in IndisputableMonolith.Foundation.SpectralEmergence decl_use
fermion_flavors in IndisputableMonolith.Foundation.SpectralEmergence decl_use
gauge_sector_dim in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
Q3_self_dual_vertex_count in IndisputableMonolith.Foundation.SpectralEmergence decl_use
quark_lepton_ratio in IndisputableMonolith.Foundation.SpectralEmergence decl_use
sector_dim_sum in IndisputableMonolith.Foundation.SpectralEmergence decl_use
SpectralEmergenceCert in IndisputableMonolith.Foundation.SpectralEmergence decl_use
SpectralSector in IndisputableMonolith.Foundation.SpectralEmergence decl_use
winding_gives_three_charges in IndisputableMonolith.Foundation.WindingCharges decl_use
tauStepCoefficientDerived in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
tauStepCoefficientDerived_eq in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
tauStepCoefficientDerived_matches_paper in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
s_inverse in IndisputableMonolith.QFT.SMatrixUnitarity decl_use
Covector in IndisputableMonolith.Relativity.Geometry.Manifold decl_use
Manifold in IndisputableMonolith.Relativity.Geometry.Manifold decl_use
partialDeriv in IndisputableMonolith.Relativity.Geometry.Manifold decl_use
Point in IndisputableMonolith.Relativity.Geometry.Manifold decl_use
Spacetime in IndisputableMonolith.Relativity.Geometry.Manifold decl_use
TangentVector in IndisputableMonolith.Relativity.Geometry.Manifold decl_use

depends on (5)

Lean names referenced from this declaration's body.

from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
W in IndisputableMonolith.Masses.Anchor decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
W in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
W in IndisputableMonolith.Physics.MassTopology decl_use