same_symm
plain-language theorem explainer
Symmetry of object-level sameness at a fixed finite trace: if an admissible judgment marks endpoints a and b the same, it marks b and a the same. Cited wherever trace-level equality is flipped or fed into equivalence arguments. Proof is a one-line unpack of the symmetry field required by the TraceJudgment admissibility package (R5).
Claim. Let $J$ be an admissible trace judgment, $T$ a finite trace, and $a,b$ endpoints. If $J$ judges $a$ the same as $b$ at $T$, then $J$ judges $b$ the same as $a$ at $T$.
background
In the Primitive Recognition Calculus, an endpoint is one side of the primitive distinction (left or right). A finite trace is built from the empty trace by successive distinction acts. A TraceJudgment packages the object-level relations SameT and DiffT on endpoints at each trace, together with the R5 admissibility proofs that SameT is an equivalence relation at every trace.
The field same is the object-level equality predicate at a trace. Its symmetry is not proved from first principles here; it is part of what it means for a judgment surface to be admissible. The sibling reflexivity and transitivity extractors play the same role for the other two equivalence laws.
Local setting is the SameDiff module: the thin interface that turns the structure fields into ordinary named lemmas so downstream forcing arguments can cite them without opening the structure.
proof idea
One-line term wrapper. Apply the structure field that asserts SameT is Symmetric at every trace, specialized to the given trace and the given witness. No further rewriting or case analysis.
why it matters
Feeds the core forcing lemma genuine_judgment_same_is_equality in PRCOnePrimitive: on the two-endpoint type, any equivalence that never identifies left with right must be literal equality. That lemma's doc-comment states explicitly that only reflexivity and symmetry of SameT are used, both supplied by TraceJudgment admissibility.
Within the Recognition foundation, this is bookkeeping for R5 (SameT is an equivalence at each trace), which sits under the K2.6–K2.8 judgment-surface package. It does not itself force dimension, phi, or the eight-tick octave; it keeps the equality side of the primitive calculus coherent so later uniqueness and forcing steps can treat SameT as a genuine equivalence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.