---
id: F-024
title: Positive-start fixed-rate loss tails
tier: lean
polarity: positive
depends_on: [F-019, F-020, F-021]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-024_positive-start-forced-loss-tail/lean/Research/RateTailPositive.lean workspace/experiments/experiment_2_elementary_upper_bound/lean/Research/RateTailPositive.lean && (cd workspace/experiments/experiment_2_elementary_upper_bound/lean && lake build)
date: 2026-07-11
---

## Statement

For every `R`, there is a fixed positive `B` such that a decreasing block
`[k,k+n)` with `n>B` has a terminal tail `[q,q+ℓ)` with **positive** `q`, at
most `B` discarded terms, and `Rℓ≤intervalLoss(q,ℓ)`.

Formal theorem: `exists_rate_forcing_modulus_pos`.

## Proof / verification

This retains the positivity output of F-021's divisible-anchor construction,
then applies F-019 and F-020 exactly as in F-021.  The strengthened interface
allows direct application of F-022.

Artifact: `lean/Research/RateTailPositive.lean`; Lean accepts it without
`sorry`, `admit`, or axioms.
