# 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.