Mixed message weights with constant coordinates omitted

Narrow and wide primary conjunctions receive their separate costs. Designated conjunction outputs of a nonliteral permutation are constant message coordinates and contribute no cost, including in the joint support-graph estimate.

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.keyWeightBoundOfClasses {X : Type u_1} [Fintype X] {g : ℕ} (message : X → Fin g → Bool) (T W O : Finset (Fin g)) (disjoint : Disjoint T W) (outputs : Disjoint (T ∪ W) O) (constant : ∀ i ∈ O, ∀ (x : X), message x i = true) {cost : ℝ} (classes : Entropy.WeightBound (fun (x : X) => (fun (i : ↥T) => message x ↑i, fun (i : ↥W) => message x ↑i)) cost) : Entropy.WeightBound message (cost + (↑g - ↑T.card - ↑W.card - ↑O.card) * Real.log 2)

Reconstruct a message from two weighted classes and the remaining nonconstant bits.

Equations

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

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.keyQuarterWeightBound {n g : ℕ} (p : Program Aggregate.Geometry.signature n g) (U : Finset (Fin n)) (i : Fin g) (pair : Aggregate.Geometry.SelectedPair (p.lines i) U) : Entropy.WeightBound (fun (x : ↥U → Bool) => Aggregate.Geometry.key p U (glue U x fun (x : ↥Uᶜ) => false) i) (Real.binEntropy (1 / 4))

A selected pair supplies the marginal quarter-entropy certificate.

Equations

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

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.retainedClassesWeightBound {n g : ℕ} (p : Program Aggregate.Geometry.signature n g) (U : Finset (Fin n)) (graph : Bool) : Entropy.WeightBound (fun (x : ↥U → Bool) => (fun (i : ↥(Joint.retainedTwo p U)) => Aggregate.Geometry.key p U (glue U x fun (x : ↥Uᶜ) => false) ↑i, fun (i : ↥(Joint.retainedWide p U)) => Aggregate.Geometry.key p U (glue U x fun (x : ↥Uᶜ) => false) ↑i)) (((↑(Joint.retainedTwo p U).card * if graph = true then Entropy.Graph.edgeCost else Real.binEntropy (1 / 4)) + if graph = true then ↑U.card * Entropy.Graph.vertexCost else 0) + ↑(Joint.retainedWide p U).card * Real.binEntropy (1 / 8))

Actual retained classes have either marginal or joint support-graph weights.

Equations

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

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.retainedKeyWeightBound {n g : ℕ} (p : Program Aggregate.Geometry.signature n g) (U : Finset (Fin n)) (O : Finset (Fin g)) (outside : Disjoint (Joint.retainedTwo p U ∪ Joint.retainedWide p U) O) (constant : ∀ i ∈ O, ∀ (x : ↥U → Bool), Aggregate.Geometry.key p U (glue U x fun (x : ↥Uᶜ) => false) i = true) (graph : Bool) : Entropy.WeightBound (fun (x : ↥U → Bool) => Aggregate.Geometry.key p U (glue U x fun (x : ↥Uᶜ) => false)) (((↑g - ↑O.card) * Real.log 2 - ↑(Joint.retainedTwo p U).card * if graph = true then Real.binEntropy (1 / 4) - 1 / 2 * Real.log 2 else Real.log 2 - Real.binEntropy (1 / 4)) - ↑(Joint.retainedWide p U).card * (Real.log 2 - Real.binEntropy (1 / 8)) + if graph = true then ↑U.card * Entropy.Graph.vertexCost else 0)

Full messages omit any known constant coordinates outside the retained classes.

Equations

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

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.marginalOutputKeyWeightBound {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 - ↑(Joint.retainedTwo p U).card * (Real.log 2 - Real.binEntropy (1 / 4)) - ↑(Joint.retainedWide p U).card * (Real.log 2 - Real.binEntropy (1 / 8)))

Adding the one designated-output bit preserves the marginal mixed savings.

Equations

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

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.sender_le_size_of_marginal_messages {n K : ℕ} (c : Circuit Aggregate.Geometry.signature n 1) (hK : 0 < K) (free : RectangleFree (c.outputFunction Aggregate.Geometry.interpretation 0) K) (freeNot : RectangleFree (fun (x : Cslib.BitString n) => !c.outputFunction Aggregate.Geometry.interpretation 0 x) K) (U : Finset (Fin n)) (large : 2 * K ≤ 2 ^ Uᶜ.card) : ↑U.card ≤ ↑c.size + 1 + Real.logb 2 ↑K - Entropy.bitSaving * ↑(Joint.retainedTwo c.program U).card - Shared.wideSaving * ↑(Joint.retainedWide c.program U).card

Separate quarter and eighth costs bound any rectangle-free sending side.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.input_le_size_of_triple_marginal {n a K : ℕ} (c : Circuit Aggregate.Geometry.signature n 1) (ha : 3 ≤ a) (han : a ≤ n) (hK : 0 < K) (free : RectangleFree (c.outputFunction Aggregate.Geometry.interpretation 0) K) (freeNot : RectangleFree (fun (x : Cslib.BitString n) => !c.outputFunction Aggregate.Geometry.interpretation 0 x) K) (large : 2 * K ≤ 2 ^ (n - a)) : ↑a ≤ ↑c.size + 1 + Real.logb 2 ↑K - Joint.tripleRetention n a * (Entropy.bitSaving * ↑(Aggregate.Geometry.Shared.exactTwo c.program).card + Shared.wideSaving * ↑(Joint.retainedWide c.program Finset.univ).card)

Weighted triple retention applies to the marginal narrow and wide costs.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.retainedTwo_univ {n g : ℕ} (p : Program Aggregate.Geometry.signature n g) : Joint.retainedTwo p Finset.univ = Aggregate.Geometry.Shared.exactTwo p

Full-primary retained pairs are exactly the original exact-two gate class.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.permutation_input_le_message_cost {n : ℕ} (c : Circuit Aggregate.Geometry.signature n n) (bijective : Function.Bijective (c.eval Aggregate.Geometry.interpretation)) (nonliteral : ∀ (i j : Fin n) (b : Bool), c.outputFunction Aggregate.Geometry.interpretation i ≠ fun (x : Fin n → Bool) => b ^^ x j) (graph : Bool) : (1 - if graph = true then Joint.overlapPenalty else 0) * ↑n ≤ ↑c.size - ↑(Aggregate.Geometry.outputConjunctionCount c) - (if graph = true then Joint.gateSaving else Entropy.bitSaving) * ↑(Aggregate.Geometry.Shared.exactTwo c.program).card - Shared.wideSaving * ↑(Joint.retainedWide c.program Finset.univ).card

Both mixed entropy bounds omit the constant conjunction-output coordinates.