The general-order half-chain collapse on the physical product space

R324CollapseChain collapses a Green chain presented as an iterated integral. The physical fibre integrates its 2m internal coordinates against Measure.pi, so this file redoes the collapse natively on Measure.pi fun _ : Fin n => paperMeasure, by recursion on n.

The recursion is the one supplied by MeasureTheory.measurePreserving_piFinSuccAbove at the index 0: v ↦ (v 0, Fin.tail v) identifies Measure.pi over Fin (n+1) with paperMeasure.prod (Measure.pi over Fin n), so the first internal coordinate is peeled as the outer integral and the tail is a chain of length n hanging off the peeled point. Hence

r324ColPiChain (n+1) q a v
  = e_{q₀}(v 0) · G(a - v 0) · r324ColPiChain n (q ∘ succ) (v 0) (tail v)

and the collapse r324Col_piChain_integral says the whole n-fold integral is

⟨q₀+…+q_{n-1}⟩⁻² ⟨q₁+…+q_{n-1}⟩⁻² ⋯ ⟨q_{n-1}⟩⁻² · e_{q₀+…+q_{n-1}}(a),

one bracket per suffix sum, and the single surviving character carrying the total momentum out to the free head a. On the zero-momentum sector (which is what the external legs enforce, see r324Col_piChain_closed) suffix sums are minus prefix sums and the brackets are the paper's ⟨S₁⟩⁻²⋯⟨S_{n-1}⟩⁻², one per internal edge.

Everything is uniform in n: no order is hardcoded.

The chain on a pi-space

def Anderson4D.r324ColPiChain (n : ℕ) : (ℕ → Z4) → T4 → (Fin n → T4) → ℂ

The physical half chain over Fin n → T4. a is the free head (an external point or the previously peeled coordinate); each internal coordinate carries its covariance character and the Green edge joining it to its predecessor.

Equations

• Anderson4D.r324ColPiChain 0 x✝¹ x✝ x_6 = 1
• Anderson4D.r324ColPiChain n.succ x✝¹ x✝ v = Anderson4D.charT4 (x✝¹ 0) (v 0) * ↑(Anderson4D.greenFn (x✝ - v 0)) * Anderson4D.r324ColPiChain n (fun (j : ℕ) => x✝¹ (j + 1)) (v 0) (Fin.tail v)

def Anderson4D.r324ColPiAbs (n : ℕ) : T4 → (Fin n → T4) → ℝ

The modulus of the half chain: the bare Green chain.

Equations

• Anderson4D.r324ColPiAbs 0 x✝ x_4 = 1
• Anderson4D.r324ColPiAbs n.succ x✝ v = Anderson4D.greenFn (x✝ - v 0) * Anderson4D.r324ColPiAbs n (v 0) (Fin.tail v)

def Anderson4D.r324ColPiProp (n : ℕ) : (ℕ → Z4) → ℝ

The propagator product harvested by a half chain of n internal coordinates: one bracket per suffix sum of the momenta.

Equations

• Anderson4D.r324ColPiProp 0 x✝ = 1
• Anderson4D.r324ColPiProp n.succ x✝ = Anderson4D.r324ColBrk (Anderson4D.r324ColPartial x✝ (n + 1)) * Anderson4D.r324ColPiProp n fun (j : ℕ) => x✝ (j + 1)

@[simp]

theorem Anderson4D.r324ColPiChain_zero (q : ℕ → Z4) (a : T4) (v : Fin 0 → T4) : r324ColPiChain 0 q a v = 1

theorem Anderson4D.r324ColPiChain_succ (n : ℕ) (q : ℕ → Z4) (a : T4) (v : Fin (n + 1) → T4) : r324ColPiChain (n + 1) q a v = charT4 (q 0) (v 0) * ↑(greenFn (a - v 0)) * r324ColPiChain n (fun (j : ℕ) => q (j + 1)) (v 0) (Fin.tail v)

@[simp]

theorem Anderson4D.r324ColPiAbs_zero (a : T4) (v : Fin 0 → T4) : r324ColPiAbs 0 a v = 1

theorem Anderson4D.r324ColPiAbs_succ (n : ℕ) (a : T4) (v : Fin (n + 1) → T4) : r324ColPiAbs (n + 1) a v = greenFn (a - v 0) * r324ColPiAbs n (v 0) (Fin.tail v)

@[simp]

theorem Anderson4D.r324ColPiProp_zero (q : ℕ → Z4) : r324ColPiProp 0 q = 1

theorem Anderson4D.r324ColPiProp_succ (n : ℕ) (q : ℕ → Z4) : r324ColPiProp (n + 1) q = r324ColBrk (r324ColPartial q (n + 1)) * r324ColPiProp n fun (j : ℕ) => q (j + 1)

theorem Anderson4D.r324ColPartial_succ' (q : ℕ → Z4) (n : ℕ) : r324ColPartial q (n + 1) = q 0 + r324ColPartial (fun (j : ℕ) => q (j + 1)) n

theorem Anderson4D.r324ColPiAbs_nonneg (n : ℕ) (a : T4) (v : Fin n → T4) : 0 ≤ r324ColPiAbs n a v

theorem Anderson4D.r324Col_norm_piChain (n : ℕ) (q : ℕ → Z4) (a : T4) (v : Fin n → T4) : ‖r324ColPiChain n q a v‖ = r324ColPiAbs n a v

Measurability

theorem Anderson4D.r324Col_measurable_tail (n : ℕ) : Measurable fun (v : Fin (n + 1) → T4) => Fin.tail v

theorem Anderson4D.r324Col_measurable_piAbs (n : ℕ) : Measurable fun (p : T4 × (Fin n → T4)) => r324ColPiAbs n p.1 p.2

theorem Anderson4D.r324Col_measurable_piChain (n : ℕ) (q : ℕ → Z4) : Measurable fun (p : T4 × (Fin n → T4)) => r324ColPiChain n q p.1 p.2

Peeling one internal coordinate

noncomputable def Anderson4D.r324ColPiSucc (n : ℕ) : (Fin (n + 1) → T4) ≃ᵐ T4 × (Fin n → T4)

The head/tail splitting of Fin (n+1) → T4, as a measurable equivalence.

Equations

• Anderson4D.r324ColPiSucc n = MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) => Anderson4D.T4) 0

theorem Anderson4D.r324ColPiSucc_apply (n : ℕ) (v : Fin (n + 1) → T4) : (r324ColPiSucc n) v = (v 0, Fin.tail v)

theorem Anderson4D.r324Col_measurePreserving_piSucc (n : ℕ) : MeasureTheory.MeasurePreserving (⇑(r324ColPiSucc n)) (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure) (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure))

theorem Anderson4D.r324Col_pi_peel_integrable {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] (F : T4 × (Fin n → T4) → E) (hF : MeasureTheory.Integrable F (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure))) : MeasureTheory.Integrable (fun (v : Fin (n + 1) → T4) => F (v 0, Fin.tail v)) (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure)

theorem Anderson4D.r324Col_pi_peel {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : T4 × (Fin n → T4) → E) (hF : MeasureTheory.Integrable F (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure))) : (∫ (v : Fin (n + 1) → T4), F (v 0, Fin.tail v) ∂MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure) = ∫ (a : T4), ∫ (w : Fin n → T4), F (a, w) ∂MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure ∂paperMeasure

Peeling the head coordinate of a pi-integral. This is the one measure-theoretic step of the recursion, uniform in n.

The bare chain has unit mass

theorem Anderson4D.r324Col_integrable_greenFn_head (a : T4) : MeasureTheory.Integrable (fun (b : T4) => greenFn (a - b)) paperMeasure

theorem Anderson4D.r324Col_piAbs_integrable_integral (n : ℕ) (a : T4) : MeasureTheory.Integrable (r324ColPiAbs n a) (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure) ∧ (∫ (v : Fin n → T4), r324ColPiAbs n a v ∂MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure) = 1

The bare Green chain is a probability density in its internal coordinates, at every length. This supplies every integrability side condition of the collapse.

theorem Anderson4D.r324Col_piChain_integrable (n : ℕ) (q : ℕ → Z4) (a : T4) : MeasureTheory.Integrable (r324ColPiChain n q a) (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure)

The general-order half-chain collapse

theorem Anderson4D.r324Col_piChain_integral (n : ℕ) (q : ℕ → Z4) (a : T4) : (∫ (v : Fin n → T4), r324ColPiChain n q a v ∂MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure) = ↑(r324ColPiProp n q) * charT4 (r324ColPartial q n) a

The half-chain collapse, at every order. The full n-fold physical integral of a Green chain against one covariance character per internal coordinate is the product of the brackets of the suffix sums of the momenta, times the single surviving character carrying the total momentum to the free head.

This is the general-m replacement for the hardcoded m ≤ 2 collapses integral_integral_greenFn_etaPair_eq_tsum and integral_prod_greenFn_mul_tsum_crossModes. The proof is a recursion on n: peel the head coordinate (r324Col_pi_peel), evaluate the exposed one-variable Green–character integral (integral_charT4_mul_greenFn_shift), and merge the migrated character with the next one (charT4_add).

theorem Anderson4D.r324Col_piChain_closed (n : ℕ) (q : ℕ → Z4) : ∫ (a : T4), ∫ (v : Fin n → T4), r324ColPiChain n q a v ∂MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure ∂paperMeasure = if r324ColPartial q n = 0 then ↑(r324ColPiProp n q * (2 * Real.pi) ^ dim) else 0

The closed half chain: momentum conservation. Integrating the free head against its own external Green leg (unit mass) leaves the Kronecker delta of total momentum: the vertex constraint that the m ≤ 2 files produced coordinate by coordinate.