diff --git a/formal/SilverSight/PIST/UnifiedCovariant.lean b/formal/SilverSight/PIST/UnifiedCovariant.lean
index 3d61caad..4d32df65 100644
--- a/formal/SilverSight/PIST/UnifiedCovariant.lean
+++ b/formal/SilverSight/PIST/UnifiedCovariant.lean
@@ -65,7 +65,6 @@
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Nat.Fib.Basic
 import Mathlib.Data.Matrix.Basic
-import Mathlib.LinearAlgebra.Matrix.Adjoints
 import Mathlib.Tactic
 
 import SilverSight.PIST.CartanConnection
@@ -319,35 +318,29 @@ theorem cp_FS_Kaehler (n : ℕ) : is_Kaehler (Fin (n+1) → ℂ) := by
     A Cartan connection is a principal bundle connection infinitesimally
     modeled on a homogeneous space G/P.
 
-    HONESTY CLASS: OPAQUE (predicate signature — NOT True, NOT axiom)
-    BLOCKED ON: Mathlib Cartan geometry API
-    This is a named Prop with mathematical content (existence of a
-    connection with specific structure group properties). It is
-    deliberately NOT `True` — that would make the companion conjecture
-    vacuously proven via `trivial`, the exact smuggle pattern the
-    anti-smuggle scanner catches. The companion theorem carries a
-    CONJECTURE sorry. -/
-def admits_Cartan_connection (M : Type) : Prop :=
-  -- When Cartan geometry API lands, replace with:
-  --   ∃ (G H : Type) [LieGroup G] [ClosedSubgroup H G],
-  --     Nonempty (CartanConnection M G H)
-  -- For now: an opaque Prop that is neither True nor provable.
-  -- It references a hypothetical structure, making it impossible to
-  -- close with `trivial` or `rfl`.
-  Nonempty (M → M)  -- placeholder: real content needs Cartan API
+    HONESTY CLASS: OPAQUE (axiom predicate signature — asserts nothing).
+    BLOCKED ON: Mathlib Cartan geometry API.
+    Declared as an opaque `axiom` predicate, NOT a `def`. Every concrete
+    `def` body writable today (e.g. `Nonempty (M → M)`) is *trivially
+    inhabited* — closable by `⟨id⟩` — which would let the companion
+    conjecture be discharged vacuously, a silent smuggle the scanner
+    cannot see (it is not literally `:= True`). An opaque axiom symbol
+    carries no content, so the ONLY proof of the companion conjecture is
+    its CONJECTURE `sorry`. When Mathlib ships Cartan geometry, replace
+    with `∃ (G H : Type) [LieGroup G] [ClosedSubgroup H G],
+    Nonempty (CartanConnection M G H)`. -/
+axiom admits_Cartan_connection (M : Type) : Prop
 
 /-- OPAQUE: M has holonomy contained in SO⁰(1,6).
     The pseudo-orthogonal group SO⁰(1,6) preserves a quadratic form of
     signature (1,6).
 
-    HONESTY CLASS: OPAQUE (predicate signature — NOT True, NOT axiom)
-    BLOCKED ON: Mathlib holonomy + indefinite orthogonal group API
-    Same treatment as admits_Cartan_connection. NOT True. -/
-def has_SO_1_6_holonomy (M : Type) : Prop :=
-  -- When holonomy API lands, replace with:
-  --   HolonomyGroup M ⊆ SO(1,6)
-  -- For now: an opaque Prop referencing M's structure.
-  Nonempty (M → M)  -- placeholder: real content needs holonomy API
+    HONESTY CLASS: OPAQUE (axiom predicate signature — asserts nothing).
+    BLOCKED ON: Mathlib holonomy + indefinite orthogonal group API.
+    Same treatment as `admits_Cartan_connection`: an opaque axiom, not a
+    secretly-inhabited `def`. Replace with `HolonomyGroup M ⊆ SO(1,6)`
+    when the API lands. -/
+axiom has_SO_1_6_holonomy (M : Type) : Prop
 
 -- ============================================================
 -- §6  THE GEOMETRIC CONJECTURES (honestly labeled)
@@ -398,9 +391,15 @@ theorem holonomy_is_SO_1_6 : has_SO_1_6_holonomy openSimplex7 := by
 -- ============================================================
 -- §7  AXIOM INVENTORY (anti-smuggle witness)
 -- ============================================================
--- After the Tier 1 conversion, the custom axiom set should be EMPTY.
--- All former axioms are now either:
---   - def (is_Kaehler, admits_Cartan_connection, has_SO_1_6_holonomy)
+-- Custom axiom set after the Tier-1 conversion:
+--   - is_Kaehler                → def (Nonempty (KählerManifold V), real content)
+--   - admits_Cartan_connection  → OPAQUE axiom (predicate signature, asserts nothing)
+--   - has_SO_1_6_holonomy       → OPAQUE axiom (predicate signature, asserts nothing)
+-- The two opaque axioms are honest: a predicate SYMBOL with no body asserts
+-- nothing, so the companion conjectures can only be closed by their sorry.
+-- (Earlier these were `def … := Nonempty (M → M)`, which is trivially
+--  inhabited by `id` — a stealth-`True`; reverted to opaque axioms.)
+-- Proven / conjectured statements:
 --   - theorem with sorry (cp_FS_Kaehler, Cartan_connection_on_J1_exists,
 --     holonomy_is_SO_1_6)
 --
@@ -410,7 +409,8 @@ theorem holonomy_is_SO_1_6 : has_SO_1_6_holonomy openSimplex7 := by
 --   - holonomy_is_SO_1_6 (CONJECTURE: 1+6 observer split)
 --
 -- Whitelist of acceptable axioms after lake build:
---   propext, Classical.choice, Quot.sound, sorryAx
+--   propext, Classical.choice, Quot.sound, sorryAx,
+--   admits_Cartan_connection, has_SO_1_6_holonomy  (OPAQUE predicate signatures)
 -- Any axiom outside this whitelist is a smuggle.
 -- #print axioms  -- uncomment after lake build to verify