IndisputableMonolith.Spiral.SpiralField

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Spiral Wavefields (scaffold)
   6
   7Variational ansatz for logarithmic spiral fields under φ-scaling and an
   8eight-tick gating constraint. This file defines only basic structures and
   9helpers; no proofs are required to compile.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Spiral
  14namespace SpiralField
  15
  16open scoped BigOperators Real
  17
  18noncomputable section
  19
  20/- Basic parameter bundle: fixed φ from constants and an integral pitch κ. -/
  21structure Params where
  22  kappa : ℤ
  23  deriving Repr, DecidableEq
  24
  25/- Log-spiral radius with base scale r0>0 and angle θ (radians):
  26   r(θ) = r0 · φ^{(κ · θ)/(2π)}. -/
  27def logSpiral (r0 : ℝ) (θ : ℝ) (P : Params) : ℝ :=
  28  let exp : ℝ := (P.kappa : ℝ) * θ / (2 * Real.pi)
  29  r0 * Real.rpow IndisputableMonolith.Constants.phi exp
  30
  31/- Unique convex cost J on ℝ₊ (display-only definition, no proofs here). -/
  32def Jcost (x : ℝ) : ℝ := (1 / 2 : ℝ) * (x + 1 / x) - 1
  33
  34/- Discrete step ratio for the spiral at angular increment Δθ. -/
  35def stepRatio (r0 θ Δθ : ℝ) (P : Params) : ℝ :=
  36  let r₁ := logSpiral r0 (θ + Δθ) P
  37  let r₀ := logSpiral r0 θ P
  38  if r₀ = 0 then 1 else r₁ / r₀
  39
  40/- Sampled cost over N steps starting at θ with increment Δθ. -/
  41def sampledCost (r0 θ Δθ : ℝ) (N : ℕ) (P : Params) : ℝ :=
  42  (Finset.range N).sum (fun n =>
  43    let θn := θ + (n : ℝ) * Δθ
  44    Jcost (stepRatio r0 θn Δθ P))
  45
  46/- Eight-gate neutrality predicate on a discrete signal w, aligned at t0. -/
  47def eightGateNeutral (w : ℕ → ℝ) (t0 : ℕ) : Prop :=
  48  (Finset.range 8).sum (fun k => w (t0 + k)) = 0
  49
  50/- Neutrality score (sum over 8 ticks), useful for diagnostics/falsifiers. -/
  51def neutralityScore (w : ℕ → ℝ) (t0 : ℕ) : ℝ :=
  52  (Finset.range 8).sum (fun k => w (t0 + k))
  53
  54/- Pitch slope proxy: multiplicative growth per full turn (Δθ = 2π).
  55   For r(θ)=r0·φ^{κ θ/(2π)}, the per-turn ratio equals φ^{κ}. -/
  56def perTurnMultiplier (P : Params) : ℝ :=
  57  Real.rpow IndisputableMonolith.Constants.phi (P.kappa : ℝ)
  58
  59/- Discrete EL-style stationarity proxy: every local step cost is ≤ the
  60   baseline J(1)=0 (achieved at unity ratio). This is a diagnostic predicate
  61   used in notes; it does not claim a proof here. -/
  62def ELStationary (r0 θ Δθ : ℝ) (N : ℕ) (P : Params) : Prop :=
  63  ∀ n : ℕ, n < N → Jcost (stepRatio r0 (θ + (n : ℝ) * Δθ) Δθ P) ≤ Jcost 1
  64
  65end
  66
  67end SpiralField
  68end Spiral
  69end IndisputableMonolith
  70