IndisputableMonolith.Gravity.SevenGaps.Gap4OperatorDecoyReceipt

declarations in this module (14)

• theorem curvedSpectrumConverges_of_coupling L43
• theorem curvedSpectrumConverges_coupling_one L50
• theorem curvedSpectrumConverges_coupling_two L57
• theorem curvedSpectrumConverges_inhabited_by_countermodels L75
• def TypedResidual_countermodel_spectrum_not_ledger_close L102
• theorem typedResidual_countermodel_spectrum_not_ledger_close L123
• theorem TypedResidual_countermodel_spectrum_not_ledger_close_closed L127
• theorem decoy_rateBound_both_couplings L133
• theorem decoy_gap4_blocker_certified L153
• def Gap4LedgerTerminalGuard L176
• theorem gap4LedgerTerminalGuard L182
• structure Gap4OperatorDecoyReceiptStatus L188
• def gap4OperatorDecoyReceiptStatus L200
• theorem gap4OperatorDecoyReceiptStatus_flags L207