LocalImages.lean`

42 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.WLIdentification.bit_eq_add_of_add_eq line 8
Source documentation
Characteristic-two rearrangement, stated without an arithmetic oracle.
```
theorem bit_eq_add_of_add_eq {x y z : Bit} (h : x + y = z) : x = z + y := by
…
```
Mentions: OAI.WLIdentification.Bit

theorem OAI.WLIdentification.RingLayout.imageSet_link line 18

Source documentation

Image consistency for every link. Only scalar image sets are equated; no common vector choice is silently imposed on distinct comparisons.

theorem imageSet_link (hr : 2 ≤ r) (beta : R.Block → Bit) (e : L) (a : R.MatchAddress e) :
    (R.firstForm e) '' R.ImageSet hr beta (R.first e) (R.leftAddress e a) =
      (fun y => R.linkShift beta e a + R.secondForm e y) ''
        R.ImageSet hr beta (R.second e) (R.rightAddress e a) := by
…

Mentions: OAI.WLIdentification.Bit

def OAI.WLIdentification.WireAlgebra.shiftSet line 35
theorem OAI.WLIdentification.WireAlgebra.shiftSet_zero line 38
theorem OAI.WLIdentification.WireAlgebra.shiftSet_shiftSet line 42

theorem OAI.WLIdentification.WireAlgebra.chain_sets line 48

Source documentation

Private internal scalar image sets telescope by translations. This does not cancel Minkowski sums or select a common endpoint vector across comparisons.

theorem chain_sets {n : ℕ} (left right : Set Bit) (q : Fin (n + 1) → Set Bit)
    (first last : Bit) (middle : Fin n → Bit)
    (hfirst : left = shiftSet first (q 0))
    (hmiddle : ∀ i, q i.castSucc = shiftSet (middle i) (q i.succ))
    (hlast : q (Fin.last n) = shiftSet last right) :
    left = shiftSet (first + (∑ i, middle i) + last) right := by
…

Mentions: OAI.WLIdentification.Bit, OAI.WLIdentification.WireAlgebra.shiftSet

def OAI.WLIdentification.ComparisonSchemas.responseImages line 69
theorem OAI.WLIdentification.ComparisonSchemas.image_consistency line 73
def OAI.WLIdentification.Marker.walkSum line 116
theorem OAI.WLIdentification.Marker.walkSum_nil line 120
theorem OAI.WLIdentification.Marker.walkSum_cons line 123
theorem OAI.WLIdentification.Marker.walkSum_append line 126
theorem OAI.WLIdentification.Marker.walkSum_reverse line 133
theorem OAI.WLIdentification.Marker.walkSum_cast_left line 142
theorem OAI.WLIdentification.Marker.exact_of_closed_zero line 149
Source documentation
A nonwrapping marker is an exact coboundary. No finiteness or connectedness assumption is needed; roots are chosen separately in actual graph components.
```
theorem exact_of_closed_zero (m : V → V → Bit)
    (hm : ∀ u v, G.Adj u v → m u v = m v u)
    (hc : ∀ u (p : G.Walk u u), walkSum m p = 0) :
    ∃ s : V → Bit, ∀ u v, G.Adj u v → m u v = s u + s v := by
…
```
Mentions: OAI.WLIdentification.Bit, OAI.WLIdentification.Marker.walkSum
theorem OAI.WLIdentification.Marker.walkSum_of_exact line 171
Source documentation
Conversely, a potential cancels around every closed walk.
```
theorem walkSum_of_exact (s : V → Bit) (m : V → V → Bit)
    (hm : ∀ u v, G.Adj u v → m u v = s u + s v)
    {u v : V} (p : G.Walk u v) : walkSum m p = s u + s v := by
…
```
Mentions: OAI.WLIdentification.Bit, OAI.WLIdentification.Marker.walkSum
theorem OAI.WLIdentification.Marker.walkSum_add line 182
theorem OAI.WLIdentification.Marker.walkSum_smul line 188
def OAI.WLIdentification.Marker.cut line 194
def OAI.WLIdentification.Marker.delta line 196
theorem OAI.WLIdentification.Marker.cut_toggle line 200
Source documentation
Moving the marked row to any other cut changes the marker by a boundary potential, including for singleton coordinate domains.
```
theorem cut_toggle {r : ℕ} (j i : Fin r) :
    cut j i + cut j (finRotate r i) = delta i + (if i = j then 1 else 0) := by
…
```
Mentions: OAI.WLIdentification.Marker.cut, OAI.WLIdentification.Marker.delta

theorem OAI.WLIdentification.Marker.closed_zero_of_missing_row line 229

Source documentation

If one row is absent, the ring marker is a boundary potential. This is valid on an arbitrary corner subgraph and uses no assumption on label factors.

theorem closed_zero_of_missing_row {r : ℕ} (row : V → Fin r) (j : Fin r)
    (m : V → V → Bit)
    (he : ∀ u v, G.Adj u v →
      (row u = row v ∧ m u v = 0) ∨
      ∃ i : Fin r, i ≠ j ∧ m u v = delta i ∧
        ((row u = i ∧ row v = finRotate r i) ∨
         (row v = i ∧ row u = finRotate r i))) :
    ∀ u (p : G.Walk u u), walkSum m p = 0 := by
…

Mentions: OAI.WLIdentification.Bit, OAI.WLIdentification.Marker.delta, OAI.WLIdentification.Marker.walkSum

theorem OAI.WLIdentification.Marker.horizontal_adjust line 251
Source documentation
The potential adjustment in the exact-projection argument, at a horizontal readout. Vector coordinates are adjusted together, not independently chosen.
```
theorem horizontal_adjust {W : Type} [AddCommGroup W] [Module Bit W]
    (M N old new : W) (s t d : Bit) (hd : s + t = d) :
    (M + s • (new + old)) + (N + t • (new + old)) + d • new = M + N + d • old := by
…
```
Mentions: OAI.WLIdentification.Bit

theorem OAI.WLIdentification.Marker.vertical_adjust line 265

Source documentation

Vertical readouts survive the same adjustment because the difference of the two affine component shifts solves the homogeneous link equation.

theorem vertical_adjust {W X : Type} [AddCommGroup W] [AddCommGroup X]
    [Module Bit W] [Module Bit X] (L : W →ₗ[Bit] Bit) (R : X →ₗ[Bit] Bit)
    (M : W) (N : X) (g : W) (h : X) (s t : Bit)
    (hst : s = t) (he : L g + R h = 0) :
    L (M + s • g) + R (N + t • h) = L M + R N := by
…

Mentions: OAI.WLIdentification.Bit

abbrev OAI.WLIdentification.RingLayout.Corner line 281
abbrev OAI.WLIdentification.RingLayout.Name line 282
instance OAI.WLIdentification.RingLayout.nameDecidableEq line 284
def OAI.WLIdentification.RingLayout.nameFirst line 286
def OAI.WLIdentification.RingLayout.nameSecond line 290
theorem OAI.WLIdentification.RingLayout.name_endpoints_ne line 294
def OAI.WLIdentification.RingLayout.blockNames line 302
def OAI.WLIdentification.RingLayout.names line 306
def OAI.WLIdentification.RingLayout.blockRow line 310
def OAI.WLIdentification.RingLayout.cornerGraph line 316
Source documentation
Shared names give a single edge. Vector bit coordinates are not counted as separate horizontal edges in the corner graph.
```
noncomputable def cornerGraph (hr : 2 ≤ r) (U : Finset R.Block) : SimpleGraph R.Corner where
…
```
def OAI.WLIdentification.RingLayout.cornerMarker line 328
theorem OAI.WLIdentification.RingLayout.cornerMarker_horizontal line 332
theorem OAI.WLIdentification.RingLayout.cornerMarker_vertical line 342
theorem OAI.WLIdentification.RingLayout.horizontal_row_mem line 347

theorem OAI.WLIdentification.RingLayout.cornerGraph_row_edge line 364

Source documentation

Every horizontal edge in the support comes from a block in its own row; vertical edges preserve the boundary index and have marker zero.

theorem cornerGraph_row_edge (hr : 3 ≤ r) {U : Finset R.Block} {u v : R.Corner}
    (h : (R.cornerGraph (by omega) U).Adj u v) :
    (u.2.1 = v.2.1 ∧ R.cornerMarker u v = 0) ∨
    ∃ i ∈ U.image R.blockRow, R.cornerMarker u v = Marker.delta i ∧
      ((u.2.1 = i ∧ v.2.1 = finRotate r i) ∨
       (v.2.1 = i ∧ u.2.1 = finRotate r i)) := by
…

Mentions: OAI.WLIdentification.Marker.delta

def OAI.WLIdentification.RingLayout.Wrapping line 383
theorem OAI.WLIdentification.RingLayout.wrapping_rows line 387
Source documentation
A closed walk of odd marker forces every row to be represented.
```
theorem wrapping_rows (hr : 3 ≤ r) {U : Finset R.Block}
    (h : R.Wrapping (by omega) U) (j : Fin r) : j ∈ U.image R.blockRow := by
…
```
theorem OAI.WLIdentification.RingLayout.wrapping_card line 404
Source documentation
A wrapping family has at least one block per row. The count is blocks, not readout names and not vertices; a square still supplies only one row.
```
theorem wrapping_card (hr : 3 ≤ r) {U : Finset R.Block}
    (h : R.Wrapping (by omega) U) : r ≤ U.card := by
…
```