Carrier-relative edges of the genuine first-left R-324 block

theorem Anderson4D.r324FirstLeft_selectedBlock_eq_Icc {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : selectedExtractionBlock e₀.fst Finset.univ hleft = Finset.Icc (selectRel e₀.fst Finset.univ hleft).1 (selectRel e₀.fst Finset.univ hleft).2

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

def Anderson4D.r324FirstLeftPredecessorEdge {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : Fin (m + 1)

Equations

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

def Anderson4D.r324FirstLeftOutgoingEdge {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : Fin (m + 1)

Equations

• Anderson4D.r324FirstLeftOutgoingEdge e₀ hleft = Anderson4D.extractedRightEdge (Anderson4D.selectRel e₀.fst Finset.univ hleft)

theorem Anderson4D.mem_r324FirstLeftShiftedBlock_iff_bounds {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (j : Fin (m + 2)) : j ∈ r324FirstLeftShiftedBlock e₀ hleft ↔ ↑(selectRel e₀.fst Finset.univ hleft).1 + 1 ≤ ↑j ∧ ↑j ≤ ↑(selectRel e₀.fst Finset.univ hleft).2 + 1

theorem Anderson4D.not_chainEdgeOutside_iff_firstLeft_range {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (edge : Fin (m + 1)) : ¬R324FirstLeftChainEdgeOutside e₀ hleft edge ↔ ↑(r324FirstLeftPredecessorEdge e₀ hleft) ≤ ↑edge ∧ ↑edge ≤ ↑(r324FirstLeftOutgoingEdge e₀ hleft)

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

Equations

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

theorem Anderson4D.r324FirstLeftTouchingGreenProduct_eq_edgeEnumeration {m : ℕ} (κ : PartialPairing (Fin m)) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (xt : Fin (m + 2) → T4) : r324FirstLeftTouchingGreenProduct κ e₀ hleft xt = ∏ k : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft) + 1), (originalGreenEdge xt (r324FirstLeftTouchingEdge e₀ hleft k) - extractedShortcutGreenEdge κ xt (r324FirstLeftTouchingEdge e₀ hleft k))

theorem Anderson4D.r324FirstLeftReconstruct_greenSkeleton_eq_carrierEdges {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) (x y : T4) (v : Fin (2 * m) → T4) : have κ := (↑(r324FirstLeftReconstruct e₀ hleft ω κB)).fst; have xt := assemble x y fun (i : Fin m) => v (leftMomentIndex i); renormalizedGreenSkeleton κ xt = (∏ k : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft) + 1), (originalGreenEdge xt (r324FirstLeftTouchingEdge e₀ hleft k) - extractedShortcutGreenEdge κ xt (r324FirstLeftTouchingEdge e₀ hleft k))) * r324FirstLeftExteriorGreenProduct κ e₀ hleft xt

theorem Anderson4D.extracted_predecessor_belongs_disjoint_analyticPrefix {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (hextracted : r324FirstLeftPredecessorEdge e₀ hleft ∈ extractedRightEdges e₀.fst) : ∃ (pre : List (R322ExtractionStep m)) (step : R322ExtractionStep m) (post : List (R322ExtractionStep m)), r322AnalyticSchedule e₀.fst = pre ++ r324FirstLeftSelectedStep e₀ hleft :: post ∧ step ∈ pre ∧ Disjoint step.2 (selectedExtractionBlock e₀.fst Finset.univ hleft) ∧ extractedRightEdge step.1 = r324FirstLeftPredecessorEdge e₀ hleft