lin-0039

1.8 An admission rule is not an equational rule

The six schemas preserve structural judgments under explicit hypotheses. Admission has a different logical form. Let

\[ \operatorname {Prop}(D,e) \]

denote the evidence used to propose \(e\), and let \(\operatorname {Val}(D,e;\mathcal V)\) denote validation on evidence \(\mathcal V\) excluded from proposal. Write \(\mathcal V\perp \operatorname {Prop}(D,e)\) for the registered provenance condition expressing that exclusion. An admission rule may have the form

\[ \frac{ \Gamma ;\mathbb S\vdash e:D\Rightarrow D'[\mathcal I\mid \mathcal E] \qquad \mathcal V\perp \operatorname {Prop}(D,e) \qquad \operatorname {Val}(D,e;\mathcal V)\models \mathcal E }{ \Gamma ,\mathcal V;\mathbb S \vdash \operatorname {Admit}(D') }. \]

This is not an equality transformation. It is a decision rule with provenance, independence, and threshold conditions. Keeping it outside the equational calculus prevents a system from confusing a well-formed edit with a successful one.