The Bilateral Identity Core of Identity-Eliminator-Conserved Paraconsistent HoTT

This is Paper 9 in the 20 Paper PHHT Series This paper defines the bilateral identity core of identity-eliminator-conserved paraconsistent homotopy type theory. The calculus replaces ordinary single-signed judgmental typing with primitive signed judgments Γ ⊢⁺ a: A, Γ ⊢⁻ a: A, so a displayed assertion may carry positive evidence, negative obstruction evidence, both, or neither. Negative identity evidence belongs to the obstruction layer rather than the positive path layer. Positive identity elimination is governed by a guarded admissibility predicate Adm≤ₙ (p), where p: IdA (a, b) is a positive identity witness. The predicate has exactly two introduction sources. The non-glutty constructor admₙg (p) is available when p has no paired negative identity evidence in the current context. The certified-glut constructor admcert (p, q, c) is available when q is paired negative identity evidence for the same identity assertion and c: Cert≤ₙ (p, q) is a protected certificate. The certificate type Cert≤ₙ (p, q) is the retained nullity record of the selected four-layer obstruction package 𝒪≤ₙ (p, q) = (Ω≤ₙ (p, q), F≤ₙ (p, q), S≤ₙ (p, q), P≤ₙ (p, q) ), where Ω≤ₙ is the primary obstruction tower, F≤ₙ is the retained filtered-shadow package, S≤ₙ is the selected secondary primitive-compatibility package, and P≤ₙ is the selected polyhedral higher-coherence package. A protected certificate is therefore a positive finite retained record witnessing Null (𝒪≤ₙ (p, q) ;0). The main theorem is a canonical-forms theorem for guarded identity elimination. Every positive identity-elimination step along p factors through exactly one of the two admissibility heads: admₙg (p), admcert (p, q, c). No other positive identity-elimination head exists in the closed guarded identity signature. Consequently, signed identity gluts are non-explosive. Raw uncertified gluts do not support positive transport. Certified gluts support precisely the guarded transport licensed by their obstruction-nullity records. The positive non-glutty fragment remains conservative over the ordinary intensional identity fragment. This paper begins the bilateral HoTT part of the series. It imports the obstruction hierarchy of Papers I–VIII as protected certificate content and fixes the positive/negative judgmental core, admissibility predicate, certificate gate, family-certificate interface, and preserving/reflecting/complete comparison terminology used by the later semantic, normalization, completion, and synthesis layers.