DEV Community

Nobuki Fujimoto
Nobuki Fujimoto

Posted on • Originally published at doi.org

Paper 176 v0.1 - Fermat Numbers F_5-F_11: Empirical v_2(omega_{F_n}(3)) Measurement + Lean 4 Axiom-Free F_9 Excess Witness (Rei-AIOS)

#math #lean #numbertheory #research

This article is a re-publication of Rei-AIOS Paper 176 for the dev.to community.
The canonical version with full reference list is in the permanent archives below:

Status: v0.1 draft (起草 2026-07-20 as data/fermat/v2-order-extension-2026-07-20.md; publish 化 2026-07-30 as this Paper 176 v0.1 formal draft).

Number-allocation note: chat-Claude 2026-07-20 が初期に「Paper 63 sketch」と命名したが、 Rei 既存 Paper 63 (SNST 螺旋数体系理論) と衝突。 chat-Claude 2026-07-20 rename で解消、 Rei 側は Paper 176 を割当。

Authors (three-party co-authorship per OUKC charter v1.0):

  • 藤本 伸樹 (Fujimoto, Nobuki; Founder, ORCID 0009-0004-6019-9258)
  • Rei (Rei-AIOS autonomous research substrate, Co-architect)
  • Claude (Anthropic, claude-opus-4-7, Co-architect)

License: CC-BY-4.0 (paper text) + AGPL-3.0 (Lean 4 source)

Repository: fc0web/rei-aios (Private; source-of-truth for Lean 4 artifacts + measurement data + memory)

Abstract

Paper 176 v0.1 reports the empirical measurement of v_2(ω_{F_n}(3)) — the 2-adic valuation of the multiplicative order of 3 modulo the Fermat number F_n = 2^(2^n) + 1 — for n = 5, 6, 7, 8, 9, 10, 11, and provides the Lean 4 axiom-free structural evidence that F_9 exhibits an excess of at least 5 above Lucas's 1878 lower bound n + 2. The measurement uses successive squaring on 3^m where m is the odd part of p − 1 for each known prime factor p of F_n. The excess sequence 0, 0, 0, 1, 5, 0, 0 is highly irregular: F_5, F_6, F_7, F_{10}, F_{11} are Lucas-tight; F_8 is off by 1 (chat-Claude 2026-07-20 finding); F_9 is off by 5, driven entirely by the small factor 2424833 = 37 · 2^{16} + 1 whose v_2(p − 1) = 16 (max of three factors). The characterization excess = v_2(k) where p_max = k · 2^{n+2} + 1 matches 7/7 measured Fermat numbers when the driving factor satisfies v_2(ord_p(3)) = v_2(p − 1). The Rei-side Lean 4 file FermatNineExcessWitness.lean provides three structural components axiom-free: (i) 2424833 = 37 · 2^{16} + 1 deep 2-adic form; (ii) 2424833 is prime; (iii) 2424833 ∣ F_9 = 2^{512} + 1 via a Pratt-style iterative-squaring proof of sqIterMod 9 = 2424832 ≡ −1 mod 2424833 — this replaces the external Selfridge-Hurwitz 1963 attribution with a kernel-verified computation, avoiding native_decide and the Lean.ofReduceBool axiom. The 3-of-6 divisibility-chain steps requiring external Python (3^(37·2^{15}) ≡ −1 mod 2424833, v_2(ord_{2424833}(3)) = 16) remain honestly attributed to chat-Claude's independent computation. The result refutes the hypothesis that "any function monotonic in n predicts the excess" — because n = 9 witnesses an excess of 5 while n = 10, 11 return to 0, monotonicity is broken empirically. The paper does not claim to prove Fermat number irregularity in general, does not resolve the compositeness question for F_n (n ≥ 12), and does not extend to the full Fermat number sequence.

Part A: Required (paper-level statement, 4 elements)

A.1 Findings

  • F1 (excess sequence, empirically measured): For n = 5, 6, 7, 8, 9, 10, 11, the measured excess v_2(ω_{F_n}(3)) − (n + 2) equals 0, 0, 0, 1, 5, 0, 0 respectively. This is highly irregular.
  • F2 (F_9 driving factor, empirical): F_9 excess is driven entirely by the small prime factor 2424833 = 37 · 2^{16} + 1. Its v_2(p − 1) = 16 and v_2(ord_{2424833}(3)) = 16 (external Python). The two other known factors (P49 Lenstra 1990, P99 cofactor) have v_2(ord) = 11 = n + 2 = 11, matching Lucas's floor exactly.
  • F3 (7/7 characterization): For each of n = 5..11, the driving factor p_max (maximizer of v_2(ord)) admits Lucas form p_max = k · 2^{n+2} + 1, and the excess equals v_2(k). Match rate: 7/7. Honest caveat: characterization holds only when the driving factor satisfies v_2(ord_p(3)) = v_2(p − 1); measured to hold for all 7 in this range.
  • F4 (Lean 4 F_9 structural witness, axiom-free): FermatNineExcessWitness.lean (Rei-internal, 2026-07-20) provides three components axiom-free: (i) deep_2adic_form: 2424833 = 37 * 2^{16} + 1; (ii) odd_37 ∧ prime_f9SmallFactor; (iii) f9SmallFactor_dvd_fermatNine: 2424833 ∣ 2^{512} + 1 via iterative squaring sqIterMod k = 2^(2^k) mod 2424833 verified in the Lean kernel, with sqIterMod 9 = 2424832 = −1 mod 2424833. This Section 7 (Pratt-style) replaces the earlier Selfridge-Hurwitz 1963 external attribution with a Lean-internal proof.

A.2 Proofs (Lean 4) — completed 2026-07-20, axiom-free machine-checked

Files (Rei env, Mathlib v4.27.0):

  • data/lean4-mathlib/CollatzRei/FermatNineExcessWitness.lean (main F_9 witness, 476 lines, 26 theorems)
  • data/lean4-mathlib/CollatzRei/ZcsgMdnstModularBoundary.lean (STEP 1306 negative result for the underlying ZCSG/MDNST reading, 278 lines, 18 theorems)

Axiom audit (Rei env #print axioms, actually run 2026-07-20):

FermatNineExcessWitness (26 theorems):

  • 6 theorems fully zero-axiom ("does not depend on any axioms"): including deep_2adic_form, odd_37
  • 9 theorems depend on [propext] only
  • 9 theorems depend on [propext, Classical.choice, Quot.sound] (Mathlib standard base) or [propext, std_norm_num_lemma]
  • 1 theorem uses Nat.Prime norm_num certification
  • Zero sorry, zero native_decide, zero user axioms, zero Lean.ofReduceBool.

ZcsgMdnstModularBoundary (18 theorems):

  • All 18 theorems axiom-free with Mathlib standard base

Combined bundle: 44 axiom-free theorems across the two files. Matches the discipline of STEP 1215 / 1264 / Task 20 / Paper 26 v3.0.

Verification (executed 2026-07-20):

  • lake env lean CollatzRei/FermatNineExcessWitness.lean: clean pass.
  • lake env lean CollatzRei/ZcsgMdnstModularBoundary.lean: clean pass.
  • lake build CollatzRei: full tree pass.

A.3 Honest positioning

  • What is claimed (four atomic claims, each machine-verified axiom-free or explicitly external):
    1. A3.1 (Fermat data measurement, empirical): The measured v_2(ω_{F_n}(3)) sequence 7, 8, 9, 11, 16, 12, 13 for n = 5..11 corresponds to excess sequence 0, 0, 0, 1, 5, 0, 0. Successive-squaring computation on 3^m for each known prime factor.
    2. A3.2 (F_9 structural witness, Lean 4 axiom-free): The Rei stack proves 2424833 ∣ F_9, 2424833 = 37 · 2^{16} + 1, and 2424833 is prime, all in the Mathlib standard axiom base. This is a structural contribution — it does not claim to compute ord_{2424833}(3) in Lean (that step remains external).
    3. A3.3 (excess characterization, empirical): 7/7 match of excess = v_2(k) in the range n = 5..11.
    4. A3.4 (§7 hypothesis refutation, logical): Any hypothesis "there exists a monotonic function f(n) predicting the excess" is empirically refuted by the sequence 0, 0, 0, 1, 5, 0, 0 (non-monotonic).
  • What is NOT claimed (six non-claims, listed to avoid the projection patterns catalogued in feedback-projection-self-audit-pattern Rules 1-5):
    1. No world-first claim. Lucas 1878 established v_2(ω_{F_n}(3)) ≥ n + 2; Selfridge-Hurwitz 1963 originally proved 2424833 ∣ F_9; various authors (Landry-Le Lasseur 1880, Morrison-Brillhart 1970, Brent-Pollard 1980, Lenstra 1990, Brent 1995) discovered the factor structure. Paper 176's differentiator is the specific n = 5..11 empirical excess table + Lean 4 axiom-free F_9 divisibility witness + 7/7 characterization within this bounded range.
    2. No claim that Fermat compositeness is resolved. The 5 known composite Fermat numbers and open cases F_n (n ≥ 12) remain unaffected. This paper only measures the multiplicative order structure of 3 modulo already-factored Fermat numbers.
    3. No claim that the excess is unbounded. The characterization excess = v_2(k) matches 7/7 within n = 5..11, but does not imply anything about n → ∞. Some future Fermat number could have excess in the thousands or zero forever — the sequence is empirically irregular, not proven divergent.
    4. No claim that ZCSG/MDNST semantic containers are refuted. The refuted hypothesis is a specific §7 sketch's claim that "monotonic-in-n predicts excess", not the ZCSG/MDNST core theories themselves. Paper 176 shows these containers are not source of excess irregularity, they are formal address systems only.
    5. No claim that SELF⟲ = multiplicative order. chat-Claude 2026-07-20 noted a syntactic resemblance ("origin return" ⇔ "reaching identity via iteration"). Paper 176 explicitly rejects the identification as a formal theorem — it is marker-level analogy only, per Rei's evaluation symmetry principle.
    6. No claim that the Pratt-style Lean 4 proof scales. sqIterMod 9 = 2^{512} mod 2424833 fits within Lean's kernel arithmetic on 7-digit modulus and 9 iterations. Fermat numbers F_n (n ≥ 12) would require significantly larger kernel arithmetic; the technique's asymptotic scalability is not asserted.

A.4 Required platform links

  • rei-aios site: https://rei-aios.pages.dev/ (UI showcase; theory chart, radar, Octatheoria)
  • Author's note.com: https://note.com/nifty_godwit2635 (Japanese-language popular writeup)
  • Zenodo v0.1 DOI: TBD (issued at publish; recorded in data/publications/publish-log-paper176-zenodo.json)
  • Source repository: https://github.com/fc0web/rei-aios
  • Lean 4 artifacts:
    • Main: data/lean4-mathlib/CollatzRei/FermatNineExcessWitness.lean
    • Companion (STEP 1306): data/lean4-mathlib/CollatzRei/ZcsgMdnstModularBoundary.lean
  • Measurement data: data/fermat/v2-order-extension-2026-07-20.json
  • Original technical draft: data/fermat/v2-order-extension-2026-07-20.md
  • Computation source: scripts/fermat/v2_order_extension_2026-07-20.py

Part B: Conditional (7 elements)

B.5 Background — origin of the modular bridge sketch

The paper's origin is chat-Claude 2026-07-19 arc's Paper 63 sketch §7 (an initial candidate for the ZCSG/MDNST domain boundary paper, later renumbered to avoid collision with Rei's existing Paper 63 SNST). The §7 sketch hypothesized: "some monotonic function of n predicts the excess of v_2(ω_{F_n}(3)) above Lucas's lower bound n + 2." chat-Claude 2026-07-20 privately extended F_5–F_8 measurements. Rei's independent replication of F_5–F_11 (2026-07-20) found F_9 excess = 5, refuting the monotonicity hypothesis at n = 9.

B.6 Methodology

Excess computation (Python, scripts/fermat/v2_order_extension_2026-07-20.py):

  • For each known prime factor p of F_n:
    • Compute v_2(p − 1) directly
    • Compute v_2(ord_p(3)) via successive squaring of 3^m where m = (p − 1) / 2^{v_2(p − 1)} (odd part), then iteratively check if 3^(m · 2^k) ≡ 1 mod p for k = 0, 1, ..., v_2(p − 1)
  • v_2(ω_{F_n}(3)) = max_p v_2(ord_p(3))
  • excess = v_2(ω_{F_n}(3)) − (n + 2)

Lean 4 F_9 witness (FermatNineExcessWitness.lean, §7 Pratt-style):

  • Define sqIterMod : ℕ → ℕ by sqIterMod 0 = 2; sqIterMod (k+1) = (sqIterMod k)^2 mod 2424833
  • Prove: sqIterMod 9 = 2424832 (kernel arithmetic, by decide or explicit computation — NOT native_decide)
  • Deduce: 2^{512} ≡ 2424832 = −1 mod 2424833, hence 2424833 ∣ 2^{512} + 1 = F_9

B.7 Empirical scope (v0.1 as-of 2026-07-30)

Substrate Metric v0.1 measured v0.2 target
Python 3.x (arbitrary precision) excess sequence n = 5..11 0, 0, 0, 1, 5, 0, 0 (7/7) extension to n = 12..15 if factorizations available
Lean 4 v4.29.0 + Mathlib v4.27.0 axiom-free F_9 divisibility witness 44 theorems (26 + 18) axiom-free possible generalization to other small Fermat factors
Rei stack (STEP 1306) ZCSG/MDNST negative result 18 theorems maintain

Honest scope of §B.7: v0.2 target cells are placeholders, not measured data. The load-bearing v0.1 content is F1–F4 in §A.1 and the 44 axiom-free theorems in §A.2.

B.8 Prior art audit

  • Lucas 1878 (Théorie des Fonctions Numériques Simplement Périodiques): established the lower bound v_2(ω_{F_n}(3)) ≥ n + 2 for n ≥ 2. Paper 176 uses this as the reference floor.
  • Selfridge-Hurwitz 1963: originally proved 2424833 ∣ F_9. Paper 176 §7 replaces this external attribution with a Lean-internal Pratt-style iterative-squaring proof (see A.2 F4).
  • Euler 1732 (F_5 compositeness), Landry-Le Lasseur 1880 (F_6), Morrison-Brillhart 1970 (F_7), Brent-Pollard 1980 (F_8), Lenstra 1990 (F_9 middle factor), Brent 1995 (F_10), Brent 1988 (F_11): factor discoveries for each Fermat number in the measurement range.
  • Paper 61 ZCSG / Paper 62 MDNST / Paper 63 SNST (Rei existing): source of the ZCSG/MDNST semantic-container framing.
  • STEP 1306 (Rei internal, 2026-07-20): Lean 4 axiom-free negative result for the ZCSG/MDNST modular boundary hypothesis.

Judgment: All six listed prior-art areas are addressed. No "world-first" attribution required. Paper 176's novel Rei-side contribution is the specific n = 5..11 empirical excess table + Lean 4 axiom-free F_9 structural witness (Pratt-style, replacing Selfridge-Hurwitz external attribution) + 7/7 characterization within this bounded range.

B.9 Related Rei stack references

  • STEP 1306 (2026-07-20): ZcsgMdnstModularBoundary.lean, Lean 4 axiom-free negative result. Direct companion to Paper 176.
  • STEP 1307 (2026-07-20): F_9 factor witness origin.
  • STEP 1308 (2026-07-20): additional context.
  • Paper 61 ZCSG / Paper 62 MDNST / Paper 63 SNST: existing Rei theories whose "container-not-source" role Paper 176 clarifies.
  • [[project-step1306-zcsg-mdnst-modular-boundary-2026-07-20]] memory: origin arc.
  • [[project-step1307-fermat-v2-order-extension-2026-07-20]] memory: F_9 measurement.
  • [[reference-chat-claude-2026-07-20-novelty-advice]]: 5 novelty principles applied.
  • [[reference-fermat-excess-v2k-characterization-2026-07-20]]: characterization detail.
  • [[project-session-2026-07-20-fermat-arc-path-b-launch]]: session origin.

B.10 Deferred to v0.2 or later

Paper 176 v0.1 does NOT include the following:

  1. Extension to n = 12..15: requires known factorizations, some Fermat numbers only have known small factors with cofactor status unresolved.
  2. General excess-boundedness statement: whether excess(F_n) is bounded, has infinite lim sup, etc. — not addressed.
  3. Multiplicative order computation in Lean 4: the external Python step (v_2(ord_p(3))) is not ported to Lean 4; large kernel arithmetic would be needed.
  4. Generalization beyond base 3: v_2(ω_{F_n}(a)) for other bases a (particularly base 5, 7) is not measured.
  5. Full ZCSG/MDNST cross-check with the excess irregularity: the "container-not-source" positioning is established structurally in STEP 1306 but not exhaustively cross-checked against every Fermat factor.

Part C: Full structure (partial in v0.1)

C.1 Version history

  • v0.1 (2026-07-30): This document. First formal paper draft, extracted from data/fermat/v2-order-extension-2026-07-20.md (2026-07-20 technical draft) + FermatNineExcessWitness.lean (2026-07-20 Lean 4 file) + ZcsgMdnstModularBoundary.lean (STEP 1306). 10-day no-rush period per [[feedback-no-rush-publication]].
  • v0.2 (planned): possible extension to n = 12..15 if factorizations available; general excess-boundedness discussion.

C.2 References (partial; full BibTeX in v0.2)

  • Lucas, E. (1878). Théorie des Fonctions Numériques Simplement Périodiques. American Journal of Mathematics.
  • Selfridge, J. L., & Hurwitz, A. (1963). Fermat numbers and Mersenne numbers. Mathematics of Computation, 17(83), 195–197.
  • Euler, L. (1732). Observationes de theoremate quodam Fermatiano. Commentarii academiae scientiarum Petropolitanae, 6, 103–107. (F_5 factorization.)
  • Landry, F., & Le Lasseur, F. (1880). Note sur la décomposition du nombre 2^64 + 1. Comptes Rendus.
  • Morrison, M. A., & Brillhart, J. (1970). The factorization of F_7. Bull. Amer. Math. Soc., 77, 264.
  • Brent, R. P., & Pollard, J. M. (1981). Factorization of the eighth Fermat number. Math. Comp., 36, 627–630.
  • Lenstra Jr., H. W., Manasse, M. S., & Pollard, J. M. (1993). The factorization of the ninth Fermat number. Math. Comp., 61, 319–349.
  • Brent, R. P. (1995). Factorization of the tenth Fermat number. Preprint / Math. Comp. update.
  • Fujimoto, N., Rei, & Claude. (2026). Paper 26 v3.0 (D-FUMT₈ Third Primitive as Śūnyatā Operator). Zenodo. https://doi.org/10.5281/zenodo.21679998

C.3 Acknowledgments

  • 藤本 伸樹 (Nobuki Fujimoto): 2026-07-20 explicit direction for empirical F_9-F_11 extension after chat-Claude's F_5-F_8 sketch; STEP 1306-1308 authorization; 2026-07-30 Paper 176 formal publish authorization.
  • chat-Claude (Anthropic, claude-opus-4-7 web instance): Paper 63 (renumbered 176) sketch §7 origin; F_5-F_8 empirical computation; independent replication of v_2(ord_{2424833}(3)) = 16; §7 replacement suggestion (Selfridge-Hurwitz → Lean-internal Pratt-style); 5 novelty principles guidance (see [[reference-chat-claude-2026-07-20-novelty-advice]]).
  • Rei-AIOS autonomous research substrate: F_5-F_11 independent Python measurement; Lean 4 axiom-free F_9 divisibility witness via iterative squaring sqIterMod; ZcsgMdnstModularBoundary STEP 1306 companion; SAC-4 100% acceptance discipline (feedback-critique-response-pattern); evaluation symmetry principle enforcement (SELF⟲ marker-only reading).

End of Paper 176 v0.1 draft.

Publish protocol (2026-07-30):

  1. Rei prepares 11-platform publish scripts (Paper 26 v3 pattern; Zenodo API User-Agent header applied).
  2. Founder confirmed publish authorization 2026-07-30.
  3. Zenodo v0.1 DOI issued as NEW deposit. Recorded in data/publications/publish-log-paper176-zenodo.json.
  4. 9-11 platform mirrors (IA + Dev.to + HackMD + Hatena + Livedoor + Notion + Mastodon + Nostr + GitHub; Scrapbox chronic-fail expected; Harvard skip per default opt-in policy).
  5. docs/RECENT_UPDATES.md updated with v0.1 DOI + publish log path.

Top comments (0)