slug: hardin185765
bibkey: hardin2011a185765
doi: null
url: https://oeis.org/A185765
triage: theorem
motivation_gids:
  - D5/S3/Combinatorics/TraceAvoidingArrays/HardinA185765Recurrence.result

Hardin’s six-column trace-avoidance recurrence

Problem

R. H. Hardin’s sole FORMULA field in OEIS A185765, revision 9, states:

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

Its NAME field is:

Number of (n+1)X6 binary arrays with no 2X2 subblock trace equal to any horizontal or vertical neighbor 2X2 subblock trace.

The claim concerns every natural $n\ge 13$. Arrays are labeled, with binary entries, open rectangular boundaries and no quotient by symmetries. Each contiguous block has its ordinary main-diagonal trace in the natural numbers. The counts are embedded in the integers before the signed recurrence is taken.

Statement echo

The row encoding uses Mathlib’s finFunctionFinEquiv. The public array predicate and cardinality retain the source’s literal conventions. The transfer vectors, residual and certificate organize the proof and add no hypothesis to result.

Motivation

The settling declaration is D5.S3.Combinatorics.TraceAvoidingArrays.HardinA185765Recurrence.result. The external assertion and conventions are preregistered in issue #22447. The source note is Library/RecurrenceComposition/hardin2011a185765.md.

Gap

The preregistration’s bounded source and literature screen found no proof or proof reference in OEIS revisions 1 through 9. The jOEIS implementation retains Conjectural. The screened nearby works on Hardinian arrays concern different constraints. These readings do not establish an exhaustive literature search; completeness and worldwide priority are ASSUMED-UNVERIFIED.

Route

Encode each binary row by an element of $\mathrm{Fin}(64)$. Horizontally admissible consecutive row pairs are states. Vertical comparisons constrain transitions between overlapping pairs. HardinA185765Transfer.counting_bridge identifies the literal array count $a(k+1)$ with the sum of the continuation vector $u(k)$ for every natural $k$.

For $Q(X)=X^9-X^8-30X^7-24X^6+95X^5+15X^4-64X^3+116X^2-16X-16$, the residual is $Q(T)u(k)$, where $T$ is the linear continuation operator. finite_certificate proves that the vector residual at five vanishes and that its scalar totals at three and four vanish. The consumed private recurrence_from_certificate propagates the vector identity by linearity, uses the two scalar boundary identities and applies the counting bridge. Its conclusion is claim; result supplies its certificate premise.

Falsifier

An admissible-array count violating the displayed recurrence at any natural $n\ge 13$ would contradict result. A nonzero scalar residual at $n=12$ does not contradict the source; it rules out lowering that starting index while keeping the same coefficients.

Evidence

The kernel declarations are D5.S3.Combinatorics.TraceAvoidingArrays.HardinA185765Transfer.counting_bridge, D5.S3.Combinatorics.TraceAvoidingArrays.HardinA185765Recurrence.finite_certificate and D5.S3.Combinatorics.TraceAvoidingArrays.HardinA185765Recurrence.result. The axiom closure of every public declaration is contained in {propext, Classical.choice, Quot.sound}.

The independent experiment is in the pinned six-column trace-avoidance directory. The script is docs/reports/six-column-trace-avoidance/check.py, at commit 8c1ae78df7371e28241a930a79d387b013bbe604, with SHA-256 4467b18b5567329731539b327f1fee36ca25bc52fb06fd9fa3b912acd0797a94. Executing the pinned script with python3 check.py exits 0. It enumerates all 4096 two-row and 262144 three-row arrays, checks all four supplied examples, compares independent state and edge constructions, matches all 200 supplied OEIS terms at $n=1,\dots ,200$, and verifies the recurrence at $n=13,\dots ,200$. It computes 680 active row pairs, 3456 directed edges and scalar residuals $-23144,27200,-4160$ at $n=10,11,12$, respectively. These are finite exact computations, separate from the all-length kernel proof.

Triage

1. Proved (kernel-checked): the literal array count equals the sum of row-pair continuation counts for every $k$, at $a(k+1)$, by HardinA185765Transfer.counting_bridge.
2. Proved (kernel-checked): the finite certificate implies the exact recurrence for every $n\ge 13$, by the consumed private HardinA185765Recurrence.recurrence_from_certificate. Its sole premise is HardinA185765Recurrence.Certificate; result discharges it with finite_certificate.
3. Proved (kernel-checked): the vector residual at five is zero and the scalar residual totals at three and four are zero, by HardinA185765Recurrence.finite_certificate.
4. Proved (kernel-checked): the exact all-length source recurrence for every $n\ge 13$, by HardinA185765Recurrence.result.
5. Computed: 680 active row pairs, 3456 directed edges, agreement with all 200 supplied terms and recurrence residual zero for $n=13,\dots ,200$. Evidence is the pinned experiment command, exit 0 and script SHA-256 above.
6. Computed: the scalar residual at $n=12$ is $-4160$. Thus the same recurrence cannot start at twelve. Evidence is the same pinned experiment.
7. Open: minimality of $Q$, other widths and a width-uniform formula. No declaration here settles them.

What the settlement shows

The counting bridge connects literal arrays to the finite transfer system; the finite vector annihilator and its two scalar boundary equalities extend it to every source index. These mechanisms are proved by the declarations named above. The threshold obstruction at twelve is computed, not a separate Lean theorem. Generalization to another width and minimality remain open. The source lists no downstream theorem relying on its empirical recurrence; the jOEIS implementation uses that recurrence with the Conjectural marker, according to the literature reading in #22447.

The escape audit is unfinished for all fourteen public theorem targets under issue #22760. No faithful compiled Reg mirror or declared_validated registration is claimed.

ASSUMED-UNVERIFIED

Literature completeness and worldwide priority are unverified: the bounded screen in #22447 has unavailable services and unread separate journal versions. The budget-exhausted helper reuse searches identified in the independent pre-freeze input supply no negative reuse result. No width-uniform extension or minimality claim is made.