A cut retaining weighted original gate classes #
Pad each original two-primary support to a triple and choose a triple inside each original wide support. Weighted averaging over fixed-size cuts then preserves the same exact triple-retention fraction of the two different information savings.
theorem
Algebraic.Cutwidth.Aggregate.Geometry.Joint.retainedWide_univ_iff
{n g : ℕ}
(line : Line Aggregate.Geometry.signature n g)
:
RetainedWide line Finset.univ ↔ Aggregate.Geometry.Op.isConjunction line.op = true ∧ 3 ≤ (Aggregate.Geometry.primaryInputs line).card
On the full input set, wide retention is the original three-primary gate predicate.
theorem
Algebraic.Cutwidth.Aggregate.Geometry.Joint.exactTwo_add_retainedWide_univ
{n g : ℕ}
(p : Program Aggregate.Geometry.signature n g)
:
Original exact-two and wide conjunction gates partition the multiple-primary count.
theorem
Algebraic.Cutwidth.Aggregate.Geometry.Joint.exists_subset_retained_weight
{n g a : ℕ}
(p : Program Aggregate.Geometry.signature n g)
(ha : 3 ≤ a)
(han : a ≤ n)
(rho r : ℝ)
(hrho : 0 ≤ rho)
(hr : 0 ≤ r)
:
∃ (U : Finset (Fin n)),
U.card = a ∧ tripleRetention n a * (rho * ↑(Aggregate.Geometry.Shared.exactTwo p).card + r * ↑(retainedWide p Finset.univ).card) ≤ rho * ↑(retainedTwo p U).card + r * ↑(retainedWide p U).card
One actual cut retains a common triple fraction of both weighted gate classes.