`UnitsEqv`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RecogSpec.Core on GitHub at line 21.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  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 ℝ :=
  48  Subfield.closure ({φ} : Set ℝ)
  49
  50/-- The value `x` is algebraic over the subfield generated by `φ` using field
  51operations. -/

papers checked against this theorem

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