alternativeTheories
plain-language theorem explainer
alternativeTheories enumerates five approaches to the cosmological constant problem and singles out the Recognition Science J-cost mechanism for its calculable cancellation. Cosmologists surveying the 120-order fine-tuning gap between QFT vacuum energy and the observed value would cite the list when contrasting solutions. The definition is a direct enumeration of string literals with no computation or lemma applications.
Claim. The list of alternative approaches to the cosmological constant problem consists of the anthropic principle in a multiverse, quintessence as a dynamic field, modified gravity models such as $f(R)$, holographic dark energy, and the Recognition Science $J$-cost cancellation mechanism on the $phi$-ladder.
background
The Cosmology.CosmologicalConstant module frames the cosmological constant problem as the observed value being roughly $10^{120}$ times smaller than naive QFT predictions, with Recognition Science deriving it from a J-cost ground state of the vacuum ledger. Upstream, the cost of a recognition event equals its J-cost, obtained as the derived cost of a multiplicative recognizer's comparator, while spin statistics supply the real-valued spin for related QFT constraints. This local setting positions the RS $phi$-scaling mechanism against standard alternatives listed in the definition.
proof idea
The definition is a direct enumeration of five string literals. No lemmas or tactics are invoked; the body simply constructs the List String by literal entry.
why it matters
The definition supplies context for the module's target derivation of Lambda from the J-cost ground state, as described in the module documentation aiming at a major paper on the cosmological constant problem. It distinguishes the RS phi-ladder cancellation from the other four proposals and underscores the framework's claim to a calculable mechanism, consistent with the eight-tick octave and phi-scaling landmarks. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.