Counting bounded fusion failures

A fusion cover excludes every witness, but a single atom need not exclude only one witness. This file packages the general counting argument in which an atom of cost c can fail on at most capacity * c witnesses. Taking the union of all failure sets then gives a weighted cover lower bound.

This layer is useful when observations are indexed by derivative directions, rank increments, monomials, cuts, or thresholds. The semantic fusion model and the combinatorial estimate on one atom remain independent.

noncomputable def Algebraic.Fusion.Atom.failures {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} (atom : Atom σ U) (model : Model operationCost interpretation problem) [Fintype model.Witness] : Finset model.Witness

The finite set of witnesses on which an atom fails to preserve soundness.

Equations

• atom.failures model = {witness : model.Witness | ¬atom.PreservedBy model witness}

@[simp]

theorem Algebraic.Fusion.Atom.mem_failures {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} (atom : Atom σ U) (model : Model operationCost interpretation problem) [Fintype model.Witness] (witness : model.Witness) : witness ∈ atom.failures model ↔ ¬atom.PreservedBy model witness

noncomputable def Algebraic.Fusion.Model.failureUnion {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} (model : Model operationCost interpretation problem) [Fintype model.Witness] (atoms : List (Atom σ U)) : Finset model.Witness

All witnesses excluded by at least one atom in a list.

Equations

• model.failureUnion atoms = List.foldr (fun (atom : Algebraic.Fusion.Atom σ U) (failures : Finset model.Witness) => atom.failures model ∪ failures) ∅ atoms

@[simp]

theorem Algebraic.Fusion.Model.failureUnion_nil {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} (model : Model operationCost interpretation problem) [Fintype model.Witness] : model.failureUnion [] = ∅

@[simp]

theorem Algebraic.Fusion.Model.failureUnion_cons {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} (model : Model operationCost interpretation problem) [Fintype model.Witness] [DecidableEq model.Witness] (atom : Atom σ U) (atoms : List (Atom σ U)) : model.failureUnion (atom :: atoms) = atom.failures model ∪ model.failureUnion atoms

theorem Algebraic.Fusion.Model.mem_failureUnion_iff {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} (model : Model operationCost interpretation problem) [Fintype model.Witness] (atoms : List (Atom σ U)) (witness : model.Witness) : witness ∈ model.failureUnion atoms ↔ ∃ atom ∈ atoms, ¬atom.PreservedBy model witness

Membership in the failure union is the expected existential statement.

theorem Algebraic.Fusion.Model.failureUnion_card_le_sum {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} (model : Model operationCost interpretation problem) [Fintype model.Witness] (atoms : List (Atom σ U)) : (model.failureUnion atoms).card ≤ (List.map (fun (atom : Atom σ U) => (atom.failures model).card) atoms).sum

The failure union has cardinality at most the sum of failure cardinalities.

theorem Algebraic.Fusion.Cover.witnessCard_le_sum_failures {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} {model : Model operationCost interpretation problem} [Fintype model.Witness] (cover : Cover model) : Fintype.card model.Witness ≤ (List.map (fun (atom : Atom σ U) => (atom.failures model).card) cover.atoms).sum

Every cover has enough total failure capacity to account for all witnesses.

theorem Algebraic.Fusion.Cover.witnessCard_le_mul_cost_of_local {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} {model : Model operationCost interpretation problem} [Fintype model.Witness] (cover : Cover model) (capacity : ℕ) (localBound : ∀ atom ∈ cover.atoms, (atom.failures model).card ≤ capacity * atom.cost operationCost) : Fintype.card model.Witness ≤ capacity * cover.cost

A failure estimate only for the atoms in one cover suffices for the counting argument. This circuit-local form is useful for restricted models whose width, degree, homogeneity, or liveness promise need not hold for every semantic atom of the ambient interpretation.

theorem Algebraic.Fusion.Cover.ceilDiv_witnessCard_le_cost_of_local {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} {model : Model operationCost interpretation problem} [Fintype model.Witness] (cover : Cover model) (capacity : ℕ) (positive : 0 < capacity) (localBound : ∀ atom ∈ cover.atoms, (atom.failures model).card ≤ capacity * atom.cost operationCost) : Fintype.card model.Witness ⌈/⌉ capacity ≤ cover.cost

Divide a circuit-local failure estimate by a positive capacity.

theorem Algebraic.Fusion.Model.ceilDiv_witnessCard_le_circuitCost_of_local {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} (model : Model operationCost interpretation problem) [Fintype model.Witness] (capacity : ℕ) (positive : 0 < capacity) (circuit : Circuit σ problem.inputCount 1) (constructs : problem.Constructs circuit interpretation) (localBound : ∀ atom ∈ circuitAtoms circuit interpretation problem.inputs, (atom.failures model).card ≤ capacity * atom.cost operationCost) : Fintype.card model.Witness ⌈/⌉ capacity ≤ circuit.cost operationCost

A bounded-failure estimate on the semantic atoms extracted from one constructing circuit transfers directly to its operation cost.

structure Algebraic.Fusion.FailureBound {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} (model : Model operationCost interpretation problem) [Fintype model.Witness] : Type

A reusable certificate that each atom destroys only boundedly many witnesses per unit of operation cost.

• capacity : ℕ

  Maximum number of failed witnesses per unit of gate cost.

• failure_card_le (atom : Atom σ U) : (atom.failures model).card ≤ self.capacity * atom.cost operationCost

  The local failure estimate for every possible semantic gate atom.

theorem Algebraic.Fusion.FailureBound.witnessCard_le_mul_coverCost {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} {model : Model operationCost interpretation problem} [Fintype model.Witness] (bound : FailureBound model) (cover : Cover model) : Fintype.card model.Witness ≤ bound.capacity * cover.cost

A bounded-failure certificate gives a weighted lower bound for every cover.

theorem Algebraic.Fusion.FailureBound.ceilDiv_witnessCard_le_coverCost {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} {model : Model operationCost interpretation problem} [Fintype model.Witness] (bound : FailureBound model) (positive : 0 < bound.capacity) (cover : Cover model) : Fintype.card model.Witness ⌈/⌉ bound.capacity ≤ cover.cost

Dividing the witness count by a positive capacity lower-bounds cover cost.

noncomputable def Algebraic.Fusion.FailureBound.framework {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} {model : Model operationCost interpretation problem} [Fintype model.Witness] (bound : FailureBound model) (positive : 0 < bound.capacity) : Framework model

A positive bounded-failure certificate packages into the core framework.

Equations

• bound.framework positive = { bound := Fintype.card model.Witness ⌈/⌉ bound.capacity, coverLowerBound := ⋯ }

theorem Algebraic.Fusion.FailureBound.ceilDiv_witnessCard_le_circuitCost {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} {model : Model operationCost interpretation problem} [Fintype model.Witness] (bound : FailureBound model) (positive : 0 < bound.capacity) (circuit : Circuit σ problem.inputCount 1) (constructs : problem.Constructs circuit interpretation) : Fintype.card model.Witness ⌈/⌉ bound.capacity ≤ circuit.cost operationCost

The counting bound transferred directly to constructing circuits.