pith. sign in
module module high

IndisputableMonolith.NumberTheory.RSPhysicalThesisDecomposition

show as:
view Lean formalization →

This module decomposes the data supporting the RS Physical Thesis into separate ledger components drawn from prime atoms, Euler partitions, completed zeta, argument principle sensors, and boundary transport. It acts as the intermediate data preparation layer in the RH-from-RCL derivation. Researchers assembling the Recognition Science physical thesis cite it before the final assembly step. The module contains only data definitions and import bridges, with no internal proofs.

claimDecomposed ledger data behind the RS physical thesis, with main object $RSPhysicalThesisData$ constructed via boundary transport and related components from the RH-from-RCL route.

background

The module sits in the NumberTheory domain and organizes the RH-from-RCL route. It imports ArgumentPrincipleSensor (zeros give annular winding charge), BoundaryTransport (bridge for collapse scalar to T1-bounded Euler realizability), CompletedZetaLedger (completed-zeta functional equation as reciprocal balance law), EulerCarrierRealizability (Euler carrier as T1-bounded ledger), EulerLedgerPartition (Euler product as partition function of prime postings), PrimeLedgerAtom (primes as irreducible postings of the multiplicative ledger), and ZetaLedgerBridge.

proof idea

This is a definition module with no proofs. It structures the decomposition by importing the seven supporting modules and exposing the main data object together with its constructors from boundary transport and related ledger components.

why it matters in Recognition Science

The module supplies the decomposed data layer that feeds RSPhysicalThesisFromRCL, whose doc-comment describes it as the 'Assembly layer: the old thesis follows from the decomposed RCL ledger data.' It separates concerns in the RH-from-RCL route before final assembly and touches the open question of transporting physical content through the Euler realizability scalar.

scope and limits

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.

declarations in this module (5)