Surviving coordinates of an R-324 within-half residual prefix

One genuine analytic head partitions the current surviving internal coordinates into the coordinates of that block and the coordinates surviving the corresponding absorb. This module constructs that partition as an actual equivalence and lifts it to a measure-preserving Fubini reindexing.

Only coordinate spaces are related here. In particular, no unintegrated production integrand is identified pointwise with a processed edge state.

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

Internal vertices which remain genuine spatial variables after the processed prefix.

Equations

• res.SurvivingCoordinate = ↥res.state.active

@[implicit_reducible]

noncomputable instance Anderson4D.R324WithinHalfResidualPrefix.survivingCoordinateFintype {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) : Fintype res.SurvivingCoordinate

Equations

• res.survivingCoordinateFintype = inferInstance

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.reconstruct {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (v : res.SurvivingCoordinate → T4) : Fin m → T4

Reconstruct an ambient internal tuple from exactly the surviving coordinates. Deleted coordinates are set to zero; residual factors read only surviving coordinates.

Equations

• res.reconstruct v i = if hi : i ∈ res.state.active then v ⟨i, hi⟩ else 0

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.reconstruct_surviving {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (v : res.SurvivingCoordinate → T4) (i : res.SurvivingCoordinate) : res.reconstruct v ↑i = v i

theorem Anderson4D.R324WithinHalfResidualPrefix.head_block_subset_active {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : head.2 ⊆ res.state.active

Every vertex of the literal schedule head is active before that head is absorbed.

@[reducible, inline]

abbrev Anderson4D.R324WithinHalfResidualPrefix.HeadCoordinate {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) : Type

Coordinates of the current head, still carrying their ambient labels.

Equations

• res.HeadCoordinate head = { i : res.SurvivingCoordinate // ↑i ∈ head.2 }

@[reducible, inline]

abbrev Anderson4D.R324WithinHalfResidualPrefix.OuterCoordinate {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) : Type

Coordinates outside the current head, still regarded as members of the pre-step surviving carrier.

Equations

• res.OuterCoordinate head = { i : res.SurvivingCoordinate // ↑i ∉ head.2 }

def Anderson4D.R324WithinHalfResidualPrefix.headCoordinateEquivStandard {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : res.HeadCoordinate head ≃ Fin (2 * residualBlockOrder head.2)

The ambiently-labelled head coordinates are exactly the standard primitive-block coordinate type.

Equations

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

def Anderson4D.R324WithinHalfResidualPrefix.outerCoordinateEquivPost {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : res.OuterCoordinate head ≃ (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate

The complement of the head in the pre-step carrier is exactly the post-absorb surviving coordinate type.

Equations

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

def Anderson4D.R324WithinHalfResidualPrefix.survivingCoordinateEquivHeadSumPost {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : res.SurvivingCoordinate ≃ Fin (2 * residualBlockOrder head.2) ⊕ (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate

Exact one-head partition of the current surviving coordinate type.

Equations

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

def Anderson4D.R324WithinHalfResidualPrefix.headSurvivingCoordinate {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (j : Fin (2 * residualBlockOrder head.2)) : res.SurvivingCoordinate

The current surviving coordinate corresponding to one standard head coordinate.

Equations

• res.headSurvivingCoordinate head tail hremaining j = ⟨↑((Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).blockOrderIso j), ⋯⟩

def Anderson4D.R324WithinHalfResidualPrefix.postSurvivingCoordinate {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (i : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate) : res.SurvivingCoordinate

Regard one post-absorb surviving coordinate as a coordinate of the pre-step surviving carrier.

Equations

• res.postSurvivingCoordinate head tail hremaining i = ⟨↑i, ⋯⟩

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.splitSurvivingPiMeasurableEquiv {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : (res.SurvivingCoordinate → T4) ≃ᵐ (Fin (2 * residualBlockOrder head.2) → T4) × ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4)

Split one current surviving tuple into the literal standard head tuple and the tuple surviving after absorb.

Equations

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

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.splitSurvivingPiMeasurableEquiv_apply_fst {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (v : res.SurvivingCoordinate → T4) (j : Fin (2 * residualBlockOrder head.2)) : ((res.splitSurvivingPiMeasurableEquiv head tail hremaining) v).1 j = v (res.headSurvivingCoordinate head tail hremaining j)

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.splitSurvivingPiMeasurableEquiv_apply_snd {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (v : res.SurvivingCoordinate → T4) (i : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate) : ((res.splitSurvivingPiMeasurableEquiv head tail hremaining) v).2 i = v (res.postSurvivingCoordinate head tail hremaining i)

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.splitSurvivingPiMeasurableEquiv_symm_head {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) (j : Fin (2 * residualBlockOrder head.2)) : (res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v) (res.headSurvivingCoordinate head tail hremaining j) = t j

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.splitSurvivingPiMeasurableEquiv_symm_post {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) (i : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate) : (res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v) (res.postSurvivingCoordinate head tail hremaining i) = v i

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.reconstruct_split_symm_block {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) (j : Fin (2 * residualBlockOrder head.2)) : res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v)) ↑((Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).blockOrderIso j) = t j

Reconstructing the pre-step ambient tuple after the exact split reads the standard head tuple literally.

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.reconstruct_split_symm_post {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) (i : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate) : res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v)) ↑i = (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v ↑i

Reconstructing the pre-step ambient tuple after the exact split agrees with the post-state reconstruction at every post-state surviving vertex.

theorem Anderson4D.R324WithinHalfResidualPrefix.measurePreserving_splitSurvivingPiMeasurableEquiv {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : MeasureTheory.MeasurePreserving (⇑(res.splitSurvivingPiMeasurableEquiv head tail hremaining)) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure) ((MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate) => paperMeasure))

The exact coordinate split preserves product Haar measure.

theorem Anderson4D.R324WithinHalfResidualPrefix.integral_splitSurviving {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : (res.SurvivingCoordinate → T4) → E) (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)) : (∫ (v : res.SurvivingCoordinate → T4), f v ∂MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure) = ∫ (t : Fin (2 * residualBlockOrder head.2) → T4), ∫ (v : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4), f ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v)) ∂MeasureTheory.Measure.pi fun (x : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate) => paperMeasure ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure

Fubini in the exact current-head/post-prefix coordinate split. The post-state appears only as the surviving coordinate space; the integrand itself is not rewritten pointwise in this theorem.