theorem
proved
c1_c3_protocol_distinct
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.OptionAEmpiricalProtocol on GitHub at line 88.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
85 intro hp
86 exact h (protocolSpec_injective hp)
87
88theorem c1_c3_protocol_distinct :
89 protocolSpec .c1CognitiveTensor ≠ protocolSpec .c3OncologyTensor := by
90 exact protocolSpec_ne_of_ne (by decide)
91
92theorem c3_c5_protocol_distinct :
93 protocolSpec .c3OncologyTensor ≠ protocolSpec .c5AttentionTensor := by
94 exact protocolSpec_ne_of_ne (by decide)
95
96theorem c5_c8_protocol_distinct :
97 protocolSpec .c5AttentionTensor ≠ protocolSpec .c8MillerSpan := by
98 exact protocolSpec_ne_of_ne (by decide)
99
100/-- A theorem bundle is empirically covered if every combination has a falsifier
101protocol. -/
102def EmpiricallyCovered : Prop :=
103 ∀ c : CombinationID, ProtocolFalsifiable c
104
105theorem empiricallyCovered : EmpiricallyCovered :=
106 protocolFalsifiable_all
107
108theorem c1_protocol :
109 ProtocolFalsifiable .c1CognitiveTensor :=
110 protocolFalsifiable_all .c1CognitiveTensor
111
112theorem c3_protocol :
113 ProtocolFalsifiable .c3OncologyTensor :=
114 protocolFalsifiable_all .c3OncologyTensor
115
116theorem c5_protocol :
117 ProtocolFalsifiable .c5AttentionTensor :=
118 protocolFalsifiable_all .c5AttentionTensor