theorem
proved
c5_protocol
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.OptionAEmpiricalProtocol on GitHub at line 116.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
139 c3_c5_distinct : protocolSpec .c3OncologyTensor ≠ protocolSpec .c5AttentionTensor
140 c5_c8_distinct : protocolSpec .c5AttentionTensor ≠ protocolSpec .c8MillerSpan
141
142def empiricalProtocolCert : EmpiricalProtocolCert where
143 all_covered := empiricallyCovered
144 c1_covered := c1_protocol
145 c3_covered := c3_protocol
146 c5_covered := c5_protocol