OAI/Algebra/DepthFive/CircuitStructure.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.homogeneous_indexed_product_positive_factors line 17

   Source documentation

   An indexed version of positive-factor normalization. The resulting list is a sublist of the original gate occurrences, so sharing and multiplicity are preserved.

   theorem homogeneous_indexed_product_positive_factors
       {K : Type u} [CommSemiring K] {σ : Type v} {ι : Type w}
       (l : List ι) (p : ι → MvPolynomial σ K) (d : ι → ℕ)
       (hl : ∀ i ∈ l, (p i).IsHomogeneous (d i)) :
       ∃ a : K, ∃ factors : List ι,
         factors.Sublist l ∧
         (∀ i ∈ factors, 0 < d i) ∧
         (factors.map d).sum = (l.map d).sum ∧
         (l.map p).prod = C a * (factors.map p).prod ∧
         factors.length ≤ (l.map d).sum := by
   …

2. theorem OAI.Problem335.upperValue_positive_factors line 42

   Source documentation

   Every upper product is a scalar multiple of positive-formal-degree middle-gate occurrences whose degrees add to the original formal degree.

   theorem upperValue_positive_factors
       {K : Type u} [CommSemiring K] {n : ℕ}
       (c : Depth5Circuit K n) (i : Fin c.upperCount) :
       ∃ a : K, ∃ factors : List (Fin c.middleCount),
         factors.Sublist (c.upperInputs i) ∧
         (∀ j ∈ factors, 0 < c.middleDegree j) ∧
         (factors.map c.middleDegree).sum =
           ((c.upperInputs i).map c.middleDegree).sum ∧
         upperValue c i = C a * (factors.map (middleValue c)).prod ∧
         factors.length ≤ ((c.upperInputs i).map c.middleDegree).sum := by
   …

   Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.upperValue, OAI.Problem335.middleValue

3. theorem OAI.Problem335.output_term_positive_factors line 58

   Source documentation

   For an upper gate occurring at the output, the positive factor degrees sum to the circuit output degree, hence there are at most that many factors.

   theorem output_term_positive_factors
       {K : Type u} [CommSemiring K] {n : ℕ}
       (c : Depth5Circuit K n) (entry : K × Fin c.upperCount)
       (hentry : entry ∈ c.outputInputs) :
       ∃ a : K, ∃ factors : List (Fin c.middleCount),
         factors.Sublist (c.upperInputs entry.2) ∧
         (∀ j ∈ factors, 0 < c.middleDegree j) ∧
         (factors.map c.middleDegree).sum = c.outputDegree ∧
         upperValue c entry.2 = C a * (factors.map (middleValue c)).prod ∧
         factors.length ≤ c.outputDegree := by
   …

   Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.upperValue, OAI.Problem335.middleValue