lemma
proved
term proof
eight_tick_cmin_value
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)
160lemma eight_tick_cmin_value : cmin eightTickModel.C = 49 / 162 := by
proof body
Term-mode proof.
161 simp only [cmin, eightTickModel]
162 norm_num
163
164/-- Verify positivity of eight-tick constants. -/
depends on (9)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
tick
in IndisputableMonolith.Constants
decl_use
-
tick
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
eightTickModel
in IndisputableMonolith.CPM.Examples
decl_use
-
cmin
in IndisputableMonolith.CPM.LawOfExistence
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use