`f_gap`

definition

show as: view math explainer →

module: IndisputableMonolith.Constants.GapWeight
domain: Constants
line: 114 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.GapWeight on GitHub at line 114.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

Derivations using this theorem

f gap · derived / MODEL
The Fine-Structure Constant · foundational / THEOREM
α⁻¹ = 4π·11·exp(−w₈·ln(φ)/(4π·11)) is forced from J-cost uniqueness, φ self-similarity, and D=3; the certified band (137.030, 137.039) contains CODATA 137.036

depends on

used by

formal source

 111  unfold w8_from_eight_tick
 112  simpa using (div_pos hnum' h7)
 113
 114noncomputable def f_gap : ℝ := w8_from_eight_tick * Real.log phi
 115
 116def fGapLowerBound : ℚ := 2993443258792019287026689 / 2500000000000000000000000
 117def fGapUpperBound : ℚ := 5986887286510633232418913 / 5000000000000000000000000
 118
 119/-- Hypothesis for the certified numerical bounds for the gap weight. -/
 120def f_gap_bounds_hypothesis : Prop :=
 121  ((fGapLowerBound : ℚ) : ℝ) < f_gap ∧ f_gap < ((fGapUpperBound : ℚ) : ℝ)
 122
 123end Constants
 124end IndisputableMonolith

papers checked against this theorem

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