defect_phase_family_exists
Given a defect sensor with nonzero charge, there exists a defect phase family whose associated sensor matches the given one. This result is cited in proofs of honest argument principle sampling within the Riemann hypothesis formalization. The proof reduces to extracting the family from a stronger existence statement that includes perturbation data.
claimLet $S$ be a defect sensor with nonzero charge. Then there exists a defect phase family $D$ such that the sensor component of $D$ equals $S$.
background
The module bridges Mathlib meromorphic-order machinery to the Recognition Science annular cost framework. A meromorphic function with order $n$ at a point factors locally as $(z - rho)^n g(z)$ where $g$ is analytic and nonvanishing, inducing phase charge $-n$ from the pole factor and charge $0$ from the regular factor. For the zeta inverse this yields charge equal to the multiplicity $m$ at a zero, matching the defect sensor charge. A defect phase family is a constant-radius package consisting of the sensor, a positive witness radius, a map from positive integers to continuous phase data, and the uniformity condition that every phase datum carries exactly the sensor charge.
proof idea
The proof is a one-line wrapper that applies the perturbation-aware existence theorem to the sensor and nonzero-charge hypothesis, then returns the family while discarding the perturbation witness.
why it matters in Recognition Science
This supplies the existence of a phase family for argument_principle_honest, which builds annular meshes from actual phase samples near hypothetical zeros rather than uniform constructions. It supports the honest sampling path in the Riemann hypothesis formalization, leaving only one genuine axiom. The result aligns with the meromorphic-order phase-charge calculation for zeta inverse and feeds the quantitative local factorization section that controls logarithmic derivatives on sampled circles.
scope and limits
- Does not construct the phase data explicitly.
- Does not bound the witness radius.
- Does not quantify the size of perturbations.
- Does not connect to the phi-ladder or J-cost directly.
Lean usage
obtain ⟨dpf, rfl⟩ := defect_phase_family_exists sensor hm exact ⟨defectAnnularMesh dpf N, rfl⟩formal statement (Lean)
257theorem defect_phase_family_exists (sensor : DefectSensor)
258 (hm : sensor.charge ≠ 0) :
259 ∃ dpf : DefectPhaseFamily, dpf.sensor = sensor := by
proof body
Term-mode proof.
260 obtain ⟨dpf, hdpf, _⟩ := defect_phase_family_with_perturbation_exists sensor hm
261 exact ⟨dpf, hdpf⟩
262
263/-! ### §4. Quantitative local factorization -/
264
265/-- A quantitative local factorization extends the basic witness with a
266uniform bound `M` on the logarithmic derivative `|g'/g|` of the regular
267factor over the disk. This is the analytic input that controls the
268phase perturbation `ε_j` on sampled circles. -/