`pureVectorCDoublingData_not_enough_for_critical_line`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.VectorCSymmetryOnlyNoGo
domain: NumberTheory
line: 149 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.VectorCSymmetryOnlyNoGo on GitHub at line 149.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 146
 147/-- In particular, pure FE symmetry plus the current doubling law do not by
 148themselves force the critical line. -/
 149theorem pureVectorCDoublingData_not_enough_for_critical_line :
 150    ¬ (∀ (Ξ : CompletedXiSurface) (ρ : ℂ),
 151        PureVectorCDoublingData Ξ ρ → OnCriticalLine ρ) := by
 152  intro h
 153  obtain ⟨Ξ, ρ, hpure, hline⟩ := pureVectorCDoublingData_offline_example
 154  exact hline (h Ξ ρ hpure)
 155
 156end
 157
 158end NumberTheory
 159end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.