Shifted Green-chain adapter for the genuine first-left R-324 fibre

An R-324 pairing lives on Fin m, while its production Green skeleton is evaluated on (x,v₀,…,vₘ₋₁,y) : Fin (m+2) → T4. Thus a selected pairing vertex i occurs at Green-chain vertex varIdx i = i+1, and its physical coordinate in the doubled moment tuple is leftMomentIndex i.

This file makes both shifts explicit and factors the production renormalizedGreenSkeleton into the chain edges touching the genuine first-left block and the remaining edges. No parallel skeleton and no Fourier or absolute-value representation is introduced.

The selected block in the (m+2) Green-chain carrier

def Anderson4D.r324FirstLeftShiftedBlock {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : Finset (Fin (m + 2))

The actual first-left block, shifted past the incoming external endpoint into the production Green-chain carrier.

Equations

• Anderson4D.r324FirstLeftShiftedBlock e₀ hleft = Finset.image Anderson4D.varIdx (Anderson4D.selectedExtractionBlock e₀.fst Finset.univ hleft)

theorem Anderson4D.varIdx_injective {m : ℕ} : Function.Injective varIdx

@[simp]

theorem Anderson4D.varIdx_mem_r324FirstLeftShiftedBlock_iff {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (i : Fin m) : varIdx i ∈ r324FirstLeftShiftedBlock e₀ hleft ↔ i ∈ selectedExtractionBlock e₀.fst Finset.univ hleft

noncomputable def Anderson4D.r324FirstLeftShiftedCoordinateEquiv {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) ≃ ↥(r324FirstLeftShiftedBlock e₀ hleft)

Increasing standard block coordinates, now regarded as the internal vertices of the production (m+2) Green chain.

Equations

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

@[simp]

theorem Anderson4D.r324FirstLeftShiftedCoordinateEquiv_apply_val {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (i : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft))) : ↑((r324FirstLeftShiftedCoordinateEquiv e₀ hleft) i) = varIdx ↑((residualPrimitiveBlockOrderIso e₀.fst (selectedExtractionBlock e₀.fst Finset.univ hleft) ⋯) i)

theorem Anderson4D.r324FirstLeftShiftedCoordinateEquiv_lt_iff {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (i j : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft))) : ↑((r324FirstLeftShiftedCoordinateEquiv e₀ hleft) i) < ↑((r324FirstLeftShiftedCoordinateEquiv e₀ hleft) j) ↔ i < j

The shifted equivalence preserves the strict order. The first +1 is the R-324 external-endpoint shift; no order information is lost.

theorem Anderson4D.assemble_leftMoment_shiftedCoordinate {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (x y : T4) (v : Fin (2 * m) → T4) (i : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft))) : assemble x y (fun (k : Fin m) => v (leftMomentIndex k)) ↑((r324FirstLeftShiftedCoordinateEquiv e₀ hleft) i) = v (leftMomentIndex ↑((residualPrimitiveBlockOrderIso e₀.fst (selectedExtractionBlock e₀.fst Finset.univ hleft) ⋯) i))

On the production assembled tuple, the shifted block vertex reads exactly the leftMomentIndex coordinate used by the original first-left Fubini fibre.

Exact factorization of the production Green skeleton

def Anderson4D.R324FirstLeftChainEdgeOutside {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (edge : Fin (m + 1)) : Prop

A production Green-chain edge is exterior to the selected shifted block when neither endpoint is one of its internal vertices.

Equations

• Anderson4D.R324FirstLeftChainEdgeOutside e₀ hleft edge = (edge.castSucc ∉ Anderson4D.r324FirstLeftShiftedBlock e₀ hleft ∧ edge.succ ∉ Anderson4D.r324FirstLeftShiftedBlock e₀ hleft)

@[implicit_reducible]

instance Anderson4D.instDecidableR324FirstLeftChainEdgeOutside {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (edge : Fin (m + 1)) : Decidable (R324FirstLeftChainEdgeOutside e₀ hleft edge)

Equations

• Anderson4D.instDecidableR324FirstLeftChainEdgeOutside e₀ hleft edge = id inferInstance

noncomputable def Anderson4D.r324FirstLeftTouchingGreenProduct {m : ℕ} (κ : PartialPairing (Fin m)) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (xt : Fin (m + 2) → T4) : ℂ

All factors of the production difference product whose chain edge touches the shifted first-left block.

Equations

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

noncomputable def Anderson4D.r324FirstLeftExteriorGreenProduct {m : ℕ} (κ : PartialPairing (Fin m)) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (xt : Fin (m + 2) → T4) : ℂ

The complementary production Green factors, with both coordinate reads outside the shifted first-left block.

Equations

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

theorem Anderson4D.renormalizedGreenSkeleton_eq_firstLeftTouching_mul_exterior {m : ℕ} (κ : PartialPairing (Fin m)) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (xt : Fin (m + 2) → T4) : renormalizedGreenSkeleton κ xt = r324FirstLeftTouchingGreenProduct κ e₀ hleft xt * r324FirstLeftExteriorGreenProduct κ e₀ hleft xt

Exact touching/exterior split of the production renormalizedGreenSkeleton.

theorem Anderson4D.r324FirstLeftReconstruct_greenSkeleton_shifted_factorization {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ω : R324FirstLeftOuterCoordinate e₀ hleft) (κB : R324FirstLeftBlockCoordinate e₀ hleft) (x y : T4) (v : Fin (2 * m) → T4) : renormalizedGreenSkeleton (↑(r324FirstLeftReconstruct e₀ hleft ω κB)).fst (assemble x y fun (i : Fin m) => v (leftMomentIndex i)) = r324FirstLeftTouchingGreenProduct (↑(r324FirstLeftReconstruct e₀ hleft ω κB)).fst e₀ hleft (assemble x y fun (i : Fin m) => v (leftMomentIndex i)) * r324FirstLeftExteriorGreenProduct (↑(r324FirstLeftReconstruct e₀ hleft ω κB)).fst e₀ hleft (assemble x y fun (i : Fin m) => v (leftMomentIndex i))

Specialization to the actual reconstructed member of the original first-left moment fibre. In particular the left side is the same production skeleton occurring in deterministicMomentIntegrand.