toZ_succ
plain-language theorem explainer
The lemma shows that incrementing the integer index by one increments the extracted coefficient by one for the subgroup generated by nonzero δ in the integers. Ledger modelers and rung-index calculations in Recognition Science cite it for discrete stepping. The proof is a one-line simplification that invokes the identity property of the coefficient map.
Claim. For nonzero integer δ and integer n, if ι_δ embeds k ↦ kδ into the subgroup δℤ and π_δ projects back to the integer coefficient, then π_δ(ι_δ(n+1)) = π_δ(ι_δ(n)) + 1.
background
LedgerUnits works with the subgroup of ℤ generated by a fixed nonzero δ, realizing an order isomorphism to ℤ itself. The maps fromZ and toZ supply the embedding and coefficient projection; the module specializes to δ = 1 for the clean case. Upstream structures supply rung as a natural-number tier index in nuclear densities (ρ_nuc ~ φ^{n_nuclear} × ρ_Planck) and asteroid ore classes, all of which rely on such integer increments.
proof idea
One-line wrapper that applies the toZ_fromZ identity via simp, reducing the successor statement directly to the coefficient map being the identity on the image of fromZ.
why it matters
Feeds rungOf_step, which lifts the same increment to the rungOf function used in tier calculations. It supplies the discrete step property required for the φ-ladder and rung indexing that appear in the Recognition Science forcing chain and in structures such as NucleosynthesisTiers.of. No open scaffolding remains here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.