Primitive local-factor form of the first-left production chain

theorem Anderson4D.r324FirstLeft_one_le_blockOrder {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : 1 ≤ residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)

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

Equations

• Anderson4D.r324FirstLeftCarrierTuple e₀ hleft xt i = xt ⟨↑(Anderson4D.selectRel e₀.fst Finset.univ hleft).1 + 1 + ↑i, ⋯⟩

def Anderson4D.r324FirstLeftInternalEdge {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) - 1)) : Fin (m + 1)

Equations

• Anderson4D.r324FirstLeftInternalEdge e₀ hleft j = ⟨↑(Anderson4D.selectRel e₀.fst Finset.univ hleft).1 + 1 + ↑j, ⋯⟩

noncomputable def Anderson4D.r324ProductionGreenEdgeFactor {m : ℕ} (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) (edge : Fin (m + 1)) : ℂ

Equations

• Anderson4D.r324ProductionGreenEdgeFactor κ xt edge = Anderson4D.originalGreenEdge xt edge - Anderson4D.extractedShortcutGreenEdge κ xt edge

def Anderson4D.r324FirstLeftInternalVertexLeft {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) - 1)) : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft))

Equations

• Anderson4D.r324FirstLeftInternalVertexLeft e₀ hleft j = ⟨↑j, ⋯⟩

def Anderson4D.r324FirstLeftInternalVertexRight {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) - 1)) : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft))

Equations

• Anderson4D.r324FirstLeftInternalVertexRight e₀ hleft j = ⟨↑j + 1, ⋯⟩

@[simp]

theorem Anderson4D.touchingEdge_zero_eq_predecessor {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : r324FirstLeftTouchingEdge e₀ hleft 0 = r324FirstLeftPredecessorEdge e₀ hleft

theorem Anderson4D.r324FirstLeftInternalEdge_not_extracted_reference {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) - 1)) : r324FirstLeftInternalEdge e₀ hleft j ∉ extractedRightEdges e₀.fst

theorem Anderson4D.r324FirstLeftInternalEdge_not_extracted {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) (j : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft) - 1)) : r324FirstLeftInternalEdge e₀ hleft j ∉ extractedRightEdges κ

theorem Anderson4D.productionInternalFactor_eq_primitiveEdge {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) (j : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft) - 1)) : r324ProductionGreenEdgeFactor κ xt (r324FirstLeftInternalEdge e₀ hleft j) = ↑(greenFn (r324FirstLeftCarrierTuple e₀ hleft xt (r324FirstLeftInternalVertexLeft e₀ hleft j) - r324FirstLeftCarrierTuple e₀ hleft xt (r324FirstLeftInternalVertexRight e₀ hleft j)))

theorem Anderson4D.r324FirstLeftTouchingGreenProduct_eq_primitiveLocal {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) : r324FirstLeftTouchingGreenProduct κ e₀ hleft xt = r324ProductionGreenEdgeFactor κ xt (r324FirstLeftPredecessorEdge e₀ hleft) * ↑(primitiveChainProduct (residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) ⋯ (fun (x : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft) - 1)) => greenFn) (r324FirstLeftCarrierTuple e₀ hleft xt)) * r324ProductionGreenEdgeFactor κ xt (r324FirstLeftOutgoingEdge e₀ hleft)

theorem Anderson4D.r324FirstLeftReconstruct_touchingGreenProduct_eq_primitiveLocal {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ω : R324FirstLeftOuterCoordinate e₀ hleft) (κB : R324FirstLeftBlockCoordinate e₀ hleft) (xt : Fin (m + 2) → T4) : have κ := (↑(r324FirstLeftReconstruct e₀ hleft ω κB)).fst; r324FirstLeftTouchingGreenProduct κ e₀ hleft xt = r324ProductionGreenEdgeFactor κ xt (r324FirstLeftPredecessorEdge e₀ hleft) * ↑(primitiveChainProduct (residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) ⋯ (fun (x : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft) - 1)) => greenFn) (r324FirstLeftCarrierTuple e₀ hleft xt)) * r324ProductionGreenEdgeFactor κ xt (r324FirstLeftOutgoingEdge e₀ hleft)