The actual first-left physical integral at the empty analytic prefix

This module factors the genuine first-left physical moment fibre in the branch where the selected block is the analytic head. The selected production Green factors and the complete primitive covariance sum are identified with the raw local integrand of the all-Green edge state after translation by the actual successor. The state is replaced only under the selected spatial integral.

Production endpoint factors

theorem Anderson4D.r324FirstLeft_selectRel_mem_extract {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : selectRel e₀.fst Finset.univ hleft ∈ extract e₀.fst

The first selected extraction pair belongs to the actual extraction list.

theorem Anderson4D.r324ProductionGreenEdgeFactor_outgoing_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) (xt : Fin (m + 2) → T4) : r324ProductionGreenEdgeFactor κ xt (r324FirstLeftOutgoingEdge e₀ hleft) = ↑(greenFn (xt (r324FirstLeftOutgoingEdge e₀ hleft).castSucc - xt (r324FirstLeftOutgoingEdge e₀ hleft).succ)) - ↑(greenFn (xt (varIdx (selectRel e₀.fst Finset.univ hleft).1) - xt (r324FirstLeftOutgoingEdge e₀ hleft).succ))

At the selected outgoing edge, the production shortcut is exactly the shortcut from the selected left endpoint.

theorem Anderson4D.r324FirstLeftPhysicalBlockTuple_zero {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) : r324FirstLeftPhysicalBlockTuple e₀ hleft v ⟨0, ⋯⟩ = assemble x y (r324LeftPhysicalTuple v) (varIdx (selectRel e₀.fst Finset.univ hleft).1)

The first physical block endpoint is the selected shortcut parent.

theorem Anderson4D.r324FirstLeftPhysicalBlockTuple_last {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) : r324FirstLeftPhysicalBlockTuple e₀ hleft v (primitiveLast (residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) ⋯) = assemble x y (r324LeftPhysicalTuple v) (r324FirstLeftOutgoingEdge e₀ hleft).castSucc

The last physical block endpoint is the left endpoint of the selected outgoing production edge.

theorem Anderson4D.r324FirstLeftPhysicalBlockTuple_zero_eq_predecessorSucc {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) : r324FirstLeftPhysicalBlockTuple e₀ hleft v ⟨0, ⋯⟩ = assemble x y (r324LeftPhysicalTuple v) (r324FirstLeftPredecessorEdge e₀ hleft).succ

theorem Anderson4D.r324FirstLeftTranslatedPhysicalBlockTuple_zero {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) : r324FirstLeftTranslatedPhysicalBlockTuple e₀ hleft x y v ⟨0, ⋯⟩ = assemble x y (r324LeftPhysicalTuple v) (r324FirstLeftPredecessorEdge e₀ hleft).succ - assemble x y (r324LeftPhysicalTuple v) (r324FirstLeftOutgoingEdge e₀ hleft).succ

theorem Anderson4D.r324FirstLeftTranslatedPhysicalBlockTuple_zero_eq_shortcutParent {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) : r324FirstLeftTranslatedPhysicalBlockTuple e₀ hleft x y v ⟨0, ⋯⟩ = assemble x y (r324LeftPhysicalTuple v) (varIdx (selectRel e₀.fst Finset.univ hleft).1) - assemble x y (r324LeftPhysicalTuple v) (r324FirstLeftOutgoingEdge e₀ hleft).succ

theorem Anderson4D.r324FirstLeftTranslatedPhysicalBlockTuple_last {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) : r324FirstLeftTranslatedPhysicalBlockTuple e₀ hleft x y v (primitiveLast (residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) ⋯) = assemble x y (r324LeftPhysicalTuple v) (r324FirstLeftOutgoingEdge e₀ hleft).castSucc - assemble x y (r324LeftPhysicalTuple v) (r324FirstLeftOutgoingEdge e₀ hleft).succ

theorem Anderson4D.r324FirstLeftTranslatedIncomingDifference {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) : r324FirstLeftPhysicalPredecessor e₀ hleft x y v - r324FirstLeftPhysicalSuccessor e₀ hleft x y v - r324FirstLeftTranslatedPhysicalBlockTuple e₀ hleft x y v ⟨0, ⋯⟩ = assemble x y (r324LeftPhysicalTuple v) (r324FirstLeftPredecessorEdge e₀ hleft).castSucc - assemble x y (r324LeftPhysicalTuple v) (r324FirstLeftPredecessorEdge e₀ hleft).succ

Translation ledgers

theorem Anderson4D.primitiveChainProduct_sub_const_r324 (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (t : Fin (2 * n) → T4) (a : T4) : (primitiveChainProduct n hn G fun (i : Fin (2 * n)) => t i - a) = primitiveChainProduct n hn G t

theorem Anderson4D.primitiveCovarianceProduct_sub_const_r324 (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (κ : PartialPairing (Fin (2 * n))) (t : Fin (2 * n) → T4) (a : T4) : (primitiveCovarianceProduct ρ ε n κ fun (i : Fin (2 * n)) => t i - a) = primitiveCovarianceProduct ρ ε n κ t

The physical outer factor after exposing the selected block

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

Every factor of the actual first-left physical integrand which is independent of the selected block coordinates.

Equations

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

The genuine initial local factor

theorem Anderson4D.r324FirstLeftInitialStepContext_rawLocalIntegrand {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (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) (u : T4) (t : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) → T4) : (r324FirstLeftInitialStepContext e₀ hleft tail hschedule).rawLocalIntegrand ρ ε u t = greenFn (u - t ⟨0, ⋯⟩) * primitiveChainProduct (residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) ⋯ (fun (x : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft) - 1)) => greenFn) t * (greenFn (t (primitiveLast (residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) ⋯)) - greenFn (t ⟨0, ⋯⟩)) * ∑ κB : R324FirstLeftBlockCoordinate e₀ hleft, primitiveCovarianceProduct ρ ε (residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) (↑κB) t

theorem Anderson4D.r324FirstLeftTouching_mul_primitiveSum_eq_initialRawLocal {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (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 : T4) (v : Fin (2 * m) → T4) : have κ₀ := ↑(firstBlockReferenceEndpointFiber e₀.fst hleft ω.fst); have xt := assemble x y (r324LeftPhysicalTuple v); let ctx := r324FirstLeftInitialStepContext e₀ hleft tail hschedule; have u := r324FirstLeftPhysicalPredecessor e₀ hleft x y v - r324FirstLeftPhysicalSuccessor e₀ hleft x y v; have t := r324FirstLeftTranslatedPhysicalBlockTuple e₀ hleft x y v; r324FirstLeftTouchingGreenProduct κ₀ e₀ hleft xt * ∑ κB : R324FirstLeftBlockCoordinate e₀ hleft, ↑(primitiveCovarianceProduct ρ ε (residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) (↑κB) (r324FirstLeftPhysicalBlockTuple e₀ hleft v)) = ↑(ctx.rawLocalIntegrand ρ ε u t)

At the empty analytic prefix, the touching production factors and the complete primitive covariance sum are exactly the translated raw local integrand. This is a pre-collapse identity: no processed state is asserted pointwise.

theorem Anderson4D.r324FirstLeftOuterFactor_mul_primitiveSum_eq_initialRaw_mul_outer {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) (v : Fin (2 * m) → T4) : let ctx := r324FirstLeftInitialStepContext e₀ hleft tail hschedule; have u := r324FirstLeftPhysicalPredecessor e₀ hleft x y v - r324FirstLeftPhysicalSuccessor e₀ hleft x y v; have t := r324FirstLeftTranslatedPhysicalBlockTuple e₀ hleft x y v; 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 ρ ε u t) * r324FirstLeftInitialPhysicalOuterFactor ρ ε α β e₀ hleft ω x y z w v

The actual first-left physical section is the honest empty-prefix raw local factor times factors exterior to the selected block.