module module

`IndisputableMonolith.Gravity.SevenGaps.FullTheoryLedger`

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.Gravity.Analysis.SRSConvergesEH4DAudit module_import

depends on (9)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.CampaignLedger module_import
IndisputableMonolith.Gravity.SevenGaps.CapShellBridge module_import
IndisputableMonolith.Gravity.SevenGaps.CurvedOperatorUnderdetermination module_import
IndisputableMonolith.Gravity.SevenGaps.DynamicStructureFunctionBlocker module_import
IndisputableMonolith.Gravity.SevenGaps.MeasureSubstrateBlocker module_import
IndisputableMonolith.Gravity.SevenGaps.MetricRefinementCarrierBlocker module_import
IndisputableMonolith.Gravity.SevenGaps.RecognitionRatioSubstrateBlocker module_import
IndisputableMonolith.Gravity.SevenGaps.ZqContinuumBlocker module_import
IndisputableMonolith.Gravity.SevenGaps.ZqShellBalanceBlocker module_import

declarations in this module (19)

theorem whose L47
structure FullTheoryBenchmarks L48
def fullTheoryBenchmarks L78
def Pillar1Closed L88
def Pillar2Closed L93
def Pillar3Closed L97
def FullTheoryClosed L102
theorem full_theory_not_yet_closed L109
theorem all_pillars_open L116
theorem starting_line_anchored L130
theorem must L148
theorem gap2_measure_selection_blocker_certified L150
theorem gap2_cutoff_limit_blocker_certified L174
theorem gap2_capshell_bridge_discharged L228
theorem gap2_shell_balance_blocker_certified L241
theorem gap2_metric_carrier_blocker_certified L261
theorem gap1_bridge_blocker_certified L280
theorem gap4_curvature_coupling_blocker_certified L292
theorem gap5_structure_function_blocker_certified L325