OAI/Computability/WLIdentification/LinearExtensions.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.WLIdentification.AffineBlocks.Response line 10
2. def OAI.WLIdentification.AffineBlocks.zeroVertex line 12
3. def OAI.WLIdentification.AffineBlocks.BlockWinning line 14
4. theorem OAI.WLIdentification.AffineBlocks.blockWinning_consistent line 20

   Source documentation

   Stable block responses agree on every shared bit. The probe retains all current responses and asks one zero bit through the stable extension bijection.

   theorem blockWinning_consistent {k : ℕ} (hk : 2 ≤ k) {beta : B → Bit}
       {p : Fin k → D.Response beta} (hp : D.BlockWinning p) (i j : Fin k)
       (c : C) (hi : c ∈ D.coordinates (p i).1) (hj : c ∈ D.coordinates (p j).1) :
       (p i).2.val ⟨c, hi⟩ = (p j).2.val ⟨c, hj⟩ := by
   …

   Mentions: OAI.WLIdentification.Bit

5. theorem OAI.WLIdentification.AffineBlocks.blockWinning_exists line 34
6. theorem OAI.WLIdentification.AffineBlocks.blockWinning_extend line 50

   Source documentation

   One response extends simultaneously in every replacement slot, and agrees with all old responses, even the one to be discarded. This is the literal place-before-discard property needed for ring transfers.

   theorem blockWinning_extend {k : ℕ} (hk : 2 ≤ k) {beta : B → Bit}
       {p : Fin k → D.Response beta} (hp : D.BlockWinning p) (b : B) :
       ∃ q : {v // D.Legal beta b v},
         (∀ i, D.BlockWinning (Function.update p i ⟨b, q⟩)) ∧
         (∀ i c (hi : c ∈ D.coordinates (p i).1) (hb : c ∈ D.coordinates b),
           (p i).2.val ⟨c, hi⟩ = q.val ⟨c, hb⟩) := by
   …

   Mentions: OAI.WLIdentification.Bit

7. def OAI.WLIdentification.AffineBlocks.responseValue line 92
8. theorem OAI.WLIdentification.AffineBlocks.responseValue_of_mem line 96
9. def OAI.WLIdentification.AffineBlocks.Agree line 100
10. theorem OAI.WLIdentification.AffineBlocks.agree_refl line 105
11. theorem OAI.WLIdentification.AffineBlocks.agree_symm line 108
12. theorem OAI.WLIdentification.AffineBlocks.blockWinning_agree line 111
13. theorem OAI.WLIdentification.AffineBlocks.blockWinning_transfer line 119

    Source documentation

    Sequentially transfer every slot to its prescribed next block. For every row the shared-coordinate values of its old block are retained.

    theorem blockWinning_transfer {beta : B → Bit} {k : ℕ} (hk : 2 ≤ k)
        {p : Fin k → D.Response beta} (hp : D.BlockWinning p) (b : Fin k → B) :
        ∃ q : Fin k → D.Response beta, D.BlockWinning q ∧
          (∀ i, (q i).1 = b i) ∧ (∀ i, D.Agree (p i) (q i)) := by
    …

    Mentions: OAI.WLIdentification.Bit

14. theorem OAI.WLIdentification.AffineBlocks.response_legal line 159
15. abbrev OAI.WLIdentification.RingLayout.siteRing line 172
16. abbrev OAI.WLIdentification.RingLayout.squareRing line 174
17. def OAI.WLIdentification.RingLayout.responseRingSum line 177
18. theorem OAI.WLIdentification.RingLayout.horizontal_agree line 182
19. theorem OAI.WLIdentification.RingLayout.square_ring_sum line 194

    Source documentation

    The actual responses of a square ring obey its summed equation. Verticals cancel because adjacent stable marked squares agree on their shared bit.

    theorem square_ring_sum (hr : 2 ≤ r) {beta : R.Block → Bit}
        {q : Fin r → (R.affine hr).Response beta} (hq : (R.affine hr).BlockWinning q)
        (e : L) (a : R.MatchAddress e)
        (hn : ∀ i, (q i).1 = .inr (R.squareRing e a i)) :
        R.firstForm e (∑ i, R.horizontal ((R.affine hr).responseValue (q i)) (R.leftH (R.squareRing e a i))) +
          R.secondForm e (∑ i, R.horizontal ((R.affine hr).responseValue (q i)) (R.rightH (R.squareRing e a i))) =
          R.linkShift beta e a := by
    …

    Mentions: OAI.WLIdentification.Bit

20. def OAI.WLIdentification.RingLayout.ImageSet line 231

    Source documentation

    Site-ring images are defined by all stable responses, not by a selected memoryless strategy or by a simultaneous choice of endpoint vectors.

    def ImageSet (hr : 2 ≤ r) (beta : R.Block → Bit) (t : T) (a : R.Address t) :
        Set (Fin (R.dimension t) → Bit) :=
    …

    Mentions: OAI.WLIdentification.Bit

21. theorem OAI.WLIdentification.RingLayout.imageSet_nonempty line 237
22. theorem OAI.WLIdentification.RingLayout.transfer_left_sums line 248
23. theorem OAI.WLIdentification.RingLayout.transfer_right_sums line 265
24. theorem OAI.WLIdentification.RingLayout.imageSet_left_support line 282
25. theorem OAI.WLIdentification.RingLayout.imageSet_right_support line 298