logicData_of_boundaryTransport
plain-language theorem explainer
Researchers deriving the Riemann hypothesis from the Recognition Composition Law with a recovered-prime ledger cite this definition to assemble the full logic-aware decomposition data. It accepts a boundary transport certificate and populates the RSPhysicalThesisDataLogic structure by direct assignment of the logic prime ledger certificate, the classical prime ledger certificate, the Euler partition certificate, the completed zeta ledger certificate, the argument principle sensor certificate, the Euler realizability certificate, and the T1-exc1
Claim. Given a boundary transport certificate $b$, the RH decomposition data with recovered prime ledger is the structure whose recovered-prime component is the logic certificate, classical prime ledger is the standard certificate, Euler partition is the structural certificate, completed zeta ledger is the balanced certificate, zero defect is the argument-principle sensor certificate, realizable ledger is the Euler realizability certificate, boundary transport is $b$, and T1 boundary is the exclusion certificate.
background
The module supplies a recovered-prime-ledger wrapper for the RH-from-RCL decomposition. Analytic zeta, xi, and winding infrastructure stays Mathlib-backed; only the arithmetic ledger hook is replaced by a certificate that includes the recovered-prime ledger and transports back to the classical PrimeLedgerCert. RSPhysicalThesisDataLogic is the structure whose fields are primeLedgerLogic (recording recovery from LogicNat and compatibility with the classical ledger), primeLedgerClassical, eulerPartition, completedLedger, zeroDefect, realizableLedger, boundaryTransport, and t1Boundary. BoundaryTransportCert is the main remaining physical bridge: realized defect collapse must transport to the actual Euler ledger boundary.
proof idea
The definition is a direct record construction that assigns each field of RSPhysicalThesisDataLogic from the corresponding certificate: primeLedgerLogic from primeLedgerLogicCert, primeLedgerClassical from primeLedgerCert, eulerPartition from eulerLedgerPartitionCert, completedLedger from completedZetaLedgerCert, zeroDefect from argumentPrincipleSensorCert, realizableLedger from eulerRealizableLedgerCert, boundaryTransport from the input parameter, and t1Boundary from t1BoundaryExclusionCert.
why it matters
This definition supplies the input to riemann_hypothesis_from_rcl_logicPrime, which states that the Riemann hypothesis follows from the Recognition Composition Law once boundary transport is given. It removes the recovered-prime ledger as a separate assumption by incorporating the logic prime ledger certificate. In the framework this advances the RH-from-RCL path by closing the arithmetic ledger gap while leaving the physical boundary transport as the remaining obstruction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.