structure definition def or abbrev

`AbsolutePack`

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

formal statement (Lean)

  38structure AbsolutePack (L : Ledger) (B : Bridge L) : Type where
  39  c_SI        : ℝ
  40  hbar_SI     : ℝ
  41  G_SI        : ℝ
  42  Lambda_SI   : ℝ
  43  masses_SI   : List ℝ
  44  energies_SI : List ℝ
  45
  46/-- Subfield generated by `φ`. -/

depends on (10)

Lean names referenced from this declaration's body.

c_SI in IndisputableMonolith.Constants.ExternalAnchors decl_use
G_SI in IndisputableMonolith.Constants.ExternalAnchors decl_use
hbar_SI in IndisputableMonolith.Constants.ExternalAnchors decl_use
c_SI in IndisputableMonolith.Cosmology.SIConversion decl_use
c_SI in IndisputableMonolith.Measurement.RSNative.Calibration.SingleAnchor decl_use
hbar_SI in IndisputableMonolith.Measurement.RSNative.Calibration.SingleAnchor decl_use
L in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use
Bridge in IndisputableMonolith.RecogSpec.Core decl_use
c_SI in IndisputableMonolith.RRF.Foundation.Constants decl_use