Exact and quantitative nested cross steps for R-324

Paper §4.2 Step 3 removes the surviving cross-cut primitive blocks from inside to outside. This file attaches all data used by one such removal to the same proof-relevant head context:

• the literal residual prefix and its next suffix;
• the canonical increasing reindexing of the current sparse block;
• the two indices carrying the moving central-gap numerator in (4.20);
• a measure-preserving split of the current surviving coordinates into the current block and the next suffix;
• the exact central-gap primitive term and its domination by the inserted Proposition 4.1 term; and
• the exact perturbative-order and numerical scale ledgers after the head is removed.

The endpoint routing of paper Step 4 is deliberately not folded into this state. Its direct and shortcut branches have different terminal majorants.

One literal nonterminal/terminal cross head

structure Anderson4D.R324NestedCrossStepContext {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : Type

All structural data of one literal head in the nested cross schedule.

• residual : R324NestedCrossResidualPrefix κp κm π
• head : R324NestedCrossBlock κp κm π
• tail : List (R324NestedCrossBlock κp κm π)
• remaining_eq : self.residual.remaining = self.head :: self.tail

def Anderson4D.R324NestedCrossStepContext.next {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : R324NestedCrossResidualPrefix κp κm π

The literal suffix after deleting the current inside-most head.

Equations

• ctx.next = ctx.residual.afterHead ctx.head ctx.tail ⋯

def Anderson4D.R324NestedCrossStepContext.order {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : ℕ

The exact perturbative order of the current sparse block.

Equations

• ctx.order = Anderson4D.residualBlockOrder ctx.head.carrier

theorem Anderson4D.R324NestedCrossStepContext.one_le_order {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : 1 ≤ ctx.order

theorem Anderson4D.R324NestedCrossStepContext.collapseMem {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : ctx.head.carrier ∈ momentResidualCollapseBlocks κp κm π

Membership of the current head in the original, possibly-empty block schedule.

theorem Anderson4D.R324NestedCrossStepContext.fullyPaired {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : IsFullyPairedOn (momentCombinedPairing κp κm π) ctx.head.carrier

Closure of the current head under the combined moment pairing.

theorem Anderson4D.R324NestedCrossStepContext.relativelyPrimitive {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : IsRelPrimitiveOn (momentCombinedPairing κp κm π) ctx.head.carrier

Relative primitivity of the current head.

def Anderson4D.R324NestedCrossStepContext.blockOrderIso {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : Fin (2 * ctx.order) ≃o ↥ctx.head.carrier

Canonical increasing coordinates on the current sparse head.

Equations

• ctx.blockOrderIso = Anderson4D.residualPrimitiveBlockOrderIso (Anderson4D.momentCombinedPairing κp κm π) ctx.head.carrier ⋯

def Anderson4D.R324NestedCrossStepContext.blockPairing {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : PartialPairing (Fin (2 * ctx.order))

Canonical primitive full pairing transported to standard block coordinates.

Equations

• ctx.blockPairing = Anderson4D.residualPrimitiveBlockPairing (Anderson4D.momentCombinedPairing κp κm π) ctx.head.carrier ⋯

theorem Anderson4D.R324NestedCrossStepContext.blockPairing_mem {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : ctx.blockPairing ∈ primitiveFullPairings ctx.order

def Anderson4D.R324NestedCrossStepContext.leftGapIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : Fin (2 * ctx.order)

Standard block index of the last current left coordinate.

Equations

• ctx.leftGapIndex = ctx.blockOrderIso.symm ⟨ctx.head.leftGap, ⋯⟩

def Anderson4D.R324NestedCrossStepContext.rightGapIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : Fin (2 * ctx.order)

Standard block index of the first current right coordinate.

Equations

• ctx.rightGapIndex = ctx.blockOrderIso.symm ⟨ctx.head.rightGap, ⋯⟩

theorem Anderson4D.R324NestedCrossStepContext.blockOrderIso_leftGapIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : ctx.blockOrderIso ctx.leftGapIndex = ⟨ctx.head.leftGap, ⋯⟩

theorem Anderson4D.R324NestedCrossStepContext.blockOrderIso_rightGapIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : ctx.blockOrderIso ctx.rightGapIndex = ⟨ctx.head.rightGap, ⋯⟩

theorem Anderson4D.R324NestedCrossStepContext.leftGapIndex_lt_rightGapIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : ctx.leftGapIndex < ctx.rightGapIndex

theorem Anderson4D.R324NestedCrossStepContext.leftGapIndex_ne_rightGapIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : ctx.leftGapIndex ≠ ctx.rightGapIndex

Exact coordinate split and Fubini

def Anderson4D.R324NestedCrossStepContext.SurvivingCoordinate {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : Type

Coordinates still present at the current cross prefix.

Equations

• ctx.SurvivingCoordinate = ↥ctx.residual.activeCarrier

@[implicit_reducible]

noncomputable instance Anderson4D.R324NestedCrossStepContext.survivingCoordinateFintype {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : Fintype ctx.SurvivingCoordinate

Equations

• ctx.survivingCoordinateFintype = inferInstance

def Anderson4D.R324NestedCrossStepContext.PostCoordinate {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : Type

Coordinates still present after the current head is deleted.

Equations

• ctx.PostCoordinate = ↥ctx.next.activeCarrier

@[implicit_reducible]

noncomputable instance Anderson4D.R324NestedCrossStepContext.postCoordinateFintype {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : Fintype ctx.PostCoordinate

Equations

• ctx.postCoordinateFintype = inferInstance

theorem Anderson4D.R324NestedCrossStepContext.head_subset_activeCarrier {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : ctx.head.carrier ⊆ ctx.residual.activeCarrier

@[reducible, inline]

abbrev Anderson4D.R324NestedCrossStepContext.HeadCoordinate {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : Type

Ambiently labelled coordinates of the current head.

Equations

• ctx.HeadCoordinate = { i : ctx.SurvivingCoordinate // ↑i ∈ ctx.head.carrier }

@[reducible, inline]

abbrev Anderson4D.R324NestedCrossStepContext.OuterCoordinate {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : Type

Coordinates outside the current head.

Equations

• ctx.OuterCoordinate = { i : ctx.SurvivingCoordinate // ↑i ∉ ctx.head.carrier }

def Anderson4D.R324NestedCrossStepContext.headCoordinateEquivStandard {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : ctx.HeadCoordinate ≃ Fin (2 * ctx.order)

The ambiently labelled head is exactly the canonical standard primitive coordinate type.

Equations

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

def Anderson4D.R324NestedCrossStepContext.outerCoordinateEquivPost {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : ctx.OuterCoordinate ≃ ctx.PostCoordinate

The complement of the current head is exactly the next suffix carrier.

Equations

• ctx.outerCoordinateEquivPost = { toFun := fun (i : ctx.OuterCoordinate) => ⟨↑↑i, ⋯⟩, invFun := fun (i : ctx.PostCoordinate) => ⟨⟨↑i, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

def Anderson4D.R324NestedCrossStepContext.survivingCoordinateEquivHeadSumPost {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : ctx.SurvivingCoordinate ≃ Fin (2 * ctx.order) ⊕ ctx.PostCoordinate

Exact partition of the current carrier into the standard current block and the next literal suffix.

Equations

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

noncomputable def Anderson4D.R324NestedCrossStepContext.splitSurvivingPiMeasurableEquiv {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : (ctx.SurvivingCoordinate → T4) ≃ᵐ (Fin (2 * ctx.order) → T4) × (ctx.PostCoordinate → T4)

The measure-theoretic coordinate split used by the Step 3 Fubini iteration.

Equations

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

def Anderson4D.R324NestedCrossStepContext.headSurvivingCoordinate {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (j : Fin (2 * ctx.order)) : ctx.SurvivingCoordinate

The current surviving coordinate corresponding to a standard head coordinate.

Equations

• ctx.headSurvivingCoordinate j = ⟨↑(ctx.blockOrderIso j), ⋯⟩

def Anderson4D.R324NestedCrossStepContext.postSurvivingCoordinate {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (i : ctx.PostCoordinate) : ctx.SurvivingCoordinate

A next-suffix coordinate regarded as a current surviving coordinate.

Equations

• ctx.postSurvivingCoordinate i = ⟨↑i, ⋯⟩

@[simp]

theorem Anderson4D.R324NestedCrossStepContext.splitSurvivingPiMeasurableEquiv_apply_fst {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (v : ctx.SurvivingCoordinate → T4) (j : Fin (2 * ctx.order)) : (ctx.splitSurvivingPiMeasurableEquiv v).1 j = v (ctx.headSurvivingCoordinate j)

@[simp]

theorem Anderson4D.R324NestedCrossStepContext.splitSurvivingPiMeasurableEquiv_apply_snd {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (v : ctx.SurvivingCoordinate → T4) (i : ctx.PostCoordinate) : (ctx.splitSurvivingPiMeasurableEquiv v).2 i = v (ctx.postSurvivingCoordinate i)

@[simp]

theorem Anderson4D.R324NestedCrossStepContext.splitSurvivingPiMeasurableEquiv_symm_head {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (t : Fin (2 * ctx.order) → T4) (v : ctx.PostCoordinate → T4) (j : Fin (2 * ctx.order)) : ctx.splitSurvivingPiMeasurableEquiv.symm (t, v) (ctx.headSurvivingCoordinate j) = t j

@[simp]

theorem Anderson4D.R324NestedCrossStepContext.splitSurvivingPiMeasurableEquiv_symm_post {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (t : Fin (2 * ctx.order) → T4) (v : ctx.PostCoordinate → T4) (i : ctx.PostCoordinate) : ctx.splitSurvivingPiMeasurableEquiv.symm (t, v) (ctx.postSurvivingCoordinate i) = v i

noncomputable def Anderson4D.R324NestedCrossStepContext.reconstruct {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (v : ctx.SurvivingCoordinate → T4) : Fin (2 * m) → T4

Reconstruct an ambient doubled tuple from exactly the current surviving coordinates. Coordinates outside the current residual carrier are set to zero.

Equations

• ctx.reconstruct v i = if hi : i ∈ ctx.residual.activeCarrier then v ⟨i, hi⟩ else 0

@[simp]

theorem Anderson4D.R324NestedCrossStepContext.reconstruct_surviving {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (v : ctx.SurvivingCoordinate → T4) (i : ctx.SurvivingCoordinate) : ctx.reconstruct v ↑i = v i

@[simp]

theorem Anderson4D.R324NestedCrossStepContext.reconstruct_split_symm_block {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (t : Fin (2 * ctx.order) → T4) (v : ctx.PostCoordinate → T4) (j : Fin (2 * ctx.order)) : ctx.reconstruct (ctx.splitSurvivingPiMeasurableEquiv.symm (t, v)) ↑(ctx.blockOrderIso j) = t j

theorem Anderson4D.R324NestedCrossStepContext.centralGapNumerator_reconstruct_split {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (t : Fin (2 * ctx.order) → T4) (v : ctx.PostCoordinate → T4) : ctx.head.centralGapNumerator (ctx.reconstruct (ctx.splitSurvivingPiMeasurableEquiv.symm (t, v))) = torusDistSq (t ctx.leftGapIndex - t ctx.rightGapIndex)

Under the exact Fubini split, the physical (4.20) numerator is literally the gap between the two canonical standard block indices.

theorem Anderson4D.R324NestedCrossStepContext.measurePreserving_splitSurvivingPiMeasurableEquiv {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : MeasureTheory.MeasurePreserving (⇑ctx.splitSurvivingPiMeasurableEquiv) (MeasureTheory.Measure.pi fun (x : ctx.SurvivingCoordinate) => paperMeasure) ((MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.order)) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : ctx.PostCoordinate) => paperMeasure))

The exact cross-head coordinate split preserves the paper product Haar measure.

theorem Anderson4D.R324NestedCrossStepContext.integral_splitSurviving_post_first {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : (ctx.SurvivingCoordinate → T4) → E) (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.pi fun (x : ctx.SurvivingCoordinate) => paperMeasure)) : (∫ (w : ctx.SurvivingCoordinate → T4), f w ∂MeasureTheory.Measure.pi fun (x : ctx.SurvivingCoordinate) => paperMeasure) = ∫ (v : ctx.PostCoordinate → T4), ∫ (t : Fin (2 * ctx.order) → T4), f (ctx.splitSurvivingPiMeasurableEquiv.symm (t, v)) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.order)) => paperMeasure ∂MeasureTheory.Measure.pi fun (x : ctx.PostCoordinate) => paperMeasure

Genuine Fubini with the current cross head on the inside and the next literal suffix on the outside.

The exact inserted cross-gap primitive term

noncomputable def Anderson4D.R324NestedCrossStepContext.crossGapPrimitiveIntegrand {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 (4.20) numerator multiplying the genuine primitive integrand on the canonical standard head coordinates.

Equations

• ctx.crossGapPrimitiveIntegrand ρ ε G x = Anderson4D.torusDistSq (x ctx.leftGapIndex - x ctx.rightGapIndex) * Anderson4D.primitiveIntegrand ρ ε ctx.order ⋯ G ctx.blockPairing x

noncomputable def Anderson4D.R324NestedCrossStepContext.crossGapPrimitiveTerm {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) : ℝ

One concrete central-gap pairing term, including the exact coupling power. The two outermost standard block coordinates are held at z,w.

Equations

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

theorem Anderson4D.R324NestedCrossStepContext.crossGapPrimitiveIntegrand_nonneg {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) : 0 ≤ ctx.crossGapPrimitiveIntegrand ρ ε G x

theorem Anderson4D.R324NestedCrossStepContext.crossGapPrimitiveIntegrand_le_inserted {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.crossGapPrimitiveIntegrand ρ ε G x ≤ primitiveInsertedIntegrand ρ ε ctx.order ⋯ G ctx.blockPairing x

The actual moving gap is no larger than the diameter insertion in Proposition 4.1.

theorem Anderson4D.R324NestedCrossStepContext.measurable_r324TorusTupleDiameterSq {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [Fintype ι] [Nonempty ι] (x : Ω → ι → T4) (hx : ∀ (i : ι), Measurable fun (ω : Ω) => x ω i) : Measurable fun (ω : Ω) => torusTupleDiameterSq (x ω)

Finite tuple diameter is measurable whenever all tuple coordinates are measurable.

theorem Anderson4D.R324NestedCrossStepContext.r324TorusTupleDiameterSq_le_four_pi_sq {ι : Type u_1} [Fintype ι] [Nonempty ι] (x : ι → T4) : torusTupleDiameterSq x ≤ 4 * Real.pi ^ 2

Uniform compact-torus bound for every finite tuple diameter.

theorem Anderson4D.R324NestedCrossStepContext.integrable_primitiveIntegrand_blockAssemble {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) (z w : T4) : MeasureTheory.Integrable (fun (v : Fin (2 * ctx.order - 2) → T4) => primitiveIntegrand ρ ε ctx.order ⋯ G ctx.blockPairing (primitiveAssemble ctx.order ⋯ z w v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.order - 2)) => paperMeasure)

Absolute integrability of the ordinary canonical head summand follows from the proved R-51 estimate (with the zero-dimensional order-one case handled separately).

theorem Anderson4D.R324NestedCrossStepContext.integrable_primitiveInsertedIntegrand_blockAssemble {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) (z w : T4) : MeasureTheory.Integrable (fun (v : Fin (2 * ctx.order - 2) → T4) => primitiveInsertedIntegrand ρ ε ctx.order ⋯ G ctx.blockPairing (primitiveAssemble ctx.order ⋯ z w v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.order - 2)) => paperMeasure)

Absolute integrability of the inserted canonical head summand is derived, rather than assumed: the tuple diameter is a bounded measurable multiplier of the ordinary R-51 summand.

theorem Anderson4D.R324NestedCrossStepContext.integrable_crossGapPrimitiveIntegrand_blockAssemble {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) (z w : T4) : MeasureTheory.Integrable (fun (v : Fin (2 * ctx.order - 2) → T4) => ctx.crossGapPrimitiveIntegrand ρ ε G (primitiveAssemble ctx.order ⋯ z w v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.order - 2)) => paperMeasure)

Absolute integrability of the exact central-gap summand follows from the same ordinary R-51 summand and the uniform torus-distance bound.

theorem Anderson4D.R324NestedCrossStepContext.crossGapPrimitiveTerm_nonneg {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (G : Fin (2 * ctx.order - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * ctx.order - 1)) (z : T4), 0 ≤ G j z) (z w : T4) : 0 ≤ ctx.crossGapPrimitiveTerm ρ lam ε G z w

The exact cross-gap term is nonnegative for the nonnegative dominating edge family used after Step 2 takes absolute values.

theorem Anderson4D.R324NestedCrossStepContext.crossGapPrimitiveTerm_le_insertedTerm {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.crossGapPrimitiveTerm ρ lam ε G z w ≤ primitivePairingKernelInsertedTerm ρ lam ε ctx.order ⋯ G ctx.blockPairing z w

Quantitative one-head comparison: the exact moving-gap term is bounded by the actual inserted pairing term used by Proposition 4.1.

Exact heterogeneous scale extraction

theorem Anderson4D.R324NestedCrossStepContext.crossGapPrimitiveIntegrand_family_mul {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (ε : ℝ) (A : Fin (2 * ctx.order - 1) → ℝ) (G : Fin (2 * ctx.order - 1) → T4 → ℝ) (x : Fin (2 * ctx.order) → T4) : ctx.crossGapPrimitiveIntegrand ρ ε (fun (j : Fin (2 * ctx.order - 1)) (u : T4) => A j * G j u) x = (∏ j : Fin (2 * ctx.order - 1), A j) * ctx.crossGapPrimitiveIntegrand ρ ε G x

Scaling every current chain edge extracts exactly the product of the named scales from the cross-gap integrand.

theorem Anderson4D.R324NestedCrossStepContext.crossGapPrimitiveTerm_family_mul {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (A : Fin (2 * ctx.order - 1) → ℝ) (G : Fin (2 * ctx.order - 1) → T4 → ℝ) (z w : T4) : ctx.crossGapPrimitiveTerm ρ lam ε (fun (j : Fin (2 * ctx.order - 1)) (u : T4) => A j * G j u) z w = (∏ j : Fin (2 * ctx.order - 1), A j) * ctx.crossGapPrimitiveTerm ρ lam ε G z w

Exact term-level scale ledger for one actual cross head.

theorem Anderson4D.R324NestedCrossStepContext.edgeScaleProduct_nonneg {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (A : Fin (2 * ctx.order - 1) → ℝ) (hA : ∀ (j : Fin (2 * ctx.order - 1)), 0 ≤ A j) : 0 ≤ ∏ j : Fin (2 * ctx.order - 1), A j

The product of nonnegative current edge scales is nonnegative.

Proposition 4.1 on every literal nested cross head

theorem Anderson4D.R324NestedCrossStepContext.exists_r324NestedCross_headTerm_le_majorant (ρ : SmoothCutoff) : ∃ (orderConstant : ℝ) (supportConstant : ℝ) (C : ℝ), 0 < orderConstant ∧ 0 < supportConstant ∧ 0 < C ∧ ∀ {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (ctx : R324NestedCrossStepContext κp κm π) (lam ε : ℝ) (G : Fin (2 * ctx.order - 1) → T4 → ℝ), PrimitiveEstimateRegime ctx.order lam ε orderConstant supportConstant C → (∀ (j : Fin (2 * ctx.order - 1)), Measurable (G j)) → IsAdmissiblePrimitiveInput ctx.order G → (∀ (j : Fin (2 * ctx.order - 1)) (z : T4), 0 ≤ G j z) → ∀ (z : T4), 0 ≤ ctx.crossGapPrimitiveTerm ρ lam ε G z 0 ∧ ctx.crossGapPrimitiveTerm ρ lam ε G z 0 ≤ primitiveInsertedMajorant C lam ε supportConstant ctx.order z

The constants from the proved Proposition 4.1 control the exact moving central-gap term for every literal cross head. The comparison is proved through the genuine inserted pairing term; neither the desired R-324 density bound nor a target-shaped reduction interface is assumed.

theorem Anderson4D.R324NestedCrossStepContext.exists_r324NestedCross_scaledHeadTerm_le_majorant (ρ : SmoothCutoff) : ∃ (orderConstant : ℝ) (supportConstant : ℝ) (C : ℝ), 0 < orderConstant ∧ 0 < supportConstant ∧ 0 < C ∧ ∀ {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (ctx : R324NestedCrossStepContext κp κm π) (lam ε : ℝ) (A : Fin (2 * ctx.order - 1) → ℝ) (G : Fin (2 * ctx.order - 1) → T4 → ℝ), PrimitiveEstimateRegime ctx.order lam ε orderConstant supportConstant C → (∀ (j : Fin (2 * ctx.order - 1)), 0 ≤ A j) → (∀ (j : Fin (2 * ctx.order - 1)), Measurable (G j)) → IsAdmissiblePrimitiveInput ctx.order G → (∀ (j : Fin (2 * ctx.order - 1)) (z : T4), 0 ≤ G j z) → ∀ (z : T4), ctx.crossGapPrimitiveTerm ρ lam ε (fun (j : Fin (2 * ctx.order - 1)) (u : T4) => A j * G j u) z 0 ≤ (∏ j : Fin (2 * ctx.order - 1), A j) * primitiveInsertedMajorant C lam ε supportConstant ctx.order z

Heterogeneous nonnegative edge scales are charged exactly once, as their product, in the quantitative one-head update.

Prefix and suffix budget recurrences

theorem Anderson4D.R324NestedCrossStepContext.next_processedOrder {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : ctx.next.processedOrder = ctx.residual.processedOrder + ctx.order

theorem Anderson4D.R324NestedCrossStepContext.next_processed_length {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : ctx.next.processed.length = ctx.residual.processed.length + 1

theorem Anderson4D.R324NestedCrossStepContext.remainingOrder_eq_order_add_next {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : ctx.residual.remainingOrder = ctx.order + ctx.next.remainingOrder

theorem Anderson4D.R324NestedCrossStepContext.remaining_eq_head_cons {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) : ctx.residual.remaining = ctx.head :: ctx.next.remaining

def Anderson4D.R324NestedCrossStepContext.processedBudget {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (res : R324NestedCrossResidualPrefix κp κm π) (C lam K : ℝ) : ℝ

Numerical budget accumulated by the already processed cross prefix. K is the uniform integration cost of one completed cross head.

Equations

• Anderson4D.R324NestedCrossStepContext.processedBudget res C lam K = (C * lam) ^ (2 * res.processedOrder) * K ^ res.processed.length

def Anderson4D.R324NestedCrossStepContext.remainingBudget {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (res : R324NestedCrossResidualPrefix κp κm π) (C lam K : ℝ) : ℝ

Numerical budget still carried by the literal remaining suffix.

Equations

• Anderson4D.R324NestedCrossStepContext.remainingBudget res C lam K = (C * lam) ^ (2 * res.remainingOrder) * K ^ res.remaining.length

theorem Anderson4D.R324NestedCrossStepContext.processedBudget_next {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (C lam K : ℝ) : processedBudget ctx.next C lam K = processedBudget ctx.residual C lam K * ((C * lam) ^ (2 * ctx.order) * K)

Exact forward update of the accumulated budget after deleting one literal head.

theorem Anderson4D.R324NestedCrossStepContext.remainingBudget_eq_head_mul_next {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (C lam K : ℝ) : remainingBudget ctx.residual C lam K = (C * lam) ^ (2 * ctx.order) * K * remainingBudget ctx.next C lam K

Exact backward factorization of the budget carried by a nonempty remaining suffix.