Finite positive synthesis and correction on the original selected coefficient space
DefinitionConnesGreen_finite_selected_correctionconnes-weilselected-correction-certificates
For finite actual-zero packet F, define P_F by the existing column-synthesis constructor applied to exactly the original positive F columns on the original physical carrier. Keep N as the original selected negative synthesis for packet S. With C=P_F* N and B=P_F* P_F + δI, define the selected coefficient correction D_S=δI−N* N+C* Ring.inverse(B) C on the ORIGINAL selected coefficient space. The inverse is the existing ring inverse; for δ>0 its coefficient covariance is proved strictly positive in subsequent theorems. No full positive actor, negative packet, zero subtype, multiplicity, carrier, or test predicate is replaced. No positivity assertion is embedded in this definition bundle.
Definition code
import Definitions.Def_ConnesGreen_integral_certificate_kernel
set_option autoImplicit false
set_option maxHeartbeats 2000000
set_option synthInstance.maxHeartbeats 200000
set_option backward.isDefEq.respectTransparency false
set_option backward.isDefEq.respectTransparency.types false
open Complex ConnesRZ ConnesRZFrontier ConnesGreen WeilDefect WeilDefect.ConnesNative
open scoped BigOperators InnerProductSpace lp ENNReal Classical ComplexOrder Topology
noncomputable section
namespace ConnesGreen
/-- Auxiliary finite synthesis of the ORIGINAL positive F columns on the
ORIGINAL physical carrier. The full positive actor remains unchanged. -/
def canonicalFinitePositiveSynthesis (t : ℝ) (F : Finset CriticalZeros) :
ℓ²({ρ : CriticalZeros // ρ ∈ F}, ℂ) →L[ℂ] Physical t :=
columnSynthesis
(fun ρ => positiveGreenColumn (fun τ => sourceEmbed t (actualGreenSource τ)) ρ.1)
(by exact Summable.of_finite)
/-- Exact finite correction on the ORIGINAL selected negative coefficient space.
Only the positive coefficient covariance is inverted, with positive δI. -/
def canonicalFiniteSelectedCorrection (t : ℝ) (ht : 0 < t)
(S F : Finset CriticalZeros) (δ : ℝ) :
ℓ²({ρ : CriticalZeros // ρ ∈ S}, ℂ) →L[ℂ] ℓ²({ρ : CriticalZeros // ρ ∈ S}, ℂ) :=
let P := canonicalFinitePositiveSynthesis t F
let N := canonicalSelectedSynthesis t ht S
δ • 1 - N.adjoint ∘L N + (P.adjoint ∘L N).adjoint ∘L
Ring.inverse (P.adjoint ∘L P + δ • 1) ∘L (P.adjoint ∘L N)
end ConnesGreen
Source
monocap-tech/weil, WeilDefect/Connes/FiniteSelectedCertificates.lean at d28908eb3d61a4a81d7b4a5aff70ea26b6680897
Literature/source audit addendum (2026-10-11; COR-19): Exact native software custody, independently verified from retained local Git objects: monocap-tech/weil d28908eb3d61a4a81d7b4a5aff70ea26b6680897, WeilDefect/Connes/FiniteSelectedCertificates.lean, SHA256 c2672521233eea07694186624f6ad1d7dc1f1586ac426b7a9784a6d96a52f1c8. Public availability of these historical pins has not been checked; this addendum verifies local source bytes and preserves the original source ancestry. The unchanged graph RHS values were checked against native definitions by Lean rfl. This is source/value custody, not an assertion that contextual literature supplies the whole definition bundle.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.