HQIV Auxiliary Field φ

The auxiliary scalar field φ in the homogeneous limit encodes the horizon-entanglement and varying-coupling effect that feeds into the HQVM metric and effective Friedmann dynamics.

All definitions here are in natural Planck units (T_Pl = 1, c = 1). The field is tied directly to the same temperature ladder that underlies the curvature imprint.

def Hqiv.phiTemperatureCoeff : ℝ

Coefficient in φ = (this) / Θ. In the paper, φ(m) = 2/Θ_local(m); we identify Θ_local with the temperature ladder T(m). So the numerator is 2 — one unit per "quadrant" of the universal cutout (0 < x < Θ). Not inserted: it is the fixed ratio from the homogeneous limit (two axioms: light-cone + informational-energy).

Equations

• Hqiv.phiTemperatureCoeff = 2

theorem Hqiv.phiTemperatureCoeff_eq_two : phiTemperatureCoeff = 2

phiTemperatureCoeff equals 2 (the paper's φ = 2/Θ convention).

theorem Hqiv.phiTemperatureCoeff_pos : 0 < phiTemperatureCoeff

phiTemperatureCoeff is positive (so φ(m) = phiTemperatureCoeff/T(m) is well-defined).

noncomputable def Hqiv.T_Pl : ℝ

Planck temperature in natural units.

Equations

• Hqiv.T_Pl = 1.0

theorem Hqiv.T_Pl_eq : T_Pl = 1

T_Pl = 1 in natural units (proved).

noncomputable def Hqiv.T (m : ℕ) : ℝ

Temperature at radial shell m (HQIV temperature ladder).

Equations

• Hqiv.T m = Hqiv.T_Pl / (↑m + 1)

theorem Hqiv.T_eq (m : ℕ) : T m = 1 / (↑m + 1)

Temperature ladder in closed form (no separate def): T(m) = 1/(m+1).

theorem Hqiv.T_pos (m : ℕ) : 0 < T m

T(m) is positive for all shells (temperature ladder in natural units).

noncomputable def Hqiv.phi_of_shell (m : ℕ) : ℝ

Auxiliary field φ at shell m in the homogeneous limit.

Formally φ(m) = phiTemperatureCoeff / Θ_local(m); here we identify Θ_local(m) with the temperature ladder T(m). The coefficient is 2 from the paper (quadrant structure).

Equations

• Hqiv.phi_of_shell m = Hqiv.phiTemperatureCoeff / Hqiv.T m

noncomputable def Hqiv.phi_of_T (t : ℝ) : ℝ

Continuous version of the auxiliary field as a function of local temperature.

Equations

• Hqiv.phi_of_T t = Hqiv.phiTemperatureCoeff / t

theorem Hqiv.phi_of_shell_eq_phi_of_T (m : ℕ) : phi_of_shell m = phi_of_T (T m)

Bridge lemma: the discrete shell version equals the continuous version.

theorem Hqiv.phi_of_shell_closed_form (m : ℕ) : phi_of_shell m = phiTemperatureCoeff * (↑m + 1)

Helper: explicit closed form for φ(m) in terms of the shell index.

theorem Hqiv.phi_of_shell_pos (m : ℕ) : 0 < phi_of_shell m

φ(m) is positive and φ(m) ≥ phiTemperatureCoeff for all shells (φ(0) = 2, then grows).

theorem Hqiv.phi_of_shell_ge_two (m : ℕ) : phiTemperatureCoeff ≤ phi_of_shell m

theorem Hqiv.shell_shape_in_terms_of_phi (m : ℕ) : shell_shape m = 1 / (phi_of_shell m / phiTemperatureCoeff) * (1 + alpha * Real.log (phi_of_shell m / phiTemperatureCoeff))

Key connection lemma: shell_shape can be expressed purely in terms of φ.

Using the closed form φ(m) = 2(m+1), we have φ(m)/2 = m+1, so the original shell shape shell_shape m = (1/(m+1)) * (1 + α log(m+1)) can be rewritten with the argument φ(m)/2. This makes φ reusable on the HQVM / Friedmann side without duplicating the curvature definitions.

theorem Hqiv.shell_shape_T_formula (m : ℕ) : shell_shape m = 1 / (↑m + 1) * (1 + alpha * Real.log (T_Pl / T m))

Shell shape from the temperature ladder:

Starting from the paper's expression [ \text{shell_shape}(m) = \frac{1}{m+1}\Bigl(1 + \alpha \log\frac{T_{\rm Pl}}{T(m)}\Bigr), ] and using the HQIV temperature ladder T m = T_Pl / (m+1) with T_Pl = 1 (T_eq and T_Pl_eq), we recover exactly the same formula used to define shell_shape and curvatureDensity. This shows that the shape is derived from the discrete temperature ladder, not an independent input.