FirstPaperLocalNeighbors.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic enumeration of the first-paper chain's neighbors

The list is obtained from ordered coordinate and cell pairs, then filtered by arithmetic edge and feasibility tests. It never enumerates all states.

def OAI.ContingencyTables.SmallGraphProfiles.ArithmeticRepair line 32
Source documentation
A directed repair is identified by its two defect cells.
```
def ArithmeticRepair (v w : SmallProfile small) : Prop :=
…
```
def OAI.ContingencyTables.SmallGraphProfiles.ArithmeticEdge line 38
Source documentation
All predicates are bounded integer-coordinate tests.
```
def ArithmeticEdge (v w : SmallProfile small) : Prop :=
…
```
lemma OAI.ContingencyTables.SmallGraphProfiles.arithmeticRepair_iff line 42
theorem OAI.ContingencyTables.SmallGraphProfiles.arithmeticEdge_iff line 65
Source documentation
On actual states the arithmetic test is exactly the graph relation used in the Poincare and mixing proofs.
```
theorem arithmeticEdge_iff (x y : PaperStates r c) :
    ArithmeticEdge r c (profile x) (profile y) ↔
      physicalAdjacent r c U L B (stateCapacity_small r c) x y := by
…
```
Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStates, OAI.ContingencyTables.SmallGraphProfiles.ArithmeticEdge, OAI.ContingencyTables.SmallGraphProfiles.physicalAdjacent, OAI.ContingencyTables.SmallGraphProfiles.stateCapacity_small
def OAI.ContingencyTables.SmallGraphProfiles.localCandidates line 89
lemma OAI.ContingencyTables.SmallGraphProfiles.localCandidates_card line 92
def OAI.ContingencyTables.SmallGraphProfiles.localNeighborList line 107
Source documentation
Passing candidates are decoded with the arithmetic feasibility test.
```
def localNeighborList (x : PaperStates r c) : List (PaperStates r c) :=
…
```
Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStates
lemma OAI.ContingencyTables.SmallGraphProfiles.localNeighborList_nodup line 111
theorem OAI.ContingencyTables.SmallGraphProfiles.mem_localNeighborList line 120
theorem OAI.ContingencyTables.SmallGraphProfiles.localNeighborList_length line 136