The canonical joint register generated by signal contributions

Every aggregate circuit has an unconditional local factorization: take the submonoid of its register product generated by the two contributions available at every signal. Its size can be much smaller than the product of the original register sizes.

def Algebraic.Aggregate.Compressed.generated {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] {n g : ℕ} (p : Program (signature State) n g) : Submonoid (Registers p)

All locally available joint contributions generate a canonical compressed monoid.

Equations

• Algebraic.Aggregate.Compressed.generated p = Submonoid.closure (Set.range fun (pair : Cslib.Circuits.Wire n g × Bool) => Algebraic.Aggregate.wireContribution p pair.1 pair.2)

@[instance_reducible]

noncomputable instance Algebraic.Aggregate.Compressed.instFintypeSubtypeRegistersMemSubmonoidGenerated {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] {n g : ℕ} [(j : J) → Fintype (State j)] (p : Program (signature State) n g) : Fintype ↥(generated p)

Equations

• Algebraic.Aggregate.Compressed.instFintypeSubtypeRegistersMemSubmonoidGenerated p = Fintype.ofFinite ↥(Algebraic.Aggregate.Compressed.generated p)

def Algebraic.Aggregate.Compressed.generatedFactorization {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] {n g : ℕ} (p : Program (signature State) n g) : Factorization p ↥(generated p)

Every circuit factors through its generated joint register, without an extra premise.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Cutwidth.Aggregate.Compressed.sourceReductionHardFamily_eventually_lt_size_generated {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] [(j : J) → Fintype (State j)] (D : ℕ → ℕ) (hD : (fun (n : ℕ) => ↑(D n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (c : Circuit (Aggregate.signature State) n 1), (c.Computes Aggregate.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => Extractor.sourceReductionHardFamily n x) → Aggregate.Compressed.budget ↥(Aggregate.Compressed.generated c.program) ≤ D n → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n < ↑c.size

The automatic generated-register instance retains the explicit Gaussian coefficient.