Layer 0 substrate round 6: contract auto-registration

Wires all 7 contracts into the Reflect.Contract registry via an
initialize block at the foot of Contract.lean.  Without this, the
Tactic surface in Tactic/EqContract.lean was decorative — the registry
was empty at module-load time, so #contract / #whichContract /
find_contract_path / via_eq_contract had no contracts to traverse.

Registered (all at ULevel.zero, the canonical-instance convention):
  · CubicalSetC, CGroupC, CCoxeterC, CSiteC, CModalC — non-parametric
  · CActionC — instantiated at Modality.unitT 0 (trivial-group action)
  · CSheafC — instantiated at (unitT 0, unitT 0) (unit-site / unit-value)

Smoke test (lake env lean --run): Reflect.Contract.allRegistered returns
7 names; lookupByName succeeds for each.

Pure addition: +57 lines, 0 removed.  No new sorries.  Both build
targets clean (lake build 48 jobs, lake build CubicalTransport 42 jobs).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

CubicalTransport/Contract.lean

@@ -58,6 +58,7 @@ import CubicalTransport.Decidable
 import CubicalTransport.Category
 import CubicalTransport.Modality
 import CubicalTransport.Reify
+import CubicalTransport.Reflect
 
 namespace CubicalTransport.Contract
 
@@ -612,4 +613,60 @@ theorem contracts_form_topos (ℓ : ULevel) :
   -- the Hom-restrictions; incl is the canonical inclusion.
   sorry
 
+-- ── §6.  Registry registration (THEORY.md §0.9 hook) ────────────────────────
+-- Each of the 7 named contracts above is registered into the
+-- `Reflect.Contract` registry at module-load time so that the
+-- tactic surface in `CubicalTransport/Tactic/EqContract.lean`
+-- (`#contract`, `#whichContract`, `find_contract_path`,
+-- `via_eq_contract`) can discover them at runtime via
+-- `Reflect.Contract.allRegistered` / `Reflect.Contract.lookupByName`.
+--
+-- ## Registration discipline
+--
+-- · Every entry holds the REAL contract value defined above — no
+--   placeholders, no `unsafeCast`, no shape-coercions.  All seven
+--   contracts in this file are CType→CTerm-shaped (`Contract ℓ`), so
+--   they fit the registry's `ContractEntry.contract : Contract level`
+--   field by definitional equality with the local re-export
+--   `Reflect.Contract`.
+--
+-- · The two contracts taking additional CType parameters
+--   (`CActionC` and `CSheafC`) are universe-polymorphic and
+--   parameter-polymorphic.  We register them at the canonical level
+--   `ULevel.zero` and instantiate the extra carrier parameters with
+--   `Modality.unitT 0` (the unit type at level 0).  This is a real,
+--   substantive instantiation — the resulting contract is the
+--   "trivial-G action" / "unit-site unit-value sheaf" specialisation,
+--   which the registry then keys under the bare contract name.
+--   Downstream tactics consume the registered name only as an
+--   identifier; further-parameterised instantiations are constructed
+--   on demand by the consuming tactic from the same un-applied
+--   definition above (looked up via `Lean.Name`).
+--
+-- · The non-parametric contracts (`CubicalSetC`, `CGroupC`,
+--   `CCoxeterC`, `CSiteC`, `CModalC`) are registered at `ULevel.zero`
+--   for the same canonical-level reason — `Reflect.ContractEntry`
+--   holds a single `level : ULevel` slot, so we pick the canonical
+--   bottom of the universe hierarchy for the registered specimen.
+--   The registered contract is the level-0 instance of the
+--   universe-polymorphic family; consumers re-look-up the symbolic
+--   name and re-instantiate at any level needed.
+initialize do
+  Reflect.Contract.register ``CubicalSetC
+    ⟨ULevel.zero, CubicalSetC ULevel.zero⟩
+  Reflect.Contract.register ``CGroupC
+    ⟨ULevel.zero, CGroupC ULevel.zero⟩
+  Reflect.Contract.register ``CActionC
+    ⟨ULevel.zero, CActionC (ℓ := ULevel.zero) (Modality.unitT ULevel.zero)⟩
+  Reflect.Contract.register ``CCoxeterC
+    ⟨ULevel.zero, CCoxeterC ULevel.zero⟩
+  Reflect.Contract.register ``CSiteC
+    ⟨ULevel.zero, CSiteC ULevel.zero⟩
+  Reflect.Contract.register ``CSheafC
+    ⟨ULevel.zero,
+      CSheafC (ℓ := ULevel.zero)
+        (Modality.unitT ULevel.zero) (Modality.unitT ULevel.zero)⟩
+  Reflect.Contract.register ``CModalC
+    ⟨ULevel.zero, CModalC ULevel.zero⟩
+
 end CubicalTransport.Contract