def definition def or abbrev

`tickEquivLogicNat`

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

formal statement (Lean)

  75def tickEquivLogicNat : Tick ≃ LogicNat :=

proof body

Definition body.

  76  tickEquivNat.trans LogicNat.equivNat.symm
  77
  78/-! ## Tick is a natural-number object -/
  79
  80/-- Recursor on `Tick`: iterate `f` from `x` exactly `t.index` times. -/

depends on (13)

Lean names referenced from this declaration's body.

iterate in IndisputableMonolith.Compat.FunctionIterate decl_use
equivNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
LogicNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
tickEquivNat in IndisputableMonolith.Foundation.TimeAsOrbit decl_use
Tick in IndisputableMonolith.Foundation.TimeEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
Tick in IndisputableMonolith.Masses.Ribbons decl_use
Tick in IndisputableMonolith.Masses.Ribbons.Tick decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
Tick in IndisputableMonolith.Measurement.RSNative.Core decl_use