Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.VacuumUniformity

show as:
view Lean formalization →

This module defines the passive and active fractions of phase-locked modes drawn from the Q₃ mode budget together with a uniformity certificate for vacuum energy. Cosmologists working in the Recognition Science framework cite these objects when partitioning mode budgets and verifying spatial uniformity. The module is a collection of definitions and elementary lemmas with no non-trivial proofs.

claimLet $p$ be the passive fraction of phase-locked modes from the Q₃ budget and $a$ the complementary active fraction, satisfying $p+a=1$. The predicate VacuumUniformityCert asserts that the resulting vacuum energy density is spatially uniform.

background

The module imports the RS time quantum τ₀ = 1 tick from IndisputableMonolith.Constants. It introduces passiveFraction and activeFraction as the two components that partition the Q₃ mode budget into phase-locked and non-locked contributions. Related sibling definitions include fractions_sum (the identity p + a = 1), vacuum_energy_uniform, and the certificate VacuumUniformityCert that packages these quantities for downstream cosmology arguments.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions supply the mode-budget partition required by any Recognition Science treatment of vacuum energy uniformity. They sit upstream of larger cosmological constructions that invoke the eight-tick octave and D = 3 spatial dimensions, even though no direct used_by edges are recorded in the current graph.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (11)