`Ledger`

definition

show as: view math explainer →

module: IndisputableMonolith.RecogSpec.Core
domain: RecogSpec
line: 11 · 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 11.

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

   8
   9/-- Basic ledger carrier augmented with optional bookkeeping data so downstream
  10modules can project canonical states without introducing additional structure. -/
  11structure Ledger where
  12  Carrier : Type
  13  state : Option Carrier := none
  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        : ℝ

papers checked against this theorem

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