ScalarExtension.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.WLIdentification.RingLayout.wrapping_row_inj line 10
def OAI.WLIdentification.RingLayout.blockRepresentative line 18
theorem OAI.WLIdentification.RingLayout.name_present line 22
theorem OAI.WLIdentification.RingLayout.name_reachable line 27

theorem OAI.WLIdentification.RingLayout.block_reachable line 33

Source documentation

Every name of a block belongs to the block's unique corner component.

theorem block_reachable (hr : 2 ≤ r) {U : Finset R.Block} {b : R.Block} (hb : b ∈ U)
    {n : R.Name} (hn : n ∈ R.blockNames b) :
    (R.cornerGraph hr U).Reachable (R.blockRepresentative b) (R.nameFirst n) ∧
    (R.cornerGraph hr U).Reachable (R.blockRepresentative b) (R.nameSecond n) := by
…

def OAI.WLIdentification.RingLayout.componentBlocks line 59
theorem OAI.WLIdentification.RingLayout.componentBlocks_subset line 63
theorem OAI.WLIdentification.RingLayout.component_edge line 68
theorem OAI.WLIdentification.RingLayout.component_walk line 83
theorem OAI.WLIdentification.RingLayout.wrapping_component line 97
Source documentation
A wrapping collection of at most r blocks is entirely in the component of its odd closed walk. This also rules out two independent old wrapping choices.
```
theorem wrapping_component (hr : 3 ≤ r) {U : Finset R.Block} (hu : U.card ≤ r)
    {u : R.Corner} (p : (R.cornerGraph (by omega) U).Walk u u)
    (hp : Marker.walkSum R.cornerMarker p = 1) :
    R.componentBlocks (by omega) U u = U := by
…
```
Mentions: OAI.WLIdentification.Marker.walkSum

theorem OAI.WLIdentification.Marker.closed_zero_of_mismatched_labels line 112

Source documentation

Label separation at a boundary cuts every winding walk. The parity incidence argument is expressed as a coboundary.

theorem closed_zero_of_mismatched_labels {r : ℕ} (hr : 2 ≤ r)
    {V : Type} {G : SimpleGraph V} (row : V → Fin r) (label : V → Bool)
    (start finish : Fin r → Bool) (j : Fin r) (hj : finish j ≠ start (finRotate r j))
    (m : V → V → Bit)
    (he : ∀ u v, G.Adj u v →
      (row u = row v ∧ label u = label v ∧ m u v = 0) ∨
      ∃ i, m u v = delta i ∧
        ((row u = i ∧ row v = finRotate r i ∧ label u = start i ∧ label v = finish i) ∨
         (row v = i ∧ row u = finRotate r i ∧ label v = start i ∧ label u = finish i))) :
    ∀ u (p : G.Walk u u), walkSum m p = 0 := by
…

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

def OAI.WLIdentification.RingLayout.Aligned line 166
Source documentation
An alignment is only required to respect actual vertical readout names. No assertion is made that ambient labels inhabit every product factor.
```
def Aligned (U : Finset R.Block) (a : R.Corner → Bool) : Prop :=
…
```
def OAI.WLIdentification.RingLayout.blockStart line 169
def OAI.WLIdentification.RingLayout.blockFinish line 173
theorem OAI.WLIdentification.RingLayout.horizontal_labels line 177
def OAI.WLIdentification.RingLayout.IsWrappingAddress line 199

theorem OAI.WLIdentification.RingLayout.wrapping_address line 204

Source documentation

Exactly r wrapping blocks prescribe one genuine aligned address.

theorem wrapping_address (hr : 3 ≤ r) {U : Finset R.Block}
    (h : R.Wrapping (by omega) U) (hu : U.card ≤ r)
    {a : R.Corner → Bool} (ha : R.Aligned U a) :
    ∃! address : Fin r → Bool, R.IsWrappingAddress U a address := by
…

theorem OAI.WLIdentification.RingLayout.names_mono line 259
theorem OAI.WLIdentification.RingLayout.cornerGraph_mono line 265
theorem OAI.WLIdentification.RingLayout.aligned_mono line 270
theorem OAI.WLIdentification.RingLayout.wrapping_blocks_reachable line 274

theorem OAI.WLIdentification.RingLayout.small_sdiff line 285

Source documentation

Two r-element subcollections of r+1 blocks differ by at most one block.

theorem small_sdiff {U V W : Finset R.Block} (hV : V ⊆ U) (hW : W ⊆ U)
    (hu : U.card ≤ r + 1) (hw : r ≤ W.card) : (V \ W).card ≤ 1 := by
…

theorem OAI.WLIdentification.RingLayout.shared_incident line 298

Source documentation

The common rows of two wrapping r-subcollections touch every boundary. This is exactly where r≥3 is used for address compatibility.

theorem shared_incident (hr : 3 ≤ r) {U V W : Finset R.Block}
    (hV : V ⊆ U) (hW : W ⊆ U) (hu : U.card ≤ r + 1)
    (hv : R.Wrapping (by omega) V) (hw : R.Wrapping (by omega) W) (i : Fin r) :
    ∃ b ∈ V ∩ W, R.blockRow b = i ∨ finRotate r (R.blockRow b) = i := by
…

theorem OAI.WLIdentification.RingLayout.wrapping_addresses_agree line 321

Source documentation

All wrapping r-subcollections of r+1 blocks have the same address in a single ambient alignment; no address is imposed by an arbitrary r+1-cycle.

theorem wrapping_addresses_agree (hr : 3 ≤ r) {U V W : Finset R.Block}
    (hV : V ⊆ U) (hW : W ⊆ U) (hu : U.card ≤ r + 1)
    (hv : R.Wrapping (by omega) V) (hw : R.Wrapping (by omega) W)
    {a : R.Corner → Bool} {v w : Fin r → Bool}
    (hvaddr : R.IsWrappingAddress V a v) (hwaddr : R.IsWrappingAddress W a w) : v = w := by
…

theorem OAI.WLIdentification.RingLayout.wrapping_subcollections_connected line 335

Source documentation

Wrapping r-subcollections also belong to one corner component, even if other nonwrapping covers appear elsewhere in U.

theorem wrapping_subcollections_connected (hr : 3 ≤ r) {U V W : Finset R.Block}
    (hV : V ⊆ U) (hW : W ⊆ U) (hu : U.card ≤ r + 1)
    (hvcard : V.card ≤ r) (hwcard : W.card ≤ r)
    (hv : R.Wrapping (by omega) V) (hw : R.Wrapping (by omega) W)
    {b c : R.Block} (hb : b ∈ V) (hc : c ∈ W) :
    (R.cornerGraph (by omega) U).Reachable (R.blockRepresentative b) (R.blockRepresentative c) := by
…

def OAI.WLIdentification.RingLayout.usedLinks line 352
theorem OAI.WLIdentification.RingLayout.mem_usedLinks line 356
theorem OAI.WLIdentification.RingLayout.usedLinks_card line 368