doubledZeroDefect_recurrence
plain-language theorem explainer
The doubling recurrence equates the doubled zero defect at complex ρ to twice the square of the zero defect plus four times the zero defect. Researchers examining the functional-equation and RCL bridge in Recognition Science cite it as the concrete Phase-4 self-composition law on the defect observable. The proof is a short algebraic reduction that substitutes the cosh closed forms, applies the double-angle identity, and closes via nlinarith on the cosh-squared relation.
Claim. Let $D(ρ)$ denote the zero defect and $D^{(2)}(ρ)$ the doubled zero defect at $ρ ∈ ℂ$. Then $D^{(2)}(ρ) = 2 [D(ρ)]^2 + 4 D(ρ)$.
background
The Zero Doubling Law module records the strongest concrete Vector C instantiation obtained from the functional-equation/J-symmetry bridge. The defect observable satisfies the doubling recurrence $D(2t) = 2 D(t)^2 + 4 D(t)$. The defect functional is defined as defect(x) := J(x) for positive x, where J is the Recognition Science cost J(x) = (x + x^{-1})/2 - 1. The doubled zero defect is constructed by applying the J-log functional to twice the zero deviation.
proof idea
The proof is a short tactic sequence. It rewrites both sides via the closed forms doubledZeroDefect_eq_cosh_sub_one and zeroDefect_eq_cosh_sub_one. It then invokes Real.cosh_two_mul for the double-angle formula on cosh. The step closes with nlinarith applied to the identity Real.cosh_sq (zeroDeviation ρ).
why it matters
This supplies the recurrence packaged into current_vectorC_attempt_data, which asserts the zero-defect equivalence to the critical line together with nonnegativity and the doubling law. It is also invoked inside pureVectorCDoublingData_of_zero to equip any completed-ξ zero with the pairing invariants plus the FE/RCL doubling recurrence. The result instantiates the Phase-4 self-composition law from the FE/RCL bridge, giving concrete evidence of nontrivial interaction between FE symmetry and the RS defect while remaining short of the full d'Alembert interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.