The last chain slot: splitting the tail external point off the headless integrand

r324DetHeadless ρ ε m κ (assemble x y v) reads the assembled tuple only at slots ≥ 1, and the tail external point y sits at the last slot m + 1. Exactly one factor of the headless integrand touches that slot:

• the last chain edge greenFn (v_{m-1} - y), unless the slot is excluded, i.e. unless some extracted pair p has p.2.val + 1 = m;
• in that case the difference factor of that pair, greenFn (v_{m-1} - y) - greenFn (v_{p.1} - y).

The right endpoints of extract κ are pairwise distinct (extract_map_snd_nodup), so there is at most one such pair: the two cases above are exhaustive and mutually exclusive, and in both the y-dependence is the single kernel r324BetaTailKernel. Everything else is r324DetTailless, which reads only the internal variables.

The tail pair

def Anderson4D.r324TailLastIdx {m : ℕ} (hm : 0 < m) : Fin m

The last internal vertex v_{m-1}, the fixed end of the tail leg.

Equations

• Anderson4D.r324TailLastIdx hm = ⟨m - 1, ⋯⟩

def Anderson4D.r324TailPairs {m : ℕ} (κ : PartialPairing (Fin m)) : List (Fin m × Fin m)

The extracted pairs whose difference factor touches the tail external slot m + 1.

Equations

• Anderson4D.r324TailPairs κ = List.filter (fun (p : Fin m × Fin m) => decide (↑p.2 + 1 = m)) (Anderson4D.extract κ)

def Anderson4D.r324TailRest {m : ℕ} (κ : PartialPairing (Fin m)) : List (Fin m × Fin m)

The extracted pairs whose difference factor is tail free.

Equations

• Anderson4D.r324TailRest κ = List.filter (fun (p : Fin m × Fin m) => !decide (↑p.2 + 1 = m)) (Anderson4D.extract κ)

def Anderson4D.r324TailAnchor {m : ℕ} (κ : PartialPairing (Fin m)) : Option (Fin m)

The shortcut anchor of the tail leg: some ℓ when the last chain slot has been replaced by the difference factor of the extracted pair (ℓ, m-1), and none when the last chain edge survives.

Equations

• Anderson4D.r324TailAnchor κ = Option.map Prod.fst (Anderson4D.r324TailPairs κ).head?

noncomputable def Anderson4D.r324BetaTailKernel {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (v : Fin m → T4) (y : T4) : ℝ

The tail leg. The only factor of the headless integrand that sees the tail external point.

Equations

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

At most one tail pair

theorem Anderson4D.r324TailPairs_mem {m : ℕ} {κ : PartialPairing (Fin m)} {p : Fin m × Fin m} (hp : p ∈ r324TailPairs κ) : p ∈ extract κ ∧ ↑p.2 + 1 = m

theorem Anderson4D.r324TailPairs_length_le {m : ℕ} (κ : PartialPairing (Fin m)) : (r324TailPairs κ).length ≤ 1

The extracted right endpoints are distinct, so a tail pair is unique.

theorem Anderson4D.r324TailPairs_eq {m : ℕ} (κ : PartialPairing (Fin m)) : r324TailPairs κ = [] ∨ ∃ (p : Fin m × Fin m), r324TailPairs κ = [p]

The tail-pair list is either empty or a single pair.

Index bookkeeping at the last chain slot

theorem Anderson4D.r324Tail_succ_val {m : ℕ} (hm : 0 < m) : ↑(r324TailLastIdx hm).succ = m

theorem Anderson4D.r324Tail_castSucc_eq {m : ℕ} (hm : 0 < m) : (r324TailLastIdx hm).succ.castSucc = varIdx (r324TailLastIdx hm)

theorem Anderson4D.r324Tail_succ_eq {m : ℕ} (hm : 0 < m) : (r324TailLastIdx hm).succ.succ = Fin.last (m + 1)

theorem Anderson4D.r324Tail_mem_excluded_iff {m : ℕ} (κ : PartialPairing (Fin m)) : m ∈ List.map (fun (p : Fin m × Fin m) => ↑p.2 + 1) (extract κ) ↔ r324TailPairs κ ≠ []

The last chain slot is excluded exactly when a tail pair exists.

The tail-free remainder

noncomputable def Anderson4D.r324DetTailless (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) : ℝ

r324DetHeadless with the tail leg deleted as well: the last chain edge is dropped and the difference factors are restricted to the pairs that do not reach the tail slot. Every remaining factor reads the assembled tuple only at the internal slots 1, …, m.

Equations

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

theorem Anderson4D.r324DetTailless_congr (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) {xt xt' : Fin (m + 2) → T4} (h : ∀ (j : Fin (m + 2)), ↑j ≠ 0 → ↑j ≠ m + 1 → xt j = xt' j) : r324DetTailless ρ ε m κ xt = r324DetTailless ρ ε m κ xt'

The tail-free remainder reads neither the head slot 0 nor the tail slot m + 1.

The split

theorem Anderson4D.diffFactor_assemble_tail {m : ℕ} (hm : 0 < m) (x y : T4) (v : Fin m → T4) (p : Fin m × Fin m) (hp : ↑p.2 + 1 = m) : diffFactor (assemble x y v) p = greenFn (v (r324TailLastIdx hm) - y) - greenFn (v p.1 - y)

The difference factor of a tail pair is the tail leg.

theorem Anderson4D.r324DetHeadless_eq_tail_mul_tailless (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (x y : T4) (v : Fin m → T4) : r324DetHeadless ρ ε m κ (assemble x y v) = r324BetaTailKernel hm κ v y * r324DetTailless ρ ε m κ (assemble x y v)

The tail split. The headless integrand is the tail leg times a tail-free remainder; the tail leg is the only factor that sees the tail external point.

noncomputable def Anderson4D.r324DetTaillessV (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) (v : Fin m → T4) : ℝ

The tail-free remainder as a function of the internal variables alone.

Equations

• Anderson4D.r324DetTaillessV ρ ε m κ v = Anderson4D.r324DetTailless ρ ε m κ (Anderson4D.assemble 0 0 v)

theorem Anderson4D.r324DetTailless_assemble_eq (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) (x y : T4) (v : Fin m → T4) : r324DetTailless ρ ε m κ (assemble x y v) = r324DetTaillessV ρ ε m κ v

theorem Anderson4D.r324DetHeadless_eq_tail_mul_taillessV (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (x y : T4) (v : Fin m → T4) : r324DetHeadless ρ ε m κ (assemble x y v) = r324BetaTailKernel hm κ v y * r324DetTaillessV ρ ε m κ v

The tail split, in tail-free form.

The β-Fourier coefficient of the tail leg

theorem Anderson4D.charT4_point_zero (k : Z4) : charT4 k 0 = 1

instance Anderson4D.instIsNegInvariantVolumeT4 : MeasureTheory.volume.IsNegInvariant

theorem Anderson4D.integrable_greenFn_sub_left (u : T4) : MeasureTheory.Integrable (fun (y : T4) => greenFn (u - y)) paperMeasure

theorem Anderson4D.integral_charT4_mul_greenFn_sub_left (k : Z4) (u : T4) : ∫ (y : T4), charT4 k y * ↑(greenFn (u - y)) ∂paperMeasure = translatedGreenMode k u

The reversed Green mode. The Green kernel is a bona fide convolution kernel: harvesting a character against G(u - ·) gives the same translated mode as against G(· - u).

noncomputable def Anderson4D.r324BetaTailChar {m : ℕ} (β : Z4) (hm : 0 < m) (κ : PartialPairing (Fin m)) (v : Fin m → T4) : ℂ

The transported tail character. What the tail leg becomes once its β-harvest has been performed: the β character at the two candidate tail anchors, inside the internal integral. This is the object the central bracket is built from — the mode β now sits on the internal vertices, against the covariance symbols.

Equations

• Anderson4D.r324BetaTailChar β hm κ v = Anderson4D.charT4 β (v (Anderson4D.r324TailLastIdx hm)) - match Anderson4D.r324TailAnchor κ with | none => 0 | some b => Anderson4D.charT4 β (v b)

theorem Anderson4D.norm_r324BetaTailChar_le {m : ℕ} (β : Z4) (hm : 0 < m) (κ : PartialPairing (Fin m)) (v : Fin m → T4) : ‖r324BetaTailChar β hm κ v‖ ≤ 2

The transported tail character is a difference of at most two unimodular characters.

theorem Anderson4D.integrable_charT4_mul_greenFn_sub_left (k : Z4) (u : T4) : MeasureTheory.Integrable (fun (y : T4) => charT4 k y * ↑(greenFn (u - y))) paperMeasure

theorem Anderson4D.integrable_charT4_mul_r324BetaTailKernel {m : ℕ} (β : Z4) (hm : 0 < m) (κ : PartialPairing (Fin m)) (v : Fin m → T4) : MeasureTheory.Integrable (fun (y : T4) => charT4 β y * ↑(r324BetaTailKernel hm κ v y)) paperMeasure

theorem Anderson4D.integral_charT4_mul_r324BetaTailKernel {m : ℕ} (β : Z4) (hm : 0 < m) (κ : PartialPairing (Fin m)) (v : Fin m → T4) : ∫ (y : T4), charT4 β y * ↑(r324BetaTailKernel hm κ v y) ∂paperMeasure = ↑(paperSecondOrderModeDecay β) * r324BetaTailChar β hm κ v

The tail harvest. The β-Fourier coefficient of the tail leg is ⟨β⟩⁻² times the transported tail character — an identity: the whole second-order decay factors out and the entity-dependent anchor survives as a character, not as a constant 2.

The left copy: harvesting y

noncomputable def Anderson4D.r324BetaLeftTransported (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (β : Z4) (hm : 0 < m) (F : Finset (MomentContraction m)) (w : T4) (v : Fin (2 * m) → T4) : ℂ

The summed core after the two head Green edges and the left tail leg have been harvested: the left tail leg has become the transported character r324BetaTailChar, still inside the entity sum.

Equations

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

theorem Anderson4D.r324Beta_charY_pointwise (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (β : Z4) (hm : 0 < m) (F : Finset (MomentContraction m)) (y w : T4) (v : Fin (2 * m) → T4) : charT4 β y * ↑(r324CMDoubleHeadlessCore ρ ε m F y w v) = ∑ e ∈ F, charT4 β y * ↑(r324BetaTailKernel hm e.fst (fun (i : Fin m) => v (leftMomentIndex i)) y) * ↑((r324DetTaillessV ρ ε m e.fst fun (i : Fin m) => v (leftMomentIndex i)) * r324DetHeadless ρ ε m e.snd.fst (assemble w w fun (i : Fin m) => v (rightMomentIndex i)) * momentCrossCovarianceProduct ρ ε m e.fst e.snd.fst e.snd.snd v)

theorem Anderson4D.r324Beta_integrable_charY (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (β : Z4) (hm : 0 < m) (e : MomentContraction m) (w : T4) (v : Fin (2 * m) → T4) : MeasureTheory.Integrable (fun (y : T4) => charT4 β y * ↑(r324BetaTailKernel hm e.fst (fun (i : Fin m) => v (leftMomentIndex i)) y) * ↑((r324DetTaillessV ρ ε m e.fst fun (i : Fin m) => v (leftMomentIndex i)) * r324DetHeadless ρ ε m e.snd.fst (assemble w w fun (i : Fin m) => v (rightMomentIndex i)) * momentCrossCovarianceProduct ρ ε m e.fst e.snd.fst e.snd.snd v)) paperMeasure

theorem Anderson4D.r324TailBetaCoefficient_eq (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (β : Z4) (hm : 0 < m) (F : Finset (MomentContraction m)) (s : T4 × (Fin (2 * m) → T4)) : r324TailBetaCoefficient ρ ε m β F s = ↑(paperSecondOrderModeDecay β) * r324BetaLeftTransported ρ ε m β hm F s.1 s.2

The left tail harvest. ⟨β⟩⁻² factors out of the entity sum exactly.

The right copy: harvesting w

noncomputable def Anderson4D.r324BetaQuadCore (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (β : Z4) (hm : 0 < m) (F : Finset (MomentContraction m)) (v : Fin (2 * m) → T4) : ℂ

The tail-amputated core with all four external modes transported inside. Both head Green edges and both tail legs have been harvested; what is left of every entity is the product of its two tail-free remainders and its internal covariance product, weighted by the two transported tail characters. The entity sum is still inside.

Equations

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

theorem Anderson4D.r324Beta_charW_pointwise (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (β : Z4) (hm : 0 < m) (F : Finset (MomentContraction m)) (w : T4) (v : Fin (2 * m) → T4) : charT4 (-β) w * r324BetaLeftTransported ρ ε m β hm F w v = ∑ e ∈ F, charT4 (-β) w * ↑(r324BetaTailKernel hm e.snd.fst (fun (i : Fin m) => v (rightMomentIndex i)) w) * ((r324BetaTailChar β hm e.fst fun (i : Fin m) => v (leftMomentIndex i)) * ↑(((r324DetTaillessV ρ ε m e.fst fun (i : Fin m) => v (leftMomentIndex i)) * r324DetTaillessV ρ ε m e.snd.fst fun (i : Fin m) => v (rightMomentIndex i)) * momentCrossCovarianceProduct ρ ε m e.fst e.snd.fst e.snd.snd v))

theorem Anderson4D.r324Beta_integral_w (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (β : Z4) (hm : 0 < m) (F : Finset (MomentContraction m)) (v : Fin (2 * m) → T4) : ∫ (w : T4), charT4 (-β) w * r324BetaLeftTransported ρ ε m β hm F w v ∂paperMeasure = ↑(paperSecondOrderModeDecay β) * r324BetaQuadCore ρ ε m β hm F v

The right tail harvest. The second ⟨β⟩⁻² factors out of the entity sum exactly.

The quadruple harvest

noncomputable def Anderson4D.r324BetaQuadHarvest (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (hm : 0 < m) (F : Finset (MomentContraction m)) : ℂ

What clause B reduces to on the tail region. All four external characters have been harvested; the two head modes α sit transported at the internal head anchors and the two tail modes β sit transported at the internal tail anchors, all inside the internal integral and with the entity sum inside as well. The only decay still to be produced is the central bracket at the conserved mode α + β.

Equations

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

theorem Anderson4D.r324Beta_integrable_headHarvestIntegrand (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (hm : 0 < m) (α β : Z4) (F : Finset (MomentContraction m)) : MeasureTheory.Integrable (fun (s : T4 × (Fin (2 * m) → T4)) => charT4 α (s.2 (leftMomentIndex ⟨0, hm⟩)) * charT4 (-α) (s.2 (rightMomentIndex ⟨0, hm⟩)) * charT4 (-β) s.1 * r324TailBetaCoefficient ρ ε m β F s) (r324TailInnerMeasure m)

theorem Anderson4D.r324Beta_headHarvest_eq (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (hm : 0 < m) (α β : Z4) (F : Finset (MomentContraction m)) : r324TailHeadHarvest ρ ε m α β F ⟨0, hm⟩ = ↑(paperFourthOrderModeDecay β) * r324BetaQuadHarvest ρ ε m α β hm F

The ⟨β⟩⁻⁴ harvest, exactly. The head-harvested integral is the fourth-order mode decay at β times the quadruple harvest. Like the head harvest this is an identity, so the remaining decay still multiplies on: no cancellation has been spent, and the entity sum has never left the integrand.

The central bracket

def Anderson4D.R324BetaQuadBracketLedger (ρ : SmoothCutoff) (K : ℝ) : Prop

The central-bracket ledger. Everything the four external harvests leave: with all four external characters transported to internal anchors (α at v_{L,0}, -α at v_{R,0}, β and -β at the two tail anchors) and integrated against the tail-amputated core — entity sum inside — produce the eighth-order decay at the conserved mode α + β.

This is the exact residue of clause B on the tail region: by r324Beta_headHarvest_eq together with r324Tail_sum_eq_alphaDecay_mul_headHarvest the clause-B left-hand side equals ⟨α⟩⁻⁴ ⟨β⟩⁻⁴ · r324BetaQuadHarvest, both factorizations being identities.

Equations

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

theorem Anderson4D.R324BracketTailResidual_of_quadBracket {ρ : SmoothCutoff} {K : ℝ} (h : R324BetaQuadBracketLedger ρ K) : R324BracketTailResidual ρ K

The tail residual from the central-bracket ledger. The ⟨β⟩⁻⁴ harvest is an identity, so the two decays multiply.

theorem Anderson4D.R324CappedBracketDensityLedger_of_quadBracket {ρ : SmoothCutoff} {K : ℝ} (hK : 0 ≤ K) (hA : R324CappedDensityLedger ρ K) (h : R324BetaQuadBracketLedger ρ K) : R324CappedBracketDensityLedger ρ K

Clause B from clause A and the central-bracket ledger.

theorem Anderson4D.R324CappedCrossLedgerStrong_of_quadBracket {ρ : SmoothCutoff} {K : ℝ} (hK : 0 ≤ K) (hA : R324CappedDensityLedger ρ K) (h : R324BetaQuadBracketLedger ρ K) : R324CappedCrossLedgerStrong ρ K

The strong capped ledger from the grading and central-bracket estimates. The tail estimate is reduced to one statement about the tail-amputated core.

theorem Anderson4D.r324Beta_sum_eq_endpointDecays_mul_quadHarvest (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (hm : 0 < m) (α β : Z4) (F : Finset (MomentContraction m)) : ∑ e ∈ F, deterministicMomentContractionTerm ρ ε m α β e = ↑(paperFourthOrderModeDecay α * paperFourthOrderModeDecay β) * r324BetaQuadHarvest ρ ε m α β hm F

The full endpoint factorization. Both endpoint decays come out of clause B as an identity, with the entity sum never leaving the integrand.

theorem Anderson4D.R324BetaQuadBracketLedger_of_tailPaperLedger {ρ : SmoothCutoff} {K : ℝ} (h : ∀ {ε : ℝ} (m : ℕ) (α β : Z4), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → 2 ≤ m → m ≤ truncOrder ε → r324CMBracketWeight ε α β ≤ 1 → ∀ (F : Finset (MomentContraction m)), ‖∑ e ∈ F, deterministicMomentContractionTerm ρ ε m α β e‖ ≤ K ^ m * |Real.log ε| ^ (m - 1) * r324BracketPaperWeight α β) : R324BetaQuadBracketLedger ρ K

The central-bracket ledger is not an over-assumption. It is implied by the ε-free tail ledger it is used to prove: the two endpoint decays divide out exactly. So R324BetaQuadBracketLedger measures precisely the central bracket and nothing more.

The modulus fallback

theorem Anderson4D.norm_r324BetaQuadHarvest_le (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (α β : Z4) (hm : 0 < m) (F : Finset (MomentContraction m)) : ‖r324BetaQuadHarvest ρ ε m α β hm F‖ ≤ ∫ (v : Fin (2 * m) → T4), ‖r324BetaQuadCore ρ ε m β hm F v‖ ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure

Dropping the two transported head characters costs only the triangle inequality — but it also destroys the central bracket, so this route proves clause B without the ⟨‖α+β‖⟩⁻⁸ factor. It is recorded to make the split precise: an L¹ ledger for the tail-amputated core r324BetaQuadCore is exactly what is not enough, and the gap is exactly the central bracket.