HQVMetric — Horizon Quantized Vacuum Metric (Non-FLRW) and Effective Friedmann Equation

HQIV is not FLRW: the background is the Horizon-Quantized Vacuum Metric (HQVM), which is inhomogeneous (Φ, φ depend on position/time). We adopt synchronous-comoving gauge (shift βⁱ = 0). The ADM lapse N is fixed by the informational-energy axiom and the horizon-overlap coefficient γ (paper: N = 1 + Φ + φ t/c; natural units: N = 1 + Φ + φ t). The line element is ds² = -N² dt² + a(t)²(1 - 2Φ) δᵢⱼ dxⁱ dxʲ.

This module provides:

• ADM lapse: definition and proof that the HQVM metric has lapse N = 1 + Φ + φ t (see HQVM_lapse and HQVM_tt_coefficient).
• Homogeneous limit: γ, G_eff, and the declarative Friedmann equation (φ ≈ H, used for volume-averaged dynamics and CLASS). For the exact lapse increment δN around Φ = 0 with background φ = H, see HQVM_lapse_increment_homogeneous in Hqiv.Geometry.HQVMPerturbations (first-order piece linearizedHQVM_lapse, remainder δφ δt).

The theory is built from the canonical HQIV pair (curvature imprint α = 3/5, monogamy γ = 2/5 with γ = 1 − α); physical derivation of these as the only such constants in the companion program is in the companion HQIV manuscript and Brodie (2026). The lapse formula encodes observer-centric time (wall-clock vs apparent age).

√3 vs 2π: The curvature norm (light-cone module) uses √3 — a spatial factor (unit-cube half-diagonal, dimension length). The time phase here uses 2π — an angular period (dimension angle). So they are not the same kind of constant: one is geometry of the 3D cube, the other is the period of phase. No conflict.

Arriving at the definitions (derivation path)

We do not introduce free parameters. Each definition is determined by prior structure:

1. Lapse N: The informational-energy axiom (paper) fixes the ADM lapse in synchronous-comoving gauge to N = 1 + Φ + φ t. So HQVM_lapse is the unique form imposed by that axiom; we then prove it equals 1 + Φ + timeAngle φ t.

2. Time angle δθ′: φ is already fixed by the lattice (AuxiliaryField: φ(m) = 2/T(m)). The horizon term in N is φ t, which we call timeAngle; it is the only cumulative-in-time piece, so it is determined by the lapse decomposition.

3. Metric components: With shift βⁱ = 0, the line element is ds² = -N² dt² + spatial. So g_tt = -N² and the spatial coefficient is a²(1 - 2Φ) from ADM with conformal factor (1 - 2Φ). No choice — just writing the metric in this gauge.

4. γ: The sole HQIV monogamy coefficient, γ := 1 − α, proved 2/5 once α = 3/5 (gamma_eq_2_5). Same external provenance as α (companion HQIV + Brodie 2026). Then (3−γ) = 13/5 and α + γ = 1 from the split.

5. G₀, H₀: Natural units (c = ħ = 1, G₀ = H₀ = 1). Convention, not a free fit; we prove G_eff(1) = 1 when φ = H₀.

6. G_eff: The paper’s varying-G relation G_eff/G₀ = (H/H₀)^α with α from the lattice (3/5). So G_eff(φ) = φ^α in natural units — determined by α and the homogeneous identification H = φ.

7. Friedmann equation: (3−γ)H² = 8π G_eff(φ)(ρ_m + ρ_r) is the Einstein equation in the homogeneous HQVM limit with varying G. So the def HQVM_Friedmann_eq is the statement of that equation; we then prove rational form, vacuum iff φ = 0, and sign of (3−γ). The CLASS density / Picard algebra (ρ_crit = 8πρ/3 at G = 1, squared-H rescaling, fixed point of the square-root map) is proved equivalent in Hqiv.Geometry.HQVMCLASSBridge (section CLASSBackgroundMethodology).

Thus the proven theory in this file rests on the light-cone (α, φ, curvature), monogamy (γ), natural units, and the informational-energy axiom; the defs are arrived at by fixing those, not by tuning.

HQVM metric and ADM lapse (non-homogeneous)

The full HQVM is not FLRW. In synchronous-comoving gauge (shift βⁱ = 0) the lapse N is fixed by the informational-energy axiom: N = 1 + Φ + φ t (natural units). We define the lapse as that expression and then prove all subsequent structure.

def Hqiv.HQVM_lapse (Φ φ t : ℝ) : ℝ

ADM lapse (determined by the informational-energy axiom): N = 1 + Φ + φ t. Φ = Newtonian potential; φ = auxiliary field from the lattice (2/Θ); t = coordinate time. The term φ t is the horizon contribution (time angle). So this def is the unique lapse imposed by the axiom in synchronous-comoving gauge.

Equations

• Hqiv.HQVM_lapse Φ φ t = 1 + Φ + φ * t

def Hqiv.timeAngle (φ t : ℝ) : ℝ

Time angle (δθ′) from the observer: φ · t (natural units).

From the observer’s perspective, the time angle is the cumulative phase that allows interaction with newly unlocked horizon modes. Those modes are the ones from the curvature already proved in the light-cone module: shell-wise mode count (new_modes, available_modes), curvature imprint (δE, shell_shape), and curvature integral / Ω_k at the chosen horizon. So δθ′ = φ t is not an extra degree of freedom: φ is tied to the lattice (e.g. φ(m) = 2/T(m) in AuxiliaryField), and as t advances the observer couples to the next shell’s unlocked modes from that curvature.

Equations

• Hqiv.timeAngle φ t = φ * t

theorem Hqiv.HQVM_lapse_eq_timeAngle (Φ φ t : ℝ) : HQVM_lapse Φ φ t = 1 + Φ + timeAngle φ t

Lapse equals 1 + Φ + time angle: N = 1 + Φ + δθ′.

theorem Hqiv.ADM_lapse_eq_HQVM_lapse (Φ φ t : ℝ) : HQVM_lapse Φ φ t = 1 + Φ + φ * t

ADM lapse is the HQVM lapse: In the HQVM line element ds² = -N² dt² + a(t)²(1 - 2Φ) δᵢⱼ dxⁱ dxʲ with shift zero, the lapse function (the function N such that g_tt = -N²) is N = 1 + Φ + φ t = 1 + Φ + timeAngle φ t.

theorem Hqiv.lapse_decompose (Φ φ t : ℝ) : HQVM_lapse Φ φ t = 1 + Φ + timeAngle φ t

Time angle is the horizon term in the lapse: N = 1 + Φ + timeAngle φ t.

theorem Hqiv.timeAngle_mono_t (φ t₁ t₂ : ℝ) (hφ : 0 < φ) (ht : t₁ ≤ t₂) : timeAngle φ t₁ ≤ timeAngle φ t₂

Time angle is monotone in t when φ > 0: more coordinate time ⇒ larger δθ′ ⇒ (in the narrative) interaction with more unlocked horizon modes.

theorem Hqiv.timeAngle_zero_t (φ : ℝ) : timeAngle φ 0 = 0

Time angle at t = 0: δθ′ = 0 (no cumulative horizon phase yet).

noncomputable def Hqiv.twoPi : ℝ

Period of the time angle: 2π (one full phase turn). Spin lost to the horizon is conserved as phase: the time angle is interpreted mod 2π, so no spin is destroyed, only wrapped. This is angular (2π); the curvature norm’s √3 is spatial (unit-cube half-diagonal) — different dimensions.

Equations

• Hqiv.twoPi = 2 * Real.pi

theorem Hqiv.twoPi_eq : twoPi = 2 * Real.pi

theorem Hqiv.timeAngle_first_period (φ : ℝ) (hφ : 0 < φ) : timeAngle φ (twoPi / φ) = twoPi

Time angle reaches 2π at the first period: when φ > 0, δθ′ = 2π at t = 2π/φ.

theorem Hqiv.timeAngle_mem_Icc_first_period (φ t : ℝ) (hφ : 0 < φ) (ht0 : 0 ≤ t) (ht : t ≤ twoPi / φ) : timeAngle φ t ∈ Set.Icc 0 twoPi

Time angle in the first period: for φ > 0 and t ∈ [0, 2π/φ], δθ′ ∈ [0, 2π]. So the time angle sweeps [0, 2π] as t goes from 0 to the first period.

theorem Hqiv.timeAngle_limit_zero (φ : ℝ) : timeAngle φ 0 = 0

Lower limit: at t = 0 the time angle is 0 (already in timeAngle_zero_t).

theorem Hqiv.timeAngle_limit_twoPi (φ : ℝ) (hφ : 0 < φ) : timeAngle φ (twoPi / φ) = twoPi

Upper limit (first period): at t = 2π/φ the time angle is 2π.

Spin conserved at the horizon

The time angle δθ′ is periodic mod 2π. Spin lost to the horizon is not destroyed: it is encoded in the phase (δθ′ mod 2π), which wraps in [0, 2π). So total spin (phase) is conserved; the horizon only resets the angle every 2π. This is the conservation statement for spin lost to the horizon.

theorem Hqiv.timeAngle_zero_to_twoPi (φ : ℝ) (hφ : 0 < φ) : timeAngle φ 0 = 0 ∧ timeAngle φ (twoPi / φ) = twoPi ∧ ∀ t ∈ Set.Icc 0 (twoPi / φ), timeAngle φ t ∈ Set.Icc 0 twoPi

Spin conservation (narrative): the time angle in [0, 2π] and its periodic extension mod 2π encodes the phase of modes locked at the horizon; that phase is conserved (wraps rather than being lost).

theorem Hqiv.HQVM_lapse_homogeneous_limit (H t : ℝ) : HQVM_lapse 0 H t = 1 + H * t

In the homogeneous limit (Φ = 0, φ = H) the lapse is N = 1 + H t.

theorem Hqiv.HQVM_lapse_Minkowski (t : ℝ) : HQVM_lapse 0 0 t = 1

Minkowski limit: when Φ = 0 and φ = 0 the lapse is N = 1.

theorem Hqiv.HQVM_lapse_at_zero (Φ φ : ℝ) : HQVM_lapse Φ φ 0 = 1 + Φ

Lapse at t = 0: N = 1 + Φ (no time-angle contribution yet).

theorem Hqiv.HQVM_lapse_mono_t (Φ φ t₁ t₂ : ℝ) (hφ : 0 ≤ φ) (ht : t₁ ≤ t₂) : HQVM_lapse Φ φ t₁ ≤ HQVM_lapse Φ φ t₂

Lapse is monotone in t when φ ≥ 0: t₁ ≤ t₂ ⇒ N(Φ, φ, t₁) ≤ N(Φ, φ, t₂).

theorem Hqiv.HQVM_lapse_pos (Φ φ t : ℝ) (h₁ : 0 < 1 + Φ) (hφ : 0 ≤ φ) (ht : 0 ≤ t) : 0 < HQVM_lapse Φ φ t

Lapse is positive when 1 + Φ > 0 and φ ≥ 0, t ≥ 0. So in the weak-field (Φ > -1) and forward-time, non-negative φ regime, N > 0 and g_tt < 0 (timelike t).

theorem Hqiv.HQVM_lapse_gt_one (Φ φ t : ℝ) (hΦ : 0 ≤ Φ) (hφ : 0 < φ) (ht : 0 < t) : 1 < HQVM_lapse Φ φ t

Lapse above Minkowski when Φ ≥ 0, φ > 0, t > 0: N > 1.

HQVM manifold geometry

The line element is ds² = -N² dt² + a(t)²(1 - 2Φ) δᵢⱼ dxⁱ dxʲ. We formalise the metric components and prove Lorentzian signature and positive-definite spatial part under natural physical assumptions (N ≠ 0, a > 0, weak field Φ < 1/2).

def Hqiv.HQVM_g_tt (N : ℝ) : ℝ

Time-time component g_tt = -N². Determined by the ADM decomposition with shift zero: the line element is -N² dt² + spatial, so g_tt is minus the lapse squared.

Equations

• Hqiv.HQVM_g_tt N = -N ^ 2

def Hqiv.HQVM_spatial_coeff (a Φ : ℝ) : ℝ

Spatial conformal factor a²(1 - 2Φ). Determined by the ADM metric in synchronous-comoving gauge: the spatial part is a(t)²(1 - 2Φ) δᵢⱼ, so this is the coefficient of each dxⁱ dxⁱ (no free choice — just the gauge and potential Φ).

Equations

• Hqiv.HQVM_spatial_coeff a Φ = a ^ 2 * (1 - 2 * Φ)

theorem Hqiv.HQVM_g_tt_neg (N : ℝ) (hN : N ≠ 0) : HQVM_g_tt N < 0

g_tt is negative whenever N ≠ 0, so the coordinate t is timelike (Lorentzian time direction).

theorem Hqiv.HQVM_spatial_coeff_pos (a Φ : ℝ) (ha : 0 < a) (hΦ : Φ < 1 / 2) : 0 < HQVM_spatial_coeff a Φ

Spatial coefficient is positive when a > 0 and Φ < 1/2 (weak-field regime: the Newtonian potential does not dominate). So the spatial metric is Riemannian.

theorem Hqiv.HQVM_ADM_decomposition (Φ φ t a : ℝ) : HQVM_g_tt (HQVM_lapse Φ φ t) = -HQVM_lapse Φ φ t ^ 2 ∧ HQVM_spatial_coeff a Φ = a ^ 2 * (1 - 2 * Φ)

ADM decomposition of the HQVM metric: with lapse N = HQVM_lapse Φ φ t and shift zero, the line element has g_tt = -N² and spatial diagonal coefficient a²(1 - 2Φ). So the manifold is foliated by spatial hypersurfaces Σ_t with induced metric a(t)²(1 - 2Φ) δᵢⱼ.

theorem Hqiv.HQVM_geometry_Minkowski (t : ℝ) : HQVM_g_tt (HQVM_lapse 0 0 t) = -1 ∧ HQVM_spatial_coeff 1 0 = 1

Minkowski limit of the geometry: Φ = 0, φ = 0, a = 1 gives g_tt = -1 and spatial coefficient 1 (flat spacetime).

theorem Hqiv.HQVM_unit_normal_squared (N : ℝ) (hN : N ≠ 0) : HQVM_g_tt N * (1 / N) ^ 2 = -1

Unit normal to constant-t hypersurfaces: with shift zero, the future-pointing normal is n = (1/N) ∂_t; its squared norm is g_tt · (1/N)² = -1, so n is timelike and unit.

theorem Hqiv.HQVM_spatial_coeff_expand (a Φ : ℝ) : HQVM_spatial_coeff a Φ = a ^ 2 - 2 * a ^ 2 * Φ

Spatial coefficient expanded: a²(1 - 2Φ) = a² - 2a²Φ.

theorem Hqiv.HQVM_g_tt_neg_of_lapse_pos (Φ φ t : ℝ) (hN : 0 < HQVM_lapse Φ φ t) : HQVM_g_tt (HQVM_lapse Φ φ t) < 0

Lorentzian signature (g_tt < 0) when the lapse is positive: N > 0 ⇒ g_tt < 0.

def Hqiv.gamma_HQIV : ℝ

γ — the only HQIV monogamy / horizon-overlap coefficient: complement of α on the unit horizon split, γ = 1 − α. Provenance matches alpha (companion HQIV manuscript + Brodie 2026). No alternate gamma in the codebase.

Equations

• Hqiv.gamma_HQIV = 1 - Hqiv.alpha

theorem Hqiv.gamma_eq_2_5 : gamma_HQIV = 2 / 5

γ = 2/5 — derived from α = 3/5 and the split α + γ = 1 (so γ = 1 − 3/5 = 2/5).

theorem Hqiv.gamma_eq_paper : gamma_HQIV = 0.40

γ equals the paper value 0.40 (2/5 = 0.40).

theorem Hqiv.alpha_add_gamma : alpha + gamma_HQIV = 1

Division of the horizon: α (lattice) + γ (monogamy) = 1. Holds by definition of γ = 1 − α.

theorem Hqiv.three_minus_gamma_eq : 3 - gamma_HQIV = 13 / 5

Coefficient (3 − γ) in the Friedmann equation equals 13/5. Derived from γ = 2/5.

theorem Hqiv.three_minus_gamma_pos : 0 < 3 - gamma_HQIV

(3 − γ) is positive (13/5 > 0); so the H² term in the Friedmann equation has the correct sign for an expanding universe.

def Hqiv.G0 : ℝ

G₀ (natural units): reference Newton coupling = 1. Convention: we set G₀ = 1, so all couplings are relative to it; no free parameter.

Equations

• Hqiv.G0 = 1.0

theorem Hqiv.G0_eq : G0 = 1

G₀ = 1 in natural units (proved).

def Hqiv.H0 : ℝ

H₀ (natural units): reference Hubble rate = 1. Same convention: H₀ = 1, so G_eff(1) = 1 when φ = H₀.

Equations

• Hqiv.H0 = 1.0

theorem Hqiv.H0_eq : H0 = 1

H₀ = 1 in natural units (proved).

def Hqiv.H_of_phi (φ : ℝ) : ℝ

H(φ) (homogeneous limit): we identify φ with H in natural units (φ ≈ H). So H_of_phi φ = φ. This is the bridge from the lattice field φ to the Hubble rate in the Friedmann equation; not an extra degree of freedom.

Equations

• Hqiv.H_of_phi φ = φ

theorem Hqiv.H_of_phi_eq (φ : ℝ) : H_of_phi φ = φ

H(φ) = φ (proved).

noncomputable def Hqiv.G_eff (φ : ℝ) : ℝ

G_eff(φ) (determined by the varying-G relation and the lattice α). Paper: G_eff/G₀ = (H/H₀)^α; with H = φ (homogeneous) and G₀ = H₀ = 1 we get G_eff(φ) = φ^α. So this def is arrived at from α (from the light cone) and natural units — no extra fit.

Equations

• Hqiv.G_eff φ = Hqiv.G0 * (Hqiv.H_of_phi φ / Hqiv.H0) ^ Hqiv.alpha

theorem Hqiv.G_eff_eq (φ : ℝ) (_hφ : 0 ≤ φ) : G_eff φ = φ ^ alpha

G_eff in terms of φ and α only: when G₀ = H₀ = 1, G_eff(φ) = φ^α (φ ≥ 0).

theorem Hqiv.G_eff_one : G_eff 1 = 1

G_eff at unit Hubble: when φ = 1 (H = H₀ in natural units), G_eff(1) = 1 = G₀.

def Hqiv.rho_total (rho_m rho_r : ℝ) : ℝ

Total homogeneous energy density (matter + radiation).

Equations

• Hqiv.rho_total rho_m rho_r = rho_m + rho_r

theorem Hqiv.rho_total_eq (rho_m rho_r : ℝ) : rho_total rho_m rho_r = rho_m + rho_r

Total density is the sum (proved).

def Hqiv.HQVM_Friedmann_eq (φ rho_m rho_r : ℝ) : Prop

Friedmann equation (arrived at from Einstein eqn in homogeneous HQVM limit). (3 − γ) H² = 8 π G_eff(φ) (ρ_m + ρ_r) (3−γ) from monogamy, H = φ, G_eff from varying-G and α. So this is the statement of the dynamics, not a new definition — we then prove rational form (13/5)φ² = …, vacuum iff φ = 0, and LHS nonnegativity.

Equations

• Hqiv.HQVM_Friedmann_eq φ rho_m rho_r = ((3.0 - Hqiv.gamma_HQIV) * Hqiv.H_of_phi φ ^ 2 = 8.0 * Real.pi * Hqiv.G_eff φ * Hqiv.rho_total rho_m rho_r)

theorem Hqiv.HQVM_Friedmann_eq_def (φ rho_m rho_r : ℝ) : HQVM_Friedmann_eq φ rho_m rho_r ↔ (3.0 - gamma_HQIV) * H_of_phi φ ^ 2 = 8.0 * Real.pi * G_eff φ * rho_total rho_m rho_r

Trivial unfolding lemma: spelling out HQVM_Friedmann_eq.

theorem Hqiv.HQVM_Friedmann_eq_rational (φ rho_m rho_r : ℝ) : HQVM_Friedmann_eq φ rho_m rho_r ↔ 13 / 5 * φ ^ 2 = 8 * Real.pi * G_eff φ * (rho_m + rho_r)

Friedmann equation in rational form: (3−γ) = 13/5, so the equation is (13/5) φ² = 8π G_eff(φ) (ρ_m + ρ_r).

theorem Hqiv.HQVM_Friedmann_eq_power (φ rho_m rho_r : ℝ) (hφ : 0 ≤ φ) : HQVM_Friedmann_eq φ rho_m rho_r ↔ 13 / 5 * φ ^ 2 = 8 * Real.pi * φ ^ alpha * (rho_m + rho_r)

Friedmann equation with G_eff as φ^α (φ ≥ 0): (13/5) φ² = 8π φ^α (ρ_m + ρ_r).

theorem Hqiv.HQVM_Friedmann_eq_vacuum_iff (φ : ℝ) : HQVM_Friedmann_eq φ 0 0 ↔ φ = 0

Vacuum (Minkowski) case: when ρ_m = ρ_r = 0, the Friedmann equation holds iff φ = 0. So in the vacuum the only homogeneous solution is H = 0.

theorem Hqiv.HQVM_Minkowski_iff_vacuum (φ : ℝ) : (∀ (t : ℝ), HQVM_lapse 0 φ t = 1) ↔ φ = 0

Minkowski limit and Friedmann vacuum agree: when Φ = 0, φ = 0, the lapse is 1 and the Friedmann equation (vacuum) holds for φ = 0. So the Minkowski geometry is the unique vacuum homogeneous limit.

theorem Hqiv.HQVM_Friedmann_LHS_nonneg (φ : ℝ) : 0 ≤ (3 - gamma_HQIV) * φ ^ 2

Friedmann equation: left-hand side (3−γ)φ² is nonnegative when φ is real; so with positive ρ, the equation constrains φ.