structure definition def or abbrev

`DimlessPack`

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

formal statement (Lean)

  28structure DimlessPack (L : Ledger) (B : Bridge L) : Type where
  29  alpha            : ℝ
  30  massRatios       : LeptonMassRatios
  31  mixingAngles     : CkmMixingAngles
  32  g2Muon           : ℝ
  33  strongCPNeutral  : Prop
  34  eightTickMinimal : Prop
  35  bornRule         : Prop
  36
  37/-- Absolute (SI) packaging for reference displays, distinct from dimensionless pack. -/

used by (1)

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

Matches in IndisputableMonolith.RecogSpec.Core decl_use

depends on (8)

Lean names referenced from this declaration's body.

alpha in IndisputableMonolith.Constants.Alpha decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
L in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use
Bridge in IndisputableMonolith.RecogSpec.Core decl_use
CkmMixingAngles in IndisputableMonolith.RecogSpec.ObservablePayloads decl_use
LeptonMassRatios in IndisputableMonolith.RecogSpec.ObservablePayloads decl_use