theorem
proved
c1_protocol
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.OptionAEmpiricalProtocol on GitHub at line 108.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
127
128structure EmpiricalProtocolCert where
129 all_covered : EmpiricallyCovered
130 c1_covered : ProtocolFalsifiable .c1CognitiveTensor
131 c3_covered : ProtocolFalsifiable .c3OncologyTensor
132 c5_covered : ProtocolFalsifiable .c5AttentionTensor
133 c8_covered : ProtocolFalsifiable .c8MillerSpan
134 unique_protocol : ∀ c : CombinationID, ∃! p : ProtocolSpec, ProtocolMatches c p
135 protocol_injective : Function.Injective protocolSpec
136 c3_unique_protocol : ∃! p : ProtocolSpec, ProtocolMatches .c3OncologyTensor p
137 protocol_eq_iff : ∀ a b : CombinationID, protocolSpec a = protocolSpec b ↔ a = b
138 c1_c3_distinct : protocolSpec .c1CognitiveTensor ≠ protocolSpec .c3OncologyTensor