The thousand bit integer has a thousand bits and exactly four threes
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.
Proposition
2 ^ 999 ≤ thousand ∧ thousand < 2 ^ 1000 ∧ (List.range' 1 6).all (fun k => (thousand % 3 ^ k == 0) == (k ≤ 4)) ∧ 999 = 27 * 37 ∧ (2 ^ 333 + 1) * (2 ^ 666 - 2 ^ 333 + 1) = thousand ∧ (2 ^ 111 + 1) * (2 ^ 222 - 2 ^ 111 + 1) = 2 ^ 333 + 1 ∧ (2 ^ 37 + 1) * (2 ^ 74 - 2 ^ 37 + 1) = 2 ^ 111 + 1 ∧ 2 ^ 37 + 1 = 3 * 1777 * 25781083Proof
By decide in thousand.lean. Checked by the Lean kernel: it depends on no axiom.
Sources and identifiers
- Lean source · src/pair/lean/proofs/thousand.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
- The thousand bit case is one hundred twenty five octaves
- The binary units tile the thousand exactly
- The thousand is the cube octave times pentagram cubed
- The thousand carries residue one mod nine
- The thousand bit case overflows the width thirty two ceiling
- The minimal register for the thousand is width thirty three
- The thousand fills between ninety seven and ninety eight percent of its register
- The thousand bit structure is decided not a quantum machine
- The sigma trapdoor is fermats difference of squares
- A wrong witness decodes nothing because a semiprime has one split
- An impossible integer with twin primes is opened blind in one reflection
- This deposits factor route returns a partial answer that multiplies back
- The free register is one hundred twenty two only at width four
- One address sits sixty seven bits below the one twenty eight floor under grover
- The seal exponent seven is undone by thirty one mod ninety one
- The fold mod eight misses one tamper in eight