Physical coordinates at an R-324 first-left processed step

The first-left routing theorem exposes the actual selected coordinates of the original deterministic moment fibre. The collapse theorem, on the other hand, is written in a standard Fin (2n) coordinate with the active successor translated to zero. This file supplies that coordinate bridge.

No unintegrated original integrand is identified with a state after an earlier block has already been integrated. The pointwise statements below only reconstruct the current, still unintegrated block. State replacement is performed only under the corresponding spatial integral.

The selected physical tuple

def Anderson4D.r324LeftPhysicalTuple {m : ℕ} (v : Fin (2 * m) → T4) : Fin m → T4

The left-copy spatial tuple inside the doubled moment coordinate.

Equations

• Anderson4D.r324LeftPhysicalTuple v i = v (Anderson4D.leftMomentIndex i)

def Anderson4D.r324FirstLeftPhysicalBlockTuple {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (v : Fin (2 * m) → T4) : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) → T4

The canonical standard tuple of the genuine first-left block.

Equations

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

noncomputable def Anderson4D.r324FirstLeftPhysicalReconstruct {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) : Fin (2 * m) → T4

Reassemble a doubled physical tuple from a fixed complementary tuple and a canonical standard tuple on the genuine first-left block.

Equations

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

@[simp]

theorem Anderson4D.r324FirstLeftPhysicalBlockTuple_reconstruct {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) : r324FirstLeftPhysicalBlockTuple e₀ hleft (r324FirstLeftPhysicalReconstruct e₀ hleft vC t) = t

Actual coordinate reconstruction reads the supplied standard tuple back on the genuine first-left block.

Literal production-chain coordinates

theorem Anderson4D.r324FirstLeft_residualOrderIso_apply_val {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (j : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft))) : ↑↑((residualPrimitiveBlockOrderIso e₀.fst (selectedExtractionBlock e₀.fst Finset.univ hleft) ⋯) j) = ↑(selectRel e₀.fst Finset.univ hleft).1 + ↑j

The canonical increasing enumeration of the genuine first-left interval is the literal affine enumeration from its selected left endpoint.

theorem Anderson4D.r324FirstLeftCarrierTuple_assemble_eq_physicalBlockTuple {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (x y : T4) (v : Fin (2 * m) → T4) : r324FirstLeftCarrierTuple e₀ hleft (assemble x y (r324LeftPhysicalTuple v)) = r324FirstLeftPhysicalBlockTuple e₀ hleft v

The physical block tuple is exactly the selected carrier tuple in the assembled production Green chain.

The honest empty-prefix state

noncomputable def Anderson4D.r324FirstLeftInitialStepContext {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (tail : List (R322ExtractionStep m)) (hschedule : r322AnalyticSchedule e₀.fst = r324FirstLeftSelectedStep e₀ hleft :: tail) : R324WithinHalfStepContext e₀.fst

The genuine selected block as a certified step from the all-Green initial state, in the branch where it is the analytic head.

Equations

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

def Anderson4D.r324FirstLeftPhysicalSuccessor {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (x y : T4) (v : Fin (2 * m) → T4) : T4

The actual production-chain point immediately after the selected first-left block.

Equations

• Anderson4D.r324FirstLeftPhysicalSuccessor e₀ hleft x y v = Anderson4D.assemble x y (Anderson4D.r324LeftPhysicalTuple v) (Anderson4D.r324FirstLeftOutgoingEdge e₀ hleft).succ

def Anderson4D.r324FirstLeftPhysicalPredecessor {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (x y : T4) (v : Fin (2 * m) → T4) : T4

The actual production-chain point immediately before the selected first-left block.

Equations

• Anderson4D.r324FirstLeftPhysicalPredecessor e₀ hleft x y v = Anderson4D.assemble x y (Anderson4D.r324LeftPhysicalTuple v) (Anderson4D.r324FirstLeftPredecessorEdge e₀ hleft).castSucc

noncomputable def Anderson4D.r324FirstLeftTranslatedPhysicalBlockTuple {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (x y : T4) (v : Fin (2 * m) → T4) : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) → T4

Translation-normalized physical first-left tuple.

Equations

• Anderson4D.r324FirstLeftTranslatedPhysicalBlockTuple e₀ hleft x y v i = Anderson4D.r324FirstLeftPhysicalBlockTuple e₀ hleft v i - Anderson4D.r324FirstLeftPhysicalSuccessor e₀ hleft x y v

Complex outer factors

theorem Anderson4D.R324WithinHalfStepContext.rawLocalSpatialIntegral_mul_complexOuter_eq_absorb {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (ρ : SmoothCutoff) (lam ε : ℝ) (u : T4) (outer : ℂ) (hstandard : MeasureTheory.Integrable (ctx.localIntegrand ρ ε u) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure)) (hinternal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2))), MeasureTheory.Integrable (fun (v : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.step.2) (↑κB) ctx.internalEdges (primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ p.1 p.2 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure)) : (↑(lamEps lam ε) ^ (2 * residualBlockOrder ctx.step.2) * ∫ (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) = ↑((ctx.absorb ρ lam ε).edges (r324WithinHalfPredecessorSlot ctx.state ctx.step) u) * outer

The real processed collapse may carry the complex outer factor of the physical moment integrand. The state changes only under the local spatial integral.

theorem Anderson4D.R324WithinHalfStepContext.integral_outer_rawLocalIntegrand_complex_eq_absorb {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.Measure Ω) (ρ : SmoothCutoff) (lam ε : ℝ) (u : Ω → T4) (outer : Ω → ℂ) (hstandard : ∀ᵐ (ω : Ω) ∂ν, MeasureTheory.Integrable (ctx.localIntegrand ρ ε (u ω)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure)) (hinternal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2))), MeasureTheory.Integrable (fun (v : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.step.2) (↑κB) ctx.internalEdges (primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ p.1 p.2 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure)) : ∫ (ω : Ω), ↑(lamEps lam ε) ^ (2 * residualBlockOrder ctx.step.2) * ∫ (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 ∂ν = ∫ (ω : Ω), ↑((ctx.absorb ρ lam ε).edges (r324WithinHalfPredecessorSlot ctx.state ctx.step) (u ω)) * outer ω ∂ν

Outer-Fubini form of the complex physical update.