`h_aczel_classification_proved`

proved

show as: view math explainer →

module: IndisputableMonolith.Cost.AczelTheorem
domain: Cost
line: 452 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cost.AczelTheorem on GitHub at line 452.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 449
 450/-- **THEOREM (Aczél, PROVED)**: `H_AczelClassification` holds unconditionally.
 451    This eliminates the sole remaining foundation axiom. -/
 452theorem h_aczel_classification_proved : H_AczelClassification :=
 453  fun H h_one h_cont h_dAlembert => dAlembert_contDiff_top H h_one h_cont h_dAlembert
 454
 455-- The typeclass-parameterized `aczel_dAlembert_smooth` lives in
 456-- `IndisputableMonolith.Cost.AczelClass` and is satisfied by the
 457-- `AczelSmoothnessPackage` instance in `IndisputableMonolith.Cost.AczelProof`,
 458-- which delegates to `dAlembert_contDiff_top` above.
 459
 460end
 461
 462end FunctionalEquation
 463end Cost
 464end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.