OAI/Algebra/DepthFive/GateSums.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem335.gateCoefficient line 13

   Source documentation

   The combined coefficient of all wires from a fixed predecessor. Wire multiplicity is absorbed into this coefficient, not charged as gates.

   def gateCoefficient {K ι : Type*} [AddCommMonoid K] [DecidableEq ι]
       (inputs : List (K × ι)) (i : ι) : K :=
   …

2. theorem OAI.Problem335.gateCoefficient_nil line 17
3. theorem OAI.Problem335.gateCoefficient_cons line 21
4. theorem OAI.Problem335.list_weighted_sum_eq_sum line 28

   Source documentation

   Any finite list of weighted inputs can be regrouped over its finite gate type.

   theorem list_weighted_sum_eq_sum {K R ι : Type*} [Semiring K] [Semiring R]
       [Fintype ι] [DecidableEq ι] (f : K →+* R) (value : ι → R)
       (inputs : List (K × ι)) :
       (inputs.map (fun entry => f entry.1 * value entry.2)).sum =
         ∑ i, f (gateCoefficient inputs i) * value i := by
   …

   Mentions: OAI.Problem335.gateCoefficient

5. theorem OAI.Problem335.gateCoefficient_eq_zero_of_not_mem line 43

   Source documentation

   A combined coefficient vanishes if its predecessor does not occur.

   theorem gateCoefficient_eq_zero_of_not_mem {K ι : Type*}
       [AddCommMonoid K] [DecidableEq ι] (inputs : List (K × ι)) (i : ι)
       (h : ∀ entry ∈ inputs, entry.2 ≠ i) : gateCoefficient inputs i = 0 := by
   …

   Mentions: OAI.Problem335.gateCoefficient

6. theorem OAI.Problem335.exists_mem_of_gateCoefficient_ne_zero line 53

   Source documentation

   A nonzero combined coefficient must come from an actual wire.

   theorem exists_mem_of_gateCoefficient_ne_zero {K ι : Type*}
       [AddCommMonoid K] [DecidableEq ι] (inputs : List (K × ι)) (i : ι)
       (h : gateCoefficient inputs i ≠ 0) : ∃ entry ∈ inputs, entry.2 = i := by
   …

   Mentions: OAI.Problem335.gateCoefficient

7. theorem OAI.Problem335.bottomValue_eq_sum line 62
8. theorem OAI.Problem335.middleValue_eq_sum line 68
9. theorem OAI.Problem335.circuitValue_eq_sum line 74
10. theorem OAI.Problem335.bottomDegree_of_gateCoefficient_ne_zero line 81

    Source documentation

    Aggregating wires preserves the bottom homogeneous-degree constraint.

    theorem bottomDegree_of_gateCoefficient_ne_zero {K : Type*} [CommSemiring K] {n : ℕ}
        (c : Depth5Circuit K n) (i : Fin c.bottomCount) (j : Fin c.leafCount)
        (h : gateCoefficient (c.bottomInputs i) j ≠ 0) :
        d5LeafDegree (c.leaves j) = c.bottomDegree i := by
    …

    Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.gateCoefficient, OAI.Problem335.d5LeafDegree

11. theorem OAI.Problem335.middleDegree_of_gateCoefficient_ne_zero line 89

    Source documentation

    Aggregating wires preserves the middle homogeneous-degree constraint.

    theorem middleDegree_of_gateCoefficient_ne_zero {K : Type*} [CommSemiring K] {n : ℕ}
        (c : Depth5Circuit K n) (i : Fin c.middleCount) (j : Fin c.lowerCount)
        (h : gateCoefficient (c.middleInputs i) j ≠ 0) :
        ((c.lowerInputs j).map c.bottomDegree).sum = c.middleDegree i := by
    …

    Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.gateCoefficient

12. theorem OAI.Problem335.outputDegree_of_gateCoefficient_ne_zero line 97

    Source documentation

    Aggregating wires preserves the output homogeneous-degree constraint.

    theorem outputDegree_of_gateCoefficient_ne_zero {K : Type*} [CommSemiring K] {n : ℕ}
        (c : Depth5Circuit K n) (j : Fin c.upperCount)
        (h : gateCoefficient c.outputInputs j ≠ 0) :
        ((c.upperInputs j).map c.middleDegree).sum = c.outputDegree := by
    …

    Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.gateCoefficient