units_identity_prop
plain-language theorem explainer
The units_identity_prop defines the statement that in any RS unit system the product of the speed of light and the fundamental tick duration equals the fundamental length. Researchers verifying dimensional closure in Recognition Science cite this when confirming that every anchor satisfies the same relation. The definition directly encodes the universal quantification over the RSUnits structure.
Claim. For every RS unit anchor $U$, $c_U · τ_{0,U} = ℓ_{0,U}$.
background
The RSUnits structure packages the three base quantities c, tau0 and ell0 together with the field c_ell0_tau0 asserting their product identity. Upstream definitions fix ell0 to 1 in native units and tau0 to the tick duration, while the derivation module recovers tau0 from the combination of hbar, G and c via the relation tau0 = sqrt(hbar G / (pi c^3)) / c. The local setting is the URCAdapters layer that prepares Recognition constants for external use.
proof idea
The declaration is a direct definition of the quantified statement over RS unit anchors. No lemmas or tactics are invoked inside the definition body.
why it matters
This proposition is the target of the lemma units_identity_holds, which discharges it by extracting the field c_ell0_tau0 from any RSUnits instance. It encodes the core unit identity c τ0 = ℓ0 required by the Recognition Composition Law and the forcing chain steps that normalize c = 1 while relating length and time units. The declaration closes the interface between the Constants module and adapter proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.