`pureVectorCDoublingData_requires_extra_input`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NumberTheory.VectorCSymmetryOnlyNoGo on GitHub at line 139.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 136the pure FE package; in this repository the natural candidates live on the
 137Euler/Hadamard side (`QuantitativeLocalFactorization`,
 138`phaseIncrementEpsilonBound`, perturbation/budget control). -/
 139theorem pureVectorCDoublingData_requires_extra_input :
 140    ¬ (∀ (Ξ : CompletedXiSurface) (ρ : ℂ),
 141        PureVectorCDoublingData Ξ ρ → Nonempty (ZeroCompositionWitness ρ)) := by
 142  intro h
 143  obtain ⟨Ξ, ρ, hpure, hline⟩ := pureVectorCDoublingData_offline_example
 144  rcases h Ξ ρ hpure with ⟨w⟩
 145  exact hline (zeroCompositionWitness_forces_on_critical_line w)
 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.