lemma proved term proof

`rungOf_step`

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

formal statement (Lean)

  76lemma rungOf_step (δ : ℤ) (hδ : δ ≠ 0) (n : ℤ) :
  77  rungOf δ (fromZ δ (n + 1)) = rungOf δ (fromZ δ n) + 1 := by

proof body

Term-mode proof.

  78  simpa [rungOf] using (toZ_succ (δ:=δ) (hδ:=hδ) (n:=n))
  79
  80/-- For any nonzero δ, the subgroup of ℤ generated by δ is (non‑canonically) equivalent to ℤ via n·δ ↦ n. -/

depends on (15)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
via in IndisputableMonolith.Derivations.MassToLight decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
fromZ in IndisputableMonolith.LedgerUnits decl_use
rungOf in IndisputableMonolith.LedgerUnits decl_use
toZ_succ in IndisputableMonolith.LedgerUnits decl_use
rungOf in IndisputableMonolith.Masses.KernelTypes decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
fromZ in IndisputableMonolith.UnitMapping decl_use