abbrev
definition
Tick
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Measurement.RSNative.Core on GitHub at line 200.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
-
ml_nucleosynthesis_eq_phi -
of -
ml_is_phi_power -
close_packed_lower_energy -
tetragonal_implies_orthorhombic -
nonzero_below_curie -
phiRung_neg -
sakharov_necessary -
rs_cone_cmin_value -
mkLabPrediction -
RelativisticFieldEffect -
sync_period_eq_360 -
fundamentalFrequency -
born_rule_jcost_connection -
RealityCertificate -
recognition_loop_has_surjection -
static_ground_state_impossible -
tickEquivLogicNat -
tickEquivNat -
tickEquivNat_apply -
tickEquivNat_succ -
tick_isNNO -
tick_orbit_eq_logicNat -
tick_orbit_eq_logicNat_succ -
tickRecursor -
tickRecursor_succ -
tickSucc -
tickSucc_index -
tickZero -
tickZero_index -
TimeAsOrbitCert -
timeAsOrbitCert_inhabited -
Epoch -
LedgerSnapshot -
Tick -
tick_within_epoch -
five_eight_coprime -
forty_five_factorization -
forcing_chain_complete -
ledger_universal
formal source
197inductive QualiaUnit : Type
198inductive ZUnit : Type
199
200abbrev Tick := Quantity TickUnit
201abbrev Voxel := Quantity VoxelUnit
202abbrev Coh := Quantity CohUnit
203abbrev Act := Quantity ActUnit
204abbrev Cost := Quantity CostUnit
205abbrev Skew := Quantity SkewUnit
206abbrev Meaning := Quantity MeaningUnit
207abbrev Qualia := Quantity QualiaUnit
208abbrev ZCharge := Quantity ZUnit
209
210end RSNative
211end Measurement
212end IndisputableMonolith