module module

`IndisputableMonolith.Foundation.LedgerComparisonToComposition`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

declarations in this module (13)

def compRatio L65
theorem compRatio_pos L71
theorem compRatio_swap L77
theorem compRatio_self L83
theorem comparison_cost_swap_invariant L90
theorem comparison_cost_self_zero L98
def CombinationCostDetermined L110
theorem hasMultiplicativeConsistency_iff_costDetermined L122
theorem hasMultiplicativeConsistency_iff_exists_composesThrough L146
theorem jcost_combinationCostDetermined L156
theorem ledgerComparison_forces_jcost L170
structure LedgerComparisonCertificate L183
theorem ledgerComparisonCertificate L203