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

AlphaProvenanceCert

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)

  45structure AlphaProvenanceCert where
  46  /-- CODATA is in the RS band -/
  47  codata_in_band : alphaInverseLower < codataAlphaInverse ∧ codataAlphaInverse < alphaInverseUpper
  48  /-- phi is the golden ratio (forced by uniqueness) -/
  49  phi_is_golden : phi = (1 + Real.sqrt 5) / 2
  50  /-- phi > 1 -/
  51  phi_gt_one : 1 < phi
  52  /-- RS threshold is positive -/
  53  threshold_pos : 0 < phi - 3 / 2
  54

used by (2)

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

depends on (9)

Lean names referenced from this declaration's body.