---
id: F-021
title: Fixed-rate loss tails inside every long decreasing block
tier: lean
polarity: positive
depends_on: [F-019, F-020]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-021_divisible-anchor-in-decreasing-block/lean/Research/DecreasingAnchor.lean workspace/experiments/experiment_2_elementary_upper_bound/lean/Research/DecreasingAnchor.lean && (cd workspace/experiments/experiment_2_elementary_upper_bound/lean && lake build)
date: 2026-07-11
---

## Statement

For every real `R` there is a fixed positive integer `B` such that every
strictly decreasing totient block `[k,k+n)` with `n>B` has a terminal subblock
`[q,q+ℓ)` satisfying

\[
 q+\ell=k+n,\qquad n\le B+\ell,\qquad
 R\ell\le \operatorname{intervalLoss}(q,\ell).
\]

Formal theorem: `exists_rate_forcing_modulus`.  The artifact also formalizes
strictly decreasing blocks, converts `DecreasingOccursUpTo` witnesses to that
form, and proves the explicit divisible-anchor lemma
`decreasingBlock_has_divisible_anchor`.

## Proof / verification

Choose F-019's modulus `B`.  The number
`q=B*(⌊k/B⌋+1)` satisfies `k<q≤k+B`; hence if `n>B`, the decreasing block has a
tail from `q` losing at most `B` terms.  Divisibility gives
`φ(q)/q≤exp(-R)`, and all later totients are at most `φ(q)`.  F-020 then gives
`Rℓ≤intervalLoss(q,ℓ)`.

Artifact: `lean/Research/DecreasingAnchor.lean`.  Lean checks all endpoint and
floor-division arithmetic and accepts the proof with no `sorry`, `admit`, or
axioms.
