path: root/library/status.md

# Active typed library status

This file records the active aggregate boundary and the consequences of the
completed content-addressed cutover. It is not a theorem-authority manifest
and does not duplicate computed IDs or premise lineages. Every production
`Verify` invocation uses the exact typed driver; the lists below record the
accepted library inventory, not a routing selector.

## Typed closures

The protected roots are `set.tex` and `nat.tex`. Their complete dependency
closure within the active `everything.tex` graph is:

```text
set.tex
set/cons.tex
set/regularity.tex
set/suc.tex
nat.tex
```

Phase 5.3 activated these ordinary library roots:

```text
set/symdiff.tex
set/powerset.tex
set/partition.tex
set/bipartition.tex
set/product.tex
set/filter.tex
relation.tex
relation/properties.tex
relation/uniqueness.tex
function.tex
set/cantor.tex
set/fixpoint.tex
set/equinumerosity.tex
order/quasiorder.tex
order/order.tex
relation/equivalence.tex
relation/closure.tex
algebra/magma.tex
algebra/semigroup.tex
algebra/monoid.tex
algebra/quasigroup.tex
algebra/loop.tex
order/semilattice.tex
topology/preclosure.tex
topology/topological-space.tex
topology/basis.tex
topology/disconnection.tex
topology/separation.tex
ordinal.tex
cardinal.tex
everything.tex
```

Each activated root has a wholly typed dependency closure. In particular,
`set/bipartition.tex` imports the typed `set.tex`, `set/cons.tex`, and
`set/powerset.tex` modules; `set/product.tex` imports only typed `set.tex`;
and `set/filter.tex` imports typed `set.tex` and `set/powerset.tex`. No
activated graph has an untyped dependency. The typed `relation.tex` root imports, in
source order, `set.tex`, `set/powerset.tex`, and `set/product.tex`; its
two activated property modules each import typed `set.tex` and `relation.tex`
in source order. The typed `function.tex` root imports, in source order,
`set.tex`, `relation.tex`, and `relation/uniqueness.tex`. The typed Cantor and
fixpoint roots each import `set/powerset.tex` followed by `function.tex`.
The typed equinumerosity root imports `set/powerset.tex`, `set/fixpoint.tex`,
and `function.tex` in source order. The typed quasiorder root imports
`relation.tex` and `relation/properties.tex`; the typed order root imports
those modules followed by `order/quasiorder.tex`. Both import lists retain
source order. The typed equivalence root imports `set.tex`,
`set/partition.tex`, `relation.tex`, and `order/quasiorder.tex`; the typed
relation-closure root imports `relation/properties.tex` followed by
`relation/equivalence.tex`. The typed magma root imports only `function.tex`,
the semigroup root imports only `algebra/magma.tex`, and the monoid root
imports only `algebra/semigroup.tex`. Quasigroup forms the second branch over
`algebra/magma.tex`; loop imports only `algebra/quasigroup.tex`, whose sealed
interface carries its unital-magma parent as a direct structure parent. These
lists also retain source order. The typed meet-semilattice root imports
`order/order.tex` followed by `function.tex`; the latter is the explicit owner
of source-level graph application used by `meet[X](x,y)`. The standalone typed
preclosure root imports `set.tex` followed by `function.tex` for the same
reason. The typed topological-space root imports `set.tex`,
`set/powerset.tex`, and `set/cons.tex` in source order. The typed basis root
imports `topology/topological-space.tex`, `set.tex`, and `set/powerset.tex`;
the disconnection root imports `set.tex`, `set/bipartition.tex`, and
`topology/topological-space.tex`; and the separation root imports
`topology/topological-space.tex` followed by `set.tex`. These lists retain
source order. The typed ordinal root imports `set.tex`, `set/cons.tex`,
`set/powerset.tex`, `set/regularity.tex`, and `set/suc.tex`; the typed
cardinal root imports `set.tex`, `ordinal.tex`, `function.tex`, and `nat.tex`.
The active `everything.tex` aggregate retains its existing 31 direct
imports in source order. Its complete graph is typed, and it is now the sole
`make lib` corpus root. Other ordinary roots still use the same typed
production driver when invoked directly.

## Fixed-foundation and prelude replacement

The protected source assumptions/providers have the following dispositions:

| Former declaration/provider | Disposition |
| --- | --- |
| `setext` | replaced by checked `SetExtensionality` |
| `emptyset` | replaced by checked `EmptyCharacteristic` |
| legacy `\emptyset` semantic provider | replaced by intrinsic `Empty`; lexical spelling retained |
| `cons_iff` and legacy `\cons` provider | rewritten as a transparent pair/family-union definition and derived theorem |
| `unions` signature and legacy provider | replaced by intrinsic `FamilyUnion`; lexical spelling retained |
| `unions_iff` | replaced by checked `FamilyUnionCharacteristic` |
| `pow_iff` and legacy `\pow` provider | replaced by intrinsic `PowerSet` and checked `PowerSetCharacteristic`; lexical spelling retained |
| `union_iff` | rewritten through a transparent binary-union definition |
| `num_naturals_inductive_set` | replaced by the final prelude's checked Omega theorem |
| `num_naturals_smallest_inductive_set` | replaced by the final prelude's checked Omega-minimality theorem |
| legacy `\naturals` semantic provider/reservation | replaced by transparent `naturals = Omega`; lexical spelling retained |
| fixed tuple syntax and `pair` marker | reused by a source-owned opaque ordered-pair signature; this is distinct from intrinsic unordered `PairSet` |
| `pair_eq_iff`, `pair_neq_emptyset`, `pair_neq_fst`, `pair_neq_snd` | deliberately retained source escape hatches |
| `fst`, `snd` signatures and `fst_eq`, `snd_eq` | deliberately retained opaque/source assumptions |
| `num_addition_is_set`, `num_addition_on_naturals`, `num_addition_axiom_1`, `num_addition_axiom_2` | deliberately retained opaque/source assumptions |

The five protected source modules now use these replacements as one typed
closure. The removed assumptions and alternative providers are absent before
the replacement proofs are prepared. Set adjunction and binary union are
transparent definitions over the fixed primitives; their characteristic facts
and the remaining protected facts have clean checked authority. The inductive
set phrase delegates to the final prelude, and `naturals` resolves only to the
prelude's transparent Omega object. Copying a marker or proposition shape never
grants foundation authority.

Set adjunction uses the compiler's canonical insertion body. The source
successor spells that same body and therefore coalesces with the packaged
successor's transparent object. Neither construction depends on the opaque
ordered-pair operation.

Intrinsic unordered pairing is written `\upair{a}{b}` and is governed only by
the clean checked `PairSetCharacteristic` fact. Tuple notation `(a,b)` resolves
to the opaque source-owned ordered-pair object. Its defining and projection
axioms retain source-axiom safety.

The active inventory includes the five protected roots and the twenty-eight
Phase 5.3 ordinary library roots. Every verification invocation acquires the
exact packaged final prelude before parsing and uses its syntax and semantics
as the first implicit inputs. The final prelude supplies
`pow_iff` through the exact clean `PowerSetCharacteristic`;
`set/powerset.tex` declares no local replacement axiom.

The base relation module deliberately has mixed, premise-derived authority.
Facts whose proofs use only clean set and relation facts, including
`union_relations_is_relation`, remain clean. Ordered-pair-dependent facts such
as `id_iff` retain `SourceAxiom` safety from the opaque tuple laws. No local
relation fact is backed by `Omitted`.

The general relation-property and uniqueness modules are also typed. Their
clean definitions and subset-preservation results remain clean. Results that
actually use ordered-pair facts, including identity injectivity, inherit
`SourceAxiom` safety. Neither module introduces a source axiom or contains an
`Omitted`-backed local fact.

Source application `f(x)` is the ordinary source spelling of
`\apply{f}{x}`. Both resolve to the transparent set-theoretic graph operation
declared by `function.tex`; neither lowers directly to checked-core native
function application. The application definition and clean set-theoretic
results retain clean authority. Ordered-pair-dependent results such as
`function_apply_intro` inherit `SourceAxiom` safety. The module introduces no
source axiom and retains exactly its six pre-existing proof-level `Omitted`
authorizations.

The Cantor proof retains its diagonal-set definition and closes the explicit
local contradiction through one indirect Vampire obligation. Its theorem is
clean. The fixpoint module retains its post-fixed-point family; both local
definitions have clean defining-equation authority, while Knaster--Tarski
inherits `SourceAxiom` safety through the existing function and ordered-pair
layer. Neither module introduces a source axiom or an `Omitted` authorization.

Equinumerosity is typed against the final prelude and its three sealed direct
imports. Its local function `h` is a scoped replacement graph and its local set
`h'` is likewise proof-local; neither is published in the module interface or
prefix. The ordinary definition has clean defining-equation authority, while
the elementary bijection results inherit the ordered-pair layer's
`SourceAxiom` safety. Cantor--Schroeder--Bernstein retains its single existing
proof-level `Omitted`; the module introduces no source axiom or additional
escape hatch.

The final prelude owns the metadata-only `onesorted structure` descriptor and
its opaque `carrier : Set -> Set` operation. Ordinary structures publish a
transparent predicate definition and independently checked clean projection
facts. `order/quasiorder.tex` owns the opaque `lt` operation;
`order/order.tex` imports that descriptor and reuses the same operation object
without allocating a replacement. Both modules mint neither `SourceAxiom` nor
`Omitted`; ordinary results inherit any ordered-pair safety solely from their
selected premises.

The equivalence module preserves its transparent quotient and bounded
relation constructions, including source-owned ordered-pair semantics. It
mints no source axiom and retains exactly the five existing direct
`OmittedAuthorization` results at the end of the module. All preceding
declarations check normally. The relation-closure module publishes three
clean transparent defining equations and no direct escape hatch; its
reflexivity theorem truthfully inherits `SourceAxiom` safety through the
selected identity and ordered-pair facts.

The magma module owns the opaque `mul` operation; unital magma adds the opaque
`neutral` operation. The public `cdot` spelling is a contextual transparent
abbreviation: it keeps surface arity two while its expansion receives the
active structure set as a hidden argument and resolves the exact `mul` object.
The structure definitions and projections are clean, and the module introduces
neither a source axiom nor an `Omitted` authorization.

The semigroup hierarchy reuses magma's exact `mul` object. Its associativity
and regularity laws quantify over `carrier[A]`; inverse semigroup adds no
operation and proves its inheritance and idempotent-orbit result with ordinary
clean exact authority. It introduces neither a source axiom nor an `Omitted`
authorization.

Monoid inherits unital magma's exact `mul` and `neutral` objects and restores
the carrier-scoped associativity law. Its implication to semigroup is an
ordinary clean exact proof; the module introduces no operation or escape
hatch.

Quasigroup inherits magma's `mul` and owns the opaque `ldiv` and `rdiv`
operations in that source order. Its six carrier-scoped laws have stable
projection labels, and both cancellation results are clean exact proofs from
the corresponding division laws. It introduces no escape hatch.

Loop has direct structure parents quasigroup and unital magma and owns no
operation. The shared `carrier` and `mul` ancestors coalesce by exact object
identity; the descriptor inherits the exact `ldiv`, `rdiv`, and `neutral`
objects without allocating replacements. Its defining and inheritance facts
are clean, and it introduces no escape hatch.

Meet semilattice has the exact ordered-set parent. Its descriptor reuses the
parent's `carrier` and `lt` objects and owns only the opaque `meet` operation.
Closure, lower-bound, greatest-lower-bound, and idempotence are explicitly
scoped to `carrier[X]`. The structure definition, projections, and theorem
have clean exact authority and introduce no escape hatch.

Preclosure space has the metadata-only onesorted parent. Its descriptor reuses
the final prelude's exact `carrier` object and owns only the opaque `cl`
operation. Its four labeled laws state carrier-bounded closure, empty-set
preservation, extensivity, and binary-union preservation through explicit
`cl[X]` applications. All generated facts are clean and the module introduces
no theorem, source axiom, or `Omitted` authorization.

Topological space also has the metadata-only onesorted parent, reuses the exact
`carrier` object, and owns only the opaque `opens` operation. Its four labeled
laws and structure definition are clean. The unqualified `U is open`
abbreviation remains a contextual transparent target requiring that exact
`opens` object; the explicit `U is open in X` form remains available without
an active structure annotation. All ordinary topology definitions are
transparent. The module has no local source axiom and retains exactly its two
pre-existing direct proof omissions, at `interior_elem_elim` and the nested
case in `intersection_of_closed_is_closed_infinite`. Omitted safety propagates
only through selected dependencies; no local fact inherits `SourceAxiom`.

The three direct topology consumers were activated as sibling maximal roots.
`topology/basis.tex` retains its transparent covering and generated-topology
definitions, and every local fact is clean; explicit local discharges prevent
the imported topology and powerset inventories from contributing incidental
escape safety. `topology/disconnection.tex` retains the opaque source-owned
ordered-pair meaning of `(U,V)`, `fst`, and `snd`. Its reverse theorem and both
definitions are clean, while `disconnection_from_disconnected` truthfully
inherits `SourceAxiom` safety from the selected ordered-pair projection laws.
The module mints no local escape authority.

`topology/separation.tex` retains exactly six direct proof-level omissions and
mints no source axiom. The two direct omissions in the imported
topological-space interface remain distinct imported authority; no current
ordinary separation fact selects them. Compound separation-space phrases keep
the exact topological-space annotation and therefore reuse the inherited
`carrier` and `opens` objects. Four regularity statements now require the
inhabitedness of `carrier[X]`, rather than incorrectly asserting inhabitedness
of the structure parameter itself; these deliberate statement corrections
change the affected proposition and downstream artifact identities. The
direct omission sites remain scoped to their original theorem candidates.

The ordinal development introduces no source axiom or omission. Its existing
public definitions and theorem statements retain their mathematical content;
two checked helper lemmas make the nested membership-connex argument explicit
under the exact one-outermost-induction rule. Narrow premise selection keeps
the resulting ordinal facts clean. `cardinal.tex` required no source rewrite:
its transparent finite, infinite, and cardinality declarations compile
directly against the sealed ordinal, function, set, and naturals interfaces.
The aggregate's final reflexive claim has an ordinary checked proof.

The active aggregate intentionally does not import the typed peripheral
modules `set/equinumerosity.tex` and `topology/preclosure.tex`; they remain
valid typed roots but are not part of the active library inventory. Three
other developments remain outside the active aggregate: `subfinite.tex`
awaits the recorded injection-direction decision, `logic/propositional.tex`
is an experimental standalone
development, and the unused `topology/order-topology.tex` sketch remains
incomplete with duplicate markers and empty laws. If invoked directly, they
still enter the typed driver and receive its ordinary located rejection; no
compatibility provider or fallback exists.

`make lib` now verifies only `library/everything.tex` against one fresh store.
The aggregate covers every module in its active inventory transitively;
production-corpus verification is no longer repeated across overlapping
frontier roots.