def Hqiv.latticeSimplexCount (m : ℕ) : ℕ

Discrete null-lattice mode counting (Nat version).

latticeSimplexCount m is the pure stars-and-bars count of integer solutions to x + y + z = m with x,y,z ≥ 0, i.e. [ \binom{m+2}{2} = \frac{(m+2)(m+1)}{2}. ] We keep the factor of (1/2) implicit and work with the numerator (m+2)*(m+1); the octonionic lift and normalisations are handled separately.

Equations

• Hqiv.latticeSimplexCount m = (m + 2) * (m + 1)

theorem Hqiv.latticeSimplexCount_zero : latticeSimplexCount 0 = 2 * 1

Base check: at m = 0 there is exactly one lattice point (0,0,0).

theorem Hqiv.latticeSimplexCount_one : latticeSimplexCount 1 = 3 * 2

Base check: at m = 1 there are exactly three lattice points.

theorem Hqiv.latticeSimplexCount_two : latticeSimplexCount 2 = 4 * 3

Base check: at m = 2 there are exactly six lattice points.

theorem Hqiv.latticeSimplexCount_eq (m : ℕ) : latticeSimplexCount m = (m + 2) * (m + 1)

Closed form: lattice count is the stars-and-bars numerator (no separate def).

theorem Hqiv.latticeSimplexCount_pos (m : ℕ) : 0 < latticeSimplexCount m

Lattice count is positive (every shell has at least one mode).

theorem Hqiv.two_dvd_latticeSimplexCount (m : ℕ) : 2 ∣ latticeSimplexCount m

Division in the lattice: the stars-and-bars numerator (m+2)(m+1) is even (one of two consecutive naturals is even), so 2 ∣ latticeSimplexCount m.

theorem Hqiv.latticeSimplexCount_cast (m : ℕ) : ↑(latticeSimplexCount m) = (↑m + 2) * (↑m + 1)

Cast to ℝ: (latticeSimplexCount m : ℝ) = (m+2)(m+1).

def Hqiv.cumLatticeSimplexCount : ℕ → ℕ

Cumulative simplex count up to shell n: cumLatticeSimplexCount n = ∑_{m=0}^{n} latticeSimplexCount m.

Equations

• Hqiv.cumLatticeSimplexCount 0 = Hqiv.latticeSimplexCount 0
• Hqiv.cumLatticeSimplexCount n.succ = Hqiv.cumLatticeSimplexCount n + Hqiv.latticeSimplexCount (n + 1)

theorem Hqiv.cumLatticeSimplexCount_zero : cumLatticeSimplexCount 0 = latticeSimplexCount 0

Explicit unfolding for small n (sanity checks).

theorem Hqiv.cumLatticeSimplexCount_one : cumLatticeSimplexCount 1 = latticeSimplexCount 0 + latticeSimplexCount 1

theorem Hqiv.cumLatticeSimplexCount_two : cumLatticeSimplexCount 2 = latticeSimplexCount 0 + latticeSimplexCount 1 + latticeSimplexCount 2

theorem Hqiv.cumLatticeSimplexCount_hockey_stick (n : ℕ) : 3 * cumLatticeSimplexCount n = (n + 1) * (n + 2) * (n + 3)

Hockey-stick: 3 × cumulative count = (n+1)(n+2)(n+3); the 1/6 factor in the paper comes from the 3! in the binomial.

theorem Hqiv.cumLatticeSimplexCount_closed (n : ℕ) : cumLatticeSimplexCount n = (n + 1) * (n + 2) * (n + 3) / 3

Closed form (arrived at from hockey-stick): cum = (n+1)(n+2)(n+3)/3. So the cumulative count is determined by the binomial, not just the recurrence.

theorem Hqiv.three_dvd_cum_numerator (n : ℕ) : 3 ∣ (n + 1) * (n + 2) * (n + 3)

Division in the lattice: the binomial numerator (n+1)(n+2)(n+3) is divisible by 3. So the cumulative mode count is an integer; the 1/3 comes from the 3D simplex (stars-and-bars).

theorem Hqiv.cumLatticeSimplexCount_succ_ge (n : ℕ) : cumLatticeSimplexCount n ≤ cumLatticeSimplexCount (n + 1)

One-step monotonicity: adding shell n+1 only increases the cumulative count.

theorem Hqiv.cumLatticeSimplexCount_le_add (m k : ℕ) : cumLatticeSimplexCount m ≤ cumLatticeSimplexCount (m + k)

Inequality across multiple shells: for all k,
cumLatticeSimplexCount m ≤ cumLatticeSimplexCount (m + k).

theorem Hqiv.cumLatticeSimplexCount_monotone {m n : ℕ} (h : m ≤ n) : cumLatticeSimplexCount m ≤ cumLatticeSimplexCount n

Global monotonicity: if m ≤ n then
cumLatticeSimplexCount m ≤ cumLatticeSimplexCount n.

theorem Hqiv.cumLatticeSimplexCount_pos (n : ℕ) : 0 < cumLatticeSimplexCount n

Cumulative simplex count is positive (every shell contributes at least one mode).

def Hqiv.available_modes (m : ℕ) : ℝ

The single axiom of HQIV
At each discrete radial step m in the observer's past light-cone,
the number of newly available modes is exactly the stars-and-bars count
for x + y + z = m (3D null lattice) multiplied by the octonion factor 8.

This combinatorial rule is the complete foundation of the model; the theory is built from division math (rational counts, 1/3 in the cumulative sum, α = 3/5 from lattice dimension) and, in the metric sector, monogamy (γ = 2/5). Repeated radial application yields α = 0.60 (growth rate) and
the permanent positive curvature limit Ω_k^true = 0.0098
(density of new available modes per radial step in the limit).

In the Lean development we tie the numeric mode count directly to the Nat-level lattice simplex count via a simple Float cast.

Equations

• Hqiv.available_modes m = 4 * ↑(Hqiv.latticeSimplexCount m)

theorem Hqiv.available_modes_eq (m : ℕ) : available_modes m = 4 * (↑m + 2) * (↑m + 1)

Available modes in closed form (ℝ): 4(m+2)(m+1).

theorem Hqiv.available_modes_octonion (m : ℕ) : available_modes m = 8 * (↑(latticeSimplexCount m) / 2)

Factor 4 from octonion × binomial: available_modes = 8 × (stars-and-bars count in ℝ). Paper: new modes = 8 × C(m+2,2); we have 2·C(m+2,2) = (m+2)(m+1), so 8·C = 4·(m+2)(m+1).

def Hqiv.new_modes (m : ℕ) : ℝ

New modes added at shell m (incremental growth from the axiom). These are the newly unlocked horizon modes the observer interacts with via the time angle δθ′ = φ t in the HQVM metric; curvature (δE, shell_shape, Ω_k) is tied to the same shells.

Equations

• Hqiv.new_modes m = if m = 0 then Hqiv.available_modes 0 else Hqiv.available_modes m - Hqiv.available_modes (m - 1)

theorem Hqiv.new_modes_zero : new_modes 0 = available_modes 0

New modes at shell 0: by definition, new_modes 0 = available_modes 0.

theorem Hqiv.new_modes_succ (m : ℕ) : new_modes (m + 1) = 8 * (↑m + 2)

New modes in closed form (m ≥ 1): new_modes (m+1) = 8(m+2). Follows from available_modes (m+1) - available_modes m and latticeSimplexCount difference.

def Hqiv.alpha : ℝ

HQIV varying-G exponent α — the only curvature-imprint exponent used in this formalism.

Provenance: the physical derivation that this exponent is (3/5) (and that it is the unique HQIV curvature imprint in the companion theory) is given in the companion HQIV manuscript and in Brodie (2026), not reproved here; Lean encodes the identification and proves alpha_eq_3_5.

Same dimensionless index as in the Python curvature pipeline (alpha = 0.60 in discrete_baryogenesis_horizon.py and main.tex), i.e. how (G_\mathrm{eff}) (or curvature imprint) scales with the shell temperature. In Lean, α is identified with the lattice ratio (n+1)(n+2)(n+3)/(5·cum n) for every n via latticeAlphaRatio_eq_alpha (hockey-stick); see also tendsto_latticeAlphaRatio.

Equations

• Hqiv.alpha = 0.60

theorem Hqiv.alpha_eq_3_5 : alpha = 3 / 5

α equals 3/5 exactly. The paper's 0.60 is the rational 3/5 (proved).

theorem Hqiv.alpha_eq_lattice_rational : alpha = 3 / (3 + 2)

α as lattice rational: α = 3/(3+2) = 3/5. The 3 is the effective growth exponent of the cumulative mode count on the 3D null lattice (hockey-stick); the 5 = 3+2 comes from stars-and-bars (binomial (m+2 choose 2)). The discrete ratio equals 3/5 for every n (latticeAlphaRatio_eq_alpha), not only in the limit.

noncomputable def Hqiv.latticeAlphaRatio (n : ℕ) : ℝ

Lattice-derived ratio: (n+1)(n+2)(n+3) / (5 · cum n) in ℝ. By the hockey-stick identity 3·cum n = (n+1)(n+2)(n+3), this equals 3/5 for every n.

Equations

• Hqiv.latticeAlphaRatio n = (↑n + 1) * (↑n + 2) * (↑n + 3) / (5 * ↑(Hqiv.cumLatticeSimplexCount n))

theorem Hqiv.latticeAlphaRatio_eq_alpha (n : ℕ) : latticeAlphaRatio n = alpha

α in the lattice: the lattice ratio equals α for every shell count n.

theorem Hqiv.tendsto_latticeAlphaRatio : Filter.Tendsto (fun (n : ℕ) => latticeAlphaRatio n) Filter.atTop (nhds alpha)

α as limit: as more shells are included, the lattice ratio tends to α = 3/5.

def Hqiv.qcdShell : ℕ

Reference horizon = minimal transition shell (derived); calibration (e.g. paper's Python runs). We take the minimal transition shell (N = 1 from exists_transition_shell); no arbitrary step. QCD transition shell: first shell with positive curvature (T ladder).

Equations

• Hqiv.qcdShell = 1

def Hqiv.latticeStepCount : ℕ

Number of discrete lattice steps from QCD to lockin (and after lockin). Set to 3 so that it equals cubeAxes (one step per spatial axis of the 3D null lattice); see latticeStepCount_eq_cubeAxes. So the "3" is not inserted — it is the same 3 as in the lattice (cubeAxes).

Equations

• Hqiv.latticeStepCount = 3

theorem Hqiv.latticeStepCount_eq_three : latticeStepCount = 3

latticeStepCount = 3.

def Hqiv.stepsFromQCDToLockin : ℕ

Steps from QCD to lockin: number of discrete lattice steps from QCD transition to η lockin; equals latticeStepCount (3D lattice).

Equations

• Hqiv.stepsFromQCDToLockin = Hqiv.latticeStepCount

def Hqiv.stepsAfterLockin : ℕ

Steps after lockin: baryogenesis proceeds latticeStepCount discrete steps after T_lockin.

Equations

• Hqiv.stepsAfterLockin = Hqiv.latticeStepCount

def Hqiv.referenceM : ℕ

Reference horizon = lockin shell = qcdShell + stepsFromQCDToLockin. Calibration at lockin; discrete steps through baryogenesis: QCD then lockin then stepsAfterLockin steps. No arbitrary 500.

Equations

• Hqiv.referenceM = Hqiv.qcdShell + Hqiv.stepsFromQCDToLockin

noncomputable def Hqiv.curvatureDensity (x : ℝ) : ℝ

Continuous curvature-imprint density on ℝ⁺, matching shell_shape on integers.

Equations

• Hqiv.curvatureDensity x = 1 / x * (1 + Hqiv.alpha * Real.log x)

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

Purely combinatorial curvature-imprint shape per shell m.

Given by the continuous density at x = m+1 (paper: (1/(m+1)) * (1 + α log(m+1))).

Equations

• Hqiv.shell_shape m = Hqiv.curvatureDensity (↑m + 1)

theorem Hqiv.curvatureDensity_pos {x : ℝ} (hx : 1 ≤ x) : 0 < curvatureDensity x

Positivity of the curvature-imprint density for x ≥ 1.

For all shells in the physical range (where we sample at x = m+1 with m ≥ 0) we have x ≥ 1, hence curvatureDensity x > 0.

theorem Hqiv.curvatureDensity_pos_succ (m : ℕ) : 0 < curvatureDensity (↑m + 1)

Specialisation of curvatureDensity_pos to integer shells x = m+1.

theorem Hqiv.curvatureDensity_ge_one_div_succ (m : ℕ) : 1 / (↑m + 1) ≤ curvatureDensity (↑m + 1)

Lower bound for the density: curvatureDensity (m+1) ≥ 1/(m+1) (the log factor is ≥ 1).

theorem Hqiv.curvatureDensity_le_one_div_succ_mul_log (m n : ℕ) (hmn : m < n) : curvatureDensity (↑m + 1) ≤ 1 / (↑m + 1) * (1 + alpha * Real.log (↑n + 1))

Analytic upper bound (per shell): for m < n, curvatureDensity (m+1) ≤ (1/(m+1))(1 + α log(n+1)). Used to bound the curvature integral above by a multiple of the harmonic sum.

theorem Hqiv.shell_shape_eq_density_succ (m : ℕ) : shell_shape m = curvatureDensity (↑m + 1)

By definition, shell_shape m is the density sampled at m+1.

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

Explicit shape formula from the paper (proved, not defined): (1/(m+1))(1 + α ln(m+1)).

Curvature norm from the cube (formalised)

The combinatorial norm (6^7\sqrt{3}) is built from: (1) expanding a cube in all directions ±x, ±y, ±z → 6 lattice directions; (2) raising each to the octonion dimension 7 → (6^7); (3) the inscribed-sphere factor → (\sqrt{3}) (half-diagonal of the unit cube). We formalise each piece and then the full formula.

def Hqiv.cubeAxes : ℕ

Number of spatial axes for the cube (x, y, z).

Equations

• Hqiv.cubeAxes = 3

def Hqiv.signsPerAxis : ℕ

Two signs per axis (±).

Equations

• Hqiv.signsPerAxis = 2

def Hqiv.cubeDirections : ℕ

Cube directions: expand a cube in all directions (±x, ±y, ±z). Equals axes × signs = 3 × 2 = 6 (the 6 outward normals / lattice directions).

Equations

• Hqiv.cubeDirections = Hqiv.cubeAxes * Hqiv.signsPerAxis

theorem Hqiv.cubeDirections_eq : cubeDirections = 6

theorem Hqiv.latticeStepCount_eq_cubeAxes : latticeStepCount = cubeAxes

latticeStepCount equals cubeAxes (3). So the step counts from QCD to lockin and after lockin are the same as the number of spatial axes in the 3D null lattice.

def Hqiv.octonionImaginaryDim : ℕ

Octonion imaginary dimension: 7 imaginary units (Fano-plane nodes).

Equations

• Hqiv.octonionImaginaryDim = 7

theorem Hqiv.octonionImaginaryDim_eq : octonionImaginaryDim = 7

noncomputable def Hqiv.unitCubeHalfDiagonal : ℝ

Half-diagonal of the unit cube (cube with vertices at (±1,±1,±1)). Distance from center to vertex = √(1²+1²+1²) = √3. This is the "inscribed sphere" factor in the curvature norm (rapidity lattice / equilateral triangle on the hyperboloid). √3 is spatial (a length); the time phase in the metric uses 2π (angle). Different dimensions — no conflict.

Equations

• Hqiv.unitCubeHalfDiagonal = √(1 ^ 2 + 1 ^ 2 + 1 ^ 2)

theorem Hqiv.unitCubeHalfDiagonal_eq_sqrt3 : unitCubeHalfDiagonal = √3

Aside: belt (1D) vs sphere (3D) — "lift by 1 adds 2π"

If you place a belt around the equator (circle of radius R) and lift it so every point is 1 meter higher, the new radius is R+1, so the new length is 2π(R+1). The added length is 2π(R+1) − 2πR = 2π, independent of R. So the increment is constant (2π per meter of lift).

In 3D, if you take a sphere of radius R and "lift" its surface outward by 1 (same idea: new radius R+1), the surface area goes from 4πR² to 4π(R+1)². The added area is 4π((R+1)² − R²) = 8πR + 4π, which depends on R. So the "constant increment" property does not hold for the sphere — it is special to the circle (1D boundary). The curvature norm's √3 is tied to the 3D cube (half-diagonal); the belt's 2π is a 1D phenomenon.

theorem Hqiv.circle_lift_adds_length (R h : ℝ) : 2 * Real.pi * (R + h) - 2 * Real.pi * R = 2 * Real.pi * h

Belt fact (1D): Lifting a circle of radius R outward by h gives new circumference 2π(R+h). The added length is 2πh — independent of R.

theorem Hqiv.sphere_lift_added_area (R : ℝ) : 4 * Real.pi * (R + 1) ^ 2 - 4 * Real.pi * R ^ 2 = 8 * Real.pi * R + 4 * Real.pi

Sphere (2-surface) does not do the same: Lifting a sphere of radius R outward by 1 gives added area 8πR + 4π, which depends on R.

def Hqiv.curvatureNormBase : ℕ

Base of the curvature norm: 6.

Intuition: expand a cube in all directions (±x, ±y, ±z); that gives 6 lattice directions (the 6 “sides” or outward normals of the cube). In the HQIV combinatorics this is also the 6 non-preferred directions in the Fano structure (7 imaginary octonion axes with one preferred for colour). Matter fraction and η require the full SM embedding to SO(8).

Equations

• Hqiv.curvatureNormBase = 6

def Hqiv.curvatureNormExponent : ℕ

Exponent of the curvature norm: 7.

Raise each of the 6 lattice directions to the octonion dimension: 6^7. The 7 is the number of imaginary octonion units (Fano-plane nodes), so the curvature norm factor is “each of the 6 cube directions raised to O^7”.

Equations

• Hqiv.curvatureNormExponent = 7

theorem Hqiv.curvatureNormBase_eq_cubeDirections : curvatureNormBase = cubeDirections

The curvature norm base equals the number of cube directions (6).

theorem Hqiv.curvatureNormExponent_eq_octonionDim : curvatureNormExponent = octonionImaginaryDim

The curvature norm exponent equals the octonion imaginary dimension (7).

theorem Hqiv.curvatureNormBase_pow_exponent : curvatureNormBase ^ curvatureNormExponent = 279936

Arithmetic identity: (6^7 = 279,936) (so the curvature norm factor is an integer).

noncomputable def Hqiv.curvature_norm_combinatorial : ℝ

Combinatorial normalisation (6^7\sqrt{3}), the HQIV invariant.

Intuition: The curvature norm comes from (1) expanding a cube in all directions (±x, ±y, ±z) → 6 lattice directions; (2) raising each to the octonion dimension → (6^7); (3) taking the inscribed sphere → (\sqrt{3}) (the rapidity lattice / equilateral triangle on the local hyperboloid).

Same as CURVATURE_NORM_COMBINATORIAL in the Python code. Multiplies the shell shape to give δE(m); Ω_k is calibrated from it. Matter fraction and η require the full SM embedding to SO(8). The factor √3 here is spatial (unit-cube half-diagonal); the time angle in HQVMetric uses 2π (angular period). So curvature norm = spatial geometry, time phase = angle — different roles.

Equations

• Hqiv.curvature_norm_combinatorial = ↑Hqiv.curvatureNormBase ^ Hqiv.curvatureNormExponent * √3

theorem Hqiv.curvature_norm_combinatorial_eq : curvature_norm_combinatorial = ↑curvatureNormBase ^ curvatureNormExponent * √3

Curvature norm from base and exponent: (6^7\sqrt{3}) in ℝ.

theorem Hqiv.curvature_norm_from_cube : curvature_norm_combinatorial = ↑cubeDirections ^ curvatureNormExponent * unitCubeHalfDiagonal

Curvature norm from the cube (formal): the combinatorial norm equals (cube directions)^(octonion dimension) × (unit-cube half-diagonal), i.e. (6^7 \cdot \sqrt{3}) from expanding the cube in ±x, ±y, ±z, raising to O^7, and the √3 factor.

theorem Hqiv.curvature_norm_from_cube_octonionDim : curvature_norm_combinatorial = ↑cubeDirections ^ octonionImaginaryDim * unitCubeHalfDiagonal

Same formula with octonion dimension explicit: (cube directions)^(octonion dim) × half-diagonal.

Not chosen by convenience: the norm is determined by three structural inputs

The value (6^7\sqrt{3} = 279,936\sqrt{3}) is the only real that can be written as (cube directions)^(octonion dimension) × (unit-cube half-diagonal) given the definitions above. It is not a free parameter tuned to match Ω_k or η.

1. 6 is fixed by the 3D cube: three spatial axes, two signs per axis ⇒ cubeDirections = cubeAxes * signsPerAxis = 3 * 2 = 6. Any other spatial dimension or counting rule would change this (e.g. 4D cube would give 8 directions).

2. 7 is fixed by the octonion algebra: there are exactly 7 imaginary units (Fano-plane nodes). That is a mathematical fact about ℝ with the octonion product; it is not a choice.

3. √3 is fixed by the unit cube: the half-diagonal from center to vertex of the cube with vertices (±1,±1,±1) is √(1²+1²+1²) = √3. So the factor is the Euclidean norm of (1,1,1); no other scale or shape appears.

So the curvature norm is uniquely determined once we assume: (A) curvature counting uses a 3D cubic lattice (6 directions), (B) the algebra is octonionic (7 imaginary dimensions), (C) the geometric factor is the unit-cube half-diagonal (√3). Change any of A, B, or C and the number changes. There is no free numerological constant.

theorem Hqiv.curvature_norm_determined_by_structure : curvature_norm_combinatorial = ↑cubeDirections ^ octonionImaginaryDim * unitCubeHalfDiagonal

Uniqueness of the norm from the three inputs: The combinatorial norm equals the product of (cube directions)^(octonion dim) and the unit-cube half-diagonal. Those three quantities are defined above without reference to Ω_k, η, or any observational constant.

theorem Hqiv.curvature_norm_from_lightcone_axiom : curvature_norm_combinatorial = ↑cubeDirections ^ octonionImaginaryDim * unitCubeHalfDiagonal

Curvature norm from the discrete light-cone axiom.

Starting from the single HQIV light-cone axiom

• new modes at shell m = 8 × stars-and-bars(m) = 4·(m+2)(m+1),

the Lean development fixes:

• the underlying lattice to be the 3D cubic null lattice (three spatial axes with two signs each),
• the number of octonionic imaginary directions to be 7 (Fano-plane nodes),
• and the discrete radial unit in the spatial lattice to be the half-diagonal of the unit cube.

These three structural inputs are exactly cubeDirections, octonionImaginaryDim, and unitCubeHalfDiagonal. The curvature norm is therefore determined by the light-cone axiom together with isotropy and the octonionic lift:

curvature_norm_combinatorial = (cube directions)^(octonion imaginary dim) × (unit-cube half-diagonal) = 6^7 · √3.

No reference to Ω_k, η, or any observational constant appears in the definition or proof.

theorem Hqiv.curvature_norm_combinatorial_exact : curvature_norm_combinatorial = 279936 * √3

Exact value of the combinatorial norm as an integer multiple of √3: [ \text{curvature_norm_combinatorial} = 279,936 \cdot \sqrt{3}. ] Uses (6^7 = 279,936).

theorem Hqiv.curvature_norm_combinatorial_pos : 0 < curvature_norm_combinatorial

Combinatorial norm is positive (base^exponent > 0 and √3 > 0).

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

Per-shell curvature imprint δE(m) = (6^7√3) * shape(m).

Equations

• Hqiv.deltaE m = Hqiv.curvature_norm_combinatorial * Hqiv.shell_shape m

theorem Hqiv.deltaE_eq (m : ℕ) : deltaE m = curvature_norm_combinatorial * curvatureDensity (↑m + 1)

Per-shell δE in terms of density only.

theorem Hqiv.deltaE_exact_norm (m : ℕ) : deltaE m = 279936 * √3 * curvatureDensity (↑m + 1)

δE using the exact combinatorial norm: δE(m) = 279936 · √3 · curvatureDensity(m+1).

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

Absolute value of the curvature-imprint shape: |shape(m)|, no separate helper def.

Equations

• Hqiv.shell_shape_abs m = |Hqiv.shell_shape m|

noncomputable def Hqiv.curvature_integral (n : ℕ) : ℝ

Unnormalised curvature imprint integral over shells 0..n-1.

Equations

• Hqiv.curvature_integral n = List.foldl (fun (acc : ℝ) (m : ℕ) => acc + Hqiv.shell_shape_abs m) 0.0 (List.range n)

theorem Hqiv.curvature_integral_eq_sum_density (n : ℕ) : curvature_integral n = List.foldl (fun (acc : ℝ) (m : ℕ) => acc + |curvatureDensity (↑m + 1)|) 0.0 (List.range n)

Discrete curvature integral as an explicit finite sum over curvatureDensity.

This rewrites the list-fold definition into the more conceptual [ \text{curvature_integral}(n) = \sum_{m=0}^{n-1} \bigl|,\text{curvatureDensity}(m+1),\bigr|. ] It makes transparent that the discrete object we are summing is exactly the continuous density sampled on integer shells.

theorem Hqiv.shell_shape_abs_pos (m : ℕ) : 0 < shell_shape_abs m

Positivity of the absolute shell shape shell_shape_abs m.

theorem Hqiv.curvature_integral_succ (n : ℕ) : curvature_integral (n + 1) = curvature_integral n + shell_shape_abs n

Recurrence relation for the discrete curvature integral: curvature_integral (n+1) = curvature_integral n + shell_shape_abs n.

theorem Hqiv.curvature_integral_ge_harmonic (n : ℕ) : curvature_integral n ≥ ∑ i ∈ Finset.range n, 1 / (↑i + 1)

Curvature integral is bounded below by the harmonic partial sum (used for divergence).

theorem Hqiv.curvature_integral_le_harmonic_mul_log (n : ℕ) : curvature_integral n ≤ (1 + alpha * Real.log (↑n + 1)) * ∑ i ∈ Finset.range n, 1 / (↑i + 1)

Analytic upper bound: curvature integral is at most (1 + α log(n+1)) times the harmonic sum. So the discrete curvature integral is sandwiched: H_n ≤ curvature_integral n ≤ (1+α log(n+1))·H_n, hence it diverges like the harmonic series (Θ(log n)).

theorem Hqiv.curvature_integral_eq_sum (n : ℕ) : curvature_integral n = ∑ i ∈ Finset.range n, curvatureDensity (↑i + 1)

Curvature integral as a Finset sum (for asymptotic analysis).

noncomputable def Hqiv.logWeightedSum (n : ℕ) : ℝ

Log-weighted sum ∑_{i=0}^{n-1} (log(i+1))/(i+1), the second piece of the curvature integral.

Equations

• Hqiv.logWeightedSum n = ∑ i ∈ Finset.range n, Real.log (↑i + 1) / (↑i + 1)

theorem Hqiv.curvature_integral_eq_harmonic_plus_alpha_log (n : ℕ) : curvature_integral n = ∑ i ∈ Finset.range n, 1 / (↑i + 1) + alpha * logWeightedSum n

Curvature integral decomposes as harmonic sum + α × log-weighted sum.

theorem Hqiv.one_sub_inv_le_log (x : ℝ) (hx : 0 < x) (_hx' : x ≠ 1) : 1 - x⁻¹ ≤ Real.log x

For x > 0, x ≠ 1, we have 1 - 1/x ≤ log x (from log(1/x) ≤ 1/x - 1).

theorem Hqiv.harmonic_sum_le_one_add_log_succ (n : ℕ) : ∑ i ∈ Finset.range n, 1 / (↑i + 1) ≤ 1 + Real.log (↑n + 1)

Harmonic sum bound: ∑_{i=0}^{n-1} 1/(i+1) ≤ 1 + log(n+1) for all n. Proof: for k ≥ 2, 1/k ≤ log(k/(k-1)); telescope gives ∑_{k=2}^n 1/k ≤ log n, so H_n ≤ 1 + log n ≤ 1 + log(n+1).

noncomputable def Hqiv.curvature_integral_asymptotic_leading (n : ℕ) : ℝ

Leading term of the asymptotic: (α/2)(log(n+1))² (from ∫₁^{n+1} (1/x)(1+α log x) dx).

Equations

• Hqiv.curvature_integral_asymptotic_leading n = Hqiv.alpha / 2 * Real.log (↑n + 1) ^ 2

theorem Hqiv.curvature_integral_asymptotic_upper (n : ℕ) : curvature_integral n ≤ curvature_integral_asymptotic_leading n + (1 + alpha) * (1 + Real.log (↑n + 1)) ^ 2

Asymptotic: curvature_integral n = (α/2)(log(n+1))² + O(log n). Explicit upper bound: curvature_integral n ≤ (α/2)(log(n+1))² + (1+α)(1+log(n+1))². The sharp O(log n) error follows from ∑ (log k)/k = (1/2)(log(n+1))² + O(log n) via ∫ (log x)/x = (1/2)(log x)².

theorem Hqiv.curvature_integral_mono : Monotone curvature_integral

Curvature integral is monotone in n.

theorem Hqiv.curvature_integral_nonneg (n : ℕ) : 0 ≤ curvature_integral n

Non-negativity of the curvature integral for all n.

theorem Hqiv.curvature_integral_pos {n : ℕ} (hn : 0 < n) : 0 < curvature_integral n

Strict positivity of the curvature integral as soon as we include at least one shell (n > 0).

theorem Hqiv.curvature_integral_ref_pos : 0 < curvature_integral referenceM

Positivity of the curvature integral at the reference (lockin) shell.

theorem Hqiv.exists_transition_shell : ∃ (N : ℕ), 0 < N ∧ 0 < curvature_integral N

Existence of a transition shell: some shell has positive curvature integral, so a discrete-to-continuous “transition” (or reference) exists; we do not fix which shell.

First-principles spatial curvature from the shell integral (dynamic, horizon-dependent Ω_k)

Spatial curvature depends on the horizon. Between any two horizons it is different — curvature between quarks (QCD horizon) and curvature at the CMB last-scattering surface are different even at the same time "now". There is no single "Ω_k at now" without specifying which horizon.

Ω_k is the curvature ratio from the discrete shell integral: at horizon N, the curvature parameter at shell n is curvature_integral n / curvature_integral N (dimensionless). At the horizon itself (n = N) this ratio is 1. Different N (e.g. QCD lockin vs CMB LSS) give different curvature; the formalism is horizon-dependent by construction.

noncomputable def Hqiv.omega_k_at_horizon (n N : ℕ) : ℝ

Curvature ratio at horizon N (first-principles). Ω_k(n; N) = curvature_integral n / curvature_integral N when the horizon integral is positive; else 1 (so at-horizon value remains 1). No external amplitude; purely from the shell integral.

Equations

• Hqiv.omega_k_at_horizon n N = if Hqiv.curvature_integral N ≤ 0 then 1 else Hqiv.curvature_integral n / Hqiv.curvature_integral N

theorem Hqiv.omega_k_at_horizon_eq (n N : ℕ) (hN : 0 < curvature_integral N) : omega_k_at_horizon n N = curvature_integral n / curvature_integral N

Equation for Ω_k at horizon N: when the horizon integral is positive, omega_k_at_horizon n N = curvature_integral n / curvature_integral N.

theorem Hqiv.omega_k_at_horizon_self (N : ℕ) (hN : 0 < curvature_integral N) : omega_k_at_horizon N N = 1

At the horizon itself (n = N), the curvature ratio equals 1 (unit in lattice units).

noncomputable def Hqiv.omega_k_partial (n : ℕ) : ℝ

Ω_k partial at reference horizon: curvature ratio relative to referenceM. omega_k_partial n = omega_k_at_horizon n referenceM.

Equations

• Hqiv.omega_k_partial n = Hqiv.omega_k_at_horizon n Hqiv.referenceM

theorem Hqiv.omega_k_partial_eq_at_horizon (n : ℕ) : omega_k_partial n = omega_k_at_horizon n referenceM

The partial is exactly the curvature ratio at the reference horizon.

theorem Hqiv.omega_k_partial_at_reference (hpos : 0 < curvature_integral referenceM) : omega_k_partial referenceM = 1

At the reference horizon, Ω_k partial = 1 (first-principles; no 0.0098).

theorem Hqiv.omega_k_at_horizon_depends_on_horizon (n N₁ N₂ : ℕ) (hn : 0 < curvature_integral n) (h₁ : 0 < curvature_integral N₁) (h₂ : 0 < curvature_integral N₂) (hne : curvature_integral N₁ ≠ curvature_integral N₂) : omega_k_at_horizon n N₁ ≠ omega_k_at_horizon n N₂

Ω_k depends on the horizon: for a fixed shell n with positive integral, different horizon cutoffs N₁ ≠ N₂ with different integrals give different Ω_k values.

theorem Hqiv.omega_k_partial_abs_bound_of_ratio (hpos_ref : 0 < curvature_integral referenceM) {n : ℕ} {δ : ℝ} (hδ : |curvature_integral n / curvature_integral referenceM - 1| < δ) : |omega_k_partial n - 1| < δ

Auxiliary bound: if the curvature ratio at shell n is within δ of 1, then |omega_k_partial n - 1| < δ.

theorem Hqiv.curvature_integral_tends_to_atTop : Filter.Tendsto curvature_integral Filter.atTop Filter.atTop

Curvature integral tends to infinity as more shells are included; the ratio curvature_integral n / curvature_integral referenceM therefore tends to ∞.

theorem Hqiv.omega_k_partial_tends_to_atTop : Filter.Tendsto (fun (n : ℕ) => omega_k_partial n) Filter.atTop Filter.atTop

Asymptotic behaviour: as more shells are included, omega_k_partial n tends to ∞ (because curvature_integral n → ∞ while the denominator is fixed).

theorem Hqiv.available_modes_zero_numeric : available_modes 0 = 8

Numeric sanity check for available_modes 0 (replaces #eval on ℝ).

#eval on Real does not run a numeric decoder in Lean; the elaborator prints Real.ofCauchy (sorry …) for the Cauchy witness. Use a short proof instead.

theorem Hqiv.new_modes_referenceM_numeric : new_modes referenceM = 40

Numeric sanity check at the reference shell referenceM = 4: new_modes 4 = 40 (same as new_modes_succ 3).