OAI/Computability/WLIdentification/GlobalSolvability.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WLIdentification.ComparisonSchemas.Avoids line 12

   Source documentation

   Cut an unused middle link on each private wire. End links need never be removed: the private interior alone is longer than any small support.

   def Avoids (n : ℕ) (U : Finset (S.layout n).Block) (cut : E → Fin n) : Prop :=
   …

2. theorem OAI.WLIdentification.ComparisonSchemas.exists_cuts line 15
3. def OAI.WLIdentification.ComparisonSchemas.root line 37
4. def OAI.WLIdentification.ComparisonSchemas.onLeft line 41
5. instance OAI.WLIdentification.ComparisonSchemas.(instance at line 44) line 44
6. theorem OAI.WLIdentification.ComparisonSchemas.cut_middle line 47
7. theorem OAI.WLIdentification.ComparisonSchemas.root_link line 53
8. theorem OAI.WLIdentification.ComparisonSchemas.binary_extension line 72

   Source documentation

   Every injective partial binary coordinate map extends to a permutation. This lemma preserves singleton domains rather than silently enlarging them.

   theorem binary_extension (A : Finset Bool) (hA : A.Nonempty)
       (f : {a // a ∈ A} → Bool) (hf : Function.Injective f) :
       ∃ p : Equiv.Perm Bool, ∀ a, p a.val = f a := by
   …

9. def OAI.WLIdentification.ComparisonSchemas.permutation line 100
10. theorem OAI.WLIdentification.ComparisonSchemas.permutation_apply line 104
11. def OAI.WLIdentification.ComparisonSchemas.align line 109
12. theorem OAI.WLIdentification.ComparisonSchemas.align_link line 113
13. theorem OAI.WLIdentification.RingLayout.vertical_usedLink line 139
14. abbrev OAI.WLIdentification.RingLayout.Shift line 150
15. abbrev OAI.WLIdentification.RingLayout.Potential line 151
16. def OAI.WLIdentification.RingLayout.potentialHorizontal line 153
17. def OAI.WLIdentification.RingLayout.potentialVertical line 156
18. def OAI.WLIdentification.RingLayout.translation line 160
19. theorem OAI.WLIdentification.RingLayout.translation_square line 165

    Source documentation

    The potential terms cancel on every square, leaving only its row marker multiplied by the affine link-shift equation.

    theorem translation_square (h : R.Shift) (M : R.Potential) (b : R.Square) :
        R.firstForm b.1 (R.horizontal (R.translation h M) (R.leftH b)) +
          R.secondForm b.1 (R.horizontal (R.translation h M) (R.rightH b)) +
          R.vertical (R.translation h M) (R.topV b) +
          R.vertical (R.translation h M) (R.bottomV b) =
        Marker.delta b.2.1 * (R.firstForm b.1 (h (R.first b.1)) +
          R.secondForm b.1 (h (R.second b.1))) := by
    …

    Mentions: OAI.WLIdentification.Marker.delta

20. theorem OAI.WLIdentification.ComparisonSchemas.align_aligned line 186
21. theorem OAI.WLIdentification.ComparisonSchemas.root_edge line 191
22. theorem OAI.WLIdentification.ComparisonSchemas.root_reachable line 204
23. abbrev OAI.WLIdentification.ComparisonSchemas.RealShift line 213
24. def OAI.WLIdentification.ComparisonSchemas.linkConstant line 215
25. def OAI.WLIdentification.ComparisonSchemas.specialTwist line 220
26. def OAI.WLIdentification.ComparisonSchemas.starShift line 226

    Source documentation

    Completing the cut layout to rooted stars gives a uniform affine shift. The real vectors may be arbitrary; internal values are constant on each arm.

    def starShift (n : ℕ) (cut : E → Fin n) (b : E → Bit) (q : S.RealShift) : (S.layout n).Shift
      | .inl p => q p
      | .inr (e, i) => fun _ => if S.onLeft n cut e i then S.left e (q (S.source e))
          else b e + S.right e (q (S.target e))

    Mentions: OAI.WLIdentification.Bit

27. theorem OAI.WLIdentification.ComparisonSchemas.starShift_link line 231
28. theorem OAI.WLIdentification.ComparisonSchemas.translation_legal line 256
29. def OAI.WLIdentification.RingLayout.coordinateName line 281
30. theorem OAI.WLIdentification.RingLayout.coordinate_name_mem line 285
31. theorem OAI.WLIdentification.RingLayout.cornerMarker_symm line 304
32. theorem OAI.WLIdentification.RingLayout.nonwrapping_exact line 319
33. theorem OAI.WLIdentification.RingLayout.adjust_potential line 335

    Source documentation

    On a nonwrapping support any two shifts with the same affine link equations induce the same offset family after a potential adjustment.

    theorem adjust_potential (hr : 3 ≤ r) {U : Finset R.Block}
        (hw : ¬R.Wrapping (by omega) U) (old new : R.Shift) (M : R.Potential)
        (he : ∀ l ∈ R.usedLinks U,
          R.firstForm l (old (R.first l)) + R.secondForm l (old (R.second l)) =
          R.firstForm l (new (R.first l)) + R.secondForm l (new (R.second l))) :
        ∃ N : R.Potential, ∀ b ∈ U, ∀ c ∈ R.coordinates b,
          R.translation new N c = R.translation old M c := by
    …

34. def OAI.WLIdentification.ComparisonSchemas.GoodAddress line 382
35. theorem OAI.WLIdentification.ComparisonSchemas.goodAddress_exists line 387
36. theorem OAI.WLIdentification.ComparisonSchemas.avoids_mono line 403
37. theorem OAI.WLIdentification.ComparisonSchemas.goodAddress_mono line 409