Encyclopedia Constants Constants Gap Weight F Gap Upper Bound

ARTICLE 4 claims 1 theorem 3 models

Constants Gap Weight F Gap Upper Bound

A number that brackets a framework constant is itself a definition, not a measurement, and it comes with a precise numerical value.

Verify this page

The gap weight's upper bound

The declaration fGapUpperBound is a rational number: 5986887286510633232418913 / 5000000000000000000000000, which is approximately 1.1973774573021266. In the Recognition Science framework, this number serves as the upper endpoint of a certified interval for a derived quantity called the gap weight. The gap weight, denoted w8, is a parameter-free constant that the framework derives from an eight-tick recognition cycle; it appears in the expression for a gap term f_gap = w8 · ln(φ), where φ is the golden ratio. The declaration itself does not prove that f_gap lies below this bound; it only defines the bound as a specific rational number.

The framework also defines a lower bound, fGapLowerBound, and a hypothesis, f_gap_bounds_hypothesis, which states that f_gap is strictly between the two bounds. This hypothesis is a formal statement in the machine-checked library, but it is not a theorem. The library does prove that w8 is positive, and it provides a closed-form expression for w8 involving φ and √2. The upper bound is a component of a larger effort to certify the numerical value of w8 without relying on free parameters, but the bound itself is a definition, not a derived result.

What the declaration does not claim is that the gap weight has been measured experimentally or that its value is confirmed by observation. It also does not claim that the hypothesis f_gap_bounds_hypothesis has been proved; that remains an open target within the framework. The upper bound is a precise, machine-readable number that the framework uses to state a conjecture about the range of f_gap, and it is a necessary piece of the framework's attempt to show that its constants are not fitted.

MODEL fGapUpperBound · IndisputableMonolith/Constants/GapWeight.lean
fGapUpperBound · IndisputableMonolith/Constants/GapWeight.lean:181 
def fGapUpperBound : ℚ := 5986887286510633232418913 / 5000000000000000000000000
MODEL w8_from_eight_tick · IndisputableMonolith/Constants/GapWeight.lean
w8_from_eight_tick · IndisputableMonolith/Constants/GapWeight.lean:96 
/-- The canonical gap weight `w₈` (parameter‑free, closed form).

This is the normalized projection weight of the gap onto the fundamental
8-tick basis. Numerically it is approximately `2.49056927545…`. -/
@[simp] noncomputable def w8_from_eight_tick : ℝ :=
  (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * phi) / 7
THEOREM w8_pos · IndisputableMonolith/Constants/GapWeight.lean
w8_pos · IndisputableMonolith/Constants/GapWeight.lean:103 
/-- Derived w₈ is positive. -/
theorem w8_pos : 0 < w8_from_eight_tick := by
  -- A coarse but self-contained positivity proof using rational upper bounds.
  -- We show the numerator is positive under worst-case substitution (largest φ and √2).
  have hs2_hi : Real.sqrt 2 < (71 / 50 : ℝ) := by
    have hx : (0 : ℝ) ≤ 2 := by norm_num
    have hy : (0 : ℝ) ≤ (71 / 50 : ℝ) := by norm_num
    have hsq : (2 : ℝ) < (71 / 50 : ℝ) ^ 2 := by norm_num
    exact (Real.sqrt_lt hx hy).2 hsq
  have hs5_hi : Real.sqrt 5 < (56 / 25 : ℝ) := by
    have hx : (0 : ℝ) ≤ 5 := by norm_num
    have hy : (0 : ℝ) ≤ (56 / 25 : ℝ) := by norm_num
    have hsq : (5 : ℝ) < (56 / 25 : ℝ) ^ 2 := by norm_num
    exact (Real.sqrt_lt hx hy).2 hsq
  have hphi_hi : phi < (81 / 50 : ℝ) := by
    -- φ = (1 + √5)/2 < (1 + 56/25)/2 = 81/50
    have : (phi : ℝ) = (1 + Real.sqrt 5) / 2 := by rfl
    rw [this]
    have h2pos : (0 : ℝ) < (2 : ℝ) := by norm_num
    have hnum : (1 + Real.sqrt 5) < (1 + (56 / 25 : ℝ)) := by linarith [hs5_hi]
    have hdiv : (1 + Real.sqrt 5) / 2 < (1 + (56 / 25 : ℝ)) / 2 :=
      div_lt_div_of_pos_right hnum h2pos
    have hR : (1 + (56 / 25 : ℝ)) / 2 = (81 / 50 : ℝ) := by norm_num
    simpa [hR] using hdiv
  have hphi_lo : (21 / 13 : ℝ) < phi := by
    -- √5 > 2.231, so φ = (1+√5)/2 > (1+2.231)/2 = 1.6155 > 21/13.
    have hs5_lo : (2231 / 1000 : ℝ) < Real.sqrt 5 := by
      have hx : (0 : ℝ) ≤ (2231 / 1000 : ℝ) := by norm_num
      have hsq : (2231 / 1000 : ℝ) ^ 2 < (5 : ℝ) := by norm_num
      exact (Real.lt_sqrt hx).2 hsq
    have : (phi : ℝ) = (1 + Real.sqrt 5) / 2 := by rfl
    rw [this]
    have h2pos : (0 : ℝ) < (2 : ℝ) := by norm_num
    have hnum : (1 + (2231 / 1000 : ℝ)) < (1 + Real.sqrt 5) := by linarith [hs5_lo]
    have hdiv : (1 + (2231 / 1000 : ℝ)) / 2 < (1 + Real.sqrt 5) / 2 :=
      div_lt_div_of_pos_right hnum h2pos
    have hconst : (21 / 13 : ℝ) < (1 + (2231 / 1000 : ℝ)) / 2 := by norm_num
    exact lt_trans hconst (by simpa using hdiv)
  have hcoeff_nonpos : (210 : ℝ) - 130 * phi ≤ 0 := by
    -- from 21/13 < φ, we get 210 ≤ 130φ
    have hφ : (21 / 13 : ℝ) ≤ phi := le_of_lt hphi_lo
    have : (210 : ℝ) ≤ 130 * phi := by
      have : (130 : ℝ) * (21 / 13 : ℝ) ≤ 130 * phi := by nlinarith [hφ]
      simpa using (le_trans (by norm_num : (210 : ℝ) ≤ (130 : ℝ) * (21 / 13 : ℝ)) this)
    linarith
  -- Numerator positivity by worst-case substitution (largest φ and √2).
  have hφ : phi ≤ (81 / 50 : ℝ) := le_of_lt hphi_hi
  have hs2 : Real.sqrt 2 ≤ (71 / 50 : ℝ) := le_of_lt hs2_hi
  have hconst :
      (0 : ℝ) <
        (348 : ℝ) - 204 * (81 / 50 : ℝ) + (71 / 50 : ℝ) * ((210 : ℝ) - 130 * (81 / 50 : ℝ)) := by
    norm_num
  have hbase :
      (348 : ℝ) - 204 * phi + (71 / 50 : ℝ) * ((210 : ℝ) - 130 * phi)
        ≥ (348 : ℝ) - 204 * (81 / 50 : ℝ) + (71 / 50 : ℝ) * ((210 : ℝ) - 130 * (81 / 50 : ℝ)) := by
    nlinarith [hφ]
  have hnum_pos :
      0 < (348 : ℝ) - 204 * phi + (71 / 50 : ℝ) * ((210 : ℝ) - 130 * phi) :=
    lt_of_lt_of_le hconst hbase
  have hterm :
      (Real.sqrt 2) * ((210 : ℝ) - 130 * phi) ≥ (71 / 50 : ℝ) * ((210 : ℝ) - 130 * phi) := by
    exact mul_le_mul_of_nonpos_right hs2 hcoeff_nonpos
  have hnum :
      0 < (348 : ℝ) - 204 * phi + (Real.sqrt 2) * ((210 : ℝ) - 130 * phi) := by
    linarith
  have hrewrite :
      (348 : ℝ) - 204 * phi + (Real.sqrt 2) * ((210 : ℝ) - 130 * phi)
        = (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * phi) := by
    ring
  have hnum' : 0 < (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * phi) := by
    simpa [hrewrite] using hnum
  have h7 : (0 : ℝ) < (7 : ℝ) := by norm_num
  unfold w8_from_eight_tick
  simpa using (div_pos hnum' h7)
MODEL f_gap_bounds_hypothesis · IndisputableMonolith/Constants/GapWeight.lean
f_gap_bounds_hypothesis · IndisputableMonolith/Constants/GapWeight.lean:183 
/-- Hypothesis for the certified numerical bounds for the gap weight. -/
def f_gap_bounds_hypothesis : Prop :=
  ((fGapLowerBound : ℚ) : ℝ) < f_gap ∧ f_gap < ((fGapUpperBound : ℚ) : ℝ)

What this page does not claim

The upper bound is not a measurement of any physical quantity. The hypothesis that f_gap lies within the bounds is not a proved theorem. The declaration does not imply that the fine-structure constant has been derived from first principles.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Constants/GapWeight.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND