theorem
proved
c5_c8_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 96.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
119
120theorem c8_protocol :
121 ProtocolFalsifiable .c8MillerSpan :=
122 protocolFalsifiable_all .c8MillerSpan
123
124theorem c3_uniqueProtocol :
125 ∃! p : ProtocolSpec, ProtocolMatches .c3OncologyTensor p :=
126 uniqueProtocolSpec .c3OncologyTensor