module module

`IndisputableMonolith.Gravity.SevenGaps.Gap2LetterCostDichotomyHostileProbe`

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

declarations in this module (14)

theorem headline_binders_are_as_claimed L41
theorem surfaceTotal_is_forall_N L48
theorem history_zero_is_global L54
theorem census_samples L62
theorem purity_witness_samples L73
theorem combined_relaxation_witness L82
theorem surfaceCost_total_is_tN3 L88
theorem indexTilt_concrete_charges L94
theorem indexTilt_block_sums_zero L99
theorem bulk_witness_dust L104
theorem bulk_witness_not_surface L108
theorem fixedKindTotals_inhabited L113
theorem fibre_member_centered L117
theorem flags_unmoved L126