regular_factor_increment_decomposition
The decomposition states that every sampled phase increment on the nth ring of a defect phase family equals the pure topological winding term plus the regular perturbation epsilon supplied by the witness. Researchers building ring perturbation control for the canonical defect family in the Axiom 2 attack cite this identity to separate topological floor from excess cost. The proof is a direct one-line appeal to the increment_eq field inside the DefectPhasePerturbationWitness structure.
claimLet $dpf$ be a defect phase family with perturbation witness $hw$. For each $n > 0$ and $j$ in the $8n$ samples, the $j$th sampled increment of the phase data at level $n$ satisfies $I_j^{(n)} = -2π · charge(dpf) / (8n) + ε(n,j)$, where $ε(n,j)$ is the regular perturbation term from $hw$.
background
The MeromorphicCircleOrder module extracts local meromorphic factorizations from Mathlib's meromorphicOrderAt machinery and feeds them into the RS annular cost framework. A DefectPhaseFamily consists of a fixed-charge DefectSensor together with a family of ContinuousPhaseData objects, one per refinement level $n$, each carrying uniform charge equal to the sensor charge. The companion DefectPhasePerturbationWitness records, for every level and sample index, a real-valued epsilon such that the sampled increment splits exactly into the pure winding term plus epsilon, with epsilon bounded by $1/|log φ|$ in absolute value.
proof idea
The proof is the one-line term application of the increment_eq field from the DefectPhasePerturbationWitness: it substitutes the witness equality directly into the definition of sampleIncrements.
why it matters in Recognition Science
This identity supplies the exact splitting required by phaseFamily_ringPerturbationControl and canonicalDefectSampledFamily_ringPerturbationControl. Those definitions assemble the RingPerturbationControl package that bounds excess cost above the topological floor for the Axiom 2 attack on the Riemann hypothesis. It realizes the local factorization of ζ^{-1} around a zero of multiplicity m, converting the meromorphic order into a phase charge that matches the defect sensor while confining the regular factor contribution to a small perturbation in the phi-cost scale.
formal statement (Lean)
187theorem regular_factor_increment_decomposition
188 {dpf : DefectPhaseFamily} (hw : DefectPhasePerturbationWitness dpf)
189 (n : ℕ) (hn : 0 < n) (j : Fin (8 * n)) :
190 (dpf.phaseAtLevel n hn).sampleIncrements n j =
191 defectPhasePureIncrement dpf n + hw.epsilon n hn j :=
proof body
Term-mode proof.
192 hw.increment_eq n hn j
193
194/-- The perturbation term lies in the unit-scale regime required by the proved
195`phiCost` perturbation lemma. -/