Bala's A295462 binary-spacing parity conjecture

Peter Bala's OEIS A295462, native record #19, defines $a(n)=(15n)!(2n)!/((10n)!(6n)!n!)$ and states in its REFERENCES (%D) field:

Conjecture: a(n) is odd iff the 1 bits in the binary expansion of n are separated by at least three 0's, that is, iff n belongs to A048718.

The offset includes $n=0$. The rational quotient is interpreted by exact division; its natural realization is explicit before oddness is tested. Preregistration #22428 fixes the statement and conventions.

Statement echo

| Source clause | Lean counterpart | Fidelity | | --- | --- | --- | | The displayed factorial quotient | a | All five natural factorials are cast to $\mathbb Q$; division is exact. | | Every natural index, including zero | claim | Universal natural quantifier, with no added hypotheses. | | The quotient is a natural integer | claim | A natural witness realizes the rational value. | | Odd iff at least three zero bits separate ones | spacedBits, claim | Every occupied pair $i<j$ satisfies $i+4\le j$, in both directions of the iff. | | Conjecture holds | result | The entire claim, without additional premises. |

The names belong to D5.S3.Arith.FactorialRatio.BalaA295462Parity. The dropped or weakened clause set is empty. All-pairs spacing is equivalent to successive spacing: the forward implication restricts to successive positions; the converse follows by ordering the occupied positions and adding successive gaps.

The settling GID is D5/S3/Arith/FactorialRatio/BalaA295462Parity.result. The admission basis is open-problem-resolution (#22428; Proved), generality is I, and utility is none. The retained assertions are unbounded symbolic statements; the finite floor reduction is internal arithmetic, with no retained standalone finite positive-instance certificate. There is no anchor atom.

The primary source explicitly labels the assertion a conjecture. The bounded literature screen in #22428 found no settlement of this exact parity iff. Bober's integrality classification, arXiv:0709.1977v1, Table 2 row 32, contains the ratio $[15,2]/[10,6,1]$ and establishes integrality, not the binary iff. Delaygue's arXiv:1310.4131v2, Theorem 3, requires a floor-function positivity condition that fails here at $x=1/2$. Guo's arXiv:1312.7548v2 concerns a different sequence. The inspected later factorial-ratio texts and public result packet concern integrality or primes at least five. The inspected A048718 attachment assumes the sparse-bit language and gives XOR identities, without this quotient's parity converse. Literature completeness is ASSUMED-UNVERIFIED.

Write $$F(x)=\lfloor15x\rfloor+\lfloor2x\rfloor-\lfloor10x\rfloor-\lfloor6x\rfloor-\lfloor x\rfloor.$$ The imported OeisA347854BalaHalfIndexIntegral.mul_div_reduce and grid_floor reduce the floor expression to thirty residue cells. Private defect_bounds shows every summand is zero or one. The imported OeisA347854BalaHalfIndexIntegral.factorial_prod_dvd_of_floor supplies the factorial divisibility used by private denominator_dvd; private quotient_natural realizes a nonzero natural quotient.

Private quotient_valuation expresses its binary valuation as the finite sum of the floor defects. Private sparse_sum_bound proves $$15\sum_{i\in s}2^i<2^e$$ for every finite four-separated support $s$ whose elements satisfy $i+4\le e$. Private tail_bound applies this estimate to the lower occupied positions. Private sparse_defect_zero makes all summands vanish for separated support. When spacing fails, private first_bad_pair chooses the lowest bad pair and gives $$n\bmod2^{t+1}=2^t+2^e+R,\qquad e<t<e+4,\qquad15R<2^e.$$ Private bad_interval computes the corresponding symbolic floor defect for each gap $1,2,3$; private bad_defect_witness supplies a summand equal to one. The nonnegative valuation sum and private odd_iff_valuation_zero complete result. These are descriptions of the named compiled helpers, not additional public theorems.

A natural index at which exact integrality or either direction of the parity iff fails would contradict result. No finite search establishes the unbounded assertion. The zero index remains in scope.

The source is D5/S3/Arith/FactorialRatio/BalaA295462Parity.lean; its Blueprint shows the complete public definitions and settling proposition. The sole public theorem is D5.S3.Arith.FactorialRatio.BalaA295462Parity.result. Its four-slot escape audit is unfinished at issue #22536: there is no retained Reg mirror or compiled dependent-family realization, reconstruction, intervention/sensitivity and observational-dependence evidence. No declared_validated registration is claimed.

The exact experiment is the pinned experiment directory. The script was extracted without alteration from that commit and run as python3 /tmp/op-bala295462/check.py, exit 0; its SHA-256 is 80f595cb2bc73a6bf05045e5ece0ede3438d73486ec684761558beb6c008c0ec. It reproduces all twelve published values ($n=0,\ldots,11$), checks exact recurrence values, both source divisibilities and parity through $n=4095$ (69 odd indices), independently compares factorial/Fraction values through $n=256$, and checks valuation/digit-sum/spacing agreement through $n=65535$ (250 sparse indices; first-bad-gap counts 37338, 18644, 9304). It also checks the thirty-cell table and three rational intervals, and ends with ALL_CHECKS_OK. These ranges are finite computation evidence.

1. Proved; kernel-checked helpers: defect_bounds makes every summand nonnegative, sparse_defect_zero makes all zero under spacing, and bad_defect_witness gives one summand equal to one for a first gap of length one, two or three. They are consumed by result.
2. Proved; kernel-checked: result covers every natural $n$, including zero, with exact rational division. Private quotient_natural additionally proves the natural witness is nonzero. No positivity hypothesis is imposed on $n$.
3. Proved; kernel-checked helper: sparse_sum_bound proves the stated strict bound for every finite four-separated support and every permitted cutoff $e$.
4. Computed: the experiment entry gives the fixed commit, command, exit 0, script SHA-256, ALL_CHECKS_OK, and the exact scopes $n\le4095$, $n\le256$ and $n\le65535$. It is not a uniform extension by computation.
5. Open: a general classification for other factorial ratios or other spacing lengths is not established by this delivery.
6. Proved in the cited source; literature reading: Bala's three-page note proves that $a(n)/(10n+1)$ and $a(n)/(6n+1)$ are integers for every natural $n$. The full-note reading is recorded in #22428. These prior ordinary mathematical proofs are independent of this parity settlement; no new Lean proof is claimed.

What the settlement shows

The decisive kernel-checked mechanism is the strict lower-tail estimate and the lowest bad pair: spacing annihilates every nonnegative valuation summand, whereas the first gap below four forces one summand to be positive. The finite-support estimate holds independently of whether the support is the whole binary expansion. The universal theorem includes the empty support and requires no relaxed domain or exceptional positive-index case. Broader ratios and spacing lengths remain open. The inspected Bala note has no result depending on the parity conjecture; its two divisibility statements retain their independent source proofs.

Completeness of the external literature screen is ASSUMED-UNVERIFIED: OpenAlex citation enumeration, complete Zenodo author pagination, general-web exclusion and exhaustive external result-dataset exclusion were not obtained. No global novelty claim follows from the bounded searches in #22428. The four-slot escape registration remains unfinished at #22536.