RSPhysicalThesisData
plain-language theorem explainer
RSPhysicalThesisData assembles seven upstream certificates into a single bundle that replaces the prior opaque RSPhysicalThesis dependency for the Riemann Hypothesis argument. Number theorists working from the Recognition Composition Law to classical data would cite this structure to access the decomposed physical ingredients. The declaration is a plain structure definition that directly packages the certificates with no additional lemmas or reductions.
Claim. A structure whose fields are certificates for the prime ledger, the Euler ledger partition, the completed zeta ledger, the argument-principle zero-defect sensor, the Euler realizable ledger, boundary transport, and the T1 boundary exclusion.
background
The module RS Physical Thesis Decomposition replaces the single opaque RSPhysicalThesis interface with an explicit bundle of the exact certificates needed for the RH proof. Each field is drawn from an upstream certificate: PrimeLedgerCert records the prime ledger atom, EulerLedgerPartitionCert records the Euler partition, CompletedZetaLedgerCert asserts a balanced arithmetic ledger on the completed Riemann zeta together with critical-line uniqueness, ArgumentPrincipleSensorCert witnesses a defect sensor carrying genuine zeta-derived phase-family data, EulerRealizableLedgerCert asserts admissibility and physical realizability for every defect sensor, BoundaryTransportCert supplies the Euler boundary bridge assumption, and T1BoundaryExclusionCert excludes the T1 boundary case.
proof idea
Structure definition that directly assembles the seven named certificates; no tactics or lemmas are applied.
why it matters
The structure is the current explicit data bundle that feeds rsPhysicalThesis_of_data, which recovers the old RSPhysicalThesis interface, and is consumed by toClassicalData in LogicRH_From_RCL. It therefore supplies the decomposed physical thesis required for the RH argument from the Recognition Composition Law. The construction closes the scaffolding gap left by the earlier monolithic dependency while leaving the boundary-transport bridge as the remaining explicit hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.