Lean
Machine-checked descriptive formalization of the gate.
The role-provenance gate has a companion Lean 4 development that gives its ablation structure a machine-checked descriptive form — the formal counterpart to the empirical RPCG5 layer-ablation chain.
RoleGateReachability.lean
File: LeanMining/SteadyState/RoleGateReachability.lean —
5 theorems, sorry count
0, mathlib base axioms only.
| Theorem |
|---|
logit_full_ablation |
logit_mono |
logit_no_ablation_le_base |
logit_le_base |
ablation_monotonically_reaches_base |
The model: the gated logit of an out-of-role primitive is a base value plus a
finite family of rank-one suppression components. The capstone,
ablation_monotonically_reaches_base, proves that ablating more
components monotonically raises every out-of-role logit, and that full ablation
reaches the un-gated base — for every out-of-role primitive simultaneously. The
empirical RPCG5 greedy-ablation chain (strictly monotone, decreasing to the
un-gated value) instantiates it.
The development is descriptive: it formalizes the gate’s monotone-reachability shape. It makes no minimality or optimality claim — matching the experiments’ v1 scope.
Source: LeanMining/SteadyState/RoleGateReachability.lean,
status/theorem-status.yaml.