abbrev definition def or abbrev

`Charge`

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

formal statement (Lean)

  61abbrev Charge := ℝ

proof body

Definition body.

  62
  63/-! ## Canonical RS-native base units -/
  64
  65/-- One tick: the fundamental time quantum. -/

used by (24)

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

constCharge in IndisputableMonolith.Foundation.TopologicalConservation decl_use
linking_iff_D3 in IndisputableMonolith.Foundation.TopologicalConservation decl_use
noether_not_necessarily_quantized in IndisputableMonolith.Foundation.TopologicalConservation decl_use
topological_charge_trajectory_conserved in IndisputableMonolith.Foundation.TopologicalConservation decl_use
loops_eq_face_pairs_D3 in IndisputableMonolith.Foundation.WindingCharges decl_use
winding_charges_certificate in IndisputableMonolith.Foundation.WindingCharges decl_use
winding_gives_three_charges in IndisputableMonolith.Foundation.WindingCharges decl_use
sectorOf in IndisputableMonolith.Masses.RungConstructor.Basic decl_use
ordering_B_equal_ends in IndisputableMonolith.Masses.SDGTForcing decl_use
zpow_phase_charge in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
two_fifth_in_jain_sequence in IndisputableMonolith.Physics.QuantumHallEffect decl_use
applyC in IndisputableMonolith.QFT.CPTInvariance decl_use
cpt_lifetime_equality in IndisputableMonolith.QFT.CPTInvariance decl_use
Ledger in IndisputableMonolith.QFT.CPTInvariance decl_use
LedgerEntry in IndisputableMonolith.QFT.CPTInvariance decl_use
harmonic_energy_conserved in IndisputableMonolith.QFT.NoetherTheorem decl_use
space_invariance_implies_conservation in IndisputableMonolith.QFT.NoetherTheorem decl_use
preferredBasisExamples in IndisputableMonolith.Quantum.PointerStates decl_use
ConservationLaw in IndisputableMonolith.RRF.Foundation.Ledger decl_use
MPForcesLedger in IndisputableMonolith.RRF.Foundation.MetaPrinciple decl_use
deepConnections in IndisputableMonolith.StandardModel.WeinbergAngle decl_use
runningAngle in IndisputableMonolith.StandardModel.WeinbergAngle decl_use
charge_zero_cost_scalar_t1_bounded in IndisputableMonolith.Unification.UnifiedRH decl_use
EBBA_iff_rh in IndisputableMonolith.Unification.UnifiedRH decl_use

depends on (2)

Lean names referenced from this declaration's body.

tick in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use