trivialDefectPhasePerturbationWitness
plain-language theorem explainer
The definition supplies a zero-perturbation witness for the trivial defect phase family on any defect sensor. Researchers applying meromorphic order to annular cost bounds in Recognition Science cite it to close the base case of the perturbation control. The construction sets the epsilon field to the zero function and discharges the increment equality, smallness, and term bounds by direct simplification and ring arithmetic.
Claim. Let $S$ be a defect sensor. The zero-perturbation witness for the trivial defect phase family of $S$ is the structure instance with perturbation term identically zero, satisfying the decomposition of each sampled increment into the pure winding increment plus zero, the bound $|log phi times epsilon| le 1$, and the existence of constant zero for the summable linear and quadratic error terms over refinement depth $N$.
background
DefectPhasePerturbationWitness is the structure recording quantitative bounds on the regular-factor perturbation epsilon inside a defect phase family. It requires that each sampled increment splits as the pure winding increment plus epsilon, that the absolute value of log phi times epsilon stays at most 1, and that the linear and quadratic coefficients in the phi-cost expansion remain summable uniformly in refinement depth N. This sits inside the MeromorphicCircleOrder module, which bridges Mathlib meromorphic-order factorization to the Recognition Science annular cost framework, showing that zeta inverse with pole order m at rho carries phase charge m matching the defect sensor charge. Upstream, the eight-tick phase supplies the discrete phases k pi over 4, the defect functional equals J, and ContinuousPhaseData packages the continuous phase assignment on the circle.
proof idea
The definition sets epsilon to the constant zero function. The increment_eq field is discharged by dsimp to the pure increment definition, followed by field_simp and ring to cancel the nonzero denominator. The small field follows by simp. The linear_term_bounded and quadratic_term_bounded fields are witnessed by the constant zero, with the forall N discharged by simp.
why it matters
This supplies the witness required by the strong existence theorem defect_phase_family_with_perturbation_exists, which packages a defect phase family together with its perturbation witness for the annular excess argument. It closes the base case for the trivial family in the meromorphic order application to phase charges and the eight-tick octave. The construction touches the open question of extending the perturbation bounds to non-trivial regular factors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.