Skip to content

v0.11.0 — the order ≤ on constructive ℝ (foundation for the transcendentals)

Choose a tag to compare

View all tags
@afflom afflom released this 06 Jun 19:19
v0.11.0
5ee784f

v0.11.0 — the order ≤ on constructive ℝ

The foundation every transcendental (exp, cos/sin, log) rests on, built the Bishop way (F1Square/Analysis/ROrder.lean):

x ≤ y :⟺ ∀ n, xₙ ≤ yₙ + 2/(n+1).

  • Order laws: Rle_refl, Rle_of_Req (≈ ⟹ ≤), Rle_antisymm (x ≤ y and y ≤ x ⟹ x ≈ y), and Rle_trans — the one genuine limiting step: chaining x ≤ y ≤ z through an auxiliary index m gives xₙ ≤ zₙ + 2/(n+1) + 6/(m+1) for every m, and the generalized Archimedean lemma Qarch_gen kills the 6/(m+1) tail (the argument behind Req_trans).
  • Rnonneg canonicalized (Bishop x ≥ 0), with Rle_zero_of_Rnonneg. New ℚ signed-bound helpers; Qle_self_add/Qle_add_self moved to QOrder.
  • Honesty gate hardened to fail on duplicate proof-layer theorem short-names; coverage 288/288, enforced. Pure Lean 4, no Mathlib, no sorry; axiom-clean and choice-free; CI machine-verified green.

Concrete remaining sequence (no open +)

  • v0.12.0 — reciprocal Rinv + exp on ℝ (real powers, real exp on [0,1] via completeness, then halving/squaring).
  • v0.13.0 — cos/sin (alternating-series sandwich) + log (positivity-as-data + artanh).
  • then the next phase — ζ's continuation into the critical strip (needs complex exp/log), the genuine λₙ realizing the v0.10.0 interfaces, and the explicit-formula trace, which ends at λₙ > 0 ∀n = RH (the open frontier).

RH remains open (June 2026); no 𝔽₁-square construction exists. The crux is never asserted.

🤖 Generated with Claude Code

Assets 2
Loading