pith. machine review for the scientific record. sign in
def

alphaFramework

definition
show as:
view math explainer →
module
IndisputableMonolith.Constants.AlphaHigherOrder
domain
Constants
line
213 · github
papers citing
none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Constants.AlphaHigherOrder on GitHub at line 213.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 210  n2_reduced : reduced_configs 2 = 217
 211  z2_sectors : Z2_sectors = 32
 212
 213def alphaFramework : AlphaFrameworkCert where
 214  cube_faces := Q3_faces_eq
 215  cube_edges := Q3_edges_eq
 216  passive := passive_edges_eq
 217  wallpaper := rfl
 218  fw_pairs := face_wallpaper_pairs_eq
 219  curv_num := curvature_numerator_eq
 220  meas_dim := measure_dimension_eq
 221  delta_1_is_ratio := delta_1_structure
 222  n2_configs := n_fold_configs_2
 223  n2_reduced := reduced_configs_2
 224  z2_sectors := Z2_sectors_eq
 225
 226end
 227
 228end AlphaHigherOrder
 229end Constants
 230end IndisputableMonolith