Difference-retaining order-two middle estimate

R324InteriorTransport establishes that the raw interior-core budget is unavailable at m = 2: the endpoint-first split sup-normalizes the terminal chain edges and discards the renormalizing difference factors, leaving the divergent raw block mass (∫ G η_ε)² ≳ ε⁻⁴. This file retains those factors at order two for the corresponding schedule:

• r324RefinedPhysicalIntegral_twoBlock_eq — the two-block refined physical integral factors exactly into its two independent halves, each of which still carries its difference factor (detIntegrand keeps diffFactor; nothing is sup-normalized);
• exists_norm_r324TwoBlockHalfIntegral_le — each half is bounded by a constant Q uniform in ρ, ε, and both external frequencies: the difference factor is integrated jointly with the block (integral_pi_twoBlock_u), parity kills the first-order phase term, and the quadratic cosine defect (1/2)|β|² ∫|z̃|² G η_ε is exactly compensated by the boundary coefficient (1+|β|²)⁻¹;
• exists_r324TwoBlock_insertedMajorantBound — the middle estimate for that schedule: with the difference retained, the weighted two-block integral obeys the paper-scale inserted-majorant bound |λ_ε|⁴ ‖⋯‖ ≤ ∫ primitiveInsertedMajorant, with an ε- and mode-uniform primitive constant. (Ledger: |λ_ε|⁴ Q² = λ⁴ Q²/log²ε against the majorant's (C₀λ)⁴/|log ε|; one full power of |log ε| to spare, so no ε-power and no log-power is borrowed.)
• r324RefinedInsertedMajorantBound_two_of_complement — the composed order-two middle-estimate interface R324RefinedInsertedMajorantBound (and hence the uniform branch MomentRefinedIntegratedReductionOutputAt of the final deterministic closure) is recovered once the remaining, difference-free order-two fibres (the cross-pairing schedules, which have no within-half extraction and hence no interior divergence mechanism) are bounded.

The two-block schedule is the distinguished order-two obstruction; the cross-pairing complement hypothesis concerns schedules whose within-half pairings are trivial, i.e. paper §4.2 Step 3 cross-cut estimates rather than the Step 2 extraction.

The cross covariance of the two-block contraction is empty

theorem Anderson4D.momentCrossCovarianceProduct_twoBlock (ρ : SmoothCutoff) (ε : ℝ) (v : Fin (2 * 2) → T4) : momentCrossCovarianceProduct ρ ε 2 pairingFinTwo pairingFinTwo (Equiv.refl ↥pairingFinTwo.singles) v = 1

Exact two-half factorization of the two-block physical integral

theorem Anderson4D.r324RefinedPhysicalIntegral_twoBlock_eq (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (α β : Z4) : r324RefinedPhysicalIntegral ρ ε 2 α β twoBlockScheduleIndex = r324TwoBlockHalfIntegral ρ ε α β * r324TwoBlockHalfIntegral ρ ε (-α) (-β)

The two-block refined physical integral factors exactly. Both factors are complete halves with their renormalizing difference factors still in place: the identity contains no interior/endpoint split and no sup-normalization.

Uniform two-block half bound

theorem Anderson4D.exists_norm_r324TwoBlockHalfIntegral_le : ∃ (Q : ℝ), 0 < Q ∧ ∀ (ρ : SmoothCutoff) {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ (a b : Z4), ‖r324TwoBlockHalfIntegral ρ ε a b‖ ≤ Q

Mode- and scale-uniform half bound. The constant is uniform in the cutoff, the scale, and both external frequencies: the boundary coefficient (1+|b|²)⁻¹ absorbs the quadratic cosine defect (1/2)|b|² exactly, leaving the ε-uniform quadratic block mass.

The order-two middle estimate

theorem Anderson4D.exists_r324TwoBlock_insertedMajorantBound : ∃ (C₀ : ℝ), 0 < C₀ ∧ ∀ (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (α β : Z4), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → |lamEps lam ε| ^ (2 * 2) * ‖r324RefinedPhysicalIntegral ρ ε 2 α β twoBlockScheduleIndex‖ ≤ ∫ (z : T4), primitiveInsertedMajorant C₀ lam ε 1 2 z ∂paperMeasure

The difference-retaining middle estimate for the two-block schedule. With the renormalizing difference factors integrated jointly with their blocks, the weighted two-block refined physical integral obeys the paper-scale inserted-majorant bound — the exact inequality shape demanded by refined_bound at m = 2 — with a primitive constant uniform in the cutoff, coupling, scale, and modes.

Ledger: |λ_ε|⁴ ‖⋯‖ ≤ λ⁴ Q²/|log ε|², while the inserted majorant integrates to at least (C₀λ)⁴/|log ε|; the estimate closes with one full power of |log ε| to spare and no ε-dependence at all, against the interior-core majorant whose mass is ≳ ε⁻⁴.

Composition with the cross-pairing complement

theorem Anderson4D.exists_r324RefinedInsertedMajorantBound_two_of_complement : ∃ (C₀ : ℝ), 0 < C₀ ∧ ∀ (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (α β : Z4), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → (∀ (p : R324RefinedScheduleIndex 2), p ≠ twoBlockScheduleIndex → |lamEps lam ε| ^ (2 * 2) * ‖r324RefinedPhysicalIntegral ρ ε 2 α β p‖ ≤ ∫ (z : T4), primitiveInsertedMajorant C₀ lam ε 1 2 z ∂paperMeasure) → R324RefinedInsertedMajorantBound ρ lam ε 2 α β C₀ 1

Order-two middle estimate from the difference-retaining schedule and the cross-pairing complement. The two-block schedule — the unique order-two case where the interior-core budget fails — is discharged unconditionally by the difference-retaining estimate; the middle estimate R324RefinedInsertedMajorantBound at order two then reduces to the complement schedules, all of which have trivial within-half pairings (no extraction, no difference factor, no interior-core mechanism): they are paper §4.2 Step 3 cross-cut objects.

theorem Anderson4D.exists_momentRefinedIntegratedReductionOutputAt_two_of_complement : ∃ (C₀ : ℝ), 0 < C₀ ∧ ∀ (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (α β : Z4), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → (∀ (p : R324RefinedScheduleIndex 2), p ≠ twoBlockScheduleIndex → |lamEps lam ε| ^ (2 * 2) * ‖r324RefinedPhysicalIntegral ρ ε 2 α β p‖ ≤ ∫ (z : T4), primitiveInsertedMajorant C₀ lam ε 1 2 z ∂paperMeasure) → MomentRefinedIntegratedReductionOutputAt ρ lam ε 2 α β C₀ 1

The uniform branch at order two. Under the cross-pairing complement hypothesis, the uniform estimate MomentRefinedIntegratedReductionOutputAt of exists_deterministicMoment_paper_bound_of_refinedIntegrated_and_countable holds at order two with the difference-retaining constant.