defect_phase_family_with_perturbation_exists
For any defect sensor with nonzero charge, a defect phase family attached to the sensor exists together with a nonempty collection of regular-factor perturbation witnesses. Researchers constructing the canonical sampled family and ring perturbation control in DefectSampledTrace cite this result to obtain the quantitative epsilon data for annular excess estimates. The proof is a direct term-mode instantiation of the trivial family and its zero-perturbation witness.
claimLet $S$ be a defect sensor with charge nonzero. Then there exists a defect phase family $D$ such that the sensor of $D$ equals $S$ and the type of defect phase perturbation witnesses for $D$ is nonempty.
background
A defect sensor records the pole order (charge) of $ζ^{-1}$ at a zero of $ζ$, together with its real part. From the upstream definition: 'A defect sensor at a point ρ: the field ζ(s)⁻¹ has a pole of order m at ρ (where m is the multiplicity of the zero of ζ).'
proof idea
The proof is a term-mode one-liner. It instantiates the trivial defect phase family for the given sensor and supplies the trivial perturbation witness, which sets all epsilon increments to zero while satisfying the increment equation and the smallness bound.
why it matters in Recognition Science
This existence result packages the perturbation witness required downstream for RingPerturbationControl and the annular excess argument. It is invoked by chosenDefectPhaseFamily, chosenDefectPhasePerturbationWitness, and the weaker defect_phase_family_exists in DefectSampledTrace. The construction closes the local meromorphic factorization into a quantitative package compatible with the phi-ladder cost estimates.
scope and limits
- Does not construct families with nonzero regular perturbation.
- Does not apply to sensors with zero charge.
- Does not guarantee uniqueness of the family or witness.
- Does not provide bounds beyond the trivial zero-perturbation case.
Lean usage
noncomputable def chosenDefectPhaseFamily (sensor : DefectSensor) (hm : sensor.charge ≠ 0) : DefectPhaseFamily := Classical.choose (defect_phase_family_with_perturbation_exists sensor hm)formal statement (Lean)
250theorem defect_phase_family_with_perturbation_exists (sensor : DefectSensor)
251 (_hm : sensor.charge ≠ 0) :
252 ∃ dpf : DefectPhaseFamily,
253 dpf.sensor = sensor ∧ Nonempty (DefectPhasePerturbationWitness dpf) := by
proof body
Term-mode proof.
254 refine ⟨trivialDefectPhaseFamily sensor, rfl, ?_⟩
255 exact ⟨trivialDefectPhasePerturbationWitness sensor⟩
256