QEvent
plain-language theorem explainer
A recognition event with natural-number endpoints and a rational ratio, the computable mirror of the real-valued ledger event. Cosmogenesis and flow-product arguments cite it as the atomic posting unit over ℚ. It is a plain structure definition (source, target, ratio), with no proof obligations.
Claim. A recognition event over the rationals is a triple $(s,t,r)$ with $s,t\in\mathbb{N}$ (source and target agents) and $r\in\mathbb{Q}$ (the posted ratio). It is the rational mirror of the real-valued recognition event used in the ledger-forcing development.
background
The CosmogenesisSim module rebuilds the PreBigBang/FirstTick dynamics over $\mathbb{Q}$ so the full eight-tick cosmogenesis is a Lean object one can #eval, with conservation proved in the kernel. The recognition ledger is mirrored exactly from Foundation.LedgerForcing: events, reciprocal posting, and J-cost increments all reappear with rational fields.
Upstream, LedgerForcing.RecognitionEvent carries source, target, and a positive real ratio; its reciprocal swaps endpoints and inverts the ratio. CostAlgebra supplies the reciprocal automorphism on the J-cost side. Here the same shape is specialized to $\mathbb{Q}$, dropping positivity proofs in favor of explicit nonzero hypotheses at use sites.
The conserved quantity $\sigma$ is rewritten multiplicatively as a flow product (product of ratios touching an agent). Rational arithmetic makes that product exact and computable; double-entry multiplies by $r\cdot r^{-1}=1$.
proof idea
No proof: this is a structure declaration with three fields (source, target, ratio : ℚ) and a Repr instance. Downstream definitions (qreciprocal, addEvent, flowContribution) pattern-match on these fields; theorems such as flowContribution_pair discharge the algebraic identities that the real ledger proved with positivity side-conditions.
why it matters
Every computable cosmogenesis object is built from this type. addEvent posts an event with its reciprocal (double-entry); cosmoEvent builds the tick-$t$ edge of the 3-cube cadence carrying the $t$-th recurrence ratio; cosmogenesis folds eight such postings from the empty ledger. Flow machinery (flowContribution, flowProduct, and the pair/addEvent lemmas) reads the ratio field to prove $\sigma\equiv 1$ at every agent after the full run (cosmogenesis_conserves), for any positive seed, with no decide and no sorry.
Framework landmarks: the eight-tick octave (T7) appears as List.range 8 over the 3-cube edges (T8, $D=3$); the self-similar recurrence $r\mapsto 1+1/r$ yields Fibonacci convergents to $\varphi$ (T6) as an exact rational sequence. This definition is the atomic carrier that makes those statements kernel-checkable over $\mathbb{Q}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.