module module moderate

`IndisputableMonolith.Cosmology.CosmogenesisSim`

Rational recognition events and their cost/flow algebra for discrete cosmogenesis simulation. The module mirrors ledger recognition events over ℚ, equipping them with reciprocal symmetry, J-cost, and a multiplicative flow product under event adjunction. Cosmologists or ledger simulators tracking discrete genesis dynamics would cite the event type and the flow-product identities. Content is mostly definitional plus short algebraic lemmas.

claimA recognition event over $\mathbb{Q}$, with reciprocal map, cost $J_{\mathbb{Q}}(x)=(x+x^{-1})/2-1$, per-event flow contribution, and a flow product that multiplies those contributions when events are adjoined to a list.

background

Recognition Science treats recognition events as atomic ledger updates. The classical forcing side uses a real-valued event type; this module supplies the parallel object over $\mathbb{Q}$ so cosmogenesis can be simulated in exact arithmetic.

The cost is the standard RS $J$-functional restricted to nonzero rationals: $J(x)=(x+x^{-1})/2-1$, which is invariant under $x\mapsto x^{-1}$. Flow contribution assigns a multiplicative weight to each event; the flow product of a list is the product of those weights (empty product $=1$). Adjoining an event multiplies the running product by that event's contribution.

The local setting is discrete cosmology: build finite event histories, track total cost and net flow, and keep every identity checkable over $\mathbb{Q}$ without floating-point error.

proof idea

Definition module with elementary algebraic lemmas, not a deep proof development. Reciprocity of $qJ$ is immediate from the formula. Cost and flow-product lemmas after addEvent are one- or two-line rewrites: cost of the extended history is old cost plus new event cost; flow product of the extended list is old product times the new contribution; the empty-list product is $1$; a two-event contribution factors as a product of singles.

why it matters in Recognition Science

Supplies the computable $\mathbb{Q}$-spine for cosmogenesis numerics inside the Cosmology domain. Downstream simulation or ledger-forcing bridges can import the event type, cost, and flow product without re-deriving reciprocal $J$-identities. No parent theorems are wired in the current graph (used-by count zero), so the module is infrastructure: it closes the gap between the abstract RecognitionEvent used in ledger forcing and an exact-arithmetic object suitable for finite-universe genesis runs. Lands next to the eight-tick and $D=3$ forcing landmarks only indirectly, by giving a discrete substrate on which those global constraints can later be checked numerically.

scope and limits

Does not prove a continuum or real-valued limit of the rational events.
Does not derive physical cosmological observables (Hubble, CMB, etc.).
Does not force dimension, tick period, or $\phi$; those live upstream in the forcing chain.
Does not claim the flow product equals a physical action or entropy without further bridge lemmas.
Does not connect used-by edges yet; pure infrastructure until simulators import it.

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