IndisputableMonolith.Verification.Necessity.RecognitionNecessity

declarations in this module (24)

• structure Observable L47
• def CanDistinguish L51
• structure ComparisonMechanism L59
• lemma recognition_event_of_states L71
• lemma nonempty_of_distinct_values L78
• def ComparisonMechanismIsRecognition L88
• theorem distinction_requires_comparison L100
• structure InternalComparison L133
• def ComparisonIsRecognition L146
• theorem MP_forbids_empty_recognition L162
• theorem recognition_must_be_nonempty L168
• theorem observables_require_distinction L178
• theorem distinction_requires_comparison_capability L191
• theorem zero_params_forces_internal_comparison L200
• theorem observables_require_recognition L216
• theorem RS_recognition_is_necessary L236
• theorem no_observables_without_recognition L247
• theorem MP_essential_for_physics L262
• theorem observables_imply_multiple_states L283
• theorem comparison_exists L297
• theorem evolve_changes_observable_implies_distinct L308
• theorem distinction_symmetric L317
• theorem measurement_is_recognition L337
• theorem classical_observation_needs_recognition L349