pith. sign in
module module moderate

IndisputableMonolith.Physics.CosmologyDepthFromRS

show as:
view Lean formalization →

CosmologyDepthFromRS defines types for cosmological epochs and depth certificates built from RS constants. Researchers deriving universe structure from the Recognition Science forcing chain would reference these objects. The module consists entirely of definition declarations with no embedded proofs or theorems.

claimThe module introduces the type $CosmologicalEpoch$ for RS-derived cosmological epochs, the function $cosmologicalEpochCount$, the type $CosmologyDepthCert$, and the certificate constructor $cosmologyDepthCert$.

background

The module imports Mathlib and IndisputableMonolith.Constants. The upstream Constants module supplies the fundamental RS time quantum with the declaration that τ₀ = 1 tick. Recognition Science places all constants in native units where c = 1 and proceeds from the forcing chain T0–T8 that yields D = 3 and the phi-ladder.

proof idea

This is a definition module, no proofs. It declares the epoch type, a counting function, the depth certificate type, and its constructor as sibling definitions.

why it matters in Recognition Science

The module supplies the epoch and certificate objects that later cosmology derivations in the Recognition framework would apply. It directly extends the time quantum from Constants toward structures involving the eight-tick octave and phi-based mass formulas.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)