theorem proved term proof

`alpha_ingredients_from_D3_cube`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 263theorem alpha_ingredients_from_D3_cube :
 264    geometric_seed_factor = cube_edges D - active_edges_per_tick ∧
 265    seam_numerator D = cube_faces D * wallpaper_groups + euler_closure ∧
 266    seam_denominator D = cube_faces D * wallpaper_groups := by

proof body

Term-mode proof.

 267  constructor
 268  · rfl
 269  constructor
 270  · rfl
 271  · rfl
 272
 273end AlphaDerivation
 274end Constants
 275end IndisputableMonolith

depends on (12)

Lean names referenced from this declaration's body.

active_edges_per_tick in IndisputableMonolith.Constants.AlphaDerivation decl_use
cube_edges in IndisputableMonolith.Constants.AlphaDerivation decl_use
cube_faces in IndisputableMonolith.Constants.AlphaDerivation decl_use
euler_closure in IndisputableMonolith.Constants.AlphaDerivation decl_use
geometric_seed_factor in IndisputableMonolith.Constants.AlphaDerivation decl_use
seam_denominator in IndisputableMonolith.Constants.AlphaDerivation decl_use
seam_numerator in IndisputableMonolith.Constants.AlphaDerivation decl_use
wallpaper_groups in IndisputableMonolith.Constants.AlphaDerivation decl_use
wallpaper_groups in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
cube_faces in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
cube_faces in IndisputableMonolith.Physics.PMNSCorrections decl_use