zetaDerivedPhaseFamily_excess_zero
plain-language theorem explainer
A phase family derived from the zeta function through a defect sensor and quantitative local factorization with order matching the negative sensor charge has vanishing annular excess at every mesh depth. Researchers bridging analytic number theory to Recognition Science cite this to place such families exactly on the topological floor. The proof reduces the excess to zero by unfolding annular cost and floor, establishing constant ring increments from the pure defect phase, and summing to the topological floor via constant-term evaluation.
Claim. Let $S$ be a defect sensor and $Q$ a quantitative local factorization with order equal to the negative of the charge of $S$. For any natural number $N$, the annular excess of the mesh at depth $N$ of the sampled family obtained from the zeta-derived phase family of $S$ and $Q$ is zero.
background
The Honest Phase Budget Bridge module supplies perturbation witnesses that convert phase families into sampled data with controlled annular excess. Key supporting definitions include the 8-tick phase (periodic angles $kπ/4$ for $k=0..7$), the defect functional (equal to the J-cost $J(x)=(x+x^{-1})/2-1$ for positive $x$), and the active edge count $A=1$ per fundamental tick. The cost of a recognition event is its J-cost, and the topological floor counts the cumulative phase steps needed to close the annular budget at a given charge and mesh depth. Upstream results establish that defect equals J at unity and that the 8-tick structure enforces the period-8 octave used in mesh construction.
proof idea
The tactic proof unfolds annularExcess, annularCost, and annularTopologicalFloor, rewrites the difference to zero, then applies Finset.sum_congr. It introduces a constant-increment lemma showing every ring increment equals the pure defect phase increment (via zetaDerivedPhasePerturbationWitness.increment_eq and defectPhasePureIncrement). The calculation then replaces the ring cost sum with a constant multiple that equals the topological floor by Finset.sum_const and nsmul_eq_mul.
why it matters
This result places the zeta-derived phase family exactly on the topological floor, feeding directly into honestPhaseFamily_excess_zero via the family_derived simplification. It supplies the Euler/Hadamard-style quantitative control described in the module doc-comment, linking the eight-tick octave and defect cost to zero excess on sampled meshes. The declaration closes one concrete case in the perturbation-witness package needed for bounded annular data, while the broader question of excess bounds for arbitrary honest families remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.