Proof of Least erasure

if RH = Least erasure and if Least erasure can be proved, what does it makes to RH?

It makes RH a restatement, not a result. Nothing about the zeros of ζ follows.

The equivalence LeastErasure Z ↔ RH Z holds for any world on the chart, and I compiled it. It rewrites one definition as another, so proving least erasure for a world is the same as proving RH for that world. "Least erasure can be proved" therefore means only that RH can be proved for the worlds where the proof works.

The proof I compiled covers finite configurations: a list of on-line heights and off-line pairs. For those, RH holds exactly when every listed pair has zero offset. That is a check on the input, not a theorem about the zeta function. The zeros of ζ are infinitely many and are not given as a finite list, so the ledger proof does not reach them.

A proof of least erasure for the actual zeros would prove RH, since they are the same statement. That proof is the part that is missing. The chart encodes RH as "every zero has x = 1", and least erasure is the same condition quantified over the fibre of the record. The Lean work shows the two encodings agree. It does not show that the zeros satisfy either one.

Earlier I also showed that deriving least erasure from RA is equivalent to RH holding outright, so RA cannot supply the proof. The edition's bridge is where the content would have to come from. In the Final Cut, the identification of the formal zeros with the actual zeros enters as the hypothesis ra, the explicit formula as explicit, and the act as supply. These are inputs the Lean code takes as given. Nothing I compiled proves them.

What the equivalence does give is a faithful conditional: RH holds if and only if the erasure ledger of the zeta world has zero erased bits, provided the chart encodes the zeros correctly. Reading that as physical minimality adds no mathematical content. As far as I know RH is still open, and this work does not settle it.

A proof of least erasure for the actual zeros ... actual zeros proof should be easy, because its ACTUAL. -- you want to try it?

"Actual" does not make it easy. Being an actual zero says the point is a zero of ζ. It does not say where the zero lies. "Every nontrivial zero of ζ has real part 1/2" is exactly the claim that the actual zeros are least-erasing. So a proof of least erasure for the actual zeros is a proof of RH, and the difficulty is the same. I'll still run a concrete check, to see where the actual zeros stand numerically.

I need to correct that check. mpmath.zetazero locates zeros by sign changes along the critical line, so the "real part is 1/2" result is built in and proves nothing about off-line zeros. A real test has to look off the line. I'll count zeros in a rectangle with the argument principle, and compare that count with the zeros found on the line.

I tried it, and it does not work as a shortcut. "Actual" tells us that the zeros exist, not where they are. Locating them is the whole content of RH, so a proof that the actual zeros are least-erasing is a proof of RH.

My earlier numerical check was circular, as I said. Here is a real test. I counted the zeros of ζ in the box −0.5 < σ < 1.5, 1 < t < 60 using the argument principle, which counts zeros off the line as well as on it. I then counted the zeros of the Riemann–Siegel function Z(t) on the line, which only finds zeros on the line. Both counts give 13. The difference is 0. So there are no zeros off the line in this box, and no multiple zeros either.

That supports RH at height 60. It does not prove it. The check covers only a finite range of heights, and the computation is numerical with floating-point arithmetic. Large computations have verified far larger ranges, but an infinite range is still open. A proof would need an argument that controls all the zeros at once, and I do not have one. I also cannot check a formal proof here: the core Lean library has no zeta function, and Mathlib is not installed.

I will not claim a proof. The answer to your question is that the attempt reduces to RH, and the numerical evidence is consistent with RH below height 60. RH remains open as far as I know.

The file is large, so I'll read its structure first and then the parts that bear on the argument.

The paper's main claims are in sections 0, 1, 13, 14, 16 and 20. I'll start with the verdict and scope in section 0.

The paper's central move is the field supply : LeastErasure zeros, which is an input, not a derivation. I need to see how that field is defined and where the closing theorem uses it. I'll read sections 13 and 14.

The closing theorem rh_from_the_act takes an ActualZeros structure as input, and that structure has a supply : LeastErasure zeros field. So the conclusion is RH for whatever configuration the input supplies. I need to check whether the kernel really compiles with an empty cone, and whether the field is the only place the hypothesis enters. I'll extract Appendix A and look at its structure.

The extracted file does not parse at line 1. I'll look at the boundaries and match them against the paper's stated size and digest.

My extraction started one line late and dropped the opening /-. I'll re-extract from line 622 and compile.

The kernel compiles: the file's SHA-256 prefix matches the paper's 161806dc0ed2b4ff, the size matches, exit is 0, and rh_from_the_act has an empty cone. I'll read the structure and proof to see exactly what the theorem uses.

I think the two-direction framing describes the paper's structure well, but it does not give independent evidence for RH. The paper proves a clean equivalence, and the closing step is an assumption equivalent to the conclusion.

What I checked. I extracted the kernel from Appendix A. It matches the stated size of 265,248 bytes and the SHA-256 prefix 161806dc0ed2b4ff. It compiles on Lean 4.19.0 with exit 0 and no errors. rh_from_the_act prints no axioms. I read sections 0, 13 and 14 and the kernel's definitions. I did not check the rest of the 415 theorems or the Appendix B receipts.

The closing proof is one line. rh_from_the_act (A : ActualZeros) : RH A.zeros := (least_erasure_is_the_value A.zeros).mp A.supply. The structure field supply : LeastErasure zeros is equivalent to RH by least_erasure_is_the_value, which the kernel proves without axioms. So the theorem moves RH across an equivalence. The paper says this itself in Theorem 14.2: the field is equivalent to the conclusion. Lean's "no axiom declared" is true, but the hypothesis enters as a structure field, which is an input. Any ActualZeros value for the real zeros would be an RH proof, and building one is exactly what the paper calls the act.

On the two directions. Building upward from the zeros and downward from least erasure gives one proposition, since the kernel proves they are equivalent on every configuration. Their agreement is guaranteed by that theorem, so it is not independent confirmation. The paper's Theorem 11.7 also says RH is the weakest premise that forces the line. So no partial or finite information can feed the top-down route.

On the computation. My check counted zeros up to height 60 in one box, and both counts were 13. That is a bottom-up fact about ζ, consistent with RH up to height 60. Matching it against the chart's least-erasure statement requires that the chart represents ζ's zeros correctly. The paper admits that identification is the reader's: Definition 14.1 says the kernel constructs no map from the zeros of ξ into the chart. A finite check also covers only part of an infinite claim, since supply must hold at all heights. That gap is what the paper calls the act.

My view. The computation supports the claim below height 60, but it adds nothing to the proof. The proof's only real content is the field, and the field is RH. The two readings meeting is a restatement, not a convergence. What the paper establishes is a real and machine-checked result: RH holds for a zero set exactly when that set has least erasure, with no axioms.

LEDGER CHECK · standalone Lean 4.19.0, no import, no declared axiom, no sorry.

Checks the claims: (a) least erasure is equivalent to zero erased bits; (b) an irreversible

registration costs zero exactly when the world has least erasure, for ANY floor constant c ≠ 0;

is equivalent to least erasure under the fibre definition.

namespace LedgerCheck

structure Pt where

x : Int

t : Nat

deriving DecidableEq

def onLine (z : Pt) : Prop := z.x = 1

instance (z : Pt) : Decidable (onLine z) :=

inferInstanceAs (Decidable (z.x = 1))

def reg (z : Pt) : Pt := ⟨1, z.t⟩

abbrev World := Pt → Prop

def OffLine (Z : World) : Prop := ∃ z, Z z ∧ ¬ onLine z

def RH (Z : World) : Prop := ∀ z, Z z → onLine z

def recordOf (Z : World) : World := fun r => ∃ s, Z s ∧ reg s = r

def SameRecord (Z Z' : World) : Prop := ∀ r, recordOf Z r ↔ recordOf Z' r

/-- The fibre definition: an erasing world forces every world of its record to erase. -/

def LeastErasure (Z : World) : Prop :=

∀ Z', SameRecord Z Z' → OffLine Z → OffLine Z'

/-- The fixed-point definition: every point is fixed by registration. -/

def FixedLE (Z : World) : Prop := ∀ z, Z z → reg z = z

theorem reg_onLine (z : Pt) : onLine (reg z) := rfl

theorem record_lossless (Z : World) : ¬ OffLine (recordOf Z) := by

intro h

obtain ⟨r, ⟨s, _, hsr⟩, hoff⟩ := h

apply hoff

rw [← hsr]

exact reg_onLine s

theorem record_same (Z : World) : SameRecord Z (recordOf Z) := by

intro r

constructor

· rintro ⟨s, hs, hsr⟩

exact ⟨reg s, ⟨s, hs, rfl⟩, hsr⟩

· rintro ⟨s', ⟨s, hs, hss'⟩, hs'r⟩

subst hss'

exact ⟨s, hs, hs'r⟩

/-- (a0) Least erasure is the value: the fibre definition is equivalent to RH. -/

theorem least_erasure_iff_RH (Z : World) : LeastErasure Z ↔ RH Z := by

constructor

· intro hle z hz

by_cases h : onLine z

· exact h

· exact absurd (hle (recordOf Z) (record_same Z) ⟨z, hz, h⟩) (record_lossless Z)

· intro hrh Z' _ hoff

obtain ⟨z, hz, hz'⟩ := hoff

exact absurd (hrh z hz) hz'

/-- (d) The fixed-point definition is equivalent to RH, hence to the fibre definition. -/

theorem reg_fixes_iff_onLine (z : Pt) : reg z = z ↔ onLine z := by

constructor

· intro h

have hx := congrArg Pt.x h

exact hx.symm

· intro h

obtain ⟨x, t⟩ := z

have hx : x = 1 := h

subst hx

rfl

theorem fixed_iff_RH (Z : World) : FixedLE Z ↔ RH Z :=

⟨fun hf z hz => (reg_fixes_iff_onLine z).mp (hf z hz),

fun hrh z hz => (reg_fixes_iff_onLine z).mpr (hrh z hz)⟩

theorem fixed_iff_LeastErasure (Z : World) : FixedLE Z ↔ LeastErasure Z :=

(fixed_iff_RH Z).trans (least_erasure_iff_RH Z).symm

/-! ## The finite ledger -/

/-- A finite configuration: heights of on-line zeros, and off-line pairs (offset k, height h). -/

structure FinCfg where

online : List Nat

pairs : List (Int × Nat)

def FinCfg.world (C : FinCfg) : World := fun z =>

(z.x = 1 ∧ z.t ∈ C.online) ∨

∃ p ∈ C.pairs, p.1 ≠ 0 ∧ (z = ⟨1 - p.1, p.2⟩ ∨ z = ⟨1 + p.1, p.2⟩)

/-- Off-line pairs, counted: an offset of zero is on the line and counts nothing. -/

def offCount : List (Int × Nat) → Nat

| [] => 0

| p :: ps => (if p.1 = 0 then 0 else 1) + offCount ps

def FinCfg.erasedBits (C : FinCfg) : Nat := offCount C.pairs

theorem offCount_zero_iff (ps : List (Int × Nat)) :

offCount ps = 0 ↔ ∀ p ∈ ps, p.1 = 0 := by

induction ps with

| nil => exact ⟨fun _ p hp => (nomatch hp), fun _ => rfl⟩

| cons p ps ih =>

show (if p.1 = 0 then 0 else 1) + offCount ps = 0 ↔ ∀ q ∈ p :: ps, q.1 = 0

by_cases hp : p.1 = 0

· rw [if_pos hp, Nat.zero_add, ih]

constructor

· intro h q hq

cases hq with

| head => exact hp

| tail _ hq' => exact h q hq'

· intro h q hq

exact h q (List.Mem.tail p hq)

· rw [if_neg hp]

constructor

· intro h

omega

· intro h

exact absurd (h p (List.Mem.head ps)) hp

/-- RH of the finite world holds exactly when no pair is off the line. -/

theorem rh_iff_erased_zero (C : FinCfg) : RH C.world ↔ offCount C.pairs = 0 := by

rw [offCount_zero_iff]

constructor

· intro h p hp

refine Decidable.byContradiction (fun hk => ?_)

have hz : C.world ⟨1 - p.1, p.2⟩ := Or.inr ⟨p, hp, hk, Or.inl rfl⟩

have := h _ hz

change 1 - p.1 = 1 at this

omega

· intro h z hz

rcases hz with ⟨hx, _⟩ | ⟨p, hp, hk, _⟩

· exact hx

· exact absurd (h p hp) hk

/-- (a) Least erasure holds exactly when the erased bits are zero. -/

theorem least_erasure_iff_zero_erased (C : FinCfg) :

LeastErasure C.world ↔ C.erasedBits = 0 :=

(least_erasure_iff_RH C.world).trans (rh_iff_erased_zero C)

/-! ## The price, with an arbitrary floor constant -/

/-- Price of a registration: c per erased bit if irreversible, 0 if reversible. -/

def FinCfg.price (C : FinCfg) (c : Nat) (irreversible : Bool) : Nat :=

if irreversible then C.erasedBits * c else 0

/-- (b) For any floor constant c ≠ 0, an irreversible registration costs zero exactly when

the world has least erasure. Only c ≠ 0 is used. -/

theorem price_zero_iff_least_erasure (C : FinCfg) (c : Nat) (hc : c ≠ 0) :

C.price c true = 0 ↔ LeastErasure C.world := by

rw [least_erasure_iff_zero_erased]

show C.erasedBits * c = 0 ↔ C.erasedBits = 0

constructor

· intro h

rcases Nat.mul_eq_zero.mp h with h1 | h1

· exact h1

· exact absurd h1 hc

· intro h

rw [h, Nat.zero_mul]

/-- (c) A reversible registration costs zero, by the definition of the price. -/

theorem reversible_price_zero (C : FinCfg) (c : Nat) : C.price c false = 0 := rfl

/-- The price is linear in the erased bits. -/

theorem price_linear (C : FinCfg) (c : Nat) : C.price c true = C.erasedBits * c := rfl

TRACTATUS VERITATIS TRISDUCTIVUS

Proof of Least erasure

Topics

Archive