IndisputableMonolith.NumberTheory.ProxyPhysicalizationBridge

declarations in this module (13)

• def ProxyPhysicalizationBridge L38
• theorem physicallyExists_of_ProxyPhysicalizationBridge L48
• def ZeroInducedProxyPhysicalizationBridge L57
• theorem rsPhysicalThesis_of_ZeroInducedProxyPhysicalizationBridge L64
• theorem rh_from_ZeroInducedProxyPhysicalizationBridge L73
• theorem proxyPhysicalizationBridge_iff_physicallyExists L93
• theorem proxyPhysicalizationBridge_iff_charge_zero L105
• theorem proxyPhysicalizationBridge_of_charge_zero L111
• theorem not_proxyPhysicalizationBridge_of_charge_ne_zero L117
• theorem zeroInducedBridge_iff_rsPhysicalThesis L126
• theorem zeroInducedBridge_iff_no_strip_zeros L137
• theorem zeroInducedBridge_of_rh L151
• theorem zeroInducedBridge_iff_rh L175