Free outgoing edges along the R-322 collapse schedule #
The analytic schedule has strictly increasing right endpoints. A proper collapse only replaces its predecessor edge, which lies strictly to the left of the collapsed block. Consequently every edge strictly to the right of all processed right endpoints is still the original Green kernel. In particular, the outgoing edge of the next scheduled block is free.
theorem
Anderson4D.R322AnalyticEdgeState.updateProper_edges_eq_of_right_lt
{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 → ℝ)
(edge : Fin (2 * q - 1))
(hright : step.1.2 < r322AnalyticEdgeLeftVertex edge)
:
A proper update does not alter an edge lying strictly to the right of the current block's right endpoint.
theorem
Anderson4D.R322AnalyticAbsorbedState.edge_eq_greenFn_of_processed_right_lt
{q : ℕ}
{hq : 1 ≤ q}
{ρ : SmoothCutoff}
{lam ε : ℝ}
{κ : PartialPairing (Fin (2 * q))}
{hκ : κ ∈ nonSplitPairings q}
{state : R322AnalyticEdgeState q hq}
(hstate : R322AnalyticAbsorbedState ρ lam ε hq κ hκ state)
(edge : Fin (2 * q - 1))
(hfuture : ∀ earlier ∈ state.processed, earlier.1.2 < r322AnalyticEdgeLeftVertex edge)
:
Every edge whose left vertex is strictly beyond all processed right endpoints is still the original Green kernel.
theorem
Anderson4D.R322AnalyticAbsorbedState.outgoingEdge_eq_greenFn
{q : ℕ}
{hq : 1 ≤ q}
{ρ : SmoothCutoff}
{lam ε : ℝ}
{κ : PartialPairing (Fin (2 * q))}
{hκ : κ ∈ nonSplitPairings q}
{state : R322AnalyticEdgeState q hq}
(hstate : R322AnalyticAbsorbedState ρ lam ε hq κ hκ state)
(ctx : R322AnalyticProperStepContext q hq)
(hpairing : ctx.pairing = κ)
(hstateEq : ctx.state = state)
:
The outgoing edge of the next proper scheduled block has not yet been
updated, hence is exactly greenFn.