IndisputableMonolith.Foundation.DeltaSpine.CostUniqueness

declarations in this module (32)

• def phiInv L84
• theorem phi_mul_phiInv L87
• theorem phiInv_mul_phi L90
• theorem phiInv_eq_phi_sub_one L94
• def phiUnit L97
• def phiZpow L101
• theorem phiZpow_add L104
• theorem phiZpow_zero L109
• theorem phiZpow_one L114
• theorem phiZpow_neg_one L119
• theorem phiZpow_neg_mul L125
• def sqrtFive L132
• theorem sqrtFive_eq L134
• theorem sqrtFive_sq L137
• def traceZ L141
• theorem traceZ_zero L143
• theorem traceZ_one L148
• theorem traceZ_neg L154
• def SatisfiesDAlembert L167
• theorem traceZ_dAlembert L172
• theorem dAlembert_symm L191
• theorem dAlembert_step L203
• theorem traceZ_step L215
• theorem dAlembert_unique L225
• def SatisfiesDiscreteRCL L259
• def Jdouble L264
• theorem Jdouble_zero L267
• theorem Jdouble_one L273
• theorem Jdouble_symm L278
• theorem Jdouble_rcl L284
• theorem discreteRCL_unique L296
• theorem t5_delta_forced L341