lemma proved term proof

`kOf_step_succ`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 101lemma kOf_step_succ (δ : ℤ) (hδ : δ ≠ 0) (m : Nat) :
 102  kOf δ (fromNat δ (m+1)) = kOf δ (fromNat δ m) + 1 := by

proof body

Term-mode proof.

 103  simp only [kOf, fromNat, toZ_fromZ δ hδ, Int.natCast_add, Int.natCast_one]
 104  rfl
 105
 106/-- Quantization: every element of the δ-subgroup has a unique integer coefficient. -/

depends on (11)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
fromNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
fromNat in IndisputableMonolith.LedgerUnits decl_use
kOf in IndisputableMonolith.LedgerUnits decl_use
toZ_fromZ in IndisputableMonolith.LedgerUnits decl_use
toZ_fromZ in IndisputableMonolith.UnitMapping decl_use