def
definition
toClassicalData
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.LogicRH_From_RCL on GitHub at line 38.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
35 t1Boundary : T1BoundaryExclusionCert
36
37/-- Forget the recovered-prime wrapper to the current decomposed data bundle. -/
38def toClassicalData (data : RSPhysicalThesisDataLogic) : RSPhysicalThesisData where
39 primeLedger := data.primeLedgerClassical
40 eulerPartition := data.eulerPartition
41 completedLedger := data.completedLedger
42 zeroDefect := data.zeroDefect
43 realizableLedger := data.realizableLedger
44 boundaryTransport := data.boundaryTransport
45 t1Boundary := data.t1Boundary
46
47/-- Build logic-aware RH decomposition data from the current boundary transport
48certificate. The only remaining obstruction is still `BoundaryTransportCert`;
49the recovered-prime ledger is no longer an extra assumption. -/
50noncomputable def logicData_of_boundaryTransport
51 (boundary : BoundaryTransportCert) : RSPhysicalThesisDataLogic where
52 primeLedgerLogic := primeLedgerLogicCert
53 primeLedgerClassical := primeLedgerCert
54 eulerPartition := eulerLedgerPartitionCert
55 completedLedger := completedZetaLedgerCert
56 zeroDefect := argumentPrincipleSensorCert
57 realizableLedger := eulerRealizableLedgerCert
58 boundaryTransport := boundary
59 t1Boundary := t1BoundaryExclusionCert
60
61/-- Logic-aware data implies the old `RSPhysicalThesis` interface. -/
62theorem rsPhysicalThesis_of_logic_data (data : RSPhysicalThesisDataLogic) :
63 RSPhysicalThesis :=
64 rsPhysicalThesis_of_data (toClassicalData data)
65
66/-- RH from RCL with a recovered-prime-ledger wrapper. Analytic boundary
67transport remains exactly the previous obstruction. -/
68theorem riemann_hypothesis_from_rcl_logicPrime