Rectangle-cover fusion bounds

This file specializes finite-support coverage fusion to combinatorial rectangles. An allowed term is a Cartesian product contained in the target relation; addition takes unions of supports. Thus the resulting circuits are monotone sums of admissible product terms, equivalently exact rectangle covers.

A local upper bound on the size of an admissible rectangle gives a term-count lower bound. For the diagonal relation every admissible rectangle contains at most one pair, so an exact cover needs one charged term per diagonal entry.

structure Algebraic.Fusion.SumOfTerms.Rectangle.Term {L : Type u} {R : Type v} [DecidableEq L] [DecidableEq R] (target : Finset (L × R)) : Type (max u v)

A combinatorial rectangle whose whole support lies in the target relation.

• left : Finset L

  Left side of the rectangle.

• right : Finset R

  Right side of the rectangle.

• product_subset : self.left.product self.right ⊆ target

  Admissibility prevents a monotone term from producing an off-target monomial.

def Algebraic.Fusion.SumOfTerms.Rectangle.termSupport {L : Type u} {R : Type v} [DecidableEq L] [DecidableEq R] {target : Finset (L × R)} (term : Term target) : Coverage.FiniteSupport (L × R)

The finite monomial support contributed by one rectangle term.

Equations

• Algebraic.Fusion.SumOfTerms.Rectangle.termSupport term = { monomials := term.left.product term.right }

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Rectangle.termSupport_monomials {L : Type u} {R : Type v} [DecidableEq L] [DecidableEq R] {target : Finset (L × R)} (term : Term target) : (termSupport term).monomials = term.left.product term.right

structure Algebraic.Fusion.SumOfTerms.Rectangle.Bound {L : Type u} {R : Type v} [DecidableEq L] [DecidableEq R] (target : Finset (L × R)) : Type

A uniform size bound for admissible rectangles in a target relation.

• capacity : ℕ

  Maximum cardinality of one admissible rectangle.

• rectangle_card_le (term : Term target) : (term.left.product term.right).card ≤ self.capacity

  The local rectangle-size estimate.

theorem Algebraic.Fusion.SumOfTerms.Rectangle.coveredWitnesses_card_le_product {L : Type u} {R : Type v} [DecidableEq L] [DecidableEq R] {target : Finset (L × R)} (term : Term target) : (Coverage.coveredWitnesses target termSupport term).card ≤ (term.left.product term.right).card

The witnesses covered by a rectangle inject into its Cartesian-product support.

noncomputable def Algebraic.Fusion.SumOfTerms.Rectangle.Bound.coverageBound {L : Type u} {R : Type v} [DecidableEq L] [DecidableEq R] {target : Finset (L × R)} (bound : Bound target) : Coverage.Bound target termSupport

Rectangle-size bounds are finite-support coverage bounds.

Equations

• bound.coverageBound = { capacity := bound.capacity, covered_card_le := ⋯ }

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Rectangle.Bound.coverageBound_capacity {L : Type u} {R : Type v} [DecidableEq L] [DecidableEq R] {target : Finset (L × R)} (bound : Bound target) : bound.coverageBound.capacity = bound.capacity

theorem Algebraic.Fusion.SumOfTerms.Rectangle.Bound.circuit_lowerBound {L : Type u} {R : Type v} [DecidableEq L] [DecidableEq R] {target : Finset (L × R)} (bound : Bound target) (positive : 0 < bound.capacity) (circuit : Circuit (SumOfTerms.signature (Term target)) 0 1) (constructs : (Coverage.problem target).Constructs circuit (SumOfTerms.interpretation termSupport)) : target.card ⌈/⌉ bound.capacity ≤ circuit.cost SumOfTerms.termCost

Every exact monotone rectangle cover has the expected cardinality lower bound.

def Algebraic.Fusion.SumOfTerms.Rectangle.diagonalEmbedding (I : Type u) : I ↪ I × I

Embedding used to enumerate the diagonal relation without duplicates.

Equations

• Algebraic.Fusion.SumOfTerms.Rectangle.diagonalEmbedding I = { toFun := fun (index : I) => (index, index), inj' := ⋯ }

def Algebraic.Fusion.SumOfTerms.Rectangle.diagonal (I : Type u) [Fintype I] : Finset (I × I)

The finite diagonal relation on an index type.

Equations

• Algebraic.Fusion.SumOfTerms.Rectangle.diagonal I = Finset.map (Algebraic.Fusion.SumOfTerms.Rectangle.diagonalEmbedding I) Finset.univ

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Rectangle.card_diagonal (I : Type u) [Fintype I] : (diagonal I).card = Fintype.card I

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Rectangle.mem_diagonal {I : Type u} [Fintype I] (pair : I × I) : pair ∈ diagonal I ↔ pair.1 = pair.2

theorem Algebraic.Fusion.SumOfTerms.Rectangle.diagonal_rectangle_card_le_one {I : Type u} [Fintype I] [DecidableEq I] (term : Term (diagonal I)) : (term.left.product term.right).card ≤ 1

A rectangle contained in the diagonal has at most one pair.

noncomputable def Algebraic.Fusion.SumOfTerms.Rectangle.diagonalBound (I : Type u) [Fintype I] [DecidableEq I] : Bound (diagonal I)

Capacity-one certificate for the finite diagonal relation.

Equations

• Algebraic.Fusion.SumOfTerms.Rectangle.diagonalBound I = { capacity := 1, rectangle_card_le := ⋯ }

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Rectangle.diagonalBound_capacity (I : Type u) [Fintype I] [DecidableEq I] : (diagonalBound I).capacity = 1

theorem Algebraic.Fusion.SumOfTerms.Rectangle.diagonal_lowerBound {I : Type u} [Fintype I] [DecidableEq I] (circuit : Circuit (SumOfTerms.signature (Term (diagonal I))) 0 1) (constructs : (Coverage.problem (diagonal I)).Constructs circuit (SumOfTerms.interpretation termSupport)) : Fintype.card I ≤ circuit.cost SumOfTerms.termCost

An exact monotone sum of diagonal-contained product terms needs one term per diagonal monomial.