IndisputableMonolith.Foundation.WindingCharges

declarations in this module (35)

• inductive LatticeStep L84
• def LatticePath L91
• def step_displacement L95
• def winding_number L107
• theorem winding_empty L111
• theorem winding_plus_self L115
• theorem winding_minus_self L120
• theorem winding_orthogonal L125
• theorem winding_stay L130
• theorem winding_additive L141
• theorem winding_cons L147
• def is_cancelling_pair L159
• theorem cancelling_pair_zero_displacement L164
• theorem insert_cancelling_preserves_winding L178
• theorem remove_cancelling_preserves_winding L191
• theorem winding_numbers_independent L205
• theorem winding_surjective_single L212
• def winding_charge L239
• theorem D_independent_charges L252
• theorem three_independent_winding_charges L271
• structure WindingLabel L298
• def winding_label_is_topological L303
• theorem winding_gives_three_charges L314
• theorem charge_count_is_dimension L326
• theorem all_threes_unified L330
• def is_closed L347
• theorem empty_is_closed L351
• theorem cancelling_pair_closed L355
• def square_loop L374
• theorem square_loop_closed L377
• theorem square_loop_trivial_when_equal L386
• def independent_loop_count L402
• theorem three_independent_loops_D3 L404
• theorem loops_eq_face_pairs_D3 L411
• theorem winding_charges_certificate L430