AffineIncidence.lean`

47 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.WLIdentification.Bit line 7
def OAI.WLIdentification.NaturalCode.fin line 14
def OAI.WLIdentification.NaturalCode.bool line 15
def OAI.WLIdentification.NaturalCode.unit line 16
def OAI.WLIdentification.NaturalCode.prod line 17
def OAI.WLIdentification.NaturalCode.sum line 20
def OAI.WLIdentification.NaturalCode.option line 32
def OAI.WLIdentification.NaturalCode.subtype line 44
def OAI.WLIdentification.NaturalCode.sigma line 47
def OAI.WLIdentification.NaturalCode.fixed line 59
structure OAI.WLIdentification.AffineBlocks line 64
abbrev OAI.WLIdentification.AffineBlocks.Local line 75
def OAI.WLIdentification.AffineBlocks.Legal line 77
instance OAI.WLIdentification.AffineBlocks.legalDecidable line 80
def OAI.WLIdentification.AffineBlocks.restrict line 83
def OAI.WLIdentification.AffineBlocks.Solves line 85
theorem OAI.WLIdentification.AffineBlocks.local_nonempty line 88
theorem OAI.WLIdentification.AffineBlocks.legal_zero line 95

def OAI.WLIdentification.AffineBlocks.legalTranslate line 100

Source documentation

Only local nonemptiness is used here; no simultaneous solution is presumed.

def legalTranslate (D : AffineBlocks C B) {beta gamma : B → Bit} (b : B)
    (offset : D.Local b) (ho : ∀ _ : D.constrained b = true,
      D.form b offset = gamma b - beta b) :
    {v // D.Legal beta b v} ≃ {v // D.Legal gamma b v} where
…

Mentions: OAI.WLIdentification.AffineBlocks, OAI.WLIdentification.Bit

theorem OAI.WLIdentification.AffineBlocks.legal_card line 115
abbrev OAI.WLIdentification.AffineBlocks.Vertex line 121
def OAI.WLIdentification.AffineBlocks.colorName line 124
def OAI.WLIdentification.AffineBlocks.baseGraph line 128
instance OAI.WLIdentification.AffineBlocks.baseGraph_decidable line 136
def OAI.WLIdentification.AffineBlocks.translationIso line 140
Source documentation
Translation uses the same named coordinate offset in every incident block.
```
def translationIso (D : AffineBlocks C B) (beta : B → Bit)
    (offset : C → Bit) (ho : D.Solves beta offset) : D.baseGraph 0 ≃g D.baseGraph beta where
…
```
Mentions: OAI.WLIdentification.AffineBlocks, OAI.WLIdentification.Bit
theorem OAI.WLIdentification.AffineBlocks.translationIso_color line 167
theorem OAI.WLIdentification.AffineBlocks.exists_bit_of_color line 172
theorem OAI.WLIdentification.AffineBlocks.exists_valuation_of_color line 181
theorem OAI.WLIdentification.AffineBlocks.coloredIso_solution line 194
Source documentation
All-zero valuations extract one global offset from a color-preserving isomorphism. No agreement between independently chosen block maps is assumed.
```
theorem coloredIso_solution (D : AffineBlocks C B) (beta : B → Bit)
    (e : D.baseGraph 0 ≃g D.baseGraph beta)
    (he : ∀ v, D.colorName (e v) = D.colorName v) :
    ∃ offset, D.Solves beta offset := by
…
```
Mentions: OAI.WLIdentification.AffineBlocks, OAI.WLIdentification.Bit
theorem OAI.WLIdentification.AffineBlocks.coloredIso_iff line 216
def OAI.WLIdentification.AffineBlocks.colorNat line 227
theorem OAI.WLIdentification.AffineBlocks.colorNat_pos line 231
theorem OAI.WLIdentification.AffineBlocks.colorNat_eq_iff line 235
theorem OAI.WLIdentification.AffineBlocks.vertex_card line 244
def OAI.WLIdentification.AffineBlocks.graph line 252
theorem OAI.WLIdentification.AffineBlocks.graph_isomorphic_iff line 255
abbrev OAI.WLIdentification.AffineBlocks.Piece line 271
Source documentation
A complete bounded incidence piece consists of its valuation class and both vertices of every bit pair used by this block.
```
abbrev Piece (D : AffineBlocks C B) (beta : B → Bit) (b : B) :=
…
```
Mentions: OAI.WLIdentification.AffineBlocks, OAI.WLIdentification.Bit
def OAI.WLIdentification.AffineBlocks.pieceEmbed line 274
def OAI.WLIdentification.AffineBlocks.pieceGraph line 291
theorem OAI.WLIdentification.AffineBlocks.bit_cases line 294
theorem OAI.WLIdentification.AffineBlocks.bit_injective_translation line 301
theorem OAI.WLIdentification.AffineBlocks.piece_bit_of_color line 310
theorem OAI.WLIdentification.AffineBlocks.piece_valuation_of_color line 321

theorem OAI.WLIdentification.AffineBlocks.local_reconstruction line 330

Source documentation

One entire incidence piece determines a shifted equation in any fixed labeling of its bit pairs. Coordinate flips in different pieces need not agree.

theorem local_reconstruction (D : AffineBlocks C B) (H : SimpleGraph (D.Vertex 0)) (b : B)
    (e : D.pieceGraph 0 b ≃g H.comap (D.pieceEmbed b))
    (he : ∀ v, D.colorName (D.pieceEmbed b (e v)) = D.colorName (D.pieceEmbed b v)) :
    ∃ offset : D.Local b, ∃ E : {v // D.Legal 0 b v} ≃ {v // D.Legal 0 b v},
      ∀ (v : {v // D.Legal 0 b v}) (c : D.coordinates b) (a : Bit),
        H.Adj (.inl (c.val, a)) (.inr ⟨b, E v⟩) ↔ v.val c + offset c = a := by
…

Mentions: OAI.WLIdentification.AffineBlocks, OAI.WLIdentification.Bit

def OAI.WLIdentification.AffineBlocks.Allowed line 366
Source documentation
Adjacencies are allowed only between a valuation class and a named bit coordinate used by that block. This records no right-hand-side information.
```
def Allowed (D : AffineBlocks C B) {beta : B → Bit} (x y : D.Vertex beta) : Prop :=
…
```
Mentions: OAI.WLIdentification.AffineBlocks, OAI.WLIdentification.Bit
theorem OAI.WLIdentification.AffineBlocks.base_adj_allowed line 372

theorem OAI.WLIdentification.AffineBlocks.base_reconstruction line 382

Source documentation

Combining the independently reconstructed pieces uses a single labeling of all shared bit pairs, but permits one independent right-hand side per block.

theorem base_reconstruction (D : AffineBlocks C B) (H : SimpleGraph (D.Vertex 0))
    (hallowed : ∀ x y, H.Adj x y → D.Allowed x y)
    (hlocal : ∀ b, ∃ e : D.pieceGraph 0 b ≃g H.comap (D.pieceEmbed b),
      ∀ v, D.colorName (D.pieceEmbed b (e v)) = D.colorName (D.pieceEmbed b v)) :
    ∃ beta, ∃ e : D.baseGraph beta ≃g H, ∀ v, D.colorName (e v) = D.colorName v := by
…

Mentions: OAI.WLIdentification.AffineBlocks