pith. sign in
module module high

IndisputableMonolith.NumberTheory.RSPhysicalThesisDecomposition

show as:
view Lean formalization →

This module decomposes the data supporting the old RS physical thesis into separate ledger components drawn from prime atoms, Euler partitions, completed zeta, argument principle sensors, Euler carrier realizability, boundary transport, and zeta bridges. Researchers following the RH-from-RCL derivation cite these certificates to inspect each bridge independently. The module consists of data definitions and extraction lemmas that repackage results from UnifiedRH.lean into the modular file layout.

claimThe decomposed data is the structure $RSPhysicalThesisData$ equipped with extraction maps $rsPhysicalThesisData_of_boundaryTransport$, $no_strip_zeros_of_decomposed_data$, $rsPhysicalThesis_of_no_strip_zeros$, and $rsPhysicalThesis_of_data$ that isolate the prime-ledger, Euler-partition, zeta-balance, winding-charge, and collapse-transport certificates.

background

The module sits inside the RH-from-RCL derivation plan. It imports seven sibling modules whose doc-comments define the arithmetic ledger: primes are the irreducible postings of the multiplicative positive-integer ledger; the Euler product is the partition function of independent prime-ledger postings; the completed zeta supplies the reciprocal balance law; zeros supply annular winding charge via the argument principle; the Euler carrier is realized as a T1-bounded ledger; boundary transport carries the collapse scalar to the T1-bounded Euler realizability scalar; and the zeta ledger bridge closes the arithmetic side.

proof idea

This is a definition module, no proofs. It declares the record $RSPhysicalThesisData$ and supplies one-line extraction lemmas that pull the relevant certificates from the imported modules (PrimeLedgerAtom, EulerLedgerPartition, CompletedZetaLedger, ArgumentPrincipleSensor, EulerCarrierRealizability, BoundaryTransport, ZetaLedgerBridge) into the new layout.

why it matters in Recognition Science

The module supplies the decomposed ledger data required by the downstream assembly layer RSPhysicalThesisFromRCL, whose doc-comment states that the old thesis follows from the decomposed RCL ledger data. It therefore completes the decomposition step that precedes the final assembly of the physical thesis from the recognition composition law.

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)