module module

`IndisputableMonolith.Gravity.SevenGaps.Gap5ReparamAttackOnConstraintSector`

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.Gravity.SevenGaps.Gap5O6ChartInvariant module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.HKTKineticFromRecognitionCost module_import

declarations in this module (29)

theorem jcost_rcl L119
theorem compositionLaw_forces_unit_weight_generic L133
theorem compositionLaw_forces_unit_weight_is_an_instance L153
theorem satisfiesCompositionLaw_comp_pow L166
def powCost L177
theorem powCost_one L179
theorem powCost_satisfiesCompositionLaw L183
theorem powCost_two_ne_Jcost L189
theorem Jcost_pos_of_one_lt L196
theorem powCost_forces_unit_weight L206
def oscCost L242
theorem oscCost_satisfiesCompositionLaw L247
theorem oscCost_neg_at_exp_pi L258
theorem oscCost_forces_unit_weight L264
theorem oscCost_not_quadratic_in_log_chart L277
theorem G_powCost L296
theorem deriv2_G_powCost L302
theorem isCalibrated_powCost_iff L324
def CalibratedWeightAtTwo L341
theorem calibratedWeightAtTwo_forces_one L345
theorem rclWeight_zero L352
theorem not_calibratedWeightAtTwo_zero L358
theorem calibratedWeightAtTwo_ne_rclWeight L365
theorem falsifier_as_printed_is_met L383
theorem chart_alone_forces_the_cost L428
theorem Jlog_is_the_C_two_solution L447
theorem profile_clause_solution_set_is_a_scale_family L457
def constraint_sector_recognition_load_is_quadraticity_not_unit_weight L501
theorem constraint_sector_recognition_load_is_quadraticity_not_unit_weight_holds L512