trivialDefectPhaseFamily
plain-language theorem explainer
The definition constructs a DefectPhaseFamily for any given DefectSensor by direct field assignment using pure winding phase data and no regular perturbation. Researchers building base cases for annular cost bounds or meromorphic order arguments in Recognition Science cite this as the unperturbed starting point before adding epsilon witnesses. The construction is realized by structure instantiation with fixed radius 1 and charge equality proved by reflexivity.
Claim. Let $s$ be a defect sensor. The trivial defect phase family for $s$ is the structure with sensor $s$, witness radius $1$, phase data at each level given by the pure defect phase function of $s$, and uniform charge equal to the charge of $s$.
background
DefectPhaseFamily is the structure that packages a constant-radius phase family carrying a prescribed defect charge: it requires a sensor, positive witness radius, a map from level $n$ to ContinuousPhaseData, and a proof that every such phase datum has charge exactly equal to the sensor charge. The module MeromorphicCircleOrder bridges Mathlib meromorphic-order machinery to the RS annular cost framework, where a meromorphic function with order $n$ at a point factors locally as $(z - rho)^n g(z)$ with $g$ holomorphic and nonvanishing, yielding phase charge $-n$ from the pole part and $0$ from the regular factor. Upstream results supply the defect functional (equal to the J-cost for positive arguments) and the eight-tick phase definition used to realize the pure winding increments.
proof idea
The definition is a direct structure instantiation. It sets the sensor field to the input, fixes witnessRadius to 1 with a norm_num positivity proof, assigns phaseAtLevel to pureDefectPhaseData sensor, and discharges the charge_uniform obligation by reflexivity on each level.
why it matters
This supplies the unperturbed base case required by defect_phase_family_with_perturbation_exists, which packages both the family and its zero-perturbation witness for the annular excess argument. It is used downstream in charge_zero_of_covered and zetaDerivedPhaseData_charge to close the pure-defect side of the meromorphic factorization before perturbation control is applied. The construction aligns with the module's goal of matching the phase charge of zeta inverse to the defect sensor charge, supporting the analytic route to the Riemann hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.