module module

`IndisputableMonolith.Verification.ZMapTopologicalDerivation`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Masses.ZMapForcing module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.AlphaDerivation module_import

declarations in this module (53)

def sm_charges L55
def integerizes_all L58
theorem six_integerizes L62
theorem one_fails L71
theorem two_fails L81
theorem three_integerizes L94
theorem four_fails L103
theorem five_fails L113
theorem face_count_eq_six L123
theorem integerization_results L126
theorem six_smallest_positive_even_integerizer L134
def Q_tilde_lepton L154
def Q_tilde_up L155
def Q_tilde_down L156
def Z_poly L160
def Z_quark_with_offset L163
theorem charge_conjugation_invariant L166
theorem neutral_vanishes L172
def Z_lepton L176
def Z_up L177
def Z_down L178
def Z_up_with_offset L181
def Z_down_with_offset L184
theorem bare_Z_values L187
theorem coefficients_forced_from_quark_bare_anchors L193
theorem full_anchor_tuple_forces_coefficients_and_offset L212
def families_separated L235
theorem canonical_separates L239
theorem quadratic_only_weak_hierarchy L249
theorem three_weak_hierarchy L256
theorem six_better_separation_than_three L261
def edge_direction_count L270
theorem edge_direction_eq_four L273
def Z_full L276
theorem full_Z_values L283
theorem matches_anchor_Z L292
structure ZMapDerivation L300
def derivation_complete L321
def ordered_hierarchy L335
theorem canonical_ordered L339
theorem quadratic_ordered L345
theorem quartic_only_separated L352
theorem minimal_nonzero_coefficients L359
theorem unique_minimal_complete L371
theorem one_one_achieves_minimum L377
theorem complete_ordered_min_budget_forces_unit_coeffs L382
def complete_ordered_minimizer L399
theorem one_one_is_complete_ordered_minimizer L404
theorem complete_ordered_minimizer_forces_unit_coeffs L412
theorem zmap_canonical_tuple_forced_from_first_principles L429
theorem zmap_canonical_tuple_satisfies_first_principles L451
def first_principles_zmap_tuple L462
theorem canonical_tuple_iff_first_principles L471