IndisputableMonolith.RecogSpec.Spec

declarations in this module (52)

• def speedFromAnchors L17
• def unitsFromAnchors L21
• lemma speedFromAnchors_of_eq_zero L31
• lemma speedFromAnchors_of_ne_zero L34
• lemma unitsFromAnchors_tau0 L37
• lemma unitsFromAnchors_ell0 L40
• lemma unitsFromAnchors_c L43
• def Calibrated L48
• lemma unitsFromAnchors_calibrated L51
• def UniqueCalibration L58
• def MeetsBands L64
• def AnchorsEqv L74
• lemma AnchorsEqv_refl L78
• lemma AnchorsEqv_symm L82
• lemma AnchorsEqv_trans L86
• instance anchorsSetoid L91
• def AnchorsQuot L96
• lemma anchors_eq_of_same_speed L103
• theorem anchors_unique_up_to_units L110
• def alphaDefault L132
• def massRatiosDefault L135
• def mixingAnglesDefault L139
• def g2Default L143
• lemma phiClosed_one_div L147
• lemma phiClosed_one_div_pow L152
• lemma phiClosed_alphaDefault L158
• def kGateWitness L168
• theorem kGate_from_units L175
• def eightTickWitness L180
• theorem eightTick_from_TruthCore L183
• def bornHolds L187
• theorem born_from_TruthCore L190
• def UD_explicit L195
• def dimlessPack_explicit L212
• def PackMatches L223
• def MatchesEval L237
• lemma matchesEval_explicit L240
• lemma uniqueCalibration_any L247
• def Inevitability_dimless L259
• def Inevitability_absolute L267
• def Recognition_Closure L273
• theorem recognition_closure_from_inevitabilities L276
• lemma meetsBands_any_of_eval L284
• lemma meetsBands_any_of_eval_rescaled L290
• lemma meetsBands_any_param L299
• def meetsBandsCheckerP L306
• lemma meetsBandsCheckerP_invariant L309
• lemma meetsBands_any_of_checker L314
• lemma meetsBands_any_default L320
• theorem absolute_layer_any L329
• theorem absolute_layer_invariant L335
• theorem absolute_layer_from_eval_invariant L344