chosenDefectPhasePerturbationWitness
plain-language theorem explainer
This definition extracts the regular-factor perturbation witness attached to the chosen phase family of a defect sensor with nonzero charge. Researchers constructing the ring perturbation control package for the Axiom 2 attack in Recognition Science cite it to obtain concrete data for bounding realized annular excess. The construction is a direct one-line extraction via classical choice from the second component of the strengthened existential package.
Claim. Let $s$ be a defect sensor with nonzero charge $m$. The chosen phase family attached to $s$ carries a perturbation witness $w$ certifying the regular factor in the local factorization of the inverse zeta function near the hypothetical defect.
background
The Defect Sampled Trace module packages realized annular meshes for the phase-sampling construction attached to a hypothetical zeta defect. After Axiom 1 is eliminated, the remaining bottleneck is Axiom 2: one must bound the cost of the canonical sampled family coming from the phase of zeta inverse near the defect, rather than quantifying over all possible annular meshes. A DefectSensor is the structure recording the multiplicity (charge) of the zero of zeta together with its real part and the fact that it lies in the right half of the critical strip. The sibling definition chosenDefectPhaseFamily selects one such family using the strengthened existential statement defect_phase_family_with_perturbation_exists, which already guarantees the presence of the required perturbation witness.
proof idea
One-line wrapper that applies Classical.choice to the second component of the choose_spec for defect_phase_family_with_perturbation_exists sensor hm.
why it matters
This supplies the concrete witness required by the downstream definition canonicalDefectSampledFamily_ringPerturbationControl, the quantitative target for the Axiom 2 attack. That parent object is the theorem that the current complex-analysis stack ought to prove from local factorization together with a log-derivative bound on the regular factor; once established it yields realizedDefectCostBounded_iff_charge_zero_and_excessBounded. In the Recognition framework the witness closes the packaging step between the existential guarantee and the control data needed to derive a contradiction with annular coercivity when the charge is nonzero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.