computo ergo sum日本語

Principia

A section for mathematics and physics. Chiefly a record of working on unsolved problems of mathematics — for each problem: what it is, how far the world has come, what was measured on this machine, and what remains.


This index falls into four parts. The articles by problem — each of them separating what the problem is / how far the world has come / what was done / what remains. Then spacetime and dimension — not unsolved problems, but the side of physics and geometry. Then what can be said across the problems, and how the work is done. Finally what remains, and machine checking — where the open items at the end of each article now stand, and the list of machine-checked claims.

Claims carry one of four labels. Leanmachine-checked paperproved, not yet machine-checked computationchecked on this machine, within the range stated knowna known theorem or a restatement. Nothing here is called a first — the most that is said is "not found in the literature searched".


The articles by problem

The Collatz conjecture 3n+1 is the only exactly critical map of this form. There are four articles on this problem, and this is the entrance
  • Only 3n+1 is exactly critical — criticality as a whole, the distribution of the overshoot (five digits of agreement with measurement), the boundary that can be counted exactly, the lower bound on cycles
  • What the sign of 1/3 decides — the sign of the asymmetry is fixed by 3³ < 2⁵
  • That constant is not yet a constant — the limit has a closed form; the value at each depth does not. The oscillation is a sawtooth built from the continued fraction of log₂3
The Riemann hypothesis The explicit formula run both ways — building the staircase of primes from the zeros, and recovering the height of the zeros from the primes. And Λ = 0 exactly, which is to say no slack at all
The Erdős conjecture on arithmetic progressions The record 3.0085385 for k=3 and the record 4.4397535 for k=4 are each a single machine-checked theorem
The BSD conjecture |Ш| agreeing to thirteen decimal places across ranks 0–7, with the record of turning the verification of curve labels into a mechanism
The Lovász conjecture Four exceptions. The search space for a fifth splits three ways by the deficiency def
The Hadwiger–Nelson problem f(α), the largest unit-distance graph with independence number at most α: f(3) = 10, and f(4) is 14 or 15
Drawing unsolved problems at random A record of the smaller problems — Sierpiński numbers, Riesel numbers, distinct distances

Spacetime and dimension

One sign is different Time is not a fourth axis; it is one sign that differs in a quadratic form. Five measured consequences of that
The world is zero Four pages of notes from 2002, written from E=mc² alone. The exponential formula agrees with the Schwarzschild solution to third order, and the places where it breaks can be named
What happens only in four dimensions A casebook for Euclidean ℝ⁴. Not an unsolved problem, but a tool for seeing — and a different thing from the four dimensions of spacetime treated in the two articles above

Across the problems, and how the work is done

Problems remain only at the exact edge The cross-cutting piece. Line up the long-unsolved problems and every one of them sits at strict criticality, which is not a coincidence but the result of selection. What can be proved is always only the "no slack" side
A map of the walls For each problem, what is out of reach. Walls that closed are marked closed
Taking stock of novelty The results sorted under four labels — closed in Lean, proved on paper, closed by computation, restatements of known facts. With theorem names

What remains, and machine checking

What remains Where the open items at the end of each article now stand — closed / changed shape / open as first posed
The Lean verification bundle The list of machine-checked claims. The bundle, the ledger of theorems, and how to check them