hubbleRadiusModel
plain-language theorem explainer
Packs a positive comoving radius and integer rung count into the Hubble-radius horizon model, with causal-accumulation and future-info flags both false. Cosmologists comparing vacuum-energy candidates cite it when the instantaneous Hubble sphere is excluded from the ledger sum. Pure structure constructor: fields are assigned, no proof obligations.
Claim. For any comoving radius $r > 0$ and integer rung count $s$, the Hubble-radius horizon model is the horizon datum with type Hubble radius, comoving radius $r$, positivity witness for $r$, rung count $s$, not causally accumulated, and not requiring future information.
background
The module forces which cosmological horizon enters the vacuum-energy rung count. The vacuum density is written $\rho_\Lambda = \rho_{\mathrm{Pl}},\varphi^{-2s}$ with $s$ the rung from the substrate scale to a horizon radius. Three candidates (particle horizon, Hubble radius, de Sitter event horizon) give three different $s$ and three different $\rho_\Lambda/\rho_{\mathrm{obs}}$ ratios; only the particle horizon lands near unity.
A horizon model is a structure carrying type tag, positive comoving radius, rung count, and two Boolean flags: whether the horizon is causally accumulated (past light-cone contact set) and whether it needs future expansion history. Horizon type is an inductive with the three candidates above.
The causal-accumulation principle says the vacuum ledger cost is the ground-state total over the maximal causally connected region. That boundary is the particle horizon by definition. The Hubble radius is only the instantaneous $v_{\mathrm{rec}}=c$ surface, so past-connected cells outside it still sit in the ledger.
proof idea
Definitional structure constructor, not a theorem. Given $r>0$ and $s:\mathbb{Z}$, it builds a horizon model by setting type to Hubble radius, copying the radius and positivity proof, copying the rung count, and hard-wiring both Boolean flags to false (not causally accumulated; does not require future information). No lemmas are applied.
why it matters
Supplies the middle row of the three-horizon comparison table that drives vacuum-horizon forcing. Sibling results use the false causal-accumulation flag to exclude the Hubble sphere: cells once in causal contact remain in the ledger even if their present recession speed exceeds $c$. That exclusion, together with the de Sitter model's future-info requirement, leaves the particle horizon as the unique causally accumulated choice, matching $\rho_\Lambda$ at rung $s\approx 294$.
In the broader Recognition ladder, the selected $s$ fixes the vacuum rung relative to the substrate and the $\varphi$-scaling of densities. No downstream dependents are wired yet in the graph; the definition is scaffolding for the selection lemmas in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.