Riemann–Hodge Program — Open Boundary and Negative Knowledge
Evidence-scoped account of what the current Riemann and Hodge repository establishes locally and what remains open globally.
Riemann–Hodge Program: Open Boundary
The central editorial rule for this research is simple: a verified local identity is not automatically a proof of a global conjecture. The repository makes that boundary explicit.
What is supported by repository evidence
- Algebraic identities such as the involution and fixed-locus calculations for the mirror map are formalized in Lean modules.
- Several differential, symplectic, spectral, wavelet, and cohomological statements are represented as formal modules or tested computationally under their declared assumptions.
- The Hodge cluster includes Gauss–Manin/Picard–Fuchs, period-matrix, leafwise Dolbeault, and Hodge-star constructions.
- The repository records numerical suites and formal artifacts as evidence attached to particular statements, not as a substitute for the missing global construction.
Negative knowledge
The repository records obstruction and falsification results that narrow the space of valid arguments:
- Reflection symmetry and local potential properties admit synthetic countermodels with off-line zeros.
- Local isolation or non-ramification near a critical-line zero does not exclude zeros elsewhere.
- A spectral operator with real-part confinement is insufficient until its spectrum is rigorously identified with the nontrivial zeros of the Riemann zeta function.
- Hodge-theoretic or noncommutative structures require a precise global object and compatibility maps before they can carry a claim about RH.
Formalization status
The source repository's own rules define a theorem as verified only when it is kernel-checked without sorryAx or custom axioms. At the same time, the current checkpoint is marked as a historical unreviewed baseline: no reviewed Git head, accepted delta, or accepted reviewer verdict is recorded. Public summaries should therefore preserve both facts:
- formal artifacts may contain kernel-checked statements within their local scope;
- the campaign-wide synthesis and the global Riemann Hypothesis implication remain unaccepted and open.
Remaining bridge
The current research boundary is the global arithmetic identification: construct and validate a foliated or spectral-geometric space whose closed-orbit data, prime contribution, Archimedean regularization, and spectral zeros agree in one rigorous object. The repository names this as an open proof obligation rather than silently promoting it to a theorem.