From 825d8af68daf8c3129aed06e84ba780e063b23df Mon Sep 17 00:00:00 2001 From: Maximus Gorog Date: Tue, 5 May 2026 15:56:03 -0600 Subject: [PATCH] Layer 0 substrate round 6: contract auto-registration MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- CubicalTransport/Contract.lean | 57 ++++++++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) diff --git a/CubicalTransport/Contract.lean b/CubicalTransport/Contract.lean index 867b728..8b55a16 100644 --- a/CubicalTransport/Contract.lean +++ b/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