pith. machine review for the scientific record. 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 derived from the Q₃ mode budget together with their positivity, summation, and uniformity properties. Cosmologists working in the Recognition Science framework would cite these when establishing vacuum energy uniformity. The module consists of direct definitions and elementary lemmas with no complex proof structure.

claimLet $p$ be the passive fraction of phase-locked modes from the $Q_3$ budget. Then $0 < p < 1$, the active fraction is $1-p$, and $p + (1-p) = 1$. The vacuum energy is uniform under the certificate VacuumUniformityCert when the voxel symmetry and phase-lock energy conditions hold.

background

The module imports the RS time quantum τ₀ = 1 tick from Constants and works in the cosmology domain. It introduces passiveFraction as the fraction of phase-locked modes from the Q₃ mode budget, together with activeFraction, their sum, and the VoxelSymmetric predicate. Additional objects include phaseLockEnergy and the vacuum_energy_uniform predicate that together certify uniformity.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the mode-budget fractions required for vacuum uniformity statements in Recognition Science cosmology. It feeds the vacuum_energy_uniform and VacuumUniformityCert objects that appear among its siblings and supports downstream claims on phase-locked energy distribution.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (11)