theorem proved term proof

`defectIterate_zero_eq_zeroDefect`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 184theorem defectIterate_zero_eq_zeroDefect (ρ : ℂ) :
 185    defectIterate (zeroDeviation ρ) 0 = zeroDefect ρ := by

proof body

Term-mode proof.

 186  rw [defectIterate_zero_eq_J_log, zeroDefect_eq_J_log]
 187
 188/-- **The composition law for zeta zeros, final form.**
 189
 190    If ρ is off the critical line, the iterated composition defect
 191    diverges, generating arbitrarily large cost values from a single zero. -/

depends on (15)

Lean names referenced from this declaration's body.

defect in IndisputableMonolith.Foundation.LawOfExistence decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
zeta in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions decl_use
defectIterate in IndisputableMonolith.NumberTheory.ZeroCompositionLaw decl_use
defectIterate_zero_eq_J_log in IndisputableMonolith.NumberTheory.ZeroCompositionLaw decl_use
zeroDefect in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use
zeroDefect_eq_J_log in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use
zeroDeviation in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use