charge_additive
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.