Complete primitive sum at one residual R-324 head

Paper §4.2 Step 3 applies Proposition 4.1 to the complete primitive-pairing sum carried by the current cross block. This file keeps that finite sum inside one head update. In particular, it does not apply the proposition term by term and introduces no pairing-cardinality loss.

The complete signed head sum

noncomputable def Anderson4D.R324NestedCrossStepContext.completeCrossGapPrimitiveIntegrand {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (ε : ℝ) (G : Fin (2 * ctx.order - 1) → T4 → ℝ) (x : Fin (2 * ctx.order) → T4) : ℝ

The moving central-gap numerator multiplying the complete primitive pairing sum at the current head. The sum is retained before any norm or Proposition 4.1 estimate is taken.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Anderson4D.R324NestedCrossStepContext.completeCrossGapPrimitiveTerm {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (G : Fin (2 * ctx.order - 1) → T4 → ℝ) (z w : T4) : ℝ

The complete current-head contribution, with the exact coupling power. This is one finite primitive sum, not a sum of separately estimated Proposition 4.1 majorants.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.R324NestedCrossStepContext.completeCrossGapPrimitiveIntegrand_eq {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (ε : ℝ) (G : Fin (2 * ctx.order - 1) → T4 → ℝ) (x : Fin (2 * ctx.order) → T4) : ctx.completeCrossGapPrimitiveIntegrand ρ ε G x = torusDistSq (x ctx.leftGapIndex - x ctx.rightGapIndex) * primitiveChainProduct ctx.order ⋯ G x * ∑ κ ∈ primitiveFullPairings ctx.order, primitiveCovarianceProduct ρ ε ctx.order κ x

Algebraic normal form exposing one complete covariance sum.

Transport of the actual residual block factor

theorem Anderson4D.R324NestedCrossStepContext.r324PrimitivePartitionBlockSum_head_reconstruct_split {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (ε : ℝ) (t : Fin (2 * ctx.order) → T4) (v : ctx.PostCoordinate → T4) : r324PrimitivePartitionBlockSum ρ ε κp κm π ctx.head.carrier (ctx.reconstruct (ctx.splitSurvivingPiMeasurableEquiv.symm (t, v))) = ∑ σ : R324PrimitiveCoordinate ctx.order, primitiveCovarianceProduct ρ ε ctx.order (↑σ) t

The complete physical block sum on the literal current residual head, after the proved head/post coordinate split, is exactly the complete primitive covariance sum on canonical head coordinates.

theorem Anderson4D.R324NestedCrossStepContext.sum_r324PrimitiveCoordinate_covariance_eq {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (ε : ℝ) (t : Fin (2 * ctx.order) → T4) : ∑ σ : R324PrimitiveCoordinate ctx.order, primitiveCovarianceProduct ρ ε ctx.order (↑σ) t = ∑ κ ∈ primitiveFullPairings ctx.order, primitiveCovarianceProduct ρ ε ctx.order κ t

Fintype coordinates and the paper's filtered primitive-pairing sum are the same complete finite family.

theorem Anderson4D.R324NestedCrossStepContext.headGapChainBlockSum_eq_completeCrossGapPrimitiveIntegrand {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (ε : ℝ) (G : Fin (2 * ctx.order - 1) → T4 → ℝ) (t : Fin (2 * ctx.order) → T4) (v : ctx.PostCoordinate → T4) : torusDistSq (t ctx.leftGapIndex - t ctx.rightGapIndex) * primitiveChainProduct ctx.order ⋯ G t * r324PrimitivePartitionBlockSum ρ ε κp κm π ctx.head.carrier (ctx.reconstruct (ctx.splitSurvivingPiMeasurableEquiv.symm (t, v))) = ctx.completeCrossGapPrimitiveIntegrand ρ ε G t

Direct exact bridge from the literal physical head factor to the complete central-gap primitive integrand.

One application of the complete inserted kernel

theorem Anderson4D.R324NestedCrossStepContext.completeCrossGapPrimitiveIntegrand_le_insertedSum {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (ε : ℝ) (G : Fin (2 * ctx.order - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * ctx.order - 1)) (z : T4), 0 ≤ G j z) (x : Fin (2 * ctx.order) → T4) : ctx.completeCrossGapPrimitiveIntegrand ρ ε G x ≤ ∑ κ ∈ primitiveFullPairings ctx.order, primitiveInsertedIntegrand ρ ε ctx.order ⋯ G κ x

Pointwise, the complete moving-gap sum is bounded by the complete inserted primitive sum. No primitive-pairing term is estimated individually by Proposition 4.1.

The following two lemmas provide integrability uniformly over the complete primitive family. They are deliberately parameterized by membership rather than by ctx.blockPairing.

theorem Anderson4D.R324NestedCrossStepContext.integrable_primitiveIntegrand_blockAssemble_of_mem {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (G : Fin (2 * ctx.order - 1) → T4 → ℝ) (hGmeas : ∀ (j : Fin (2 * ctx.order - 1)), Measurable (G j)) (hinput : IsAdmissiblePrimitiveInput ctx.order G) (κ : PartialPairing (Fin (2 * ctx.order))) (hκ : κ ∈ primitiveFullPairings ctx.order) (z w : T4) : MeasureTheory.Integrable (fun (v : Fin (2 * ctx.order - 2) → T4) => primitiveIntegrand ρ ε ctx.order ⋯ G κ (primitiveAssemble ctx.order ⋯ z w v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.order - 2)) => paperMeasure)

theorem Anderson4D.R324NestedCrossStepContext.integrable_primitiveInsertedIntegrand_blockAssemble_of_mem {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (G : Fin (2 * ctx.order - 1) → T4 → ℝ) (hGmeas : ∀ (j : Fin (2 * ctx.order - 1)), Measurable (G j)) (hinput : IsAdmissiblePrimitiveInput ctx.order G) (κ : PartialPairing (Fin (2 * ctx.order))) (hκ : κ ∈ primitiveFullPairings ctx.order) (z w : T4) : MeasureTheory.Integrable (fun (v : Fin (2 * ctx.order - 2) → T4) => primitiveInsertedIntegrand ρ ε ctx.order ⋯ G κ (primitiveAssemble ctx.order ⋯ z w v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.order - 2)) => paperMeasure)

theorem Anderson4D.R324NestedCrossStepContext.integrable_completeCrossGapSummand_blockAssemble_of_mem {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (G : Fin (2 * ctx.order - 1) → T4 → ℝ) (hGmeas : ∀ (j : Fin (2 * ctx.order - 1)), Measurable (G j)) (hinput : IsAdmissiblePrimitiveInput ctx.order G) (κ : PartialPairing (Fin (2 * ctx.order))) (hκ : κ ∈ primitiveFullPairings ctx.order) (z w : T4) : MeasureTheory.Integrable (fun (v : Fin (2 * ctx.order - 2) → T4) => torusDistSq (primitiveAssemble ctx.order ⋯ z w v ctx.leftGapIndex - primitiveAssemble ctx.order ⋯ z w v ctx.rightGapIndex) * primitiveIntegrand ρ ε ctx.order ⋯ G κ (primitiveAssemble ctx.order ⋯ z w v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.order - 2)) => paperMeasure)

theorem Anderson4D.R324NestedCrossStepContext.completeCrossGapPrimitiveTerm_eq_integral {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (G : Fin (2 * ctx.order - 1) → T4 → ℝ) (hGmeas : ∀ (j : Fin (2 * ctx.order - 1)), Measurable (G j)) (hinput : IsAdmissiblePrimitiveInput ctx.order G) (z w : T4) : ctx.completeCrossGapPrimitiveTerm ρ lam ε G z w = lamEps lam ε ^ (2 * ctx.order) * ∫ (v : Fin (2 * ctx.order - 2) → T4), ctx.completeCrossGapPrimitiveIntegrand ρ ε G (primitiveAssemble ctx.order ⋯ z w v) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.order - 2)) => paperMeasure

The sum-of-integrals presentation of the complete term is exactly the integral of the complete pointwise primitive sum.

theorem Anderson4D.R324NestedCrossStepContext.completeCrossGapPrimitiveTerm_le_primitiveKernelInserted {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (G : Fin (2 * ctx.order - 1) → T4 → ℝ) (hGmeas : ∀ (j : Fin (2 * ctx.order - 1)), Measurable (G j)) (hinput : IsAdmissiblePrimitiveInput ctx.order G) (hG : ∀ (j : Fin (2 * ctx.order - 1)) (z : T4), 0 ≤ G j z) (z w : T4) : ctx.completeCrossGapPrimitiveTerm ρ lam ε G z w ≤ primitiveKernelInserted ρ lam ε ctx.order ⋯ G z w

The complete moving-gap head is bounded by a single complete inserted kernel. This is the precise bridge needed before invoking Proposition 4.1; there is no factor counting primitive pairings.