defectIterate_zero_eq_J_log
The zero-level defect for real deviation t equals the logarithmic J-cost. Analysts of the zeta zero composition law cite this base case to initialize the defect cascade under the Recognition Composition Law. The proof is a direct simplification that unfolds the iteration definition together with the log form of J.
claimFor any real number $t$, the zero-level defect satisfies $d_0(t) = 2^{-1}(e^t + e^{-t}) - 1$.
background
The module develops the composition law for zeta zeros induced by the Recognition Composition Law on the J functional equation. For a zero with real deviation parameter t, the initial defect is the level-zero term of the iteration sequence. Upstream, J_log is defined by J(e^t) = cosh(t) - 1; the doc-comment states: 'J in log coordinates: J(eᵗ) = cosh(t) - 1. This is a convex bowl centered at t = 0.'
proof idea
The proof is a one-line term-mode simplification that rewrites using the definitions of defectIterate at iteration count zero and J_log from the DiscretenessForcing foundation.
why it matters in Recognition Science
This supplies the base case for the defect iteration sequence in the zero composition law. It is invoked directly by defectIterate_zero_eq_zeroDefect to equate the iterated defect to zeroDefect and by defectIterate_zero_pos to obtain strict positivity for t ≠ 0. The step connects J-uniqueness (T5) to the exponential amplification of defects for off-critical zeros, consistent with the eight-tick octave.
scope and limits
- Does not establish the successor recurrence d_{n+1} = 2 d_n (d_n + 2).
- Does not prove positivity or growth bounds for the sequence.
- Does not map complex zeta zeros to the real deviation parameter t.
- Does not derive the Recognition Composition Law from axioms.
formal statement (Lean)
61theorem defectIterate_zero_eq_J_log (t : ℝ) :
62 defectIterate t 0 = Foundation.DiscretenessForcing.J_log t := by
proof body
Term-mode proof.
63 simp [defectIterate, Foundation.DiscretenessForcing.J_log]
64
65/-- dₙ ≥ 0 for all n and t (from cosh ≥ 1). -/