Shor vector dwarfs the number
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.
Each vector dwarfs the number it factors by more than a hundredfold — the exponential a physical device would not spend, stated as three inequalities.
Proposition
4096 > 15 * 100 ∧ 32768 > 21 * 100 ∧ 262144 > 35 * 100Proof
By decide in corpus.lean. Checked by the Lean kernel: it depends on no axiom.
Sources and identifiers
- Lean source · src/pair/lean/proofs/corpus.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
- Euler characteristic and genus are inverse
- The genus reads back from chi at every genus
- Census bands are gapless and descending
- Census is one hundred twenty three
- Fibonacci partial sum identity
- Folding by chi is undone by unfolding
- Reflection is an involution
- Reflection pairs and one fixed point
- Reflection closes on the digits
- Reflection is an involution on the whole lattice
- Golden ratio bounds
- Golden ratio minus one bounds
- Splitting then burning water is the identity
- Verify beats recompute by magnitudes
- Hexbit receipt beats rebuild
- Hexbit advantage widens
- Sixty four components
- Shor state vectors unchanged
- Shor rsa gap is between exponents
- Shor zero skipping divides by the work register