Reindexing R-322 block products into analytic order

The existing coordinate factorization uses the unordered finite type ExtractionBlockIndex κ. This file equips it with the exact order of r322AnalyticSchedule κ. The construction is purely finite and uses the block-projection permutation together with block nodup; no integral is changed here.

The ordered block equivalence

theorem Anderson4D.r322AnalyticSchedule_blocks_nodup {m : ℕ} (κ : PartialPairing (Fin m)) : (List.map Prod.snd (r322AnalyticSchedule κ)).Nodup

The scheduled block projection has no duplicates.

def Anderson4D.r322AnalyticBlockEquiv {m : ℕ} (κ : PartialPairing (Fin m)) : Fin (r322AnalyticSchedule κ).length ≃ ExtractionBlockIndex κ

Analytic list positions are exactly the concrete extraction-block coordinates.

Equations

• Anderson4D.r322AnalyticBlockEquiv κ = ((finCongr ⋯).trans (List.Nodup.getEquiv (List.map Prod.snd (Anderson4D.r322AnalyticSchedule κ)) ⋯)).trans (Equiv.subtypeEquivRight ⋯)

@[simp]

theorem Anderson4D.r322AnalyticBlockEquiv_apply_val {m : ℕ} (κ : PartialPairing (Fin m)) (i : Fin (r322AnalyticSchedule κ).length) : ↑((r322AnalyticBlockEquiv κ) i) = ((r322AnalyticSchedule κ).get i).2

Applying the ordered block equivalence returns precisely the block stored in the corresponding schedule step.

Exact finite-product reindexing

theorem Anderson4D.extractionBlock_prod_eq_analyticSchedule {m : ℕ} (κ : PartialPairing (Fin m)) {M : Type u_1} [CommMonoid M] (f : ExtractionBlockIndex κ → M) : ∏ B : ExtractionBlockIndex κ, f B = ∏ i : Fin (r322AnalyticSchedule κ).length, f ((r322AnalyticBlockEquiv κ) i)

Reindex an unordered product over extraction blocks by analytic schedule position.

Splitting a nonempty analytic schedule

def Anderson4D.r322AnalyticConsIndexEquiv {m : ℕ} (κ : PartialPairing (Fin m)) {head : R322ExtractionStep m} {tail : List (R322ExtractionStep m)} (hschedule : r322AnalyticSchedule κ = head :: tail) : Fin (tail.length + 1) ≃ Fin (r322AnalyticSchedule κ).length

The standard Fin (n + 1) indexing of a displayed head :: tail schedule.

Equations

• Anderson4D.r322AnalyticConsIndexEquiv κ hschedule = finCongr ⋯

def Anderson4D.r322AnalyticHeadBlockIndex {m : ℕ} (κ : PartialPairing (Fin m)) {head : R322ExtractionStep m} {tail : List (R322ExtractionStep m)} (hschedule : r322AnalyticSchedule κ = head :: tail) : ExtractionBlockIndex κ

The extraction-block coordinate at the head of a displayed schedule.

Equations

• Anderson4D.r322AnalyticHeadBlockIndex κ hschedule = (Anderson4D.r322AnalyticBlockEquiv κ) ((Anderson4D.r322AnalyticConsIndexEquiv κ hschedule) 0)

def Anderson4D.r322AnalyticTailBlockIndex {m : ℕ} (κ : PartialPairing (Fin m)) {head : R322ExtractionStep m} {tail : List (R322ExtractionStep m)} (hschedule : r322AnalyticSchedule κ = head :: tail) (j : Fin tail.length) : ExtractionBlockIndex κ

The extraction-block coordinate at one position of the displayed tail.

Equations

• Anderson4D.r322AnalyticTailBlockIndex κ hschedule j = (Anderson4D.r322AnalyticBlockEquiv κ) ((Anderson4D.r322AnalyticConsIndexEquiv κ hschedule) j.succ)

@[simp]

theorem Anderson4D.r322AnalyticHeadBlockIndex_val {m : ℕ} (κ : PartialPairing (Fin m)) {head : R322ExtractionStep m} {tail : List (R322ExtractionStep m)} (hschedule : r322AnalyticSchedule κ = head :: tail) : ↑(r322AnalyticHeadBlockIndex κ hschedule) = head.2

The head coordinate carries exactly the block stored in head.

@[simp]

theorem Anderson4D.r322AnalyticTailBlockIndex_val {m : ℕ} (κ : PartialPairing (Fin m)) {head : R322ExtractionStep m} {tail : List (R322ExtractionStep m)} (hschedule : r322AnalyticSchedule κ = head :: tail) (j : Fin tail.length) : ↑(r322AnalyticTailBlockIndex κ hschedule j) = (tail.get j).2

A tail coordinate carries exactly the block stored at that tail position.

theorem Anderson4D.extractionBlock_prod_eq_head_mul_tail {m : ℕ} (κ : PartialPairing (Fin m)) {head : R322ExtractionStep m} {tail : List (R322ExtractionStep m)} (hschedule : r322AnalyticSchedule κ = head :: tail) {M : Type u_1} [CommMonoid M] (f : ExtractionBlockIndex κ → M) : ∏ B : ExtractionBlockIndex κ, f B = f (r322AnalyticHeadBlockIndex κ hschedule) * ∏ j : Fin tail.length, f (r322AnalyticTailBlockIndex κ hschedule j)

A product in analytic block order splits into the head factor followed by the product over the displayed tail.