pith. machine review for the scientific record. sign in
def definition def or abbrev high

passiveFraction

show as:
view Lean formalization →

The declaration supplies the constant fraction 11/16 of phase-locked modes drawn from the Q₃ budget. Cosmologists working in the Recognition Science setting cite the value when constructing the isotropic vacuum energy density per voxel. The definition consists of a direct numerical assignment with no lemmas or computation required.

claimThe passive fraction of phase-locked modes from the Q₃ mode budget is defined as $11/16$.

background

The Vacuum Uniformity module shows that phase-locked modes on the ℤ³ carrier contribute a constant J-cost background. These modes are committed ledger entries whose maintenance cost vanishes under the J-function. The module invokes VoxelSymmetry to guarantee that the combinatorial fraction of such modes is the same at every lattice point, yielding a spatially uniform vacuum energy density.

proof idea

The declaration is a direct definition that assigns the rational constant 11/16. No lemmas are invoked and no tactics are applied.

why it matters in Recognition Science

This definition supplies the numerical input to phaseLockEnergy and to the uniformity theorem vacuum_energy_uniform, which asserts VoxelSymmetric (fun _ => phaseLockEnergy). It realizes the combinatorial step in the module argument that the fraction is independent of position. The same 11/16 appears in the bridge from PhaseSaturationVacuum to the stress-energy tensor T_μν^vac.

scope and limits

formal statement (Lean)

  26noncomputable def passiveFraction : ℝ := 11 / 16

proof body

Definition body.

  27

used by (7)

From the project-wide theorem graph. These declarations reference this one in their body.