theorem
proved
empiricallyCovered
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.OptionAEmpiricalProtocol on GitHub at line 105.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
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