Kin
plain-language theorem explainer
Kin equips a RecognitionStructure M with a Kinematics instance on M.U by setting the step relation to M.R. Ledger uniqueness proofs and potential difference lemmas cite it to apply Causality reachability predicates such as ReachN and inBall to recognition data. The definition is a direct record instantiation with no proof obligations.
Claim. Let $M$ be a recognition structure with universe $M.U$ and recognition relation $M.R$. Define $Kin(M)$ to be the kinematics structure on $M.U$ whose step relation is exactly $M.R$.
background
Kinematics is the structure whose single field is a binary relation step : α → α → Prop. RecognitionStructure supplies a carrier type U together with a relation R : U → U → Prop. The Potential module develops dependency-light T4 uniqueness lemmas on discrete reach sets; these lemmas require the recognition relation to be presented as a Kinematics instance so that general Causality reachability predicates apply directly.
proof idea
The definition is a one-line wrapper that constructs the Kinematics record by setting step := M.R.
why it matters
Kin supplies the interface that lets reachability lemmas from Causality operate on RecognitionStructure instances. It is invoked by LedgerUniqueness results unique_on_reachN and unique_up_to_const_on_component, as well as by the difference-constancy lemmas diff_const_on_component, diff_const_on_ReachN and diff_in_deltaSub inside Potential. This packaging supports the T4 uniqueness chain on discrete components without extra axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.