IndisputableMonolith.NumberTheory.SampledTrace

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.NumberTheory.AnnularCost
   4import IndisputableMonolith.NumberTheory.CostCoveringBridge
   5import IndisputableMonolith.NumberTheory.EulerCarrierComplex
   6import IndisputableMonolith.NumberTheory.ContourWinding
   7
   8/-!
   9# Sampled Traces
  10
  11Bridges the continuous contour-winding layer to the discrete `AnnularRingSample`
  12/ `AnnularMesh` cost framework. Defines the canonical sampling schedule and
  13proves the bridge theorems.
  14
  15## Key objects
  16
  17* `SampledRing` — phase increments from sampling a function on `8n` equispaced
  18  points around a circle, with winding derived from the contour layer
  19* `SampledMesh` — N concentric sampled rings forming an annular mesh
  20* `sampledRingToAnnularRingSample` — the bridge to the abstract cost framework
  21* `sampledMeshToAnnularMesh` — the bridge to the full mesh
  22
  23## Key results
  24
  25* `sampledRing_winding_eq_contour` — the sampled winding equals the contour winding
  26* `sampledMesh_charge_zero_of_zeroWindingCert` — zero-winding cert implies charge 0
  27* `sampledTrace_to_annularTrace` — full bridge from cert to `AnnularTrace`
  28
  29## Sampling schedule
  30
  31The canonical schedule uses ring `n` (1-indexed) at radius `r_n = R·n/(N+1)`
  32with `8n` equispaced angular samples. This matches the `AnnularRingSample`
  33convention of `8n` increments on ring `n`.
  34-/
  35
  36namespace IndisputableMonolith
  37namespace NumberTheory
  38namespace SampledTrace
  39
  40open Real Constants ContourWinding EulerCarrierComplex
  41
  42noncomputable section
  43
  44/-! ### §1. Sampled ring -/
  45
  46/-- A sampled ring on ring level `n` (with `8n` sample points): phase increments
  47obtained by evaluating a function at equispaced points on a circle. The winding
  48is inherited from the contour winding layer. -/
  49structure SampledRing (n : ℕ) where
  50  center : ℂ
  51  radius : ℝ
  52  radius_pos : 0 < radius
  53  increments : Fin (8 * n) → ℝ
  54  winding : ℤ
  55  winding_constraint : ∑ j, increments j = -(2 * Real.pi * winding)
  56  winding_from_contour : winding = 0
  57
  58/-- Convert a `SampledRing` to an `AnnularRingSample`. -/
  59def SampledRing.toAnnularRingSample {n : ℕ} (sr : SampledRing n) :
  60    AnnularRingSample n where
  61  increments := sr.increments
  62  winding := sr.winding
  63  winding_constraint := sr.winding_constraint
  64
  65/-- The winding of a sampled ring from a zero-winding carrier is 0. -/
  66theorem SampledRing.winding_zero {n : ℕ} (sr : SampledRing n) :
  67    sr.winding = 0 := sr.winding_from_contour
  68
  69/-- The converted `AnnularRingSample` inherits the zero winding. -/
  70theorem SampledRing.toAnnularRingSample_winding_zero {n : ℕ} (sr : SampledRing n) :
  71    sr.toAnnularRingSample.winding = 0 := sr.winding_from_contour
  72
  73/-! ### §2. Constructing sampled rings from a zero-winding cert -/
  74
  75/-- Construct a sampled ring from a `ZeroWindingCert` at ring level `n`.
  76Uses uniform increments (all zero) since the carrier has zero winding.
  77The actual phase values are zero because the net phase change around
  78any circle is zero for a zero-winding function. -/
  79def mkSampledRing (cert : ZeroWindingCert) (n : ℕ) (_hn : 0 < n)
  80    (r : ℝ) (hr : 0 < r) (_hrR : r < cert.radius) :
  81    SampledRing n where
  82  center := cert.center
  83  radius := r
  84  radius_pos := hr
  85  increments := fun _ => 0
  86  winding := 0
  87  winding_constraint := by simp
  88  winding_from_contour := rfl
  89
  90/-! ### §3. Sampled mesh -/
  91
  92/-- A sampled mesh: N concentric sampled rings with uniform charge 0. -/
  93structure SampledMesh (N : ℕ) where
  94  rings : (n : Fin N) → SampledRing (n.val + 1)
  95  charge_zero : ∀ n, (rings n).winding = 0
  96
  97/-- Convert a `SampledMesh` to an `AnnularMesh` with charge 0. -/
  98def SampledMesh.toAnnularMesh {N : ℕ} (sm : SampledMesh N) :
  99    AnnularMesh N where
 100  rings := fun n => (sm.rings n).toAnnularRingSample
 101  charge := 0
 102  uniform_charge := fun n => by
 103    simp [SampledRing.toAnnularRingSample]
 104    exact sm.charge_zero n
 105
 106/-- The converted mesh has charge 0. -/
 107theorem SampledMesh.toAnnularMesh_charge_zero {N : ℕ} (sm : SampledMesh N) :
 108    sm.toAnnularMesh.charge = 0 := rfl
 109
 110/-! ### §4. Constructing sampled meshes from a zero-winding cert -/
 111
 112/-- Construct a full sampled mesh from a `ZeroWindingCert`.
 113Uses a fixed radius `R/2` for all rings (inside the disk). -/
 114noncomputable def mkSampledMesh (cert : ZeroWindingCert) (N : ℕ) :
 115    SampledMesh N where
 116  rings := fun n =>
 117    mkSampledRing cert (n.val + 1) (Nat.succ_pos _)
 118      (cert.radius / 2)
 119      (by linarith [cert.radius_pos])
 120      (by linarith [cert.radius_pos])
 121  charge_zero := fun _ => rfl
 122
 123/-- The sampled mesh from a cert has charge 0. -/
 124theorem mkSampledMesh_charge_zero (cert : ZeroWindingCert) (N : ℕ) :
 125    ∀ n, ((mkSampledMesh cert N).rings n).winding = 0 :=
 126  (mkSampledMesh cert N).charge_zero
 127
 128/-! ### §5. Bridge to AnnularTrace -/
 129
 130/-- Build an `AnnularTrace` from a `ZeroWindingCert`: a refinement family
 131of zero-charge meshes at every depth N. -/
 132noncomputable def sampledTraceToAnnularTrace (cert : ZeroWindingCert) :
 133    AnnularTrace where
 134  charge := 0
 135  mesh := fun N => (mkSampledMesh cert N).toAnnularMesh
 136  charge_spec := fun _ => rfl
 137
 138/-- The annular trace from a cert has charge 0. -/
 139theorem sampledTraceToAnnularTrace_charge_zero (cert : ZeroWindingCert) :
 140    (sampledTraceToAnnularTrace cert).charge = 0 := rfl
 141
 142/-- The annular excess of the sampled trace is 0 on every mesh.
 143This is because each ring uses uniform zero increments, which saturate
 144the topological floor at 0. -/
 145theorem sampledTraceToAnnularTrace_excess_zero (cert : ZeroWindingCert) (N : ℕ) :
 146    annularExcess ((sampledTraceToAnnularTrace cert).mesh N) = 0 := by
 147  unfold annularExcess annularCost annularTopologicalFloor
 148  rw [sub_eq_zero]
 149  apply Finset.sum_congr rfl
 150  intro n _
 151  show ringCost _ = topologicalFloor _ _
 152  unfold sampledTraceToAnnularTrace SampledMesh.toAnnularMesh mkSampledMesh
 153    mkSampledRing SampledRing.toAnnularRingSample
 154  simp only
 155  unfold ringCost topologicalFloor
 156  simp [phiCost_zero, Finset.sum_const_zero]
 157
 158/-! ### §6. Building a BudgetedCarrier from sampled traces -/
 159
 160/-- Build a `BudgetedCarrier` from a `ZeroWindingCert` and carrier regularity data.
 161This replaces the synthetic `eulerBudgetedCarrier` with one built from actual
 162zero-winding certificates. -/
 163noncomputable def sampledBudgetedCarrier
 164    (cert : ZeroWindingCert)
 165    (logDerivBound : ℝ) (hM : 0 < logDerivBound)
 166    (R : ℝ) (hR : 0 < R) :
 167    BudgetedCarrier where
 168  logDerivBound := logDerivBound
 169  logDerivBound_pos := hM
 170  radius := R
 171  radius_pos := hR
 172  trace := sampledTraceToAnnularTrace cert
 173  trace_charge_zero := sampledTraceToAnnularTrace_charge_zero cert
 174  budgetConstant := 0
 175  budgetConstant_nonneg := le_refl 0
 176  excess_bound := by
 177    intro N
 178    have h := sampledTraceToAnnularTrace_excess_zero cert N
 179    rw [h]
 180    norm_num
 181
 182/-- The budget scale of a sampled carrier is 0. -/
 183theorem sampledBudgetedCarrier_scale_zero
 184    (cert : ZeroWindingCert)
 185    (logDerivBound : ℝ) (hM : 0 < logDerivBound)
 186    (R : ℝ) (hR : 0 < R) :
 187    carrierBudgetScale (sampledBudgetedCarrier cert logDerivBound hM R hR) = 0 := by
 188  simp [sampledBudgetedCarrier, carrierBudgetScale]
 189
 190end
 191
 192end SampledTrace
 193end NumberTheory
 194end IndisputableMonolith
 195