Cosmology Vacuum Uniformity Passive Fraction Pos

The passive fraction

In the Recognition Science framework, the vacuum is not empty space but a structured ledger: a discrete record of recognition events, where each event carries a cost. The framework's library of machine-checked formal theorems contains a definition called the passive fraction, a real number set to 11/16. The theorem passive_fraction_pos proves that this fraction is greater than zero. It is a statement about arithmetic, not about physics: 11/16 is a positive number because it is a ratio of two positive integers.

The number itself arises from a combinatorial budget of modes on a three-dimensional grid of voxels, the framework's term for small volume elements. The fraction 11/16 is the share of phase-locked modes, those that are committed ledger entries with zero maintenance cost. The companion theorem passive_fraction_lt_one proves the fraction is less than one, and fractions_sum shows that the passive and active fractions add to one. These are exact arithmetic facts, each verified by direct computation in the framework's library.

What the declaration does not claim is where its real significance lies. It does not claim that the vacuum energy density is uniform. That stronger statement is a separate theorem, vacuum_energy_uniform, which relies on an additional axiom: voxel symmetry, the assertion that no location on the grid is distinguished. The positivity lemma alone says nothing about space, energy, or cosmology. It is a necessary ingredient, not a sufficient one.

Nor does the lemma claim that the physical vacuum has this structure. The identification of the framework's phase-locked modes with the stress-energy tensor of conventional physics is a hypothesis, not a theorem. The library is explicit about this: the structural uniformity is proved, but the physical identification remains a prediction. The lemma is a small, exact step in a larger argument, and its power lies in how precisely it is scoped.

theorem passive_fraction_pos : passiveFraction > 0 := by
  unfold passiveFraction; norm_num

/-- Fraction of phase-locked modes from Q₃ mode budget. -/
noncomputable def passiveFraction : ℝ := 11 / 16

theorem passive_fraction_lt_one : passiveFraction < 1 := by
  unfold passiveFraction; norm_num

theorem fractions_sum : passiveFraction + activeFraction = 1 := by
  unfold activeFraction; ring

What this page does not claim

The lemma does not claim the vacuum energy density is uniform. The lemma does not claim the framework's phase-locked modes correspond to any physical entity. The lemma does not claim that 11/16 has any cosmological meaning outside the framework's mode budget.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/VacuumUniformity.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: