A twelve-element atomistic lattice answers Question 7.4

Abstract

A finite lattice separates weak and strong coset-likeness.

Definition 1.1 (The join-irreducible set).

$$\forall L\in \mathrm{Type},[\mathrm{Lattice}\left(L\right)][\mathrm{BoundedOrder}\left(L\right)][\mathrm{Fintype}\left(L\right)],J\left(L\right)=\mathrm{Finset}.\mathrm{filter}\left(SupIrred,(\mathrm{Finset}.\mathrm{univ}:\mathrm{Finset}\left(L\right))\right)$$

Formalization. D5/S3/Combinatorics/Lattices/ShalaCosetLikeAtomisticLattice.J (✓ std3).

Citation. Besfort Shala (2024). The Probabilistic Zeta Function of a Finite Lattice. URL: https://arxiv.org/abs/2112.13766v6.

Commentary.

For a finite bounded lattice L, J is the finite set of elements satisfying Mathlib’s SupIrred predicate.

Definition 1.2 (Join-irreducibles below an element).

$$\forall L\in \mathrm{Type},[\mathrm{Lattice}\left(L\right)][\mathrm{BoundedOrder}\left(L\right)][\mathrm{Fintype}\left(L\right)][\mathrm{DecidableLE}\left(L\right)],\forall x\in L,\mathrm{Jx}\left(x\right)=\mathrm{Finset}.\mathrm{filter}\left(\lambda (j:L)\mapsto (j\le x),J\left(L\right)\right)$$

Formalization. D5/S3/Combinatorics/Lattices/ShalaCosetLikeAtomisticLattice.Jx (✓ std3).

Citation. Besfort Shala (2024). The Probabilistic Zeta Function of a Finite Lattice. URL: https://arxiv.org/abs/2112.13766v6.

Commentary.

Jx x filters J by the order relation j ≤ x.

Definition 1.3 (The atom-index ratio).

$$\forall L\in \mathrm{Type},[\mathrm{Lattice}\left(L\right)][\mathrm{BoundedOrder}\left(L\right)][\mathrm{Fintype}\left(L\right)][\mathrm{DecidableLE}\left(L\right)],\forall x\in L,\mathrm{index}\left(x\right)=\frac{(\mathrm{Finset}.\mathrm{card}\left(J\left(L\right)\right):\mathbb{Q})}{(\mathrm{Finset}.\mathrm{card}\left(\mathrm{Jx}\left(x\right)\right):\mathbb{Q})}$$

Formalization. D5/S3/Combinatorics/Lattices/ShalaCosetLikeAtomisticLattice.index (✓ std3).

Citation. Besfort Shala (2024). The Probabilistic Zeta Function of a Finite Lattice. URL: https://arxiv.org/abs/2112.13766v6.

Commentary.

index x is the rational ratio of the cardinality of J to the cardinality of Jx x.

Definition 1.4 (The probabilistic zeta function).

$$\forall L\in \mathrm{Type},[\mathrm{Lattice}\left(L\right)][\mathrm{BoundedOrder}\left(L\right)][\mathrm{Fintype}\left(L\right)][\mathrm{DecidableEq}\left(L\right)][\mathrm{DecidableLE}\left(L\right)][\mathrm{LocallyFiniteOrder}\left(L\right)],\forall s\in \mathbb{C},P\left(s\right)=\mathrm{Finset}.\mathrm{sum}\left(\mathrm{Finset}.\mathrm{erase}\left((\mathrm{Finset}.\mathrm{univ}:\mathrm{Finset}\left(L\right)),(\mathrm{Bot}.\mathrm{bot}:L)\right),\lambda (x:L)\mapsto ((\mathrm{IncidenceAlgebra}.\mathrm{mu}\left(\mathbb{Z},x,(\mathrm{Top}.\mathrm{top}:L)\right):\mathbb{C})\cdot (((\mathrm{index}\left(x\right):\mathbb{Q}):\mathbb{C}){)}^{-(s)})\right)$$

Formalization. D5/S3/Combinatorics/Lattices/ShalaCosetLikeAtomisticLattice.P (✓ std3).

Citation. Besfort Shala (2024). The Probabilistic Zeta Function of a Finite Lattice. URL: https://arxiv.org/abs/2112.13766v6.

Commentary.

P L s sums the upper-interval Möbius coefficients over all elements except bottom, weighted by the complex power of the rational index.

Definition 1.5 (Strong coset-likeness).

$$\forall L\in \mathrm{Type},[\mathrm{Lattice}\left(L\right)][\mathrm{BoundedOrder}\left(L\right)][\mathrm{Fintype}\left(L\right)][\mathrm{DecidableLE}\left(L\right)],\mathrm{StronglyCosetLike}\left(L\right)=(\forall x\in L,x\ne (\mathrm{Bot}.\mathrm{bot}:L)\Rightarrow (\mathrm{Finset}.\mathrm{card}\left(\mathrm{Jx}\left(x\right)\right)\mid \mathrm{Finset}.\mathrm{card}\left(J\left(L\right)\right)))$$

Formalization. D5/S3/Combinatorics/Lattices/ShalaCosetLikeAtomisticLattice.StronglyCosetLike (✓ std3).

Citation. Besfort Shala (2024). The Probabilistic Zeta Function of a Finite Lattice. URL: https://arxiv.org/abs/2112.13766v6.

Commentary.

Strong coset-likeness requires the cardinality of Jx x to divide the cardinality of J for every non-bottom element.

Definition 1.6 (Weak coset-likeness).

$$\forall L\in \mathrm{Type},[\mathrm{Lattice}\left(L\right)][\mathrm{BoundedOrder}\left(L\right)][\mathrm{Fintype}\left(L\right)][\mathrm{DecidableEq}\left(L\right)][\mathrm{DecidableLE}\left(L\right)][\mathrm{LocallyFiniteOrder}\left(L\right)],\mathrm{WeaklyCosetLike}\left(L\right)=(\exists N\in \mathbb{N},\exists a\in \mathbb{N}\to \mathbb{Z},\forall s\in \mathbb{C},P\left(s\right)=\mathrm{Finset}.\mathrm{sum}\left(\mathrm{Finset}.\mathrm{Icc}\left(1,N\right),\lambda (n:\mathbb{N})\mapsto ((a\left(n\right):\mathbb{C})\cdot ((n:\mathbb{C}){)}^{-(s)})\right))$$

Formalization. D5/S3/Combinatorics/Lattices/ShalaCosetLikeAtomisticLattice.WeaklyCosetLike (✓ std3).

Citation. Besfort Shala (2024). The Probabilistic Zeta Function of a Finite Lattice. URL: https://arxiv.org/abs/2112.13766v6.

Commentary.

Weak coset-likeness requires P L s to have a finite ordinary Dirichlet-series representation with integer coefficients.

Definition 1.7 (The universal form of Question 7.4).

$$\forall L\in \mathrm{Type},[\mathrm{Lattice}\left(L\right)][\mathrm{BoundedOrder}\left(L\right)][\mathrm{Fintype}\left(L\right)][\mathrm{DecidableEq}\left(L\right)][\mathrm{DecidableLE}\left(L\right)][\mathrm{LocallyFiniteOrder}\left(L\right)]\mathrm{IsAtomistic}\left(L\right)\Rightarrow (\mathrm{WeaklyCosetLike}\left(L\right)\Rightarrow (\mathrm{StronglyCosetLike}\left(L\right)))$$

Formalization. D5/S3/Combinatorics/Lattices/ShalaCosetLikeAtomisticLattice.claim (✓ std3).

Citation. Besfort Shala (2024). The Probabilistic Zeta Function of a Finite Lattice. URL: https://arxiv.org/abs/2112.13766v6.

Commentary.

Question 7.4 asks verbatim: ‘Does there exist a weakly coset-like atomistic lattice that is not strongly coset-like?’ The formal claim is its universal negation: every finite atomistic weakly coset-like lattice is strongly coset-like.

Theorem 1.8 (The universal implication is false).

$$\neg \left(\forall L\in \mathrm{Type},[\mathrm{Lattice}\left(L\right)][\mathrm{BoundedOrder}\left(L\right)][\mathrm{Fintype}\left(L\right)][\mathrm{DecidableEq}\left(L\right)][\mathrm{DecidableLE}\left(L\right)][\mathrm{LocallyFiniteOrder}\left(L\right)]\mathrm{IsAtomistic}\left(L\right)\Rightarrow (\mathrm{WeaklyCosetLike}\left(L\right)\Rightarrow (\mathrm{StronglyCosetLike}\left(L\right)))\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Lattices/ShalaCosetLikeAtomisticLattice.result (✓ std3). ∎

Resolves. Problems/shala-2024-coset-like-lattice-question-7-4 (refuted) by D5/S3/Combinatorics/Lattices/ShalaCosetLikeAtomisticLattice.result.

Source. Repository-derived.

Acknowledgement. Besfort Shala (2024). The Probabilistic Zeta Function of a Finite Lattice. URL: https://arxiv.org/abs/2112.13766v6.

Commentary.

With Ω = {1, …, 8}, X = {1, 2, 3} and A = {1, 2, 3, 4}, let L₄ = {∅, X, A, Ω} ∪ {{i} : i ∈ Ω}, ordered by inclusion. The elements p0, …, p7 correspond to the singletons {1}, …, {8}, x to X, a to A, bot to ∅ and top to Ω. This lattice has twelve elements, and its join-irreducibles are the eight singletons. Exactly three of them lie below X, and 3 does not divide 8. The upper Möbius coefficient of X vanishes, and the remaining terms give P L₄ s = 1 − 2^(−s) − 4·8^(−s), an ordinary Dirichlet series. Thus the lattice is weakly coset-like but not strongly coset-like, refuting the universal implication and answering the question affirmatively. The formal result uses this single lattice (m = 4); the uniform family for every m ≥ 4 is not formalized and remains open. The d-divisible partition-lattice question and minimality are not settled here.

References

• Truth anchor: D5/S3/Combinatorics/Lattices/ShalaCosetLikeAtomisticLattice.J
• Truth anchor: D5/S3/Combinatorics/Lattices/ShalaCosetLikeAtomisticLattice.Jx
• Truth anchor: D5/S3/Combinatorics/Lattices/ShalaCosetLikeAtomisticLattice.P
• Truth anchor: D5/S3/Combinatorics/Lattices/ShalaCosetLikeAtomisticLattice.StronglyCosetLike
• Truth anchor: D5/S3/Combinatorics/Lattices/ShalaCosetLikeAtomisticLattice.WeaklyCosetLike
• Truth anchor: D5/S3/Combinatorics/Lattices/ShalaCosetLikeAtomisticLattice.claim
• Truth anchor: D5/S3/Combinatorics/Lattices/ShalaCosetLikeAtomisticLattice.index
• Truth anchor: D5/S3/Combinatorics/Lattices/ShalaCosetLikeAtomisticLattice.result