norm_form_eq_carrierDerivTerm
plain-language theorem explainer
The equality shows that the squared-norm form of the per-prime Euler factor exactly matches the real carrier derivative term at the real part of s. Analysts bounding logarithmic derivatives of the zeta function via Recognition Science carriers cite this when instantiating abstract cost axioms with concrete Euler products. The tactic proof rewrites the complex norm to a real power, unfolds the term definitions, verifies the doubled-exponent identity via rpow_add, and commutes the log factor.
Claim. For a prime $p$ and complex $s$, the expression $ (log p) |prime power complex factor at p and s|^2 / (1 - |prime power complex factor at p and s|) equals the per-prime carrier derivative term evaluated at the real part of $s$.
background
The module shows how the Euler product for the zeta function satisfies the abstract carrier and sensor framework from AnnularCost and CostCoveringBridge. Core objects include the prime sum, Hilbert-Schmidt norm of the operator A(s), carrier log series, and carrier derivative bound as the sum over primes of (log p) p^{-2 sigma} / (1 - p^{-sigma}). This theorem supplies the exact per-prime match between the norm expression from the complex factor and the real derivative term. Upstream results supply the norm identity for the Euler prime power complex and the definition of the carrier derivative term.
proof idea
The proof first records positivity of p. It rewrites the norm of the Euler prime power complex using the real power identity, unfolds carrierDerivTerm and primeLog, proves the squared power equals the double-exponent form via rpow_add and ring, then commutes the log factor to reach the target.
why it matters
This equality is invoked by the subsequent inequality that bounds the complex per-prime log-derivative term by the carrier derivative. It advances the module goal of showing the Euler product satisfies the EulerCarrier and RegularCarrier interfaces, which permits the cost-covering axiom and yields a conditional Riemann hypothesis. It corresponds to the concrete-to-abstract step linking Euler factors to bounded logarithmic derivative in the Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.