Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Metadata 
bibkey: oeis2026a387319
authors: OEIS Foundation Inc.
year: 2025
title: OEIS A387319
doi: null
url: https://oeis.org/A387319
claim: A multiple-of-three residue coincidence characterizes composites except 4, 8, 10, and 25.
strata_touched:
  - D5/S3/Arith/Congruence/MultipleOfThreeCoincidence
license: citation-only
triage: anchor

OEIS A387319

Provenance and preregistration

The record through “Declaration shape and admission” is inherited from the first implementation worker, whose Lean checkpoints are commits 37cfd58620 and 5594455426. Commit 25f37ff59e preserved its unfinished documentation. Statements below attributed to “this worker” in that inherited record refer to that first worker. The continuation’s independent checks are separately recorded in “Continuation verification”; no independent review is implied by either worker’s implementation self-checks.

Skill context: lean4. One Codex implementation worker in the caller’s consensus-rnd:sshx implementation attempt; no independent review or model diversity is claimed here. Fixed source: e7e63c615460da48effcb4a76f96a3a6730af75d. The caller reports independent enumeration at k=1..3000, with zero differences between the exact predicate below and the proposed classification. The triage worker reports k=1..5000. These are separately attributed reports, not this worker’s measurements or a kernel proof.

The explicit brief and oeis2026triage0909.md (A387319 row and paragraph) preregister the first-tier OEIS conjecture. The exact target is Coincides k ↔ 1 < k ∧ ¬Nat.Prime k ∧ k ∉ ({4,8,10,25} : Finset ℕ), where Coincides k := ∃ m : ℕ, 6 ≤ m ∧ m ≤ k ∧ 3 ∣ m ∧ 3 * ((2*k) % m) = m * ((2*k) % 3). There is no cutoff and no extra hypothesis. No atom was supplied; this brief is the source obligation.

Before implementing new content, attempt closure from pinned Mathlib and frozen declarations. If successful, report bind-only and create no module. Otherwise the proposed escape witness is the divisor/residue criterion: writing m=3t, the equality is equivalent to t dividing 2k and (2k/t) % 3 = (2k) % 3, with 2≤t and 3t≤k. For 3 not dividing k, the residue condition is equivalent to t%3=1 (under that divisibility). This criterion is to be used in the live construction and prime exclusion. The planned witnesses are t=2 for multiples of 3; t=4 for remaining even composites; and t=p or 2p for odd composites, with p the least prime factor. The bound in the last branch requires separating k=25 explicitly. This is a proposed proof route, not an already verified theorem.

Verified locator

  • URL: https://oeis.org/A387319
  • Complete entry opened on 2026-09-09: revision 69, November 10, 2025.
  • Machine-readable URL: https://oeis.org/search?q=id:A387319&fmt=json
  • Independent HTML source: https://oeis.org/A387319/internal
  • The first comment explicitly calls the classification a conjecture. Its empirical verification to 10^5 is an OEIS author report.

The entry’s separate assertion that even k first coincides at m=12 is false as written: k=6 coincides at m=6, both fractions being zero. This ancillary observation is not the selected classification. The A343311 sequence-equality conjecture is also outside this implementation.

Initial evidence

The first command after reading the repository instructions was make lean-cache-ensure, exit 0: status=present, mathlib/project=warm, mathlib_missing_olean_files=0, clonefile_attempts=0, stamp_miss=null, pin_sha256=sha256:6c4c682ffba051b5744fe7a75ccc99d7f3b20227b3b026f392f3315be0adaa4e. No cold-tree Lake invocation occurred. Lean is v4.33.0 and Mathlib is pinned at db584cd6d46c92f209a44c0f1c829460d327499d.

Read the exact signatures of Nat.not_prime_iff_exists_mul_eq (Mathlib/Data/Nat/Prime/Basic.lean:85), Nat.minFac_sq_le_self (Mathlib/Data/Nat/Prime/Defs.lean:368), and Nat.Prime.dvd_mul (same file:422). These supply factors, a bound and prime divisibility, but do not state a residue coincidence characterization. Frozen D5/S3/Arith/EuclidLemma is the direct Mathlib wrapper; D5/S3/Arith/PrimeFactorization gives a list of prime factors. Neither identifies the residue predicate.

git ls-tree origin/dev --name-only D5/S3/ confirms the registered Arith domain. The existing Congruence subdirectory has 18 Lean files and its Blueprint mirror has 36 raw files at the fixed baseline. The actual SL-003 count excludes generated Markdown: Congruence has 18 counted sources on each side, growing to 19. The Arith Blueprint root’s raw count of 48 is 24 counted sources, not an exhausted bucket; the initial raw-count-based capacity interpretation was wrong. Congruence remains the natural existing subdirectory for this modular theorem. Problems is excluded from directory capacity by its canonical slug-path rule. No new domain or subdirectory is needed.

Unclaimed

No exhaustive search, universal absence of published proofs, mathematical novelty, priority, independent review, or larger-conjecture consequence is claimed. The triage worker’s direct-reference audit and enumeration, and the caller’s enumeration, remain attributed reports except where independently checked below. No downloaded b-file is used as a proof. Results of the Lean probe, supplementary literature search and repository gates are recorded below.

Bind-only and supplementary literature audit

The clean bind-only probe (bind-only-clean.log, exit 1) imports Mathlib and the two frozen arithmetic wrappers, then tries exact? and definitional simplification. It leaves the complete existential/classification equivalence unsolved. The earlier probe also contained a nonexistent diagnostic name Nat.dvd_prime_mul; the clean rerun removes it, so the residual goal is not attributed to that lookup error. This is an unsuccessful concrete attempt, not a proof that all possible bindings fail. The inspected scope contains no matching characterization; new divisor and bound arguments are necessary in the proposed route. Candidate discovery used D5 and pinned Mathlib Nat/number theory keyword searches, followed by reading the named declarations. Public GitHub Lean code searches for A387319, "coincident" "mod", and "coincidence" "fraction" (limit 30 each) returned zero paths. No third-party dependency was added and search exhaustiveness is not claimed.

Independently reread the complete primary entry and the relevant fields of A343311 (rev. 11), A387426 (rev. 107), and A389863 (rev. 29). All three still label their related claims conjectures. Their new direct references beyond the triage set are A343270 (rev. 5) and A100484 (rev. 137); both complete JSON entries were opened. A343270 gives a finite sum for three-part partition counts, not the residue classification. A100484 describes doubled primes. Its linked MathWorld Semiprime article concerns products of two primes and their counting/function identities, not equality of the present fractions. Lanterman’s linked paper, arXiv:1210.2991, was downloaded (14 pages): the inspected definitions and Theorems 1-11 classify irreducibles under congruent factorization relations, with units ±1 allowed. This is a different predicate; no identification with the positive bounded divisor criterion is supplied in those passages. The Anderson–Frazier DOI landing page returned an Incapsula block, so that paper is not claimed read. No proof of the selected target was found in the inspected passages. This scoped finding permits proceeding under the caller’s proof-versus-conjectural-restatement rule.

Network limitations: Python urllib initially received four HTTP 403s; curl retrieved the entries successfully. Google returned a challenge, and Bing’s exact-A-number query returned an irrelevant result; neither is evidence of absence. The first HTML text extractor mishandled escaped inequalities; it was replaced with HTMLParser and the source was reread against full JSON. PDF extraction required a temporary pypdf install and emitted font-encoding warnings; only the legible passages above are claimed inspected. No exhaustive recursive traversal of the doubled-prime reference graph is claimed.

The first Lean fragment compiles with zero diagnostics (fragment-1.log, exit 0): the exact divisor/quotient criterion and its modulo-one construction helper are proved. The proof uses the positive factor t explicitly, so no zero denominator or division-by-zero case enters the criterion. The main classification is not yet claimed at this checkpoint.

The complete classification now compiles with zero diagnostics (fragment-2b.log, exit 0). The first full fragment had two unhelpful multiplication/division simplifications and multi-location normalization errors after a contradiction already closed the goal; removing the redundant simplifications and normalizing the whole context repaired these tactic errors. The mathematical statement and route were unchanged. The public result quantifies over every natural k, including 0 and 1. No sorry, custom axiom, strengthened hypothesis, or finite cutoff was introduced.

Independent worker Python enumeration at k=0..5000 found zero classification mismatches and zero divisor-criterion mismatches for all 2≤t≤k/3. This uses an independently generated prime sieve and direct modular arithmetic; exact Fraction examples were also calculated. At k=14, m=12 gives 4/12=1/3, matching m=3. At prime k=13, the eligible fractions at m=6,9,12 are 1/3, 8/9, 1/6, all different from 2/3 at m=3. At composite k=25 the eligible fractions are 1/3, 5/9, 1/6, 1/3, 7/9, 8/21, 1/12, all different from 2/3. At k=6, both fractions at 3 and 6 equal 0; this genuine zero-valued coincidence must be included. k=0,1 give false on both sides. The finite checks are evidence only, not frozen numerical results.

Declaration shape and admission

The sole public theorem is classify. proof_shape: content; admission_basis: escape-witness; added_hypotheses: []; direct_frozen_dependencies: []. The final module imports only pinned Mathlib, so no external repository GID or frozen statement_id is a proof prerequisite. The frozen wrappers were inspected during the binding search, not imported by the new module.

The preregistered escape content is the divisor/quotient characterization coincides_iff_divisor, proved through residue_factor_iff, and its use in the explicit t=2,4,p,2p construction in coincides_composite. The four clause-3.2 obligations are assessed as follows:

  1. Dependency closure: classify consumes coincides_composite and not_coincides_prime; both consume coincides_iff_divisor. The criterion consumes residue_factor_iff. A symbol-level elaborated audit below checks these edges rather than inferring them from an import or a name.
  2. New content: the inspected frozen and Mathlib declarations provide prime facts and general modular identities, but not the admissible divisor classification. Extracting the factor from the remainder equation and constructing a divisor subject to both the residue and size constraints are new obligations on the actual target path. In particular the least prime bound must be combined with the residue split and the k=25 exclusion to produce the witness 2p. The failed binding probe alone is not a proof of nonderivability; this judgment rests on the unfolded construction.
  3. Different statement: the intermediate characterizes a fixed remainder equation by divisibility and quotient residue. It does not assert prime or composite membership, nor the four-element exceptional set, and is not definitionally the public classification.
  4. Live use: the prime exclusion consumes the divisor and quotient facts; sufficiency uses the reverse criterion to turn each constructed t into the actual modulus m=3t. These values feed the existential conclusion, with no discarded conjunction or dead helper used for admission. Generic factorization alone leaves that conversion and the bounded construction unproved. Constant-edge checks establish reachability; nonprojection and live semantic use remain review judgments, not a machine classifier.

computational_content.kind: none: the definition and all theorem declarations concern unbounded natural arguments. Finite base cases are internal branches of the general classification. No independent bounded enumeration, certified positive instance, checker, or numerical-reduction result is deposited. The other utility fields are not-applicable(kind=none). question_answered is the exact OEIS predicate classification preregistered here before the first proof fragment; dominating_theorem_search: not-found-in-searched-scope as detailed above.

Continuation verification

On 2026-09-09 a second Codex implementation worker, using lean4, continued the same lane/math/a387319-coincident branch. The four supplied commits were present and the worktree was clean. Current dev 74e9341e5e merged without conflicts as 2950fbe974; the original proof bytes were retained. This is serial continuation and implementation self-check, not a separate review vote or a claim of model diversity.

The continuation independently retried the exact target using only Mathlib and the frozen EuclidLemma and PrimeFactorization modules. exact? and simplification left the entire existential/classification equivalence unsolved (bind-only.log, exit 1). No new A387319 theorem was imported by that probe. The named Mathlib declarations and both frozen wrappers were reread. Public GitHub Lean searches for A387319 and "coincidence" "fraction" returned no paths (limit 30 each, exit 0). These are scoped unsuccessful searches, not a nonderivability proof.

The primary OEIS JSON and internal HTML were fetched again. Revision 69 still explicitly labels the target a conjecture. All five direct A-number references were fetched: A000040 (1398), A002808 (351), A343311 (11), A387426 (107), A389863 (29). The three related conjectures remain labelled as such. A343270 (5) and A100484 (137) were also fetched; their statements concern partition counts and doubled primes. The continuation downloaded Lanterman’s 14-page paper again and read Definitions 1-4 and Theorems 5-11: the signed-factorization predicate allows units and negative factors and does not supply this positive bounded-modulus classification. PDF extraction warned about missing fontTools; only the legible passages are claimed read. The first worker’s wording “Theorems 1-11” should be read as the numbered definitions and results through Theorem 11, not eleven theorems. No proof of this target was found in these inspected sources. The earlier Anderson–Frazier access failure remains an inherited limitation, not a fresh access measurement by the continuation.

Independent continuation enumeration used trial division through isqrt(k) for primality, rather than the first worker’s sieve, and checked every k=0..5000 directly against the original cross product: zero differences. The divisor criterion was separately compared on all 4,160,835 eligible (k,t) pairs: zero differences. Exact Fraction controls confirm k=14,m=12 gives 1/3 on both sides; k=6,m=6 gives zero on both sides; k=13 has no match; and all four exceptional composites have no match. For k=0,1 both logical predicates are false. These are this continuation’s own readings, not the caller or triage worker’s reports, and do not replace the unbounded proof.

The attempt-local receipts live under /var/folders/wv/ht3wzsj138b4sxl3q4t0xdr40000gn/T/consensus-rnd/sshx/a387319-cont2-0909/attempt-3/. They include bind-only.log, search-receipts.txt, fetched source files, and numeric-verification.json. The prior fragment logs were located under the sibling a387319-impl-0909/attempt-1 directory and reread; they contain no diagnostics. Fresh compilation and repository gate results are recorded below; the inherited logs alone are not used to claim them.

Fresh continuation compilation is now verified. make lean-cache-ensure returned exit 0, status=present, both layers warm, stamp_miss=null and mathlib_missing_olean_files=0. The source-minus-olean count was 3 before merging dev and 19 after merging it, so warmth was not treated as validity. The supplied serial fallback completed built=19 failed=0 missing=19, exit 0. Subsequent make lean completed all 12,798 jobs, exit 0, in 8.22 s on this warm macOS ARM tree (this timing excludes serial prewarming). /usr/bin/time -l reported maximum resident set size 1,064,419,328 bytes; this is the command’s RSS reading, not an aggregate host peak.

The unchanged A387319 source was independently elaborated with lake env lean D5/S3/Arith/Congruence/MultipleOfThreeCoincidence.lean after ensure, exit 0 with zero diagnostics (fresh-module.log). A separate Lean metaprogram uses getConstInfo, theorem value?, and Expr.getUsedConstants to inspect actual proof constants (SymbolAudit.lean, symbol-audit.log, exit 0). It confirms classify -> coincides_composite / not_coincides_prime -> coincides_iff_divisor -> residue_factor_iff, as well as the mod-one construction helper’s criterion dependency. #print axioms reports exactly propext, Classical.choice, Quot.sound. The printed target is the unrestricted forall-k statement above. A first scratch audit used the reserved token prefix as a local name and failed to parse; renaming that scratch variable repaired the audit, with no theorem change. Its failure log is retained separately. Constant reachability is machine checked; the assessment of live, non-bind-only mathematical use remains the implementation worker’s semantic self-check.

The first continuation make lean-report attempt did not pass. No local cached report matched producer 89aef18ce098f3931b3873cc7953ad7496ea257cc78259cd8152ac83cfab7b28, so its plan was mode=fallback, not a small delta. The own inspector’s observed RSS reached 9,656,384 KiB; the continuation sent it SIGTERM before continuing with a report seed. The command returned exit 2 and its maximum RSS reading was 10,363,797,504 bytes. This is a deliberate stop recorded in make-lean-report-full-stopped.log, not an inferred host-kill diagnosis or a successful gate. The existing recovery path is to fetch the canonical report from successful dev CI run 34363934206 (dev 74e9341e5e), validate it with tools/scripts/report/lean-report-ci-baseline.sh, and rerun the same make lean-report producer against that seed. No report provenance is manually substituted and no detection is relaxed.

The recovery completed successfully. The downloaded candidate report’s SHA-256 was verified before staging it under the canonical basename; only the filename in its SHA sidecar was normalized, with report, attestation and provenance bytes preserved. The existing baseline validator returned status=ready. The second make lean-report returned exit 0, mode=delta changed=0 added=1 removed=0 recheck=1, in 60.81 s; its maximum resident set size was 3,913,318,400 bytes (make-lean-report.log). The report hash is sha256:e28b1d810091361e9a4cf1767fd3655066ec07a6e6ca0681bfb4c0f0ab9fd384. It records the unchanged source hash and the standard three-axiom closure. The public classification’s statement identity is sha256:1bbe1e5377afb6142c20ec1c05401abc422ae469662570631eda3d26d9b60557.

ledger-align --add returned exit 0 with selectors_considered=3912 changed=0 added=1 unchanged=3911 conflicts=0 (ledger-align.log). The new module state identity is sha256:62ba2110cc58637c85eb0af385e6a133d1efd620afa59725fee8e25c24940883; the accepted Freeze event is sha256:173afdb177fd30c7d9be81d28e6a584571dad5ac6ab773636c0a9f1a24cf5b89. There are no frozen prerequisites. No source atom was supplied, so no digestion coverage edge is claimed or added.

The first make emit rejected inherited Scribe token adjacency that would emit the invalid LaTeX control word \cdotk (make-emit.log, exit 2). The continuation inserted FormulaDsl.Sp between Cdot and the variable in TwiceK; the Lean source and statement remained unchanged. The second make emit returned exit 0 and emitted one changed Blueprint, including the frozen classify binding and the proved problem-resolution claim (make-emit-retry.log). This is the continuation’s verified repair of inherited documentation, not an inherited successful emission receipt.