Actual Weighted Column Remainder

Abstract

SOURCE_ONLY_UNCOMPILED: faithful author statements; no validated provenance claim.

The actual weighted first-jet error and infinite paired remainder are owned here. All Lean proofs, Reg selections and Scribe emission await caller-owned verification.

Definition 1.1 (The actual weighted absolute head moment).

$$W(S,v)=\mathrm{SumAbsIndexTimesCoefficientNorm}(S,v)$$

Formalization. D5/S3/Weil/ZetaBridge/ActualColumnRemainder.weightedHeadMass (✓ std3).

Source. Repository-derived.

Commentary.

SOURCE_ONLY_UNCOMPILED. W(S,v)=sum_{n in S} abs(n)*norm(v(n)). S is any finite integer set and v has arbitrary complex values; the n=0 contribution is exactly zero. W is never replaced by A times the unweighted mass.

Definition 1.2 (The exact paired weighted remainder budget).

$$R(c,N,A,S,v)=\mathrm{div}(\mathrm{mul}(8,\mathrm{square}(\mathrm{arithmeticBoundaryBudget}(c)),\mathrm{square}(W(S,v)),\mathrm{square}(\mathrm{add}(N,1))),\mathrm{mul}(3,\mathrm{square}(pi),\mathrm{cube}(N),\mathrm{square}(\mathrm{sub}(\mathrm{add}(N,1),A))))$$

Formalization. D5/S3/Weil/ZetaBridge/ActualColumnRemainder.pairedRemainderBudget (✓ std3).

Source. Repository-derived.

Commentary.

SOURCE_ONLY_UNCOMPILED. R=8arithmeticBoundaryBudget(c)^2W(S,v)^2*(M+1)^2/(3pi^2M^3*(M+1-A)^2). Its admitted domain is c>=2, natural M>0, real A>=0, abs(n)<=A for every n in S, and A<M+1. No stronger separation such as M>=2A is used.

Theorem 1.3 (Weighted error of the actual divided-difference column).

$$\mathrm{And}(\mathrm{AtLeastTwo}(c),\mathrm{Nonnegative}(A),\mathrm{HeadWithin}(S,A),\mathrm{Less}(A,\mathrm{abs}(m)))\Rightarrow \mathrm{LessEqual}(\mathrm{norm}(\mathrm{ColumnMinusJet}(c,S,v,m)),\mathrm{div}(\mathrm{mul}(2,\mathrm{arithmeticBoundaryBudget}(c),W(S,v)),\mathrm{mul}(pi,\mathrm{abs}(m),\mathrm{sub}(\mathrm{abs}(m),A))))$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaBridge/ActualColumnRemainder.weighted_coupling_first_jet_error (✓ std3). ∎

Source. Repository-derived.

Commentary.

SOURCE_ONLY_UNCOMPILED. For c>=2, every finite S subset Z, arbitrary v:Z->C, A>=0, abs(n)<=A on S, and integer m with A<abs(m), norm(couplingColumn(c,S,v,m)-couplingFirstJet(c,S,v,m))<=2arithmeticBoundaryBudget(c)W(S,v)/(piabs(m)(abs(m)-A)). The proof consumes arithmetic_coupling_first_jet_error at each singleton with radius abs(n), including n=0, compares the positive denominators, and sums the actual differences. It imposes no reality or moment-vanishing premise.

Theorem 1.4 (Infinite paired first-jet remainder with cubic cutoff decay).

$$\mathrm{And}(\mathrm{AtLeastTwo}(c),\mathrm{Positive}(N),\mathrm{Nonnegative}(A),\mathrm{HeadWithin}(S,A),\mathrm{Less}(A,\mathrm{add}(N,1)))\Rightarrow \mathrm{And}(\mathrm{Summable}(\mathrm{PairedRemainderSequence}(c,N,S,v)),\mathrm{LessEqual}(\mathrm{PairedRemainderTsum}(c,N,S,v),R(c,N,A,S,v)))$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaBridge/ActualColumnRemainder.paired_first_jet_remainder_tail (✓ std3). ∎

Source. Repository-derived.

Commentary.

SOURCE_ONLY_UNCOMPILED. For every c>=2, natural M>0, real A>=0 with A<M+1 and abs(n)<=A on any finite integer S, and every complex coefficient function v, the sequence norm(Column(m)-Jet(m))^2+norm(Column(-m)-Jet(-m))^2, m=M+j+1, is summable and its genuine tsum is at most R. For t>=M+1, t/(t-A)<=(M+1)/(M+1-A); the one-sign square is bounded by C^2/t^4 with C=2BW*(M+1)/(pi*(M+1-A)). The consumed exact owner inverse-fourth partial tail yields 2C^2/(3M^3)=R. Both signs and the zero/empty head remain. For fixed head, c and A this budget has cubic cutoff decay. No finite terminal exterior cutoff is asserted.

References

• Truth anchor: D5/S3/Weil/ZetaBridge/ActualColumnRemainder.pairedRemainderBudget
• Truth anchor: D5/S3/Weil/ZetaBridge/ActualColumnRemainder.paired_first_jet_remainder_tail
• Truth anchor: D5/S3/Weil/ZetaBridge/ActualColumnRemainder.weightedHeadMass
• Truth anchor: D5/S3/Weil/ZetaBridge/ActualColumnRemainder.weighted_coupling_first_jet_error
• Dependency: D5/S3/Weil/ZetaBridge/WeilArithmeticCouplingJet
• Dependency: D5/S3/Weil/ZetaBridge/WeilEvenFourierObservationTail