The literal complete nested run of paper Step 3

This module closes the last exact seam between the two terminal half chains and the complete grouped primitive head used in (4.20). It keeps the primitive-pairing sum intact. The one artificial edge across the central cut is inserted only inside normalizedInput and is cancelled exactly, almost everywhere, by the moving torusDistSq numerator.

theorem Anderson4D.R324NestedCrossProperStepContext.reconstruct_eq_nextContext_reconstruct {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (v : ctx.step.SurvivingCoordinate → T4) (i : ctx.step.PostCoordinate) : ctx.step.reconstruct v ↑i = ctx.nextContext.reconstruct (ctx.step.splitSurvivingPiMeasurableEquiv v).2 ↑i

On the untouched suffix, the current reconstruction is literally the next-step reconstruction of the post tuple.

theorem Anderson4D.R324NestedCrossProperStepContext.nestedResidualPrimitiveSumProduct_next_reconstruct_eq {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (ρ : SmoothCutoff) (ε : ℝ) (v : ctx.step.SurvivingCoordinate → T4) : r324NestedResidualPrimitiveSumProduct ρ ε κp κm π ctx.step.next (ctx.step.reconstruct v) = r324NestedResidualPrimitiveSumProduct ρ ε κp κm π ctx.step.next (ctx.nextContext.reconstruct (ctx.step.splitSurvivingPiMeasurableEquiv v).2)

The grouped covariance product on the untouched suffix is insensitive to replacing the current reconstruction by the next-step reconstruction.

def Anderson4D.R324NestedCrossProperStepContext.leftPrimitiveEdgeIndices {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) : Finset (Fin (2 * ctx.step.order - 1))

Standard primitive edges wholly contained in the left half of the current cross shell.

Equations

• ctx.leftPrimitiveEdgeIndices = {j : Fin (2 * ctx.step.order - 1) | ↑j < ↑ctx.step.leftGapIndex}

def Anderson4D.R324NestedCrossProperStepContext.rightPrimitiveEdgeIndices {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) : Finset (Fin (2 * ctx.step.order - 1))

Standard primitive edges wholly contained in the right half.

Equations

• ctx.rightPrimitiveEdgeIndices = {j : Fin (2 * ctx.step.order - 1) | ↑ctx.step.rightGapIndex ≤ ↑j}

def Anderson4D.R324NestedCrossProperStepContext.centralPrimitiveEdgeIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) : Fin (2 * ctx.step.order - 1)

The unique standard edge crossing the doubled cut.

Equations

• ctx.centralPrimitiveEdgeIndex = ⟨↑ctx.step.leftGapIndex, ⋯⟩

def Anderson4D.R324NestedCrossProperStepContext.leftHeadPrimitiveEdgeIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (i : Fin m) (hi : i ∈ r324LeftHalfPullback ctx.step.head.carrier) (hne : i ≠ (r324LeftHalfPullback ctx.step.head.carrier).max' ⋯) : Fin (2 * ctx.step.order - 1)

Standard primitive edge sourced at a nonterminal left-half vertex of the current shell.

Equations

• ctx.leftHeadPrimitiveEdgeIndex i hi hne = ⟨↑(ctx.step.blockOrderIso.symm ⟨Anderson4D.leftMomentIndex i, ⋯⟩), ⋯⟩

@[simp]

theorem Anderson4D.R324NestedCrossProperStepContext.leftHeadPrimitiveEdgeIndex_val {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (i : Fin m) (hi : i ∈ r324LeftHalfPullback ctx.step.head.carrier) (hne : i ≠ (r324LeftHalfPullback ctx.step.head.carrier).max' ⋯) : ↑(ctx.leftHeadPrimitiveEdgeIndex i hi hne) = ↑(ctx.step.blockOrderIso.symm ⟨leftMomentIndex i, ⋯⟩)

theorem Anderson4D.R324NestedCrossProperStepContext.leftHeadPrimitiveEdgeIndex_mem {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (i : Fin m) (hi : i ∈ r324LeftHalfPullback ctx.step.head.carrier) (hne : i ≠ (r324LeftHalfPullback ctx.step.head.carrier).max' ⋯) : ctx.leftHeadPrimitiveEdgeIndex i hi hne ∈ ctx.leftPrimitiveEdgeIndices

def Anderson4D.R324NestedCrossProperStepContext.rightHeadPrimitiveEdgeIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (i : Fin m) (hi : i ∈ r324RightHalfPullback ctx.step.head.carrier) (hne : i ≠ (r324RightHalfPullback ctx.step.head.carrier).max' ⋯) : Fin (2 * ctx.step.order - 1)

Standard primitive edge sourced at a nonterminal right-half vertex.

Equations

• ctx.rightHeadPrimitiveEdgeIndex i hi hne = ⟨↑(ctx.step.blockOrderIso.symm ⟨Anderson4D.rightMomentIndex i, ⋯⟩), ⋯⟩

@[simp]

theorem Anderson4D.R324NestedCrossProperStepContext.rightHeadPrimitiveEdgeIndex_val {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (i : Fin m) (hi : i ∈ r324RightHalfPullback ctx.step.head.carrier) (hne : i ≠ (r324RightHalfPullback ctx.step.head.carrier).max' ⋯) : ↑(ctx.rightHeadPrimitiveEdgeIndex i hi hne) = ↑(ctx.step.blockOrderIso.symm ⟨rightMomentIndex i, ⋯⟩)

theorem Anderson4D.R324NestedCrossProperStepContext.rightHeadPrimitiveEdgeIndex_mem {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (i : Fin m) (hi : i ∈ r324RightHalfPullback ctx.step.head.carrier) (hne : i ≠ (r324RightHalfPullback ctx.step.head.carrier).max' ⋯) : ctx.rightHeadPrimitiveEdgeIndex i hi hne ∈ ctx.rightPrimitiveEdgeIndices

def Anderson4D.R324NestedCrossProperStepContext.leftHeadSuccessorVertex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (i : Fin m) (hi : i ∈ r324LeftHalfPullback ctx.step.head.carrier) (hne : i ≠ (r324LeftHalfPullback ctx.step.head.carrier).max' ⋯) : Fin m

The next terminal left vertex along a current-shell internal edge.

Equations

• ctx.leftHeadSuccessorVertex i hi hne = ⟨↑↑(ctx.step.blockOrderIso (Anderson4D.primitiveEdgeRight ctx.step.order ⋯ (ctx.leftHeadPrimitiveEdgeIndex i hi hne))), ⋯⟩

theorem Anderson4D.R324NestedCrossProperStepContext.leftMomentIndex_leftHeadSource {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (i : Fin m) (hi : i ∈ r324LeftHalfPullback ctx.step.head.carrier) (hne : i ≠ (r324LeftHalfPullback ctx.step.head.carrier).max' ⋯) : leftMomentIndex i = ↑(ctx.step.blockOrderIso (primitiveEdgeLeft ctx.step.order ⋯ (ctx.leftHeadPrimitiveEdgeIndex i hi hne)))

theorem Anderson4D.R324NestedCrossProperStepContext.leftMomentIndex_leftHeadSuccessorVertex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (i : Fin m) (hi : i ∈ r324LeftHalfPullback ctx.step.head.carrier) (hne : i ≠ (r324LeftHalfPullback ctx.step.head.carrier).max' ⋯) : leftMomentIndex (ctx.leftHeadSuccessorVertex i hi hne) = ↑(ctx.step.blockOrderIso (primitiveEdgeRight ctx.step.order ⋯ (ctx.leftHeadPrimitiveEdgeIndex i hi hne)))

def Anderson4D.R324NestedCrossProperStepContext.rightHeadSuccessorVertex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (i : Fin m) (hi : i ∈ r324RightHalfPullback ctx.step.head.carrier) (hne : i ≠ (r324RightHalfPullback ctx.step.head.carrier).max' ⋯) : Fin m

The next terminal right vertex along a current-shell internal edge.

Equations

• ctx.rightHeadSuccessorVertex i hi hne = ⟨↑↑(ctx.step.blockOrderIso (Anderson4D.primitiveEdgeRight ctx.step.order ⋯ (ctx.rightHeadPrimitiveEdgeIndex i hi hne))) - m, ⋯⟩

theorem Anderson4D.R324NestedCrossProperStepContext.rightMomentIndex_rightHeadSource {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (i : Fin m) (hi : i ∈ r324RightHalfPullback ctx.step.head.carrier) (hne : i ≠ (r324RightHalfPullback ctx.step.head.carrier).max' ⋯) : rightMomentIndex i = ↑(ctx.step.blockOrderIso (primitiveEdgeLeft ctx.step.order ⋯ (ctx.rightHeadPrimitiveEdgeIndex i hi hne)))

theorem Anderson4D.R324NestedCrossProperStepContext.rightMomentIndex_rightHeadSuccessorVertex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (i : Fin m) (hi : i ∈ r324RightHalfPullback ctx.step.head.carrier) (hne : i ≠ (r324RightHalfPullback ctx.step.head.carrier).max' ⋯) : rightMomentIndex (ctx.rightHeadSuccessorVertex i hi hne) = ↑(ctx.step.blockOrderIso (primitiveEdgeRight ctx.step.order ⋯ (ctx.rightHeadPrimitiveEdgeIndex i hi hne)))

@[simp]

theorem Anderson4D.R324NestedCrossProperStepContext.primitiveEdgeLeft_centralPrimitiveEdgeIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) : primitiveEdgeLeft ctx.step.order ⋯ ctx.centralPrimitiveEdgeIndex = ctx.step.leftGapIndex

@[simp]

theorem Anderson4D.R324NestedCrossProperStepContext.primitiveEdgeRight_centralPrimitiveEdgeIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) : primitiveEdgeRight ctx.step.order ⋯ ctx.centralPrimitiveEdgeIndex = ctx.step.rightGapIndex

theorem Anderson4D.R324NestedCrossProperStepContext.primitiveEdgeIndices_eq_left_central_right {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) : Finset.univ = ctx.leftPrimitiveEdgeIndices ∪ {ctx.centralPrimitiveEdgeIndex} ∪ ctx.rightPrimitiveEdgeIndices

The primitive edge family is the disjoint union of left internal edges, the phantom cut edge, and right internal edges.

theorem Anderson4D.R324NestedCrossProperStepContext.leftPrimitiveEdgeIndices_disjoint_central {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) : Disjoint ctx.leftPrimitiveEdgeIndices {ctx.centralPrimitiveEdgeIndex}

theorem Anderson4D.R324NestedCrossProperStepContext.leftCentral_disjoint_rightPrimitiveEdgeIndices {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) : Disjoint (ctx.leftPrimitiveEdgeIndices ∪ {ctx.centralPrimitiveEdgeIndex}) ctx.rightPrimitiveEdgeIndices

theorem Anderson4D.R324NestedCrossProperStepContext.primitiveChainProduct_normalized_eq_left_central_right {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (t : Fin (2 * ctx.step.order) → T4) : primitiveChainProduct ctx.step.order ⋯ ctx.step.normalizedInput t = (∏ j ∈ ctx.leftPrimitiveEdgeIndices, invSqKer (t (primitiveEdgeLeft ctx.step.order ⋯ j) - t (primitiveEdgeRight ctx.step.order ⋯ j))) * invSqKer (t ctx.step.leftGapIndex - t ctx.step.rightGapIndex) * ∏ j ∈ ctx.rightPrimitiveEdgeIndices, invSqKer (t (primitiveEdgeLeft ctx.step.order ⋯ j) - t (primitiveEdgeRight ctx.step.order ⋯ j))

Exact three-way product decomposition of the normalized primitive chain.

Head-local geometry for the genuine final shell

The preceding declarations were originally stated on a proper step because they were first needed to expose the two connector legs. The final shell has no next block. The following head-local names record exactly the same sparse primitive order without manufacturing a dummy proper step.

theorem Anderson4D.R324NestedCrossStepContext.finalLeftHeadNonempty {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) : (r324LeftHalfPullback step.head.carrier).Nonempty

theorem Anderson4D.R324NestedCrossStepContext.finalRightHeadNonempty {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) : (r324RightHalfPullback step.head.carrier).Nonempty

theorem Anderson4D.R324NestedCrossStepContext.final_leftGapIndex_add_one_eq_rightGapIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) : ↑step.leftGapIndex + 1 = ↑step.rightGapIndex

The two cut sites are consecutive in the standard increasing order of the final shell.

def Anderson4D.R324NestedCrossStepContext.finalLeftPrimitiveEdgeIndices {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) : Finset (Fin (2 * step.order - 1))

Equations

• step.finalLeftPrimitiveEdgeIndices = {j : Fin (2 * step.order - 1) | ↑j < ↑step.leftGapIndex}

def Anderson4D.R324NestedCrossStepContext.finalRightPrimitiveEdgeIndices {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) : Finset (Fin (2 * step.order - 1))

Equations

• step.finalRightPrimitiveEdgeIndices = {j : Fin (2 * step.order - 1) | ↑step.rightGapIndex ≤ ↑j}

def Anderson4D.R324NestedCrossStepContext.finalCentralPrimitiveEdgeIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) : Fin (2 * step.order - 1)

Equations

• step.finalCentralPrimitiveEdgeIndex = ⟨↑step.leftGapIndex, ⋯⟩

def Anderson4D.R324NestedCrossStepContext.finalLeftHeadPrimitiveEdgeIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) (i : Fin m) (hi : i ∈ r324LeftHalfPullback step.head.carrier) (hne : i ≠ (r324LeftHalfPullback step.head.carrier).max' ⋯) : Fin (2 * step.order - 1)

Equations

• step.finalLeftHeadPrimitiveEdgeIndex i hi hne = ⟨↑(step.blockOrderIso.symm ⟨Anderson4D.leftMomentIndex i, ⋯⟩), ⋯⟩

@[simp]

theorem Anderson4D.R324NestedCrossStepContext.finalLeftHeadPrimitiveEdgeIndex_val {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) (i : Fin m) (hi : i ∈ r324LeftHalfPullback step.head.carrier) (hne : i ≠ (r324LeftHalfPullback step.head.carrier).max' ⋯) : ↑(step.finalLeftHeadPrimitiveEdgeIndex i hi hne) = ↑(step.blockOrderIso.symm ⟨leftMomentIndex i, ⋯⟩)

theorem Anderson4D.R324NestedCrossStepContext.finalLeftHeadPrimitiveEdgeIndex_mem {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) (i : Fin m) (hi : i ∈ r324LeftHalfPullback step.head.carrier) (hne : i ≠ (r324LeftHalfPullback step.head.carrier).max' ⋯) : step.finalLeftHeadPrimitiveEdgeIndex i hi hne ∈ step.finalLeftPrimitiveEdgeIndices

def Anderson4D.R324NestedCrossStepContext.finalRightHeadPrimitiveEdgeIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) (i : Fin m) (hi : i ∈ r324RightHalfPullback step.head.carrier) (hne : i ≠ (r324RightHalfPullback step.head.carrier).max' ⋯) : Fin (2 * step.order - 1)

Equations

• step.finalRightHeadPrimitiveEdgeIndex i hi hne = ⟨↑(step.blockOrderIso.symm ⟨Anderson4D.rightMomentIndex i, ⋯⟩), ⋯⟩

@[simp]

theorem Anderson4D.R324NestedCrossStepContext.finalRightHeadPrimitiveEdgeIndex_val {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) (i : Fin m) (hi : i ∈ r324RightHalfPullback step.head.carrier) (hne : i ≠ (r324RightHalfPullback step.head.carrier).max' ⋯) : ↑(step.finalRightHeadPrimitiveEdgeIndex i hi hne) = ↑(step.blockOrderIso.symm ⟨rightMomentIndex i, ⋯⟩)

theorem Anderson4D.R324NestedCrossStepContext.finalRightHeadPrimitiveEdgeIndex_mem {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) (i : Fin m) (hi : i ∈ r324RightHalfPullback step.head.carrier) (hne : i ≠ (r324RightHalfPullback step.head.carrier).max' ⋯) : step.finalRightHeadPrimitiveEdgeIndex i hi hne ∈ step.finalRightPrimitiveEdgeIndices

def Anderson4D.R324NestedCrossStepContext.finalLeftHeadSuccessorVertex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) (i : Fin m) (hi : i ∈ r324LeftHalfPullback step.head.carrier) (hne : i ≠ (r324LeftHalfPullback step.head.carrier).max' ⋯) : Fin m

Equations

• step.finalLeftHeadSuccessorVertex i hi hne = ⟨↑↑(step.blockOrderIso (Anderson4D.primitiveEdgeRight step.order ⋯ (step.finalLeftHeadPrimitiveEdgeIndex i hi hne))), ⋯⟩

theorem Anderson4D.R324NestedCrossStepContext.final_leftMomentIndex_headSource {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) (i : Fin m) (hi : i ∈ r324LeftHalfPullback step.head.carrier) (hne : i ≠ (r324LeftHalfPullback step.head.carrier).max' ⋯) : leftMomentIndex i = ↑(step.blockOrderIso (primitiveEdgeLeft step.order ⋯ (step.finalLeftHeadPrimitiveEdgeIndex i hi hne)))

theorem Anderson4D.R324NestedCrossStepContext.final_leftMomentIndex_headSuccessor {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) (i : Fin m) (hi : i ∈ r324LeftHalfPullback step.head.carrier) (hne : i ≠ (r324LeftHalfPullback step.head.carrier).max' ⋯) : leftMomentIndex (step.finalLeftHeadSuccessorVertex i hi hne) = ↑(step.blockOrderIso (primitiveEdgeRight step.order ⋯ (step.finalLeftHeadPrimitiveEdgeIndex i hi hne)))

def Anderson4D.R324NestedCrossStepContext.finalRightHeadSuccessorVertex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) (i : Fin m) (hi : i ∈ r324RightHalfPullback step.head.carrier) (hne : i ≠ (r324RightHalfPullback step.head.carrier).max' ⋯) : Fin m

Equations

• step.finalRightHeadSuccessorVertex i hi hne = ⟨↑↑(step.blockOrderIso (Anderson4D.primitiveEdgeRight step.order ⋯ (step.finalRightHeadPrimitiveEdgeIndex i hi hne))) - m, ⋯⟩

theorem Anderson4D.R324NestedCrossStepContext.final_rightMomentIndex_headSource {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) (i : Fin m) (hi : i ∈ r324RightHalfPullback step.head.carrier) (hne : i ≠ (r324RightHalfPullback step.head.carrier).max' ⋯) : rightMomentIndex i = ↑(step.blockOrderIso (primitiveEdgeLeft step.order ⋯ (step.finalRightHeadPrimitiveEdgeIndex i hi hne)))

theorem Anderson4D.R324NestedCrossStepContext.final_rightMomentIndex_headSuccessor {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) (i : Fin m) (hi : i ∈ r324RightHalfPullback step.head.carrier) (hne : i ≠ (r324RightHalfPullback step.head.carrier).max' ⋯) : rightMomentIndex (step.finalRightHeadSuccessorVertex i hi hne) = ↑(step.blockOrderIso (primitiveEdgeRight step.order ⋯ (step.finalRightHeadPrimitiveEdgeIndex i hi hne)))

@[simp]

theorem Anderson4D.R324NestedCrossStepContext.primitiveEdgeLeft_finalCentralPrimitiveEdgeIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) : primitiveEdgeLeft step.order ⋯ step.finalCentralPrimitiveEdgeIndex = step.leftGapIndex

@[simp]

theorem Anderson4D.R324NestedCrossStepContext.primitiveEdgeRight_finalCentralPrimitiveEdgeIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) : primitiveEdgeRight step.order ⋯ step.finalCentralPrimitiveEdgeIndex = step.rightGapIndex

theorem Anderson4D.R324NestedCrossStepContext.finalPrimitiveEdgeIndices_eq_left_central_right {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) : Finset.univ = step.finalLeftPrimitiveEdgeIndices ∪ {step.finalCentralPrimitiveEdgeIndex} ∪ step.finalRightPrimitiveEdgeIndices

theorem Anderson4D.R324NestedCrossStepContext.finalLeftPrimitiveEdgeIndices_disjoint_central {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) : Disjoint step.finalLeftPrimitiveEdgeIndices {step.finalCentralPrimitiveEdgeIndex}

theorem Anderson4D.R324NestedCrossStepContext.finalLeftCentral_disjoint_rightPrimitiveEdgeIndices {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) : Disjoint (step.finalLeftPrimitiveEdgeIndices ∪ {step.finalCentralPrimitiveEdgeIndex}) step.finalRightPrimitiveEdgeIndices

theorem Anderson4D.R324NestedCrossStepContext.primitiveChainProduct_normalized_eq_finalParts {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) (t : Fin (2 * step.order) → T4) : primitiveChainProduct step.order ⋯ step.normalizedInput t = (∏ j ∈ step.finalLeftPrimitiveEdgeIndices, invSqKer (t (primitiveEdgeLeft step.order ⋯ j) - t (primitiveEdgeRight step.order ⋯ j))) * invSqKer (t step.leftGapIndex - t step.rightGapIndex) * ∏ j ∈ step.finalRightPrimitiveEdgeIndices, invSqKer (t (primitiveEdgeLeft step.order ⋯ j) - t (primitiveEdgeRight step.order ⋯ j))

theorem Anderson4D.R324NestedCrossStepContext.final_blockOrderIso_last_eq_max {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) : ↑(step.blockOrderIso (primitiveLast step.order ⋯)) = step.head.carrier.max' ⋯

theorem Anderson4D.R324NestedCrossStepContext.final_rightMomentIndex_headMax_eq_last {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) : rightMomentIndex ((r324RightHalfPullback step.head.carrier).max' ⋯) = ↑(step.blockOrderIso (primitiveLast step.order ⋯))

theorem Anderson4D.R324TwoHalfTerminalData.left_edgeSuccessor_finalHeadInternal {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) (htail : step.tail = []) (i : Fin m) (hi : i ∈ r324LeftHalfPullback step.head.carrier) (hne : i ≠ (r324LeftHalfPullback step.head.carrier).max' ⋯) : terminal.left.edgeSuccessor (r324InternalVertexEdgeSlot i) = varIdx (step.finalLeftHeadSuccessorVertex i hi hne)

Internal successor geometry for the genuine last left shell. The tail = [] hypothesis removes the connector case and leaves exactly the next standard primitive coordinate.

theorem Anderson4D.R324TwoHalfTerminalData.right_edgeSuccessor_finalHeadInternal {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) (htail : step.tail = []) (i : Fin m) (hi : i ∈ r324RightHalfPullback step.head.carrier) (hne : i ≠ (r324RightHalfPullback step.head.carrier).max' ⋯) : terminal.right.edgeSuccessor (r324InternalVertexEdgeSlot i) = varIdx (step.finalRightHeadSuccessorVertex i hi hne)

Right-half analogue of left_edgeSuccessor_finalHeadInternal.

theorem Anderson4D.R324TwoHalfTerminalData.left_finalHeadInternal_edgeDisplacement_eq {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) (htail : step.tail = []) (i : Fin m) (hi : i ∈ r324LeftHalfPullback step.head.carrier) (hne : i ≠ (r324LeftHalfPullback step.head.carrier).max' ⋯) (v : step.SurvivingCoordinate → T4) : terminal.left.edgeDisplacement 0 0 (terminal.left.reconstruct (terminal.leftTupleOfNestedStep step v)) (r324InternalVertexEdgeSlot i) = (step.splitSurvivingPiMeasurableEquiv v).1 (primitiveEdgeLeft step.order ⋯ (step.finalLeftHeadPrimitiveEdgeIndex i hi hne)) - (step.splitSurvivingPiMeasurableEquiv v).1 (primitiveEdgeRight step.order ⋯ (step.finalLeftHeadPrimitiveEdgeIndex i hi hne))

theorem Anderson4D.R324TwoHalfTerminalData.right_finalHeadInternal_edgeDisplacement_eq {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) (htail : step.tail = []) (i : Fin m) (hi : i ∈ r324RightHalfPullback step.head.carrier) (hne : i ≠ (r324RightHalfPullback step.head.carrier).max' ⋯) (v : step.SurvivingCoordinate → T4) : terminal.right.edgeDisplacement 0 0 (terminal.right.reconstruct (terminal.rightTupleOfNestedStep step v)) (r324InternalVertexEdgeSlot i) = (step.splitSurvivingPiMeasurableEquiv v).1 (primitiveEdgeLeft step.order ⋯ (step.finalRightHeadPrimitiveEdgeIndex i hi hne)) - (step.splitSurvivingPiMeasurableEquiv v).1 (primitiveEdgeRight step.order ⋯ (step.finalRightHeadPrimitiveEdgeIndex i hi hne))

theorem Anderson4D.R324TwoHalfTerminalData.left_edgeSuccessor_headInternal {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (i : Fin m) (hi : i ∈ r324LeftHalfPullback ctx.step.head.carrier) (hne : i ≠ (r324LeftHalfPullback ctx.step.head.carrier).max' ⋯) : terminal.left.edgeSuccessor (r324InternalVertexEdgeSlot i) = varIdx (ctx.leftHeadSuccessorVertex i hi hne)

A nonterminal left source in the current shell points to the next standard block coordinate in the full terminal sparse chain.

theorem Anderson4D.R324TwoHalfTerminalData.right_edgeSuccessor_headInternal {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (i : Fin m) (hi : i ∈ r324RightHalfPullback ctx.step.head.carrier) (hne : i ≠ (r324RightHalfPullback ctx.step.head.carrier).max' ⋯) : terminal.right.edgeSuccessor (r324InternalVertexEdgeSlot i) = varIdx (ctx.rightHeadSuccessorVertex i hi hne)

Right-half internal successor.

theorem Anderson4D.R324TwoHalfTerminalData.left_headInternal_edgeDisplacement_eq {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (i : Fin m) (hi : i ∈ r324LeftHalfPullback ctx.step.head.carrier) (hne : i ≠ (r324LeftHalfPullback ctx.step.head.carrier).max' ⋯) (v : ctx.step.SurvivingCoordinate → T4) : terminal.left.edgeDisplacement 0 0 (terminal.left.reconstruct (terminal.leftTupleOfNestedStep ctx.step v)) (r324InternalVertexEdgeSlot i) = (ctx.step.splitSurvivingPiMeasurableEquiv v).1 (primitiveEdgeLeft ctx.step.order ⋯ (ctx.leftHeadPrimitiveEdgeIndex i hi hne)) - (ctx.step.splitSurvivingPiMeasurableEquiv v).1 (primitiveEdgeRight ctx.step.order ⋯ (ctx.leftHeadPrimitiveEdgeIndex i hi hne))

A left internal half-chain slot reads exactly the corresponding standard primitive edge of the current head coordinates.

theorem Anderson4D.R324TwoHalfTerminalData.right_headInternal_edgeDisplacement_eq {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (i : Fin m) (hi : i ∈ r324RightHalfPullback ctx.step.head.carrier) (hne : i ≠ (r324RightHalfPullback ctx.step.head.carrier).max' ⋯) (v : ctx.step.SurvivingCoordinate → T4) : terminal.right.edgeDisplacement 0 0 (terminal.right.reconstruct (terminal.rightTupleOfNestedStep ctx.step v)) (r324InternalVertexEdgeSlot i) = (ctx.step.splitSurvivingPiMeasurableEquiv v).1 (primitiveEdgeLeft ctx.step.order ⋯ (ctx.rightHeadPrimitiveEdgeIndex i hi hne)) - (ctx.step.splitSurvivingPiMeasurableEquiv v).1 (primitiveEdgeRight ctx.step.order ⋯ (ctx.rightHeadPrimitiveEdgeIndex i hi hne))

Right-half analogue of left_headInternal_edgeDisplacement_eq.

theorem Anderson4D.R324TwoHalfTerminalData.nestedLeftHalfInvSqProduct_finalHead_eq_primitiveEdges {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) (htail : step.tail = []) (v : step.SurvivingCoordinate → T4) : terminal.nestedLeftHalfInvSqProduct step step.head.carrier ⋯ v = ∏ j ∈ step.finalLeftPrimitiveEdgeIndices, invSqKer ((step.splitSurvivingPiMeasurableEquiv v).1 (primitiveEdgeLeft step.order ⋯ j) - (step.splitSurvivingPiMeasurableEquiv v).1 (primitiveEdgeRight step.order ⋯ j))

On the genuine last shell, the restricted terminal left path is the left internal part of the normalized primitive chain.

theorem Anderson4D.R324TwoHalfTerminalData.nestedRightHalfInvSqProduct_finalHead_eq_primitiveEdges {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) (htail : step.tail = []) (v : step.SurvivingCoordinate → T4) : terminal.nestedRightHalfInvSqProduct step step.head.carrier ⋯ v = ∏ j ∈ step.finalRightPrimitiveEdgeIndices, invSqKer ((step.splitSurvivingPiMeasurableEquiv v).1 (primitiveEdgeLeft step.order ⋯ j) - (step.splitSurvivingPiMeasurableEquiv v).1 (primitiveEdgeRight step.order ⋯ j))

Right-half analogue of nestedLeftHalfInvSqProduct_finalHead_eq_primitiveEdges.

theorem Anderson4D.R324TwoHalfTerminalData.nestedLeftHalfInvSqProduct_head_eq_primitiveEdges {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (v : ctx.step.SurvivingCoordinate → T4) : terminal.nestedLeftHalfInvSqProduct ctx.step ctx.step.head.carrier ⋯ v = ∏ j ∈ ctx.leftPrimitiveEdgeIndices, invSqKer ((ctx.step.splitSurvivingPiMeasurableEquiv v).1 (primitiveEdgeLeft ctx.step.order ⋯ j) - (ctx.step.splitSurvivingPiMeasurableEquiv v).1 (primitiveEdgeRight ctx.step.order ⋯ j))

The restricted terminal left path is exactly the left internal part of the normalized primitive chain.

theorem Anderson4D.R324TwoHalfTerminalData.nestedRightHalfInvSqProduct_head_eq_primitiveEdges {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (v : ctx.step.SurvivingCoordinate → T4) : terminal.nestedRightHalfInvSqProduct ctx.step ctx.step.head.carrier ⋯ v = ∏ j ∈ ctx.rightPrimitiveEdgeIndices, invSqKer ((ctx.step.splitSurvivingPiMeasurableEquiv v).1 (primitiveEdgeLeft ctx.step.order ⋯ j) - (ctx.step.splitSurvivingPiMeasurableEquiv v).1 (primitiveEdgeRight ctx.step.order ⋯ j))

The restricted terminal right path is exactly the right internal part of the normalized primitive chain.

theorem Anderson4D.R324TwoHalfTerminalData.ae_headHalfPaths_mul_completeCrossGap_one_eq_completeNormalized {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) : ∀ᵐ (v : ctx.step.SurvivingCoordinate → T4) ∂MeasureTheory.Measure.pi fun (x : ctx.step.SurvivingCoordinate) => paperMeasure, lamEps lam ε ^ (2 * ctx.step.order) * (terminal.nestedLeftHalfInvSqProduct ctx.step ctx.step.head.carrier ⋯ v * terminal.nestedRightHalfInvSqProduct ctx.step ctx.step.head.carrier ⋯ v * ∑ κ ∈ primitiveFullPairings ctx.step.order, primitiveCovarianceProduct ρ ε ctx.step.order κ (ctx.step.splitSurvivingPiMeasurableEquiv v).1) = ctx.step.completeNormalizedHeadDensity ρ lam ε (ctx.step.splitSurvivingPiMeasurableEquiv v).1

Paper Step 3's exact current-shell identity. The two physical half paths contain every normalized primitive edge except the cut edge; the moving torusDistSq numerator cancels precisely that missing edge almost everywhere. The complete primitive-pairing covariance sum remains grouped throughout.

theorem Anderson4D.R324TwoHalfTerminalData.ae_finalHeadHalfPaths_mul_completeCrossGap_one_eq_completeNormalized {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) (htail : step.tail = []) : ∀ᵐ (v : step.SurvivingCoordinate → T4) ∂MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure, lamEps lam ε ^ (2 * step.order) * (terminal.nestedLeftHalfInvSqProduct step step.head.carrier ⋯ v * terminal.nestedRightHalfInvSqProduct step step.head.carrier ⋯ v * ∑ κ ∈ primitiveFullPairings step.order, primitiveCovarianceProduct ρ ε step.order κ (step.splitSurvivingPiMeasurableEquiv v).1) = step.completeNormalizedHeadDensity ρ lam ε (step.splitSurvivingPiMeasurableEquiv v).1

The last application of paper (4.4): on a genuine final shell the two terminal half paths contain every normalized primitive edge except the cut edge, which is cancelled a.e. by the moving gap numerator.

theorem Anderson4D.R324TwoHalfTerminalData.nestedLeftHalfInvSqProduct_post_eq_next {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (v : ctx.step.SurvivingCoordinate → T4) : terminal.nestedLeftHalfInvSqProduct ctx.step ctx.step.next.activeCarrier ⋯ v = terminal.nestedLeftHalfInvSqProduct ctx.nextContext ctx.step.next.activeCarrier ⋯ fun (i : ctx.nextContext.SurvivingCoordinate) => (ctx.step.splitSurvivingPiMeasurableEquiv v).2 ⟨↑i, ⋯⟩

The left post-path is unchanged when it is re-read as the current path of the next literal shell.

theorem Anderson4D.R324TwoHalfTerminalData.nestedRightHalfInvSqProduct_post_eq_next {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (v : ctx.step.SurvivingCoordinate → T4) : terminal.nestedRightHalfInvSqProduct ctx.step ctx.step.next.activeCarrier ⋯ v = terminal.nestedRightHalfInvSqProduct ctx.nextContext ctx.step.next.activeCarrier ⋯ fun (i : ctx.nextContext.SurvivingCoordinate) => (ctx.step.splitSurvivingPiMeasurableEquiv v).2 ⟨↑i, ⋯⟩

Right-half analogue of nestedLeftHalfInvSqProduct_post_eq_next.

noncomputable def Anderson4D.R324TwoHalfTerminalData.completeNestedRunDensity {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) (hleft : (r324LeftHalfPullback step.residual.activeCarrier).Nonempty) (hright : (r324RightHalfPullback step.residual.activeCarrier).Nonempty) (v : step.SurvivingCoordinate → T4) : ℝ

The literal nonnegative Steps 2--3 density on one remaining nested suffix: both terminal half paths and every residual block covariance are kept as products/sums until the shell is removed.

Equations

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

theorem Anderson4D.R324TwoHalfTerminalData.ae_completeNestedRunDensity_eq_head_connector_next {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) : terminal.completeNestedRunDensity ctx.step ⋯ ⋯ =ᵐ[MeasureTheory.Measure.pi fun (x : ctx.step.SurvivingCoordinate) => paperMeasure] fun (v : ctx.step.SurvivingCoordinate → T4) => ctx.step.completeNormalizedHeadDensity ρ lam ε (ctx.step.splitSurvivingPiMeasurableEquiv v).1 * ctx.connector (ctx.step.splitSurvivingPiMeasurableEquiv v).1 (ctx.step.splitSurvivingPiMeasurableEquiv v).2 * terminal.completeNestedRunDensity ctx.nextContext ⋯ ⋯ fun (i : ctx.nextContext.SurvivingCoordinate) => (ctx.step.splitSurvivingPiMeasurableEquiv v).2 ⟨↑i, ⋯⟩

Literal one-shell recursion for paper Step 3. The equality is a.e. only because the compensating cut edge is cancelled off the diagonal; no absolute value and no pairing-wise triangle inequality is used.

Integrability certificates for the literal complete run

theorem Anderson4D.R324NestedCrossStepContext.integrable_completeNormalizedHeadDensity_at_truncation {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (hlam : 0 < lam) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) : MeasureTheory.Integrable (ctx.completeNormalizedHeadDensity ρ lam ε) (MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.order)) => paperMeasure)

Proposition 4.1 supplies the genuine integrability certificate for one complete normalized shell, uniformly over every shell below the ambient truncation. This is separated from the quantitative terminal bound because the budget-run constructor needs the certificate itself.

theorem Anderson4D.R324NestedCrossProperStepContext.integrable_completeNormalizedHeadDensity_mul_connector_at_truncation {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (hlam : 0 < lam) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (post : ctx.step.PostCoordinate → T4) : MeasureTheory.Integrable (fun (t : Fin (2 * ctx.step.order) → T4) => ctx.step.completeNormalizedHeadDensity ρ lam ε t * ctx.connector t post) (MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.step.order)) => paperMeasure)

A complete normalized proper shell remains integrable after the two literal flanking edges are attached. The proof first integrates only the internal block variables, and compares the resulting endpoint density with the already-established inserted-convolution majorant.

theorem Anderson4D.R324NestedCrossProperStepContext.integrable_completeProperDensity_at_truncation {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (hlam : 0 < lam) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (hmtrunc : m ≤ truncOrder ε) (nextDensity : (ctx.step.PostCoordinate → T4) → ℝ) (hnext : MeasureTheory.Integrable nextDensity (MeasureTheory.Measure.pi fun (x : ctx.step.PostCoordinate) => paperMeasure)) : MeasureTheory.Integrable (fun (v : ctx.step.SurvivingCoordinate → T4) => ((ctx.step.completeNormalizedHeadDensity ρ lam ε fun (j : Fin (2 * ctx.step.order)) => v (ctx.step.headSurvivingCoordinate j)) * ctx.connector (fun (j : Fin (2 * ctx.step.order)) => v (ctx.step.headSurvivingCoordinate j)) fun (i : ctx.step.PostCoordinate) => v (ctx.step.postSurvivingCoordinate i)) * nextDensity fun (i : ctx.step.PostCoordinate) => v (ctx.step.postSurvivingCoordinate i)) (MeasureTheory.Measure.pi fun (x : ctx.step.SurvivingCoordinate) => paperMeasure)

If the untouched outer suffix is integrable, then adjoining one complete proper shell gives the exact integrable density required by the proper constructor of R324CompleteNestedCrossBudgetRun.

noncomputable def Anderson4D.R324NestedCrossStepContext.completeHeadPullbackDensity {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (v : ctx.SurvivingCoordinate → T4) : ℝ

The complete head density read on the genuine surviving carrier. At the final shell the post coordinate is empty; retaining this uniform definition lets the structural recursion use the same coordinate split at every depth.

Equations

• ctx.completeHeadPullbackDensity ρ lam ε v = ctx.completeNormalizedHeadDensity ρ lam ε (ctx.splitSurvivingPiMeasurableEquiv v).1

theorem Anderson4D.R324NestedCrossStepContext.completeHeadPullbackDensity_nonneg {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (v : ctx.SurvivingCoordinate → T4) : 0 ≤ ctx.completeHeadPullbackDensity ρ lam ε v

theorem Anderson4D.R324NestedCrossStepContext.integrable_completeHeadPullbackDensity_at_truncation {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (hlam : 0 < lam) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) : MeasureTheory.Integrable (ctx.completeHeadPullbackDensity ρ lam ε) (MeasureTheory.Measure.pi fun (x : ctx.SurvivingCoordinate) => paperMeasure)

theorem Anderson4D.R324NestedCrossStepContext.integral_completeHeadPullbackDensity_eq_of_tail_eq_nil {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (htail : ctx.tail = []) : (∫ (v : ctx.SurvivingCoordinate → T4), ctx.completeHeadPullbackDensity ρ lam ε v ∂MeasureTheory.Measure.pi fun (x : ctx.SurvivingCoordinate) => paperMeasure) = ∫ (t : Fin (2 * ctx.order) → T4), ctx.completeNormalizedHeadDensity ρ lam ε t ∂MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.order)) => paperMeasure

At the genuine final shell the post carrier is empty, so pulling the complete head back to the surviving carrier does not create an additional volume factor. This is the terminal Fubini identity in paper Step 3.

theorem Anderson4D.R324TwoHalfTerminalData.ae_completeNestedRunDensity_eq_completeHeadPullback_of_tail_eq_nil {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) (htail : step.tail = []) (hleft : (r324LeftHalfPullback step.residual.activeCarrier).Nonempty) (hright : (r324RightHalfPullback step.residual.activeCarrier).Nonempty) : terminal.completeNestedRunDensity step hleft hright =ᵐ[MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure] step.completeHeadPullbackDensity ρ lam ε

Base case of the literal Step 3 recursion. When no outer shell remains, the grouped physical density is exactly the complete final primitive head, almost everywhere.

theorem Anderson4D.R324NestedCrossStepContext.ae_post_comp_eq {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (step : R324NestedCrossStepContext κp κm π) {f g : (step.PostCoordinate → T4) → ℝ} (hfg : f =ᵐ[MeasureTheory.Measure.pi fun (x : step.PostCoordinate) => paperMeasure] g) : (fun (v : step.SurvivingCoordinate → T4) => f fun (i : step.PostCoordinate) => v (step.postSurvivingCoordinate i)) =ᵐ[MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure] fun (v : step.SurvivingCoordinate → T4) => g fun (i : step.PostCoordinate) => v (step.postSurvivingCoordinate i)

Pull an a.e. identity on the untouched suffix back to the current surviving carrier.

Structural producer for the existing complete budget run

theorem Anderson4D.exists_r324CompleteNestedCrossBudgetRun_identified {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hlam : 0 < lam) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (hmtrunc : m ≤ truncOrder ε) (step : R324NestedCrossStepContext κp κm π) (hleft : (r324LeftHalfPullback step.residual.activeCarrier).Nonempty) (hright : (r324RightHalfPullback step.residual.activeCarrier).Nonempty) : ∃ (density : (step.SurvivingCoordinate → T4) → ℝ) (prefixOrder : ℕ) (terminalOrder : ℕ), R324CompleteNestedCrossBudgetRun ρ lam ε step.residual density prefixOrder terminalOrder ∧ terminal.completeNestedRunDensity step hleft hright =ᵐ[MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure] density ∧ step.residual.remainingOrder = prefixOrder + terminalOrder

The literal grouped Step 3 density is identified a.e. with the density of an existing complete budget run. The accompanying equality of orders is the exact inside-to-outside ledger of (4.20), not an auxiliary estimate.

theorem Anderson4D.R324TwoHalfTerminalData.integrable_completeNestedRunDensity_at_truncation {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hlam : 0 < lam) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (hmtrunc : m ≤ truncOrder ε) (step : R324NestedCrossStepContext κp κm π) (hleft : (r324LeftHalfPullback step.residual.activeCarrier).Nonempty) (hright : (r324RightHalfPullback step.residual.activeCarrier).Nonempty) : MeasureTheory.Integrable (terminal.completeNestedRunDensity step hleft hright) (MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure)

The literal grouped Step 3 density is integrable throughout the paper's truncation range. This is only the public analytic consequence of the identified complete budget run above.

theorem Anderson4D.R324TwoHalfTerminalData.ae_completeNestedRunDensity_nonneg_at_truncation {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hlam : 0 < lam) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (hmtrunc : m ≤ truncOrder ε) (step : R324NestedCrossStepContext κp κm π) (hleft : (r324LeftHalfPullback step.residual.activeCarrier).Nonempty) (hright : (r324RightHalfPullback step.residual.activeCarrier).Nonempty) : ∀ᵐ (v : step.SurvivingCoordinate → T4) ∂MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure, 0 ≤ terminal.completeNestedRunDensity step hleft hright v

Positivity of the literal grouped Step 3 density, in the a.e. form needed by the proper-head integral comparison.

theorem Anderson4D.R324TwoHalfTerminalData.exists_prefix_terminal_integral_completeNestedRunDensity_le {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) {D : ℝ} (hlam : 0 < lam) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (hmtrunc : m ≤ truncOrder ε) (provider : R324CompleteProperHeadSharpProvider ρ lam ε D κp κm π) (step : R324NestedCrossStepContext κp κm π) (hleft : (r324LeftHalfPullback step.residual.activeCarrier).Nonempty) (hright : (r324RightHalfPullback step.residual.activeCarrier).Nonempty) : ∃ (prefixOrder : ℕ) (terminalOrder : ℕ) (finalStep : R324NestedCrossStepContext κp κm π), step.residual.remainingOrder = prefixOrder + terminalOrder ∧ terminalOrder = finalStep.order ∧ (∫ (v : step.SurvivingCoordinate → T4), terminal.completeNestedRunDensity step hleft hright v ∂MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure) ≤ (D * lam) ^ (2 * prefixOrder) * ∫ (t : Fin (2 * finalStep.order) → T4), finalStep.completeNormalizedHeadDensity ρ lam ε t ∂MeasureTheory.Measure.pi fun (x : Fin (2 * finalStep.order)) => paperMeasure

Paper Step 3, quantitatively: removing all proper nested shells leaves one genuine final complete head. prefixOrder is exactly the sum of the removed proper-shell orders and terminalOrder is the order of that final head. This statement keeps the complete primitive-pairing sum grouped through every Fubini transition.

theorem Anderson4D.R324TwoHalfTerminalData.exists_integral_completeNestedRunDensity_le_primitiveInsertedMajorant (ρ : SmoothCutoff) : ∃ (supportConstant : ℝ) (C : ℝ), 0 < supportConstant ∧ 0 < C ∧ ∀ {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm), 0 < lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → m ≤ truncOrder ε → ∀ (step : R324NestedCrossStepContext κp κm π) (hleft : (r324LeftHalfPullback step.residual.activeCarrier).Nonempty) (hright : (r324RightHalfPullback step.residual.activeCarrier).Nonempty), (∫ (v : step.SurvivingCoordinate → T4), terminal.completeNestedRunDensity step hleft hright v ∂MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure) ≤ ∫ (z : T4), primitiveInsertedMajorant C lam ε supportConstant step.residual.remainingOrder z ∂paperMeasure

Uniform integrated closure of paper Steps 2(f)--3, equations (4.18)--(4.20). The two constants are selected from the cutoff before lam, ε, the pairings, the terminal half traces, or the nested schedule; the complete primitive-pairing sum is never split by a triangle inequality.

theorem Anderson4D.exists_r324CompleteNestedCrossBudgetRun_of_remaining_ne_nil {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ρ : SmoothCutoff) (lam ε : ℝ) (hlam : 0 < lam) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (hmtrunc : m ≤ truncOrder ε) (res : R324NestedCrossResidualPrefix κp κm π) (hne : res.remaining ≠ []) : ∃ (density : (↥res.activeCarrier → T4) → ℝ) (prefixOrder : ℕ) (terminalOrder : ℕ), R324CompleteNestedCrossBudgetRun ρ lam ε res density prefixOrder terminalOrder

Every nonempty literal nested suffix produces the already-defined complete budget run. The recursion stops at the genuine last shell and uses proper at every preceding shell, so the accumulated prefix order is the paper's exact inside-to-outside removal order.