OAI/Computability/FourierCircuit/Core.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.ExactFourier.Gate line 9

   Source documentation

   One charged scalar gate, referencing only available values.

   Also declared: ComparatorChallenges/ExactFourier.lean:13 (same declaration text).

   inductive Gate (w : ℕ) where
   …

2. def OAI.ExactFourier.Gate.eval line 14

   Also declared: ComparatorChallenges/ExactFourier.lean:18 (same declaration text).

3. inductive OAI.ExactFourier.Program line 20

   Source documentation

   A topologically ordered scalar DAG; available values are never consumed.

   Also declared: ComparatorChallenges/ExactFourier.lean:24 (same declaration text).

   inductive Program (n : ℕ) : ℕ → Type where
   …

4. def OAI.ExactFourier.Program.eval line 24

   Also declared: ComparatorChallenges/ExactFourier.lean:28 (same declaration text).

5. structure OAI.ExactFourier.Circuit line 32

   Source documentation

   Outputs name available values, so permutations and arbitrary fanout are uncharged.

   Also declared: ComparatorChallenges/ExactFourier.lean:36 (same declaration text).

   structure Circuit (n : ℕ) where
   …

6. def OAI.ExactFourier.Circuit.eval line 37

   Also declared: ComparatorChallenges/ExactFourier.lean:41 (same declaration text).

7. def OAI.ExactFourier.zeta line 40

   Also declared: ComparatorChallenges/ExactFourier.lean:44 (same declaration text), ComparatorChallenges/UniformFourier.lean:6 (same declaration text).

8. def OAI.ExactFourier.fourierMatrix line 41

   Also declared: ComparatorChallenges/ExactFourier.lean:45 (same declaration text).

9. def OAI.ExactFourier.Circuit.Computes line 44

   Also declared: ComparatorChallenges/ExactFourier.lean:48 (same declaration text).

10. def OAI.ExactFourier.MainStatement line 47

    Also declared: ComparatorChallenges/ExactFourier.lean:52 (same declaration text).