Hanna's A369673 square classification and five-adic orders

Paul D. Hanna's OEIS A369673, revision #21, states four conjectures for $a(N)=\prod_{k=0}^{N}(2^k+2^{N-k})$:

• (C.1) $a(N)$ is a square if and only if $4\nmid N$.
• (C.2) $5\nmid a(2n+1)$.
• (C.3) $v_5(a(4n))=2b(n)$.
• (C.4) $v_5(a(4n+2))=2b(n+1)$.

Here $b(n)=v_5((10n)!)-v_5((5n)!)$ is the signed integer difference in OEIS A127428. All indices are natural, including zero. The valuation agrees with A112765 on positive arguments. The source, conventions and literature screen are in preregistration #21915.

Statement echo

| Source item | Lean counterpart | Fidelity | | --- | --- | --- | | Product from $k=0$ through $k=N$ | HannaA369673.a | Literal finite product; natural subtraction has nonnegative arguments on the range. | | Signed factorial valuation difference | HannaA369673.b | Natural valuations cast into integers before subtraction. | | C.1 | First conjunct of HannaA369673.claim | Natural square root and both directions of the equivalence. | | C.2 | Second conjunct of HannaA369673.claim | Every natural index. | | C.3 | Third conjunct of HannaA369673.claim | Exact integer-valued equality, zero included. | | C.4 | Fourth conjunct of HannaA369673.claim | Exact integer-valued equality with the source shift. | | Entire conjecture package | HannaA369673.result | All four conjuncts, with no additional hypothesis. |

No source clause is dropped. The private products and sums are proof auxiliaries; they impose no hypothesis on the public claim.

The settling declaration is D5/S3/Arith/FactorialRatio/HannaA369673.result. Its admission basis is open-problem-resolution (#21915; Proved), with generality I and utility: none. The conclusion is an unbounded symbolic classification and valuation formula. The source note records the source statements and their locators.

The preregistration's partial literature screen found no resolution in its read sources. It distinguishes the OEIS conjectures from related cyclotomic valuation and weighted-permutation papers. OpenAlex and Semantic Scholar discovery was rate-limited, and the broad arXiv search was inspected only on its first page. Literature completeness is ASSUMED-UNVERIFIED; no exhaustive novelty claim is made.

Equal boundary factors give the two-step recurrence $a(N+2)=2^{N+1}(1+2^{N+2})^2a(N)$. For $Q(m)=\prod_{j=1}^{m}(1+4^j)$, induction gives $a(2m)=2^{m^2+1}Q(m)^2$. Positivity and oddness of $Q(m)$ identify the exact two-adic order. At odd indices the same recurrence preserves squareness and excludes divisibility by five. The imported Erdos7.finset_prod_odd_nat supplies oddness of the auxiliary product. Mathlib's padicValNat.pow_add_pow supplies the odd-exponent lifting step; padicValNat_factorial_mul identifies the resulting sum with $b$.

A failure at any natural index of one of the four conjuncts contradicts the claim. Index zero is included: $a(0)=2$, $b(0)=0$ and $v_5(a(0))=0$. Finite agreement alone does not prove any universal assertion.

D5.S3.Arith.FactorialRatio.HannaA369673.result proves the full claim. The public definitions are a, b and claim; all proof helpers are private. The implementation is classified bind-only, admitted as the named external open-problem resolution, with no claimed escape witness.

The escape audit for the public result is unfinished: issue #22235. No valid four-slot Reg mirror is delivered. The missing evidence is a lawful common-family reconstruction/readout bridge with variation and sensitivity proofs for the conjunction of heterogeneous square, divisibility and valuation observations.

What the settlement shows

| Item | Status and evidence kind | Evidence | | --- | --- | --- | | Equal boundary factors give the recurrence and the even-index factorization | Proved; kernel-checked private declarations | a_step, a_even: $a(N+2)=2^{N+1}(1+2^{N+2})^2a(N)$ and $a(2m)=2^{m^2+1}Q(m)^2$. | | $Q(m)$ is positive and odd, $v_2(a(2m))=m^2+1$, and parity gives the exact square classification; odd indices are squares | Proved; kernel-checked private declarations and public result | Q_pos, Q_odd, a_even_twoVal, a_even_square, a_odd_square, square_classification, and the first conjunct of result. | | Odd-index products are units modulo five; odd and even exponents give the five-adic sum | Proved; kernel-checked private declarations and public result | odd_two_factor, a_odd_not_five, five_even_factor, five_odd_factor, five_Q_even, five_Q_odd, five_a_even, and the second through fourth conjuncts of result. | | The factorial bridge identifies the odd-exponent sum with signed A127428 at every natural $r$, zero included | Proved; kernel-checked private declarations | S_factorial and S_eq_b identify $\sum_{j=0}^{r-1}(1+v_5(2j+1))$ with $b(r)$. | | Independent source and bounded arithmetic checks | Computed; exact integer computation | Experiment entry below: source fidelity 15/15 and 31/31; C.1 $N=0..400$, C.2 $n=0..199$, C.3 $n=0..100$, C.4 $n=0..99$; 5,000 lifting checks and 202 factorial bridges. | | General base-$q$ square classifications, other-prime formulas and source asymptotics | Open | Outside the four-conjunct claim; no new theorem for these questions is asserted. |

The mechanism separates the central power of two from paired square factors and from the odd-exponent five-adic sum. The universal proof includes both even residue classes and the empty auxiliary product at zero. No dependence of another source result on these conjectures was identified in the entries read; the source's asymptotics are neither used nor proved here. General-base and other-prime extensions require separate statements and evidence.

Independent computation

Experiment directory at commit b4f84ca0a42162a9c908249b6eb8404cc1eef3b0. The immutable script is docs/reports/hanna-a369673-square-five-valuation/check.py. Its SHA-256 is a1fa74176981b716e44064edd4758158d7f7dc3e2614904a937bdac54261257b. Command: python3 /Users/auric/.sshx/deaa86554f498a91affdfc6b/attempt-1/stageb/check.py, using the byte-identical script extracted from that commit; exit 0, final result ALL_CHECKS_OK. The script uses exact integers and integer square roots. It reproduces 15 A369673 values and 31 A127428 values; checks C.1 at $N=0..400$, C.2 at $n=0..199$, C.3 at $n=0..100$, C.4 at $n=0..99$; both pairings at every product index through 400; the lifting formula at $j=1..5000$; and the factorial bridge at $r=0..201$. These are finite checks, separate from the universal proof.

Literature completeness and an exhaustive novelty determination remain unverified. The partial screen and inaccessible discovery channels are recorded in #21915. The escape audit remains unfinished under #22235. No general-base classification, other-prime formula or asymptotic conclusion is included.