IndisputableMonolith.Foundation.DAlembert.FullUnconditional

declarations in this module (18)

• theorem P_symmetric_of_F_symmetric L58
• theorem P_symmetric_on_range L82
• theorem P_at_zero_left L96
• theorem P_at_zero_right L111
• theorem P_diagonal L129
• def LogConsistency L150
• theorem log_consistency_of_mult_consistency L154
• theorem H_dAlembert_of_G_RCL L168
• theorem dAlembert_even_solution L199
• def dAlembert_forces_cosh_hypothesis L208
• theorem dAlembert_forces_cosh_is_theorem L218
• def consistency_forces_RCL_form_hypothesis L230
• theorem consistency_forces_RCL_form_is_theorem L242
• structure FullUnconditionalHypotheses L269
• theorem full_unconditional_inevitability L288
• theorem full_inevitability_explicit L352
• theorem washburn_full_unconditional L434
• theorem consistency_forces_RCL_polynomial L466