DarkEnergyFalsifier
plain-language theorem explainer
The DarkEnergyFalsifier structure records the four pieces of information needed to test whether a given observation refutes the Recognition Science derivation of dark energy as residual ledger tension. A cosmologist comparing the model to supernova or CMB data would cite it to check consistency with w = -1 and uniform Λ scaling. The declaration is a plain record definition whose fields directly package observation type, RS prediction, measured value, and falsification flag.
Claim. A falsifier record for the ledger-tension derivation of dark energy is a tuple $(o, p, m, b)$ where $o$ names the observation class, $p$ states the RS-predicted value, $m$ states the measured value, and $b$ is true exactly when the discrepancy falsifies the model.
background
Recognition Science obtains the cosmological constant from the global J-cost balance constraint on an expanding ledger. New spacetime volume created by expansion requires fresh ledger entries; the residual tension per unit volume supplies Λ. The module COS-006 states that this tension equals H₀² times a small numerical factor fixed by the golden-ratio ladder. Upstream structures calibrate the ingredients: LedgerFactorization.of fixes the J function on the positive reals, PhiForcingDerived.of supplies the self-similar fixed point, and SpectralEmergence.of fixes the three-dimensional spatial sector that sets the volume scaling.
proof idea
The declaration is a structure definition that introduces no proof obligations or computational content; it simply packages four strings and a boolean into a named record.
why it matters
The record closes the falsifiability loop for the COS-006 derivation of dark energy from ledger tension. It enumerates the four concrete tests (w ≠ -1, epoch-dependent Λ, fifth forces, clumping) that would refute the claim that Λ is the J-cost of maintaining global balance during expansion. No downstream theorems currently depend on it, leaving open the formalization of statistical comparison between predicted and observed values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.