IndisputableMonolith.Foundation.RecognitionOperator

declarations in this module (48)

• abbrev Signal8 L13
• abbrev BondId L30
• abbrev AgentId L31
• abbrev LedgerState L32
• def time L36
• def Z_patterns L37
• def global_phase L38
• def channels L39
• def active_bonds L40
• def bond_multipliers L41
• def bond_pos L42
• def bond_agents L45
• def total_Z L49
• def RecognitionCost L50
• def net_skew L51
• def signed_log_flow L52
• def reciprocity_skew L53
• def reciprocity_skew_abs L54
• def admissible L55
• def neutralRegister L58
• def quarterTurnCore L73
• structure StructuredSector L78
• def quarterTurnModes L84
• lemma mem_quarterTurnModes L87
• def quarterTurnSector L92
• structure RecognitionOperator L101
• def shiftLinear L105
• lemma shiftLinear_apply L116
• lemma dft_coefficients_add L120
• lemma dft_coefficients_smul L126
• lemma dft_coefficients_mode L132
• lemma dft8_mode_mem_neutralRegister L138
• theorem quarterTurnCore_le_neutralRegister L150
• def sectorProject L164
• lemma sectorProject_apply L199
• lemma sectorProject_mode L203
• def recognitionUpdate L224
• lemma recognitionUpdate_apply L227
• def cyclicShiftIter L253
• lemma cyclicShiftIter_add L258
• lemma cyclicShiftIter_smul L269
• lemma cyclicShiftIter_mode L280
• lemma odd_mode_fourth_eigenvalue L301
• theorem shift_mem_quarterTurnCore L307
• theorem shift_four_eq_neg_on_quarterTurnCore L329
• theorem twoBeat_square_eq_neg_on_quarterTurnCore L355
• theorem sectorProject_eq_id_on_quarterTurnCore L360
• theorem recognitionUpdate_eq_shift_on_quarterTurnCore L382