module
module
IndisputableMonolith.Gravity.Analysis.RecognitionMeshDualEntryCoupling4D
show as:
view Lean formalization →
used by (2)
depends on (3)
declarations in this module (13)
-
def
meshDualEntry -
def
meshDualEntrySource -
theorem
meshDualEntrySource_eq -
def
meshDualEntryCoupling -
theorem
mesh_recognition_ratio_derived -
def
TypedResidual_DeficitSourceConstitutiveCoupling_from_enrichment -
theorem
typedResidual_DeficitSourceConstitutiveCoupling_from_enrichment_closed -
theorem
TypedResidual_DeficitSourceConstitutiveCoupling_from_enrichment_closed -
theorem
decoy_magnitude_only_ne_mesh_geometricDeficit -
theorem
adversarial_decoys_mesh_dual_entry -
structure
RecognitionMeshDualEntryCoupling4DStatus -
def
recognitionMeshDualEntryCoupling4DStatus -
theorem
recognitionMeshDualEntryCoupling4DStatus_flags