`codataAlphaInverse`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.AlphaDerivationExplicit
domain: Foundation
line: 34 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.AlphaDerivationExplicit on GitHub at line 34.

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

used by

formal source

  31def alphaInverseUpper : ℝ := 137.039
  32
  33/-- The CODATA 2022 value lies inside the RS band. -/
  34def codataAlphaInverse : ℝ := 137.035999084
  35
  36theorem codata_in_band : alphaInverseLower < codataAlphaInverse ∧ codataAlphaInverse < alphaInverseUpper := by
  37  constructor <;> norm_num [alphaInverseLower, alphaInverseUpper, codataAlphaInverse]
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.