def
definition
coherenceExponentCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.CoherenceExponentUniqueness on GitHub at line 84.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
81 unique_at_3 : ∀ D ∈ ({1, 2, 3, 4} : Finset ℕ), k_fib D = k_int D ↔ D = 3
82 k5_forced : k_fib 3 = 5 ∧ k_int 3 = 5 ∧ k_fib 3 = k_int 3
83
84def coherenceExponentCert : CoherenceExponentCert where
85 agree_at_3 := agreement_at_3
86 both_five := both_equal_5_at_3
87 disagree_1 := disagreement_at_1
88 disagree_2 := disagreement_at_2
89 disagree_4 := disagreement_at_4
90 unique_at_3 := exponent_unique_at_D3
91 k5_forced := k5_forced_at_D3
92
93end IndisputableMonolith.Foundation.CoherenceExponentUniqueness