Semantic Nonvacuity for ZeroData

Abstract

Separate outer universal vacuity from claims realized on an actual zeta-zero enumeration.

Theorem 1.1 (Universal claims acquire a real witness).

Lean statement: D5/S3/Weil/ZeroData/ZeroDataSemanticNonvacuity.realized_claim_with_nontrivial_zero

Proof. Machine-checked in Lean as D5/S3/Weil/ZeroData/ZeroDataSemanticNonvacuity.realized_claim_with_nontrivial_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every supplied ZeroData is indexed by the natural numbers and therefore already contains a zeroth represented zero. The possible vacuity is the emptiness of the outer type ZeroData itself.

Riemann-von Mangoldt growth supplies Nonempty ZeroData through the existing infinitude equivalence. A universally quantified theorem can then be instantiated on the selected exhaustive enumeration and on an actual represented nontrivial zeta zero.

References

• Truth anchor: D5/S3/Weil/ZeroData/ZeroDataSemanticNonvacuity.realized_claim_with_nontrivial_zero
• Dependency: D5/S3/Weil/ZeroData/CanonicalZeroDataFromRiemannVonMangoldt