def
definition
alphaFramework
show as:
view math explainer →
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
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