Invariants

This page is generated from the code and must not be edited by hand.

Properties every published Index keeps. The engine checks them when it publishes a run, and a run that breaks one is not published.

Invariant	What must hold	Relations it concerns
INV-1	contains and embeds form forests: no node has two parents, and no cycles.	contains, embeds
INV-2	derives is acyclic. Nothing is its own ancestor.	derives
INV-3	identical is a proper equivalence: symmetric and transitively closed.	identical
INV-4	equivalent is transitively closed within each respect, and implies nothing across respects.	equivalent
INV-5	succeeds series are total: every pair within a series is comparable.	succeeds
INV-6	concerns is never used transitively: every edge rests on direct, weighted support and composes no others.	concerns
INV-7	Substitutivity is confined to identical: no content-derived fact is transferred across any other relation.	identical
INV-8	Every embeds edge carries an expansion state, and no closed-world statement is made over a container that was not fully expanded.	embeds
INV-9	Every asserted edge names a rule and a rule version, and every specialization resolves to an enabled primitive.
INV-10	Adding an extractor never lowers a claim’s tier. Verified by differential run.