theorem proved term proof

`zeroCompositionWitness_forces_on_critical_line`

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

formal statement (Lean)

  91theorem zeroCompositionWitness_forces_on_critical_line
  92    {ρ : ℂ} (w : ZeroCompositionWitness ρ) :
  93    OnCriticalLine ρ :=

proof body

Term-mode proof.

  94  (zeroCompositionLaw_forces_eta_zero w.law ρ).mp w.value_at_deviation
  95
  96/-- Therefore the zero-location defect must vanish there as well. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

charge_zero_of_honest_phase_of_vectorC in IndisputableMonolith.NumberTheory.AnalyticTrace decl_use
pureVectorCDoublingData_requires_extra_input in IndisputableMonolith.NumberTheory.VectorCSymmetryOnlyNoGo decl_use
zeroCompositionWitness_forces_zero_defect in IndisputableMonolith.NumberTheory.ZeroCompositionInterface decl_use

depends on (5)

Lean names referenced from this declaration's body.

defect in IndisputableMonolith.Foundation.LawOfExistence decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
zeroCompositionLaw_forces_eta_zero in IndisputableMonolith.NumberTheory.ZeroCompositionInterface decl_use
ZeroCompositionWitness in IndisputableMonolith.NumberTheory.ZeroCompositionInterface decl_use
OnCriticalLine in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use