IndisputableMonolith.Verification.T5.ConstraintForcing

declarations in this module (16)

• def RecognitionLogCost L86
• theorem recognition_exchange_invariance_axiom L90
• theorem recognition_identity_axiom L103
• def IsCostFunction L111
• theorem reciprocal_symmetry_forced L117
• theorem unit_normalization_forced L147
• theorem curvature_is_gauge_normalization L161
• theorem curvature_cancels_in_dimensionless L171
• def ExchangeInvariant L179
• def ReciprocalSymmetric L182
• def IdentityRecognitionZero L185
• def UnitNormalized L188
• theorem t5_constraints_are_forced L201
• theorem t5_constraints_forced_from_ledger L223
• theorem t5_constraints_imply_reciprocal_from_ledger L232
• theorem t5_constraints_implies_reciprocal_from_ledger L240