bibkey: oeis2026a388986
authors: OEIS Foundation Inc.
year: 2026
title: OEIS A388986
doi: null
url: https://oeis.org/A388986
claim: Every Euler-form number in A228058 is conjectured to satisfy the unitary-plus-squarefree divisor-sum inequality.
strata_touched: []
license: citation-only
triage: anchor

OEIS A388986

Provenance and preregistration

Skill context: lean4. One Codex implementation worker in the caller’s consensus-rnd:sshx implementation stage performs the source reading, numerical checks and Lean work. No independent review or multi-model consensus is claimed by this worker. Baseline: e7e63c615460da48effcb4a76f96a3a6730af75d; branch lane/math/a388986-euler-form.

The caller’s target is the exact A228058 inclusion question. For natural p,a,r with p prime, p % 4 = 1, r odd, r > 1 and gcd(p,r)=1, put N=p^(4*a+1)r^2. Define U(N) as the sum of divisors d of N satisfying gcd(d,N/d)=1, and S(N) as the sum of squarefree divisors of N. Prove U(N)+S(N)<2N. All normalized calculations take place in the rationals; N is positive under the hypotheses. There is no sequence-index shift.

Before any Lean implementation, the proposed escape witness is the triage finite-product bound: for a finite set F of integers q >= b > 1, product (1+1/q^2) <= b/(b-1). The live route splits the prime support of r into: no 3; only 3; 3 and another prime. The source divisor sums must be connected to their actual prime-power products. This is a first-tier small OEIS question, conditional on the literature and bind-only checks below.

Verified locator

Canonical URL: https://oeis.org/A388986

Opened the complete text entry https://oeis.org/search?q=id:A388986&fmt=text on 2026-09-09: revision 36, May 19 2026. The COMMENTS field says:

Question: Is A228058 a subsequence? See the graph of A389217.

The NAME field defines the strict inequality for the sum of unitary and squarefree divisors. The FORMULA field is {k | A034448(k)+A048250(k) < 2*k}. The PARI code gives the exact products prod(p^e+1) and prod(p+1). A228058 revision 45, November 5 2025, defines odd p^(1+4k)*r^2 with p prime congruent to 1 modulo 4, r>1 and gcd(p,r)=1. Its claim that odd perfect numbers belong to A228058 is a different theorem.

Initial checks

CLAUDE.md was read completely, together with agents/CONTEXT.md and the A388986 row and paragraph of Library/Words/oeis2026triage0909.md. make lean-cache-ensure was the first build command; receipt pending. Pinned Mathlib is db584cd6d46c92f209a44c0f1c829460d327499d, Lean v4.33.0.

ASSUMED-UNVERIFIED

The triage seat reports reading the main entry and its 15 direct A references; that reading is attributed to the triage seat, not independently claimed here. Its million-bound numerical check and prime-support counterexample 240 are being independently checked in this attempt. No exhaustive search, priority, absence of proof everywhere, Lean closure, frozen status, or larger odd-perfect-number conclusion is claimed at this preregistration checkpoint.

Independent numerical evidence

attempt-1/numeric.py uses smallest-prime-factor factorization and an independent divisor sieve: for each d dividing N it separately tests gcd(d,N/d)=1 and squarefreeness of d. All 1,000,000 positive N through 10^6 agree with both prime-product formulas (zero mismatches). Of these, 12,941 are Euler-form instances: no 3 in r: 5,905; only 3: 6,104; 3 and another prime: 932. All satisfy both proposed class bounds and U+S<2N. Maximum observed (U+S)/N is 28/15, attained at N=45.

Positive nonempty witness: p=5,a=0,r=3,N=45,U=60,S=24,2N=90. Negative control: p=5,a=0,r=1,N=5,U=6,S=6,2N=10. Only r>1 fails, and the conclusion fails. Three-class witnesses are respectively N=245 (300+48<490), 45 (60+24<90), and 2205 (3000+192<4410). Browne’s support interpretation first differs at 240: U=408,S=72,2N=480; rad(240)=30 divides 210<240, whose support includes the additional prime 7. The sibling interpretation is not the implementation target.

Binding and literature checks

The scratch bind-only probe unfolds the actual two sums, tries direct exact?, simplification, and omega. It does not close the inequality; omega leaves both filtered sums unconstrained. One exploratory #check used an unavailable lemma name; that diagnostic is separate from the failed main-goal closure, and is not evidence of mathematical impossibility. The two Mathlib sigma declarations cited by triage were #checked at the pin: they sum all divisor powers. Nat.sum_divisors_filter_squarefree supplies the powerset parametrization for S. Source searches in D5 and pinned NumberTheory locate no unitary-divisor inequality theorem. D5’s existing PrimeGaps/EulerProducts has weighted sieve-coefficient estimates, with different functions and hypotheses. Third-party GitHub code search for "unitary" "divisors" language:lean returns algebraic-unitary definitions and unrelated number-theory files; no exact target was found in that scope. This is not a proof of bind-only impossibility or search exhaustion.

Supplement beyond the triage seat’s 15 direct A entries: read Finch’s full nine-page Unitarism and Infinitarism, cached at https://oeis.org/A007947/a007947.pdf. Section 0.1 proves the unitary and squarefree divisor parametrizations; section 0.2 concerns asymptotic means and reciprocal sums. It does not prove the Euler-form sum inequality. Read all six pages of Tim Trudgian’s The sum of the unitary divisor function, Publications de l’Institut Mathématique 97(111) (2015), 175–180, https://doi.org/10.2298/PIM140617001T, from the DOI page’s linked full text. Theorem 1.1 bounds U(N) by 1.3007Nlog(log N) for N>=570571; the later results concern exponential divisors. None states the present joint bound. The known prime-product formulas in A034448/A048250 are published facts; the target inclusion in A388986 remains a question in the source.

Google and DuckDuckGo requests returned browser/bot challenges; a Bing RSS request returned unrelated results and was discarded as search evidence. An attempted arXiv identifier was checked against its PDF title, found to be an unrelated Neretin paper, and discarded; it is not a Trudgian source. No search-complete or priority claim is made.

Cache and location

The first build command was make lean-cache-ensure. Its receipt was status=fetched, method=cache-get, stamp_miss=missing, clonefile_attempts=0, mathlib_missing_olean_files=0, project_olean_state=warm, mathlib_olean_state=warm. The pre-existing .lake lacked a producer stamp; the canonical ensure producer repaired it in place. A subsequent ensure returned status=present and both layers warm; full JSON is in attempt-1/cache-present.log. No cold-tree bare Lake was run. git ls-tree origin/dev --name-only D5/S3/Arith/ returned 41 direct entries; Arith is already registered for elementary prime-factorization arithmetic. The new file brings this directory to 42 entries, below SL-003’s 48 limit.

Lean checkpoints

The finite reciprocal-square product bound compiled without diagnostics (fragment-1b.log) and was committed as a21c1d41a4. The proof uses minimum induction with the lower bound shifted to q+1; this is an equivalent finite route to the preregistered telescoping estimate, with no infinite product. The first attempt left a (q-1) denominator; explicitly using its positivity before field_simp resolved that failure.

The second Lean fragment compiles without diagnostics (fragment-2d.log). For a unitary divisor d, coprimality identifies each exponent in d with the full exponent in N. The resulting map d -> primeFactors(d) is injective into the powerset of primeFactors(N), giving U(N) <= product(q^e+1). Only this upper bound is needed; no equality or surjectivity is claimed by that lemma. S(N)=product(q+1) reuses Mathlib’s squarefree powerset formula. Initial elaboration repairs were root namespace, a left-only rewrite of d, and the List-to-Multiset coercion; the final check has no diagnostics.

The third fragment compiles without diagnostics (fragment-3b.log): a nonempty finite set of integers >=3 excluding 4 satisfies product(1+1/q^2)+product((q+1)/q^2)<5/3. The proof explicitly handles F={3}, F containing 3 and another member, and F excluding 3. It consumes the reciprocal-square bound and a one-selected-factor bound for the second product. This is the triage three-class route; no numeric enumeration is used by the Lean proof.

Continuation verification (2026-09-09, attempt-2)

This continuation starts at fcd1fdad16 on the same branch and worktree. The four inherited commits above were present and the worktree was clean. One Codex worker using lean4 performs this continuation; no independent review or model diversity is claimed. The preceding sections describe the previous worker’s work, not new measurements by this worker.

The first build command was again make lean-cache-ensure, exit 0 in 16.628 seconds. Its receipt: status=present, method=none, donor=null, stamp_miss=null, clonefile_attempts=0, mathlib_missing_olean_files=0, archive_status=not_attempted, archive_skip_reason=project olean state is warm, mathlib_olean_state=warm, project_olean_state=warm. Full JSON is preserved in the runner-owned attempt-2/cache-ensure.log. No LAKE_JOBS setting is used.

Independent numerical verification in attempt-2/numeric.py recomputes both actual divisor sums by a divisor sieve, with gcd and an independent square-divisibility sieve, and compares them against SPF factorization products for every N=1..1,000,000. Exit 0, zero product mismatches; 12,941 Euler-form instances split 5,905 / 6,104 / 932, all three class bounds and the strict target pass. The maximum ratio is 28/15, uniquely at N=45 in this interval. Witnesses: N=45 gives 60+24<90; N=245 gives 300+48<490; N=2205 gives 3000+192<4410. The r=1 negative control N=5 gives 6+6>10. These readings independently agree with the inherited report; they are finite checks, not the proof of the universal statement.

The pinned-Mathlib-only exact-goal probe tries exact?, simp_all and omega; it fails with the two filtered sums unconstrained (attempt-2/bind-only.log, exit 1). The cited sigma declarations have been reread and concern all divisors, not the joint filtered-sum inequality. Current dev source search and a repeated GitHub Lean code search found no exact dominating result in the searched scope. This is not a proof that binding is impossible.

The complete inherited Lean file was reread and independently compiled by lake env lean D5/S3/Arith/EulerFormDivisorSum.lean, exit 0 in 2.814 seconds, with no diagnostics (attempt-2/inherited-lean.log). The reciprocal-product induction, unitary support injection, squarefree powerset identity, and all three finite-support cases are therefore rechecked in this session. Arith has 42 direct entries on this branch, below the 48-entry limit; no new domain or Problems chapter is introduced.

The new normalized-sums bridge compiles without diagnostics (normalized-1.log, exit 0, 2.436 seconds). It divides the actual sums by positive N, uses the prime-power factorization of N, and distributes division through each finite product. The unitary side remains an upper bound; the squarefree side is an equality. All exponents are those of N.factorization.

The complete current text entries for A388986 and all 15 direct A references listed in triage were downloaded and read independently in attempt-2. A388986 revision 36 still asks whether A228058 is a subsequence; A389079 and A389219 restate this as a conjecture. A048108 compares U+S with sigma, which does not give the Euler-form bound against 2N. The product formulas in A034448 and A048250 are known results, but no proof of the selected inclusion was found in these entries. The earlier worker’s two full-paper readings remain attributed to that worker until independently checked.

The exponent-comparison bridge compiles without diagnostics (support-2.log, exit 0, 2.956 seconds). A distinguished factor p>=5 with exponent at least one contributes at most 6/5 to each product; every other factor has exponent at least two. The live application of joint_products_lt then gives a strict bound below 2. An initial additive-order elaboration mismatch was repaired with explicit add_le_add; no statement or estimate was changed.

The exact public target euler_form_lt now compiles without diagnostics (final-theorem-2.log, exit 0, 2.968 seconds). Its signature preserves all five hypotheses and the actual natural-number sums. Coprimality separates p from the prime support of r; oddness excludes 2; primality excludes 4; factorization of the square gives every remaining prime exponent >=2. The rational strict bound is transported back using the proved positivity of N. Initial repairs were a Finset singleton-union rewrite and explicit decidable proof that 4 is not prime. Project gates, axiom inspection, Scribe, freezing, and PR merge are still pending at this checkpoint.

Continuation delivery checks

The two full papers have now also been independently downloaded and read in attempt-2: Finch’s nine-page Unitarism and Infinitarism and Trudgian’s six-page The sum of the unitary divisor function. The latter’s Theorem 1.1 is the U(N) <= 1.3007Nlog(log N) bound for N>=570571. Neither paper establishes the selected joint Euler-form inequality. This supersedes the earlier attribution-only status for these two readings, without claiming an exhaustive literature search or publication priority.

The precise SL-003 capacity count is 30 direct .lean files in D5/S3/Arith and 25 direct .scribe.cs files in its Blueprint mirror, including this addition. Generated Markdown and subdirectories are excluded from this file-cap calculation. The earlier 42-entry count included directories. Both counted pools are below 48; Problems has exactly the eight required sections and no new domain is introduced.

Before the full build, the warm-tree missing-olean list contained 11 modules, including this target. The canonical serial-lean.sh was absent on fetched dev, so the caller’s serial module-build form was used with the existing cache stamp, timeout 1200 per module, and no LAKE_JOBS. All 11 calls passed (serial-lean.log, exit 0, 252.050 seconds). The subsequent make lean passed (make-lean.log, exit 0, 19.415 seconds, 12782 Lake jobs), with the cache receipt still present and both olean layers warm. Replayed warnings belong to existing unrelated modules; no target diagnostic was reported. No build was killed in this continuation.

The independent scratch Checks.lean prints the exact public signature and its axiom closure: propext, Classical.choice, Quot.sound only. It proves the admissible p=5,a=0,r=3 hypotheses, computes U(45)=60 and S(45)=24 and 84<90, computes U(5)=S(5)=6 and not 12<10, and instantiates euler_form_lt at the positive witness. Ordinary decide and a simproc-based alternative failed to reduce the squarefree/factor-list computations; decide +kernel completes the checks with no native-decide axiom (axioms-witnesses-4.log, exit 0, 2.599 seconds). The failed scratch probes are preserved separately; the target theorem source was unchanged by these checks.

For the sole public theorem euler_form_lt: proof_shape=content; direct frozen D5 dependencies=[] (there are only Mathlib imports); escape_witness=reciprocal_square_product_le, the preregistered finite minimum-induction estimate, consumed by joint_products_lt, then support_products_lt, then euler_form_lt; admission_basis=escape-witness. The two other public declarations are the actual divisor-sum definitions. Utility is none: the delivered theorem is universally quantified, and is not a certified finite instance, enumeration, checker or numeric-reduction artifact. The finite numerical and nonempty-witness checks remain scratch diagnostics outside the delivered module.

The required project delivery sequence now passes: make lean (19.415s), make lean-report (55.475s), ledger-align –add (8.874s), and make emit (60.230s), all exit 0. The report contains 3947 modules; all 22 declarations of this target, including private and generated declarations, have only standard axioms, and its source hash matches the current file. The public theorem statement_id is sha256:94bfb76f8e74a9dfd858320409cd772c7069a422f681141e171e6ec4bf74db1f. The ledger considered 3896 selectors: changed=0, added=1, unchanged=3895, conflicts=0. It wrote this module’s state pin and its accepted Freeze event.

The first emit failed because StatementSource.FromLean had no display entry for the new unitarySum declaration. Following the existing Arith Scribe pattern, the three displayed formulas are now authored typed Formula ASTs, linked to the exact Lean handles; the Lean source was unchanged. The second emit passed and the generated Markdown was read back: both actual filtered sums, all five hypotheses, and the strict conclusion are present. Its resolution claim refers to the frozen euler_form_lt. No emitted Markdown was hand-edited. Full logs: attempt-2/lean-report.log, ledger-align.log, emit.log (failed probe), emit-2.log (successful delivery).

The first PR CI attempt failed its Canonical Lean report production job. The subsequent local preflight against the branch’s immutable starting baseline e7e63c615460da48effcb4a76f96a3a6730af75d reproduces one Scribe content finding: incomplete-library-locator. The verifier requires a literal Verified locator or Locator heading and the canonical URL within that section; the inherited heading was Verified source locator and only the text-search endpoint appeared in that section. The heading and URL are corrected above. This changes source-locator metadata, not the theorem, source reading, or proof. The failure and rerun remain recorded in attempt-2/preflight.log and the subsequent delivery logs.

Exact first-ensure receipt for this continuation:

{"status":"present","worktree":"/Users/chronoai/trureturing-cs0260-partial","donor":null,"method":"none","reason":null,"stamp_miss":null,"pin_sha256":"sha256:6c4c682ffba051b5744fe7a75ccc99d7f3b20227b3b026f392f3315be0adaa4e","clonefile_errno":null,"clonefile_errnos":[],"clonefile_attempts":0,"clonefile_cleanup_error":null,"mathlib_missing_olean_files":0,"mathlib_missing_olean_samples":[],"archive_status":"not_attempted","archive_mode":null,"archive_skip_reason":"project olean state is warm","archive_reason":null,"archive_producer_commit_sha":null,"archive_workflow_run_id":null,"mathlib_olean_state":"warm","mathlib_olean_probe_error":null,"project_olean_state":"warm","project_olean_probe_error":null}