Sothic cycle meshes
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 Sothic cycle meshes the Egyptian civil year — 1461 × 365 = 1460 × 365.25, in whole quarter-days.
Proposition
1461 * 365 * 4 = 1460 * 1461Proof
By decide in registry.lean. Checked by the Lean kernel: it depends on no axiom.
Sources and identifiers
- Lean source · src/pair/lean/proofs/registry.lean
- Typeset paper · src/research/lean-theorems.tex
- Repository deposit · doi:10.5281/zenodo.21787144
- Author · ORCID 0009-0000-7312-9778
Proved in the same file
- Sothic cycle days
- Vdw nine forces
- Vdw eight escapes
- Condorcet profiles are 216
- Condorcet six cycle
- Graeco latin none of order two
- Graeco latin order three
- Graeco latin order four
- Graeco latin order five
- Kummer instances
- Tau six is product
- K5 k33 break planar bounds
- Catalan heptagon
- Exactly three regular tilings
- Steiner two three seven
- Heawood moore bound
- Exactly five platonic solids
- Pisano ten is sixty
- Pisano nine is twenty four
- Pisano reads sixty at ten
- Pisano is even from three to fifty
- Cassini step negates
- Cassini for every n
- Catalan parity is mersenne
- Fibonacci partial sum for every n
- Lucas is the sum of the fibonacci neighbours
- Lucas fibonacci identity for every n
- Triangular closed form for every n
- Odd sum is a square for every n
- Pyramidal closed form for every n
- Nicomachus for every n
- Gray code is a one bit cycle to twelve
- Hockey stick to twenty
- Vandermonde convolution to twelve
- Amicable 220 284 is the smallest
- The three digit armstrong numbers are four
- Taxicab two is 1729
- Euler polynomial is prime to 39 then 41 squared
- Fermat five is composite
- Frobenius six nine twenty misses 43
- Frobenius six nine twenty reaches every n from 44
- Schur two is four
- Z doubling orbit lies in the units on odd moduli
- Z order of two divides the unit count on odd moduli
- Z two is no unit on even moduli
- Z reflection is an involution and partitions
- Z fibonacci period returns and is even beyond two
- Z nine orbit is the vortex sequence
- Circle of fifths does not close