OAI/Algebra/DepthFive/BlockCircuitValue.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.BlockData.indexedCircuit_bottomValue line 15
2. theorem OAI.Problem335.BlockData.indexedCircuit_lowerValue line 20
3. theorem OAI.Problem335.BlockData.indexedCircuit_middleValue line 26
4. theorem OAI.Problem335.BlockData.indexedCircuit_upperValue line 35
5. theorem OAI.Problem335.BlockData.indexedCircuit_circuitValue line 45

   Source documentation

   The block circuit computes the corresponding entry of the product of block matrices.

   theorem indexedCircuit_circuitValue (K : Type*) [CommSemiring K]
       (blocks : List (List (Fin n))) (z : Fin n) :
       (indexedCircuit K blocks z).circuitValue =
         ((blocks.map (immBlock K n)).prod) z z := by
   …

   Mentions: OAI.Problem335.BlockData.indexedCircuit, OAI.Problem335.circuitValue, OAI.Problem335.immBlock

6. theorem OAI.Problem335.BlockData.circuit_value line 61

   Source documentation

   Semantic correctness after converting all gate indices to Fin.

   theorem circuit_value (K : Type*) [CommSemiring K]
       (blocks : List (List (Fin n))) (z : Fin n) :
       Problem335.circuitValue (circuit K blocks z) =
         ((blocks.map (immBlock K n)).prod) z z := by
   …

   Mentions: OAI.Problem335.circuitValue, OAI.Problem335.BlockData.circuit, OAI.Problem335.immBlock

7. theorem OAI.Problem335.BlockData.circuit_value_eq_imm line 69

   Source documentation

   Any partition of the layers produces a circuit computing the qualified IMM polynomial.

   theorem circuit_value_eq_imm (K : Type*) [CommSemiring K]
       (hn : 0 < n) (blocks : List (List (Fin n)))
       (hblocks : blocks.flatten = List.finRange n) :
       Problem335.circuitValue (circuit K blocks ⟨0, hn⟩) = imm K n := by
   …

   Mentions: OAI.Problem335.circuitValue, OAI.Problem335.BlockData.circuit, OAI.Problem335.imm