Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

PrimeQuadraticLValues

Abstract

The character is the actual integer quadratic character mapped to complex coefficients. Nontriviality and prime modulus prove primitivity. Doubling least representatives, with the genuine L(0) finite evaluation, gives the lower-half sum (2-chi(2))*L(0). The L(0) supplier is the existing attributed Yao Xu/cadamcat port, not newly authored source.

The character is the actual integer quadratic character mapped to complex coefficients. Nontriviality and prime modulus prove primitivity. Doubling least representatives, with the genuine L(0) finite evaluation, gives the lower-half sum (2-chi(2))*L(0). The L(0) supplier is the existing attributed Yao Xu/cadamcat port, not newly authored source.

Four-slot escape registrations are unfinished, tracked at https://github.com/the-omega-institute/trureturing/issues/26321. No declared_validated status is claimed. This registration debt is separate from the native mathematical proof.

Definition 1.1 (primeCharacter).

Lean statement: D5/S3/Analytic/Zeta/PrimeQuadraticLValues.primeCharacter

Formalization. D5/S3/Analytic/Zeta/PrimeQuadraticLValues.primeCharacter (✓ std3).

Source. Repository-derived.

Acknowledgement. Deyi Chen and Zhi-Wei Sun (2024). On determinants involving (j+k/p) plus or minus (j-k/p). DOI: 10.48550/arXiv.2409.08213. URL: https://arxiv.org/html/2409.08213v4#S1.E11.

Commentary.

The same integer-valued quadratic character as in the Legendre symbol, mapped to the coefficient field used by Mathlib’s L-functions.

Theorem 1.2 (primeCharacter_quadratic).

Lean statement: D5/S3/Analytic/Zeta/PrimeQuadraticLValues.primeCharacter_quadratic

Proof. Machine-checked in Lean as D5/S3/Analytic/Zeta/PrimeQuadraticLValues.primeCharacter_quadratic (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Deyi Chen and Zhi-Wei Sun (2024). On determinants involving (j+k/p) plus or minus (j-k/p). DOI: 10.48550/arXiv.2409.08213. URL: https://arxiv.org/html/2409.08213v4#S1.E11.

Commentary.

The exact Lean declaration D5.S3.Analytic.Zeta.PrimeQuadraticLValues.primeCharacter_quadratic supplies this step in the proof chain described above; its complete Lean statement is retained in the scoped report. The pinned projection corpus has no formula for this new declaration.

Theorem 1.3 (primeCharacter_nontrivial).

Lean statement: D5/S3/Analytic/Zeta/PrimeQuadraticLValues.primeCharacter_nontrivial

Proof. Machine-checked in Lean as D5/S3/Analytic/Zeta/PrimeQuadraticLValues.primeCharacter_nontrivial (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Deyi Chen and Zhi-Wei Sun (2024). On determinants involving (j+k/p) plus or minus (j-k/p). DOI: 10.48550/arXiv.2409.08213. URL: https://arxiv.org/html/2409.08213v4#S1.E11.

Commentary.

The exact Lean declaration D5.S3.Analytic.Zeta.PrimeQuadraticLValues.primeCharacter_nontrivial supplies this step in the proof chain described above; its complete Lean statement is retained in the scoped report. The pinned projection corpus has no formula for this new declaration.

Theorem 1.4 (primeCharacter_primitive).

Lean statement: D5/S3/Analytic/Zeta/PrimeQuadraticLValues.primeCharacter_primitive

Proof. Machine-checked in Lean as D5/S3/Analytic/Zeta/PrimeQuadraticLValues.primeCharacter_primitive (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Deyi Chen and Zhi-Wei Sun (2024). On determinants involving (j+k/p) plus or minus (j-k/p). DOI: 10.48550/arXiv.2409.08213. URL: https://arxiv.org/html/2409.08213v4#S1.E11.

Commentary.

The exact Lean declaration D5.S3.Analytic.Zeta.PrimeQuadraticLValues.primeCharacter_primitive supplies this step in the proof chain described above; its complete Lean statement is retained in the scoped report. The pinned projection corpus has no formula for this new declaration.

Theorem 1.5 (primeCharacter_odd).

Lean statement: D5/S3/Analytic/Zeta/PrimeQuadraticLValues.primeCharacter_odd

Proof. Machine-checked in Lean as D5/S3/Analytic/Zeta/PrimeQuadraticLValues.primeCharacter_odd (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Deyi Chen and Zhi-Wei Sun (2024). On determinants involving (j+k/p) plus or minus (j-k/p). DOI: 10.48550/arXiv.2409.08213. URL: https://arxiv.org/html/2409.08213v4#S1.E11.

Commentary.

The exact Lean declaration D5.S3.Analytic.Zeta.PrimeQuadraticLValues.primeCharacter_odd supplies this step in the proof chain described above; its complete Lean statement is retained in the scoped report. The pinned projection corpus has no formula for this new declaration.

Theorem 1.6 (half_sum_eq_LFunction_zero).

Lean statement: D5/S3/Analytic/Zeta/PrimeQuadraticLValues.half_sum_eq_LFunction_zero

Proof. Machine-checked in Lean as D5/S3/Analytic/Zeta/PrimeQuadraticLValues.half_sum_eq_LFunction_zero (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Deyi Chen and Zhi-Wei Sun (2024). On determinants involving (j+k/p) plus or minus (j-k/p). DOI: 10.48550/arXiv.2409.08213. URL: https://arxiv.org/html/2409.08213v4#S1.E11.

Commentary.

A finite doubling argument gives the half-interval sum from the actual analytic L(0). This theorem uses no class-number parameter or class-number identity.

References