Observing a compressed candidate computation

One joint-state guess determines all special outputs. A product of local observations checks that guess and the designated output, including after outside inputs are fixed.

@[reducible, inline]

abbrev Algebraic.Aggregate.Compressed.Observation (M : Type) : Type

The joint aggregate and the multiplicative output flag.

Equations

• Algebraic.Aggregate.Compressed.Observation M = (M × ZMod 2)

def Algebraic.Aggregate.Compressed.Factorization.observe {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) (out wire : Wire n g) (value : Bool) : Observation M

Each signal contributes once to the compressed state and designated output.

Equations

• c.observe out wire value = (c.contribution wire value, Algebraic.Aggregate.outputFlag out wire value)

def Algebraic.Aggregate.Compressed.Factorization.AcceptObservation {M : Type} (state : M) (observed : Observation M) : Prop

The final aggregate equals its guess and the designated output is true.

Equations

• Algebraic.Aggregate.Compressed.Factorization.AcceptObservation state observed = (observed.1 = state ∧ observed.2 = 1)

def Algebraic.Aggregate.Compressed.Factorization.AcceptsGuess {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) (out : Wire n g) (input : Fin n → Bool) : Prop

A candidate accepts when its accumulated state agrees with its guess.

Equations

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

theorem Algebraic.Aggregate.Compressed.Factorization.acceptObservation_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) (out : Wire n g) (input : Fin n → Bool) : AcceptObservation state (∏ wire : Wire n g, c.observe out wire ((erase p (c.guess state)).trace ordinaryInterpretation input wire)) ↔ c.AcceptsGuess state out input

The observation predicate is the candidate's aggregate and output check.

theorem Algebraic.Aggregate.Compressed.Factorization.acceptsGuess_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) (out : Wire n g) (input : Fin n → Bool) : c.AcceptsGuess state out input ↔ state = c.actual input ∧ p.trace interpretation input out = true

An accepted state is the actual state and the original circuit accepts.

theorem Algebraic.Aggregate.Compressed.Factorization.accepts_iff_exists_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) (out : Wire n g) (input : Fin n → Bool) : p.trace interpretation input out = true ↔ ∃ (state : M), c.AcceptsGuess state out input

Existentially guessing the compressed state preserves the original function.

def Algebraic.Aggregate.Compressed.Factorization.outsideObservation {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) (S : Finset (Wire n g)) (out : Wire n g) (fixed : Fin n → Bool) : Observation M

Fixed outside signals contribute to the final observation predicate.

Equations

• c.outsideObservation state S out fixed = ∏ wire ∈ Sᶜ, c.observe out wire ((Algebraic.Aggregate.erase p (c.guess state)).trace Algebraic.Aggregate.ordinaryInterpretation fixed wire)

def Algebraic.Aggregate.Compressed.Factorization.ComponentAccept {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) (S : Finset (Wire n g)) (out : Wire n g) (fixed : Fin n → Bool) (observed : Observation M) : Prop

Component acceptance includes the already fixed outside observations.

Equations

• c.ComponentAccept state S out fixed observed = Algebraic.Aggregate.Compressed.Factorization.AcceptObservation state (observed * c.outsideObservation state S out fixed)

theorem Algebraic.Aggregate.Compressed.Factorization.componentAccept_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) (K : Cutwidth.MultiOutput.Internal.ClosedSet (erase p (c.guess state))) (out : Wire n g) (fixed input : Fin n → Bool) (agree : ∀ j ∉ Cutwidth.SingleCut.inputsIn K.carrier, input j = fixed j) : c.ComponentAccept state K.carrier out fixed (∏ wire : Cutwidth.MultiOutput.Internal.WireGraph.Signal K, c.observe out (↑wire) ((erase p (c.guess state)).trace ordinaryInterpretation input ↑wire)) ↔ c.AcceptsGuess state out input

Closed components retain exact compressed-state semantics after restriction.

theorem Algebraic.Aggregate.Compressed.card_guess_mul_card_observation_le {M : Type} [Fintype M] : Fintype.card M * Fintype.card (Observation M) ≤ 2 ^ (budget M + 1)

The guess and observation use only one output bit beyond the compressed budget.