diff options
Diffstat (limited to 'library/status.md')
| -rw-r--r-- | library/status.md | 211 |
1 files changed, 188 insertions, 23 deletions
diff --git a/library/status.md b/library/status.md index f5da116..bbb67bd 100644 --- a/library/status.md +++ b/library/status.md @@ -1,8 +1,10 @@ -# Active library migration status +# Active typed library status -This file records the dependency boundary and cutover consequences for the -content-addressed migration. It is not a theorem-authority manifest and does -not duplicate computed IDs or premise lineages. +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 @@ -17,7 +19,7 @@ set/suc.tex nat.tex ``` -Phase 5.3 additionally selects these ordinary library roots: +Phase 5.3 activated these ordinary library roots: ```text set/symdiff.tex @@ -32,19 +34,66 @@ 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 selected root has a wholly typed dependency closure. In particular, +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 -selected graph has a legacy edge. The typed `relation.tex` root imports, in +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 selected property modules each import typed `set.tex` and `relation.tex` +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`. Later relation, -order, and function dependents remain unselected. The typed Cantor and +`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 @@ -87,12 +136,12 @@ 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 production typed-root selection includes the five protected roots and the -twelve Phase 5.3 ordinary library roots. Each selected invocation installs the +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 now supplies `pow_iff` through -the exact clean `PowerSetCharacteristic`; `set/powerset.tex` declares no local -replacement axiom. +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 @@ -122,12 +171,128 @@ 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. -`relation/equivalence.tex`, `relation/closure.tex`, all order modules, and -remaining importers of `function.tex`, including `set/equinumerosity.tex`, -remain outside the typed selection. An invocation rooted at one of these -modules therefore remains wholly legacy until its complete graph is migrated. +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 active `library/everything.tex` root remains unselected on the transitional -legacy route and currently does not verify. Its first failure is the removed -`setext` provider referenced by `set.tex`. It must not receive a compatibility -provider or a mixed typed/legacy graph. +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. |