No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
40def k_int (D : ℕ) : ℕ := D + 2
proof body
Definition body.
41
42/-- k_fib and k_int agree at D = 3. -/
used by (9)
From the project-wide theorem graph. These declarations reference this one in their body.
-
agreement_at_3
in IndisputableMonolith.Foundation.CoherenceExponentUniqueness
decl_use
-
both_equal_5_at_3
in IndisputableMonolith.Foundation.CoherenceExponentUniqueness
decl_use
-
CoherenceExponentCert
in IndisputableMonolith.Foundation.CoherenceExponentUniqueness
decl_use
-
disagreement_at_1
in IndisputableMonolith.Foundation.CoherenceExponentUniqueness
decl_use
-
disagreement_at_2
in IndisputableMonolith.Foundation.CoherenceExponentUniqueness
decl_use
-
disagreement_at_4
in IndisputableMonolith.Foundation.CoherenceExponentUniqueness
decl_use
-
exponent_unique_at_D3
in IndisputableMonolith.Foundation.CoherenceExponentUniqueness
decl_use
-
k5_forced_at_D3
in IndisputableMonolith.Foundation.CoherenceExponentUniqueness
decl_use
-
k_fib
in IndisputableMonolith.Foundation.CoherenceExponentUniqueness
decl_use
depends on (2)
Lean names referenced from this declaration's body.
-
k_fib
in IndisputableMonolith.Foundation.CoherenceExponentUniqueness
decl_use
-
and
in IndisputableMonolith.NumberTheory.CirclePhaseLift
decl_use