Integral-level residual prefixes for one R-324 half

This module packages an arbitrary genuine prefix of the analytic schedule. The state is generated only by prior absorb operations, and the remaining list is the literal schedule suffix. The one-step theorem below is therefore an integral transition between two reachable prefix states. It does not identify an original unintegrated production integrand pointwise with either state.

structure Anderson4D.R324WithinHalfResidualPrefix (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) : Type

A processed prefix and its exact analytic suffix.

• state : R324WithinHalfEdgeState m
• remaining : List (R322ExtractionStep m)
• schedule_eq : r322AnalyticSchedule pairing = self.state.processed ++ self.remaining
• reachable : R324WithinHalfStateReachable pairing ρ lam ε self.state

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.initial (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) : R324WithinHalfResidualPrefix ρ lam ε pairing

The all-Green state before any analytic block has been integrated.

Equations

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

def Anderson4D.R324WithinHalfResidualPrefix.remainingOrder {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) : ℕ

Exact perturbative order still present in the suffix.

Equations

• res.remainingOrder = (List.map (fun (step : Anderson4D.R322ExtractionStep m) => Anderson4D.residualBlockOrder step.2) res.remaining).sum

def Anderson4D.R324WithinHalfResidualPrefix.processedOrder {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) : ℕ

Exact perturbative order already absorbed into named edges.

Equations

• res.processedOrder = (List.map (fun (step : Anderson4D.R322ExtractionStep m) => Anderson4D.residualBlockOrder step.2) res.state.processed).sum

theorem Anderson4D.R324WithinHalfResidualPrefix.processedOrder_add_remainingOrder {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) : res.processedOrder + res.remainingOrder = (List.map (fun (step : R322ExtractionStep m) => residualBlockOrder step.2) (r322AnalyticSchedule pairing)).sum

The prefix/suffix order ledger is just the fixed schedule order, with no cardinality or asymptotic estimate.

def Anderson4D.R324WithinHalfResidualPrefix.headContext {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : R324WithinHalfStepContext pairing

Context for the literal head of an arbitrary remaining suffix.

Equations

• res.headContext head tail hremaining = { state := res.state, step := head, suffix := tail, schedule_eq := ⋯ }

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.afterHead {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : R324WithinHalfResidualPrefix ρ lam ε pairing

Residual data after the literal head has been integrated and absorbed.

Equations

• res.afterHead head tail hremaining = { state := (res.headContext head tail hremaining).absorb ρ lam ε, remaining := tail, schedule_eq := ⋯, reachable := ⋯ }

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.afterHead_remaining {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : (res.afterHead head tail hremaining).remaining = tail

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.afterHead_state {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : (res.afterHead head tail hremaining).state = (res.headContext head tail hremaining).absorb ρ lam ε

theorem Anderson4D.R324WithinHalfResidualPrefix.remainingOrder_head {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : res.remainingOrder = residualBlockOrder head.2 + (res.afterHead head tail hremaining).remainingOrder

theorem Anderson4D.R324WithinHalfResidualPrefix.lamEps_pow_integral_head_rawLocal_eq_afterHead {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (u : T4) (outer : ℂ) (hstandard : MeasureTheory.Integrable ((res.headContext head tail hremaining).localIntegrand ρ ε u) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder (res.headContext head tail hremaining).step.2)) => paperMeasure)) (hinternal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))), MeasureTheory.Integrable (fun (v : Fin (2 * residualBlockOrder head.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB) (res.headContext head tail hremaining).internalEdges (primitiveAssemble (residualBlockOrder head.2) ⋯ p.1 p.2 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure)) : (↑(lamEps lam ε) ^ (2 * residualBlockOrder head.2) * ∫ (t : Fin (2 * residualBlockOrder head.2) → T4), ↑((res.headContext head tail hremaining).rawLocalIntegrand ρ ε u t) * outer ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure) = ↑((res.afterHead head tail hremaining).state.edges (r324WithinHalfPredecessorSlot res.state head) u) * outer

Arbitrary-prefix integral transition.

For the actual head of a reachable schedule suffix, the honest raw local spatial integral updates exactly the predecessor edge of afterHead. The outer complex factor is fixed during this local integral, and the state change occurs only in the conclusion.

The genuine first-left selector after its arbitrary analytic prefix

theorem Anderson4D.exists_r324FirstLeftResidualPrefix {m : ℕ} (ρ : SmoothCutoff) (lam ε : ℝ) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : ∃ (pre : List (R322ExtractionStep m)) (post : List (R322ExtractionStep m)) (res : R324WithinHalfResidualPrefix ρ lam ε e₀.fst), r322AnalyticSchedule e₀.fst = pre ++ r324FirstLeftSelectedStep e₀ hleft :: post ∧ res.state.processed = pre ∧ res.remaining = r324FirstLeftSelectedStep e₀ hleft :: post ∧ ∀ earlier ∈ pre, Disjoint earlier.2 (selectedExtractionBlock e₀.fst Finset.univ hleft)

The analytic decomposition of the first-left selector produces an actual reachable residual prefix whose literal head is that selector.