Metadata

slug: h369673
bibkey: hanna2024a369673
doi: null
triage: theorem
motivation_gids:
  - D5/S3/Arith/FactorialRatio/HannaA369673.result
url: https://oeis.org/A369673/internal

Hanna’s A369673 square classification and five-adic orders

Problem

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 ∤ N$ .
(C.2) $5 ∤ a (2 n + 1)$ .
(C.3) $v_{5} (a (4 n)) = 2 b (n)$ .
(C.4) $v_{5} (a (4 n + 2)) = 2 b (n + 1)$ .

Here $b (n) = v_{5} ((10 n)!) - v_{5} ((5 n)!)$ 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.

Motivation

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.

Gap

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.

Route

Equal boundary factors give the two-step recurrence $a (N + 2) = 2^{N + 1} (1 + 2^{N + 2})^{2} a (N)$ . For $Q (m) = \prod_{j = 1}^{m} (1 + 4^{j})$ , induction gives $a (2 m) = 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$ .

Falsifier

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.

Evidence

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.

Triage

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})^{2} a (N)$ and $a (2 m) = 2^{m^{2} + 1} Q (m)^{2}$ .
$Q (m)$ is positive and odd, $v_{2} (a (2 m)) = 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} (2 j + 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.

ASSUMED-UNVERIFIED

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.

Keyboard shortcuts

trureturing — Discovering truth