genuine_pure_increment_abs_eq
plain-language theorem explainer
The theorem computes the absolute magnitude of the pure winding increment generated by a genuine zeta-derived phase family at sampling level n. Analysts studying annular cost perturbations around meromorphic poles in the Recognition Science framework cite this identity to isolate the exact contribution from the pole factor before bounding regular perturbations. The proof is a direct calculation that unfolds the family definition and simplifies the resulting absolute value expression using field arithmetic and absolute value identities.
Claim. Let $S$ be a defect sensor with charge $c$ and let $Q$ be a quantitative local factorization satisfying $Q.order = -c$. For each natural number $n > 0$, the absolute value of the pure increment of the genuine zeta-derived phase family built from $S$ and $Q$ equals $ (π ⋅ |c| / 4) / n $.
background
The module bridges Mathlib meromorphic-order machinery to the RS annular cost framework. A meromorphic function with order $n$ at $ρ$ factors locally as $(z-ρ)^n g(z)$ where $g$ is holomorphic and nonvanishing at $ρ$; the power term carries phase charge $-n$ while $g$ carries charge 0, so the total charge is $-n$. For the RS/RH application, $ζ^{-1}$ has meromorphic order $-m$ at a zero of multiplicity $m$, yielding phase charge $m$ that matches the DefectSensor.charge. QuantitativeLocalFactorization extends LocalMeromorphicWitness by a uniform bound $M$ on $|g'/g|$ together with the regime condition $M ⋅ radius ≤ 1$; this bound controls the size of the regular perturbation $ε_j$ on sampled circles.
proof idea
The tactic proof opens a calc block and applies simp to unfold defectPhasePureIncrement and genuineZetaDerivedPhaseFamily, producing the concrete expression |−(2π charge)/(8n)|. It then rewrites the absolute value of a quotient using abs_div and abs_of_pos, replaces the negated charge by its absolute value via abs_neg and Int.cast_abs, and finishes with field_simp plus ring to reduce the coefficient 2π/8 to π/4.
why it matters
This identity supplies the exact pure term in the decomposition required by genuineZetaDerivedPhasePerturbationWitness, which in turn feeds the perturbation bounds for canonicalDefectSampledFamily_ringPerturbationControl. It confirms that the winding contribution from the pole part of ζ^{-1} scales exactly as 1/n, consistent with eight-tick angular sampling and the phase-charge matching between meromorphic order and DefectSensor. The result closes one analytic input in the meromorphic-circle-order layer of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.