Complement independence and the first physical R-324 collapse

This module keeps the genuine first-left physical fibre while proving that the factor exposed outside its selected block is a function of the complementary coordinates alone. It then reindexes the selected coordinate, translates it, and invokes the honest complex outer-Fubini collapse.

Reading reconstructed complementary coordinates

@[simp]

theorem Anderson4D.r324FirstLeftPhysicalReconstruct_complement {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (vC : { i : Fin (2 * m) // ¬r324FirstLeftSelected e₀ hleft i } → T4) (t : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) → T4) (i : { i : Fin (2 * m) // ¬r324FirstLeftSelected e₀ hleft i }) : r324FirstLeftPhysicalReconstruct e₀ hleft vC t ↑i = vC i

theorem Anderson4D.r324FirstLeftPhysicalReconstruct_eq_of_not_selected {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (vC : { i : Fin (2 * m) // ¬r324FirstLeftSelected e₀ hleft i } → T4) (t t' : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) → T4) (i : Fin (2 * m)) (hi : ¬r324FirstLeftSelected e₀ hleft i) : r324FirstLeftPhysicalReconstruct e₀ hleft vC t i = r324FirstLeftPhysicalReconstruct e₀ hleft vC t' i

theorem Anderson4D.leftMomentIndex_not_selected_of_not_mem {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (i : Fin m) (hi : i ∉ selectedExtractionBlock e₀.fst Finset.univ hleft) : ¬r324FirstLeftSelected e₀ hleft (leftMomentIndex i)

theorem Anderson4D.rightMomentIndex_not_firstLeftSelected {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (i : Fin m) : ¬r324FirstLeftSelected e₀ hleft (rightMomentIndex i)

Exterior production-chain reads

theorem Anderson4D.assemble_leftPhysicalReconstruct_eq_of_not_shifted {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (vC : { i : Fin (2 * m) // ¬r324FirstLeftSelected e₀ hleft i } → T4) (t t' : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) → T4) (x y : T4) (j : Fin (m + 2)) (hj : j ∉ r324FirstLeftShiftedBlock e₀ hleft) : assemble x y (r324LeftPhysicalTuple (r324FirstLeftPhysicalReconstruct e₀ hleft vC t)) j = assemble x y (r324LeftPhysicalTuple (r324FirstLeftPhysicalReconstruct e₀ hleft vC t')) j

theorem Anderson4D.r324FirstLeft_extractedShortcutParent_not_shifted {m : ℕ} (κ : PartialPairing (Fin m)) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (hsig : reductionEndpointSignature κ = reductionEndpointSignature e₀.fst) (edge : Fin (m + 1)) (hi : edge ∈ extractedRightEdges κ) (hout : R324FirstLeftChainEdgeOutside e₀ hleft edge) : Fin.castLE ⋯ (extractedShortcutParent κ edge hi) ∉ r324FirstLeftShiftedBlock e₀ hleft

theorem Anderson4D.r324FirstLeftExteriorGreenProduct_physicalReconstruct_eq {m : ℕ} (κ : PartialPairing (Fin m)) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (hsig : reductionEndpointSignature κ = reductionEndpointSignature e₀.fst) (vC : { i : Fin (2 * m) // ¬r324FirstLeftSelected e₀ hleft i } → T4) (t t' : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) → T4) (x y : T4) : r324FirstLeftExteriorGreenProduct κ e₀ hleft (assemble x y (r324LeftPhysicalTuple (r324FirstLeftPhysicalReconstruct e₀ hleft vC t))) = r324FirstLeftExteriorGreenProduct κ e₀ hleft (assemble x y (r324LeftPhysicalTuple (r324FirstLeftPhysicalReconstruct e₀ hleft vC t')))

theorem Anderson4D.r324FirstLeftPredecessorVertex_not_shifted {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : (r324FirstLeftPredecessorEdge e₀ hleft).castSucc ∉ r324FirstLeftShiftedBlock e₀ hleft

theorem Anderson4D.r324FirstLeftSuccessorVertex_not_shifted {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : (r324FirstLeftOutgoingEdge e₀ hleft).succ ∉ r324FirstLeftShiftedBlock e₀ hleft

theorem Anderson4D.r324FirstLeftPhysicalPredecessor_reconstruct_eq {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (vC : { i : Fin (2 * m) // ¬r324FirstLeftSelected e₀ hleft i } → T4) (t t' : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) → T4) (x y : T4) : r324FirstLeftPhysicalPredecessor e₀ hleft x y (r324FirstLeftPhysicalReconstruct e₀ hleft vC t) = r324FirstLeftPhysicalPredecessor e₀ hleft x y (r324FirstLeftPhysicalReconstruct e₀ hleft vC t')

theorem Anderson4D.r324FirstLeftPhysicalSuccessor_reconstruct_eq {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (vC : { i : Fin (2 * m) // ¬r324FirstLeftSelected e₀ hleft i } → T4) (t t' : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) → T4) (x y : T4) : r324FirstLeftPhysicalSuccessor e₀ hleft x y (r324FirstLeftPhysicalReconstruct e₀ hleft vC t) = r324FirstLeftPhysicalSuccessor e₀ hleft x y (r324FirstLeftPhysicalReconstruct e₀ hleft vC t')

Covariance factors on complementary coordinates

theorem Anderson4D.pairingCovarianceProductOn_complement_physicalReconstruct_eq {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin m)) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (hfull : IsFullyPairedOn κ (selectedExtractionBlock e₀.fst Finset.univ hleft)) (vC : { i : Fin (2 * m) // ¬r324FirstLeftSelected e₀ hleft i } → T4) (t t' : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) → T4) : (pairingCovarianceProductOn ρ ε κ (Finset.univ \ selectedExtractionBlock e₀.fst Finset.univ hleft) fun (i : Fin m) => r324FirstLeftPhysicalReconstruct e₀ hleft vC t (leftMomentIndex i)) = pairingCovarianceProductOn ρ ε κ (Finset.univ \ selectedExtractionBlock e₀.fst Finset.univ hleft) fun (i : Fin m) => r324FirstLeftPhysicalReconstruct e₀ hleft vC t' (leftMomentIndex i)

theorem Anderson4D.rightPhysicalTuple_reconstruct_eq {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (vC : { i : Fin (2 * m) // ¬r324FirstLeftSelected e₀ hleft i } → T4) (t t' : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) → T4) : (fun (i : Fin m) => r324FirstLeftPhysicalReconstruct e₀ hleft vC t (rightMomentIndex i)) = fun (i : Fin m) => r324FirstLeftPhysicalReconstruct e₀ hleft vC t' (rightMomentIndex i)

theorem Anderson4D.momentCrossCovarianceProduct_physicalReconstruct_eq {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (hfull : IsFullyPairedOn κp (selectedExtractionBlock e₀.fst Finset.univ hleft)) (vC : { i : Fin (2 * m) // ¬r324FirstLeftSelected e₀ hleft i } → T4) (t t' : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) → T4) : momentCrossCovarianceProduct ρ ε m κp κm π (r324FirstLeftPhysicalReconstruct e₀ hleft vC t) = momentCrossCovarianceProduct ρ ε m κp κm π (r324FirstLeftPhysicalReconstruct e₀ hleft vC t')

theorem Anderson4D.firstBlockReferenceEndpointFiber_isFullyPairedOn_selected {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ω : R324FirstLeftOuterCoordinate e₀ hleft) (tail : List (R322ExtractionStep m)) (hschedule : r322AnalyticSchedule e₀.fst = r324FirstLeftSelectedStep e₀ hleft :: tail) : IsFullyPairedOn (↑(firstBlockReferenceEndpointFiber e₀.fst hleft ω.fst)) (selectedExtractionBlock e₀.fst Finset.univ hleft)

theorem Anderson4D.r324FirstLeftInitialPhysicalOuterFactor_reconstruct_eq {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (α β : Z4) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ω : R324FirstLeftOuterCoordinate e₀ hleft) (tail : List (R322ExtractionStep m)) (hschedule : r322AnalyticSchedule e₀.fst = r324FirstLeftSelectedStep e₀ hleft :: tail) (x y z w : T4) (vC : { i : Fin (2 * m) // ¬r324FirstLeftSelected e₀ hleft i } → T4) (t t' : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) → T4) : r324FirstLeftInitialPhysicalOuterFactor ρ ε α β e₀ hleft ω x y z w (r324FirstLeftPhysicalReconstruct e₀ hleft vC t) = r324FirstLeftInitialPhysicalOuterFactor ρ ε α β e₀ hleft ω x y z w (r324FirstLeftPhysicalReconstruct e₀ hleft vC t')

Haar translation to successor-relative coordinates

noncomputable def Anderson4D.R324WithinHalfStepContext.physicalBlockTranslation {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (a : T4) : (Fin (2 * residualBlockOrder ctx.step.2) → T4) ≃ᵐ (Fin (2 * residualBlockOrder ctx.step.2) → T4)

Equations

• ctx.physicalBlockTranslation a = MeasurableEquiv.piCongrRight fun (x : Fin (2 * Anderson4D.residualBlockOrder ctx.step.2)) => MeasurableEquiv.addRight a

@[simp]

theorem Anderson4D.R324WithinHalfStepContext.physicalBlockTranslation_apply {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (a : T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : (ctx.physicalBlockTranslation a) t = fun (j : Fin (2 * residualBlockOrder ctx.step.2)) => t j + a

theorem Anderson4D.R324WithinHalfStepContext.measurePreserving_physicalBlockTranslation {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (a : T4) : MeasureTheory.MeasurePreserving (⇑(ctx.physicalBlockTranslation a)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure)

theorem Anderson4D.R324WithinHalfStepContext.integral_rawLocal_sub_const_mul_complex {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (ρ : SmoothCutoff) (ε : ℝ) (u a : T4) (outer : ℂ) : (∫ (actual : Fin (2 * residualBlockOrder ctx.step.2) → T4), ↑(ctx.rawLocalIntegrand ρ ε u fun (i : Fin (2 * residualBlockOrder ctx.step.2)) => actual i - a) * outer ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure) = ∫ (t : Fin (2 * residualBlockOrder ctx.step.2) → T4), ↑(ctx.rawLocalIntegrand ρ ε u t) * outer ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure

Complement-only data for the actual selected section

noncomputable def Anderson4D.r324FirstLeftComplementBaseTuple {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (vC : { i : Fin (2 * m) // ¬r324FirstLeftSelected e₀ hleft i } → T4) : Fin (2 * m) → T4

Equations

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

noncomputable def Anderson4D.r324FirstLeftComplementSuccessor {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (x y : T4) (vC : { i : Fin (2 * m) // ¬r324FirstLeftSelected e₀ hleft i } → T4) : T4

Equations

• Anderson4D.r324FirstLeftComplementSuccessor e₀ hleft x y vC = Anderson4D.r324FirstLeftPhysicalSuccessor e₀ hleft x y (Anderson4D.r324FirstLeftComplementBaseTuple e₀ hleft vC)

noncomputable def Anderson4D.r324FirstLeftComplementDisplacement {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (x y : T4) (vC : { i : Fin (2 * m) // ¬r324FirstLeftSelected e₀ hleft i } → T4) : T4

Equations

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

noncomputable def Anderson4D.r324FirstLeftComplementOuter {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (α β : Z4) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ω : R324FirstLeftOuterCoordinate e₀ hleft) (x y z w : T4) (vC : { i : Fin (2 * m) // ¬r324FirstLeftSelected e₀ hleft i } → T4) : ℂ

Equations

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

theorem Anderson4D.r324FirstLeftPhysicalSection_reconstruct_eq_relativeRaw {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (α β : Z4) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ω : R324FirstLeftOuterCoordinate e₀ hleft) (tail : List (R322ExtractionStep m)) (hschedule : r322AnalyticSchedule e₀.fst = r324FirstLeftSelectedStep e₀ hleft :: tail) (x y z w : T4) (vC : { i : Fin (2 * m) // ¬r324FirstLeftSelected e₀ hleft i } → T4) (t : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) → T4) : have v := r324FirstLeftPhysicalReconstruct e₀ hleft vC t; let ctx := r324FirstLeftInitialStepContext e₀ hleft tail hschedule; r324FirstLeftOuterFactor ρ ε α β e₀ hleft ω x y z w v * ∑ κB : R324FirstLeftBlockCoordinate e₀ hleft, ↑(primitiveCovarianceProduct ρ ε (residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) (↑κB) (r324FirstLeftPhysicalBlockTuple e₀ hleft v)) = ↑(ctx.rawLocalIntegrand ρ ε (r324FirstLeftComplementDisplacement e₀ hleft x y vC) fun (i : Fin (2 * residualBlockOrder ctx.step.2)) => t i - r324FirstLeftComplementSuccessor e₀ hleft x y vC) * r324FirstLeftComplementOuter ρ ε α β e₀ hleft ω x y z w vC

After genuine physical reconstruction, the original selected section is the translated empty-prefix raw local integrand times complement-only data.

noncomputable def Anderson4D.r324FirstLeftSelectedPhysicalSection {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (α β : Z4) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ω : R324FirstLeftOuterCoordinate e₀ hleft) (x y z w : T4) (vC : { i : Fin (2 * m) // ¬r324FirstLeftSelected e₀ hleft i } → T4) (vB : { i : Fin (2 * m) // r324FirstLeftSelected e₀ hleft i } → T4) : ℂ

Equations

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

theorem Anderson4D.r324FirstLeftSelectedPhysicalSection_standardBlock {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (α β : Z4) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ω : R324FirstLeftOuterCoordinate e₀ hleft) (x y z w : T4) (vC : { i : Fin (2 * m) // ¬r324FirstLeftSelected e₀ hleft i } → T4) (t : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) → T4) : r324FirstLeftSelectedPhysicalSection ρ ε α β e₀ hleft ω x y z w vC ((r324FirstLeftSelectedTupleMeasurableEquiv e₀ hleft) t) = have v := r324FirstLeftPhysicalReconstruct e₀ hleft vC t; r324FirstLeftOuterFactor ρ ε α β e₀ hleft ω x y z w v * ∑ κB : R324FirstLeftBlockCoordinate e₀ hleft, ↑(primitiveCovarianceProduct ρ ε (residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) (↑κB) (r324FirstLeftPhysicalBlockTuple e₀ hleft v))

theorem Anderson4D.integral_r324FirstLeftSelectedPhysicalSection_eq_initialRaw {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (α β : Z4) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ω : R324FirstLeftOuterCoordinate e₀ hleft) (tail : List (R322ExtractionStep m)) (hschedule : r322AnalyticSchedule e₀.fst = r324FirstLeftSelectedStep e₀ hleft :: tail) (x y z w : T4) (vC : { i : Fin (2 * m) // ¬r324FirstLeftSelected e₀ hleft i } → T4) : (∫ (vB : { i : Fin (2 * m) // r324FirstLeftSelected e₀ hleft i } → T4), r324FirstLeftSelectedPhysicalSection ρ ε α β e₀ hleft ω x y z w vC vB ∂MeasureTheory.Measure.pi fun (x : { i : Fin (2 * m) // r324FirstLeftSelected e₀ hleft i }) => paperMeasure) = ∫ (t : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) → T4), ↑((r324FirstLeftInitialStepContext e₀ hleft tail hschedule).rawLocalIntegrand ρ ε (r324FirstLeftComplementDisplacement e₀ hleft x y vC) t) * r324FirstLeftComplementOuter ρ ε α β e₀ hleft ω x y z w vC ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft))) => paperMeasure

Reindexing the genuine selected doubled coordinates and translating by the complement-determined successor gives the exact raw local integral.

theorem Anderson4D.lamEps_pow_integral_r324FirstLeftSelectedPhysicalSection_eq_initialAbsorb {m : ℕ} (ρ : SmoothCutoff) (lam ε : ℝ) (α β : Z4) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ω : R324FirstLeftOuterCoordinate e₀ hleft) (tail : List (R322ExtractionStep m)) (hschedule : r322AnalyticSchedule e₀.fst = r324FirstLeftSelectedStep e₀ hleft :: tail) (x y z w : T4) (vC : { i : Fin (2 * m) // ¬r324FirstLeftSelected e₀ hleft i } → T4) (hstandard : MeasureTheory.Integrable ((r324FirstLeftInitialStepContext e₀ hleft tail hschedule).localIntegrand ρ ε (r324FirstLeftComplementDisplacement e₀ hleft x y vC)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder (r324FirstLeftInitialStepContext e₀ hleft tail hschedule).step.2)) => paperMeasure)) (hinternal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : R324FirstLeftBlockCoordinate e₀ hleft), MeasureTheory.Integrable (fun (v : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft) - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) (↑κB) (r324FirstLeftInitialStepContext e₀ hleft tail hschedule).internalEdges (primitiveAssemble (residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) ⋯ p.1 p.2 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft) - 2)) => paperMeasure)) : (↑(lamEps lam ε) ^ (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) * ∫ (vB : { i : Fin (2 * m) // r324FirstLeftSelected e₀ hleft i } → T4), r324FirstLeftSelectedPhysicalSection ρ ε α β e₀ hleft ω x y z w vC vB ∂MeasureTheory.Measure.pi fun (x : { i : Fin (2 * m) // r324FirstLeftSelected e₀ hleft i }) => paperMeasure) = ↑(((r324FirstLeftInitialStepContext e₀ hleft tail hschedule).absorb ρ lam ε).edges (r324WithinHalfPredecessorSlot (r324FirstLeftInitialStepContext e₀ hleft tail hschedule).state (r324FirstLeftInitialStepContext e₀ hleft tail hschedule).step) (r324FirstLeftComplementDisplacement e₀ hleft x y vC)) * r324FirstLeftComplementOuter ρ ε α β e₀ hleft ω x y z w vC

Actual first-left physical selected integral = initial absorbed integral.

The left side is the selected section occurring literally in the routed physical moment fibre. The right side is the genuine all-Green initial edge state after one R324WithinHalfStepContext.absorb. The state change occurs only after the selected spatial integral.