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

alphaInverseRS

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.AlphaDerivationExplicit on GitHub at line 41.

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

  38
  39/-- The RS alpha formula: 44*pi*exp(-8*ln(phi)/(44*pi)).
  40    The 44 comes from the recognition frequency slots forced by D=3 and phi. -/
  41noncomputable def alphaInverseRS : ℝ :=
  42  44 * Real.pi * Real.exp (-8 * Real.log phi / (44 * Real.pi))
  43
  44/-- Structural certificate for the alpha provenance chain. -/
  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
  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

papers checked against this theorem (showing 1 of 1)