Hardin and Barker’s five-column array formulas

Abstract

Exact five-column array counts, parity, recurrence and formal generating series.

Definition 1.1 (Distinct signed clockwise differences).

$$\forall a\in \mathrm{Fin}\left(3\right),\forall b\in \mathrm{Fin}\left(3\right),\forall c\in \mathrm{Fin}\left(3\right),\forall d\in \mathrm{Fin}\left(3\right),\mathrm{DistinctClockwise}\left(a,b,c,d\right)=\mathrm{List}.\mathrm{Pairwise}\left((\mathrm{fun}xy:\mathbb{Z}\mapsto x\ne y),[(\mathrm{val}\left(b\right):\mathbb{Z})-(\mathrm{val}\left(a\right):\mathbb{Z}),(\mathrm{val}\left(d\right):\mathbb{Z})-(\mathrm{val}\left(b\right):\mathbb{Z}),(\mathrm{val}\left(c\right):\mathbb{Z})-(\mathrm{val}\left(d\right):\mathbb{Z}),(\mathrm{val}\left(a\right):\mathbb{Z})-(\mathrm{val}\left(c\right):\mathbb{Z})]\right)$$

Formalization. D5/S3/Combinatorics/Graph/Pressure/HardinBarkerA209723EdgeDifferences.DistinctClockwise (✓ std3).

Citation. R. H. Hardin; Colin Barker (2012). OEIS A209723: five-column arrays with distinct clockwise edge differences. URL: https://oeis.org/A209723/internal.

Commentary.

OEIS A209723, revision 11, NAME: “1/4 the number of (n+1) X 5 0..2 arrays with every 2 X 2 subblock having distinct clockwise edge differences.” For a square with top row a,b and bottom row c,d, clockwise differences are b-a,d-b,c-d,a-c in the integers. Entries have type Fin 3; val is the natural representative and each representative is coerced to the integers before subtraction.

Definition 1.2 (The literal arrays).

$$\forall n\in \mathbb{N},\forall X\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n+1\right),\mathrm{Fin}\left(5\right),\mathrm{Fin}\left(3\right)\right),\mathrm{IsSourceArray}\left(X\right)=(\forall i\in \mathrm{Fin}\left(n\right),\forall j\in \mathrm{Fin}\left(4\right),\mathrm{DistinctClockwise}\left(X\left(\mathrm{Fin}.\mathrm{castSucc}\left(i\right),\mathrm{Fin}.\mathrm{castSucc}\left(j\right)\right),X\left(\mathrm{Fin}.\mathrm{castSucc}\left(i\right),\mathrm{Fin}.\mathrm{succ}\left(j\right)\right),X\left(\mathrm{Fin}.\mathrm{succ}\left(i\right),\mathrm{Fin}.\mathrm{castSucc}\left(j\right)\right),X\left(\mathrm{Fin}.\mathrm{succ}\left(i\right),\mathrm{Fin}.\mathrm{succ}\left(j\right)\right)\right))$$

Formalization. D5/S3/Combinatorics/Graph/Pressure/HardinBarkerA209723EdgeDifferences.IsSourceArray (✓ std3).

Citation. R. H. Hardin; Colin Barker (2012). OEIS A209723: five-column arrays with distinct clockwise edge differences. URL: https://oeis.org/A209723/internal.

Commentary.

OEIS A209723, revision 11, NAME: “1/4 the number of (n+1) X 5 0..2 arrays with every 2 X 2 subblock having distinct clockwise edge differences.” Matrix has n+1 labelled rows and five labelled columns, with entries Fin 3. Fin.castSucc and Fin.succ select the two consecutive row or column positions. Every adjacent square is tested; rotations, reflections and translations are not identified.

Definition 1.3 (One quarter of the raw count).

$$\forall n\in \mathbb{N},a\left(n\right)=\frac{(\mathrm{Nat}.\mathrm{card}\left(\{X:\mathrm{Matrix}\left(\mathrm{Fin}\left(n+1\right),\mathrm{Fin}\left(5\right),\mathrm{Fin}\left(3\right)\right)//\mathrm{IsSourceArray}\left(X\right)\}\right):\mathbb{Q})}{4}$$

Formalization. D5/S3/Combinatorics/Graph/Pressure/HardinBarkerA209723EdgeDifferences.a (✓ std3).

Citation. R. H. Hardin; Colin Barker (2012). OEIS A209723: five-column arrays with distinct clockwise edge differences. URL: https://oeis.org/A209723/internal.

Commentary.

OEIS A209723, revision 11, NAME: “1/4 the number of (n+1) X 5 0..2 arrays with every 2 X 2 subblock having distinct clockwise edge differences.” Nat.card counts the full subtype of these labelled arrays. The result is coerced to the rationals and divided by rational four. Offset 1,1 restricts the source formulas to positive n; a is defined for every natural input.

Definition 1.4 (Coefficients of the ordinary formal series).

$$\forall A\in \mathrm{PowerSeries}\left(\mathbb{Q}\right),\mathrm{IsSourceSeries}\left(A\right)=(\mathrm{PowerSeries}.\mathrm{coeff}\left(0,A\right)=0\wedge \left(\forall n\in \mathbb{N},1\le n\Rightarrow \mathrm{PowerSeries}.\mathrm{coeff}\left(n,A\right)=a\left(n\right)\right))$$

Formalization. D5/S3/Combinatorics/Graph/Pressure/HardinBarkerA209723EdgeDifferences.IsSourceSeries (✓ std3).

Citation. R. H. Hardin; Colin Barker (2012). OEIS A209723: five-column arrays with distinct clockwise edge differences. URL: https://oeis.org/A209723/internal.

Commentary.

OEIS A209723, revision 11, FORMULA: “G.f.: x*(6 + x - 11x^2) / ((1 - x)(1 - 2*x^2)).” With offset 1,1, the ordinary series has zero constant coefficient and coefficient a(n) for every n at least one. The carrier is PowerSeries over the rationals.

Definition 1.5 (Parity, recurrence, existence and generating identity).

$$\mathrm{claim}=((\forall m\in \mathbb{N},a\left(2\cdot (m+1)\right)=3\cdot (2:\mathbb{Q}{)}^m+4)\wedge \left((\forall m\in \mathbb{N},a\left(2\cdot m+1\right)=(2:\mathbb{Q}{)}^{m+1}+4)\wedge \left((\forall m\in \mathbb{N},a\left(m+4\right)=a\left(m+3\right)+2\cdot a\left(m+2\right)-2\cdot a\left(m+1\right))\wedge \left((\exists A\in \mathrm{PowerSeries}\left(\mathbb{Q}\right),\mathrm{IsSourceSeries}\left(A\right))\wedge (\forall A\in \mathrm{PowerSeries}\left(\mathbb{Q}\right),\mathrm{IsSourceSeries}\left(A\right)\Rightarrow A\cdot ((1-\mathrm{PowerSeries}.X)\cdot (1-2\cdot \mathrm{PowerSeries}.X^2))=\mathrm{PowerSeries}.X\cdot (6+\mathrm{PowerSeries}.X-11\cdot \mathrm{PowerSeries}.X^2))\right)\right)\right))$$

Formalization. D5/S3/Combinatorics/Graph/Pressure/HardinBarkerA209723EdgeDifferences.claim (✓ std3).

Citation. R. H. Hardin; Colin Barker (2012). OEIS A209723: five-column arrays with distinct clockwise edge differences. URL: https://oeis.org/A209723/internal.

Commentary.

OEIS A209723, revision 11, FORMULA (the entry has no page numbers): Empirical: a(n) = a(n-1) + 2a(n-2) - 2a(n-3). Conjectures from Colin Barker, Jul 12 2018: (Start) G.f.: x*(6 + x - 11x^2) / ((1 - x)(1 - 2x^2)). a(n) = 32^(n/2 - 1) + 4 for n even. a(n) = 2^((n + 1)/2) + 4 for n odd. (End) The positive even index is 2*(m+1), the odd index is 2*m+1, and the recurrence index is m+4, for natural m. The series assertion includes existence and holds for every series with the specified coefficients. Multiplication by the denominator expresses the rational generating identity in PowerSeries, since its constant coefficient is one.

Theorem 1.6 (The full five-column counting theorem).

$$(\forall m\in \mathbb{N},a\left(2\cdot (m+1)\right)=3\cdot (2:\mathbb{Q}{)}^m+4)\wedge \left((\forall m\in \mathbb{N},a\left(2\cdot m+1\right)=(2:\mathbb{Q}{)}^{m+1}+4)\wedge \left((\forall m\in \mathbb{N},a\left(m+4\right)=a\left(m+3\right)+2\cdot a\left(m+2\right)-2\cdot a\left(m+1\right))\wedge \left((\exists A\in \mathrm{PowerSeries}\left(\mathbb{Q}\right),\mathrm{IsSourceSeries}\left(A\right))\wedge (\forall A\in \mathrm{PowerSeries}\left(\mathbb{Q}\right),\mathrm{IsSourceSeries}\left(A\right)\Rightarrow A\cdot ((1-\mathrm{PowerSeries}.X)\cdot (1-2\cdot \mathrm{PowerSeries}.X^2))=\mathrm{PowerSeries}.X\cdot (6+\mathrm{PowerSeries}.X-11\cdot \mathrm{PowerSeries}.X^2))\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Pressure/HardinBarkerA209723EdgeDifferences.result (✓ std3). ∎

Resolves. Problems/hardin-barker-a209723-edge-differences (proved) by D5/S3/Combinatorics/Graph/Pressure/HardinBarkerA209723EdgeDifferences.result.

Source. Repository-derived.

Acknowledgement. R. H. Hardin; Colin Barker (2012). OEIS A209723: five-column arrays with distinct clockwise edge differences. URL: https://oeis.org/A209723/internal.

Commentary.

Reading consecutive rows gives an explicit equivalence between the array subtype and finite compatible row sequences. The exact row adjacency table has two branching three-vertex paths and sixteen deterministic starting rows. At odd length 2m+1, the number from a fixed start is 2^m times its branching degree plus its deterministic indicator; at even length 2m+2 it is 2^(m+1) times its branching indicator plus its deterministic indicator. The two-step induction holds for every natural m. Summing over starting rows and dividing by four proves both parity formulas. The affine relation a(n+3)=2*a(n+1)-4 yields the homogeneous recurrence. PowerSeries.mk gives existence, and coefficient extensionality gives the full generating identity without an analytic convergence premise.

References

• Truth anchor: D5/S3/Combinatorics/Graph/Pressure/HardinBarkerA209723EdgeDifferences.DistinctClockwise
• Truth anchor: D5/S3/Combinatorics/Graph/Pressure/HardinBarkerA209723EdgeDifferences.IsSourceArray
• Truth anchor: D5/S3/Combinatorics/Graph/Pressure/HardinBarkerA209723EdgeDifferences.IsSourceSeries
• Truth anchor: D5/S3/Combinatorics/Graph/Pressure/HardinBarkerA209723EdgeDifferences.a
• Truth anchor: D5/S3/Combinatorics/Graph/Pressure/HardinBarkerA209723EdgeDifferences.claim
• Truth anchor: D5/S3/Combinatorics/Graph/Pressure/HardinBarkerA209723EdgeDifferences.result