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)
37def k_fib (D : ℕ) : ℕ := 2^D - D
proof body
Definition body.
38
39/-- Integration measure: k_int(D) = D + 2. -/
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_int
in IndisputableMonolith.Foundation.CoherenceExponentUniqueness
decl_use
depends on (1)
Lean names referenced from this declaration's body.
-
k_int
in IndisputableMonolith.Foundation.CoherenceExponentUniqueness
decl_use