Coverage fusion for finite monomial supports

This is the support-theoretic counterpart of the rank certificate. Semantic values are finite sets of monomials, addition is union, and a charged term contributes a prescribed finite support. A witness is one monomial in the target support. Union preserves non-membership, while a term fails precisely on the target monomials it covers.

If every allowed term covers at most r target monomials, every circuit whose union is the target uses at least ceil(target.card / r) charged terms. The local coverage estimate can come from separated monomials, rectangle bounds, or other monotone-support arguments.

@[reducible, inline]

abbrev Algebraic.Fusion.SumOfTerms.Coverage.FiniteSupport (M : Type u) : Type u

Compatibility name for the reusable finite-support carrier.

Equations

• Algebraic.Fusion.SumOfTerms.Coverage.FiniteSupport M = Algebraic.FiniteSupport M

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Coverage.monomials_add {M : Type u_1} [DecidableEq M] (left right : FiniteSupport M) : (left + right).monomials = left.monomials ∪ right.monomials

theorem Algebraic.Fusion.SumOfTerms.Coverage.mem_add {M : Type u_1} [DecidableEq M] (monomial : M) (left right : FiniteSupport M) : monomial ∈ (left + right).monomials ↔ monomial ∈ left.monomials ∨ monomial ∈ right.monomials

@[reducible, inline]

abbrev Algebraic.Fusion.SumOfTerms.Coverage.problem {M : Type u_1} (target : Finset M) : Problem (FiniteSupport M)

Construct a target support from charged terms, with no free inputs.

Equations

• Algebraic.Fusion.SumOfTerms.Coverage.problem target = { inputCount := 0, inputs := fun (input : Fin 0) => input.elim0, target := { monomials := target } }

@[reducible, inline]

abbrev Algebraic.Fusion.SumOfTerms.Coverage.model {M : Type u_1} {T : Type u_2} [DecidableEq M] (target : Finset M) (termSupport : T → FiniteSupport M) : Model SumOfTerms.termCost (SumOfTerms.interpretation termSupport) (problem target)

Fusion model whose observations say that a target monomial remains uncovered.

Equations

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

@[instance_reducible]

noncomputable instance Algebraic.Fusion.SumOfTerms.Coverage.witnessFintype {M : Type u_1} {T : Type u_2} [DecidableEq M] (target : Finset M) (termSupport : T → FiniteSupport M) : Fintype (model target termSupport).Witness

Equations

• Algebraic.Fusion.SumOfTerms.Coverage.witnessFintype target termSupport = id inferInstance

theorem Algebraic.Fusion.SumOfTerms.Coverage.witness_card {M : Type u_1} {T : Type u_2} [DecidableEq M] (target : Finset M) (termSupport : T → FiniteSupport M) : Fintype.card (model target termSupport).Witness = target.card

theorem Algebraic.Fusion.SumOfTerms.Coverage.add_preserved {M : Type u_1} {T : Type u_2} [DecidableEq M] (target : Finset M) (termSupport : T → FiniteSupport M) (arguments : Fin 2 → FiniteSupport M) (witness : (model target termSupport).Witness) : { op := SumOfTerms.Op.add, arguments := arguments }.PreservedBy (model target termSupport) witness

Union preserves non-membership of every target monomial.

theorem Algebraic.Fusion.SumOfTerms.Coverage.term_preserved_iff {M : Type u_1} {T : Type u_2} [DecidableEq M] (target : Finset M) (termSupport : T → FiniteSupport M) (term : T) (arguments : Fin (SumOfTerms.arity (SumOfTerms.Op.term term)) → FiniteSupport M) (witness : (model target termSupport).Witness) : { op := SumOfTerms.Op.term term, arguments := arguments }.PreservedBy (model target termSupport) witness ↔ ↑witness ∉ (termSupport term).monomials

A term preserves a witness exactly when it does not cover that monomial.

noncomputable def Algebraic.Fusion.SumOfTerms.Coverage.coveredWitnesses {M : Type u_1} {T : Sort u_2} [DecidableEq M] (target : Finset M) (termSupport : T → FiniteSupport M) (term : T) : Finset ↥target

Target witnesses covered by one dictionary term.

Equations

• Algebraic.Fusion.SumOfTerms.Coverage.coveredWitnesses target termSupport term = {witness ∈ target.attach | ↑witness ∈ (termSupport term).monomials}

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Coverage.mem_coveredWitnesses {M : Type u_1} {T : Sort u_2} [DecidableEq M] (target : Finset M) (termSupport : T → FiniteSupport M) (term : T) (witness : ↥target) : witness ∈ coveredWitnesses target termSupport term ↔ ↑witness ∈ (termSupport term).monomials

structure Algebraic.Fusion.SumOfTerms.Coverage.Bound {M : Type u_1} {T : Sort u_2} [DecidableEq M] (target : Finset M) (termSupport : T → FiniteSupport M) : Type

A local bound on how many target monomials one term can cover.

• capacity : ℕ

  Maximum target coverage of one term.

• covered_card_le (term : T) : (coveredWitnesses target termSupport term).card ≤ self.capacity

  The combinatorial coverage estimate for every allowed term.

noncomputable def Algebraic.Fusion.SumOfTerms.Coverage.Bound.failureBound {M : Type u_1} {T : Type u_2} [DecidableEq M] {target : Finset M} {termSupport : T → FiniteSupport M} (bound : Bound target termSupport) : FailureBound (model target termSupport)

Coverage bounds compile to the generic finite-witness failure bound.

Equations

• bound.failureBound = { capacity := bound.capacity, failure_card_le := ⋯ }

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Coverage.Bound.failureBound_capacity {M : Type u_1} {T : Type u_2} [DecidableEq M] {target : Finset M} {termSupport : T → FiniteSupport M} (bound : Bound target termSupport) : bound.failureBound.capacity = bound.capacity

theorem Algebraic.Fusion.SumOfTerms.Coverage.Bound.circuit_lowerBound {M : Type u_1} {T : Type u_2} [DecidableEq M] {target : Finset M} {termSupport : T → FiniteSupport M} (bound : Bound target termSupport) (positive : 0 < bound.capacity) (circuit : Circuit (SumOfTerms.signature T) 0 1) (constructs : (problem target).Constructs circuit (SumOfTerms.interpretation termSupport)) : target.card ⌈/⌉ bound.capacity ≤ circuit.cost SumOfTerms.termCost

A positive coverage capacity gives the expected circuit lower bound.

theorem Algebraic.Fusion.SumOfTerms.Coverage.circuit_lowerBound_of_separated {M : Type u_1} {T : Type u_2} [DecidableEq M] {target : Finset M} {termSupport : T → FiniteSupport M} (separated : ∀ (term : T), (coveredWitnesses target termSupport term).card ≤ 1) (circuit : Circuit (SumOfTerms.signature T) 0 1) (constructs : (problem target).Constructs circuit (SumOfTerms.interpretation termSupport)) : target.card ≤ circuit.cost SumOfTerms.termCost

The separated case: each term covers at most one target monomial.