module module

`IndisputableMonolith.Gravity.SevenGaps.Gap5ConstraintCloseStatus`

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.SevenGaps.Gap5ConstraintCloseStatusAudit module_import

depends on (10)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.CampaignLedger module_import
IndisputableMonolith.Gravity.SevenGaps.DiracAlgebraContinuumBinding module_import
IndisputableMonolith.Gravity.SevenGaps.FullTheoryLedger module_import
IndisputableMonolith.Gravity.SevenGaps.Gap5ConstraintResidualDAG module_import
IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomTarget module_import
IndisputableMonolith.Gravity.SevenGaps.HKTKineticNormalizedRigidity module_import
IndisputableMonolith.Gravity.SevenGaps.HKTOneSiteCounterexample module_import
IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitStrong module_import
IndisputableMonolith.Gravity.SevenGaps.HKTVacuumSectorKill module_import
IndisputableMonolith.Gravity.SevenGaps.HypersurfaceDeformation module_import

declarations in this module (10)