rsPhysicalThesis_of_data
plain-language theorem explainer
Decomposed ledger certificates imply the RS Physical Thesis. Number theorists deriving the Riemann Hypothesis from Recognition Science axioms cite this to connect explicit arithmetic data to the physical existence requirement. The proof is a one-line composition: it first extracts the no-strip-zeros property from the data bundle and then applies the vacuous lifting to the thesis interface.
Claim. Given a structure containing a prime ledger certificate, an Euler ledger partition certificate, a completed zeta ledger certificate, an argument principle sensor certificate, an Euler realizable ledger certificate, a boundary transport certificate, and a T1 boundary exclusion certificate, every nontrivial zero $ρ$ of the Riemann zeta function with $1/2 < Re(ρ) < 1$ satisfies that the associated defect sensor is physically realized.
background
The module replaces the opaque RSPhysicalThesis dependency with a structured bundle of the exact ingredients needed for the RH proof. RSPhysicalThesisData collects seven certificates: primeLedger, eulerPartition, completedLedger, zeroDefect, realizableLedger, boundaryTransport, and t1Boundary. The upstream result no_strip_zeros_of_decomposed_data establishes that boundary transport rules out every right-half strip zero. The companion theorem rsPhysicalThesis_of_no_strip_zeros shows that the absence of such zeros makes the RSPhysicalThesis hold vacuously.
proof idea
The proof is a one-line wrapper that applies rsPhysicalThesis_of_no_strip_zeros to the output of no_strip_zeros_of_decomposed_data applied to the input data bundle.
why it matters
This declaration bridges the decomposed data structure to the original RSPhysicalThesis interface used in the RH argument. It is invoked by rsPhysicalThesis_of_logic_data and rsPhysicalThesis_from_boundaryTransport, which recover the thesis from logic-aware data and from boundary transport alone. In the Recognition Science framework it supplies the single non-mechanical ingredient asserting that zeros in the critical strip correspond to physical recognition events on the arithmetic ledger, advancing the chain from the Recognition Composition Law toward the Riemann Hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.