The order-one contraction bound for the R-324 uniform branch

Order one has exactly one contraction entity: no within-half pair can exist on a one-point half, so both partial pairings are trivial and the cross bijection is unique. Its physical integral is the two complete one-vertex half chains joined by a single cross covariance. All four boundary Green edges peel at unit paper mass and the cross covariance has mollifier mass at most one, so the term is bounded by the paper volume alone — no logarithm and no window is spent, exactly the K^1 |log ε|^0 entry of the general peel ledger.

The unique order-one contraction

def Anderson4D.oneCrossContraction : MomentContraction 1

Both halves unpaired, singles matched by the unique bijection.

Equations

• Anderson4D.oneCrossContraction = ⟨Anderson4D.PartialPairing.id, ⟨Anderson4D.PartialPairing.id, Equiv.refl ↥Anderson4D.PartialPairing.id.singles⟩⟩

theorem Anderson4D.partialPairing_finOne_eq (κ : PartialPairing (Fin 1)) : κ = PartialPairing.id

A one-point half admits only the trivial pairing.

theorem Anderson4D.momentContraction_one_eq (e : MomentContraction 1) : e = oneCrossContraction

The order-one contraction entity is unique.

theorem Anderson4D.fintype_card_momentContraction_one : Fintype.card (MomentContraction 1) = 1

Order one has exactly one contraction entity.

theorem Anderson4D.extract_id_finOne : extract PartialPairing.id = []

Nothing is extracted from the trivial pairing of a one-point half.

theorem Anderson4D.detIntegrand_one_id_assemble (ρ : SmoothCutoff) (ε : ℝ) (x y : T4) (u : Fin 1 → T4) : detIntegrand ρ ε 1 PartialPairing.id (assemble x y u) = greenFn (x - u 0) * greenFn (u 0 - y)

Closed form of the order-one trivial-pairing integrand: the plain two-edge chain.

theorem Anderson4D.momentCrossCovarianceProduct_one (ρ : SmoothCutoff) (ε : ℝ) (π : ↥PartialPairing.id.singles ≃ ↥PartialPairing.id.singles) (v : Fin (2 * 1) → T4) : momentCrossCovarianceProduct ρ ε 1 PartialPairing.id PartialPairing.id π v = ρ.etaEpsT4 ε (v (leftMomentIndex 0) - v (rightMomentIndex 0))

The order-one cross covariance: exactly one factor.

The order-one physical density

noncomputable def Anderson4D.r324OneCoreDensity (ρ : SmoothCutoff) (ε : ℝ) (v : Fin (2 * 1) → T4) : ℝ

Internal core: the single cross covariance.

Equations

• Anderson4D.r324OneCoreDensity ρ ε v = ρ.etaEpsT4 ε (v (Anderson4D.leftMomentIndex 0) - v (Anderson4D.rightMomentIndex 0))

noncomputable def Anderson4D.r324OnePhysicalDensity (ρ : SmoothCutoff) (ε : ℝ) (p : R324PhysicalPoint 1) : ℝ

The full order-one physical density in peel-ready nested form: each external variable multiplies one unit-mass boundary Green edge.

Equations

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

theorem Anderson4D.norm_r324Flatten_one_eq (ρ : SmoothCutoff) (ε : ℝ) (α β : Z4) (p : R324PhysicalPoint 1) : ‖r324Flatten (deterministicMomentIntegrand ρ ε 1 α β oneCrossContraction.fst oneCrossContraction.snd.fst oneCrossContraction.snd.snd) p‖ = r324OnePhysicalDensity ρ ε p

The norm of the unique order-one flat integrand is the order-one physical density.

theorem Anderson4D.integral_flat_r324OnePhysicalDensity (ρ : SmoothCutoff) (ε : ℝ) (hint : MeasureTheory.Integrable (r324OnePhysicalDensity ρ ε) (r324PhysicalMeasure 1)) : ∫ (p : R324PhysicalPoint 1), r324OnePhysicalDensity ρ ε p ∂r324PhysicalMeasure 1 = ∫ (v : Fin (2 * 1) → T4), r324OneCoreDensity ρ ε v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * 1)) => paperMeasure

Exact peeling of the four external variables. Each boundary Green edge has unit paper mass; the flat order-one density integrates to the internal core integral.

theorem Anderson4D.integrable_r324OneCoreDensity_of_flat (ρ : SmoothCutoff) (ε : ℝ) (hint : MeasureTheory.Integrable (r324OnePhysicalDensity ρ ε) (r324PhysicalMeasure 1)) : MeasureTheory.Integrable (r324OneCoreDensity ρ ε) (MeasureTheory.Measure.pi fun (x : Fin (2 * 1)) => paperMeasure)

The order-one core inherits integrability from the flat density.

The core mass bound

theorem Anderson4D.integral_r324OneCoreDensity_le (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hcore : MeasureTheory.Integrable (r324OneCoreDensity ρ ε) (MeasureTheory.Measure.pi fun (x : Fin (2 * 1)) => paperMeasure)) : (∫ (v : Fin (2 * 1) → T4), r324OneCoreDensity ρ ε v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * 1)) => paperMeasure) ≤ (2 * Real.pi) ^ dim

Unit mollifier mass bound for the order-one core. One cross covariance integrates to at most one over its first variable; the remaining variable contributes the paper volume.

The order-one contraction bound

theorem Anderson4D.norm_deterministicMomentContractionTerm_one_le (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (α β : Z4) (e : MomentContraction 1) : ‖deterministicMomentContractionTerm ρ ε 1 α β e‖ ≤ (2 * Real.pi) ^ dim

Every order-one contraction term is bounded by the paper volume. No logarithm is spent: the four boundary Green edges peel at unit mass and the single cross covariance has mass at most one.