module
module
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Continuum.ForcedJOnCompletion
show as:
view Lean formalization →
depends on (4)
-
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Continuum.CharacterRigidityForcing -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCostOnField -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCompleteOrderedField
declarations in this module (9)
-
theorem
completion_R_delta_exists -
theorem
canonical_cost_is_J_formula -
theorem
canonical_cost_reciprocal_symmetric -
theorem
generated_cost_formula -
theorem
calibrated_character_forces_J -
theorem
calibration_propagates_to_cyclic_subgroup -
theorem
forced_J_on_completion -
theorem
forced_cost_exists_on_completion -
def
target_global_identity_from_one_point_calibration