CausalClosureForced
plain-language theorem explainer
The CausalClosureForced structure packages the requirement that dimensional forcing fixes the scaling exponents in the effective frequency to beta = 1 and gamma = 1. It functions as the proposition-level interface for A7 on causal plus scale-free closure within the DIF paper. Cosmologists and network theorists working from the RS foundation would cite it when closing scaling relations for large-scale structure. The declaration is a pure structure definition that asserts the conjunction without derivation or additional lemmas.
Claim. Let $k$ be a mode number and $a$ a scale factor. A structure consists of real numbers $beta, gamma$ together with the assertion $beta = 1$ and $gamma = 1$, which enforces that the effective frequency satisfies $omega_{eff} proportional to k^{1} a^{-1}$.
background
Recognition Science models cosmological mode frequencies with power-law scalings on wavenumber and scale factor. The structure collects the two exponents under the single constraint that dimensional forcing requires both to equal unity. Upstream results supply the scale function defined as phi raised to the integer power k and the Euler-Mascheroni constant, though the gamma field here denotes the scaling exponent rather than the constant. The local setting is the DIF paper's treatment of causal closure, where this structure serves as the explicit interface for proposition A7.
proof idea
The declaration is a structure definition whose sole content is the field dimensional_forcing carrying the conjunction beta = 1 and gamma = 1. No lemmas are applied; the construction is a direct packaging of the forcing condition.
why it matters
This declaration supplies the proposition-level interface for A7 on causal plus scale-free closure. It sits inside the forcing chain after the eight-tick octave and D = 3 are fixed, ensuring that closure scaling remains linear in k and inverse in a. No downstream theorems are recorded, indicating it functions as an early packaging step before integration with the phi-ladder or RCL. It touches the open question of how the resulting closure interacts with the mass formula yardstick times phi to the power (rung minus 8 plus gap).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.