module module

`IndisputableMonolith.Foundation.LedgerToFactorization`

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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.LedgerCompositionToJCost module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.DAlembert.FactorizationForcing module_import
IndisputableMonolith.Foundation.RecognitionLedgerFloor module_import

declarations in this module (46)

theorem monotone_additive_isLinear L26
theorem antitone_additive_isLinear L92
theorem additive_nonnegOnNonneg_isMonotone L114
structure LedgerLinearResponse L133
structure FreeLedgerCombinerSemantics L150
structure PrimitiveLedgerPostingSemantics L171
theorem primitiveLedgerPosting_forces_rightPostedAdditive L190
theorem freeLedgerCombinerSemantics_from_primitiveLedgerPosting L212
structure DiscreteLedgerPostingSemantics L229
theorem discreteLedgerPosting_from_primitiveLedgerPosting L246
structure RationalLedgerPostingSemantics L277
theorem discreteLedgerPosting_forces_natAffineResponse L295
theorem primitiveLedgerPosting_forces_natAffineResponse L326
theorem rclCombiner_discreteLedgerPostingSemantics L335
theorem rclCombiner_primitiveLedgerPostingSemantics L351
theorem ledgerLinearResponse_from_rationalLedgerPosting L367
theorem rclCombiner_rationalLedgerPostingSemantics L398
theorem rationalLedgerPosting_iff_ledgerLinearResponse L419
theorem ledgerLinearResponse_from_free_ledger L446
theorem ledgerLinearResponse_from_primitiveLedgerPosting L482
theorem ledgerLinearResponse_from_primitiveLedgerPosting_monotone L497
theorem ledgerLinearResponse_from_primitiveLedgerPosting_nonneg L528
theorem ledgerLinearResponse_from_primitiveLedgerPosting_directional L557
theorem freeLedgerCombinerSemantics_iff_ledgerLinearResponse L589
theorem rightAffine_of_ledgerLinearResponse L616
theorem factorizationGate_of_ledgerLinearResponse L624
theorem ledgerLinearResponse_forces_rcl L634
theorem factorizationGate_of_primitiveLedgerPosting L643
theorem primitiveLedgerPosting_forces_rcl L652
theorem factorizationGate_of_primitiveLedgerPosting_monotone L662
theorem primitiveLedgerPosting_monotone_forces_rcl L672
theorem factorizationGate_of_primitiveLedgerPosting_nonneg L682
theorem primitiveLedgerPosting_nonneg_forces_rcl L694
theorem factorizationGate_of_primitiveLedgerPosting_directional L704
theorem primitiveLedgerPosting_directional_forces_rcl L716
theorem ledgerCost_le_add_right L728
theorem rclCombiner_postingNonneg L741
theorem rclCombiner_directional L754
theorem rclCombiner_ledgerLinearResponse L769
theorem rclCombiner_freeLedgerSemantics L785
theorem ledgerLinearResponse_iff_rcl L805
theorem factorizationGate_of_rationalLedgerPosting L836
theorem rationalLedgerPosting_forces_rcl L843
theorem rationalLedgerPosting_iff_rcl L851
theorem freeLedgerCombinerSemantics_iff_rationalLedgerPosting L861
theorem freeLedgerCombinerSemantics_iff_rcl L874