The descent is strictly monotone
NOT A NOVELTY CLAIM. This is a machine-checked formalisation, checked by the Lean 4 kernel and depending on no axiom. It is dated and citable. Prior art, where it exists, is cited below. No discovery is claimed.
THE RATCHET LAW over the real history, read newest-first: each count is strictly below the one before it. A wave that added an index.ts would make this proof fail, which is exactly what "the count may fall, never rise" means when it is checkable. The pairs are DERIVED from `recorded` — `recorded.zip recorded.tail` is the consecutive pairing — because they used to be typed out a second time and that second copy rotted: the corpus descended to 138, the record above followed, and this list did not. It went on proving a true fact about a history that had stopped being the whole history, which is the exact failure the comment on `recorded` describes, committed one definition further down. A record read twice is a record that can disagree with itself.
Proposition
(∀ p ∈ recorded.zip recorded.tail, p.1 < p.2)Proof
By decide in wave-57-extraction-verified.lean. Checked by the Lean kernel: it depends on no axiom.
Sources and identifiers
- Lean source · src/pair/lean/proofs/wave-57-extraction-verified.lean
- Typeset paper · src/research/lean-theorems.tex
- Repository deposit · doi:10.5281/zenodo.21787144
- Author · ORCID 0009-0000-7312-9778