The central bracket: anchor resolution of the quadruple harvest

R324BetaQuadBracketLedger is the residual tail-region estimate: tail region: the quadruple harvest r324BetaQuadHarvest, in which all four external characters have been transported to internal anchors, must carry the ε-free eighth-order bracket ⟨‖freq (α+β)‖⟩⁻⁸ at the conserved mode.

This file resolves the two transported tail characters — which are differences charT4 β (v_{m-1}) - charT4 β (v_a) whose anchor a depends on the entity — into four anchor-resolved harvests in which every character sits at a fixed internal coordinate slot, outside the entity sum. That is exactly the shape the general collapse machine consumes: one character per internal coordinate.

The corresponding analytic estimate is named R324CentralAnchorLedger.

Anchor-indexed characters

noncomputable def Anderson4D.r324CentralAnchorChar {m : ℕ} (β : Z4) (a : Option (Fin m)) (u : Fin m → T4) : ℂ

The character of mode β at an optional internal anchor: 0 at none. Both terms of r324BetaTailChar are of this form, so the transported tail character is literally a difference of two of them.

Equations

• Anderson4D.r324CentralAnchorChar β none u = 0
• Anderson4D.r324CentralAnchorChar β (some b) u = Anderson4D.charT4 β (u b)

theorem Anderson4D.norm_r324CentralAnchorChar_le {m : ℕ} (β : Z4) (a : Option (Fin m)) (u : Fin m → T4) : ‖r324CentralAnchorChar β a u‖ ≤ 1

theorem Anderson4D.r324BetaTailChar_eq_anchorChars {m : ℕ} (β : Z4) (hm : 0 < m) (κ : PartialPairing (Fin m)) (v : Fin m → T4) : r324BetaTailChar β hm κ v = r324CentralAnchorChar β (some (r324TailLastIdx hm)) v - r324CentralAnchorChar β (r324TailAnchor κ) v

The transported tail character is an anchor difference.

The anchor-resolved harvest

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

The anchor-resolved integrand. All four external characters sit at fixed internal coordinate slots — α at the left head anchor, -α at the right head anchor, β at the left tail slot aL e and -β at the right tail slot aR e — multiplying the character-free real core (two tailless chain products and the internal covariance product). The anchor slots are allowed to depend on the entity, which is exactly what the entity-dependent tail shortcut needs, and is harmless for the collapse machine because it consumes one entity at a time.

Equations

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

noncomputable def Anderson4D.r324CentralAnchorHarvest (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (hm : 0 < m) (F : Finset (MomentContraction m)) (aL aR : MomentContraction m → Option (Fin m)) : ℂ

The anchor-resolved harvest: the internal integral of the anchor-resolved integrand.

Equations

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

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

The central-anchor ledger. The analytic residue of clause B after anchor resolution: on the tail region every anchor-resolved harvest is integrable and carries the ε-free central bracket at the conserved mode α + β.

Compared with R324BetaQuadBracketLedger this is a statement about a plain four-character Fourier coefficient of a real core — no differences, no entity-dependent characters — i.e. precisely the input format of the general collapse machine (r324Col_piChain_integral): one character per internal coordinate, with the conserved mode α + β routed through the two head anchors.

Equations

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

Resolving the quadruple harvest into four anchor harvests

def Anderson4D.r324CentralLastAnchor {m : ℕ} (hm : 0 < m) : MomentContraction m → Option (Fin m)

The constant "tail slot" anchor assignment.

Equations

• Anderson4D.r324CentralLastAnchor hm x✝ = some (Anderson4D.r324TailLastIdx hm)

def Anderson4D.r324CentralLeftAnchor {m : ℕ} : MomentContraction m → Option (Fin m)

The left shortcut anchor assignment.

Equations

• Anderson4D.r324CentralLeftAnchor e = Anderson4D.r324TailAnchor e.fst

def Anderson4D.r324CentralRightAnchor {m : ℕ} : MomentContraction m → Option (Fin m)

The right shortcut anchor assignment.

Equations

• Anderson4D.r324CentralRightAnchor e = Anderson4D.r324TailAnchor e.snd.fst

theorem Anderson4D.r324CentralAnchor_integrand_pointwise (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (α β : Z4) (hm : 0 < m) (F : Finset (MomentContraction m)) (v : Fin (2 * m) → T4) : charT4 α (v (leftMomentIndex ⟨0, hm⟩)) * charT4 (-α) (v (rightMomentIndex ⟨0, hm⟩)) * r324BetaQuadCore ρ ε m β hm F v = r324CentralAnchorIntegrand ρ ε m α β hm F (r324CentralLastAnchor hm) (r324CentralLastAnchor hm) v - r324CentralAnchorIntegrand ρ ε m α β hm F (r324CentralLastAnchor hm) r324CentralRightAnchor v - r324CentralAnchorIntegrand ρ ε m α β hm F r324CentralLeftAnchor (r324CentralLastAnchor hm) v + r324CentralAnchorIntegrand ρ ε m α β hm F r324CentralLeftAnchor r324CentralRightAnchor v

Anchor resolution, pointwise. Expanding the two transported tail characters as anchor differences splits the quadruple-harvest integrand into the four anchor-resolved integrands with alternating signs.

theorem Anderson4D.r324BetaQuadHarvest_eq_anchorCombination (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (α β : Z4) (hm : 0 < m) (F : Finset (MomentContraction m)) (h₁ : MeasureTheory.Integrable (r324CentralAnchorIntegrand ρ ε m α β hm F (r324CentralLastAnchor hm) (r324CentralLastAnchor hm)) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)) (h₂ : MeasureTheory.Integrable (r324CentralAnchorIntegrand ρ ε m α β hm F (r324CentralLastAnchor hm) r324CentralRightAnchor) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)) (h₃ : MeasureTheory.Integrable (r324CentralAnchorIntegrand ρ ε m α β hm F r324CentralLeftAnchor (r324CentralLastAnchor hm)) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)) (h₄ : MeasureTheory.Integrable (r324CentralAnchorIntegrand ρ ε m α β hm F r324CentralLeftAnchor r324CentralRightAnchor) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)) : r324BetaQuadHarvest ρ ε m α β hm F = r324CentralAnchorHarvest ρ ε m α β hm F (r324CentralLastAnchor hm) (r324CentralLastAnchor hm) - r324CentralAnchorHarvest ρ ε m α β hm F (r324CentralLastAnchor hm) r324CentralRightAnchor - r324CentralAnchorHarvest ρ ε m α β hm F r324CentralLeftAnchor (r324CentralLastAnchor hm) + r324CentralAnchorHarvest ρ ε m α β hm F r324CentralLeftAnchor r324CentralRightAnchor

Anchor resolution of the quadruple harvest. Given integrability of the four anchor-resolved integrands, the quadruple harvest is their alternating sum.

The central bracket from the anchor ledger

theorem Anderson4D.R324BetaQuadBracketLedger_of_centralAnchor {ρ : SmoothCutoff} {K : ℝ} (hK : 0 ≤ K) (h : R324CentralAnchorLedger ρ K) : R324BetaQuadBracketLedger ρ (4 * K)

The central bracket, from anchor resolution. The four anchor harvests cost a factor 4, absorbed into the base constant.

Which mechanism can produce the ε-free central bracket

Two candidate mechanisms are ruled in / out here by explicit arithmetic.

theorem Anderson4D.paperModeNormSq_add_le (α β : Z4) : paperModeNormSq (α + β) ≤ 2 * paperModeNormSq α + 2 * paperModeNormSq β

theorem Anderson4D.r324Central_peetre (α β : Z4) : 1 + paperModeNormSq (α + β) ≤ 2 * ((1 + paperModeNormSq α) * (1 + paperModeNormSq β))

Peetre for the paper bracket.

theorem Anderson4D.r324Central_endpointTrade_sq (α β : Z4) : (paperFourthOrderModeDecay α * paperFourthOrderModeDecay β) ^ 2 ≤ 16 * eighthOrderFrequencyDecay ‖z4EuclideanFrequency (α + β)‖

The endpoint trade, exactly priced. The square of the two endpoint decays is dominated by the central bracket (up to 16), and the square is sharp: at β = α the bracket is genuinely smaller than the endpoint product itself. So buying the central bracket out of endpoint decay costs ⟨α⟩⁻⁸⟨β⟩⁻⁸ on the harvest, i.e. ⟨α⟩⁻¹²⟨β⟩⁻¹² on the entity sum — three endpoint harvests per external mode, where the four external Green legs supply only one each. The trade is therefore not the mechanism.

theorem Anderson4D.r324Central_epsScale_gap {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (x : ℝ) : ε⁻¹ ^ 8 * eighthOrderFrequencyDecay (ε * x) ≤ ε⁻¹ ^ 16 * eighthOrderFrequencyDecay x

The half-symbol route is ε⁻¹⁶ away from the target. The covariance symbols only see ε k, so the product bracket produced by r324HdetAssembly_prod_eighthDecay_le is ε⁻⁸⟨ε‖α+β‖⟩⁻⁸, which exceeds the ε-free bracket by exactly the endpoint loss squared. On the capped range m ≤ truncOrder ε the factor ε⁻¹⁶ = e^{16|log ε|} is not absorbable into K^m|log ε|^{m-1} (which only sees m ≤ |log ε| copies), so the half-symbol harvest cannot supply the ε-free central bracket either.

Where the ε-free bracket actually comes from

The proved chain collapse r324Col_piChain_integral evaluates a Green chain carrying one character per internal coordinate to r324ColPiProp n q times a character, and every factor of r324ColPiProp is a bracket ⟨·⟩⁻² at a suffix sum of the keys — ε-free, because it comes from a Green edge and not from a covariance symbol ρ̂(εk). With α at the head slot and β at the tail anchor slot, the head suffix sum is exactly the conserved mode α + β: the central bracket is produced by the Green edges downstream of the anchors. r324Central_epsScale_gap above shows that the competing half-symbol mechanism misses the ε-free target by ε⁻¹⁶.

def Anderson4D.r324CentralKeys (α β : Z4) (a : ℕ) : ℕ → Z4

The two-mode key assignment: α at the head slot, β at the tail anchor slot a, nothing elsewhere.

Equations

• Anderson4D.r324CentralKeys α β a j = if j = 0 then α else if j = a then β else 0

theorem Anderson4D.r324ColPartial_centralKeys (α β : Z4) {a n : ℕ} (ha : 0 < a) (han : a < n) : r324ColPartial (r324CentralKeys α β a) n = α + β

Momentum conservation at the head bracket. The collapse's head suffix sum for the two-mode key assignment is the conserved mode α + β, so the head factor of r324ColPiProp is the ε-free bracket ⟨α+β⟩⁻².

theorem Anderson4D.r324ColBrk_centralKeys (α β : Z4) {a n : ℕ} (ha : 0 < a) (han : a < n) : r324ColBrk (r324ColPartial (r324CentralKeys α β a) n) = paperSecondOrderModeDecay (α + β)

The head factor of the collapse product is the ε-free central bracket.