Product counting inside conjunction majority events

A selected coordinate has at most two of the three allowed pair states. Selecting both coordinates leaves at most one state, so their combined cost also satisfies the product bound. Unused coordinates retain their two independent states.

def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.Internal.pairSelected (mask : Bool → Bool) : ℕ

The number of selected coordinates in one signed pair.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.Internal.pairSelected mask = (if mask false = true then 1 else 0) + if mask true = true then 1 else 0

@[reducible, inline]

abbrev Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.Internal.PairAllowed (a b : Bool) (mask bits x : Bool → Bool) : Prop

Local assignments satisfying a majority pair and any selected literals.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.Internal.PairAllowed a b mask bits x = ((x false == a && x true == b) = false ∧ ∀ (i : Bool), mask i = true → x i = bits i)

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.Internal.pair_count (a b : Bool) (mask bits : Bool → Bool) : 3 ^ pairSelected mask * Fintype.card { x : Bool → Bool // PairAllowed a b mask bits x } ≤ 2 ^ pairSelected mask * 3

The three-state pair obeys the two-thirds cylinder bound.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.Internal.free_count (mask bit : Bool) : (3 ^ if mask = true then 1 else 0) * Fintype.card { x : Bool // mask = true → x = bit } ≤ (2 ^ if mask = true then 1 else 0) * 2

A free Boolean coordinate also obeys the two-thirds cylinder bound.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.Internal.card_pi_constraints {I : Type u_1} [Fintype I] {X : I → Type u_2} [(i : I) → Fintype (X i)] (P : (i : I) → X i → Prop) [(i : I) → DecidablePred (P i)] : Fintype.card { x : (i : I) → X i // ∀ (i : I), P i (x i) } = ∏ i : I, Fintype.card { x : X i // P i x }

Cardinalities factor when all constraints are local to one product coordinate.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.Internal.product_count {I : Type u_1} [Fintype I] (k count : I → ℕ) (base : ℕ) (bound : ∀ (i : I), 3 ^ k i * count i ≤ 2 ^ k i * base) : (3 ^ ∑ i : I, k i) * ∏ i : I, count i ≤ (2 ^ ∑ i : I, k i) * base ^ Fintype.card I

Product estimates accumulate one exponent for each selected coordinate.

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.Internal.indexSplit {E : Type u_1} {V : Type u_2} (edge : E → Entropy.SignedEdge V) (disjoint : Function.Injective (endpoint edge)) : E × Bool ⊕ { v : V // v ∉ Set.range (endpoint edge) } ≃ V

Split every original coordinate into a pair endpoint or an unused coordinate.

Equations

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

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.Internal.selected_count {E : Type u_1} {V : Type u_2} [Fintype E] [Fintype V] (edge : E → Entropy.SignedEdge V) (disjoint : Function.Injective (endpoint edge)) (mask : V → Bool) : ((∑ e : E, pairSelected fun (b : Bool) => mask (endpoint edge (e, b))) + ∑ v : { v : V // v ∉ Set.range (endpoint edge) }, if mask ↑v = true then 1 else 0) = ∑ v : V, if mask v = true then 1 else 0

Selection counts add across all independent blocks.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.Internal.constrained_card {E : Type u_1} {V : Type u_2} [Fintype E] [Fintype V] (edge : E → Entropy.SignedEdge V) (disjoint : Function.Injective (endpoint edge)) (mask bits : V → Bool) : Fintype.card { x : V → Bool // (∀ (e : E), (edge e).eval x = false) ∧ ∀ (v : V), mask v = true → x v = bits v } = (∏ e : E, Fintype.card { x : Bool → Bool // PairAllowed (edge e).leftSign (edge e).rightSign (fun (b : Bool) => mask (endpoint edge (e, b))) (fun (b : Bool) => bits (endpoint edge (e, b))) x }) * ∏ v : { v : V // v ∉ Set.range (endpoint edge) }, Fintype.card { x : Bool // mask ↑v = true → x = bits ↑v }

Majority assignments with extra fixed literals factor into independent local counts.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.Internal.constrained_count {E : Type u_1} {V : Type u_2} [Fintype E] [Fintype V] (edge : E → Entropy.SignedEdge V) (disjoint : Function.Injective (endpoint edge)) (mask bits : V → Bool) : (3 ^ ∑ v : V, if mask v = true then 1 else 0) * Fintype.card { x : V → Bool // (∀ (e : E), (edge e).eval x = false) ∧ ∀ (v : V), mask v = true → x v = bits v } ≤ (2 ^ ∑ v : V, if mask v = true then 1 else 0) * (majorityInputs edge).card

The entire product obeys the two-thirds cost per selected coordinate.