toZ_succ
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not apply when δ = 0.
- Does not extend the map to real or non-integer multipliers.
- Does not address continuous or topological completions.
- Does not prove that the isomorphism is canonical.
Lean usage
simpa [rungOf] using (toZ_succ (δ:=δ) (hδ:=hδ) (n:=n))formal statement (Lean)
65@[simp] lemma toZ_succ (δ : ℤ) (hδ : δ ≠ 0) (n : ℤ) :
66 toZ δ (fromZ δ (n + 1)) = toZ δ (fromZ δ n) + 1 := by
proof body
Term-mode proof.
67 simp [toZ_fromZ δ hδ]
68
69/-- Package rung index as the `toZ` coefficient of a δ‑element. -/