Constants Alpha Genesis Spectral Forcing Norm Sq Omega8 Pow Sub One

The trig closure

The declaration normSq_omega8_pow_sub_one proves a specific trigonometric identity: for any integer k, the squared modulus of the complex number ω₈ᵏ − 1 equals 4·sin²(kπ/8), where ω₈ is the primitive eighth root of unity e^(2πi/8). In plain words, it establishes that the distance (in the complex plane) from the point ω₈ᵏ to the number 1, squared, is exactly four times the square of the sine of kπ/8. This is a standard identity from complex analysis, but here it is formalized as a theorem in a machine-checked library of formal theorems, meaning every step of the proof has been verified by a computer.

The identity is not an isolated curiosity. Within the Recognition Science framework, it serves as the trigonometric closure in a chain of results about the eight-tick cycle, a discrete record of events. The framework models the difference energy of a mode k as the squared modulus of its shift eigenvalue minus one, written |ω₈ᵏ − 1|². The theorem shows this energy equals 4·sin²(kπ/8). This connects the oscillation factor that appears in gap-weight mode weights to the spectrum of the one-step difference operator on the cycle, evaluated on the DFT-8 eigenbasis. The factorization that follows, geometricWeight k = (diffEnergy8(mode k)/4) · latticeWeight k, states that the mode weight is the product of the difference-operator spectrum and the T9 forced measure, with both factors now theorem-backed rather than assumed.

What the declaration does not claim is broader than what it proves. It does not assert that the eight-tick cycle or the gap-weight structure is physically real; those are modeling choices within the framework. It does not claim that the fine-structure constant α is derived or predicted; the pack explicitly states that no CODATA reference appears in this file, and the derivation of α remains an open target. The identity itself is a mathematical fact, true for any integer k, but its interpretation as the derivative spectrum of a recognition cycle is a framework-specific application, not a consequence of the theorem alone.

The practical payoff is that the oscillation factor in the gap weight is no longer an input or a free parameter. It is forced by the difference operator on the eight-tick cycle, just as the pattern, envelope, and dressing form are forced by other theorems in the chain. The only remaining ingredient inherited without re-derivation is the Parseval or 64-cell normalization, named in the premise section of the source. This closes the last interior joint of the gap weight, leaving a structure where every factor is either a theorem or an explicitly stated premise.

/-- **The trig closure.** The squared modulus of the shift eigenvalue minus
one is four times the squared half-angle sine:
`|ω₈ᵏ − 1|² = 4 sin²(kπ/8)`. -/
theorem normSq_omega8_pow_sub_one (k : ℕ) :
    Complex.normSq (omega8 ^ k - 1) =
      4 * (Real.sin ((k : ℝ) * Real.pi / 8)) ^ 2 := by
  -- ω₈ᵏ = exp(i·θ) with θ = −kπ/4
  have hpow : omega8 ^ k = Complex.exp ((-((k : ℝ) * Real.pi / 4) : ℝ) * Complex.I) := by
    unfold omega8
    rw [← Complex.exp_nat_mul]
    congr 1
    push_cast
    ring
  rw [hpow, Complex.exp_mul_I]
  -- normSq(cos θ + sin θ·i − 1) = (cos θ − 1)² + sin² θ
  have hcos : Complex.cos ((-((k : ℝ) * Real.pi / 4) : ℝ) : ℂ) =
      ((Real.cos (-((k : ℝ) * Real.pi / 4)) : ℝ) : ℂ) := by
    rw [Complex.ofReal_cos]
  have hsin : Complex.sin ((-((k : ℝ) * Real.pi / 4) : ℝ) : ℂ) =
      ((Real.sin (-((k : ℝ) * Real.pi / 4)) : ℝ) : ℂ) := by
    rw [Complex.ofReal_sin]
  rw [hcos, hsin]
  set θ : ℝ := -((k : ℝ) * Real.pi / 4) with hθ
  have hrw : (Real.cos θ : ℂ) + (Real.sin θ : ℂ) * Complex.I - 1
      = ((Real.cos θ - 1 : ℝ) : ℂ) + ((Real.sin θ : ℝ) : ℂ) * Complex.I := by
    push_cast
    ring
  rw [hrw, Complex.normSq_add_mul_I]
  -- (cos θ − 1)² + sin² θ = 2 − 2 cos θ
  have hpyth : Real.sin θ ^ 2 + Real.cos θ ^ 2 = 1 := Real.sin_sq_add_cos_sq θ
  have h2 : (Real.cos θ - 1) ^ 2 + (Real.sin θ) ^ 2 = 2 - 2 * Real.cos θ := by
    nlinarith [hpyth]
  rw [h2]
  -- cos θ = cos(kπ/4) (cos is even)
  have hcos_even : Real.cos θ = Real.cos ((k : ℝ) * Real.pi / 4) := by
    rw [hθ, Real.cos_neg]
  rw [hcos_even]
  -- half-angle via double-angle: cos(2x) = 2cos²x − 1 and sin²x = 1 − cos²x
  have hcos2 : Real.cos (2 * ((k : ℝ) * Real.pi / 8)) =
      2 * Real.cos ((k : ℝ) * Real.pi / 8) ^ 2 - 1 :=
    Real.cos_two_mul ((k : ℝ) * Real.pi / 8)
  have harg : 2 * ((k : ℝ) * Real.pi / 8) = (k : ℝ) * Real.pi / 4 := by ring
  rw [harg] at hcos2
  have hsq : Real.sin ((k : ℝ) * Real.pi / 8) ^ 2 =
      1 - Real.cos ((k : ℝ) * Real.pi / 8) ^ 2 :=
    Real.sin_sq ((k : ℝ) * Real.pi / 8)
  nlinarith [hcos2, hsq]

/-- **The spectrum identity.** The difference energy of DFT mode k equals
`4 sin²(kπ/8)`: the oscillation factor of the gap weight is exactly one
quarter of the difference-operator spectrum. -/
theorem diffEnergy8_mode_eq_four_sin_sq (k : Fin 8) :
    diffEnergy8 (dft8_mode k) =
      4 * (Real.sin ((k.val : ℝ) * Real.pi / 8)) ^ 2 := by
  rw [diffEnergy8_mode k]
  exact normSq_omega8_pow_sub_one k.val

/-- **SPECTRAL FORCING.** For every nonzero mode, the gap-weight mode
weight factors as (difference-operator spectrum / 4) times the T9 forced
measure:
`geometricWeight k = (diffEnergy8(mode k)/4) · latticeWeight k`.
Both factors are theorems; neither is an input. -/
theorem geometricWeight_eq_spectrum_mul_measure (k : Fin 8) (hk : ¬ k.val = 0) :
    GapWeight.geometricWeight k =
      (diffEnergy8 (dft8_mode k) / 4) *
        Foundation.MeasureForcing.latticeWeight k.val := by
  rw [geometricWeight_eq_sin_mul_forced_measure k hk,
    diffEnergy8_mode_eq_four_sin_sq k]
  ring

What this page does not claim

The declaration does not derive the fine-structure constant α. The declaration does not assert that the eight-tick cycle is physically real. The declaration does not claim that the oscillation factor is a modeling choice; it is a theorem.

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/AlphaGenesis/SpectralForcing.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: