CoordinateSector.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Saxl.coordinateProjection line 11
Source comment
Coordinate projection; equivariance is asserted only for preserved predicates.
```
def coordinateProjection {n d : ℕ} (P : (Fin n → Fin d) → Prop) :
    Module.End ℂ (WordSpace n d) := by
…
```
Mentions: OAI.Saxl.WordSpace
lemma OAI.Saxl.coordinateProjection_apply line 19
lemma OAI.Saxl.coordinateProjection_single line 25

def OAI.Saxl.sectorGroup line 35

Source comment

Permutations preserving a position sector.

def sectorGroup {n : ℕ} (D : Fin n → Prop) : Subgroup (Equiv.Perm (Fin n)) where
…

def OAI.Saxl.altWord line 44
Source comment
The genuine unnormalized signed block alternation.
```
def altWord {n d : ℕ} (G : Subgroup (Equiv.Perm (Fin n))) (a : Fin n → Fin d) :
    WordSpace n d := by
…
```
Mentions: OAI.Saxl.WordSpace
lemma OAI.Saxl.altWord_move line 51

theorem OAI.Saxl.altWord_sector line 74

Source comment

Keeping a prescribed coloring restricts the alternating group to its sector stabilizer. This is the finite coset calculation behind block-factorization.

theorem altWord_sector {n d : ℕ} (G : Subgroup (Equiv.Perm (Fin n)))
    (a : Fin n → Fin d) (Q : Fin d → Prop) (D : Fin n → Prop)
    (ha : ∀ i, Q (a i) ↔ D i) :
    coordinateProjection (fun b => ∀ i, Q (b i) ↔ D i) (altWord G a) =
      altWord (G ⊓ sectorGroup D) a := by
…

Mentions: OAI.Saxl.coordinateProjection, OAI.Saxl.altWord, OAI.Saxl.sectorGroup

def OAI.Saxl.stairHigh line 109
Source comment
The prescribed high sector in the actual staircase enumeration.
```
def stairHigh (h s : ℕ) (i : Fin (staircase (h+s)).card) : Prop :=
…
```
Mentions: OAI.Saxl.staircase
lemma OAI.Saxl.staircase_projected_sector line 112
lemma OAI.Saxl.coordinateProjection_tensor line 132
lemma OAI.Saxl.altWord_sector_rotated line 143
lemma OAI.Saxl.polytabloid_eq_altWord line 152
def OAI.Saxl.cutRowWord line 156
Source comment
The cut's two layers, with their exact retained row and column permutations.
```
def cutRowWord (h s : ℕ) :=
…
```
def OAI.Saxl.cutColumnWord line 160
lemma OAI.Saxl.rotatePositions_sign line 164
theorem OAI.Saxl.staircase_cut_layers line 180
Source comment
Exact sign cancellation in the two retained layers.
```
theorem staircase_cut_layers (h s : ℕ) :
    sameHighProjection _ _ _ s (staircaseWord (h+s)) =
      wordTensor _ _ _ (cutRowWord h s ⊗ₜ[ℂ] cutColumnWord h s) := by
…
```
Mentions: OAI.Saxl.sameHighProjection, OAI.Saxl.staircaseWord, OAI.Saxl.wordTensor, OAI.Saxl.cutRowWord, OAI.Saxl.cutColumnWord