Closure of the order-two complement schedules

The difference-retaining estimate discharges the two-block schedule (the unique order-two witness of the interior-core nonexistence theorem) and reduces the order-two uniform branch to the complement schedules. This file closes that complement and composes the unconditional order-two uniform-branch output.

• momentContraction_two_classify — an order-two contraction is the two-block full swap or a cross matching ⟨idPairingFinTwo, idPairingFinTwo, π⟩; consequently every complement refined fibre consists of cross contractions only (mem_momentRefinedContractionFiber_complement);
• exists_r324ComplementSchedule_insertedMajorantBound — the complement middle estimate: on every schedule other than the two-block one, the weighted refined physical integral obeys the paper-scale inserted-majorant bound. Ledger: |λ_ε|⁴ · 3·C_W·|log ε| = 3 C_W λ⁴/|log ε| against the majorant's (C₀λ)⁴/|log ε|: the diagonal window Σ_k ‖ρ̂(εk)‖⁴⟨k⟩⁻⁴ ≲ |log ε| spends exactly the one logarithm that λ_ε⁴ = λ⁴/log²ε affords;
• exists_r324RefinedInsertedMajorantBound_two, exists_momentRefinedIntegratedReductionOutputAt_two — the unconditional order-two middle estimate and uniform-branch output, combining the proved difference-retaining two-block estimate with the complement bound at a common primitive constant.

The primitive constant depends on the mollifier ρ (quantifier order ∀ ρ, ∃ C₀): the complement window is supported on |k| ≲ (radius·ε)⁻¹, so its logarithm degrades like |log radius| as the mollifier concentrates; a ρ-uniform constant is impossible for the cross-cut fibres, in contrast with the two-block estimate.

Order-two contraction classification

theorem Anderson4D.momentContraction_two_classify (e : MomentContraction 2) : e = twoBlockContraction ∨ ∃ (π : ↥idPairingFinTwo.singles ≃ ↥idPairingFinTwo.singles), e = ⟨idPairingFinTwo, ⟨idPairingFinTwo, π⟩⟩

An order-two contraction entity is the two-block full swap or a trivial-pairing cross matching.

theorem Anderson4D.mem_momentRefinedContractionFiber_complement {p : R324RefinedScheduleIndex 2} (hp : p ≠ twoBlockScheduleIndex) {e : MomentContraction 2} (he : e ∈ momentRefinedContractionFiber 2 ↑p.fst ↑p.snd) : ∃ (π : ↥idPairingFinTwo.singles ≃ ↥idPairingFinTwo.singles), e = ⟨idPairingFinTwo, ⟨idPairingFinTwo, π⟩⟩

Every contraction in a complement refined fibre is a cross matching: the two-block entity forces its schedule index.

The complement middle estimate

theorem Anderson4D.fintype_card_momentContraction_two : Fintype.card (MomentContraction 2) = 3

The order-two contraction entities number exactly three.

theorem Anderson4D.exists_r324ComplementSchedule_insertedMajorantBound (ρ : SmoothCutoff) : ∃ (C₁ : ℝ), 0 < C₁ ∧ ∀ (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

The complement middle estimate. On every refined schedule other than the two-block one, the weighted physical integral obeys the paper-scale inserted-majorant bound: the cross fibres carry no extraction and no difference factor, and their diagonal window spends one logarithm against the two afforded by λ_ε⁴.

Majorant monotonicity in the primitive constant

theorem Anderson4D.primitiveInsertedMajorant_mono_const {C C' : ℝ} (hC : 0 ≤ C) (hCC' : C ≤ C') (lam ε supportConstant : ℝ) (n : ℕ) (z : T4) : primitiveInsertedMajorant C lam ε supportConstant n z ≤ primitiveInsertedMajorant C' lam ε supportConstant n z

theorem Anderson4D.integral_primitiveInsertedMajorant_mono_const {C C' : ℝ} (hC : 0 ≤ C) (hCC' : C ≤ C') (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (supportConstant : ℝ) (n : ℕ) : ∫ (z : T4), primitiveInsertedMajorant C lam ε supportConstant n z ∂paperMeasure ≤ ∫ (z : T4), primitiveInsertedMajorant C' lam ε supportConstant n z ∂paperMeasure

The unconditional order-two middle estimate

theorem Anderson4D.exists_r324RefinedInsertedMajorantBound_two (ρ : SmoothCutoff) : ∃ (C₀ : ℝ), 0 < C₀ ∧ ∀ (lam : ℝ) {ε : ℝ} (α β : Z4), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → R324RefinedInsertedMajorantBound ρ lam ε 2 α β C₀ 1

The unconditional order-two middle estimate. The two-block schedule is discharged by the proved difference-retaining estimate and every complement schedule by the cross-cut window bound, at the common primitive constant max.

theorem Anderson4D.exists_momentRefinedIntegratedReductionOutputAt_two (ρ : SmoothCutoff) : ∃ (C₀ : ℝ), 0 < C₀ ∧ ∀ (lam : ℝ) {ε : ℝ} (α β : Z4), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → MomentRefinedIntegratedReductionOutputAt ρ lam ε 2 α β C₀ 1

The unconditional order-two uniform-branch output. The property MomentRefinedIntegratedReductionOutputAt holds at order two, with a primitive constant depending only on the mollifier — no complement hypothesis remains.