Coordinate independence for one analytic R-322 head block

The analytic schedule removes an innermost primitive block before every interval which contains it. For a head step s = (p,B) and a later step t = (q,C), the only coordinates read by the later generalized difference factor are q.1, q.2, and (when it exists) q.2 + 1. This file proves that all three lie outside B under the exact disjoint-right/containing interval dichotomy.

The three later difference coordinates avoid the head block

theorem Anderson4D.r322ExtractionStep_fst_le_snd {m : ℕ} (t : R322ExtractionStep m) (ht : ExtractionPairBlockAligned t.1 t.2) : t.1.1 ≤ t.1.2

The endpoints of an aligned later extraction step are ordered.

theorem Anderson4D.r322AnalyticLater_left_not_mem_headBlock {m : ℕ} (s t : R322ExtractionStep m) (hs : ExtractionPairBlockAligned s.1 s.2) (hrel : s.1.2 < t.1.1 ∨ t.1.1 < s.1.1 ∧ s.1.2 < t.1.2) : t.1.1 ∉ s.2

Under the analytic disjoint-right/containing dichotomy, the later left endpoint does not belong to the head block.

theorem Anderson4D.r322AnalyticHead_right_lt_laterRight {m : ℕ} (s t : R322ExtractionStep m) (ht : ExtractionPairBlockAligned t.1 t.2) (hrel : s.1.2 < t.1.1 ∨ t.1.1 < s.1.1 ∧ s.1.2 < t.1.2) : s.1.2 < t.1.2

The later right endpoint is strictly to the right of the head right endpoint.

theorem Anderson4D.r322AnalyticLater_right_not_mem_headBlock {m : ℕ} (s t : R322ExtractionStep m) (hs : ExtractionPairBlockAligned s.1 s.2) (ht : ExtractionPairBlockAligned t.1 t.2) (hrel : s.1.2 < t.1.1 ∨ t.1.1 < s.1.1 ∧ s.1.2 < t.1.2) : t.1.2 ∉ s.2

Consequently the later right endpoint does not belong to the head block.

theorem Anderson4D.r322AnalyticLater_rightSucc_not_mem_headBlock {m : ℕ} (s t : R322ExtractionStep m) (hs : ExtractionPairBlockAligned s.1 s.2) (ht : ExtractionPairBlockAligned t.1 t.2) (hrel : s.1.2 < t.1.1 ∨ t.1.1 < s.1.1 ∧ s.1.2 < t.1.2) (hguard : ↑t.1.2 + 1 < m) : ⟨↑t.1.2 + 1, hguard⟩ ∉ s.2

The third coordinate read by diffFactorJWith, namely the successor of the later right endpoint, also lies outside the head block.

theorem Anderson4D.r322AnalyticLater_diffCoordinates_not_mem_headBlock {m : ℕ} (s t : R322ExtractionStep m) (hs : ExtractionPairBlockAligned s.1 s.2) (ht : ExtractionPairBlockAligned t.1 t.2) (hrel : s.1.2 < t.1.1 ∨ t.1.1 < s.1.1 ∧ s.1.2 < t.1.2) : t.1.1 ∉ s.2 ∧ t.1.2 ∉ s.2 ∧ ∀ (hguard : ↑t.1.2 + 1 < m), ⟨↑t.1.2 + 1, hguard⟩ ∉ s.2

Bundled form matching the three actual tuple reads in a later generalized difference factor.

Later differences are independent of head-block variables

theorem Anderson4D.diffFactorJWith_eq_of_eq_outside_analyticHeadBlock {m : ℕ} (G : Fin (m - 1) → T4 → ℝ) (x y : Fin m → T4) (s t : R322ExtractionStep m) (hs : ExtractionPairBlockAligned s.1 s.2) (ht : ExtractionPairBlockAligned t.1 t.2) (hrel : s.1.2 < t.1.1 ∨ t.1.1 < s.1.1 ∧ s.1.2 < t.1.2) (hxy : ∀ i ∉ s.2, x i = y i) : diffFactorJWith G x t.1 = diffFactorJWith G y t.1

If two tuples agree away from the head block, every later generalized difference factor has exactly the same value.

theorem Anderson4D.diffFactorJ_eq_of_eq_outside_analyticHeadBlock {m : ℕ} (x y : Fin m → T4) (s t : R322ExtractionStep m) (hs : ExtractionPairBlockAligned s.1 s.2) (ht : ExtractionPairBlockAligned t.1 t.2) (hrel : s.1.2 < t.1.1 ∨ t.1.1 < s.1.1 ∧ s.1.2 < t.1.2) (hxy : ∀ i ∉ s.2, x i = y i) : diffFactorJ x t.1 = diffFactorJ y t.1

Free-Green specialization of the same independence statement.

The head outgoing coordinate is external to its own block

theorem Anderson4D.r322AnalyticHead_rightSucc_not_mem_headBlock {m : ℕ} (s : R322ExtractionStep m) (hs : ExtractionPairBlockAligned s.1 s.2) (hguard : ↑s.1.2 + 1 < m) : ⟨↑s.1.2 + 1, hguard⟩ ∉ s.2

In the proper guarded case, the successor of the head right endpoint is outside the aligned head block.