occ_zero
plain-language theorem explainer
Zero φ-rungs of cosmic scale carry unit aging-charge occupancy: occ(0) = 1 (full charge, no dilution). Anyone proving the forced rung law occ n = φ^{-n} cites this as the induction base. The proof applies multiplicative composition at (0,0), obtains x = x², and kills the zero root by positivity.
Claim. Under rung factorization (occupancy multiplies across independent φ-rung blocks) and strict positivity of occupancy, the zero-rung occupancy equals one: $\mathrm{occ}(0) = 1$.
background
This module forces the shape of the BIT dark-energy kernel $K(z)$ in $w(z) = -1 + \delta w_0 \cdot K(z)$ from two premises: rung factorization and single-rung balance. Rung factorization says aging-charge attenuation across $m+n$ φ-rungs is the product of the sub-attenuations (the multiplicative shadow of cost additivity). Occupancy $\mathrm{occ},n$ is that attenuation factor after $n$ rungs on the lattice $1+z = \varphi^n$.
The structure $L$ packages the factorization law ($L.\mathrm{composes}$) and the positivity hypothesis ($L.\mathrm{occ_pos}$). Composition at $(0,0)$ is the algebraic seed for the unit base value. Upstream, mul_eq_zero supplies the no-zero-divisors fact used to split the resulting quadratic relation, and the arithmetic add_zero identities clear the $0+0$ index.
proof idea
Apply composition at $(0,0)$: $L.\mathrm{composes},0,0$. Simplify the index with Nat.add_zero to obtain $\mathrm{occ},0 = (\mathrm{occ},0)^2$. Rearrange by linear combination to $\mathrm{occ},0 \cdot (\mathrm{occ},0 - 1) = 0$. Split by mul_eq_zero: the left factor zero contradicts $L.\mathrm{occ_pos},0$ (strict positivity); the right factor zero is $\mathrm{occ},0 = 1$ via sub_eq_zero.
why it matters
Base case of the forced rung dilution law. Downstream, occ_forced inducts on $n$ with this theorem at zero and composition against a single rung at the successor step, yielding $\mathrm{occ},n = \varphi^{-n}$. That law is the lattice form of $K(z) = 1/(1+z)$ and is what pins the scale-free power $s=1$, excludes volume ($s=3$) and spacetime ($s=4$) dilution, and forces the CPL thawing line $w_a = -(1+w_0)$ with $w_0 + w_a = -1$.
In the Recognition chain this sits on the φ-ladder (T6) and the cost-additivity shadow of the Recognition Composition Law: multiplicative occupancy is the dual of additive J-cost across independent rung blocks. The module status is theorem given the two premises; the BIT mechanism and single-channel selection remain hypotheses, and the today-amplitude $\delta w_0$ is open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.