doubledZeroDefect_zero_iff_on_critical_line
plain-language theorem explainer
The doubled zero defect vanishes precisely when the zero lies on the critical line. Number theorists examining Riemann zeros through Recognition Science's J-symmetry and defect observables would cite this equivalence. The proof rewrites the doubled defect to its closed-form cosh expression then applies the base zero-deviation criterion in both directions.
Claim. For $ρ ∈ ℂ$, let $D_2(ρ)$ denote the doubled zero defect $J(2·δ(ρ))$ with $δ$ the zero deviation and $J$ the Recognition Science cost function. Then $D_2(ρ) = 0$ if and only if $ρ$ lies on the critical line.
background
The Zero Doubling Law module records the strongest concrete Vector C instantiation from the functional-equation/J-symmetry bridge. It establishes that the defect observable satisfies the doubling recurrence $D(2t) = 2·D(t)^2 + 4·D(t)$. The doubled zero defect is defined as $J_log(2·zeroDeviation ρ)$, where zeroDeviation and OnCriticalLine come from ZeroLocationCost. Upstream structures supply the J-cost convexity from PhysicsComplexityStructure and the ledger factorization from DAlembert.LedgerFactorization.
proof idea
The proof rewrites via the lemma doubledZeroDefect_eq_cosh_sub_one. It splits the equivalence. Forward: assume doubled defect zero, derive contradiction if deviation nonzero via 1 < cosh(2·dev), conclude deviation zero by linarith, then apply zeroDeviation_eq_zero_iff_on_critical_line. Reverse: substitute deviation zero directly into the closed form.
why it matters
This result strengthens the Zero Doubling Law by showing the doubled defect inherits exact critical-line vanishing. It links to J-uniqueness (T5) and RCL self-composition in the Recognition framework. No downstream theorems yet reference it, but it supports the FE symmetry bridge to RS defect observables and touches the open question of whether the model forces all zeros onto the critical line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.