module module

`IndisputableMonolith.Verification.T5.LedgerCost`

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.Verification.T5.ConstraintForcing module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Recognition module_import
IndisputableMonolith.RecogSpec.Core module_import

declarations in this module (17)

structure LedgerPosting L69
structure LedgerCostFunctional L117
theorem symmetry_forced_from_double_entry L147
theorem unit_forced_from_identity_posting L192
lemma log_ratio_additive L239
structure LedgerCompatible L258
theorem ledger_forces_t5_constraints L273
def CoshAddFromLedger L303
def aczel_theorem_3_1_3_hypothesis L324
def quadraticWitness L334
lemma quadraticWitness_even L336
lemma quadraticWitness_zero L339
lemma quadraticWitness_continuous L342
lemma quadraticWitness_deriv L345
lemma quadraticWitness_second_deriv L352
lemma quadraticWitness_not_coshAdd L357
theorem aczel_hypothesis_refuted L368