OAI/Computability/SpaceSimulation/Evaluation/Schedule.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Verification of the activation flow at a given circuit, using induction on the meter. The induction contract is from every initial pool.

  1. theorem OAI.Fifths.Circuit.Ylimit line 14
  2. theorem OAI.Fifths.Circuit.fee_form line 17
  3. theorem OAI.Fifths.Circuit.width_below line 24
  4. def OAI.Fifths.Circuit.solved line 27
  5. structure OAI.Fifths.Circuit.HasKids line 31
  6. def OAI.Fifths.Circuit.sampleTerm line 41
  7. def OAI.Fifths.Circuit.predVal line 46
  8. def OAI.Fifths.Circuit.summand line 51

    Source comment

    Evaluation of a gate on its distinguished (possibly shifted) register, evaluating each factor already at semantic child vectors.
    def summand (x : C.Request) (H : C.Vec) (z y : ℕ) : C.F :=
…
  9. def OAI.Fifths.Circuit.formula line 53
  10. def OAI.Fifths.Circuit.cropped line 55
  11. def OAI.Fifths.Circuit.advanceR line 57
  12. theorem OAI.Fifths.Circuit.sample_one line 64

    Source documentation

    Forward and reverse call on an array. Caller labors over arbitrary pool R; hash coefficient is between those calls.

    theorem sample_one (R : C.Pool) {s z y i r : ℕ}
    (a : s < C.P.n) (b : z ≤ C.width) (c : y < C.YCount x.node)
    (d : i < C.count) (e : r < C.P.n)
    (u w : C.F) :
    C.flow.Continues (B x.node) R (C.fSample x s z y i r u w) R
      (C.fSample x s z y i (r+1) u (w + sampleTerm x R z y i r)) := by
…

    Mentions: OAI.Fifths.Circuit.sampleTerm

  13. theorem OAI.Fifths.Circuit.sample_seq line 100

    Source documentation

    The sum of the interpolated two-word test over sample points.

    theorem sample_seq (R : C.Pool) {s z y i : ℕ} (n : ℕ)
    (a : s < C.P.n) (b : z ≤ C.width) (c : y < C.YCount x.node)
    (d : i < C.count) (e : n ≤ C.P.n)
    (u : C.F) :
    C.flow.Continues (B x.node) R (C.fSample x s z y i 0 u 0) R
      (C.fSample x s z y i n u (∑ r ∈ range n, sampleTerm x R z y i r)) := by
…

    Mentions: OAI.Fifths.Circuit.sampleTerm

  14. theorem OAI.Fifths.Circuit.factor_one line 112
  15. theorem OAI.Fifths.Circuit.factor_seq line 135
  16. theorem OAI.Fifths.Circuit.guess_one line 149
  17. theorem OAI.Fifths.Circuit.guess_seq line 165
  18. theorem OAI.Fifths.Circuit.coord_one line 198
  19. theorem OAI.Fifths.Circuit.coord_seq line 213
  20. theorem OAI.Fifths.Circuit.outer_one line 242
  21. theorem OAI.Fifths.Circuit.outer_seq line 274
  22. theorem OAI.Fifths.Circuit.extracted line 293
  23. theorem OAI.Fifths.Circuit.recurse_node line 324
  24. theorem OAI.Fifths.Circuit.answers line 336