toposSystem_exprReflexive
plain-language theorem explainer
The topos formal system (tokens = global points of Ω, expressions = derivation lengths in ℕ) has a reflexive expression order: every length extends itself under ordinary ≤. Cited when checking that the category-theoretic parse meets the Distinction Dichotomy interface axioms. Proof is a one-line term applying reflexivity of natural-number order.
Claim. The expression-extension order of the topos formal system is reflexive: for every expression $e$ (a natural number, read as derivation length), $e$ extends $e$, i.e. $e \le e$.
background
The Distinction Dichotomy packages a logical foundation as a FormalSystem: a type of tokens, a type of expressions, a discrimination relation on tokens, an expression-extension preorder, and endpoint tokens. ExprReflexive is the interface axiom that every expression extends itself. Its doc states it is "true of any is-derivable-from / ⊆ / extends relation."
Here the concrete system is the category-theoretic parse toposSystem. Tokens are global points of the subobject classifier Ω (truth values); discrimination is inequality of those points; endpoints are ⊤ and ⊥; expressions are natural numbers, with extension given by ordinary ≤ on derivation length.
The needed arithmetic fact is reflexivity of ≤ on ℕ (and the parallel le_refl facts in the logic-native and signed-orbit orders upstream).
proof idea
Term-mode one-liner. Unfolding ExprReflexive toposSystem yields ∀ n : ℕ, n ≤ n because exprExtends on this system is · ≤ ·. Supply fun n => Nat.le_refl n. No case split, induction, or interface lemmas beyond the definition of the system.
why it matters
Closes one interface obligation for the topos parse of PRC: the expression order really is a reflexive extends-relation. Sibling obligations in the same module cover expressiveness, δ-embedding, and non-degeneracy (toposSystem_expressive, toposSystem_embeds_delta, toposSystem_not_degenerate), culminating in category_theory_realizes_delta.
In the broader Recognition stack this sits in Foundation, under Primitive Recognition Calculus: it shows a standard categorical substrate (Ω, ⊤, ⊥) can be read as a FormalSystem meeting the dichotomy axioms, before any appeal to J-cost uniqueness (T5), φ (T6), the eight-tick octave (T7), or D = 3 (T8). No downstream dependents are recorded yet; the lemma is local glue for the parse.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.