`f_gap_def`

proved

show as: view math explainer →

module: IndisputableMonolith.Pipelines
domain: Pipelines
line: 31 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Pipelines on GitHub at line 31.

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

  28
  29/-- The master gap value as the generator at z=1. -/
  30noncomputable def f_gap : ℝ := F 1
  31@[simp] lemma f_gap_def : f_gap = Real.log (1 + 1 / phi) := rfl
  32
  33end GapSeries
  34
  35namespace Curvature
  36
  37/-- Curvature-closure constant δ_κ used in the α pipeline.
  38Defined here as the exact rational/π expression from the voxel seam count. -/
  39noncomputable def deltaKappa : ℝ := - (103 : ℝ) / (102 * Real.pi ^ 5)
  40
  41/-- The predicted dimensionless inverse fine-structure constant
  42α^{-1} = 4π·11 − (ln φ + δ_κ).
  43This is a pure expression-level definition (no numerics here). -/
  44noncomputable def alphaInvPrediction : ℝ := 4 * Real.pi * 11 - (Real.log phi + deltaKappa)
  45
  46end Curvature
  47
  48end Pipelines
  49end IndisputableMonolith

papers checked against this theorem

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