# verified_math.md — the ledger of verified mathematics

This folder, [`verified_math/`](.), is **the heart and soul of the entire
operation**. Every formally established result — **positive and negative** —
lives here. Progress on the problem *is* the growth of this folder: each
verified lemma or theorem is one confirmed step toward a true solution.
Everything else (searches, heuristics, notes) exists to produce entries here.

## How this ledger works — two tiers, strict

**This file is ONLY a list of one-liners.** One line per verified fact, nothing
more. Full statements NEVER live in this file — they live in each fact's own
folder. That keeps this file cheap to read in full (you will re-read it after
every context reset) no matter how many facts accumulate.

```
verified_math/
├── verified_math.md            ← this file: ONE LINE per fact (the index)
└── F-001_<short-slug>/         ← one folder per verified fact
    ├── entry.md                ← the FULL story: frontmatter + complete
    │                             statement, proof sketch, how to re-verify
    └── <proof artifacts>       ← the Lean file(s) / witness data / checker run
```

To learn more about any fact: open its folder's `entry.md`. The proof code is
right next to it.

## Admission rule — verified means verified

**Nothing enters this folder unless it has been machine-verified**, either:
- proved in **Lean** and accepted by `lake build`, with no `sorry`/`admit`
  (lemmas / theorems / impossibility results), or
- accepted by the answer checker in [`check_answer/`](../check_answer)
  (constructions / computations / exhaustive non-existence).

No conjectures. No "probably". No unchecked claims. Informal/heuristic dead ends
go in [`notebook.md`](../notebook.md), not here — but once you can *prove*
something doesn't exist or can't work, it becomes a **negative** entry here.
Expect the early phase to fill this folder with negative results (AGENTS.md
§1a) — a large verified negative space narrows the hunt.

## How to add a fact — run `new-fact`

```bash
new-fact <short-slug> [--tier lean|gate|census] [--negative] \
         [--depends F-001,F-002] [--supersedes F-011]
```

It mints the next zero-padded id, creates `F-<nnn>_<slug>/entry.md` with the
frontmatter template, and appends the one-liner below. Then you fill in the
entry body and copy the proof artifacts into the folder.

`entry.md` starts with structured frontmatter — keep every field accurate,
because this is what makes the fact findable later:

```markdown
---
id: F-003
title: <short human title>
tier: lean            # lean (kernel proof) | gate (named verifier binary) | census (exhaustive computation)
polarity: positive    # positive | negative
depends_on: [F-002]   # facts this proof builds on — `rg "depends_on:.*F-002"` = reverse graph
supersedes: []        # set when this fact corrects an earlier one
verifier: <the EXACT command that re-verifies this fact>
date: 2026-07-04
---

## Statement
<plain language AND the formal statement>

## Proof / verification
<proof sketch; what the verifier checks; artifact list>
```

Rules:
- **Never edit or delete an existing fact.** If a fact turns out wrong, mint a
  NEW fact with `supersedes: [F-<nnn>]` explaining what broke, and mark the old
  ledger line `(superseded by F-<mmm>)`. Anything you already read must stay true.
- Keep `depends_on` honest — it is how a fresh session pulls only the subgraph
  it needs instead of re-reading everything.

The ledger line format (`new-fact` writes it for you):

```
- **F-<nnn>** [lean|gate|census] <title>: <one-sentence statement> → F-<nnn>_<slug>/
```

---

## The facts (one line each — full detail in each folder)

- **F-001** [gate] Faithful strict-pattern formalization and finite-witness gate: The Lean target and independent exact Rust counterexample checker pin down the strict reading while explicitly isolating the source's tie ambiguity. → F-001_verifier-formalization/
- **F-002** [census] The decreasing pattern is not always first missing: Exhaustively, `F(826)=3` while `φ(823)>φ(824)>φ(825)>φ(826)`, disproving the strict first-missing claim. → F-002_decreasing-not-first/
- **F-003** [lean] Every-pattern length is bounded by decreasing-run length: For every cutoff, choosing the reverse permutation proves `F(n)≤G(n)`. → F-003_all-patterns-bounded-by-decreasing/
- **F-004** [lean] Sub-triple-log decreasing runs obstruct the proposed asymptotic: If `G(n)/logloglog n→0`, then the same holds for `F`, ruling out every positive constant `c`. → F-004_subtriplelog-obstruction/
- **F-005** [lean] Natural weak pattern is not most frequent at cutoff 7 (superseded by F-026): Under exact finite-start frequency, the natural equality pattern occurs twice through 7 while the increasing pattern occurs three times. → F-005_natural-weak-not-most-frequent/
- **F-006** [census] Exact first cutoff for all length-four strict patterns: All 24 patterns first become complete at `N=185,910,725`, when rank vector `[2,3,1,0]` first appears. → F-006_exact-length4-threshold/
- **F-007** [lean] Universal strict-pattern occurrence is prefix-closed in length: `AllPatternsUpTo n (k+1)` implies `AllPatternsUpTo n k` by extending and restricting permutations. → F-007_universal-pattern-prefix-closure/
- **F-008** [lean] Abel formula for the finite prime-reciprocal sum: Formally, `∑_{p≤x}1/p = π(⌊x⌋)/x + ∫₂ˣ π(⌊t⌋)/t² dt` for `x≥2`. → F-008_prime-reciprocal-abel/
- **F-009** [lean] Formal Chebyshev upper bound for prime reciprocal sums: There is `E>0` with `∑_{p≤x}1/p ≤ E log log x` eventually. → F-009_prime-reciprocal-loglog-upper/
- **F-010** [lean] Exponential prime-loss lower bound for totient ratios: For `n≠0`, `exp(-∑_{p|n}1/(p-1)) ≤ φ(n)/n`. → F-010_totient-exponential-loss/
- **F-011** [lean] Uniform divisibility count in consecutive intervals: A positive `p` divides at most `⌊n/p⌋+1` numbers in any interval of `n` consecutive naturals. → F-011_interval-divisibility-count/
- **F-012** [lean] Prime-by-prime rearrangement of consecutive totient loss: Total `∑_{m in interval}∑_{p|m}1/(p-1)` equals the sum over primes of divisor counts divided by `p-1`. → F-012_interval-loss-prime-rearrangement/
- **F-013** [lean] Elementary logarithmic bound on distinct prime factors: For `n≠0`, `2^ω(n)≤n` and hence `ω(n) log 2≤log n`. → F-013_distinct-prime-factor-card-bound/
- **F-014** [lean] Uniform bounds for the two prime-loss kernels: For every `Z`, `∑_{p≤Z}1/(p(p-1))≤π²/3` and `∑_{p≤Z}1/(p-1)≤2∑_{p≤Z}1/p`. → F-014_prime-loss-kernel-bounds/
- **F-015** [lean] Low-prime loss bound for every consecutive interval: The `p≤Z` contribution is at most `(π²/3)n + 2∑_{p≤Z}1/p` on any length-`n` interval. → F-015_low-prime-interval-loss/
- **F-016** [lean] High-prime loss bound for every consecutive interval: On `[k,k+n)⊆[1,X]`, the `p>Z` contribution satisfies `L_{>Z}·Z·log 2≤n·log X`. → F-016_high-prime-interval-loss/
- **F-017** [lean] Combined low/high prime bound for total interval loss: On `[k,k+n)⊆[1,X]`, total loss is at most `(π²/3)n+2∑_{p≤Z}1/p+n log X/(Z log 2)`. → F-017_combined-interval-loss/
- **F-018** [lean] Exponential lower bound for an interval product of totient ratios: `exp(-total prime loss)≤∏_{m in interval}φ(m)/m` for every positive-start interval. → F-018_interval-ratio-product-lower/
- **F-019** [lean] Arbitrarily small totient ratios at fixed multiples: For every `R`, one fixed modulus `B` forces `φ(m)/m≤e⁻ᴿ` at all nonzero multiples of `B`. → F-019_small-totient-ratio-at-multiples/
- **F-020** [lean] A decreasing low-ratio tail forces linear interval loss: If a length-`ℓ` tail decreases from an anchor with `φ(q)/q≤e⁻ᴿ`, then `Rℓ≤intervalLoss(q,ℓ)`. → F-020_decreasing-tail-forces-loss/
- **F-021** [lean] Fixed-rate loss tails inside every long decreasing block: For every `R`, a fixed `B` makes each decreasing block longer than `B` contain a tail of length `ℓ≥n-B` with `Rℓ≤intervalLoss`. → F-021_divisible-anchor-in-decreasing-block/
- **F-022** [lean] Uniform linear-plus-triple-log interval loss bound: Eventually every `[q,q+ℓ)⊆[1,X]` has loss at most `(π²/3+2/log 2)ℓ+A log log log X` for one fixed `A`. → F-022_interval-loss-triplelog-upper/
- **F-023** [lean] Eventual successor stability of the triple logarithm: Eventually `log log log(X+1)≤2 log log log X`. → F-023_triplelog-successor-comparison/
- **F-024** [lean] Positive-start fixed-rate loss tails: F-021's forced-loss tail can be chosen with positive start `q`, so the uniform interval bound applies directly. → F-024_positive-start-forced-loss-tail/
- **F-025** [lean] The proposed positive triple-log asymptotic is false: `G(X)/log log log X→0`, hence `F(X)/log log log X→0` and no positive constant `c` as proposed exists. → F-025_no-positive-triplelog-asymptotic/
- **F-026** [lean] Kernel-only weak-frequency counterexample: Explicit kernel enumeration proves the natural equality order occurs 2 times through 7 while increase occurs 3 times, superseding F-005's native evaluation. → F-026_kernel-weak-frequency-counterexample/
- **F-027** [lean] Eventual natural-frequency dominance implies Erdős #1003: If the natural length-two equality order eventually matches or beats cumulative increasing frequency, then `φ(n)=φ(n+1)` infinitely often. → F-027_natural-frequency-implies-problem1003/
- **F-028** [lean] Canonical eventual-frequency reading implies Erdős #1003: If the natural weak order is most frequent at all sufficiently large cutoffs even just for `k=2`, then `φ(n)=φ(n+1)` infinitely often. → F-028_canonical-third-question-obstruction/
- **F-029** [lean] Exact logarithmic totient loss and cutoff decomposition: `∑_{p|n}-log(1-1/p)=-log(φ(n)/n)`, splits at any cutoff, and equal adjacent totients prescribe its exact first difference. → F-029_exact-log-totient-loss/
- **F-030** [lean] Uniformly vanishing mean of the large-prime log tail: For every `ε>0`, one cutoff `Z` makes `∑_{m≤N} tailLogLoss(Z,m)<εN` for every positive `N`. → F-030_vanishing-mean-log-tail/
- **F-031** [lean] Periodic decomposition of finite-prime adjacent loss: The cutoff loss splits into a six-periodic injective base and a coprime periodic extra-prime term. → F-031_periodic-small-prime-loss/
- **F-032** [lean] One-sixth concentration bound for finite-prime adjacent loss: Uniformly in the center, at most one sixth of a complete finite-prime period lies in a sufficiently short loss interval. → F-032_finite-prime-one-sixth-concentration/
- **F-033** [lean] Equal adjacent totients have upper density below one third: Eventually fewer than one third of adjacent starts have equal totients, so equality cannot dominate both strict orders. → F-033_adjacent-equal-upper-density/
- **F-034** [lean] The natural length-two weak order is asymptotically not most frequent: Eventually, and under the limiting-frequency reading, equality loses to a strict adjacent order. → F-034_natural-frequency-negative/
