Pith. sign in
module module moderate

IndisputableMonolith.Physics.Vacuum_Speed_Light_RS

show as:
view Lean formalization →

Packages the RS-native vacuum speed of light as the unit convention c = 1, via a nonnegative domain cost with an equality case and a positive canonical threshold. Physicists citing RS units, null cones in tick time, or lightlike recognition bounds would reference it. The module is mostly definitions plus elementary nonnegativity/positivity lemmas assembled into an inhabited SpeedLightCert.

claimIn RS-native units the vacuum speed of light is the convention $c = 1$, witnessed by a nonnegative domain cost that attains a distinguished equality case on the lightlike locus and by a strictly positive canonical threshold, packaged as an inhabited speed-of-light certificate.

background

Recognition Science fixes units so the fundamental time quantum is one tick ($\tau_0 = 1$) and works with the forced spatial dimension $D = 3$. In that system the vacuum speed of light is not a measured free parameter; it is set to unity so that lightlike intervals are pure tick counts. The module lives in the Physics layer and imports Constants (RS time quantum) and Cost (J-cost and related recognition scoring).

Sibling definitions introduce a domain cost (nonnegative, with an equality lemma at a canonical point), a positive canonical threshold, and a SpeedLightCert structure. The certificate bundles those facts into a single witness that vacuum lightlike propagation sits at the cost/threshold boundary used elsewhere in the monolith.

proof idea

Definition-and-certificate module rather than a deep derivation. It defines the domain cost and proves nonnegativity plus an equality-at-locus lemma; defines the canonical threshold and proves positivity; then assembles both into a SpeedLightCert structure with an inhabited instance. The supporting proofs are elementary real inequalities and structure construction on top of Cost and Constants, not a walk through the T0–T8 forcing chain.

why it matters in Recognition Science

Anchors the primer convention that RS-native units take $c = 1$ (alongside $\hbar = \varphi^{-5}$ and $G = \varphi^5/\pi$). Any later physics that treats null cones, light-travel times in ticks, or vacuum causal structure in RS units depends on this certificate existing as a named, checkable object. The current graph snapshot lists no downstream used-by edges, so the module functions as a leaf-facing physics primitive: it freezes the unit choice rather than feeding a named parent theorem in-tree. It does not itself re-derive $c$ from J-uniqueness or the eight-tick octave.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)