pith. sign in
module module high

IndisputableMonolith.NumberTheory.CompletedXiSymmetry

show as:
view Lean formalization →

This module supplies the minimal completed-ξ symmetry surface for Vector C. It encodes reflection from the functional equation and conjugation from reality, which together induce zero pairings. Researchers testing whether these symmetries alone force the critical line cite it as the base layer before stronger constraints. The module is purely definitional with no proofs.

claimA completed-ξ surface equipped with reflection invariance from the functional equation and conjugation invariance from reality, inducing zero pairings via zeroDeviation and zeroDefect without forcing the critical line.

background

The module imports the zero-location cost dictionary from ZeroLocationCost, where zeroDeviation ρ = 2 (Re ρ - 1/2) and zeroDefect ρ = defect (exp (zeroDeviation ρ)). It establishes the base symmetry data for the completed ξ in the Recognition Science number-theory setting. The doc-comment states that reflection is the completed functional equation and conjugation is the standard reality symmetry, with any stronger zero-location constraint added on top.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module feeds the Vector C Symmetry-Only No-Go result, which certifies that functional-equation reflection plus conjugation give pairing data on zeros but do not force the critical line. It supplies the minimal symmetry surface on which the no-go toy example is built.

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)