RSPhysicalThesisDataLogic
plain-language theorem explainer
RSPhysicalThesisDataLogic packages eight certificates into a single record that supplies a recovered-prime version of the RH decomposition data. Number theorists extending the RH-from-RCL argument would cite this structure when they need to track the LogicNat-derived prime ledger alongside the classical analytic components. The definition is a plain record type that aggregates the certificates without adding relations or proof obligations among them.
Claim. A record type containing a certificate that recovered-prime atoms satisfy the classical primality predicate and transport to the classical ledger, a classical prime ledger certificate, an Euler product convergence certificate on Re(s) > 1, a completed zeta ledger certificate asserting balanced arithmetic and critical-line uniqueness, an argument-principle sensor certificate witnessing nonzero phase-family data, an Euler realizability certificate, a boundary-transport certificate, and a T1-boundary-exclusion certificate.
background
The LogicRH_From_RCL module keeps the analytic zeta, xi, and winding machinery exactly as supplied by Mathlib while replacing the arithmetic ledger hook with a recovered-prime certificate. The local setting is therefore a wrapper that transports the LogicNat-based ledger back to the classical PrimeLedgerCert required by the existing RH assembly. PrimeLedgerLogicCert records the atom-to-prime equivalence and the transport map; BoundaryTransportCert supplies the EulerBoundaryBridgeAssumption that remains the principal obstruction; CompletedZetaLedgerCert asserts both balanced arithmetic on the completed zeta and that every critical line point satisfies Re(s) = 1/2; ArgumentPrincipleSensorCert witnesses a defect sensor carrying genuine zeta-derived phase-family data; EulerRealizableLedgerCert asserts admissibility and physical realizability for every defect sensor.
proof idea
This declaration is a structure definition that directly assembles the eight named certificates into a single record type with no additional proof steps or lemmas applied.
why it matters
The structure supplies the logic-aware data bundle consumed by rsPhysicalThesis_of_logic_data, which recovers the classical RSPhysicalThesis interface, and by logicData_of_boundaryTransport, which constructs instances once the boundary-transport certificate is supplied. It therefore isolates the recovered-prime ledger component while leaving the analytic boundary-transport obstruction explicit. In the Recognition Science setting this step closes the arithmetic side of the RH-from-RCL decomposition, keeping the RCL-derived forcing chain and the eight-tick octave machinery compatible with the classical zeta stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.