Clause B, factored: the anchor lattice series and the composed theorem

R324CentralAnchorLedger factors into two named inputs:

• a physical → lattice collapse for the anchor-resolved harvest (R324AnchorCollapseAt), the analogue of R324ColPhysicalCollapseAt in the character-free case; and
• a lattice budget with the central bracket (R324AnchorCentralBudget), the analogue of R324ColDoubledBudgetAt / R324ColGradedBudgetAt, except that the target carries the extra factor eighthOrderFrequencyDecay ‖freq (α+β)‖,

and then assembles everything downstream: clause B (R324CentralAnchorLedger), the quadruple bracket ledger, the strong capped cross ledger, and MainConditional.

The lattice series

The anchor-resolved harvest of one entity is a Green chain in each half carrying one character per internal coordinate, so r324Col_piChain_integral turns it into r324AnchorLatWeight: the proved symbol weight r324ColLatSym times the two anchor-resolved propagator products r324AnchorLatProp, whose brackets sit at the suffix sums computed in R324AnchorSuffixCount. With the external modes switched off it is the proved r324ColLatWeight (r324AnchorLatWeight_zero_modes), and the right half may be taken with the momenta un-negated because the propagator product is even (r324Anchor_latProp_neg).

The configuration sector is shifted: momentum conservation now reads ∑ᵢ qᵢ = -(α+β) (r324Anchor_key_sum_closed), not ∑ᵢ qᵢ = 0. That shift — and not any individual Green bracket — is where the conserved mode survives the collapse, which is exactly the content of R324AnchorSuffixCount.

The composed theorem

mainConditional_of_gradedBudget composes

R324CentralAnchorLedger → R324BetaQuadBracketLedger → R324CappedCrossLedgerStrong → MainConditional

with clause A, in the form the graded lattice budget delivers it (R324ColGradedBudgetAt ρ D m r324LayerSplitGrade, via an explicit bridge hypothesis).

The anchor-resolved lattice weight

noncomputable def Anderson4D.r324AnchorLatProp {m : ℕ} (α β : Z4) (a : ℕ) (q : Fin m → Z4) : ℝ

The propagator product of one anchor-resolved half chain: the suffix-sum brackets of r324AnchorKeys.

Equations

• Anderson4D.r324AnchorLatProp α β a q = Anderson4D.r324ColPiProp m (Anderson4D.r324AnchorKeys α β a (Anderson4D.r324ColExtend q))

theorem Anderson4D.r324AnchorLatProp_nonneg {m : ℕ} (α β : Z4) (a : ℕ) (q : Fin m → Z4) : 0 ≤ r324AnchorLatProp α β a q

theorem Anderson4D.r324Anchor_colPartial_neg (f : ℕ → Z4) (n : ℕ) : r324ColPartial (fun (j : ℕ) => -f j) n = -r324ColPartial f n

theorem Anderson4D.r324Anchor_colBrk_neg (b : Z4) : r324ColBrk (-b) = r324ColBrk b

theorem Anderson4D.r324Anchor_piProp_neg (n : ℕ) (f : ℕ → Z4) : (r324ColPiProp n fun (j : ℕ) => -f j) = r324ColPiProp n f

The propagator product is even. So the right half chain, whose momenta and external modes are the negatives of the left ones, has the same bracket product: the lattice weight below may be written with a single sign convention.

theorem Anderson4D.r324AnchorKeys_zero_modes (a : ℕ) (k : ℕ → Z4) : r324AnchorKeys 0 0 a k = k

noncomputable def Anderson4D.r324AnchorLatWeight (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (α β : Z4) (aL aR : ℕ) (τ : Equiv.Perm (Fin m)) (q : Fin m → Z4) : ℝ

The lattice summand of one anchor-resolved entity: the proved symbol weight against the two anchor-resolved propagator products, the left one in identity order and the right one in the order τ.

Equations

• Anderson4D.r324AnchorLatWeight ρ ε α β aL aR τ q = Anderson4D.r324ColLatSym ρ ε q * (Anderson4D.r324AnchorLatProp α β aL q * Anderson4D.r324AnchorLatProp α β aR (q ∘ ⇑τ))

theorem Anderson4D.r324AnchorLatWeight_nonneg (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (α β : Z4) (aL aR : ℕ) (τ : Equiv.Perm (Fin m)) (q : Fin m → Z4) : 0 ≤ r324AnchorLatWeight ρ ε α β aL aR τ q

theorem Anderson4D.r324AnchorLatProp_zero_modes {m : ℕ} (a : ℕ) (q : Fin m → Z4) : r324AnchorLatProp 0 0 a q = r324ColLatProp q

theorem Anderson4D.r324AnchorLatWeight_zero_modes (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (aL aR : ℕ) (τ : Equiv.Perm (Fin m)) (q : Fin m → Z4) : r324AnchorLatWeight ρ ε 0 0 aL aR τ q = r324ColLatWeight ρ ε τ q

Sanity: switching off the external modes returns the proved lattice weight. So r324AnchorLatWeight really is the proved r324ColLatWeight decorated with the two external insertions.

The shifted configuration sector

def Anderson4D.R324AnchorSector (m : ℕ) (γ : Z4) : Type

The shifted momentum sector. With α at the head slot and β at the anchor slot, momentum conservation on the closed chain reads ∑ᵢ qᵢ = -(α+β) (r324Anchor_key_sum_closed), not ∑ᵢ qᵢ = 0. At γ = 0 this is the proved R324ColZeroSum.

Equations

• Anderson4D.R324AnchorSector m γ = { q : Fin m → Anderson4D.Z4 // ∑ i : Fin m, q i = γ }

@[implicit_reducible]

instance Anderson4D.instCoeFunR324AnchorSectorForallFinZ4 (m : ℕ) (γ : Z4) : CoeFun (R324AnchorSector m γ) fun (x : R324AnchorSector m γ) => Fin m → Z4

Equations

• Anderson4D.instCoeFunR324AnchorSectorForallFinZ4 m γ = { coe := Subtype.val }

theorem Anderson4D.r324AnchorSector_zero (m : ℕ) : R324AnchorSector m 0 = R324ColZeroSum m

Anchor collapse inputs

def Anderson4D.R324AnchorCollapseAt (ρ : SmoothCutoff) (C : ℝ) (m : ℕ) : Prop

The anchor collapse, as a named Prop: the anchor-resolved integrand is integrable and its harvest is dominated by the anchor lattice series on the shifted sector. It is the character-bearing analogue of R324ColPhysicalCollapseAt: the four external characters ride along into the suffix sums, one character per internal coordinate, in the form supported by r324Col_piChain_integral.

The bound is stated with an existential pairing τ and existential anchor indices, because the entity set F is summed inside the harvest and the collapse machine consumes one entity at a time.

Equations

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

def Anderson4D.R324AnchorCentralBudget (ρ : SmoothCutoff) (D : ℝ) : Prop

The central lattice budget, as a named Prop: on the tail region the anchor lattice series over the shifted sector carries the ε-free eighth-order bracket at the conserved mode, on top of the usual D^m·|log ε|^{m-1} window budget.

This is the analytic content of clause B. R324AnchorSuffixCount shows it cannot be read off the Green brackets alone (the unique suffix sum carrying α+β freely is the head one, and conservation sets it to 0), that the ε-scaled symbols miss by ε⁻¹⁶ (r324Central_epsScale_gap), and that the endpoint trade needs ⟨α⟩⁻⁸⟨β⟩⁻⁸ where only ⟨α⟩⁻⁴⟨β⟩⁻⁴ is available (r324Central_endpointTrade_sq). What the sector does give for free is that the free keys must sum to -(α+β), so a large conserved mode forces a large key (r324Anchor_conserved_le_prod_keyBrackets); the remaining orders have to come from combining that constraint with the symbol decay uniformly in ε.

Equations

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

Clause B from the two inputs

theorem Anderson4D.R324CentralAnchorLedger_of_collapse_and_budget {ρ : SmoothCutoff} {C D : ℝ} (hC : 0 ≤ C) (hcol : ∀ (m : ℕ), R324AnchorCollapseAt ρ C m) (hbud : R324AnchorCentralBudget ρ D) : R324CentralAnchorLedger ρ (C * D)

Clause B, factored. The anchor collapse plus the central lattice budget give R324CentralAnchorLedger with the product constant, exactly as r324Col_entityBoundAt_of_collapse combines the proved R324ColPhysicalCollapseAt with R324ColDoubledBudgetAt.

Monotonicity of the two clauses in the budget constant

theorem Anderson4D.R324CappedDensityLedger_mono {ρ : SmoothCutoff} {K K' : ℝ} (hK : 0 ≤ K) (hKK : K ≤ K') (h : R324CappedDensityLedger ρ K) : R324CappedDensityLedger ρ K'

theorem Anderson4D.R324CentralAnchorLedger_mono {ρ : SmoothCutoff} {K K' : ℝ} (hK : 0 ≤ K) (hKK : K ≤ K') (h : R324CentralAnchorLedger ρ K) : R324CentralAnchorLedger ρ K'

The strong capped ledger and MainConditional

theorem Anderson4D.R324CappedCrossLedgerStrong_of_clauses {ρ : SmoothCutoff} {K : ℝ} (hK : 0 ≤ K) (hA : R324CappedDensityLedger ρ K) (hB : R324CentralAnchorLedger ρ K) : R324CappedCrossLedgerStrong ρ (4 * K)

The strong capped cross ledger from the grading and tail estimates. Clause A is R324CappedDensityLedger; clause B, on the tail region, is R324CentralAnchorLedger. They compose through R324BetaQuadBracketLedger_of_centralAnchor then R324CappedCrossLedgerStrong_of_quadBracket.

theorem Anderson4D.mainConditional_of_clauses {M : NoiseModel} {ρ : SmoothCutoff} {K : ℝ} (hK : 0 ≤ K) (hA : R324CappedDensityLedger ρ K) (hB : R324CentralAnchorLedger ρ K) : MainConditional M ρ

The two clauses close the theorem. Clause A plus the central-anchor clause B give MainConditional through mainConditional_of_cappedCrossLedgerStrong.

theorem Anderson4D.mainConditional_of_gradedBudget {M : NoiseModel} {ρ : SmoothCutoff} {C D E K : ℝ} (hK : 0 ≤ K) (hC : 0 ≤ C) (hE : 0 ≤ E) (hgrade : ∀ (m : ℕ), R324ColGradedBudgetAt ρ D m r324LayerSplitGrade) (hbridge : (∀ (m : ℕ), R324ColGradedBudgetAt ρ D m r324LayerSplitGrade) → R324CappedDensityLedger ρ K) (hcol : ∀ (m : ℕ), R324AnchorCollapseAt ρ C m) (hbud : R324AnchorCentralBudget ρ E) : MainConditional M ρ

Conditional assembly from the graded lattice budget and the two anchor inputs.

hbridge is clause A in the form the graded lattice budget delivers it; hcol and hbud are the two named inputs of clause B isolated above. Given those, MainConditional M ρ holds.