module module

`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Continuum.CharacterRigidityForcing`

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.Continuum.ForcedJOnCompletion module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness module_import

declarations in this module (14)

def CharacterCalibratedAt L41
theorem character_mul_toRat L47
theorem character_one_toRat L55
theorem character_recip_toRat L63
theorem calibrated_one L73
theorem calibrated_mul L80
theorem calibrated_recip L89
theorem calibrated_square L98
theorem onRatioOrbit_crossEq L107
theorem character_trace_rigid L115
theorem costFromCharacter_rigid L128
theorem doubledTrace_character_rigid L136
theorem prime_calibration_forces_identity_on_direction L155
def target_OnePointCalibrationForcesGlobalIdentity L175