cube_faces

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

• alpha_ingredients_from_D3_cube in IndisputableMonolith.Constants.AlphaDerivation decl_use
• cube_faces in IndisputableMonolith.Constants.AlphaDerivation decl_use
• faces_at_D3 in IndisputableMonolith.Constants.AlphaDerivation decl_use
• face_solid_angle_sum in IndisputableMonolith.Constants.AlphaDerivation decl_use
• per_face_solid_angle in IndisputableMonolith.Constants.AlphaDerivation decl_use
• per_face_solid_angle_eq in IndisputableMonolith.Constants.AlphaDerivation decl_use
• seam_denominator in IndisputableMonolith.Constants.AlphaDerivation decl_use
• alphaFramework in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
• AlphaFrameworkCert in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
• Q3_faces in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
• generation_ordering_general in IndisputableMonolith.Masses.BaselineDerivation decl_use
• total_geometric_content in IndisputableMonolith.Masses.BaselineDerivation decl_use
• W_endo in IndisputableMonolith.Masses.BaselineDerivation decl_use
• lepton_integer_slot_iff_bundle_no_hk in IndisputableMonolith.Masses.JCostPerturbation decl_use
• o4_channel_closure_certificate in IndisputableMonolith.Masses.JCostPerturbation decl_use
• o4_slot_forcing_certificate in IndisputableMonolith.Masses.JCostPerturbation decl_use
• step_mu_tau_channel_split in IndisputableMonolith.Masses.JCostPerturbation decl_use
• step_mu_tau_coeff_forced_from_six_face_term in IndisputableMonolith.Masses.JCostPerturbation decl_use
• step_mu_tau_coeff_iff_full_forced_under_dim_bound in IndisputableMonolith.Masses.JCostPerturbation decl_use
• step_mu_tau_coeff_iff_kn_under_dim_bound in IndisputableMonolith.Masses.JCostPerturbation decl_use
• step_mu_tau_coeff_iff_kn_under_dim_bound_no_hk in IndisputableMonolith.Masses.JCostPerturbation decl_use
• step_mu_tau_denominator_forced in IndisputableMonolith.Masses.JCostPerturbation decl_use
• step_mu_tau_denominator_iff_numerator_under_dim_bound in IndisputableMonolith.Masses.JCostPerturbation decl_use
• step_mu_tau_denominator_iff_numerator_under_dim_bound_no_hk in IndisputableMonolith.Masses.JCostPerturbation decl_use
• step_mu_tau_face_count_forced in IndisputableMonolith.Masses.JCostPerturbation decl_use
• step_mu_tau_face_term_forced in IndisputableMonolith.Masses.JCostPerturbation decl_use
• step_mu_tau_full_affine_forced_from_face_term in IndisputableMonolith.Masses.JCostPerturbation decl_use
• step_mu_tau_full_family_coeff_iff_under_dim_bound in IndisputableMonolith.Masses.JCostPerturbation decl_use
• step_mu_tau_full_family_coeff_iff_under_dim_bound_no_hk in IndisputableMonolith.Masses.JCostPerturbation decl_use
• step_mu_tau_full_family_forced_from_coeff_match in IndisputableMonolith.Masses.JCostPerturbation decl_use

… and 10 more