module module

`IndisputableMonolith.Gravity.SevenGaps.Gap2JDiamondRankHostileProbe`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2JDiamondRank module_import

declarations in this module (29)

theorem probe_edge_counts L32
theorem probe_loopPoint_counts L36
theorem probe_same_count_vector L40
theorem probe_edge_SJ L46
theorem probe_loopPoint_SJ L48
theorem probe_path_SJ L51
theorem probe_twoEdge_SJ L53
theorem probe_outStar_SJ L56
theorem probe_fork_SJ L59
theorem probe_seed_defect_SJ L64
theorem probe_seed_localized L68
theorem probe_seed_inner_product L75
theorem probe_outStar_defect_SJ L81
theorem probe_disjoint_defect_SJ L85
theorem probe_seed_J_at_one L89
theorem probe_outStar_J_at_one L96
theorem probe_disjoint_J_at_one L103
theorem probe_count_conflict_J_at_one L110
theorem probe_seed_clash_from_path_rows_alone L121
theorem probe_count_clash_alone L127
theorem probe_inconsistent_seed L132
theorem probe_inconsistent_counts L140
theorem probe_not_function_of_counts L145
theorem probe_lhs_length L154
theorem probe_lhs_rank_two L156
theorem probe_aug_independent L162
theorem probe_empty_iface_is_corollary L169
theorem probe_balanced_iface_is_corollary L176
theorem probe_verdict L184