IndisputableMonolith.Gravity.CubicReggeProof

declarations in this module (26)

• theorem deriv_J_log_eq_sinh L58
• def euler_lagrange L68
• theorem flat_satisfies_el L76
• theorem sinh_deriv_at_zero L82
• theorem linearized_el_plus_laplacian_zero L94
• theorem linearized_el_eq_neg_laplacian L106
• theorem linearized_el_zero_iff_laplacian_zero L116
• theorem action_per_bond L129
• theorem total_action_convergence L140
• theorem relative_convergence_rate L156
• theorem relative_error_tendsto_zero L163
• theorem laplacian_continuum_limit L174
• theorem laplacian_3D_decomposition L184
• theorem quartic_coeff L204
• theorem sextic_coeff L207
• theorem taylor_coefficients_positive L211
• theorem expansion_convergence_ratio L216
• theorem kappa_derived L230
• theorem kappa_positive L233
• theorem newtonian_positive_source L238
• theorem cubic_flat_deficit L246
• theorem cubic_shape_bound_positive L250
• structure ProvedConvergenceChain L268
• theorem proved_convergence_chain L294
• structure CubicReggeConvergenceCert L323
• theorem cubic_regge_convergence_cert L360