Cosmology Cosmogenesis Sim Cosmogenesis Length

The sixteen-event ledger

The declaration cosmogenesis_length is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It proves that a particular simulated cosmogenesis, built from eight ticks of a self-similar recurrence, produces a ledger of exactly sixteen events. The ledger is a discrete record of events, each with a source, a target, and a ratio. The proof is computational: it runs over rational numbers, so the simulation is a concrete object that can be evaluated, not just described.

The sixteen events arise from double-entry bookkeeping. Each of the eight ticks posts an event and its reciprocal, which swaps source and target and inverts the ratio. The theorem cosmogenesis_length states that the length of the resulting list is 16, following from the general fact that n ticks produce 2n events. This is not a physical claim about the universe; it is a statement about a formal construction inside the framework's library.

In Recognition Science, this construction mirrors a larger forcing chain that derives the golden ratio and an eight-tick cycle from a cost function. The simulation makes that chain computable: the recurrence r ↦ 1 + 1/r produces the Fibonacci convergents 2, 3/2, 5/3, 8/5, 13/8, which approach φ. The conserved quantity, the flow product at an agent, stays exactly 1 after all sixteen events, for any positive seed. These are internal framework results, proved in the library, not measurements of the physical world.

What the declaration does not claim is just as important. It does not say the universe began with sixteen events, nor that physical cosmogenesis has this length. It does not assert that the golden ratio emerges in nature. It establishes only that a specific formal simulation, defined within the framework, has a list length of 16. The step from this formal result to any physical claim about the cosmos is not made by this theorem.

/-- The cosmogenesis posts sixteen events (eight ticks, each paired). -/
theorem cosmogenesis_length (seed : ℚ) : (cosmogenesis seed).length = 16 := by
  have h : (cosmogenesis seed).length = 2 * 8 := foldl_addEvent_length (cosmoEvent seed) 8
  omega

/-- Post one distinction. Double-entry forces the reciprocal in with it.
Mirror of `LedgerForcing.add_event`. -/
def addEvent (es : List QEvent) (e : QEvent) : List QEvent :=
  e :: qreciprocal e :: es

/-- **σ conservation, proved.** After the full cosmogenesis, the flow product is
exactly `1` at every agent, for any positive seed. No `decide`, no `sorry`. -/
theorem cosmogenesis_conserves (seed : ℚ) (hs : 0 < seed) (agent : ℕ) :
    flowProduct (cosmogenesis seed) agent = 1 :=
  flowProduct_foldl agent (cosmoEvent seed)
    (fun t => (recurSeq_pos seed hs t).ne') 8

/-- The self-similar recognition recurrence `r ↦ 1 + 1/r` over `ℚ`.
Exact Fibonacci convergents to `φ`. -/
def recurSeq (seed : ℚ) : ℕ → ℚ
  | 0 => seed
  | (n + 1) => 1 + (recurSeq seed n)⁻¹

What this page does not claim

The universe began with sixteen events. The golden ratio emerges in physical nature. The simulation describes any actual physical process.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/CosmogenesisSim.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: