84 theorems, every one decided by the Lean 4 kernel and depending on no axiom. Each is a formalisation of a stated result, dated and citable. None is a novelty claim.

bsd.lean

• Sigma is an involution
• Central point is the fixed point
• Root number squares to one
• Root number one iff rank even
• Parity is an involution

coin.lean

• The coin is an involution
• The harmonic is the only fixed point
• All that is not harmonic is moved
• The sides are equal and exchanged
• The coin is two sides and one edge
• Every bit of resistance drains
• The harmonic carries no resistance
• The whole surface sums to zero
• The drain is exact at every scale

decidability.lean

• Verified at every point below the bound
• And false at the bound
• Finite verification does not entail the universal
• A bigger bound proves no more
• What a finite check does establish
• The clay files quantify over finite lists

hodge.lean

• Sigma is an involution
• Sigma preserves degree
• Fixed type is p equals q
• Diagonal is fixed at every k
• Involution fixes the diagonal

involution.lean

• Orbit sums to zero
• Odd vanishes at a fixed point
• EvenPart is symmetric
• The split loses nothing
• The instance is an involution
• The instance cancels over every orbit
• The instance has one harmonic point
• The instance splits without loss

navier-stokes.lean

• Reversal is an involution
• Euler is time reversible
• Viscosity breaks time reversal
• Fixed points are exactly the inviscid

p-vs-np.lean

• Sigma is an involution
• Fixed points are p and pspace
• Np and conp are swapped
• If np is fixed then np equals conp
• P is closed under complement

poincare.lean

• Chi and genus are inverse
• Sphere has euler characteristic two
• Torus has euler characteristic zero
• Double torus has chi minus two and rank four
• Homology rank is twice the genus

riemann.lean

• Sigma is an involution
• Critical line is the fixed point
• Sigma pairs the plane
• The fixed line is one half
• Involution fixes the critical line

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

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

yang-mills.lean

• Middle forms have dimension six
• Star squares to the identity
• Selfdual and antiselfdual split the six
• Star is an endomorphism only in the middle
• Involution splits the middle forms