Jointly compressed aggregate registers

A single finite monoid can encode the simultaneous contributions to every special gate. Guessing its final state determines all special outputs; checking the same state checks every special equation. This charges joint states rather than gates.

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

A local factorization of all special registers through one commutative monoid.

• contribution : Wire n g → Bool → M

  The compressed contribution emitted once by each signal.

• decode : M →* Registers p

  Decoding recovers all original special registers.

• factor (wire : Wire n g) (value : Bool) : self.decode (self.contribution wire value) = wireContribution p wire value

  Decoding commutes with each local contribution, including repeated slots.

def Algebraic.Aggregate.Compressed.Factorization.aggregate {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] {n g : ℕ} {p : Program (signature State) n g} {M : Type} [CommMonoid M] (c : Factorization p M) (S : Finset (Wire n g)) (values : Wire n g → Bool) : M

The compressed state emitted by a set of signals.

Equations

• c.aggregate S values = ∏ wire ∈ S, c.contribution wire (values wire)

def Algebraic.Aggregate.Compressed.Factorization.guess {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] {n g : ℕ} {p : Program (signature State) n g} {M : Type} [CommMonoid M] (c : Factorization p M) (state : M) : Guess p

A joint state determines every Boolean special-gate output.

Equations

• c.guess state gate = Algebraic.Aggregate.Op.readout (p.lines ↑gate).op (c.decode state gate)

def Algebraic.Aggregate.Compressed.Factorization.actual {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] {n g : ℕ} {p : Program (signature State) n g} {M : Type} [CommMonoid M] (c : Factorization p M) (input : Fin n → Bool) : M

The joint state of the true circuit evaluation.

Equations

• c.actual input = c.aggregate Finset.univ (p.trace Algebraic.Aggregate.interpretation input)

def Algebraic.Aggregate.Compressed.Factorization.componentKey {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] {n g : ℕ} {p : Program (signature State) n g} {M : Type} [CommMonoid M] (c : Factorization p M) (S : Finset (Wire n g)) (input : Fin n → Bool) : M × M

One final-state guess and one partial aggregate form the component mixing key.

Equations

• c.componentKey S input = (c.actual input, c.aggregate S (p.trace Algebraic.Aggregate.interpretation input))

def Algebraic.Aggregate.Compressed.budget (M : Type) [Fintype M] : ℕ

The budget counts the guessed joint state and its independent accumulator.

Equations

• Algebraic.Aggregate.Compressed.budget M = 2 * Nat.clog 2 (Fintype.card M)