pith. sign in
module module high

IndisputableMonolith.NumberTheory.RH_From_RCL

show as:
view Lean formalization →

RH_From_RCL assembles the Riemann hypothesis from decomposed Recognition Composition Law ledger data together with boundary transport. Researchers tracing the RS derivation of analytic number theory results cite this module as the bridge between the physical thesis and the full RH certificate. The structure composes the honest phase admissibility predicate with the RCL assembly layer and the existing RH chain.

claimThe Riemann hypothesis follows from the decomposed RCL ledger satisfying the honest phase admissibility predicate together with boundary transport conditions.

background

This module operates in the NumberTheory domain of Recognition Science. It imports HonestPhaseAdmissibility, whose doc-comment states that Route C narrows the analytic RH target to honest zeta-derived phase data and proves the admissibility predicate equivalent to the charge-zero conclusion. It further imports RH_Certificate, which assembles every link in the RS chain for the Riemann Hypothesis, and RSPhysicalThesisFromRCL, described as the assembly layer where the old thesis follows from the decomposed RCL ledger data.

proof idea

This is an assembly module with no new proofs. It imports the three upstream modules (HonestPhaseAdmissibility, RH_Certificate, RSPhysicalThesisFromRCL) and composes their results to obtain RH from the RCL decomposition plus boundary transport.

why it matters in Recognition Science

The module supplies the core RH derivation from RCL data that is then wrapped by the downstream LogicRH_From_RCL module for the recovered-prime-ledger version. It completes the step connecting the physical thesis from RCL to the analytic RH certificate in the Recognition Science chain.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (3)