Exact first-head bridge for the complete R-324 residual sum

This file keeps the signed terminal within-half chains intact while reindexing the complete residual primitive sum along the literal initial nested-cross schedule. For a nonempty schedule it then exposes the head/post coordinate split before any norm or estimate is taken.

The complete primitive-pairing sum on the head is kept as one finite sum. The final lemmas identify the physical terminal Green chains with one canonical head chain and the two outer connector edges.

The literal residual sum carried by an arbitrary nested suffix

noncomputable def Anderson4D.r324NestedResidualPrimitiveSumProduct {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (res : R324NestedCrossResidualPrefix κp κm π) (v : Fin (2 * m) → T4) : ℝ

Complete primitive-sum product along the remaining blocks of one literal nested-cross prefix. The argument is still the ambient doubled tuple, so this definition introduces no coordinate replacement.

Equations

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

@[simp]

theorem Anderson4D.r324NestedResidualPrimitiveSumProduct_initial {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (v : Fin (2 * m) → T4) : r324NestedResidualPrimitiveSumProduct ρ ε κp κm π (R324NestedCrossResidualPrefix.initial κp κm π) v = r324ResidualPrimitiveSumProduct ρ ε κp κm π v

theorem Anderson4D.r324NestedResidualPrimitiveSumProduct_head {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (v : Fin (2 * m) → T4) : r324NestedResidualPrimitiveSumProduct ρ ε κp κm π ctx.residual v = r324PrimitivePartitionBlockSum ρ ε κp κm π ctx.head.carrier v * r324NestedResidualPrimitiveSumProduct ρ ε κp κm π ctx.next v

The signed physical core on the concrete initial prefix

noncomputable def Anderson4D.R324TwoHalfTerminalData.initialNestedSignedChainFactor {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (x y z w : T4) (v : terminal.NestedCoordinate π → T4) : ℂ

The two completed, still signed, within-half Green chains read on the literal initial nested reconstruction.

Equations

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

theorem Anderson4D.R324TwoHalfTerminalData.initialNestedResidualSumPhysicalCore_eq_signedChain_mul_nested {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (x y z w : T4) (v : terminal.NestedCoordinate π → T4) : terminal.initialNestedResidualSumPhysicalCore π x y z w v = terminal.initialNestedSignedChainFactor π x y z w v * ↑(r324NestedResidualPrimitiveSumProduct ρ ε κp κm π (R324NestedCrossResidualPrefix.initial κp κm π) (terminal.nestedReconstruct π v))

Pointwise identification of the transported physical core with the literal initial nested prefix: the terminal Green chains stay signed and the complete residual primitive sums remain grouped blockwise.

A nonempty initial schedule and its exact head/post split

def Anderson4D.r324InitialNestedCrossStepContext {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (head : R324NestedCrossBlock κp κm π) (tail : List (R324NestedCrossBlock κp κm π)) (hremaining : (R324NestedCrossResidualPrefix.initial κp κm π).remaining = head :: tail) : R324NestedCrossStepContext κp κm π

The proof-relevant first step of a nonempty literal initial schedule.

Equations

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

theorem Anderson4D.R324NestedCrossStepContext.initial_residualSum_reconstruct_split {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (hinitial : ctx.residual = R324NestedCrossResidualPrefix.initial κp κm π) (ρ : SmoothCutoff) (ε : ℝ) (t : Fin (2 * ctx.order) → T4) (post : ctx.PostCoordinate → T4) : r324ResidualPrimitiveSumProduct ρ ε κp κm π (ctx.reconstruct (ctx.splitSurvivingPiMeasurableEquiv.symm (t, post))) = r324PrimitivePartitionBlockSum ρ ε κp κm π ctx.head.carrier (ctx.reconstruct (ctx.splitSurvivingPiMeasurableEquiv.symm (t, post))) * r324NestedResidualPrimitiveSumProduct ρ ε κp κm π ctx.next (ctx.reconstruct (ctx.splitSurvivingPiMeasurableEquiv.symm (t, post)))

Exact first-head factorization of the complete residual primitive sum after the proved head/post coordinate split.

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

The head covariance factor, multiplied by the moving central gap, is the complete primitive head integrand with the trivial local chain. The physical signed terminal Green chains have deliberately not been moved inside this factor.

theorem Anderson4D.R324NestedCrossStepContext.centralGap_mul_nestedResidualSum_reconstruct_split {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (ε : ℝ) (t : Fin (2 * ctx.order) → T4) (post : ctx.PostCoordinate → T4) : torusDistSq (t ctx.leftGapIndex - t ctx.rightGapIndex) * r324NestedResidualPrimitiveSumProduct ρ ε κp κm π ctx.residual (ctx.reconstruct (ctx.splitSurvivingPiMeasurableEquiv.symm (t, post))) = ctx.completeCrossGapPrimitiveIntegrand ρ ε (fun (x : Fin (2 * ctx.order - 1)) (x_1 : T4) => 1) t * r324NestedResidualPrimitiveSumProduct ρ ε κp κm π ctx.next (ctx.reconstruct (ctx.splitSurvivingPiMeasurableEquiv.symm (t, post)))

Pointwise head normal form at an arbitrary nested suffix. Unlike centralGap_mul_initialResidualSum_reconstruct_split, this statement does not identify the current residual with the initial prefix. It is therefore the recursive covariance identity needed after each proper head has been removed: the complete primitive sum stays grouped, the current head is exposed exactly, and the untouched product is indexed by ctx.next.

theorem Anderson4D.R324NestedCrossStepContext.centralGap_mul_initialResidualSum_reconstruct_split {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (hinitial : ctx.residual = R324NestedCrossResidualPrefix.initial κp κm π) (ρ : SmoothCutoff) (ε : ℝ) (t : Fin (2 * ctx.order) → T4) (post : ctx.PostCoordinate → T4) : torusDistSq (t ctx.leftGapIndex - t ctx.rightGapIndex) * r324ResidualPrimitiveSumProduct ρ ε κp κm π (ctx.reconstruct (ctx.splitSurvivingPiMeasurableEquiv.symm (t, post))) = ctx.completeCrossGapPrimitiveIntegrand ρ ε (fun (x : Fin (2 * ctx.order - 1)) (x_1 : T4) => 1) t * r324NestedResidualPrimitiveSumProduct ρ ε κp κm π ctx.next (ctx.reconstruct (ctx.splitSurvivingPiMeasurableEquiv.symm (t, post)))

Pointwise first-head normal form: after multiplying by the moving central gap, the whole complete residual sum is one complete primitive head integrand times the untouched literal suffix product.