Exact semantics and mixing for joint aggregate compression

Factoring local contributions preserves every special equation. Guessing one final joint state therefore recovers the true trace whenever the accumulated state agrees.

theorem Algebraic.Aggregate.Compressed.Factorization.decode_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) : c.decode (c.aggregate S values) = fun (gate : SpecialGate p) => lineAggregate (p.lines ↑gate) S values

Decoding any partial aggregate recovers the original partial registers.

theorem Algebraic.Aggregate.Compressed.Factorization.guess_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) : c.guess (c.actual input) = actualGuess p input

Decoding the true joint state gives the true special-output vector.

theorem Algebraic.Aggregate.Compressed.Factorization.componentKey_eq {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)) (x y : Fin n → Bool) (same : c.componentKey S x = c.componentKey S y) : Aggregate.componentKey p S x = Aggregate.componentKey p S y

Equal compressed keys imply equality of the original component keys.

theorem Algebraic.Aggregate.Compressed.Factorization.accepts_mix_of_componentKey_eq {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)) (closed : ClosedSet p S) (out : Wire n g) (x y : Fin n → Bool) (hx : p.trace interpretation x out = true) (hy : p.trace interpretation y out = true) (same : c.componentKey S x = c.componentKey S y) : p.trace interpretation (Cutwidth.SingleCut.mix S x y) out = true

The compressed state preserves the exact component mixing argument.

theorem Algebraic.Aggregate.Compressed.Factorization.consistent_of_aggregate_eq {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) (input : Fin n → Bool) (same : c.aggregate Finset.univ ((erase p (c.guess state)).trace ordinaryInterpretation input) = state) : Consistent p (c.guess state) input

Checking the joint state checks every original special gate.

theorem Algebraic.Aggregate.Compressed.Factorization.aggregate_eq_iff {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) (input : Fin n → Bool) : c.aggregate Finset.univ ((erase p (c.guess state)).trace ordinaryInterpretation input) = state ↔ state = c.actual input

A guessed joint state accepts only if it is the actual joint state.

theorem Algebraic.Aggregate.Compressed.card_key_le {M : Type} [Fintype M] : Fintype.card (M × M) ≤ 2 ^ budget M

Two copies of the compressed state fit in the stated budget.