same_refl
plain-language theorem explainer
Object-level sameness is reflexive at every finite trace: for any admissible trace judgment, any endpoint is the same as itself. Downstream forcing that identifies sameness with equality on the two-endpoint type cites this fact. The proof is a one-line projection of the reflexivity field required by the admissibility structure.
Claim. Let $J$ be an admissible trace judgment surface, $T$ a finite trace, and $a$ an endpoint. Then the object-level sameness predicate of $J$ holds at $(T,a,a)$: $\mathrm{same}_J(T,a,a)$.
background
In the Primitive Recognition Calculus, an endpoint is one side of the primitive distinction (left or right). A finite trace is either empty or obtained by extending a prior trace by one distinction act. Together they form the raw combinatorial substrate on which judgments are stated.
A trace judgment surface packages two object-level predicates at each trace: sameness and witnessed difference. Admissibility (R5) requires that sameness be an equivalence relation at every trace, recorded as three proof fields: reflexivity, symmetry, and transitivity. The present lemma is the extracted reflexivity clause.
The local module builds the Same/Diff layer used later to force that genuine judgments coincide with equality on the two-endpoint type.
proof idea
One-line term wrapper. The structure TraceJudgment already carries a field asserting that for every trace $T$, the binary relation $\mathrm{same}(T,\cdot,\cdot)$ is reflexive. Apply that field at the given trace and endpoint; no further reasoning is required.
why it matters
This is the reflexivity half of the equivalence package that the core forcing lemma genuine_judgment_same_is_equality consumes. That lemma states: on the two-endpoint type, any equivalence that never identifies left with right is exactly equality; only reflexivity and symmetry of sameness are used, both supplied by the admissibility fields of a trace judgment.
In the Recognition foundation chain, this sits inside the Primitive Recognition Calculus layer that turns distinction acts into a judgment surface before the T0–T8 forcing steps. Without extracted reflexivity, the later identification of sameness with equality cannot even be stated as a theorem about admissible surfaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.