module module

`IndisputableMonolith.Cosmology.CosmogenesisSim`

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

declarations in this module (29)

structure QEvent L38
def qreciprocal L45
def qJ L48
def qcost L51
def flowContribution L55
def flowProduct L61
def addEvent L66
theorem qJ_recip L72
theorem qcost_addEvent L76
theorem flowProduct_nil L85
theorem flowContribution_pair L90
theorem flowProduct_addEvent L101
theorem flowProduct_foldl L109
def recurSeq L123
theorem recurSeq_pos L128
def cyc L137
theorem cyc_length L140
theorem cosmogenesis_tick_count L143
theorem qJ_pos L147
theorem seed2_distinction L160
def cosmoEvent L164
def cosmogenesis L169
theorem cosmogenesis_conserves L174
theorem addEvent_length L180
theorem foldl_addEvent_length L185
theorem cosmogenesis_length L196
theorem seed2_first_tick_cost_pos L201
structure TraceCertificates L205
theorem trace_certificates_seed2 L213