`Bridge`

definition

show as: view math explainer →

module: IndisputableMonolith.RecogSpec.Core
domain: RecogSpec
line: 17 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RecogSpec.Core on GitHub at line 17.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  14  tick : Option (Carrier → ℕ) := none
  15
  16/-- Bridge over a ledger. -/
  17structure Bridge (L : Ledger) : Type where
  18  dummy : Unit := ()
  19
  20/-- Units equivalence relation over bridges. -/
  21structure UnitsEqv (L : Ledger) : Type where
  22  Rel   : Bridge L → Bridge L → Prop
  23  refl  : ∀ B, Rel B B
  24  symm  : ∀ {B₁ B₂}, Rel B₁ B₂ → Rel B₂ B₁
  25  trans : ∀ {B₁ B₂ B₃}, Rel B₁ B₂ → Rel B₂ B₃ → Rel B₁ B₃
  26
  27/-- Dimensionless predictions extracted from a bridge. -/
  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. -/
  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 `φ`. -/
  47def phiSubfield (φ : ℝ) : Subfield ℝ :=

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.