module module

`IndisputableMonolith.Foundation.TimeAsOrbit`

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.Foundation.RealityFromDistinction module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.ArithmeticFromLogic module_import
IndisputableMonolith.Foundation.TimeEmergence module_import
IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject module_import

declarations in this module (21)

def tickSucc L47
theorem tickSucc_index L49
def tickZero L52
theorem tickZero_index L54
def tickEquivNat L59
theorem tickEquivNat_apply L65
theorem tickEquivNat_symm_apply L66
theorem tickEquivNat_zero L69
theorem tickEquivNat_succ L71
def tickEquivLogicNat L75
def tickRecursor L81
theorem tickRecursor_zero L84
theorem tickRecursor_succ L87
def tick_isNNO L93
def tick_orbit_eq_logicNat L119
theorem tick_orbit_eq_logicNat_zero L123
theorem tick_orbit_eq_logicNat_succ L129
theorem recognitionStep_iterates_succ L140
structure TimeAsOrbitCert L157
def timeAsOrbitCert L167
theorem timeAsOrbitCert_inhabited L174