module module

`IndisputableMonolith.Gravity.SevenGaps.Gap2LedgerGeneratedHostileProbe`

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.Gap2LedgerGenerated module_import

declarations in this module (12)

theorem probe_jCost_vertex_matches_charge L30
theorem probe_jCost_edge_zero L35
theorem probe_jCost_tet_zero L40
theorem probe_jCost_ledgerGenerated L45
theorem probe_decoy_fails L51
def sjTotalVertexCost L57
theorem probe_sjTotal_not_ledgerGenerated L62
theorem probe_seed_history L89
theorem probe_C27_shape_cap2 L100
theorem probe_C27_hard_stop_bool L103
theorem probe_flag_unmoved L106
theorem probe_verdict L109