Pith. sign in
module module low

IndisputableMonolith.Physics.CosmologicalPerturbationFromRS

show as:
view Lean formalization →

The module defines objects for cosmological perturbations derived from Recognition Science. It introduces an enumeration of perturbation categories along with a count and a certification structure. All content rests on the imported RS time quantum of one tick. The module supplies the basic types needed for later physics derivations but contains no theorems.

claimDefines an enumeration of perturbation categories, its cardinality, and a certification structure for perturbations in RS-native units with time quantum $\tau_0 = 1$ tick.

background

The module sits in the Physics domain and imports the Constants module. That upstream module supplies the fundamental RS time quantum stated as $\tau_0 = 1$ tick. The module introduces three sibling objects: an inductive type classifying perturbation kinds, a natural number giving the count of those kinds, and a structure that certifies a perturbation instance.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the type-level objects that later cosmological results in Recognition Science would cite. It prepares the ground for applications of the forcing chain T0-T8 and the Recognition Composition Law to perturbation dynamics. No downstream declarations are recorded yet.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)