RHConditionalPackage
plain-language theorem explainer
RHConditionalPackage bundles classical analysis, recognition geometry, and oscillation bounds assumptions with the Riemann Hypothesis statement into one record. Number theorists working on conditional proofs of the Riemann Hypothesis under Recognition Science geometry would cite this package to supply the required hypotheses explicitly. The definition is a pure structure with four fields, each typed as True or as the RH_Statement proposition, replacing earlier unconditional axioms.
Claim. A record containing the classical analysis assumption, the recognition geometry assumption, the oscillation bounds assumption, and the statement that every non-trivial zero $ρ$ of the completed Riemann zeta function satisfies $ρ.re = 1/2$ whenever $ρ.im ≠ 0$.
background
The module defines RH_Statement as the proposition ∀ ρ : ℂ, completedRiemannZeta ρ = 0 → ρ.im ≠ 0 → ρ.re = 1/2, carrying the status of a major open Millennium problem. This package replaces prior unconditional axiom-valued functions by requiring callers to supply the three assumption fields explicitly. Upstream RH_Statement is conditional on ClassicalAnalysis ∧ RecognitionGeometry ∧ OscillationBounds, with conditional proofs available only under oscillation hypotheses.
proof idea
The declaration is a structure definition that introduces four fields: classical_assumptions, recognition_geometry_assumptions, and oscillation_bounds each of type True, plus the rh field of type RH_Statement. No lemmas or tactics are invoked; it is a direct record constructor with no computational content.
why it matters
The structure is consumed directly by the RH_conditional theorem, which extracts the rh field to recover the Riemann Hypothesis statement. It supports the legacy conditional route for RH under oscillation hypotheses, a path kept separate from the core T0-T8 forcing chain. The package keeps the open status of the Millennium problem explicit while allowing modular use of the conditional payload.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.