module module

`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCalibrationTarget`

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 (4)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaRealCalibration module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCalibrationIndependence module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCChainBridge module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCShrunkCertificate module_import

declarations in this module (7)

theorem logCurvature L76
theorem clog_inj L100
theorem curvature_one_iff_J L115
theorem costLambda_one_eq_J L128
theorem calibration_unit_is_a_gauge L137
theorem gauge_action_transitive L147
theorem cost_freedom_is_one_real_torsor L163