OAI/Algebra/DepthFive/BlockCircuit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.BlockData.middleInputs_empty_degree line 12
2. theorem OAI.Problem335.BlockData.outputInputs_empty_degree line 28
3. def OAI.Problem335.BlockData.indexedCircuit line 44

   Source documentation

   The actual homogeneous five-layer block-expansion circuit, before finite reindexing.

   def indexedCircuit (K : Type*) [CommSemiring K]
       (blocks : List (List (Fin n))) (z : Fin n) :
       IndexedDepth5Circuit K n
         (Fin n × Fin n × Fin n) (Fin n × Fin n × Fin n)
         (Lower blocks) (Middle blocks) (Upper blocks z) where
   …

   Mentions: OAI.Problem335.IndexedDepth5Circuit, OAI.Problem335.BlockData.Lower, OAI.Problem335.BlockData.Middle, OAI.Problem335.BlockData.Upper

4. def OAI.Problem335.BlockData.circuit line 74

   Source documentation

   The qualified Fin-indexed circuit produced by block expansion.

   def circuit (K : Type*) [CommSemiring K]
       (blocks : List (List (Fin n))) (z : Fin n) : Depth5Circuit K n :=
   …

   Mentions: OAI.Problem335.Depth5Circuit

5. theorem OAI.Problem335.BlockData.circuit_outputDegree line 78
6. theorem OAI.Problem335.BlockData.circuit_size line 82