---
id: F-031
title: Periodic decomposition of finite-prime adjacent loss
tier: lean
polarity: positive
depends_on: [F-029]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-031_periodic-small-prime-loss/lean/Research/PeriodicLogLoss.lean workspace/experiments/experiment_3_adjacent_equal_density/lean/Research/PeriodicLogLoss.lean && (cd workspace/experiments/experiment_3_adjacent_equal_density/lean && lake build)
date: 2026-07-11
---

## Statement

The logarithmic loss from primes at most `Z`, written as a divisibility sum
`fixedLogLoss Z n`, is periodic with squarefree period
`primeModulus Z = ∏_{p≤Z}p` and agrees with `truncatedLogLoss Z n` for nonzero
`n`.  Its adjacent difference decomposes, for `Z≥3`, as

```lean
fixedLogLoss Z (n + 1) - fixedLogLoss Z n =
  baseLogDiff n + extraLogDiff Z n
```

where `baseLogDiff` is six-periodic and injective on residues `0,…,5`, the
extra term is periodic modulo the product of primes in `(3,Z]`, and that extra
modulus is coprime to six.

Formal theorems include `fixedLogLoss_eq_truncated`,
`fixedLogLoss_periodic`, `baseLogDiff_periodic`, `baseLogDiff_injOn`,
`extraLogDiff_periodic`, `six_coprime_extraModulus`, and
`fixedLogDiff_eq_base_add_extra`.

## Proof / verification

Divisibility by each selected prime is unchanged after adding the product of
all selected primes.  The cutoff-three formula is enumerated explicitly; its
six adjacent values are proved distinct from positivity of the losses at 2 and
3 and the strict inequality `primeLogLoss 3 < primeLogLoss 2`.  Splitting the
finite prime set at 3 gives the additive decomposition.  Every extra prime is
coprime to 6, so their product is as well.

Artifact: `lean/Research/PeriodicLogLoss.lean`; Lean accepts it with no
`sorry`, `admit`, native evaluator axiom, or project-declared axiom.
