Grounded Types as Cross-Layer Invariants: Admissible Updates and Traceable Witnesses in Two-Topos Grounding

Grounding connects what is observed to what is conceptualized, yet many formal designs collapse these regimes into a single layer, making groundedness unstable under update. In the Two-Topos Grounding (TTG) setting, we define grounded types as cross-layer invariant schemas: a concept is grounded relative to evidence when there exists an explicit observation-side witness w: O → g^*(A), optionally restricted to an auditable witness class. We introduce admissible update steps via stepwise compatibility morphisms and show a preservation theorem: admissible updates transport witnesses compositionally and preserve groundedness. A corollary yields traceable witnesses enabling compact per-step audits, and we provide an executable witness in TTGOS v0.2.1. This preprint is part of the Two-Topos Grounding (TTG) series.Software reference: TTGOS v0.2.1.