Skip to content

v0.0.1 β€” 𝔽₁-square RH research base

Choose a tag to compare

View all tags
@afflom afflom released this 06 Jun 12:01
v0.0.1
459e0e1

Initial research base for the 𝔽₁-square / Riemann Hypothesis program.

The Riemann Hypothesis remains OPEN. This release builds the research base, not a solution: the formalization compiles and states the construction problem precisely; it does not assert the crux.

Added

  • F1Square.lean β€” Lean 4 formalization of the target object Spec β„€ Γ—_{𝔽₁} Spec β„€ and its intersection theory (UOR.Bridge.F1Square), encoding each result's honest epistemic status. The RH crux (the Hodge index theorem) is encoded as universallyValid := none and is never asserted true.
  • docs/ β€” the three companion research documents: the intersection-theory specification, the missing-object-over-β„š map, and the verified characteristic-1 / tropical stack (R1–R16).
  • Lake project pinning the uor dependency to UOR-Framework v0.5.2 (392c7f91e202cf7d119997ac14497444416ed2ce) β€” the latest UOR-Framework release that ships the lean4/ library. lake build compiles cleanly; CI is green.
  • Repository infrastructure: README, CITATION.cff, CHANGELOG, .gitignore, and a lake build CI workflow.

Semantic versioning starts at v0.0.1. See CHANGELOG.md.

Assets 2
Loading