A five-element chain m-semiring where ⊗ does not distribute over ⊖

This file defines ChainFive, a commutative m-semiring on the five-element chain 𝟘 < lo < mid < hi < 𝟙 with ⊕ = max, the chain monus (a ⊖ b = 𝟘 if a ≤ b, else a), and the commutative multiplication determined by

• hi ⊗ hi = hi,
• hi ⊗ mid = hi ⊗ lo = lo,
• every other product of elements strictly between 𝟘 and 𝟙 is 𝟘.

ChainFive is absorptive (hence idempotent) but does not satisfy mul_sub_left_distributive: hi ⊗ (𝟙 ⊖ hi) = hi while hi ⊗ 𝟙 ⊖ hi ⊗ hi = 𝟘.

Why this semiring exists

Its purpose is to show that the mul_sub_left_distributive hypothesis of Having.world_bound – and hence of Having.G_eq_S_monus_S and Having.atMost_eq_S_monus_S, which rest on it – is genuinely needed and cannot be weakened away as it can for Having.F_eq_S (which needs only absorptivity, via Having.upward_closed_collapse).

The witness is the family α = (mid, hi, hi) on a three-element universe U, with W = {0} and C = 1:

• the exactly-W annotation is T_U(W) = mid ⊖ (mid⊗hi ⊕ mid⊗hi) = mid ⊖ lo = mid, but
• S_1(U) ⊖ S_2(U) = (mid ⊕ hi ⊕ hi) ⊖ (lo ⊕ lo ⊕ hi) = hi ⊖ hi = 𝟘,

so the bound T_U(W) ≤ S_1(U) ⊖ S_2(U) of Having.world_bound fails (ChainFive.not_world_bound), and with it the HAVING count = 1 identity G_1(U) = S_1(U) ⊖ S_2(U) (ChainFive.G_ne_S_monus_S) and the HAVING count ≤ 1 identity (ChainFive.atMost_ne_S_monus_S).

Intuitively, in the factored form T_U(W) = A_W ⊗ (𝟙 ⊖ E_W) the failure disappears: 𝟙 ⊖ E_W = 𝟙 ⊖ hi = 𝟙 and mid ⊗ 𝟙 = mid, but the world of size 2 extending W by one hi-occurrence has annotation lo, which the chain monus of the unfactored form A_W ⊖ ⊕_x A_{W∪{x}} fails to cancel against mid. The two forms of the world annotation coincide exactly when ⊗ distributes over ⊖; ChainFive is where they part company.

All proofs are by decide: the carrier is a five-element enumeration with derived decidable equality and order.

inductive ChainFive : Type

The five-element chain 𝟘 < lo < mid < hi < 𝟙 (constructor order is the chain order), carrying the m-semiring structure described in the module docstring.

• zero : ChainFive
• lo : ChainFive
• mid : ChainFive
• hi : ChainFive
• one : ChainFive

@[instance_reducible]

instance instDecidableEqChainFive : DecidableEq ChainFive

Equations

• instDecidableEqChainFive x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance instReprChainFive : Repr ChainFive

Equations

• instReprChainFive = { reprPrec := instReprChainFive.repr }

def instReprChainFive.repr : ChainFive → ℕ → Std.Format

Equations

• instReprChainFive.repr ChainFive.zero prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ChainFive.zero")).group prec✝
• instReprChainFive.repr ChainFive.lo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ChainFive.lo")).group prec✝
• instReprChainFive.repr ChainFive.mid prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ChainFive.mid")).group prec✝
• instReprChainFive.repr ChainFive.hi prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ChainFive.hi")).group prec✝
• instReprChainFive.repr ChainFive.one prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ChainFive.one")).group prec✝

@[instance_reducible]

instance instOrdChainFive : Ord ChainFive

Equations

• instOrdChainFive = { compare := instOrdChainFive.ord }

def instOrdChainFive.ord : ChainFive → ChainFive → Ordering

Equations

• instOrdChainFive.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

@[instance_reducible]

instance instFintypeChainFive : Fintype ChainFive

Equations

• instFintypeChainFive = { elems := { val := ↑ChainFive.enumList, nodup := ChainFive.enumList_nodup }, complete := instFintypeChainFive._proof_1 }

@[instance_reducible]

instance ChainFive.instLE : LE ChainFive

Equations

• ChainFive.instLE = { le := fun (a b : ChainFive) => (compare a b).isLE = true }

@[instance_reducible]

instance ChainFive.instLinearOrder : LinearOrder ChainFive

Equations

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

@[instance_reducible]

instance ChainFive.instZero : Zero ChainFive

Equations

• ChainFive.instZero = { zero := ChainFive.zero }

@[instance_reducible]

instance ChainFive.instOne : One ChainFive

Equations

• ChainFive.instOne = { one := ChainFive.one }

@[instance_reducible]

instance ChainFive.instAdd : Add ChainFive

Addition is max (the chain join).

Equations

• ChainFive.instAdd = { add := fun (a b : ChainFive) => max a b }

@[instance_reducible]

instance ChainFive.instMul : Mul ChainFive

The commutative multiplication: 𝟙 is neutral, 𝟘 absorbing, hi ⊗ hi = hi, hi ⊗ mid = hi ⊗ lo = lo, and all other products of non-unit elements are 𝟘.

Equations

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

@[instance_reducible]

instance ChainFive.instSub : Sub ChainFive

The chain monus: a ⊖ b = 𝟘 if a ≤ b, and a otherwise.

Equations

• ChainFive.instSub = { sub := fun (a b : ChainFive) => if a ≤ b then ChainFive.zero else a }

@[instance_reducible]

instance ChainFive.instCommSemiring : CommSemiring ChainFive

Equations

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

@[instance_reducible]

instance ChainFive.instSemiringWithMonus : SemiringWithMonus ChainFive

Equations

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

theorem ChainFive.not_isDelta_id : ¬IsDelta id

On ChainFive the identity is not an admissible δ, even though the semiring is absorptive (ChainFive.absorptive): what delta_absorb asks of δ := id is the lattice law a ⊗ (a ⊕ b) = a, and mid ⊗ (mid ⊕ mid) = mid ⊗ mid = 𝟘 ≠ mid.

@[instance_reducible]

instance ChainFive.instCommSemiringWithMonus : CommSemiringWithMonus ChainFive

Equations

• ChainFive.instCommSemiringWithMonus = { toSemiringWithMonus := ChainFive.instSemiringWithMonus, mul_comm := ChainFive.instCommSemiringWithMonus._proof_1 }

@[instance_reducible]

instance ChainFive.instHasAltLinearOrder : HasAltLinearOrder ChainFive

Equations

• ChainFive.instHasAltLinearOrder = { altOrder := inferInstance }

theorem ChainFive.absorptive : _root_.absorptive ChainFive

theorem ChainFive.idempotent : _root_.idempotent ChainFive

theorem ChainFive.not_mul_sub_left_distributive : ¬mul_sub_left_distributive ChainFive

ChainFive does not satisfy left-distributivity of ⊗ over ⊖: hi ⊗ (𝟙 ⊖ hi) = hi ⊗ 𝟙 = hi, while hi ⊗ 𝟙 ⊖ hi ⊗ hi = hi ⊖ hi = 𝟘.

def ChainFive.alphaCE : Fin 3 → ChainFive

The witness family α = (mid, hi, hi) on a three-element universe.

Equations

• ChainFive.alphaCE i = if ↑i = 0 then ChainFive.mid else ChainFive.hi

theorem ChainFive.not_world_bound : ¬∀ (α : Fin 3 → ChainFive) (U W : Finset (Fin 3)), W ⊆ U → ∀ (j C : ℕ), j ≤ W.card → W.card ≤ C → Having.T α U W ≤ Having.S α U j - Having.S α U (C + 1)

Having.world_bound fails without mul_sub_left_distributive. In the absorptive m-semiring ChainFive, the per-world upper bound T_U(W) ≤ S_j(U) ⊖ S_{C+1}(U) (for j ≤ |W| ≤ C) does not hold: with α = (mid, hi, hi), W = {0} and j = C = 1, the left-hand side is mid and the right-hand side is 𝟘. Together with ChainFive.not_mul_sub_left_distributive and ChainFive.absorptive, this shows the distributivity hypothesis of Having.world_bound is essential, in contrast with Having.F_eq_S where it can be dropped.

theorem ChainFive.G_ne_S_monus_S : Having.G alphaCE Finset.univ 1 ≠ Having.S alphaCE Finset.univ 1 - Having.S alphaCE Finset.univ 2

Having.G_eq_S_monus_S fails without mul_sub_left_distributive. The HAVING count = 1 identity G_1(U) = S_1(U) ⊖ S_2(U) does not hold in ChainFive for α = (mid, hi, hi): the left-hand side is mid, the right-hand side 𝟘.

theorem ChainFive.atMost_ne_S_monus_S : ∑ W ∈ Finset.univ.powerset with 1 ≤ W.card ∧ W.card ≤ 1, Having.T alphaCE Finset.univ W ≠ Having.S alphaCE Finset.univ 1 - Having.S alphaCE Finset.univ 2

Having.atMost_eq_S_monus_S fails without mul_sub_left_distributive. The HAVING count ≤ 1 identity does not hold in ChainFive for α = (mid, hi, hi): the left-hand side is mid, the right-hand side 𝟘.

Home · Documentation · Publications · Contributors · Source · Cite