Actual circuit messages as finite signed literal sets

Selected conjunction slots become literal sets on Alice's input coordinates. Identical slots collapse and conflicting literals remain, preserving the original message exactly without a circuit normalization assumption.

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Joint.conjunctionLiterals {r n g : ℕ} (polarity : Fin r → Bool) (wires : Fin r → Wire n g) (U : Finset (Fin n)) : Finset (↥U × Bool)

Signed literals on selected primary inputs of an actual conjunction line.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Joint.conjunctionLiterals polarity wires U = {t : ↥U × Bool | ∃ (slot : Fin r), wires slot = Cslib.Circuits.Wire.input ↑t.1 ∧ polarity slot = t.2}

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Joint.lineLiterals {n g : ℕ} (line : Line Aggregate.Geometry.signature n g) (U : Finset (Fin n)) : Finset (↥U × Bool)

Literal representation of a conjunction message; affine lines have no literals.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.Cutwidth.Aggregate.Geometry.Joint.lineLiterals { op := Algebraic.Aggregate.Geometry.Op.affine arity bias coefficient, wires := wires } U = ∅

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.mem_conjunctionLiterals {r n g : ℕ} (polarity : Fin r → Bool) (wires : Fin r → Wire n g) (U : Finset (Fin n)) (t : ↥U × Bool) : t ∈ conjunctionLiterals polarity wires U ↔ ∃ (slot : Fin r), wires slot = Wire.input ↑t.1 ∧ polarity slot = t.2

Membership records an actual selected primary slot and its polarity.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.mem_conjunctionLiteralVars {r n g : ℕ} (polarity : Fin r → Bool) (wires : Fin r → Wire n g) (U : Finset (Fin n)) (i : ↥U) : i ∈ literalVars (conjunctionLiterals polarity wires U) ↔ ∃ (slot : Fin r), wires slot = Wire.input ↑i

The variables of a selected literal set are exactly selected primary wires.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.eval_conjunctionLiterals {r n g : ℕ} (polarity : Fin r → Bool) (wires : Fin r → Wire n g) (U : Finset (Fin n)) (x : ↥U → Bool) : evalLiterals (conjunctionLiterals polarity wires U) x = Aggregate.Geometry.conjunctionSummary polarity wires U (Wire.elim (glue U x fun (x : ↥Uᶜ) => false) fun (x : Fin g) => false)

Literal-set evaluation is exactly the original partial conjunction message.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.lineSummary_eq_evalLiterals {n g : ℕ} (line : Line Aggregate.Geometry.signature n g) (conjunction : Aggregate.Geometry.Op.isConjunction line.op = true) (U : Finset (Fin n)) (x : ↥U → Bool) : Aggregate.Geometry.lineSummary line U (Wire.elim (glue U x fun (x : ↥Uᶜ) => false) fun (x : Fin g) => false) = evalLiterals (lineLiterals line U) x

Conjunction lines retain exactly their literal-set message.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.two_le_literalVars_iff_selectedPair {n g : ℕ} (line : Line Aggregate.Geometry.signature n g) (U : Finset (Fin n)) : 2 ≤ (literalVars (lineLiterals line U)).card ↔ Aggregate.Geometry.SelectedPair line U

A selected pair is exactly a literal-set message on at least two variables.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.key_eq_evalLiterals_of_selectedPair {n g : ℕ} (p : Program Aggregate.Geometry.signature n g) (U : Finset (Fin n)) (gate : Fin g) (selected : Aggregate.Geometry.SelectedPair (p.lines gate) U) (x : ↥U → Bool) : Aggregate.Geometry.key p U (glue U x fun (x : ↥Uᶜ) => false) gate = evalLiterals (lineLiterals (p.lines gate) U) x

The gate coordinates of the actual message agree with the selected literal sets.

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Joint.outputKeyWeightBoundOfLiterals {n g : ℕ} (p : Program Aggregate.Geometry.signature n g) (U : Finset (Fin n)) (out : Wire n g) (literalBound : Entropy.WeightBound (fun (x : ↥U → Bool) (i : { gate : Fin g // Aggregate.Geometry.SelectedPair (p.lines gate) U }) => evalLiterals (lineLiterals (p.lines ↑i) U) x) (↑(Fintype.card { gate : Fin g // Aggregate.Geometry.SelectedPair (p.lines gate) U }) * Entropy.Graph.edgeCost + ↑U.card * Entropy.Graph.vertexCost)) : Entropy.WeightBound (fun (x : ↥U → Bool) => Aggregate.Geometry.outputKey p U out (glue U x fun (x : ↥Uᶜ) => false)) ((↑g + 1) * Real.log 2 - ↑{gate : Fin g | Aggregate.Geometry.SelectedPair (p.lines gate) U}.card * (Real.binEntropy (1 / 4) - 1 / 2 * Real.log 2) + ↑U.card * (Real.binEntropy (1 / 4) - 3 / 4 * Real.log 2))

A joint certificate on the eligible conjunctions extends to the actual whole message.

Equations

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

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Joint.outputKeyWeightBound {n g : ℕ} (p : Program Aggregate.Geometry.signature n g) (U : Finset (Fin n)) (out : Wire n g) : Entropy.WeightBound (fun (x : ↥U → Bool) => Aggregate.Geometry.outputKey p U out (glue U x fun (x : ↥Uᶜ) => false)) ((↑g + 1) * Real.log 2 - ↑{gate : Fin g | Aggregate.Geometry.SelectedPair (p.lines gate) U}.card * (Real.binEntropy (1 / 4) - 1 / 2 * Real.log 2) + ↑U.card * (Real.binEntropy (1 / 4) - 3 / 4 * Real.log 2))

The actual one-way circuit message obeys the joint conjunction information bound.

Equations

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