IndisputableMonolith.Gravity.SevenGaps.RecognitionRatioSubstrateBlocker

declarations in this module (14)

• structure DeficitSourceConstitutiveCoupling L52
• def deficitSourceAction L66
• theorem deficitSourceAction_eq_jcost_sum L75
• def ratioBridgeFromDeficitSourceCoupling L88
• theorem recognition_ratio_derived_of_deficit_source_coupling L101
• theorem deficitSourceCoupling_logRatio_eq_minimizer_strain L111
• def signBlindBareLedger L128
• theorem recognitionLedger_cost_ext L134
• theorem signBlindBareLedger_neg_eq L145
• def RecoversSignedSourceFromBareLedger L171
• theorem no_bare_ledger_selector_recovers_signed_source L181
• theorem nontrivial_source_backed_family_exists L199
• structure RecognitionRatioSubstrateBlockerCertificate L220
• theorem recognition_ratio_derived_bare_ledger_terminal L256