module module

`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCMonotoneDAlembert`

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.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Cost.FunctionalEquation module_import

declarations in this module (18)

theorem monotone_additive_isLinear L63
theorem monotone_additive_nonneg_isLinear L125
theorem dAlembert_duplication L195
theorem dAlembert_ge_one_of_monotone L211
theorem dAlembert_prod L221
theorem dAlembert_diff_sq L236
theorem dAlembert_diff_eq_of_monotone L263
theorem dAlembert_add_of_monotone L303
theorem dAlembert_S_add_of_monotone L320
theorem phi_mul_of_monotone L355
theorem dAlembert_cosh_of_monotone L381
theorem composition_law_monotone_forces_cosh_family L465
theorem cosh_scale_curvature L501
theorem H_jcost_eq_cosh L517
theorem cosh_mul_monotoneOn L524
theorem about L534
theorem H_jcost_monotoneOn L536
theorem jcost_forced_by_order L555