Global processed-prefix residual invariant for R-322

The one-step residual Fubini theorem carries an arbitrary outer factor. To iterate it honestly, that outer factor must be the complete surviving integrand on the sparse active carrier, not an unconstrained placeholder. This module defines that object.

After a processed prefix:

• coordinates range only over active non-endpoint vertices;
• every active left vertex reads its actual sparse successor;
• right-edge slots of the remaining proper extraction steps are replaced by their signed difference factors;
• every remaining extraction block carries its complete primitive covariance sum; and
• the coupling power is exactly the sum of the remaining block orders.

No unintegrated initial integrand is identified with a post-collapse state.

A reachable processed prefix and its surviving coordinates

structure Anderson4D.R322AnalyticResidualPrefix (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) (hq : 1 ≤ q) : Type

Complete data at one genuine processed prefix of the production schedule.

• pairing : PartialPairing (Fin (2 * q))
• pairing_mem : self.pairing ∈ nonSplitPairings q
• state : R322AnalyticEdgeState q hq
• remaining : List (R322ExtractionStep (2 * q))
• schedule_eq : r322AnalyticSchedule self.pairing = self.state.processed ++ self.remaining
• absorbed : R322AnalyticAbsorbedState ρ lam ε hq self.pairing ⋯ self.state

def Anderson4D.R322AnalyticResidualPrefix.SurvivingCoordinate {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) : Type

Active vertices which remain genuine spatial variables. The two global endpoints are fixed separately to z and 0.

Equations

• res.SurvivingCoordinate = { i : Fin (2 * q) // i ∈ res.state.active ∧ 0 < ↑i ∧ ↑i < 2 * q - 1 }

@[implicit_reducible]

noncomputable instance Anderson4D.R322AnalyticResidualPrefix.survivingCoordinateFintype {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) : Fintype res.SurvivingCoordinate

Equations

• res.survivingCoordinateFintype = inferInstance

noncomputable def Anderson4D.R322AnalyticResidualPrefix.reconstruct {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (z : T4) (v : res.SurvivingCoordinate → T4) : Fin (2 * q) → T4

Canonical ambient tuple reconstructed from surviving coordinates. Coordinates deleted by the processed prefix are set to zero; every residual factor below is proved/defined to read only active coordinates.

Equations

• res.reconstruct z v i = if hzero : ↑i = 0 then z else if hlast : ↑i = 2 * q - 1 then 0 else if hactive : i ∈ res.state.active then v ⟨i, ⋯⟩ else 0

@[simp]

theorem Anderson4D.R322AnalyticResidualPrefix.reconstruct_zero {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (z : T4) (v : res.SurvivingCoordinate → T4) : res.reconstruct z v ⟨0, ⋯⟩ = z

@[simp]

theorem Anderson4D.R322AnalyticResidualPrefix.reconstruct_last {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (z : T4) (v : res.SurvivingCoordinate → T4) : res.reconstruct z v ⟨2 * q - 1, ⋯⟩ = 0

@[simp]

theorem Anderson4D.R322AnalyticResidualPrefix.reconstruct_surviving {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (z : T4) (v : res.SurvivingCoordinate → T4) (i : res.SurvivingCoordinate) : res.reconstruct z v ↑i = v i

theorem Anderson4D.R322AnalyticResidualPrefix.reconstruct_eq_zero_of_internal_inactive {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (z : T4) (v : res.SurvivingCoordinate → T4) (i : Fin (2 * q)) (hzero : ↑i ≠ 0) (hlast : ↑i ≠ 2 * q - 1) (hinactive : i ∉ res.state.active) : res.reconstruct z v i = 0

The complete surviving suffix factor

def Anderson4D.R322AnalyticResidualPrefix.edgeSuccessor {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (edge : Fin (2 * q - 1)) : Fin (2 * q)

The next active vertex to the right of an ambient edge slot.

Equations

• res.edgeSuccessor edge = Anderson4D.r322AnalyticSuccessorVertex res.state (Anderson4D.r322AnalyticEdgeLeftVertex edge) ⋯

def Anderson4D.R322AnalyticResidualPrefix.remainingRightValues {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) : List ℕ

Right-endpoint values whose ordinary active edge is replaced by a remaining signed extraction difference.

Equations

• res.remainingRightValues = List.map (fun (step : Anderson4D.R322ExtractionStep (2 * q)) => ↑step.1.2) res.remaining

noncomputable def Anderson4D.R322AnalyticResidualPrefix.residualChainEdgeFactor {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (x : Fin (2 * q) → T4) (edge : Fin (2 * q - 1)) : ℝ

One surviving sparse chain factor. Inactive slots contribute one, and remaining extraction right edges are reserved for the signed difference product below.

Equations

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

noncomputable def Anderson4D.R322AnalyticResidualPrefix.residualChainProduct {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (x : Fin (2 * q) → T4) : ℝ

Product of all ordinary sparse-carrier edges still present after the processed prefix.

Equations

• res.residualChainProduct x = ∏ edge : Fin (2 * q - 1), res.residualChainEdgeFactor x edge

noncomputable def Anderson4D.R322AnalyticResidualPrefix.residualStepDifference {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (x : Fin (2 * q) → T4) (step : R322ExtractionStep (2 * q)) : ℝ

Signed difference belonging to one remaining extraction step, read on the current sparse carrier. The terminal whole-carrier step has no outgoing edge and contributes one, exactly as in the closed J definition.

Equations

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

noncomputable def Anderson4D.R322AnalyticResidualPrefix.residualDifferenceProduct {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (x : Fin (2 * q) → T4) : ℝ

Product of every remaining signed extraction difference.

Equations

• res.residualDifferenceProduct x = (List.map (res.residualStepDifference x) res.remaining).prod

def Anderson4D.R322AnalyticResidualPrefix.remainingBlockIndex {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (j : Fin res.remaining.length) : ExtractionBlockIndex res.pairing

A remaining schedule block is an actual extraction block of the frozen pairing.

Equations

• res.remainingBlockIndex j = ⟨(res.remaining.get j).2, ⋯⟩

@[simp]

theorem Anderson4D.R322AnalyticResidualPrefix.remainingBlockIndex_val {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (j : Fin res.remaining.length) : ↑(res.remainingBlockIndex j) = (res.remaining.get j).2

noncomputable def Anderson4D.R322AnalyticResidualPrefix.residualPrimitiveProduct {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) : SmoothCutoff → ℝ → (x : Fin (2 * q) → T4) → ℝ

Complete primitive covariance coordinate for every remaining block.

Equations

• res.residualPrimitiveProduct ρ ε x = ∏ j : Fin res.remaining.length, Anderson4D.r322ExtractionBlockPrimitiveSum ρ ε res.pairing (res.remainingBlockIndex j) x

noncomputable def Anderson4D.R322AnalyticResidualPrefix.residualIntegrand {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) : SmoothCutoff → ℝ → (x : Fin (2 * q) → T4) → ℝ

Complete post-prefix residual integrand on the sparse carrier.

Equations

• res.residualIntegrand ρ ε x = res.residualChainProduct x * res.residualDifferenceProduct x * res.residualPrimitiveProduct ρ ε x

def Anderson4D.R322AnalyticResidualPrefix.remainingOrder {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) : ℕ

Exact perturbative order which has not yet been integrated.

Equations

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

noncomputable def Anderson4D.R322AnalyticResidualPrefix.residualValue {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) : SmoothCutoff → ℝ → ℝ → (z : T4) → ℝ

Complete scalar residual value after the processed prefix.

Equations

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

The exact order ledger

theorem Anderson4D.R322AnalyticResidualPrefix.processedOrder_add_remainingOrder {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) : (List.map (fun (step : R322ExtractionStep (2 * q)) => residualBlockOrder step.2) res.state.processed).sum + res.remainingOrder = q

Proper and terminal transitions of the data object

def Anderson4D.R322AnalyticResidualPrefix.properStepContext {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) : R322AnalyticProperStepContext q hq

The genuine proper-step context at the head of a nonterminal residual res.

Equations

• res.properStepContext step suffix hremaining hproper = { state := res.state, pairing := res.pairing, pairing_mem := ⋯, suffix := suffix, step := step, schedule_eq := ⋯, proper := hproper }

noncomputable def Anderson4D.R322AnalyticResidualPrefix.afterProper {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) : R322AnalyticResidualPrefix ρ lam ε q hq

Residual-prefix data after one actual proper state update.

Equations

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

@[simp]

theorem Anderson4D.R322AnalyticResidualPrefix.afterProper_remaining {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) : (res.afterProper step suffix hremaining hproper).remaining = suffix

@[simp]

theorem Anderson4D.R322AnalyticResidualPrefix.afterProper_active {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) : (res.afterProper step suffix hremaining hproper).state.active = res.state.active \ step.2

def Anderson4D.R322AnalyticResidualPrefix.terminalStepContext {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (terminal : R322ExtractionStep (2 * q)) (hremaining : res.remaining = [terminal]) (hterminal : terminal.1 = r322WholeEndpoint q hq) : R322AnalyticTerminalStepContext q hq

A singleton whole-carrier suffix produces the certified terminal context on exactly the current heterogeneous state.

Equations

• res.terminalStepContext terminal hremaining hterminal = { state := res.state, pairing := res.pairing, pairing_mem := ⋯, terminal := terminal, schedule_eq := ⋯, terminal_endpoint := hterminal }

The first production update in the global residual type

noncomputable def Anderson4D.R322AnalyticResidualPrefix.initial (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) : R322AnalyticResidualPrefix ρ lam ε q hq

The unprocessed production schedule as a residual-prefix object.

Equations

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

noncomputable def Anderson4D.R322AnalyticResidualPrefix.afterInitialProper (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) : R322AnalyticResidualPrefix ρ lam ε q hq

The first proper production absorption, expressed in the global residual data type.

Equations

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

@[simp]

theorem Anderson4D.R322AnalyticResidualPrefix.afterInitialProper_remaining (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) : (afterInitialProper ρ lam ε hq κ hκ head tail hschedule hproper).remaining = tail

@[simp]

theorem Anderson4D.R322AnalyticResidualPrefix.afterInitialProper_state (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) : (afterInitialProper ρ lam ε hq κ hκ head tail hschedule hproper).state = (r322InitialProperStepContext hq κ hκ head tail hschedule hproper).nextState ρ lam ε

theorem Anderson4D.R322AnalyticResidualPrefix.afterInitialProper_active (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) : (afterInitialProper ρ lam ε hq κ hκ head tail hschedule hproper).state.active = Finset.univ \ head.2

The surviving carrier after the first production absorption is exactly the complement of the first concrete block.

@[reducible, inline]

abbrev Anderson4D.R322AnalyticResidualPrefix.InitialComplementCoordinate {q : ℕ} (hq : 1 ≤ q) (head : R322ExtractionStep (2 * q)) : Type

Complementary ambient internal coordinates used by the first-step Fubini theorem.

Equations

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

@[reducible, inline]

abbrev Anderson4D.R322AnalyticResidualPrefix.AfterInitialSurvivingCoordinate (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) : Type

Explicit carrier form used to keep the ambient order visible during the dependent first-prefix reindex.

Equations

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

@[simp]

theorem Anderson4D.R322AnalyticResidualPrefix.primitiveInternalIdx_val_residual (q : ℕ) (hq : 1 ≤ q) (i : Fin (2 * q - 2)) : ↑(primitiveInternalIdx q hq i) = ↑i + 1

def Anderson4D.R322AnalyticResidualPrefix.initialComplementEquivSurviving (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) : InitialComplementCoordinate hq head ≃ AfterInitialSurvivingCoordinate ρ lam ε hq κ hκ head tail hschedule hproper

The first-step complementary coordinates are precisely the surviving active internal vertices after the first block has been removed.

Equations

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

noncomputable def Anderson4D.R322AnalyticResidualPrefix.initialComplementPiMeasurableEquiv (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) : (InitialComplementCoordinate hq head → T4) ≃ᵐ (AfterInitialSurvivingCoordinate ρ lam ε hq κ hκ head tail hschedule hproper → T4)

Coordinate-function reindex induced by initialComplementEquivSurviving.

Equations

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

theorem Anderson4D.R322AnalyticResidualPrefix.measurePreserving_initialComplementPiMeasurableEquiv (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) : MeasureTheory.MeasurePreserving (⇑(initialComplementPiMeasurableEquiv ρ lam ε hq κ hκ head tail hschedule hproper)) (MeasureTheory.Measure.pi fun (x : InitialComplementCoordinate hq head) => paperMeasure) (MeasureTheory.Measure.pi fun (x : AfterInitialSurvivingCoordinate ρ lam ε hq κ hκ head tail hschedule hproper) => paperMeasure)

The concrete first-prefix reindex preserves the exact product Haar measure.

@[simp]

theorem Anderson4D.R322AnalyticResidualPrefix.initialComplementPiMeasurableEquiv_apply (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (vC : InitialComplementCoordinate hq head → T4) (j : InitialComplementCoordinate hq head) : (initialComplementPiMeasurableEquiv ρ lam ε hq κ hκ head tail hschedule hproper) vC ((initialComplementEquivSurviving ρ lam ε hq κ hκ head tail hschedule hproper) j) = vC j

The concrete first-prefix function reindex reads the same coordinate at the corresponding surviving ambient vertex.

theorem Anderson4D.R322AnalyticResidualPrefix.properHeadReferenceTuple_internal_complement {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (z : T4) (vC : InitialComplementCoordinate hq head → T4) (j : InitialComplementCoordinate hq head) : r322AnalyticProperHeadReferenceTuple hq κ hκ head tail hschedule hproper z vC (primitiveInternalIdx q hq ↑j) = vC j

The proper-head reference tuple reads a complementary internal coordinate literally.

theorem Anderson4D.R322AnalyticResidualPrefix.properHeadReferenceTuple_eq_zero_of_mem {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (z : T4) (vC : InitialComplementCoordinate hq head → T4) (i : Fin (2 * q)) (hi : i ∈ head.2) : r322AnalyticProperHeadReferenceTuple hq κ hκ head tail hschedule hproper z vC i = 0

Every deleted first-block coordinate is zero in the fixed proper-head reference tuple.

theorem Anderson4D.R322AnalyticResidualPrefix.afterInitialProper_reconstruct_reindex (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (z : T4) (vC : InitialComplementCoordinate hq head → T4) : (afterInitialProper ρ lam ε hq κ hκ head tail hschedule hproper).reconstruct z ((initialComplementPiMeasurableEquiv ρ lam ε hq κ hκ head tail hschedule hproper) vC) = r322AnalyticProperHeadReferenceTuple hq κ hκ head tail hschedule hproper z vC

Under the concrete finite-coordinate reindex, the global residual reconstruction is exactly the first-step reference tuple.

Exact first-prefix factor ledger

theorem Anderson4D.R322AnalyticResidualPrefix.edgeSuccessor_eq_adjacent_of_right_mem_active {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (edge : Fin (2 * q - 1)) (hright : r322JChainEdgeRight edge ∈ res.state.active) : res.edgeSuccessor edge = r322JChainEdgeRight edge

If the ordinary adjacent right vertex is active, it is already the least sparse successor.

theorem Anderson4D.R322AnalyticResidualPrefix.afterInitialProper_predecessor_successor_eq (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) : have ctx := r322InitialProperStepContext hq κ hκ head tail hschedule hproper; have post := afterInitialProper ρ lam ε hq κ hκ head tail hschedule hproper; post.edgeSuccessor ctx.predecessorEdge = ctx.successorVertex

The updated predecessor slot skips exactly the deleted first block.

theorem Anderson4D.R322AnalyticResidualPrefix.afterInitialProper_residualPrimitiveProduct_eq (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (x : Fin (2 * q) → T4) : (afterInitialProper ρ lam ε hq κ hκ head tail hschedule hproper).residualPrimitiveProduct ρ ε x = ∏ j : Fin tail.length, r322ExtractionBlockPrimitiveSum ρ ε κ (r322AnalyticTailBlockIndex κ hschedule j) x

The primitive-block part of the global residual is literally the tail primitive product from the first-step pointwise factorization.

theorem Anderson4D.R322AnalyticResidualPrefix.afterInitialProper_headRight_lt_tailRight {q : ℕ} (κ : PartialPairing (Fin (2 * q))) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (step : R322ExtractionStep (2 * q)) (hstep : step ∈ tail) : head.1.2 < step.1.2

Every later right endpoint lies strictly beyond the first one.

theorem Anderson4D.R322AnalyticResidualPrefix.afterInitialProper_tail_successor_eq_adjacent (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (step : R322ExtractionStep (2 * q)) (hstep : step ∈ tail) (hguard : ↑step.1.2 < 2 * q - 1) : r322AnalyticSuccessorVertex (afterInitialProper ρ lam ε hq κ hκ head tail hschedule hproper).state step.1.2 hguard = ⟨↑step.1.2 + 1, ⋯⟩

After removing the first block, the sparse successor of every later right endpoint is still its ordinary adjacent ambient vertex.

theorem Anderson4D.R322AnalyticResidualPrefix.afterInitialProper_tail_edge_eq_greenFn (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (step : R322ExtractionStep (2 * q)) (hstep : step ∈ tail) (hguard : ↑step.1.2 < 2 * q - 1) : (afterInitialProper ρ lam ε hq κ hκ head tail hschedule hproper).state.edges ⟨↑step.1.2, hguard⟩ = greenFn

The outgoing edge of every tail step is untouched by the first update and therefore remains the free Green kernel.

theorem Anderson4D.R322AnalyticResidualPrefix.afterInitialProper_residualDifferenceProduct_eq (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (x : Fin (2 * q) → T4) : (afterInitialProper ρ lam ε hq κ hκ head tail hschedule hproper).residualDifferenceProduct x = r322AnalyticDiffProductWith (fun (x : Fin (2 * q - 1)) => greenFn) tail x

The global sparse signed-difference product after the first update is exactly the old all-Green tail difference product.

theorem Anderson4D.R322AnalyticResidualPrefix.afterInitialProper_residualChainEdgeFactor_predecessor (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (x : Fin (2 * q) → T4) : have ctx := r322InitialProperStepContext hq κ hκ head tail hschedule hproper; have post := afterInitialProper ρ lam ε hq κ hκ head tail hschedule hproper; post.residualChainEdgeFactor x ctx.predecessorEdge = post.state.edges ctx.predecessorEdge (x (r322AnalyticEdgeLeftVertex ctx.predecessorEdge) - x ctx.successorVertex)

The predecessor contribution in the first post-update sparse chain is the newly collapsed heterogeneous edge, read against the actual sparse successor.

theorem Anderson4D.R322AnalyticResidualPrefix.afterInitialProper_residualChainEdgeFactor_eq_of_ne (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (x : Fin (2 * q) → T4) (edge : Fin (2 * q - 1)) (hne : edge ≠ (r322InitialProperStepContext hq κ hκ head tail hschedule hproper).predecessorEdge) : have post := afterInitialProper ρ lam ε hq κ hκ head tail hschedule hproper; post.residualChainEdgeFactor x edge = if R322ChainEdgeOutside head.2 edge then r322AnalyticChainEdgeFactorWith (fun (x : Fin (2 * q - 1)) => greenFn) κ x edge else 1

Away from the collapsed predecessor slot, the post-update sparse-chain factor is exactly the corresponding exterior factor from the old head split.

theorem Anderson4D.R322AnalyticResidualPrefix.afterInitialProper_residualChainProduct_eq (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (x : Fin (2 * q) → T4) : have ctx := r322InitialProperStepContext hq κ hκ head tail hschedule hproper; have post := afterInitialProper ρ lam ε hq κ hκ head tail hschedule hproper; post.residualChainProduct x = post.state.edges ctx.predecessorEdge (x (r322AnalyticEdgeLeftVertex ctx.predecessorEdge) - x ctx.successorVertex) * r322AnalyticHeadOuterChainProductWith (fun (x : Fin (2 * q - 1)) => greenFn) κ head x

Exact chain ledger after the first absorption: the new predecessor edge is pulled out once, and every other slot is the old exterior head-chain factor.

theorem Anderson4D.R322AnalyticResidualPrefix.afterInitialProper_residualIntegrand_eq (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (x : Fin (2 * q) → T4) : have ctx := r322InitialProperStepContext hq κ hκ head tail hschedule hproper; have post := afterInitialProper ρ lam ε hq κ hκ head tail hschedule hproper; post.residualIntegrand ρ ε x = post.state.edges ctx.predecessorEdge (ctx.predecessorPoint x - ctx.successorPoint x) * r322AnalyticHeadOuterIntegrandFactor ρ ε κ head tail hschedule x

Pointwise closure of the complete first post-prefix integrand. This is the missing compatibility statement between the global sparse residual and the concrete outer factor produced by the first Fubini absorption.

Exact first residual-value transition

theorem Anderson4D.R322AnalyticResidualPrefix.r322InitialUpdatedOuterIntegral_eq_afterInitialProper_residualValue (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (z : T4) : r322InitialUpdatedOuterIntegral hq ρ lam ε κ hκ head tail hschedule hproper z = (afterInitialProper ρ lam ε hq κ hκ head tail hschedule hproper).residualValue ρ lam ε z

The concrete first updated outer integral is exactly the value of the global post-prefix residual object. The proof uses the explicit finite coordinate equivalence above; no identification of pre- and post-collapse ambient integrands is made.

Arbitrary proper-prefix coordinate decomposition

theorem Anderson4D.R322AnalyticResidualPrefix.properBlockVertex_mem_active {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (i : Fin (2 * q)) (hi : i ∈ step.2) : have _ctx := res.properStepContext step suffix hremaining hproper; i ∈ res.state.active

Every vertex of the current concrete block is active before the current proper update.

theorem Anderson4D.R322AnalyticResidualPrefix.properBlockVertex_internal {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (i : Fin (2 * q)) (hi : i ∈ step.2) : have _ctx := res.properStepContext step suffix hremaining hproper; 0 < ↑i ∧ ↑i < 2 * q - 1

A proper block contains neither global endpoint, so each of its vertices is represented in the pre-update surviving-coordinate type.

theorem Anderson4D.R322AnalyticResidualPrefix.afterProper_vertex_mem_previous_active {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (i : Fin (2 * q)) (hi : i ∈ (res.afterProper step suffix hremaining hproper).state.active) : i ∈ res.state.active

The updated active carrier is a subset of the old one.

def Anderson4D.R322AnalyticResidualPrefix.properBlockOrderIso {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) : Fin (2 * residualBlockOrder step.2) ≃ ↥step.2

The current context's canonical block order, with its definitionally equal step field hidden behind a stable public type.

Equations

• res.properBlockOrderIso step suffix hremaining hproper = (res.properStepContext step suffix hremaining hproper).blockOrderIso.toEquiv

def Anderson4D.R322AnalyticResidualPrefix.properCoordinateEquiv {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) : Fin (2 * residualBlockOrder step.2) ⊕ (res.afterProper step suffix hremaining hproper).SurvivingCoordinate ≃ res.SurvivingCoordinate

Exact index decomposition at an arbitrary reachable proper prefix: current standard block vertices, followed by all post-update surviving vertices.

Equations

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

noncomputable def Anderson4D.R322AnalyticResidualPrefix.properCoordinatePiMeasurableEquiv {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) : (res.SurvivingCoordinate → T4) ≃ᵐ (Fin (2 * residualBlockOrder step.2) → T4) × ((res.afterProper step suffix hremaining hproper).SurvivingCoordinate → T4)

Measurable splitting of all pre-update surviving coordinates into the current standard block and the post-update surviving carrier.

Equations

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

theorem Anderson4D.R322AnalyticResidualPrefix.measurePreserving_properCoordinatePiMeasurableEquiv {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) : MeasureTheory.MeasurePreserving (⇑(res.properCoordinatePiMeasurableEquiv step suffix hremaining hproper)) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure) ((MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder step.2)) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : (res.afterProper step suffix hremaining hproper).SurvivingCoordinate) => paperMeasure))

The arbitrary-prefix split preserves the exact product Haar measure.

@[simp]

theorem Anderson4D.R322AnalyticResidualPrefix.properCoordinatePiMeasurableEquiv_fst_apply {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (v : res.SurvivingCoordinate → T4) (j : Fin (2 * residualBlockOrder step.2)) : ((res.properCoordinatePiMeasurableEquiv step suffix hremaining hproper) v).1 j = v ((res.properCoordinateEquiv step suffix hremaining hproper) (Sum.inl j))

@[simp]

theorem Anderson4D.R322AnalyticResidualPrefix.properCoordinatePiMeasurableEquiv_snd_apply {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (v : res.SurvivingCoordinate → T4) (i : (res.afterProper step suffix hremaining hproper).SurvivingCoordinate) : ((res.properCoordinatePiMeasurableEquiv step suffix hremaining hproper) v).2 i = v ((res.properCoordinateEquiv step suffix hremaining hproper) (Sum.inr i))

def Anderson4D.R322AnalyticResidualPrefix.properReconstructBlockTuple {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (base : Fin (2 * q) → T4) (t : Fin (2 * residualBlockOrder step.2) → T4) : Fin (2 * q) → T4

Stable, step-typed wrapper around the context's ambient block reconstruction.

Equations

• res.properReconstructBlockTuple step suffix hremaining hproper base t i = if hi : i ∈ step.2 then t ((res.properBlockOrderIso step suffix hremaining hproper).symm ⟨i, hi⟩) else base i

theorem Anderson4D.R322AnalyticResidualPrefix.properReconstructBlockTuple_eq_context {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (base : Fin (2 * q) → T4) (t : Fin (2 * residualBlockOrder step.2) → T4) : res.properReconstructBlockTuple step suffix hremaining hproper base t = (res.properStepContext step suffix hremaining hproper).reconstructBlockTuple base t

The stable wrapper is the actual context reconstruction.

theorem Anderson4D.R322AnalyticResidualPrefix.reconstructBlockTuple_properCoordinateSplit {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (z : T4) (v : res.SurvivingCoordinate → T4) : res.properReconstructBlockTuple step suffix hremaining hproper ((res.afterProper step suffix hremaining hproper).reconstruct z ((res.properCoordinatePiMeasurableEquiv step suffix hremaining hproper) v).2) ((res.properCoordinatePiMeasurableEquiv step suffix hremaining hproper) v).1 = res.reconstruct z v

Reassembling the two components of the arbitrary-prefix coordinate split reproduces the original ambient residual tuple exactly.

noncomputable def Anderson4D.R322AnalyticResidualPrefix.properOuterBlockPiMeasurableEquiv {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) : (res.SurvivingCoordinate → T4) ≃ᵐ ((res.afterProper step suffix hremaining hproper).SurvivingCoordinate → T4) × (Fin (2 * residualBlockOrder step.2) → T4)

Outer-first form of the proper coordinate split, matching the order of integration in the one-step residual Fubini API.

Equations

• res.properOuterBlockPiMeasurableEquiv step suffix hremaining hproper = (res.properCoordinatePiMeasurableEquiv step suffix hremaining hproper).trans MeasurableEquiv.prodComm

theorem Anderson4D.R322AnalyticResidualPrefix.measurePreserving_properOuterBlockPiMeasurableEquiv {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) : MeasureTheory.MeasurePreserving (⇑(res.properOuterBlockPiMeasurableEquiv step suffix hremaining hproper)) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure) ((MeasureTheory.Measure.pi fun (x : (res.afterProper step suffix hremaining hproper).SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder step.2)) => paperMeasure))

The outer-first split preserves outer-product-block Haar measure.

@[simp]

theorem Anderson4D.R322AnalyticResidualPrefix.properOuterBlockPiMeasurableEquiv_fst_apply {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (v : res.SurvivingCoordinate → T4) : ((res.properOuterBlockPiMeasurableEquiv step suffix hremaining hproper) v).1 = ((res.properCoordinatePiMeasurableEquiv step suffix hremaining hproper) v).2

@[simp]

theorem Anderson4D.R322AnalyticResidualPrefix.properOuterBlockPiMeasurableEquiv_snd_apply {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (v : res.SurvivingCoordinate → T4) : ((res.properOuterBlockPiMeasurableEquiv step suffix hremaining hproper) v).2 = ((res.properCoordinatePiMeasurableEquiv step suffix hremaining hproper) v).1

theorem Anderson4D.R322AnalyticResidualPrefix.reconstructBlockTuple_properOuterBlockSplit {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (z : T4) (v : res.SurvivingCoordinate → T4) : res.properReconstructBlockTuple step suffix hremaining hproper ((res.afterProper step suffix hremaining hproper).reconstruct z ((res.properOuterBlockPiMeasurableEquiv step suffix hremaining hproper) v).1) ((res.properOuterBlockPiMeasurableEquiv step suffix hremaining hproper) v).2 = res.reconstruct z v

Reassembly stated directly for the outer-first measurable split.

theorem Anderson4D.R322AnalyticResidualPrefix.residualValue_eq_iteratedProperRaw {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (ρ✝ : SmoothCutoff) (lam✝ ε✝ : ℝ) (z : T4) (hint : MeasureTheory.Integrable (fun (v : res.SurvivingCoordinate → T4) => res.residualIntegrand ρ✝ ε✝ (res.reconstruct z v)) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)) : res.residualValue ρ✝ lam✝ ε✝ z = lamEps lam✝ ε✝ ^ (2 * res.remainingOrder) * ∫ (outer : (res.afterProper step suffix hremaining hproper).SurvivingCoordinate → T4), ∫ (t : Fin (2 * residualBlockOrder step.2) → T4), res.residualIntegrand ρ✝ ε✝ (res.properReconstructBlockTuple step suffix hremaining hproper ((res.afterProper step suffix hremaining hproper).reconstruct z outer) t) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder step.2)) => paperMeasure ∂MeasureTheory.Measure.pi fun (x : (res.afterProper step suffix hremaining hproper).SurvivingCoordinate) => paperMeasure

Exact outer-then-block Fubini form of an arbitrary proper-prefix residual value. The sole premise is genuine joint integrability of the current residual integrand; no equality or estimate is assumed.

Arbitrary proper-prefix factor ledgers

theorem Anderson4D.R322AnalyticResidualPrefix.remainingOrder_eq_current_add_afterProper {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) : res.remainingOrder = residualBlockOrder step.2 + (res.afterProper step suffix hremaining hproper).remainingOrder

The coupling order splits exactly into the current block order and the post-update suffix order.

theorem Anderson4D.R322AnalyticResidualPrefix.residualPrimitiveProduct_eq_current_mul_afterProper {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (ρ✝ : SmoothCutoff) (ε✝ : ℝ) (x : Fin (2 * q) → T4) : res.residualPrimitiveProduct ρ✝ ε✝ x = r322ExtractionBlockPrimitiveSum ρ✝ ε✝ res.pairing (res.remainingBlockIndex ⟨0, ⋯⟩) x * (res.afterProper step suffix hremaining hproper).residualPrimitiveProduct ρ✝ ε✝ x

The primitive covariance product splits at the current schedule head; the suffix is exactly the post-update primitive product.

theorem Anderson4D.R322AnalyticResidualPrefix.remainingBlockIndex_zero_val {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) : ↑(res.remainingBlockIndex ⟨0, ⋯⟩) = step.2

The current residual block index is the actual block stored at the displayed proper head.

theorem Anderson4D.R322AnalyticResidualPrefix.properStep_right_lt_suffix_right {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (later : R322ExtractionStep (2 * q)) (hlater : later ∈ suffix) : have _ctx := res.properStepContext step suffix hremaining hproper; step.1.2 < later.1.2

Every suffix step has a strictly larger right endpoint than the current proper head.

theorem Anderson4D.R322AnalyticResidualPrefix.successorCandidates_afterProper_eq_of_mem_suffix {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (later : R322ExtractionStep (2 * q)) (hlater : later ∈ suffix) : r322AnalyticSuccessorCandidates (res.afterProper step suffix hremaining hproper).state later.1.2 = r322AnalyticSuccessorCandidates res.state later.1.2

Removing the current block does not alter the active-successor set strictly to the right of any suffix endpoint.

theorem Anderson4D.R322AnalyticResidualPrefix.successorVertex_afterProper_eq_of_mem_suffix {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (later : R322ExtractionStep (2 * q)) (hlater : later ∈ suffix) (hguard : ↑later.1.2 < 2 * q - 1) : r322AnalyticSuccessorVertex (res.afterProper step suffix hremaining hproper).state later.1.2 hguard = r322AnalyticSuccessorVertex res.state later.1.2 hguard

Consequently every suffix endpoint has exactly the same sparse successor before and after the current proper update.

theorem Anderson4D.R322AnalyticResidualPrefix.afterProper_suffix_edge_eq {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (later : R322ExtractionStep (2 * q)) (hlater : later ∈ suffix) (hguard : ↑later.1.2 < 2 * q - 1) : (res.afterProper step suffix hremaining hproper).state.edges ⟨↑later.1.2, hguard⟩ = res.state.edges ⟨↑later.1.2, hguard⟩

The edge stored at a suffix right endpoint is untouched by the current proper update.

theorem Anderson4D.R322AnalyticResidualPrefix.residualStepDifference_afterProper_eq_of_mem_suffix {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (x : Fin (2 * q) → T4) (later : R322ExtractionStep (2 * q)) (hlater : later ∈ suffix) : (res.afterProper step suffix hremaining hproper).residualStepDifference x later = res.residualStepDifference x later

Every signed suffix difference is pointwise unchanged by the current proper update.

theorem Anderson4D.R322AnalyticResidualPrefix.residualDifferenceProduct_eq_current_mul_afterProper {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (x : Fin (2 * q) → T4) : res.residualDifferenceProduct x = res.residualStepDifference x step * (res.afterProper step suffix hremaining hproper).residualDifferenceProduct x

The complete difference product splits into the current signed difference and the unchanged post-update suffix product.

theorem Anderson4D.R322AnalyticResidualPrefix.residualStepDifference_current_eq {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (x : Fin (2 * q) → T4) : res.residualStepDifference x step = res.state.edges (res.properStepContext step suffix hremaining hproper).outgoingEdge (x step.1.2 - x (res.properStepContext step suffix hremaining hproper).successorVertex) - res.state.edges (res.properStepContext step suffix hremaining hproper).outgoingEdge (x step.1.1 - x (res.properStepContext step suffix hremaining hproper).successorVertex)

The current residual difference is the context's actual sparse outgoing difference.

Arbitrary proper-prefix chain ledgers

theorem Anderson4D.R322AnalyticResidualPrefix.afterProper_predecessor_successor_eq {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) : (res.afterProper step suffix hremaining hproper).edgeSuccessor (res.properStepContext step suffix hremaining hproper).predecessorEdge = (res.properStepContext step suffix hremaining hproper).successorVertex

After deleting the current proper block, the predecessor slot skips exactly that block and lands at the old sparse successor of the current right endpoint.

theorem Anderson4D.R322AnalyticResidualPrefix.afterProper_predecessor_chain_factor {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (x : Fin (2 * q) → T4) : (res.afterProper step suffix hremaining hproper).residualChainEdgeFactor x (res.properStepContext step suffix hremaining hproper).predecessorEdge = (res.afterProper step suffix hremaining hproper).state.edges (res.properStepContext step suffix hremaining hproper).predecessorEdge (x (r322AnalyticEdgeLeftVertex (res.properStepContext step suffix hremaining hproper).predecessorEdge) - x (res.properStepContext step suffix hremaining hproper).successorVertex)

The updated predecessor is active in the post-state and is not reserved for a later signed-difference slot.

theorem Anderson4D.R322AnalyticResidualPrefix.properStep_blockOrderIso_zero {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) : ↑((res.properStepContext step suffix hremaining hproper).blockOrderIso ⟨0, ⋯⟩) = step.1.1

The first coordinate in the increasing current-block enumeration is the selected left endpoint.

theorem Anderson4D.R322AnalyticResidualPrefix.edgeSuccessor_predecessor_eq_step_left {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) : res.edgeSuccessor (res.properStepContext step suffix hremaining hproper).predecessorEdge = step.1.1

Before deletion, the sparse successor of the predecessor slot is the first coordinate of the current block.

theorem Anderson4D.R322AnalyticResidualPrefix.residualChainEdgeFactor_predecessor_eq {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (x : Fin (2 * q) → T4) : res.residualChainEdgeFactor x (res.properStepContext step suffix hremaining hproper).predecessorEdge = res.state.edges (res.properStepContext step suffix hremaining hproper).predecessorEdge ((res.properStepContext step suffix hremaining hproper).predecessorPoint x - (res.properStepContext step suffix hremaining hproper).standardBlockTuple x ⟨0, ⋯⟩)

The pre-update predecessor factor is the incoming edge of the actual ambient local integrand.

theorem Anderson4D.R322AnalyticResidualPrefix.edgeSuccessor_internalEdge_eq {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (j : Fin (2 * residualBlockOrder step.2 - 1)) : let ctx := res.properStepContext step suffix hremaining hproper; have jnext := ⟨↑j + 1, ⋯⟩; res.edgeSuccessor (ctx.internalEdge j) = ↑(ctx.blockOrderIso jnext)

On an internal current-block edge, the sparse successor is the next coordinate in the increasing block enumeration.

theorem Anderson4D.R322AnalyticResidualPrefix.residualChainEdgeFactor_internal_eq {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (x : Fin (2 * q) → T4) (j : Fin (2 * residualBlockOrder step.2 - 1)) : let ctx := res.properStepContext step suffix hremaining hproper; res.residualChainEdgeFactor x (ctx.internalEdge j) = ctx.internalEdges j (ctx.standardBlockTuple x (primitiveEdgeLeft (residualBlockOrder step.2) ⋯ j) - ctx.standardBlockTuple x (primitiveEdgeRight (residualBlockOrder step.2) ⋯ j))

Every current internal ordinary chain factor is exactly the corresponding primitive-chain factor in standard block coordinates.

theorem Anderson4D.R322AnalyticResidualPrefix.residualChainEdgeFactor_outgoing_eq {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (x : Fin (2 * q) → T4) : res.residualChainEdgeFactor x (res.properStepContext step suffix hremaining hproper).outgoingEdge = 1

The current outgoing slot is reserved for the signed difference product and contributes one to the ordinary chain.

noncomputable def Anderson4D.R322AnalyticResidualPrefix.properOuterChainProduct {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (x : Fin (2 * q) → T4) : ℝ

Ordinary chain slots which remain genuinely exterior to the current proper block and its incoming predecessor slot.

Equations

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

noncomputable def Anderson4D.R322AnalyticResidualPrefix.properOuterIntegrand {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) : SmoothCutoff → ℝ → (x : Fin (2 * q) → T4) → ℝ

The complete exterior factor carried unchanged through the current proper block integration.

Equations

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

theorem Anderson4D.R322AnalyticResidualPrefix.prod_internalEdgesFinset_residualChainEdgeFactor {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (x : Fin (2 * q) → T4) : have ctx := res.properStepContext step suffix hremaining hproper; ∏ edge ∈ ctx.internalEdgesFinset, res.residualChainEdgeFactor x edge = primitiveChainProduct (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges (ctx.standardBlockTuple x)

The product over the actual internal ambient slots is exactly the primitive chain product in standard current-block coordinates.

theorem Anderson4D.R322AnalyticResidualPrefix.residualChainProduct_eq_local_mul_outer {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (x : Fin (2 * q) → T4) : let ctx := res.properStepContext step suffix hremaining hproper; res.residualChainProduct x = res.state.edges ctx.predecessorEdge (ctx.predecessorPoint x - ctx.standardBlockTuple x ⟨0, ⋯⟩) * primitiveChainProduct (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges (ctx.standardBlockTuple x) * res.properOuterChainProduct step suffix hremaining hproper x

Exact ordinary-chain factorization at an arbitrary reachable proper prefix: incoming edge, current internal primitive chain, and the complete exterior chain.

theorem Anderson4D.R322AnalyticResidualPrefix.afterProper_edgeSuccessor_eq_of_outer {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (edge : Fin (2 * q - 1)) (hedge : edge ∈ Finset.univ \ ({(res.properStepContext step suffix hremaining hproper).predecessorEdge} ∪ (res.properStepContext step suffix hremaining hproper).blockEdges)) (hactive : r322AnalyticEdgeLeftVertex edge ∈ res.state.active) : (res.afterProper step suffix hremaining hproper).edgeSuccessor edge = res.edgeSuccessor edge

Away from the deleted block and its predecessor slot, removing the current block does not alter the least sparse successor of an active left vertex.

theorem Anderson4D.R322AnalyticResidualPrefix.outerEdge_remainingRightValues_iff {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (edge : Fin (2 * q - 1)) (hedge : edge ∈ Finset.univ \ ({(res.properStepContext step suffix hremaining hproper).predecessorEdge} ∪ (res.properStepContext step suffix hremaining hproper).blockEdges)) : ↑edge ∈ res.remainingRightValues ↔ ↑edge ∈ (res.afterProper step suffix hremaining hproper).remainingRightValues

Exterior slots see the same reserved suffix-right values before and after removal of the current head; the only deleted value is the outgoing slot, which is not exterior.

theorem Anderson4D.R322AnalyticResidualPrefix.afterProper_residualChainEdgeFactor_eq_of_outer {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (x : Fin (2 * q) → T4) (edge : Fin (2 * q - 1)) (hedge : edge ∈ Finset.univ \ ({(res.properStepContext step suffix hremaining hproper).predecessorEdge} ∪ (res.properStepContext step suffix hremaining hproper).blockEdges)) : (res.afterProper step suffix hremaining hproper).residualChainEdgeFactor x edge = res.residualChainEdgeFactor x edge

Every exterior ordinary chain factor is pointwise unchanged by the current proper state update.

theorem Anderson4D.R322AnalyticResidualPrefix.afterProper_residualChainEdgeFactor_eq_one_of_mem_blockEdges {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (x : Fin (2 * q) → T4) (edge : Fin (2 * q - 1)) (hedge : edge ∈ (res.properStepContext step suffix hremaining hproper).blockEdges) : (res.afterProper step suffix hremaining hproper).residualChainEdgeFactor x edge = 1

Slots based in the deleted current block are inactive in the post-state, so their ordinary post-chain factor is one.

theorem Anderson4D.R322AnalyticResidualPrefix.afterProper_residualChainProduct_eq_updated_mul_outer {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (x : Fin (2 * q) → T4) : have ctx := res.properStepContext step suffix hremaining hproper; have post := res.afterProper step suffix hremaining hproper; post.residualChainProduct x = post.state.edges ctx.predecessorEdge (x (r322AnalyticEdgeLeftVertex ctx.predecessorEdge) - x ctx.successorVertex) * res.properOuterChainProduct step suffix hremaining hproper x

Exact post-update ordinary-chain ledger: the newly collapsed predecessor edge is pulled out once, and the exterior chain is literally the same product as before the update.

theorem Anderson4D.R322AnalyticResidualPrefix.remainingBlockIndex_zero_eq_contextBlockIndex {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) : res.remainingBlockIndex ⟨0, ⋯⟩ = (res.properStepContext step suffix hremaining hproper).blockIndex

The current residual head index is the actual block index used by the proper-step context.

theorem Anderson4D.R322AnalyticResidualPrefix.currentPrimitiveSum_eq_standardBlock {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (ρ✝ : SmoothCutoff) (ε✝ : ℝ) (x : Fin (2 * q) → T4) : r322ExtractionBlockPrimitiveSum ρ✝ ε✝ res.pairing (res.remainingBlockIndex ⟨0, ⋯⟩) x = have ctx := res.properStepContext step suffix hremaining hproper; ∑ κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2)), primitiveCovarianceProduct ρ✝ ε✝ (residualBlockOrder ctx.step.2) (↑κB) (ctx.standardBlockTuple x)

The current primitive coordinate in the residual product is exactly the standard-block covariance sum in the ambient local factor.

theorem Anderson4D.R322AnalyticResidualPrefix.residualStepDifference_current_eq_standardBlock {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (x : Fin (2 * q) → T4) : let ctx := res.properStepContext step suffix hremaining hproper; res.residualStepDifference x step = ctx.state.edges ctx.outgoingEdge (ctx.standardBlockTuple x (primitiveLast (residualBlockOrder ctx.step.2) ⋯) - ctx.successorPoint x) - ctx.state.edges ctx.outgoingEdge (ctx.standardBlockTuple x ⟨0, ⋯⟩ - ctx.successorPoint x)

The current signed residual difference is the outgoing term in standard current-block coordinates.

theorem Anderson4D.R322AnalyticResidualPrefix.residualIntegrand_eq_ambientLocal_mul_outer {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (ρ✝ : SmoothCutoff) (ε✝ : ℝ) (x : Fin (2 * q) → T4) : have ctx := res.properStepContext step suffix hremaining hproper; res.residualIntegrand ρ✝ ε✝ x = ctx.ambientLocalIntegrand ρ✝ ε✝ x * res.properOuterIntegrand step suffix hremaining hproper ρ✝ ε✝ x

Pointwise local-times-outer factorization of the complete pre-update residual integrand at an arbitrary reachable proper prefix.

theorem Anderson4D.R322AnalyticResidualPrefix.afterProper_residualIntegrand_eq_updated_mul_outer {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (ρ✝ : SmoothCutoff) (ε✝ : ℝ) (x : Fin (2 * q) → T4) : have ctx := res.properStepContext step suffix hremaining hproper; have post := res.afterProper step suffix hremaining hproper; post.residualIntegrand ρ✝ ε✝ x = post.state.edges ctx.predecessorEdge (ctx.predecessorPoint x - ctx.successorPoint x) * res.properOuterIntegrand step suffix hremaining hproper ρ✝ ε✝ x

Pointwise updated-edge-times-outer factorization of the complete post-update residual integrand.

Exterior-factor independence of current block coordinates

theorem Anderson4D.R322AnalyticResidualPrefix.properReconstructBlockTuple_eq_of_not_mem {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (base : Fin (2 * q) → T4) (t : Fin (2 * residualBlockOrder step.2) → T4) (i : Fin (2 * q)) (hi : i ∉ step.2) : res.properReconstructBlockTuple step suffix hremaining hproper base t i = base i

The stable current-block reconstruction leaves every complementary ambient coordinate unchanged.

theorem Anderson4D.R322AnalyticResidualPrefix.afterProper_residualChainEdgeFactor_eq_of_eq_outside_step {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (x y : Fin (2 * q) → T4) (hxy : ∀ i ∉ step.2, x i = y i) (edge : Fin (2 * q - 1)) : (res.afterProper step suffix hremaining hproper).residualChainEdgeFactor x edge = (res.afterProper step suffix hremaining hproper).residualChainEdgeFactor y edge

A post-update ordinary chain factor depends only on post-active coordinates, hence is insensitive to changes inside the deleted block.

theorem Anderson4D.R322AnalyticResidualPrefix.properOuterChainProduct_eq_of_eq_outside_step {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (x y : Fin (2 * q) → T4) (hxy : ∀ i ∉ step.2, x i = y i) : res.properOuterChainProduct step suffix hremaining hproper x = res.properOuterChainProduct step suffix hremaining hproper y

The exterior ordinary-chain product is independent of every current block coordinate.

theorem Anderson4D.R322AnalyticResidualPrefix.properStep_later_right_or_contains {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (later : R322ExtractionStep (2 * q)) (hlater : later ∈ suffix) : have _ctx := res.properStepContext step suffix hremaining hproper; step.1.2 < later.1.1 ∨ later.1.1 < step.1.1 ∧ step.1.2 < later.1.2

Every displayed suffix step has the paper's disjoint-right-or-containing relation to the current head.

theorem Anderson4D.R322AnalyticResidualPrefix.afterProper_residualStepDifference_eq_of_eq_outside_step {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (x y : Fin (2 * q) → T4) (hxy : ∀ i ∉ step.2, x i = y i) (later : R322ExtractionStep (2 * q)) (hlater : later ∈ suffix) : (res.afterProper step suffix hremaining hproper).residualStepDifference x later = (res.afterProper step suffix hremaining hproper).residualStepDifference y later

Every remaining signed post-update difference is insensitive to current block coordinates.

theorem Anderson4D.R322AnalyticResidualPrefix.afterProper_residualDifferenceProduct_eq_of_eq_outside_step {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (x y : Fin (2 * q) → T4) (hxy : ∀ i ∉ step.2, x i = y i) : (res.afterProper step suffix hremaining hproper).residualDifferenceProduct x = (res.afterProper step suffix hremaining hproper).residualDifferenceProduct y

The complete remaining signed-difference product is independent of the current block coordinates.

theorem Anderson4D.R322AnalyticResidualPrefix.afterProper_residualPrimitiveProduct_eq_of_eq_outside_step {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (ρ✝ : SmoothCutoff) (ε✝ : ℝ) (x y : Fin (2 * q) → T4) (hxy : ∀ i ∉ step.2, x i = y i) : (res.afterProper step suffix hremaining hproper).residualPrimitiveProduct ρ✝ ε✝ x = (res.afterProper step suffix hremaining hproper).residualPrimitiveProduct ρ✝ ε✝ y

The complete remaining primitive covariance product is independent of the current block, using the schedule's exact pairwise block disjointness.

theorem Anderson4D.R322AnalyticResidualPrefix.properOuterIntegrand_eq_of_eq_outside_step {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (ρ✝ : SmoothCutoff) (ε✝ : ℝ) (x y : Fin (2 * q) → T4) (hxy : ∀ i ∉ step.2, x i = y i) : res.properOuterIntegrand step suffix hremaining hproper ρ✝ ε✝ x = res.properOuterIntegrand step suffix hremaining hproper ρ✝ ε✝ y

The complete exterior factor is constant along every current-block coordinate fibre.

theorem Anderson4D.R322AnalyticResidualPrefix.properOuterIntegrand_properReconstructBlockTuple {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (ρ✝ : SmoothCutoff) (ε✝ : ℝ) (base : Fin (2 * q) → T4) (t : Fin (2 * residualBlockOrder step.2) → T4) : res.properOuterIntegrand step suffix hremaining hproper ρ✝ ε✝ (res.properReconstructBlockTuple step suffix hremaining hproper base t) = res.properOuterIntegrand step suffix hremaining hproper ρ✝ ε✝ base

Concrete fibre form: evaluating the exterior factor on a reconstructed current block gives exactly its value on the outer base tuple.

Exact arbitrary-prefix value transition

theorem Anderson4D.R322AnalyticResidualPrefix.residualValue_eq_afterProper {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (step : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (z : T4) (hint : MeasureTheory.Integrable (fun (v : res.SurvivingCoordinate → T4) => res.residualIntegrand ρ ε (res.reconstruct z v)) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)) (hstandard : ∀ᵐ (outer : (res.afterProper step suffix hremaining hproper).SurvivingCoordinate → T4) ∂MeasureTheory.Measure.pi fun (x : (res.afterProper step suffix hremaining hproper).SurvivingCoordinate) => paperMeasure, MeasureTheory.Integrable ((res.properStepContext step suffix hremaining hproper).localIntegrand ρ ε ((res.properStepContext step suffix hremaining hproper).predecessorPoint ((res.afterProper step suffix hremaining hproper).reconstruct z outer) - (res.properStepContext step suffix hremaining hproper).successorPoint ((res.afterProper step suffix hremaining hproper).reconstruct z outer))) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder (res.properStepContext step suffix hremaining hproper).step.2)) => paperMeasure)) (hinternal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder step.2))), MeasureTheory.Integrable (fun (v : Fin (2 * residualBlockOrder step.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder step.2) (↑κB) (res.properStepContext step suffix hremaining hproper).internalEdges (primitiveAssemble (residualBlockOrder step.2) ⋯ p.1 p.2 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder step.2 - 2)) => paperMeasure)) : res.residualValue ρ lam ε z = (res.afterProper step suffix hremaining hproper).residualValue ρ lam ε z

One actual proper schedule step preserves the complete residual value.

The only analytic premises are genuine integrability of the current full residual (for the coordinate Fubini split) and the native almost-everywhere section premises consumed by the local collapse theorem. No equality or estimate interface is assumed.