Encyclopedia Constants Constants Gap Weight W8 Pos

ARTICLE 3 claims 2 theorems 1 model

Constants Gap Weight W8 Pos

A single number, about 2.49, that the Recognition Science framework derives from an eight-step cycle, and the theorem that guarantees it is positive.

Verify this page

The gap weight

The gap weight, written w₈, is a number that appears in the Recognition Science framework's account of how a discrete record of events, its ledger, projects onto a repeating eight-step pattern. The framework models this projection with a weight that multiplies the logarithm of the golden ratio, φ ≈ 1.618. The number is not chosen to fit any measurement; it is defined by a closed algebraic expression, (348 + 210√2 − (204 + 130√2)φ) / 7, which evaluates to approximately 2.49056927545.

The declaration w8_pos is a theorem in the framework's machine-checked library of formal theorems. It proves that this gap weight is greater than zero. That may sound like a small fact, but it is the kind of guarantee a formal system can verify exactly: the expression is not just approximately positive, it is provably positive for all real numbers satisfying the defining relations of φ and √2. The proof rests on the closed form itself, not on numerical approximation.

The framework's library shows that the integers in the closed form, 348, 210, 204, 130, and 7, are not free parameters. They emerge from a chain of forced choices: the eight-step pattern is fixed by the framework's earlier theorems, the discrete Fourier transform on eight points is standard, the spectral weights come from a discrete derivative, and Parseval's theorem normalizes the total energy. The 64 in the scaling is the product of eight ticks and eight vertices, the size of the fundamental interface cell. The equality between the projected weight and this closed form is itself a proved theorem, with no unproved assumptions in the framework's own axioms.

What w8_pos does not claim is just as important. It does not claim that this gap weight is the fine-structure constant α, nor that it predicts any measured physical constant. The framework's expression for α, which involves this weight, lands close to the measured value, but that comparison is an empirical check, not a theorem, and the exact value of α remains an open target. The theorem w8_pos only establishes positivity of the weight; it says nothing about what the weight is used for or whether that use is physically correct.

The practical consequence is that the framework can build on w₈ without worrying about sign errors. A negative weight would change the character of the projection, so the positivity theorem is a necessary foundation for any later use of the gap term. It is a small, clean result that the framework's own standards require before the weight can participate in further derivations.

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 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_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

What this page does not claim

The theorem w8_pos does not claim that the gap weight predicts or equals any measured physical constant. The theorem does not claim that the framework's expression for α is exact or derived. The theorem does not claim that the gap weight is physically meaningful outside the framework's own model.

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