def definition def or abbrev

`OnCriticalLine`

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

formal statement (Lean)

  25def OnCriticalLine (ρ : ℂ) : Prop :=

proof body

Definition body.

  26  ρ.re = 1 / 2
  27
  28/-- Reflection across the line `Re(s) = 1/2`. -/

used by (19)

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
CompositionClosureHypothesis in IndisputableMonolith.NumberTheory.CompositionDivergence decl_use
CompositionRHCertificate in IndisputableMonolith.NumberTheory.CompositionDivergence decl_use
composition_violates_budget in IndisputableMonolith.NumberTheory.CompositionDivergence decl_use
rh_from_composition_closure in IndisputableMonolith.NumberTheory.CompositionDivergence decl_use
completedXiSurface_symmetry_only_no_go in IndisputableMonolith.NumberTheory.VectorCSymmetryOnlyNoGo decl_use
pureVectorCDoublingData_not_enough_for_critical_line in IndisputableMonolith.NumberTheory.VectorCSymmetryOnlyNoGo decl_use
pureVectorCDoublingData_offline_example in IndisputableMonolith.NumberTheory.VectorCSymmetryOnlyNoGo decl_use
toyCompletedXiSurface_has_off_critical_zero in IndisputableMonolith.NumberTheory.VectorCSymmetryOnlyNoGo decl_use
zeroDeviationSet_neg_closed_not_enough in IndisputableMonolith.NumberTheory.VectorCSymmetryOnlyNoGo decl_use
rh_equivalent_to_zero_cost in IndisputableMonolith.NumberTheory.XiJBridge decl_use
zeroCompositionLaw_forces_eta_zero in IndisputableMonolith.NumberTheory.ZeroCompositionInterface decl_use
zeroCompositionWitness_forces_on_critical_line in IndisputableMonolith.NumberTheory.ZeroCompositionInterface decl_use
zero_composition_diverges in IndisputableMonolith.NumberTheory.ZeroCompositionLaw decl_use
current_vectorC_attempt_data in IndisputableMonolith.NumberTheory.ZeroDoublingLaw decl_use
doubledZeroDefect_zero_iff_on_critical_line in IndisputableMonolith.NumberTheory.ZeroDoublingLaw decl_use
zeroDefect_pos_iff_off_critical_line in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use
zeroDefect_zero_iff_on_critical_line in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use
zeroDeviation_eq_zero_iff_on_critical_line in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use