pith. machine review for the scientific record. sign in
theorem proved term proof

pureVectorCDoublingData_offline_example

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 123theorem pureVectorCDoublingData_offline_example :
 124    ∃ Ξ : CompletedXiSurface, ∃ ρ : ℂ,
 125      PureVectorCDoublingData Ξ ρ ∧ ¬ OnCriticalLine ρ := by

proof body

Term-mode proof.

 126  refine ⟨toyCompletedXiSurface, (3 / 4 : ℂ), ?_, ?_⟩
 127  · exact pureVectorCDoublingData_of_zero toyCompletedXiSurface
 128      toyCompletedXiSurface_has_off_critical_zero.1
 129  · exact toyCompletedXiSurface_has_off_critical_zero.2
 130
 131/-- Even after adding the current FE/RCL doubling law, pure completed-ξ
 132symmetry data still cannot force a `ZeroCompositionWitness`.
 133
 134Therefore any successful upgrade from honest zeta-derived phase data to
 135`ZeroCompositionWitness` must use genuinely extra analytic input not present in
 136the pure FE package; in this repository the natural candidates live on the
 137Euler/Hadamard side (`QuantitativeLocalFactorization`,
 138`phaseIncrementEpsilonBound`, perturbation/budget control). -/

used by (2)

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

depends on (14)

Lean names referenced from this declaration's body.