ContinuousPhaseData
A record packages the center and positive radius of a circle in the complex plane, a continuous real phase function, an integer winding charge, and the condition that the phase changes by minus two pi times the charge over one full turn. Researchers in holomorphic factorization and discrete sampling within Recognition Science cite this when building regular factor phases from nonvanishing analytic functions or proving charge additivity under products. The declaration is a plain record definition with no attached proof.
claimA structure consisting of a center $c$ in the complex plane, a radius $R > 0$, a continuous function $Θ : ℝ → ℝ$, an integer $m$, and the equality $Θ(2π) - Θ(0) = -2π m$.
background
The Circle Phase Lift module supplies continuous-phase infrastructure that links Mathlib complex analysis to the discrete AnnularRingSample and AnnularMesh cost framework. A continuous phase assignment packages a continuous real-valued function Θ representing the argument along the circle parametrized by circleMap c R, with the integer charge m satisfying Θ(2π) − Θ(0) = −2π m as the winding number. This setup enables sampling the phase at 8n equispaced angles to produce increments that telescope to the total winding, feeding into annular cost calculations. Upstream results include the eight-tick phase definition, which supplies discrete phases at kπ/4 for k = 0 to 7, providing the periodic structure that the continuous lift extends.
proof idea
The structure is introduced as a record type whose fields directly encode the geometric and analytic data: center and radius locate the circle, the phase function supplies the continuous lift with a continuity hypothesis, the charge is the integer winding number, and the phase winding field enforces the total change condition. No tactics or lemmas are invoked in the definition itself; it functions as a carrier type for subsequent theorems that construct instances from holomorphic data.
why it matters in Recognition Science
This declaration provides the core data structure for phase lifting in the NumberTheory component of Recognition Science. It is extended by RegularFactorPhase, which adds a log-derivative Lipschitz bound and forces charge zero, and is used in holomorphic_nonvanishing_zero_charge to obtain zero-charge data from nonvanishing holomorphic functions on a disk, as well as in charge_additive to show charges add under multiplication. The construction supports the bridge from continuous analysis to the eight-tick discrete sampling (T7), enabling connections to the phi-ladder mass formulas and annular cost models. It touches the open question of how such phases relate to the J-cost functional in the broader forcing chain.
scope and limits
- Does not establish existence of a phase function for an arbitrary continuous function on the circle.
- Does not provide a Lipschitz bound on the phase map.
- Does not derive the charge from an underlying holomorphic function.
- Does not connect the phase to the J-uniqueness or phi fixed point.
- Does not address sampling beyond the 8n equispaced points.
formal statement (Lean)
46structure ContinuousPhaseData where
47 center : ℂ
48 radius : ℝ
49 radius_pos : 0 < radius
50 phase : ℝ → ℝ
51 phase_continuous : Continuous phase
52 charge : ℤ
53 phase_winding : phase (2 * π) - phase 0 = -(2 * π * (charge : ℝ))
54
55/-! ### §2. Sampling into AnnularRingSample -/
56
57/-- Sample phase increments at `8n` equispaced angles.
58Increment k is Θ(2π(k+1)/(8n)) − Θ(2πk/(8n)). -/
59def ContinuousPhaseData.sampleIncrements
60 (cpd : ContinuousPhaseData) (n : ℕ) : Fin (8 * n) → ℝ :=
proof body
Definition body.
61 fun k =>
62 cpd.phase (2 * π * ((k.val : ℝ) + 1) / (8 * (n : ℝ))) -
63 cpd.phase (2 * π * (k.val : ℝ) / (8 * (n : ℝ)))
64
65/-- The sampled increments telescope to the total phase change.
66
67**Proof route**: standard Finset telescoping sum. The last sample point
682π · (8n)/(8n) = 2π coincides with the right endpoint, and the first
69sample point 2π · 0/(8n) = 0 coincides with the left endpoint, so the
70sum collapses to Θ(2π) − Θ(0) = −2π · charge. -/
71theorem ContinuousPhaseData.sample_winding_constraint
72 (cpd : ContinuousPhaseData) (n : ℕ) (hn : 0 < n) :
73 ∑ j, cpd.sampleIncrements n j = -(2 * π * (cpd.charge : ℝ)) := by
74 let f : ℕ → ℝ := fun k => cpd.phase (2 * π * (k : ℝ) / (8 * (n : ℝ)))
75 have hsum :
76 (∑ j, cpd.sampleIncrements n j) =
77 (∑ k ∈ Finset.range (8 * n), (f (k + 1) - f k)) := by
78 rw [Finset.sum_fin_eq_sum_range]
79 refine Finset.sum_congr rfl ?_
80 intro k hk
81 simp [ContinuousPhaseData.sampleIncrements, f, Finset.mem_range.mp hk]
82 have hnR : 0 < (n : ℝ) := by
83 exact_mod_cast hn
84 have hden_ne : (8 * (n : ℝ)) ≠ 0 := by
85 nlinarith
86 have hlast : f (8 * n) = cpd.phase (2 * π) := by
87 dsimp [f]
88 have hcast : (((8 * n : ℕ) : ℝ)) = 8 * (n : ℝ) := by
89 norm_num [Nat.cast_mul]
90 rw [hcast]
91 field_simp [hden_ne]
92 have hzero : f 0 = cpd.phase 0 := by
93 dsimp [f]
94 simp
95 calc
96 ∑ j, cpd.sampleIncrements n j
97 = ∑ k ∈ Finset.range (8 * n), (f (k + 1) - f k) := hsum
98 _ = f (8 * n) - f 0 := by
99 rw [Finset.sum_range_sub]
100 _ = cpd.phase (2 * π) - cpd.phase 0 := by
101 rw [hlast, hzero]
102 _ = -(2 * π * (cpd.charge : ℝ)) := cpd.phase_winding
103
104/-- Convert continuous phase data to an `AnnularRingSample`. -/
105def ContinuousPhaseData.toAnnularRingSample
106 (cpd : ContinuousPhaseData) (n : ℕ) (hn : 0 < n) :
107 AnnularRingSample n where
108 increments := cpd.sampleIncrements n
109 winding := cpd.charge
110 winding_constraint := cpd.sample_winding_constraint n hn
111
112/-! ### §3. Genuine regular-factor phase from analytic nonvanishing functions -/
113
114/-- A regular-factor phase witness packages the continuous phase of a
115nonvanishing analytic function `g` on a circle, together with a
116log-derivative Lipschitz bound.
117
118`charge = 0` because `g` is holomorphic and nonvanishing on a disk
119containing the circle (argument principle). The Lipschitz bound `M`
120comes from `sup |g'/g|` on the circle. -/
used by (20)
-
charge_additive -
holomorphic_nonvanishing_zero_charge -
logDeriv_circle_integral_zero -
mkRegularFactorPhase -
RegularFactorPhase -
RegularFactorPhase -
zpow_charge_eq_winding_integral -
zpow_phase_charge -
canonicalDefectSampledFamily_ringPerturbationControl -
phaseFamily_ringPerturbationControl -
DefectPhaseFamily -
genuineZetaDerivedPhaseData -
genuineZetaDerivedPhasePerturbationWitness -
meromorphic_phase_charge -
phaseIncrementEpsilonBound_decreasing -
pureDefectPhaseData -
trivialDefectPhasePerturbationWitness -
zetaDerivedPhaseData -
zetaDerivedPhaseDataBundle -
zetaDerivedPhasePerturbationWitness