Special-gate consistency as a product of signal observations

Each signal emits all its contributions once, including repeated special-gate slots. A two-state multiplicative output flag observes the designated output without adding a graph edge. Values outside a closed component can be folded into the final predicate.

def Algebraic.Aggregate.wireContribution {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (wire : Wire n g) (value : Bool) : Registers p

All contributions emitted by one signal. Repeated occurrences multiply repeatedly.

Equations

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

@[reducible, inline]

abbrev Algebraic.Aggregate.Observation {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) : Type

Aggregate registers and a two-state output observation.

Equations

• Algebraic.Aggregate.Observation p = (Algebraic.Aggregate.Registers p × ZMod 2)

def Algebraic.Aggregate.outputFlag {n g : ℕ} (out wire : Wire n g) (value : Bool) : ZMod 2

The flag is multiplicative: only the designated output emits a possibly zero value.

Equations

• Algebraic.Aggregate.outputFlag out wire value = if wire = out then if value = true then 1 else 0 else 1

def Algebraic.Aggregate.observe {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (out wire : Wire n g) (value : Bool) : Observation p

The local observation emitted by a signal vertex.

Equations

• Algebraic.Aggregate.observe p out wire value = (Algebraic.Aggregate.wireContribution p wire value, Algebraic.Aggregate.outputFlag out wire value)

def Algebraic.Aggregate.AcceptObservation {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) (a : Guess p) (state : Observation p) : Prop

The final predicate tests all special readouts and the designated output.

Equations

• Algebraic.Aggregate.AcceptObservation p a state = ((∀ (gate : Algebraic.Aggregate.SpecialGate p), Algebraic.Aggregate.Op.readout (p.lines ↑gate).op (state.1 gate) = a gate) ∧ state.2 = 1)

theorem Algebraic.Aggregate.prod_wireContribution {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (S : Finset (Wire n g)) (values : Wire n g → Bool) (gate : SpecialGate p) : (∏ wire ∈ S, wireContribution p wire (values wire)) gate = lineAggregate (p.lines ↑gate) S values

theorem Algebraic.Aggregate.prod_outputFlag {n g : ℕ} (out : Wire n g) (values : Wire n g → Bool) : ∏ wire : Wire n g, outputFlag out wire (values wire) = if values out = true then 1 else 0

theorem Algebraic.Aggregate.special_eval_eq_readout {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (line : Line (signature State) n g) (hs : Op.isSpecial line.op = true) (input : Fin n → Bool) (gates : Fin g → Bool) : line.eval interpretation input gates = Op.readout line.op (lineAggregate line Finset.univ (Wire.elim input gates))

theorem Algebraic.Aggregate.acceptObservation_iff {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (a : Guess p) (out : Wire n g) (input : Fin n → Bool) : AcceptObservation p a (∏ wire : Wire n g, observe p out wire ((erase p a).trace ordinaryInterpretation input wire)) ↔ Consistent p a input ∧ (erase p a).trace ordinaryInterpretation input out = true

For one fixed guess, the observation predicate is exactly the original consistency test and the erased circuit's output test.

def Algebraic.Aggregate.outsideObservation {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (a : Guess p) (S : Finset (Wire n g)) (out : Wire n g) (fixed : Fin n → Bool) : Observation p

All observations outside a component, evaluated at the fixed outside assignment.

Equations

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

def Algebraic.Aggregate.ComponentAccept {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (a : Guess p) (S : Finset (Wire n g)) (out : Wire n g) (fixed : Fin n → Bool) (state : Observation p) : Prop

The component's final predicate includes all fixed outside contributions.

Equations

• Algebraic.Aggregate.ComponentAccept p a S out fixed state = Algebraic.Aggregate.AcceptObservation p a (state * Algebraic.Aggregate.outsideObservation p a S out fixed)

def Algebraic.Aggregate.AcceptsGuess {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (a : Guess p) (out : Wire n g) (input : Fin n → Bool) : Prop

A guessed computation accepts when all special equations and the output check pass.

Equations

• Algebraic.Aggregate.AcceptsGuess p a out input = (Algebraic.Aggregate.Consistent p a input ∧ (Algebraic.Aggregate.erase p a).trace Algebraic.Aggregate.ordinaryInterpretation input out = true)

theorem Algebraic.Aggregate.componentAccept_iff {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (a : Guess p) (K : Cutwidth.MultiOutput.Internal.ClosedSet (erase p a)) (out : Wire n g) (fixed input : Fin n → Bool) (agree : ∀ j ∉ Cutwidth.SingleCut.inputsIn K.carrier, input j = fixed j) : ComponentAccept p a K.carrier out fixed (∏ wire : Cutwidth.MultiOutput.Internal.WireGraph.Signal K, observe p out (↑wire) ((erase p a).trace ordinaryInterpretation input ↑wire)) ↔ AcceptsGuess p a out input

Exact component observation semantics after the outside primary inputs are fixed.

theorem Algebraic.Aggregate.acceptsGuess_iff {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (a : Guess p) (out : Wire n g) (input : Fin n → Bool) : AcceptsGuess p a out input ↔ a = actualGuess p input ∧ p.trace interpretation input out = true

Accepted guesses are precisely the true guess on originally accepted inputs.

theorem Algebraic.Aggregate.accepts_iff_exists_guess {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (out : Wire n g) (input : Fin n → Bool) : p.trace interpretation input out = true ↔ ∃ (a : Guess p), AcceptsGuess p a out input

Existentially guessing the special outputs preserves the accepted inputs exactly.

theorem Algebraic.Aggregate.card_guess_mul_card_observation_le {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → Fintype (State j)] (p : Program (signature State) n g) : Fintype.card (Guess p) * Fintype.card (Observation p) ≤ 2 ^ (budget p + 1)

The observation monoid uses just one additional bit beyond the aggregate registers.