OAI/Computability/WLIdentification/ConstraintSchemas.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.WLIdentification.ComparisonSchemas line 7
  2. abbrev OAI.WLIdentification.ComparisonSchemas.InternalType line 24
  3. abbrev OAI.WLIdentification.ComparisonSchemas.Link line 25
  4. def OAI.WLIdentification.ComparisonSchemas.first line 27
  5. def OAI.WLIdentification.ComparisonSchemas.second line 32
  6. def OAI.WLIdentification.ComparisonSchemas.wire line 37
  7. def OAI.WLIdentification.ComparisonSchemas.layoutDimension line 42
  8. def OAI.WLIdentification.ComparisonSchemas.layoutLabels line 46
  9. def OAI.WLIdentification.ComparisonSchemas.firstLabel line 50
  10. def OAI.WLIdentification.ComparisonSchemas.secondLabel line 58
  11. def OAI.WLIdentification.ComparisonSchemas.firstForm line 66
  12. def OAI.WLIdentification.ComparisonSchemas.secondForm line 74
  13. def OAI.WLIdentification.ComparisonSchemas.layout line 82
  14. theorem OAI.WLIdentification.CycleRows.RowSum.sum line 135
  15. theorem OAI.WLIdentification.CycleRows.RowSum.pi line 146
  16. def OAI.WLIdentification.WireAlgebra.prefixSum line 159
  17. theorem OAI.WLIdentification.WireAlgebra.prefix_zero line 163
  18. theorem OAI.WLIdentification.WireAlgebra.prefix_last line 167
  19. theorem OAI.WLIdentification.WireAlgebra.prefix_succ line 170
  20. theorem OAI.WLIdentification.WireAlgebra.sum_adjacent line 186
  21. theorem OAI.WLIdentification.WireAlgebra.chain_lifting line 204

    Source documentation

    A wire's internal scalars cancel; the converse uses explicit prefixSum sums.

    theorem chain_lifting {n : ℕ} (left right first last : Bit) (middle : Fin n → Bit) :
    (∃ h : Fin (n + 1) → Bit,
      left + h 0 = first ∧
      (∀ i, h i.castSucc + h i.succ = middle i) ∧
      h (Fin.last n) + right = last) ↔
    left + right = first + (∑ i, middle i) + last := by
…

    Mentions: OAI.WLIdentification.Bit

  22. theorem OAI.WLIdentification.WireAlgebra.prefix_equations line 242
  23. abbrev OAI.WLIdentification.ComparisonSchemas.Address line 272
  24. abbrev OAI.WLIdentification.ComparisonSchemas.DomainAddress line 274
  25. def OAI.WLIdentification.ComparisonSchemas.sourceAddress line 276
  26. def OAI.WLIdentification.ComparisonSchemas.targetAddress line 278
  27. def OAI.WLIdentification.ComparisonSchemas.firstShift line 281
  28. def OAI.WLIdentification.ComparisonSchemas.middleShift line 284
  29. def OAI.WLIdentification.ComparisonSchemas.lastShift line 287
  30. def OAI.WLIdentification.ComparisonSchemas.wireShift line 290
  31. theorem OAI.WLIdentification.ComparisonSchemas.wireShift_rowSum line 294
  32. theorem OAI.WLIdentification.ComparisonSchemas.offsets_iff_real_rowSums line 303