def
definition
branchSelectionCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.BranchSelection on GitHub at line 206.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
additive_branch_not_coupling -
branch_selection -
BranchSelectionCert -
isCouplingCombiner_iff_interactionDefect_nonzero -
RCLCombiner_isCoupling_iff -
separatelyAdditive_iff_interactionDefect_zero
used by
formal source
203 additive_branch_excluded :
204 ¬ IsCouplingCombiner (RCLCombiner 0)
205
206def branchSelectionCert : BranchSelectionCert where
207 separately_additive_iff_defect_zero :=
208 fun P => separatelyAdditive_iff_interactionDefect_zero P
209 coupling_iff_defect_nonzero :=
210 fun P => isCouplingCombiner_iff_interactionDefect_nonzero P
211 rcl_coupling_iff := RCLCombiner_isCoupling_iff
212 bilinear_branch_forced := branch_selection
213 additive_branch_excluded := additive_branch_not_coupling
214
215theorem branchSelectionCert_inhabited : Nonempty BranchSelectionCert :=
216 ⟨branchSelectionCert⟩
217
218end BranchSelection
219end Foundation
220end IndisputableMonolith