263 theorems, every one checked by the Lean 4 kernel, none resting on an axiom beyond propext and Quot.sound — and most on none. Each is a formalisation of a stated result, dated and citable. None is a novelty claim.
bsd.lean
coin.lean
corpus.lean
- 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 vector dwarfs the number
- Shor rsa gap is between exponents
- Shor zero skipping divides by the work register
decidability.lean
hodge.lean
involution.lean
navier-stokes.lean
p-vs-np.lean
poincare.lean
quantum.lean
- Gi add re
- Gi add im
- Gi mul re
- Gi zero re
- Gi one re
- Gi zero im
- Gi one im
- H unitary
- H squared
- Paulis unitary
- Y unitary
- S squared
- Cnot
- Swap
- Toffoli
- Omega fourth
- T gate
- Bell state
- Ghz state
- Chsh classical bound
- Chsh quantum value
- Teleport exact
- Teleport no signalling
- Superdense exact
- Both ways
- No cloning
- Cnot copies the basis
- Stabilizer hadamard
- Stabilizer phase
- Stabilizer cnot
- Deutsch jozsa
- Promise census
- Grover search
- Qft unitary
- Phase estimation exact
- Swap routing
- Unrouted differs
- Routed depth
- Repetition corrects
- Repetition fails on two
- Steane corrects
- Steane css
- Shor nine
- Distance corrects
- Pauli products
- Pauli anticommute
- Pauli square adjoint trace
- Hadamard exchanges phase and bit
- Ghz mermin quantum
- Ghz mermin classical
- No communication
- Alice changes the pair
- Toll is uniform
- Entanglement swapping
- No pairs no swapping
- Sixty degrees is a primitive sixth root of unity
- Zero plus an integer is that integer
- Zero times an integer is zero
- Rotation by sixty degrees keeps the eisenstein integers
- The rotation leaves the integers and keeps the norm
- Six is the first perfect number and a tetrahedron sums to 720
- The doubling circuit steps forty eighty one sixty and back
- The six two star is the two triangles and not the doubling cycle
- The two reflections connect the three trinities
- The two mirrors compose to the forty degree step
- The nines reflection carries the doubling circuit onto itself
- A two to one fold of addresses is many to one by pigeonhole
rational.lean
registry.lean
- Sothic cycle meshes
- 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
riemann.lean
spacetime.lean
- Light is the fixed point
- Light is fixed from either side
- Rest is the identity
- Composition is symmetric
- Below c composes to below c
- The boost preserves the interval
- The light cone is carried to itself
- The reverse boost undoes the boost
- The reverse boost undoes every boost
- Sq lt
- Lt of sq
- Interval scales
- Scale positive
- Timelike invariant
- Spacelike invariant
- Null invariant
- Timelike order absolute
- Spacelike order reverses
- Spacelike simultaneous
- Velocity addition below c
thousand.lean
- 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
- The thousand bit integer has a thousand bits and exactly four threes
- 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
three.lean
- Closure is one hundred sixty two
- Closure is the product
- Closure has no duplicate
- Closure is complete
- Address inverts
- Addresses are the interval
- The compound fraction clears
- Focal plane is unit scale
- Depth is strictly monotone
- Frustum brackets the focal plane
- Denominator is positive on the frustum
- Reflection is an involution
- Reflection closes on the closure
- Reflection has no fixed point
- The closure is eighty one orbits
- Orbit positions cancel
- Reflection complements the address
- The involution laws are general