pith. sign in
structure

CosmologyDepthCert

definition
show as:
module
IndisputableMonolith.Physics.CosmologyDepthFromRS
domain
Physics
line
27 · github
papers citing
none yet

plain-language theorem explainer

CosmologyDepthCert is a structure that certifies the cardinality of the cosmological epochs type equals five, aligning with the five epochs in the Recognition Science cosmology model. Physicists modeling RS-derived cosmology would cite it to confirm the epoch count matches configDim D = 5. The declaration is a pure structure definition with no proof body or computational content.

Claim. The structure $CosmologyDepthCert$ consists of the field $five_epochs : |CosmologicalEpoch| = 5$, where $CosmologicalEpoch$ is the inductive type with constructors inflation, radiation-dominated, matter-dominated, dark-energy-dominated, and future de Sitter.

background

In the Recognition Science framework, cosmology is modeled via five canonical epochs, each tied to a distinct J-cost regime in the recognition field. The inductive type CosmologicalEpoch enumerates these epochs explicitly as inflation, radiationDominated, matterDominated, darkEnergyDominated, and futureDeSitter, with the module stating that this count equals configDim D = 5. Inflation corresponds to J approaching zero at reheating, radiation to thermal J-cost, and dark energy to J locked at the phi value yielding Lambda_RS approximately 1.91.

proof idea

This is a structure definition with no proof body. The single field is declared directly and is populated downstream by the definition cosmologyDepthCert, which assigns the value from cosmologicalEpochCount.

why it matters

This declaration supplies the five-epoch certificate that feeds the cosmology depth certificate in the RS framework. It implements the module statement that five epochs equal configDim D = 5 and connects to the broader chain by providing the epoch count for J-cost regime analysis. The parent use is in cosmologyDepthCert; it touches the phi-ladder and constants such as G = phi^5 / pi without addressing open questions like the alpha band.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.