pith. machine review for the scientific record. sign in
def

alphaProvenanceCert

definition
show as:
view math explainer →
module
IndisputableMonolith.Foundation.AlphaDerivationExplicit
domain
Foundation
line
55 · github
papers citing
35 papers (below)

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.AlphaDerivationExplicit on GitHub at line 55.

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

Derivations using this theorem

depends on

used by

formal source

  52  /-- RS threshold is positive -/
  53  threshold_pos : 0 < phi - 3 / 2
  54
  55noncomputable def alphaProvenanceCert : AlphaProvenanceCert where
  56  codata_in_band := codata_in_band
  57  phi_is_golden := phi_golden_ratio
  58  phi_gt_one := by linarith [phi_gt_onePointFive]
  59  threshold_pos := by linarith [phi_gt_onePointFive]
  60
  61theorem alphaProvenance_inhabited : Nonempty AlphaProvenanceCert := ⟨alphaProvenanceCert⟩
  62
  63end AlphaDerivationExplicit
  64end Foundation
  65end IndisputableMonolith