abbrev
definition
Charge
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.RSNativeUnits on GitHub at line 61.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
-
constCharge -
linking_iff_D3 -
noether_not_necessarily_quantized -
topological_charge_trajectory_conserved -
loops_eq_face_pairs_D3 -
winding_charges_certificate -
winding_gives_three_charges -
sectorOf -
ordering_B_equal_ends -
zpow_phase_charge -
two_fifth_in_jain_sequence -
applyC -
cpt_lifetime_equality -
Ledger -
LedgerEntry -
harmonic_energy_conserved -
space_invariance_implies_conservation -
preferredBasisExamples -
ConservationLaw -
MPForcesLedger -
deepConnections -
runningAngle -
charge_zero_cost_scalar_t1_bounded -
EBBA_iff_rh
formal source
58abbrev Mass := ℝ
59abbrev Frequency := ℝ
60abbrev Momentum := ℝ
61abbrev Charge := ℝ
62
63/-! ## Canonical RS-native base units -/
64
65/-- One tick: the fundamental time quantum. -/
66@[simp] def tick : Time := Constants.tick
67
68/-- One voxel: the fundamental length quantum. -/
69@[simp] def voxel : Length := 1
70
71/-! ## Derived speed of light in RS-native units -/
72
73/-- Speed of light: c = ℓ₀/τ₀ = 1 voxel/tick. -/
74@[simp] def c : Velocity := 1
75
76/-! ## Canonical `RSUnits` pack for bridge/cert code -/
77
78/-- RS-native gauge: τ₀ = 1 tick, ℓ₀ = 1 voxel, c = 1. -/
79@[simp] noncomputable def U : RSUnits :=
80{ tau0 := tick
81, ell0 := voxel
82, c := c
83, c_ell0_tau0 := by simp [tick, voxel, c] }
84
85@[simp] lemma U_tau0 : U.tau0 = 1 := rfl
86@[simp] lemma U_ell0 : U.ell0 = 1 := rfl
87@[simp] lemma U_c : U.c = 1 := rfl
88
89/-! ## Coherence and action quanta
90
91`Constants.E_coh = φ⁻⁵` is a **dimensionless** RS-derived number.