# RCIG Kernel Calculus v0.1 — Minimal Trusted Judgment Set

This compact specification accompanies Run 123.

## Primitive judgments

```text
Γ ⊢ x : τ
Γ ⊢ c ▷ φ
Γ ⊢ SoundRule(ρ)
Γ ⊢ Δ ⇒ρ Δ'
Γ ⊢ WF(R, ≺)
Γ ⊢ r(Δ') ≺ r(Δ)
Γ ⊢ x ≈T y
Γ ⊢ Compat(⇒, ≈T)
Γ ⊢ LocalConfluentT
Γ ⊢ V : Verdict
```

## Required verdict kinds

```text
Closed
Reopened
Unknown
```

## Minimum certified-mode requirements

A `Closed` verdict must be backed by:
1. well-typed CDIR;
2. replayable certified rewrites or an equivalent direct proof;
3. empty semantic residual debt in declared scope;
4. explicit trust base.

A `Reopened` verdict must be backed by:
1. well-typed witness;
2. certified `Reopens_T(w)` judgment;
3. explicit scope and trust base.

An `Unknown` verdict must:
1. make no unsupported closure/reopening claim;
2. expose residual debt or verification failure.

## Canonicality add-on

To claim semantic canonicality, additionally certify:
1. termination or equivalent well-founded search;
2. closure-sound semantic equivalence;
3. rewrite compatibility;
4. local semantic confluence.

Then Newman's lemma may be invoked on the quotient rewrite system.

## Trust rule

No external assumption is silently converted into a checked theorem.
Every opaque assumption must remain visible in `TrustBase(V)`.