IndisputableMonolith.Spectra.SpectralLadder

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Spectral Ladder (scaffold)
   6
   7Cross-domain spectral rails: f_n = f0 · φ^{2n}, where f0 = E_coh / h.
   8This module exposes basic helpers for rails and an eight-gate coherence test.
   9-/
  10
  11namespace IndisputableMonolith
  12namespace Spectra
  13namespace SpectralLadder
  14
  15open scoped BigOperators Real
  16
  17noncomputable section
  18
  19/-- Base frequency f0 (e.g., E_coh/h) is supplied by the caller.
  20    A default fit-free choice from RS gates is \(1/(2\pi\cdot\tau_0)\). -/
  21def f0_default : ℝ := 1 / (2 * Real.pi * IndisputableMonolith.Constants.tau0)
  22
  23def railFactor (n : ℤ) : ℝ :=
  24  Real.rpow IndisputableMonolith.Constants.phi ((2 : ℝ) * (n : ℝ))
  25
  26def frequencyOnRail (f0 : ℝ) (n : ℤ) : ℝ :=
  27  f0 * railFactor n
  28
  29/-- Sliding sum over 8 samples (coherence/neutrality diagnostic). -/
  30def sum8 (x : ℕ → ℝ) (t0 : ℕ) : ℝ :=
  31  (Finset.range 8).sum (fun k => x (t0 + k))
  32
  33def eightGateCoherent (x : ℕ → ℝ) (t0 : ℕ) : Prop :=
  34  sum8 x t0 = 0
  35
  36end
  37
  38end SpectralLadder
  39end Spectra
  40end IndisputableMonolith
  41