The odd-dimensional improvement

Abstract

In every odd dimension at least eleven, one more member than the chain guarantee is unavoidable. A balanced binary rank word of even length at least twelve has either three equally spaced consecutive occurrences of one colour or a balanced interval of length twelve. Balanced colourings of twelve ranks admit a seven-member monochromatic sublattice.

Definition 1.1 (Equally spaced consecutive occurrences).

$$\forall g\in \mathrm{Nat}\to \mathrm{Bool},\forall n\in \mathrm{Nat},\mathrm{ConsecutiveAP}\left(g,n\right)\iff \left(\exists a\in \mathrm{Nat},\exists b\in \mathrm{Nat},\exists c\in \mathrm{Nat},a<b\wedge \left(b<c\wedge \left(c\le n\wedge \left(a+c=\mathrm{mul}\left(2,b\right)\wedge \left(g\left(a\right)=g\left(b\right)\wedge \left(g\left(b\right)=g\left(c\right)\wedge \left(\left(\forall r\in \mathrm{Nat},\left(a<r\wedge r<b\right)\Rightarrow \left(\neg g\left(r\right)=g\left(b\right)\right)\right)\wedge \left(\forall r\in \mathrm{Nat},\left(b<r\wedge r<c\right)\Rightarrow \left(\neg g\left(r\right)=g\left(b\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/ErdosUlam/SublatticeChainBound.ConsecutiveAP (✓ std3).

Source. Repository-derived.

Commentary.

The ranks a, b, c have one colour and equal positive gaps. Every rank strictly between a and b or between b and c has the other colour.

Definition 1.2 (Balanced interval of length twelve).

$$\forall g\in \mathrm{Nat}\to \mathrm{Bool},\forall b\in \mathrm{Nat},\mathrm{BalancedWindow}\left(g,b\right)\iff \mathrm{card}\left(\mathrm{filter}\left(\mathrm{range}\left(12\right),\mathrm{trueAtOffset}\left(g,b\right)\right)\right)=6$$

Formalization. D5/S3/Combinatorics/ErdosUlam/SublatticeChainBound.BalancedWindow (✓ std3).

Source. Repository-derived.

Commentary.

The interval beginning at b contains six true ranks and six false ranks.

Theorem 1.3 (The balanced rank-word alternative).

$$\forall g\in \mathrm{Nat}\to \mathrm{Bool},\forall n\in \mathrm{Nat},\left(11\le n\wedge \left(\mathrm{Odd}\left(n\right)\wedge \mathrm{card}\left(\mathrm{filter}\left(\mathrm{range}\left(n+1\right),\mathrm{trueAtOffset}\left(g,0\right)\right)\right)=\mathrm{div}\left(n+1,2\right)\right)\right)\Rightarrow \left(\mathrm{ConsecutiveAP}\left(g,n\right)\vee \left(\exists b\in \mathrm{Nat},b+11\le n\wedge \mathrm{BalancedWindow}\left(g,b\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/ErdosUlam/SublatticeChainBound.rank_word_lemma (✓ std3). ∎

Source. Repository-derived.

Commentary.

An equally spaced consecutive triple is present in each of the local words 000, 111, 01010, 10101, 0110110 and 1001001. Extend a word one letter at a time, excluding those suffixes and balanced suffixes of length twelve. The resulting collection is empty at length fifteen. At length fourteen none of its words has seven letters of each colour. A balanced word of length twelve is already the required interval. These three cases cover every even length at least twelve.

Theorem 1.4 (Balanced rank colourings).

$$\forall g\in \mathrm{Nat}\to \mathrm{Bool},\mathrm{card}\left(\mathrm{filter}\left(\mathrm{trueRanks}\left(g\right),\mathrm{range}\left(12\right)\right)\right)=6\Rightarrow \left(\exists L\in \mathrm{Finset}\left(\mathrm{Finset}\left(\mathrm{Fin}\left(11\right)\right)\right),\mathrm{IsSublattice}\left(L\right)\wedge \left(\mathrm{Monochromatic}\left(\mathrm{rankColouring}\left(g\right),L\right)\wedge 7\le \mathrm{card}\left(L\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/ErdosUlam/SublatticeChainBound.balanced_rank_base (✓ std3). ∎

Source. Repository-derived.

Commentary.

Of the 924 balanced rank patterns, 874 contain three consecutive occurrences of one colour in arithmetic progression. The corresponding diamond augments the six same-colour prefixes. Each of the remaining fifty patterns is covered by one of ten bitmask families closed under union and intersection, with seven or eight distinct members.

Definition 1.5 (Guaranteed size).

$$\forall n\in \mathrm{Nat},f\left(n\right)=\underset{chi:\mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right)\to \mathrm{Bool}}{\min }\underset{L:\mathrm{Finset}\left(\mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right)\right),\mathrm{IsSublattice}\left(L\right)\wedge \mathrm{Monochromatic}\left(chi,L\right)}{\max }\mathrm{card}\left(L\right)$$

Formalization. D5/S3/Combinatorics/ErdosUlam/SublatticeChainBound.f (✓ std3).

Source. Repository-derived.

Commentary.

Minimize over all colourings the largest cardinality of a monochromatic sublattice.

Definition 1.6 (Proposed formula).

$$claim\iff \left(\forall n\in \mathrm{Nat},f\left(n\right)=\lfloor \frac{n+2}{2}\rfloor \right)$$

Formalization. D5/S3/Combinatorics/ErdosUlam/SublatticeChainBound.claim (✓ std3).

Source. Repository-derived.

Commentary.

The proposed equality is asserted in every natural dimension.

Theorem 1.7 (The odd-dimensional lower bound).

$$\forall n\in \mathrm{Nat},11\le n\Rightarrow \left(\mathrm{Odd}\left(n\right)\Rightarrow \lfloor \frac{n+3}{2}\rfloor \le f\left(n\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/ErdosUlam/SublatticeChainBound.odd_lower_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

If every monochromatic sublattice had at most half the number of ranks, equal-size subsets would have equal colour and both rank colours would be balanced. A consecutive arithmetic progression adds a diamond member. Otherwise a balanced twelve-rank interval admits a seven-member sublattice; embedding it and adjoining the same-colour prefixes outside the interval again adds one member.

Theorem 1.8 (The formula is false).

$$\neg claim$$

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

Resolves. Problems/bhattacharjee-mandal-bhattacharya-2026-sublattice-chain-bound-refutation (refuted) by D5/S3/Combinatorics/ErdosUlam/SublatticeChainBound.result.

Source. Repository-derived.

Commentary.

At dimension eleven the lower bound is seven, whereas the proposed formula gives six. The separate linear-growth question remains open.

References

• Truth anchor: D5/S3/Combinatorics/ErdosUlam/SublatticeChainBound.BalancedWindow
• Truth anchor: D5/S3/Combinatorics/ErdosUlam/SublatticeChainBound.ConsecutiveAP
• Truth anchor: D5/S3/Combinatorics/ErdosUlam/SublatticeChainBound.balanced_rank_base
• Truth anchor: D5/S3/Combinatorics/ErdosUlam/SublatticeChainBound.claim
• Truth anchor: D5/S3/Combinatorics/ErdosUlam/SublatticeChainBound.f
• Truth anchor: D5/S3/Combinatorics/ErdosUlam/SublatticeChainBound.odd_lower_bound
• Truth anchor: D5/S3/Combinatorics/ErdosUlam/SublatticeChainBound.rank_word_lemma
• Truth anchor: D5/S3/Combinatorics/ErdosUlam/SublatticeChainBound.result
• Dependency: D5/S3/Combinatorics/ErdosUlam/SublatticeConstructions
• Dependency: D5/S3/Combinatorics/ErdosUlam/SublatticeRankRigidity