abbrev definition def or abbrev

`Tick`

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

formal statement (Lean)

 200abbrev Tick := Quantity TickUnit

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

ml_nucleosynthesis_eq_phi in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
ml_is_phi_power in IndisputableMonolith.Astrophysics.StellarAssembly decl_use
close_packed_lower_energy in IndisputableMonolith.Chemistry.CrystalStructure decl_use
tetragonal_implies_orthorhombic in IndisputableMonolith.Chemistry.CrystalSymmetry decl_use
nonzero_below_curie in IndisputableMonolith.Chemistry.Ferromagnetism decl_use
phiRung_neg in IndisputableMonolith.Constants.RSNativeUnits decl_use
sakharov_necessary in IndisputableMonolith.Cosmology.MatterAntimatter decl_use
rs_cone_cmin_value in IndisputableMonolith.CPM.Examples decl_use
mkLabPrediction in IndisputableMonolith.Flight.GravityBridge decl_use
RelativisticFieldEffect in IndisputableMonolith.Flight.SolidState.VirtualRotor decl_use
sync_period_eq_360 in IndisputableMonolith.Foundation.DimensionForcing decl_use
fundamentalFrequency in IndisputableMonolith.Foundation.EightTick decl_use
born_rule_jcost_connection in IndisputableMonolith.Foundation.QuantumLedger decl_use
RealityCertificate in IndisputableMonolith.Foundation.RealityFromDistinction decl_use
recognition_loop_has_surjection in IndisputableMonolith.Foundation.SimplicialLedger decl_use
static_ground_state_impossible in IndisputableMonolith.Foundation.StillnessGenerative decl_use
tickEquivLogicNat in IndisputableMonolith.Foundation.TimeAsOrbit decl_use
tickEquivNat in IndisputableMonolith.Foundation.TimeAsOrbit decl_use
tickEquivNat_apply in IndisputableMonolith.Foundation.TimeAsOrbit decl_use
tickEquivNat_succ in IndisputableMonolith.Foundation.TimeAsOrbit decl_use
tick_isNNO in IndisputableMonolith.Foundation.TimeAsOrbit decl_use
tick_orbit_eq_logicNat in IndisputableMonolith.Foundation.TimeAsOrbit decl_use
tick_orbit_eq_logicNat_succ in IndisputableMonolith.Foundation.TimeAsOrbit decl_use
tickRecursor in IndisputableMonolith.Foundation.TimeAsOrbit decl_use
tickRecursor_succ in IndisputableMonolith.Foundation.TimeAsOrbit decl_use
tickSucc in IndisputableMonolith.Foundation.TimeAsOrbit decl_use
tickSucc_index in IndisputableMonolith.Foundation.TimeAsOrbit decl_use
tickZero in IndisputableMonolith.Foundation.TimeAsOrbit decl_use
tickZero_index in IndisputableMonolith.Foundation.TimeAsOrbit decl_use

… and 10 more

depends on (5)

Lean names referenced from this declaration's body.

Tick in IndisputableMonolith.Foundation.TimeEmergence decl_use
Tick in IndisputableMonolith.Masses.Ribbons decl_use
Tick in IndisputableMonolith.Masses.Ribbons.Tick decl_use
Quantity in IndisputableMonolith.Measurement.RSNative.Core decl_use
TickUnit in IndisputableMonolith.Measurement.RSNative.Core decl_use