rsPhysicalThesis_from_boundaryTransport
plain-language theorem explainer
Given a boundary transport certificate, the RS physical thesis follows from the decomposed RCL ledger data. Number theorists deriving the Riemann hypothesis via recognition science cite this to link the physical boundary bridge to the arithmetic ledger. The proof is a direct term composition that builds the data bundle from the certificate and then extracts the thesis.
Claim. If a boundary transport certificate exists, then every nontrivial zero $ρ$ of the Riemann zeta function with $1/2 < ρ.re < 1$ corresponds to a physically existing zeta defect sensor.
background
RSPhysicalThesis is the proposition that every nontrivial zero of riemannZeta in the critical strip corresponds to a physical recognition event, so the associated zetaDefectSensor satisfies PhysicallyExists. BoundaryTransportCert is the structure containing an EulerBoundaryBridgeAssumption; it encodes the remaining physical bridge that realized defect collapse must transport to the Euler ledger boundary. The module assembles the old thesis from decomposed RCL data, where rsPhysicalThesisData_of_boundaryTransport produces the explicit bundle of primeLedgerCert, eulerLedgerPartitionCert, completedZetaLedgerCert, and argumentPrincipleSensorCert.
proof idea
The proof is a one-line term that applies rsPhysicalThesisData_of_boundaryTransport to the input boundary certificate and then feeds the resulting data bundle to rsPhysicalThesis_of_data.
why it matters
This theorem completes the assembly layer that lets riemann_hypothesis_from_rcl derive RiemannHypothesis from the decomposed RCL ledger data plus the boundary transport certificate. It supplies the final link from the physical boundary bridge to the arithmetic thesis that underpins the no-strip-zeros step. The result closes one segment of the RCL-to-RH chain while leaving the boundary transport certificate as the sole remaining hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.