charge_additive
If two continuous phase assignments on the same circle have charges m1 and m2, their pointwise sum yields a phase assignment with charge m1 + m2. Workers on meromorphic order or annular sampling in Recognition Science cite this when superposing regular factors. The argument builds the summed phase explicitly and confirms the winding equality by additivity of the total phase change.
claimLet $c$ be a complex center and $r > 0$ a common radius. Let $m_1, m_2$ be integers and let $Θ_1, Θ_2 : ℝ → ℝ$ be continuous functions satisfying $Θ_i(2π) - Θ_i(0) = -2π m_i$ for $i=1,2$. Then the function $Θ(θ) := Θ_1(θ) + Θ_2(θ)$ is continuous and satisfies the winding condition for charge $m_1 + m_2$ on the same circle.
background
ContinuousPhaseData packages a center, positive radius, a continuous phase function Θ : ℝ → ℝ, an integer charge, and the winding equality phase(2π) − phase(0) = −2π·charge. This structure lifts nonvanishing functions on a circle to their argument functions for sampling into annular cost models. The module CirclePhaseLift supplies the bridge from Mathlib contour integrals to the discrete AnnularRingSample framework used in Recognition Science. Key siblings include holomorphic_nonvanishing_zero_charge, which shows analytic nonvanishing implies charge zero, and zpow_phase_charge for powers. Upstream results such as the phase definition in EightTick provide the discrete angular sampling that this continuous lift extends.
proof idea
The proof constructs a new ContinuousPhaseData record whose phase is the pointwise sum of the two input phases, inheriting continuity by addition of continuous functions. It then verifies the winding condition by a short calculation: the total change of the sum equals the sum of the total changes, which by the input winding equalities is −2π(m1 + m2). The verification uses ring and simp tactics on the integer cast.
why it matters in Recognition Science
This result is invoked by regularFactorPhaseFromWitness when constructing phases for regular factors in meromorphic order computations. It closes the additive structure needed for superposing zpow factors and holomorphic nonvanishing pieces in the factorization pipeline. Within the Recognition framework it supports the phase lift that connects the eight-tick octave sampling to continuous winding numbers on circles of radius governed by the phi-ladder.
scope and limits
- Does not guarantee that the summed phase arises from an analytic function.
- Does not bound the Lipschitz constant of the sum.
- Does not extend to non-continuous phases.
- Does not address multiple circles or varying radii.
formal statement (Lean)
248theorem charge_additive (cpd₁ cpd₂ : ContinuousPhaseData)
249 (_hc : cpd₁.center = cpd₂.center) (_hr : cpd₁.radius = cpd₂.radius) :
250 ∃ cpd : ContinuousPhaseData,
251 cpd.center = cpd₁.center ∧ cpd.radius = cpd₁.radius ∧
252 cpd.charge = cpd₁.charge + cpd₂.charge := by
proof body
Tactic-mode proof.
253 refine ⟨
254 { center := cpd₁.center
255 radius := cpd₁.radius
256 radius_pos := cpd₁.radius_pos
257 phase := fun θ => cpd₁.phase θ + cpd₂.phase θ
258 phase_continuous := cpd₁.phase_continuous.add cpd₂.phase_continuous
259 charge := cpd₁.charge + cpd₂.charge
260 phase_winding := ?_ }, rfl, rfl, rfl⟩
261 calc
262 (cpd₁.phase (2 * π) + cpd₂.phase (2 * π)) - (cpd₁.phase 0 + cpd₂.phase 0)
263 = (cpd₁.phase (2 * π) - cpd₁.phase 0) + (cpd₂.phase (2 * π) - cpd₂.phase 0) := by
264 ring
265 _ = -(2 * π * (cpd₁.charge : ℝ)) + -(2 * π * (cpd₂.charge : ℝ)) := by
266 rw [cpd₁.phase_winding, cpd₂.phase_winding]
267 _ = -(2 * π * ((cpd₁.charge + cpd₂.charge : ℤ) : ℝ)) := by
268 simp [Int.cast_add]
269 ring
270
271/-! ### §6. Lipschitz-controlled perturbation bounds -/
272
273/-- The Lipschitz-controlled phase has bounded increments. For a mesh
274of `8n` equispaced samples, each increment deviates from the uniform
275increment by at most `logDerivBound * (2π / (8n))`. -/
276theorem RegularFactorPhase.increment_bound
277 (rfp : RegularFactorPhase) (n : ℕ) (hn : 0 < n) (j : Fin (8 * n)) :
278 |rfp.sampleIncrements n j| ≤
279 rfp.logDerivBound * (2 * π / (8 * (n : ℝ))) := by
280 simp only [ContinuousPhaseData.sampleIncrements]
281 have hnR : (0 : ℝ) < 8 * (n : ℝ) := by positivity
282 have hstep : |(2 * π * ((j.val : ℝ) + 1) / (8 * (n : ℝ))) -
283 (2 * π * (j.val : ℝ) / (8 * (n : ℝ)))| = 2 * π / (8 * (n : ℝ)) := by
284 rw [show 2 * π * ((j.val : ℝ) + 1) / (8 * (n : ℝ)) -
285 2 * π * (j.val : ℝ) / (8 * (n : ℝ)) =
286 2 * π / (8 * (n : ℝ)) from by ring]
287 rw [abs_of_pos (by positivity)]
288 calc |rfp.phase (2 * π * ((j.val : ℝ) + 1) / (8 * (n : ℝ))) -
289 rfp.phase (2 * π * (j.val : ℝ) / (8 * (n : ℝ)))|
290 ≤ rfp.logDerivBound * |(2 * π * ((j.val : ℝ) + 1) / (8 * (n : ℝ))) -
291 (2 * π * (j.val : ℝ) / (8 * (n : ℝ)))| :=
292 rfp.phase_lipschitz _ _
293 _ = rfp.logDerivBound * (2 * π / (8 * (n : ℝ))) := by rw [hstep]
294
295/-! ### §7. Connection to Mathlib circle integrals
296
297This section bridges the abstract `ContinuousPhaseData.charge` (defined via
298`phase_winding`) to Mathlib's contour integrals, making the winding number
299connection machine-checkable.
300
301Key Mathlib theorems used:
302- `circleIntegral.integral_sub_inv_of_mem_ball`:
303 `∮ z in C(c, R), (z - w)⁻¹ = 2 * π * I` for `w ∈ ball c R`
304- `circleIntegral.integral_sub_zpow_of_ne`:
305 `∮ z in C(c, R), (z - w) ^ n = 0` for `n ≠ -1`
306- `circleIntegral_eq_zero_of_differentiable_on_off_countable`:
307 Cauchy–Goursat for functions differentiable off a countable set -/
308
309/-- The abstract winding number for a meromorphic function at a simple pole:
310the contour integral `(2πi)⁻¹ ∮ (z-w)⁻¹ dz = 1` for `w` inside the circle.
311
312This connects `ContinuousPhaseData.charge` for zpow to the Mathlib integral. -/