theorem
proved
ml_follows_phi_structure
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Derivations.MassToLight on GitHub at line 267.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
264 ML_derived = phi_power n
265
266/-- Summary: M/L follows the φ-structure. -/
267theorem ml_follows_phi_structure :
268 ∃ n : ℤ, n = 12 := by
269 use 12
270
271end MassToLight
272end Derivations
273end IndisputableMonolith