Evolving heterogeneous edges for R-322

A proper sparse-carrier step updates the greatest active predecessor slot.

theorem Anderson4D.r322AnalyticProperStep_endpoint_bounds {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (pre suffix : List (R322ExtractionStep (2 * q))) (step : R322ExtractionStep (2 * q)) (hschedule : r322AnalyticSchedule κ = pre ++ step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) : 0 < ↑step.1.1 ∧ ↑step.1.2 < 2 * q - 1

Bounds for any proper step, not only the first scheduled step.

structure Anderson4D.R322AnalyticEdgeState (q : ℕ) (hq : 1 ≤ q) : Type

Processed prefix, heterogeneous edges, and surviving global endpoints.

• processed : List (R322ExtractionStep (2 * q))
• edges : Fin (2 * q - 1) → T4 → ℝ
• zero_mem : ⟨0, ⋯⟩ ∈ r322AnalyticActiveCarrier self.processed
• last_mem : ⟨2 * q - 1, ⋯⟩ ∈ r322AnalyticActiveCarrier self.processed

def Anderson4D.R322AnalyticEdgeState.active {q : ℕ} {hq : 1 ≤ q} (state : R322AnalyticEdgeState q hq) : Finset (Fin (2 * q))

The active carrier derived from the processed prefix.

Equations

• state.active = Anderson4D.r322AnalyticActiveCarrier state.processed

noncomputable def Anderson4D.r322InitialAnalyticEdgeState (q : ℕ) (hq : 1 ≤ q) : R322AnalyticEdgeState q hq

Initial all-free-Green state.

Equations

• Anderson4D.r322InitialAnalyticEdgeState q hq = { processed := [], edges := fun (x : Fin (2 * q - 1)) => Anderson4D.greenFn, zero_mem := ⋯, last_mem := ⋯ }

def Anderson4D.r322AnalyticPredecessorCandidates {q : ℕ} {hq : 1 ≤ q} (state : R322AnalyticEdgeState q hq) (step : R322ExtractionStep (2 * q)) : Finset (Fin (2 * q))

Active vertices strictly before the next left endpoint.

Equations

• Anderson4D.r322AnalyticPredecessorCandidates state step = {i ∈ state.active | i < step.1.1}

theorem Anderson4D.r322AnalyticPredecessorCandidates_nonempty {q : ℕ} {hq : 1 ≤ q} (state : R322AnalyticEdgeState q hq) (step : R322ExtractionStep (2 * q)) (hleft : 0 < ↑step.1.1) : (r322AnalyticPredecessorCandidates state step).Nonempty

def Anderson4D.r322AnalyticPredecessorVertex {q : ℕ} {hq : 1 ≤ q} (state : R322AnalyticEdgeState q hq) (step : R322ExtractionStep (2 * q)) (hleft : 0 < ↑step.1.1) : Fin (2 * q)

Greatest active vertex before the next block.

Equations

• Anderson4D.r322AnalyticPredecessorVertex state step hleft = (Anderson4D.r322AnalyticPredecessorCandidates state step).max' ⋯

theorem Anderson4D.r322AnalyticPredecessorVertex_mem_active {q : ℕ} {hq : 1 ≤ q} (state : R322AnalyticEdgeState q hq) (step : R322ExtractionStep (2 * q)) (hleft : 0 < ↑step.1.1) : r322AnalyticPredecessorVertex state step hleft ∈ state.active

theorem Anderson4D.r322AnalyticPredecessorVertex_lt_left {q : ℕ} {hq : 1 ≤ q} (state : R322AnalyticEdgeState q hq) (step : R322ExtractionStep (2 * q)) (hleft : 0 < ↑step.1.1) : r322AnalyticPredecessorVertex state step hleft < step.1.1

theorem Anderson4D.r322AnalyticPredecessorVertex_maximal {q : ℕ} {hq : 1 ≤ q} (state : R322AnalyticEdgeState q hq) (step : R322ExtractionStep (2 * q)) (hleft : 0 < ↑step.1.1) (i : Fin (2 * q)) (hi : i ∈ state.active) (hil : i < step.1.1) : i ≤ r322AnalyticPredecessorVertex state step hleft

No active vertex lies strictly between the chosen predecessor and the left endpoint.

def Anderson4D.r322AnalyticPredecessorEdge {q : ℕ} {hq : 1 ≤ q} (state : R322AnalyticEdgeState q hq) (step : R322ExtractionStep (2 * q)) (hleft : 0 < ↑step.1.1) : Fin (2 * q - 1)

Ambient left-edge slot carried by the sparse predecessor.

Equations

• Anderson4D.r322AnalyticPredecessorEdge state step hleft = ⟨↑(Anderson4D.r322AnalyticPredecessorVertex state step hleft), ⋯⟩

def Anderson4D.r322AnalyticEdgeLeftVertex {q : ℕ} (edge : Fin (2 * q - 1)) : Fin (2 * q)

Regard an ambient edge slot as its left vertex.

Equations

• Anderson4D.r322AnalyticEdgeLeftVertex edge = ⟨↑edge, ⋯⟩

@[simp]

theorem Anderson4D.r322AnalyticEdgeLeftVertex_predecessorEdge {q : ℕ} {hq : 1 ≤ q} (state : R322AnalyticEdgeState q hq) (step : R322ExtractionStep (2 * q)) (hleft : 0 < ↑step.1.1) : r322AnalyticEdgeLeftVertex (r322AnalyticPredecessorEdge state step hleft) = r322AnalyticPredecessorVertex state step hleft

def Anderson4D.r322AnalyticOutgoingEdge {q : ℕ} (step : R322ExtractionStep (2 * q)) (hright : ↑step.1.2 < 2 * q - 1) : Fin (2 * q - 1)

The outgoing edge of a proper block is still indexed by its right endpoint before that endpoint is deleted.

Equations

• Anderson4D.r322AnalyticOutgoingEdge step hright = ⟨↑step.1.2, hright⟩

noncomputable def Anderson4D.R322AnalyticEdgeState.updateProper {q : ℕ} {hq : 1 ≤ q} (state : R322AnalyticEdgeState q hq) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (suffix : List (R322ExtractionStep (2 * q))) (step : R322ExtractionStep (2 * q)) (hschedule : r322AnalyticSchedule κ = state.processed ++ step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (J : T4 → ℝ) : R322AnalyticEdgeState q hq

One proper sparse-carrier update.

Equations

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

@[simp]

theorem Anderson4D.R322AnalyticEdgeState.updateProper_processed {q : ℕ} {hq : 1 ≤ q} (state : R322AnalyticEdgeState q hq) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (suffix : List (R322ExtractionStep (2 * q))) (step : R322ExtractionStep (2 * q)) (hschedule : r322AnalyticSchedule κ = state.processed ++ step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (J : T4 → ℝ) : (state.updateProper κ hκ suffix step hschedule hproper J).processed = state.processed ++ [step]

theorem Anderson4D.R322AnalyticEdgeState.updateProper_active {q : ℕ} {hq : 1 ≤ q} (state : R322AnalyticEdgeState q hq) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (suffix : List (R322ExtractionStep (2 * q))) (step : R322ExtractionStep (2 * q)) (hschedule : r322AnalyticSchedule κ = state.processed ++ step :: suffix) (hproper : step.1 ≠ r322WholeEndpoint q hq) (J : T4 → ℝ) : (state.updateProper κ hκ suffix step hschedule hproper J).active = state.active \ step.2