zeroDeviationSet
zeroDeviationSet collects the real deviation values realized at the zeros of a supplied completed-ξ surface. Researchers working on zero-pairing invariants for Vector C cite this definition when deriving negation symmetry from the functional equation. The definition is a direct set comprehension that extracts zeroDeviation values from the zeros of the xi map.
claimLet $Ξ$ be a completed-ξ surface. Then zeroDeviationSet$(Ξ)$ is the set of all real $t$ such that there exists complex $s$ with $Ξ.xi(s)=0$ and zeroDeviation$(s)=t$.
background
CompletedXiSurface is the minimal structure that supplies a map xi : ℂ → ℂ together with the reflection axiom xi(1-s)=xi(s) and the conjugation axiom xi(conj s)=conj(xi s). zeroDeviation is the real-valued function on ℂ that records the deviation cost of each point, imported from the zero-location cost module. The present module deliberately restricts itself to these pairing data and does not yet encode any d'Alembert-style composition law.
proof idea
One-line definition that builds the set by existential quantification over the zeros of Ξ.xi and the matching zeroDeviation values.
why it matters in Recognition Science
The definition supplies the deviation set that is proved negation-closed in the downstream theorem zeroDeviationSet_neg_closed, which follows immediately from the reflection property of the completed-ξ surface. It therefore records the strongest zero-location consequence currently available from the minimal functional-equation symmetry surface for Vector C. The module leaves open whether this negation-closed property forces the only realized deviation to be zero.
scope and limits
- Does not impose any zero-location constraints beyond the minimal reflection and conjugation axioms.
- Does not claim that zero is the only element of the set.
- Does not derive a composition law from the d'Alembert ledger.
Lean usage
theorem neg_closed_example (Ξ : CompletedXiSurface) (t : ℝ) (ht : t ∈ zeroDeviationSet Ξ) : -t ∈ zeroDeviationSet Ξ := zeroDeviationSet_neg_closed Ξ htformal statement (Lean)
38def zeroDeviationSet (Ξ : CompletedXiSurface) : Set ℝ :=
proof body
Definition body.
39 { t : ℝ | ∃ s : ℂ, Ξ.xi s = 0 ∧ zeroDeviation s = t }
40
41/-- The set of zero defects realized by zeros of a completed-ξ surface. -/