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

Hypothesis

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)

  39structure Hypothesis (N : ℕ) where
  40  C : Constants
  41  F : Functionals N
  42  /- Projection-Defect (A): D ≤ K_net · C_proj · ||proj_{S⊥}||² -/
  43  projection_defect : ∀ a : State N, F.defectMass a ≤ C.Knet * C.Cproj * F.orthoMass a
  44  /- Energy control (B): ||proj_{S⊥}||² ≤ C_eng · (E−E₀) -/
  45  energy_control    : ∀ a : State N, F.orthoMass a ≤ C.Ceng * F.energyGap a
  46  /- Dispersion/interface (C): ||proj_{S⊥}||² ≤ C_disp · sup tests -/
  47  dispersion        : ∀ a : State N, F.orthoMass a ≤ C.Cdisp * F.tests a
  48
  49/-- Build a CPM `Model` from the hypothesis bundle. -/

used by (40)

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

… and 10 more

depends on (23)

Lean names referenced from this declaration's body.