module
module
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaRealCalibration
show as:
view Lean formalization →
used by (4)
-
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaNativeAnalysis -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaNativeStrongClosure -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ObjecthoodRegistry -
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PhysicalOneActCalibration
depends on (1)
declarations in this module (10)
-
def
oneActCurvature -
theorem
oneActCurvature_eq -
theorem
unit_forced_by_one_act -
theorem
discrete_does_not_force_unit -
theorem
calibration_is_one_continuum_act -
structure
NormalizedOneActInterface -
theorem
normalized_interface_forces_J -
theorem
calibration_datum_necessary_and_sufficient -
def
canonicalInterface -
theorem
calibration_gap_closed_by_normalized_interface