The full/full refined-fibre branch of R-324

Paper Section 4.2 Step 1 treats a contraction whose two within-copy pairings are full. Such a refined fibre has no cross-copy covariance and factors exactly into the two complete endpoint-signature half fibres. This file joins that exact factorization to the already proved numerical closure of Step 1.

The only hypotheses left below are the two literal R324Step1Reduction statements identifying the weighted half-fibre sums with outputs of the successive-removal argument. In particular, the conclusion has exactly the MomentRefinedIntegratedReductionData.refined_bound shape; no target-shaped analytic estimate is assumed. The product of the two Step-1 logarithmic gains is absorbed by the explicit lower bound for the integrated inserted majorant (with support constant 1).

Exact weighted factorization

theorem Anderson4D.norm_weighted_momentRefinedDeterministicTermSum_eq_fullFull_product (rho : SmoothCutoff) {eps : ℝ} (heps : 0 < eps) (heps1 : eps ≤ 1) (lam : ℝ) (m : ℕ) (alpha beta : Z4) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e0 : MomentContraction m) (he0 : e0 ∈ momentRefinedContractionFiber m s r) (hp : e0.fst.IsFull) (hm : e0.snd.fst.IsFull) : |lamEps lam eps| ^ (2 * m) * ‖momentRefinedDeterministicTermSum rho eps m alpha beta s r‖ = ‖↑(lamEps lam eps) ^ m * ∑ kp : ReductionEndpointFiberAt e0.fst, deterministicFullHalfIntegral rho eps m alpha beta ↑kp‖ * ‖↑(lamEps lam eps) ^ m * ∑ km : ReductionEndpointFiberAt e0.snd.fst, deterministicFullHalfIntegral rho eps m (-alpha) (-beta) ↑km‖

After the full/full finite-fibre factorization, the complete 2m coupling weight splits exactly into one m weight on each half.

Step 1 numerical closure in the refined-bound shape

theorem Anderson4D.exists_fullFull_refined_bound_of_step1Reductions (rho : SmoothCutoff) {removalConstant : ℝ} (hremovalConstant : 0 < removalConstant) : ∃ (primitiveConstant : ℝ), 0 < primitiveConstant ∧ ∀ (lam eps : ℝ) (m : ℕ) (alpha beta : Z4), 0 < lam → 0 < eps → eps ≤ 1 → 1 ≤ |Real.log eps| → 1 ≤ m → ∀ {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))}, ∀ e0 ∈ momentRefinedContractionFiber m s r, e0.fst.IsFull → e0.snd.fst.IsFull → R324Step1Reduction rho lam eps m alpha beta removalConstant (↑(lamEps lam eps) ^ m * ∑ kp : ReductionEndpointFiberAt e0.fst, deterministicFullHalfIntegral rho eps m alpha beta ↑kp) → R324Step1Reduction rho lam eps m (-alpha) (-beta) removalConstant (↑(lamEps lam eps) ^ m * ∑ km : ReductionEndpointFiberAt e0.snd.fst, deterministicFullHalfIntegral rho eps m (-alpha) (-beta) ↑km) → |lamEps lam eps| ^ (2 * m) * ‖momentRefinedDeterministicTermSum rho eps m alpha beta s r‖ ≤ ∫ (z : T4), primitiveInsertedMajorant primitiveConstant lam eps 1 m z ∂paperMeasure

Full/full branch of MomentRefinedIntegratedReductionData.refined_bound.

Assume the two weighted endpoint-fibre sums have been identified with the successive-removal output in the precise paper vocabulary R324Step1Reduction. The proved Step-1 theorem bounds each half by (C lambda)^m / |log eps|. Their product has two inverse logarithms, while the inserted majorant at support constant 1 needs only one; the paper range 1 ≤ |log eps| closes the comparison.

Thus the only missing full/full interface is the exact removal identification for each half. All finite-fibre, Fourier-integrability, and numerical-majorant bookkeeping is discharged here.