Semantic Models for Bilateral Identity-Eliminator-Conserved Paraconsistent HoTT

This is Paper 11 in the 20 Paper PHHT Series This paper constructs semantic models for bilateral identity-eliminator-conserved paraconsistent homotopy type theory. A model consists of an ordinary positive HoTT model 𝒞, an independent negative obstruction overlay 𝔈⁻ on typed evidence tokens, finite retained negative stores at identity, universe-identity, and equivalence gate types, obstruction objects through dimension n, and protected certificate types interpreted by singleton/empty semantics. Positive evidence is exposed only by the selected positive rules and by certified bridge rules. Negative evidence is not interpreted as classical complement; it is interpreted as independent obstruction data. A token may therefore be positive only, negative only, glutty, or undetermined. The central theorem is an exact semantic gate theorem. Ordinary non-glutty identity elimination is exposed precisely when the retained negative store at the relevant identity type is empty. If retained negative identity evidence is present, guarded identity elimination IdElim⁺, cert≤ₙ is exposed precisely when the full retained certificate family FamCert≤ₙ (p, R) = (∏ₐ∈ₑ Cert≤ₙ (p, q) ) × StoreCompat≤ₙ (p, R) is exposed inhabited. The same retained-family discipline governs universe transport and obstruction-gated univalence. Universe transport is exposed only through certified universe-identity stores, and obstruction-gated univalence requires certified retained equivalence data. Strong univalence additionally requires a post-certificate family for the universe path it produces. Aggregate and tower certificates are valid semantic refinements only after comparison to the retained-family gate. The construction gives positively nontrivial paraconsistent models over positively nontrivial bases. It realizes raw gluts without positive explosion and preserves the positive non-glutty fragment under the stated positive-fullness or syntactic-base hypotheses. The paper also gives concrete semantic realizations. Four-layer cellular models instantiate the obstruction package by the primary tower, filtered-shadow data, secondary operations, and polyhedral coherence operations. External cubical obstruction-presheaf models interpret negative evidence as obstruction to filler problems rather than as absence of positive fillers. Cellular–cubical comparison preserves and reflects certification under the displayed typed, zero-preserving, zero-reflecting, and retained-family-compatible hypotheses. This paper supplies the model-theoretic interface for the later higher-categorical semantics and classifying-object constructions. It separates ordinary positive HoTT semantics from exposed positive validity, keeps negative obstruction independent from classical negation, and proves that identity elimination, universe transport, and univalence enter the paraconsistent setting only through explicit retained certificate gates.