IndisputableMonolith.Constants.RSUnitsHelpers
RSUnitsHelpers supplies auxiliary lemmas for constants in RS-native units. It would be cited by derivations that convert between c, τ₀ and derived lengths. The module consists of two imports followed by targeted equalities such as the sibling c_mul_tau0_eq_ell0.
claimHelpers for the relation $c · τ₀ = ℓ₀$ together with related RS-unit conversions.
background
The module sits inside the Constants domain and imports IndisputableMonolith.Constants, whose doc-comment states 'The fundamental RS time quantum (RS-native). τ₀ = 1 tick.' It therefore inherits the RS-native convention in which c = 1 and supplies only thin conversion lemmas. No new core objects are introduced beyond these helpers.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module feeds the parent Constants module by supplying the unit-conversion lemmas required for constant derivations inside the Recognition Science framework.