IndisputableMonolith.Foundation.ComplexStructureForcing

declarations in this module (35)

• abbrev Signal8 L45
• def nextIdx L48
• def shift L54
• def shiftIter L58
• lemma nextIdx_8 L63
• theorem shift_period_8 L71
• def dftBasis L90
• def eigenvalue L94
• theorem eigenvalue_eq_phaseExp L97
• theorem eigenvalue_2_is_I L118
• theorem eigenvalue_6_is_neg_I L134
• theorem no_real_root_x2_plus_1 L143
• theorem x2_plus_1_no_real_root L147
• theorem x2_plus_1_divides_x8_minus_1 L151
• theorem complexification_forced L166
• def inner8 L174
• theorem inner8_conj_symm L178
• def dft8 L186
• def idft8 L191
• theorem star_ L197
• theorem dft8_eq_mulVec L216
• theorem dft8_preserves_inner L239
• theorem dft8_preserves_norm L249
• def JcostC L257
• theorem jcost_phase_invariant L265
• theorem jcost_modulus_only L278
• def netSkew L288
• def totalModeCost L292
• theorem mode_cost_phase_invariant L303
• structure EvolutionOp L311
• structure UnitaryEvolution L318
• structure ComplexStructureCertificate L344
• theorem complex_structure_certificate L354
• theorem cost_phase_duality L369
• theorem hamiltonian_emergence L379