pith. sign in
module module high

IndisputableMonolith.NumberTheory.CompletedXiSymmetry

show as:
view Lean formalization →

This module supplies the minimal symmetry data for the completed xi function in Vector C constructions. It encodes reflection from the completed functional equation together with conjugation from reality symmetry, yielding zero pairings but no critical-line constraint. Researchers on zero-location problems in Recognition Science cite it as the base surface before defect costs are imposed. The module is purely definitional with no deductive content.

claimThe completed ξ surface equipped with reflection symmetry ξ(s) = ξ(1-s) and conjugation symmetry conjugate(ξ(conjugate(s))) = ξ(s), inducing zero pairings under ρ ↦ 1-ρ and ρ ↦ conjugate(ρ) but no forcing to Re ρ = 1/2.

background

This module sits in the NumberTheory domain and imports the ZeroLocationCost module. The upstream dictionary states: zeroDeviation ρ = 2 (Re ρ - 1/2) and zeroDefect ρ = defect (exp (zeroDeviation ρ)), linking zero locations to defect costs via the Recognition Science dictionary between zeta-zero location and zero-defect cost.

proof idea

This is a definition module, no proofs. It declares the symmetry invariants, the associated zero sets, and the pairing maps induced by reflection and conjugation.

why it matters in Recognition Science

The module supplies the base symmetry surface for the Vector C symmetry-only no-go result, which shows that functional-equation reflection plus conjugation produce pairing data on zeros but do not force the critical line. It fills the initial stage before any stronger zero-location constraint from the J-cost or phi-ladder is added on top of this surface.

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (12)