module
module
IndisputableMonolith.Gravity.SevenGaps.Gap2ContinuumMeasureResidualDAG
show as:
view Lean formalization →
depends on (12)
-
IndisputableMonolith.Gravity.SevenGaps.CapShellBridge -
IndisputableMonolith.Gravity.SevenGaps.ExactShellGaugePreflight -
IndisputableMonolith.Gravity.SevenGaps.ExactShellGaugeUV -
IndisputableMonolith.Gravity.SevenGaps.FullTheoryLedger -
IndisputableMonolith.Gravity.SevenGaps.Gap2CertifiedFin8PhaseClose -
IndisputableMonolith.Gravity.SevenGaps.Gap2MeasureStatusBinding -
IndisputableMonolith.Gravity.SevenGaps.Gap2PostingCocycleCarrier -
IndisputableMonolith.Gravity.SevenGaps.Gap2TailAutFiberParityBlocker -
IndisputableMonolith.Gravity.SevenGaps.GaugeHistoryMeasure -
IndisputableMonolith.Gravity.SevenGaps.MeasureSubstrateBlocker -
IndisputableMonolith.Gravity.SevenGaps.PathSumMeasure -
IndisputableMonolith.Gravity.SevenGaps.ZqContinuumBlocker
declarations in this module (16)
-
def
TypedResidual_measure_gaugeCounting_blocker -
def
TypedResidual_measure_history_presentation -
def
TypedResidual_continuum_cauchy_iff_oscillatoryTail -
def
TypedResidual_continuum_capShellCompatibility -
def
TypedResidual_continuum_substrate_oscillatoryTail -
theorem
typedResidual_measure_gaugeCounting_blocker -
theorem
typedResidual_measure_history_presentation -
theorem
typedResidual_continuum_cauchy_iff_oscillatoryTail -
theorem
typedResidual_continuum_capShellCompatibility -
theorem
decoy_zeroPhase_not_oscillatoryTail -
structure
Gap2ResidualDAGStatus -
def
gap2ResidualDAGStatus -
theorem
that -
theorem
gap2ResidualDAGStatus_flags -
theorem
typedResidual_measure_status_retracted -
theorem
gap2_rollup_closed_after_residual_dag