vacuumJCost
plain-language theorem explainer
vacuumJCost defines the J-cost of the vacuum as the J-cost function evaluated at the golden ratio phi. Cosmologists working in Recognition Science cite this baseline when constructing the effective cosmological constant from ledger ground-state energy before cancellation. The definition is a direct one-line instantiation of the imported Jcost at the self-similar fixed point.
Claim. Let $J$ be the J-cost function. The vacuum J-cost is defined by $J_0 := J(phi)$, where $phi$ is the golden ratio and $J(x) = (x + x^{-1})/2 - 1$.
background
Recognition Science equips every state with a J-cost via the cost function induced by a multiplicative recognizer. This satisfies the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. The constant phi is the unique positive self-similar fixed point forced at step T6 of the UnifiedForcingChain. The module CosmologicalConstant treats the vacuum as carrying nonzero J-cost due to phi-mismatch, so that Lambda emerges from the difference between positive field-mode contributions and negative phi-structure cancellation. Upstream results supply the ledger factorization structure from DAlembert.LedgerFactorization.of and the cost definition from MultiplicativeRecognizerL4.cost as derivedCost of the comparator.
proof idea
One-line definition that applies the Jcost function (imported from Cost via ObserverForcing.cost and MultiplicativeRecognizerL4.cost) directly to the constant phi supplied by PhiForcingDerived.of.
why it matters
This definition supplies the starting J-cost value for the vacuum in the module that targets resolution of the cosmological constant problem. It precedes the J-cost cancellation mechanism and the phiLadderSum sibling, connecting to T5 J-uniqueness and T6 phi fixed point in the forcing chain. The module doc-comment notes that the raw value is approximately 0.118 and therefore requires further suppression to reach the observed 10^{-122} residual; the declaration therefore marks the entry point for that cancellation argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.