QFTVacuumNaiveCutoff
plain-language theorem explainer
A positive-real parameter type standing for any hypothetical QFT ultraviolet cutoff. Cosmologists and RS auditors cite it as the straw-man input that naive vacuum-energy estimates depend on. The definition is the subtype of positive reals; no proof content.
Claim. Let a naive QFT vacuum cutoff be any positive real number: the type $\{ x \in \mathbb{R} \mid x > 0 \}$. This is the free UV scale $\Lambda_{\mathrm{UV}}$ on which a QFT-naive vacuum-energy estimate would depend.
background
Track 4.B of the quantum-gravity master plan addresses the vacuum-fluctuation discrepancy structurally. The standard $10^{120}$ cosmological-constant problem assumes QFT vacuum modes contribute to $\Lambda$ on equal footing with classical gravity. In Recognition Science the substrate has no free vacuum modes in that sense; $\Omega_\Lambda$ is derived from the phase-mode budget as $11/16 - \alpha/\pi$, with no vacuum-mode sum.
This declaration is the straw-man parameterization of the usual problem: a hypothetical UV cutoff scale. Downstream, the naive energy density is taken proportional to $\Lambda_{\mathrm{UV}}^4$. The RS value of $\Omega_\Lambda$ (from OmegaLambdaDerivation) carries no such parameter, so independence of cutoff is definitional once the type is in place.
The module status is structural theorem grade: zero sorry, zero RS-internal axiom. The cutoff type exists only to make the contrast with the QFT-naive estimate formally checkable.
proof idea
Pure type definition: the subtype of real numbers strictly greater than zero. No tactics, no lemmas, no computational content beyond the subtype predicate $0 < x$.
why it matters
Anchors Track 4.B's structural address of the vacuum-fluctuation discrepancy. Downstream, QFTNaiveVacuumEnergy maps a cutoff to $\Lambda_{\mathrm{UV}}^4$; omega_lambda_independent_of_QFT_cutoff states that RS $\Omega_\Lambda = 11/16 - \alpha_{\mathrm{CODATA}}/\pi$ for every such cutoff (the argument is unused); and QFT_naive_depends_on_cutoff_but_RS_does_not packages the contrast that the naive energy varies with cutoff while RS does not.
Those facts feed VacuumFluctuationStructuralCert and the one-statement theorem vacuum_fluctuation_one_statement, which record that RS $\Omega_\Lambda$ is closed-form, cutoff-independent, and inside the observed Planck/DESI/SN1a band. The $10^{120}$ gap never arises because the RS derivation never passes through a QFT vacuum-mode sum. Framework landmark: $\Omega_\Lambda$ from integer combinatorics ($[4,2,2]$ Gray-code $\times$ eight-tick addressing) plus one measured $\alpha$, not from a Planck-scale mode integral.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.