OAI/Computability/WLIdentification/AcceptingBroadcast.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.WLIdentification.ProductCircuit.Shifts line 10
2. structure OAI.WLIdentification.ProductCircuit.Images line 14

   Source documentation

   General, address-dependent image consistency, as extracted from arbitrary WL mates. It is deliberately weaker than simultaneous pointwise solvability.

   structure Images (delta : C.Shifts) where
   …

3. theorem OAI.WLIdentification.ProductCircuit.Images.first_equation line 26
4. theorem OAI.WLIdentification.ProductCircuit.Images.second_equation line 31
5. theorem OAI.WLIdentification.ProductCircuit.Images.third_equation line 36
6. theorem OAI.WLIdentification.ProductCircuit.Images.forward line 42
7. theorem OAI.WLIdentification.ProductCircuit.Images.coordinate_eq_sum_of_one line 49
8. theorem OAI.WLIdentification.ProductCircuit.Images.seed line 55
9. theorem OAI.WLIdentification.ProductCircuit.Images.true_port line 68
10. theorem OAI.WLIdentification.ProductCircuit.Images.true_output line 77
11. theorem OAI.WLIdentification.ProductCircuit.cube_propagation line 85

    Source documentation

    Coordinate flips connect the entire Boolean address cube, not only the addresses actually visited by the computation.

    theorem cube_propagation (Q : (Fin r → Bool) → Prop)
        (hstep : ∀ a i, Q a → Q (fun j => if j = i then !(a j) else a j))
        {a₀ : Fin r → Bool} (h₀ : Q a₀) : ∀ a, Q a := by
    …

12. theorem OAI.WLIdentification.ProductCircuit.Images.accepted_broadcast line 116
13. theorem OAI.WLIdentification.ProductCircuit.Images.accepted_primary line 125
14. def OAI.WLIdentification.ProductCircuit.Images.primaryValue line 137
15. theorem OAI.WLIdentification.ProductCircuit.Images.primaryValue_mem line 140
16. theorem OAI.WLIdentification.ProductCircuit.Images.primary_eq_singleton line 143
17. def OAI.WLIdentification.ProductCircuit.Images.bufferValue line 159
18. theorem OAI.WLIdentification.ProductCircuit.Images.bufferValue_mem line 162
19. theorem OAI.WLIdentification.ProductCircuit.Images.buffer_values line 166
20. theorem OAI.WLIdentification.ProductCircuit.Images.primary_rowSum line 195
21. theorem OAI.WLIdentification.ProductCircuit.Images.solve_shift line 216
22. theorem OAI.WLIdentification.ProductCircuit.Images.buffer_rowSum line 221
23. theorem OAI.WLIdentification.ProductCircuit.Images.buffer_extension line 248
24. theorem OAI.WLIdentification.ProductCircuit.Images.rows_of_accepted line 259

    Source documentation

    Acceptance supplies genuine row-sum functions at ALL real types, not merely pointwise scalar images. No property outside a buffer's active domain is used.

    theorem rows_of_accepted (h : C.Accepted)
        (hd : ∀ e, CycleRows.RowSum (fun i => {x // x ∈ (C.comparisonMap e).domain i}) Bit (delta e)) :
        ∃ f : (p : C.RealType) → (Fin r → Bool) → Fin (C.realDimension p) → Bit,
          (∀ p, CycleRows.RowSum (fun _ : Fin r => Bool) (Fin (C.realDimension p) → Bit) (f p)) ∧
          ∀ e (a : (C.comparisonMap e).Point),
            C.comparisonLeft e (f (C.comparisonSource e) ((C.comparisonMap e).source a)) +
            C.comparisonRight e (f (C.comparisonTarget e) ((C.comparisonMap e).target a)) = delta e a := by
    …

    Mentions: OAI.WLIdentification.CycleRows.RowSum, OAI.WLIdentification.Bit

25. abbrev OAI.WLIdentification.ProductCircuit.wireDelta line 308
26. def OAI.WLIdentification.ProductCircuit.imagesOfEquivalent line 311
27. theorem OAI.WLIdentification.ProductCircuit.identifies_of_accepted line 321

    Source documentation

    Acceptance gives identification against every finite simple uncolored mate; no special-twist condition is imposed on its shifts.

    theorem identifies_of_accepted (hr : 32 ≤ r) (n : ℕ) (h : C.Accepted) :
        Identifies r (((C.schemas.layout n).affine (by omega)).graph 0) := by
    …

    Mentions: OAI.WLIdentification.Identifies