module module

`IndisputableMonolith.Gravity.SevenGaps.Gap2PostingCocycleCarrier`

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 (3)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.SevenGaps.Gap2ContinuumMeasureResidualDAG module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2PostingCocycleCarrierAudit module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2PostingHistoryContinuumResidual module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2AntipodalBalanceBridge module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2CertifiedFin8PhaseClose module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2EnrichedCarrierPhase module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2TickPhaseTailBlocker module_import

declarations in this module (22)

structure PostingEnrichedPathClass L58
def forgetPostingPhase L63
def postingPhase L68
theorem forgetPostingPhase_mk L71
theorem postingPhase_mk L75
def FactorsThroughPostingForget L81
theorem carrier_forgets_posting_phase L91
theorem postingPhase_not_factors_through_forget L104
structure PostingEnrichedExactHistory L121
def forgetExactHistory L125
def FactorsThroughExactHistoryForget L129
theorem exact_carrier_forgets_posting_phase L135
theorem exact_postingPhase_not_factors_through_forget L147
def TypedResidual_carrier_forgets_posting_phase L169
theorem typedResidual_carrier_forgets_posting_phase L172
structure PostingCocycleExactPathBridge L182
def bridgeClassTick L190
def TypedResidual_posting_cocycle_bridge L195
def certifiedRecipe_of_bridge L200
structure Gap2PostingCocycleCarrierStatus L210
def gap2PostingCocycleCarrierStatus L220
theorem gap2PostingCocycleCarrierStatus_flags L230