pith. machine review for the scientific record. sign in
def definition def or abbrev

model

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  50noncomputable def model {N : ℕ} (H : Hypothesis N) : Model (State N) :=

proof body

Definition body.

  51  { C := H.C
  52    defectMass := H.F.defectMass
  53    orthoMass  := H.F.orthoMass
  54    energyGap  := H.F.energyGap
  55    tests      := H.F.tests
  56    projection_defect := H.projection_defect
  57    energy_control    := H.energy_control
  58    dispersion        := H.dispersion }
  59
  60/-- Pack the `Model` into the bridge-local `CPMBridge` structure (for traceability notes). -/

used by (40)

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

… and 10 more

depends on (17)

Lean names referenced from this declaration's body.