SmallContextCoordinates.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Actual row-major small-prefix coordinate splitting

The retained prefix is precisely the earlier small cells. The remaining ordinary cells all follow the next exposed cell, which is the condition needed for the completion-retaining conditional repair injection.

lemma OAI.ContingencyTables.SmallContextCoordinates.rowMajor_trichotomy line 22
abbrev OAI.ContingencyTables.SmallContextCoordinates.Cells line 31
def OAI.ContingencyTables.SmallContextCoordinates.Earlier line 33
def OAI.ContingencyTables.SmallContextCoordinates.Later line 34
instance OAI.ContingencyTables.SmallContextCoordinates.earlierFintype line 36
instance OAI.ContingencyTables.SmallContextCoordinates.laterFintype line 41
def OAI.ContingencyTables.SmallContextCoordinates.cellSplitEquiv line 46
def OAI.ContingencyTables.SmallContextCoordinates.splitPairEquiv line 86
Source documentation
Pack the prefix, special pair and suffix into the cell split.
```
def splitPairEquiv (P T : Type u) :
    ((P×Bool) ⊕ (Bool ⊕ (T×Bool))) ≃ (P ⊕ (Unit ⊕ T))×Bool where
…
```
def OAI.ContingencyTables.SmallContextCoordinates.contextEquiv line 101
Source documentation
The exact small-coordinate bijection required by physical context transport. The suffix enumeration introduces no extra assignment.
```
noncomputable def contextEquiv (small : I → J → Bool) (s : I×J)
    (hs : small s.1 s.2=true) {n : ℕ} (e : Fin n ≃ Later small s) (U : ℕ) :
    ((Earlier small s×Bool) ⊕ Coordinates Bool (widths (fun _ : Fin n => U))) ≃
      SmallView (fun a : I×J => small a.1 a.2) :=
…
```
Mentions: OAI.ContingencyTables.SmallContextCoordinates.Later, OAI.ContingencyTables.SmallContextCoordinates.Earlier
lemma OAI.ContingencyTables.SmallContextCoordinates.contextEquiv_prefix line 109
lemma OAI.ContingencyTables.SmallContextCoordinates.contextEquiv_special line 114
lemma OAI.ContingencyTables.SmallContextCoordinates.contextEquiv_later line 122