ExprReflexive
plain-language theorem explainer
A formal system has a reflexive expression order when every expression extends itself. This is the standing hypothesis for the δ-distinction dichotomy: any such foundation is either degenerate or realizes the δ core. Anyone citing the dichotomy or the “distinction is not optional” headline needs this predicate. The body is a one-line Prop abbreviation over the system’s extends relation.
Claim. For a formal system $F$, the expression order is reflexive when $\forall e \in F.\mathrm{Expr},\; e$ extends $e$. Equivalently, the binary relation $\mathrm{exprExtends}_F$ is reflexive on the carrier of expressions.
background
The Primitive Recognition Calculus (PRC) packages an arbitrary foundation as a minimal FormalSystem: carriers for tokens and expressions, a distinction predicate on tokens, an extension (or derivability) order on expressions, and a map from abstract endpoints into tokens. The order exprExtends is the verifier-side stand-in for “is derivable from,” “⊆,” or any other reflexive “extends” relation a foundation might use.
The surrounding module studies when such a foundation is forced to realize the δ core (a PRC embedding into its own interface). Reflexivity of the expression order is the mild structural hypothesis that makes the dichotomy well-posed: without it, the collapse of traces to a fixed expression in the realizing map would not type-check against the system’s own order.
Upstream, FormalSystem is exactly the interface the inevitability theorem needs; the expression carrier is deliberately abstract (not tied to the certified analytic Expr tree), so the reflexivity predicate applies equally to logic, arithmetic, HF set theory, toposes, and the native PRC system.
proof idea
Definitional: the predicate is the universal quantification ∀ e : F.Expr, F.exprExtends e e. No lemmas are applied; instances later discharge it by reflexivity of ≤ on ℕ, of trace extension, or of whatever concrete order the foundation uses.
why it matters
This predicate is the gate on the δ4 headline results in the same module. distinction_dichotomy states that any foundation with a reflexive expression order is either degenerate or realizes δ. distinction_not_optional strengthens that to the biconditional “realizes δ ↔ discriminating,” plus the exclusion of degeneracy once δ is realized. The realizing construction realizesDelta_of_discriminating explicitly takes reflexivity so it can collapse every trace to one fixed expression that extends itself.
Downstream instance theorems (prcFormalSystem_exprReflexive, ofTwoDistinct_exprReflexive, toposSystem_exprReflexive, hfSystem_exprReflexive, zfSystem_exprReflexive) discharge the hypothesis for the named foundations, feeding named_foundations_not_degenerate. In the Recognition forcing chain this is foundation-side scaffolding for inevitability of distinction, not a physics constant step (T5–T8), but it is what makes “δ is not optional” a theorem rather than a slogan.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.