OAI/Computability/WLIdentification/AddressArithmetic.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WLIdentification.BinaryAddress.carryMap line 9
2. theorem OAI.WLIdentification.BinaryAddress.carryMap_rel line 18
3. theorem OAI.WLIdentification.BinaryAddress.carryMap_sound line 39
4. theorem OAI.WLIdentification.BinaryAddress.carryMap_complete line 45
5. def OAI.WLIdentification.BinaryAddress.cycleMap line 58

   Source documentation

   An additional all-ones case supplies the cyclic seam for positions only.

   def cycleMap (d : ℕ) : Option (Fin d) → ProductMap d
     | none => ProductMap.singleton (fun _ => true) (fun _ => false)
     | some h => carryMap h

   Mentions: OAI.WLIdentification.ProductMap, OAI.WLIdentification.ProductMap.singleton, OAI.WLIdentification.BinaryAddress.carryMap

6. theorem OAI.WLIdentification.BinaryAddress.cycleMap_sound line 62
7. theorem OAI.WLIdentification.BinaryAddress.cycleMap_complete line 72
8. def OAI.WLIdentification.BinaryAddress.rotation line 79
9. theorem OAI.WLIdentification.BinaryAddress.rotation_advance line 82
10. theorem OAI.WLIdentification.BinaryAddress.value_lt_iff line 97

    Source documentation

    The largest differing bit determines strict numeric order.

    theorem value_lt_iff {d : ℕ} (x y : Bits d) : value x < value y ↔
        ∃ h : Fin d, x h = false ∧ y h = true ∧ ∀ i, h < i → x i = y i := by
    …

    Mentions: OAI.WLIdentification.BinaryAddress.Bits, OAI.WLIdentification.BinaryAddress.value

11. def OAI.WLIdentification.BinaryAddress.aboveMap line 142

    Source documentation

    A threshold request fixes its high prefix and first strictly-larger bit.

    def aboveMap {d : ℕ} (x : Bits d) (h : Fin d) : ProductMap d where
    …

    Mentions: OAI.WLIdentification.BinaryAddress.Bits, OAI.WLIdentification.ProductMap

12. theorem OAI.WLIdentification.BinaryAddress.aboveMap_rel line 148
13. abbrev OAI.WLIdentification.BinaryAddress.ThresholdCase line 164
14. def OAI.WLIdentification.BinaryAddress.thresholdMap line 166
15. theorem OAI.WLIdentification.BinaryAddress.threshold_sound line 170
16. theorem OAI.WLIdentification.BinaryAddress.threshold_complete line 181
17. theorem OAI.WLIdentification.ProductCircuit.edge_rel line 194
18. theorem OAI.WLIdentification.ProductCircuit.seed_rel line 199