IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCalibrationIndependence

declarations in this module (16)

• def costLambda L55
• theorem costLambda_eq_cosh L59
• theorem costLambda_unit0 L71
• theorem costLambda_symm L76
• theorem costLambda_isCostRequirements L85
• theorem costLambda_continuousOn L92
• theorem costLambda_one_eq_Jcost L104
• theorem costLambda_inj L113
• theorem calibration_unit_not_forced_by_cost_laws L134
• theorem G_costLambda L167
• theorem costLambda_coshAddIdentity L174
• theorem costLambda_isReciprocalCost L183
• theorem costLambda_isNormalized L187
• theorem costLambda_satisfiesCompositionLaw L191
• theorem costLambda_isCalibrated_iff L197
• theorem calibration_is_the_only_hypothesis_pinning_J L213