IndisputableMonolith.Foundation.NineParities

declarations in this module (28)

• inductive ParityIndex L59
• abbrev ParityVector L72
• def vacuumParity L75
• theorem parity_count_eq_nine L80
• theorem parity_space_dimension L84
• def isSpacetimeParity L90
• def isColorParity L98
• def isGenerationParity L105
• theorem parity_trichotomy L111
• theorem source_decomposition L118
• def tickReversalConjugate L124
• theorem parities_flip_under_tick_reversal L128
• theorem tick_reversal_involutive L137
• theorem vacuum_parities_vanish L152
• theorem vacuum_is_zero_vector L158
• theorem vacuum_not_fixed_by_tick_reversal L162
• def basisVector L171
• theorem basisVector_nonzero L175
• theorem basisVectors_distinct L182
• theorem parity_independence L191
• theorem color_parity_count_from_D3 L200
• theorem spacetime_parity_count L205
• theorem generation_parity_count L210
• def hammingWeight L215
• theorem vacuum_hamming_weight L219
• theorem tick_reversed_vacuum_hamming_weight L224
• theorem total_parity_configs L230
• theorem nine_parities_master L247