HardinA185765Recurrence

Abstract

Six-column binary arrays and Hardin’s trace-avoidance recurrence.

Definition 1.1 (Hardin’s empirical recurrence).

$$(claim)\iff (\forall (n:\mathbb{N}),(13\le n)\Rightarrow ((a\left(n\right):\mathbb{Z})=(a\left(n-1\right):\mathbb{Z})+30\cdot (a\left(n-2\right):\mathbb{Z})+24\cdot (a\left(n-3\right):\mathbb{Z})-95\cdot (a\left(n-4\right):\mathbb{Z})-15\cdot (a\left(n-5\right):\mathbb{Z})+64\cdot (a\left(n-6\right):\mathbb{Z})-116\cdot (a\left(n-7\right):\mathbb{Z})+16\cdot (a\left(n-8\right):\mathbb{Z})+16\cdot (a\left(n-9\right):\mathbb{Z})))$$

Formalization. D5/S3/Combinatorics/TraceAvoidingArrays/HardinA185765Recurrence.claim (✓ std3).

Citation. R. H. Hardin (2011). OEIS A185765: six-column binary arrays with unequal neighboring subblock traces. URL: https://oeis.org/A185765.

Commentary.

Empirical: a(n)=a(n-1)+30a(n-2)+24a(n-3)-95a(n-4)-15a(n-5)+64a(n-6)-116a(n-7)+16a(n-8)+16a(n-9) for n>12 Sole FORMULA field, OEIS A185765 revision 9, without page numbering. The count a is the preceding finite cardinality. Natural subtraction is truncated; all ten indices are positive when n is at least thirteen. Counts are embedded in the integers before signed operations.

Definition 1.2 (The vector residual).

$$\forall (k:\mathbb{N}),\mathrm{residual}\left(k\right)=u\left(k+9\right)-u\left(k+8\right)-HSMul.hSMul\left((30:\mathbb{Z}),u\left(k+7\right)\right)-HSMul.hSMul\left((24:\mathbb{Z}),u\left(k+6\right)\right)+HSMul.hSMul\left((95:\mathbb{Z}),u\left(k+5\right)\right)+HSMul.hSMul\left((15:\mathbb{Z}),u\left(k+4\right)\right)-HSMul.hSMul\left((64:\mathbb{Z}),u\left(k+3\right)\right)+HSMul.hSMul\left((116:\mathbb{Z}),u\left(k+2\right)\right)-HSMul.hSMul\left((16:\mathbb{Z}),u\left(k+1\right)\right)-HSMul.hSMul\left((16:\mathbb{Z}),u\left(k\right)\right)$$

Formalization. D5/S3/Combinatorics/TraceAvoidingArrays/HardinA185765Recurrence.residual (✓ std3).

Source. Repository-derived.

Acknowledgement. R. H. Hardin (2011). OEIS A185765: six-column binary arrays with unequal neighboring subblock traces. URL: https://oeis.org/A185765.

Commentary.

The residual applies the nine coefficients of the recurrence to consecutive continuation vectors, with scalar multiplication over the integers.

Definition 1.3 (Three finite equalities).

$$(Certificate)\iff ((\mathrm{residual}\left(5\right)=0)\wedge ((\sum _{r:\mathrm{Fin}\left(64\right)}(\sum _{s:\mathrm{Fin}\left(64\right)}(\mathrm{residual}\left(3\right)\left(r,s\right)))=0)\wedge (\sum _{r:\mathrm{Fin}\left(64\right)}(\sum _{s:\mathrm{Fin}\left(64\right)}(\mathrm{residual}\left(4\right)\left(r,s\right)))=0)))$$

Formalization. D5/S3/Combinatorics/TraceAvoidingArrays/HardinA185765Recurrence.Certificate (✓ std3).

Source. Repository-derived.

Acknowledgement. R. H. Hardin (2011). OEIS A185765: six-column binary arrays with unequal neighboring subblock traces. URL: https://oeis.org/A185765.

Commentary.

The vector residual at five is zero, and the scalar totals at three and four are zero.

Theorem 1.4 (The three equalities hold).

$$(\mathrm{residual}\left(5\right)=0)\wedge ((\sum _{r:\mathrm{Fin}\left(64\right)}(\sum _{s:\mathrm{Fin}\left(64\right)}(\mathrm{residual}\left(3\right)\left(r,s\right)))=0)\wedge (\sum _{r:\mathrm{Fin}\left(64\right)}(\sum _{s:\mathrm{Fin}\left(64\right)}(\mathrm{residual}\left(4\right)\left(r,s\right)))=0))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/TraceAvoidingArrays/HardinA185765Recurrence.finite_certificate (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. R. H. Hardin (2011). OEIS A185765: six-column binary arrays with unequal neighboring subblock traces. URL: https://oeis.org/A185765.

Commentary.

The literal tables satisfy every transfer step through fourteen, the vector residual at five vanishes, and the scalar residual totals at three and four vanish.

Theorem 1.5 (The recurrence holds for every stated index).

$$\forall (n:\mathbb{N}),(13\le n)\Rightarrow ((a\left(n\right):\mathbb{Z})=(a\left(n-1\right):\mathbb{Z})+30\cdot (a\left(n-2\right):\mathbb{Z})+24\cdot (a\left(n-3\right):\mathbb{Z})-95\cdot (a\left(n-4\right):\mathbb{Z})-15\cdot (a\left(n-5\right):\mathbb{Z})+64\cdot (a\left(n-6\right):\mathbb{Z})-116\cdot (a\left(n-7\right):\mathbb{Z})+16\cdot (a\left(n-8\right):\mathbb{Z})+16\cdot (a\left(n-9\right):\mathbb{Z}))$$

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

Resolves. Problems/hardin185765 (proved) by D5/S3/Combinatorics/TraceAvoidingArrays/HardinA185765Recurrence.result.

Source. Repository-derived.

Acknowledgement. R. H. Hardin (2011). OEIS A185765: six-column binary arrays with unequal neighboring subblock traces. URL: https://oeis.org/A185765.

Commentary.

Linearity propagates the vanishing vector residual from five onward. The scalar equalities at three and four cover indices thirteen and fourteen. The counting identity then gives the stated recurrence for every n at least thirteen.

References

• Truth anchor: D5/S3/Combinatorics/TraceAvoidingArrays/HardinA185765Recurrence.Certificate
• Truth anchor: D5/S3/Combinatorics/TraceAvoidingArrays/HardinA185765Recurrence.claim
• Truth anchor: D5/S3/Combinatorics/TraceAvoidingArrays/HardinA185765Recurrence.finite_certificate
• Truth anchor: D5/S3/Combinatorics/TraceAvoidingArrays/HardinA185765Recurrence.residual
• Truth anchor: D5/S3/Combinatorics/TraceAvoidingArrays/HardinA185765Recurrence.result
• Dependency: D5/S3/Combinatorics/TraceAvoidingArrays/HardinA185765Transfer