IndisputableMonolith.Constants.AlphaHigherOrder

declarations in this module (44)

• def Q3_vertices L59
• theorem Q3_vertices_eq L60
• def Q3_edges L63
• theorem Q3_edges_eq L64
• def Q3_faces L67
• theorem Q3_faces_eq L68
• def active_edges L71
• def passive_edges L74
• theorem passive_edges_eq L75
• def wallpaper_groups L78
• def face_wallpaper_pairs L81
• theorem face_wallpaper_pairs_eq L82
• def curvature_numerator L85
• theorem curvature_numerator_eq L86
• def measure_dimension L89
• theorem measure_dimension_eq L90
• def alpha_seed L95
• def f_gap L98
• def delta_1 L102
• theorem delta_1_structure L104
• theorem delta_1_numerator L108
• theorem delta_1_denominator_nat L109
• theorem delta_1_power L110
• theorem delta_1_neg L113
• def n_fold_configs L126
• theorem n_fold_configs_1 L128
• theorem n_fold_configs_2 L129
• def Q3_aut_order L132
• def reduced_configs L135
• theorem reduced_configs_2 L137
• def half_period_dim L142
• theorem half_period_dim_eq L143
• def Z2_sectors L146
• theorem Z2_sectors_eq L147
• def VoxelSeamCorrection L153
• def delta_n L157
• def partial_alpha L161
• def CODATA_alpha_inv L167
• structure AlphaPrecisionHypothesis L170
• def additive_residual L181
• def exponential_residual L185
• theorem exp_minus_add_pos L189
• structure AlphaFrameworkCert L200
• def alphaFramework L213