OAI/Computability/WLIdentification/RowOffsets.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WLIdentification.CycleRows.RowSum line 11

    Source documentation

    The row-sum restriction is retained explicitly; pointwise globally consistent address values alone are not used as a substitute for actual readout offsets.

    def RowSum {r : ℕ} (A : Fin r → Type) (V : Type) [AddCommMonoid V]
    (h : ((i : Fin r) → A i) → V) : Prop :=
…
  2. theorem OAI.WLIdentification.CycleRows.RowSum.zero line 19
  3. theorem OAI.WLIdentification.CycleRows.RowSum.add line 21
  4. theorem OAI.WLIdentification.CycleRows.RowSum.map line 29
  5. theorem OAI.WLIdentification.CycleRows.RowSum.pullback line 34
  6. theorem OAI.WLIdentification.CycleRows.RowSum.constant line 40
  7. theorem OAI.WLIdentification.CycleRows.RowSum.extend line 49

    Source documentation

    Extending the adjacent-coordinate terms, not an arbitrary full-address function, gives the extension on a product subdomain used by private buffers.

    theorem extend {A' : Fin r → Type} {h : ((i : Fin r) → A i) → V}
    (hh : RowSum A V h) (f : (i : Fin r) → A i → A' i)
    (hf : ∀ i, Function.Injective (f i)) :
    ∃ h', RowSum A' V h' ∧ ∀ a, h' (fun i => f i (a i)) = h a := by
…

    Mentions: OAI.WLIdentification.CycleRows.RowSum

  8. theorem OAI.WLIdentification.CycleRows.square_lifting line 75

    Source documentation

    One link, with arbitrary nonempty coordinate match domains, has legal vertical offsets exactly when the horizontal ring sums have the required shift. This is the local-to-global step used independently on every private wire link.

    theorem square_lifting {r : ℕ} (hr : 3 ≤ r) (A : Fin r → Type)
    (base : (i : Fin r) → A i)
    (left right beta : (i : Fin r) → A i → A (finRotate r i) → Bit) :
    (∃ y : (i : Fin r) → A i → Bit, ∀ i u v,
      left i u v + right i u v + y i u + y (finRotate r i) v = beta i u v) ↔
    ∀ a : (i : Fin r) → A i,
      (∑ i, left i (a i) (a (finRotate r i))) +
        (∑ i, right i (a i) (a (finRotate r i))) =
      ∑ i, beta i (a i) (a (finRotate r i)) := by
…

    Mentions: OAI.WLIdentification.Bit

  9. structure OAI.WLIdentification.RingLayout line 113
  10. abbrev OAI.WLIdentification.RingLayout.Label line 136
  11. abbrev OAI.WLIdentification.RingLayout.Match line 137
  12. abbrev OAI.WLIdentification.RingLayout.HName line 138
  13. abbrev OAI.WLIdentification.RingLayout.VName line 139
  14. abbrev OAI.WLIdentification.RingLayout.Square line 140
  15. abbrev OAI.WLIdentification.RingLayout.Coordinate line 141
  16. abbrev OAI.WLIdentification.RingLayout.Block line 142
  17. def OAI.WLIdentification.RingLayout.leftH line 144
  18. def OAI.WLIdentification.RingLayout.rightH line 148
  19. def OAI.WLIdentification.RingLayout.topV line 152
  20. def OAI.WLIdentification.RingLayout.bottomV line 153
  21. theorem OAI.WLIdentification.RingLayout.vertical_ne line 155
  22. theorem OAI.WLIdentification.RingLayout.horizontal_ne line 160
  23. instance OAI.WLIdentification.RingLayout.coordinateDecidableEq line 164
  24. instance OAI.WLIdentification.RingLayout.blockDecidableEq line 165
  25. def OAI.WLIdentification.RingLayout.hCoords line 167
  26. def OAI.WLIdentification.RingLayout.coordinates line 171
  27. theorem OAI.WLIdentification.RingLayout.hCoord_mem line 176
  28. theorem OAI.WLIdentification.RingLayout.left_mem line 181
  29. theorem OAI.WLIdentification.RingLayout.right_mem line 186
  30. theorem OAI.WLIdentification.RingLayout.top_mem line 191
  31. theorem OAI.WLIdentification.RingLayout.bottom_mem line 195
  32. def OAI.WLIdentification.RingLayout.localProj line 199
  33. def OAI.WLIdentification.RingLayout.squareForm line 202
  34. theorem OAI.WLIdentification.RingLayout.squareForm_apply line 208
  35. theorem OAI.WLIdentification.RingLayout.squareForm_nonzero line 214
  36. def OAI.WLIdentification.RingLayout.hIndex line 244
  37. def OAI.WLIdentification.RingLayout.vIndex line 248
  38. def OAI.WLIdentification.RingLayout.squareIndex line 252
  39. def OAI.WLIdentification.RingLayout.colorIndex line 256
  40. def OAI.WLIdentification.RingLayout.affine line 261
  41. abbrev OAI.WLIdentification.RingLayout.Horizontal line 280
  42. abbrev OAI.WLIdentification.RingLayout.Vertical line 281
  43. def OAI.WLIdentification.RingLayout.horizontal line 283
  44. def OAI.WLIdentification.RingLayout.vertical line 284
  45. def OAI.WLIdentification.RingLayout.pack line 285
  46. theorem OAI.WLIdentification.RingLayout.solves_iff line 289
  47. abbrev OAI.WLIdentification.RingLayout.Address line 302
  48. abbrev OAI.WLIdentification.RingLayout.MatchAddress line 303
  49. def OAI.WLIdentification.RingLayout.leftAddress line 305
  50. def OAI.WLIdentification.RingLayout.rightAddress line 307
  51. def OAI.WLIdentification.RingLayout.ringValue line 310
  52. def OAI.WLIdentification.RingLayout.linkShift line 313
  53. theorem OAI.WLIdentification.RingLayout.ringValue_rowSum line 317
  54. theorem OAI.WLIdentification.RingLayout.linkShift_rowSum line 322
  55. theorem OAI.WLIdentification.RingLayout.offsets_iff_horizontal line 328

    Source documentation

    All link square equations are lifted simultaneously. No arbitrary-address assignment substitutes for readouts shared by adjacent-coordinate pairs.

    theorem offsets_iff_horizontal (hr : 3 ≤ r) (beta : R.Block → Bit) :
    (∃ z, (R.affine (by omega)).Solves beta z) ↔
    ∃ x : R.Horizontal, ∀ e (a : R.MatchAddress e),
      R.firstForm e (R.ringValue x (R.first e) (R.leftAddress e a)) +
      R.secondForm e (R.ringValue x (R.second e) (R.rightAddress e a)) = R.linkShift beta e a := by
…

    Mentions: OAI.WLIdentification.Bit

  56. theorem OAI.WLIdentification.RingLayout.offsets_iff_rowSums line 361
  57. theorem OAI.WLIdentification.AffineBlocks.constrained_card line 387

    Source documentation

    A nonzero scalar equation cuts a binary valuation class exactly in half.

    theorem constrained_card (D : AffineBlocks C B) (beta : B → Bit) (b : B)
    (hc : D.constrained b = true) :
    2 * Fintype.card {v // D.Legal beta b v} = 2 ^ (D.coordinates b).card := by
…

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

  58. theorem OAI.WLIdentification.AffineBlocks.local_card_le line 401
  59. theorem OAI.WLIdentification.AffineBlocks.piece_card_bound line 407
  60. theorem OAI.WLIdentification.RingLayout.hCoords_card line 434
  61. theorem OAI.WLIdentification.RingLayout.coordinates_card line 442
  62. theorem OAI.WLIdentification.RingLayout.piece_card_le line 465

    Source documentation

    The advertised 26-vertex bound, including both vertices of every readout bit.

    theorem piece_card_le (hr : 2 ≤ r) (beta : R.Block → Bit) (b : R.Block) :
    Fintype.card ((R.affine hr).Piece beta b) ≤ 26 := by
…

    Mentions: OAI.WLIdentification.Bit

  63. def OAI.WLIdentification.RingLayout.owner line 478

    Source documentation

    Every vertical name has a neighboring square, even for singleton factors.

    noncomputable def owner : R.Coordinate → R.Block
  | .inl h => .inl h.1
  | .inr v => .inr ⟨v.1, v.2.1, v.2.2,
      ⟨(R.matchLabels_nonempty v.1 (finRotate r v.2.1)).choose,
        (R.matchLabels_nonempty v.1 (finRotate r v.2.1)).choose_spec⟩⟩

omit [Fintype T] [Fintype L] in
  64. theorem OAI.WLIdentification.RingLayout.owner_covers line 485
  65. theorem OAI.WLIdentification.RingLayout.arbitrary_mate line 491

    Source documentation

    All-mates reconstruction for the ring construction when r≥32.

    theorem arbitrary_mate (hr : 32 ≤ r) (H : Graph)
    (h : Equivalent r ((R.affine (by omega)).graph 0) H) :
    ∃ beta, Isomorphic H ((R.affine (by omega)).graph beta) :=
…

    Mentions: OAI.WLIdentification.Graph, OAI.WLIdentification.Equivalent, OAI.WLIdentification.Isomorphic