Make the redundancy check part of the database tests

.claude/skills/structure-proofs/SKILL.md

@@ -3,7 +3,7 @@ name: structure-proofs
 description: Decide the unknown properties (and, for categories, the special objects and special morphisms) of an existing CatDat structure YAML file by proving or disproving them one at a time, then clean up redundant assignments and summarize. Use when asked to fill in, decide, or prove the properties of a structure.
 argument-hint: '[structure file or ID] [optional time limit, e.g. 30m or 2h (default 60m)] (defaults to the current file)'
 disable-model-invocation: true
-allowed-tools: Read, Edit, Write, Grep, Glob, Bash(pnpm db:update), Bash(pnpm db:structure *), Bash(pnpm db:redundancies), Bash(pnpm db:redundancies *), Bash(pnpm cspell), Bash(date *), Bash(grep *), Bash(sqlite3 database/catdat.db *)
+allowed-tools: Read, Edit, Write, Grep, Glob, Bash(pnpm db:update), Bash(pnpm db:structure *), Bash(pnpm cspell), Bash(date *), Bash(grep *), Bash(sqlite3 database/catdat.db *)
 ---
 
 # Structure Proofs
@@ -26,7 +26,7 @@ State the target file, structure type, and time limit at the start.
 1. Read the structure file in full. Understand the definition precisely: what the objects and morphisms are, how composition works, and any parameters (for parametrized structures such as `BG` or `R-Mod`, properties may depend on the parameter).
 2. Read the files of the structures listed under `related`, `dual`, `parent`, and `associated`. Their proofs are templates for style and often for content (a proof for a similar category can frequently be adapted, or a property can be transferred along a functor via a lemma in `content/`).
 3. Skim [database/data/macros.yaml](../../../database/data/macros.yaml) for available KaTeX macros and the file names in `content/` for reusable lemmas (e.g. `missing_cogenerator`, `subcategories`, `relationships-epis-monos`, `thin_extremal_generator`).
-4. Run `pnpm db:update`, so that the database reflects the current YAML (a new structure only exists in the database after this). If it fails, stop and report the error to the user; do not start editing on a broken database.
+4. Run `pnpm db:update`, so that the database reflects the current YAML (a new structure only exists in the database after this). If it fails, stop and report the error to the user; do not start editing on a broken database. A failure caused only by redundancies of the target structure (reported by the last test of `db:test`) is not a broken database: continue, and handle them in the redundancy phase.
 5. Run `pnpm db:structure <ID>` to see all groups and counts. For categories, also check which special objects and special morphisms are known, including deduced ones (from rules, parents, and dual categories):
 
     ```
@@ -71,12 +71,12 @@ Repeat until no unknown properties (and, for categories, no open special morphis
     - satisfied → `satisfied_properties`; unsatisfied → `unsatisfied_properties`;
     - `undecidable_properties` (rare): only with a proof that the answer depends on the parameters of the structure (e.g. "This holds if and only if $G$ is countable.") or that the question is independent of ZFC.
     - Insert the entry at a sensible position: easy and trivial properties first, closely related properties grouped together (see "Order of assignments" in CLAUDE.md), not necessarily at the end. Create the list key if it does not exist yet (e.g. `unsatisfied_properties: []` must become a proper list).
-    - Do not add `check_redundancy: false` when recording an entry, even if the template you adapted has it. The flag is only set in the redundancy phase, for an assignment that the redundancy script actually reports.
+    - Do not add `check_redundancy: false` when recording an entry, even if the template you adapted has it. The flag is only set in the redundancy phase, for an assignment that `db:test` actually reports as redundant.
     - Use `>-` with blank lines between paragraphs for long proofs, single quotes for values containing `:`, existing macros, and the notation conventions from CLAUDE.md (`\varnothing`, `f : X \to Y`, `\coloneqq`, `non-empty`). Very long or reusable arguments may go into a new `content/` page, but prefer proofs inside the YAML file.
-7. **Run `pnpm db:update` after every single proof**, so that new properties are deduced before the next pick. Then continue with step 1; deduction often decides many further properties at once.
+7. **Run `pnpm db:update` after every single proof**, so that new properties are deduced before the next pick. Then continue with step 1; deduction often decides many further properties at once. The last test of `db:test` reports redundant assignments; those of the target structure are handled in the redundancy phase, so continue despite them.
     - If seeding fails, fix the YAML syntax or schema error.
     - If deduction reports a **contradiction**, the new claim conflicts with the existing data. Remove the new entry, re-examine the argument, and re-run `pnpm db:update`. If you remain convinced the new claim is right, leave it out and report the suspected inconsistency (with the conflicting implications or assignments) to the user instead of changing other files.
-    - If `db:test` fails because of this structure, report it; do not edit `expected-data/`.
+    - If `db:test` fails because of this structure (other than redundancies), report it; do not edit `expected-data/`.
 8. Whenever a new (co)limit property is proven, also add the corresponding special object description (see above). Steps 3 to 7 apply in the same way to special morphism classifications.
 
 Edit only the target structure file, plus new `content/` pages if really needed and `.cspell.json` for legitimate new words. Never edit other structures, properties, implications, or `expected-data/`, and never edit the database directly. Do not commit.
@@ -85,12 +85,12 @@ Edit only the target structure file, plus new `content/` pages if really needed
 
 After the loop ends (also when the time limit was reached, since this phase is quick and leaves the file clean):
 
-1. Run `pnpm db:redundancies` and look for lines mentioning this structure (`for <ID>:`). The script reports at most one redundant satisfied and one redundant unsatisfied assignment per structure.
+1. Run `pnpm db:update` and look for redundancy errors mentioning this structure (`for <ID>:`). The test reports at most one redundant satisfied and one redundant unsatisfied assignment per structure.
 2. For a redundant **satisfied** assignment: keep it with `check_redundancy: false` if the proof is illuminating, constructs (co)limits used later, establishes an intermediate result used by later proofs, or avoids an overly complex deduction (see "No redundant assignments" in CLAUDE.md). Otherwise remove it.
 3. For a redundant **unsatisfied** assignment: almost always remove it.
 4. Before removing an entry, grep the file for its `label` and for phrases like "we already know"; if another proof relies on it, either keep the entry (with `check_redundancy: false`) or adjust the dependent proof and its `references`.
-5. Run `pnpm db:update`, then `pnpm db:redundancies` again. Repeat until no redundancy for this structure is reported.
-6. Test every `check_redundancy: false` flag in the file, one at a time: remove the flag, run `pnpm db:update` and `pnpm db:redundancies`. If the script does not report that assignment as redundant, the flag was unnecessary: keep it removed. Only restore the flag if the assignment is reported and should be kept (see step 2).
+5. Run `pnpm db:update` again. Repeat until no redundancy for this structure is reported.
+6. Test every `check_redundancy: false` flag in the file, one at a time: remove the flag and run `pnpm db:update`. If the test does not report that assignment as redundant, the flag was unnecessary: keep it removed. Only restore the flag if the assignment is reported and should be kept (see step 2).
 
 Finally, run `pnpm cspell` and fix spelling issues in the target file (add legitimate mathematical terms to `.cspell.json`).
 

CLAUDE.md

@@ -42,13 +42,12 @@ Database (all scripts run with `tsx` and are type-checked by `pnpm check` via th
 - `pnpm db:setup`: delete `database/catdat.db` and recreate it from the SQL schema files. It also stores a hash of the schema in `database/schema/schema.json`. Required after any schema change; `db:seed` aborts if the schema hash is outdated.
 - `pnpm db:seed`: clear all data and insert the entries parsed from the YAML files (validated with `valibot` schemas in `database/scripts/utils/seed.schemas.ts`).
 - `pnpm db:deduce`: for each structure type, dualize implications and deduce satisfied and unsatisfied properties (for categories also special objects and morphisms). Deduced rows are marked with `is_deduced`, and those inherited from a parent structure additionally with `is_inherited`.
-- `pnpm db:test`: check data quality: properties and their duals are mutual, categories and their duals are mutual, `1`, `id_Set`, and `1_tensor` have no unsatisfied properties (positivity), all properties are decided for the structures listed in `database/scripts/decided-structures/`, the properties of selected structures exactly match their JSON files in `expected-data/`, adjoint functors are recorded on both sides with matching domains and codomains, links in proofs point to existing entries, and all entries of the history file exist.
+- `pnpm db:test`: check data quality: properties and their duals are mutual, categories and their duals are mutual, `1`, `id_Set`, and `1_tensor` have no unsatisfied properties (positivity), all properties are decided for the structures listed in `database/scripts/decided-structures/`, the properties of selected structures exactly match their JSON files in `expected-data/`, adjoint functors are recorded on both sides with matching domains and codomains, links in proofs point to existing entries, all entries of the history file exist, and no property assignment can be deduced from others or inherited from the parent structure (except those marked with `check_redundancy: false`). The redundancy test runs last and lists all redundancies, at most one per structure and kind (satisfied or unsatisfied).
 - `pnpm db:sort`: sort the arrays in the JSON files in `expected-data/` and `decided-structures/` alphabetically and format them with Prettier.
 - `pnpm db:snapshot`: copy the database to `static/databases/catdat-snapshot.db` for the download page.
-- `pnpm db:update`: run `db:sort`, `db:seed`, `db:deduce`, `db:test`, and `db:snapshot` in sequence. **This is the standard command after editing any YAML data.** Use `--watch` to rerun it whenever a file in `database/data/` changes.
+- `pnpm db:update`: run `db:sort`, `db:seed`, `db:deduce`, `db:test`, and `db:snapshot` in sequence. **This is the standard command after editing any YAML data.** It also runs in the test workflow in CI. Use `--watch` to rerun it whenever a file in `database/data/` changes.
 - `pnpm db:text`: fast path for text-only changes to existing structures (names, notations, alternative notations, descriptions, nLab links, comments, keywords, objects and morphisms of categories, proofs of property assignments), properties (descriptions, nLab links, keywords), and implications (proofs). It updates changed fields without rebuilding relations or running deductions. Special objects, special morphisms, and special morphism rules are not covered. Supports `--watch`.
 - After `db:update`, and after `db:text` when it changed something, the script writes a timestamp to `database/.last-update` (gitignored). A Vite plugin in [vite.config.ts](vite.config.ts) watches this file and the Markdown files in `content/`, and reloads the browser when one of them changes while `pnpm dev` is running.
-- `pnpm db:redundancies`: report property assignments that could already be deduced from others. It reports at most one per structure and kind, so rerun it after each removal. Not part of `db:update`.
 - `pnpm db:combinations <id> [<id> ...]`: list the combinations p ∧ ¬q that the given structures (or their duals) witness and that no other structure in the database witnesses. Needs only the IDs, not the type (all IDs must have the same type). Useful to judge whether a structure adds new information.
 - `pnpm db:structure <id> [group]`: print the property IDs of a structure, grouped into `satisfied`, `unsatisfied`, `unknown`, and `undecidable` with counts (a terminal version of the structure detail page). An optional group argument restricts the output to that group, e.g. `pnpm db:structure Ab unsatisfied`. Needs only the ID, not the type.
 - `pnpm db:shell`: open a `sqlite3` shell on the local database.
@@ -81,15 +80,15 @@ Use existing files as templates: [database/data/categories/N.yaml](database/data
 - Use single quotes for values that contain `:`, and escape a literal single quote as `''`.
 - Use `>-` for multiline text; an empty line in it starts a new paragraph when rendered. Do not use `|-`.
 - Optional `keywords` (list of strings) on structures and properties: alternative names a user would search for that do not already occur in the `name` (for properties: the ID), e.g. `posets` for `Pos`, `aleph1-accessible` for `ℵ₁-accessible` (no special characters needed), or `tripleable` for `monadic`. Only terms that identify the structure or property, not related concepts. The search filters on the list pages match them.
-- Set `check_redundancy: false` on a satisfied property assignment that is redundant but deliberately kept (see below).
+- Set `check_redundancy: false` on a property assignment that is redundant but deliberately kept (see below).
 
 ## Contribution guidelines
 
 Full guidelines: [CONTRIBUTING.md](CONTRIBUTING.md). Contributions come in through the suggestion form on the site, GitHub issues, or pull requests from forks. The essentials for data changes:
 
 - **Proofs for every claim**: satisfied and unsatisfied properties, implications, and special morphisms all need a proof or reference. If a proof refers to another proof, make the link explicit with labels and references. Put reusable lemmas and proofs that require lemmas into a `content/` page and link to it; long proofs alone are fine in the YAML files.
 - **Reduce unknowns**: when adding a structure, decide as many of its properties as possible. When adding a property, try to decide it for all existing structures, and include implications connecting it to existing properties. For the structures in `database/scripts/decided-structures/`, deciding every property is mandatory (enforced by `db:test`).
-- **No redundant assignments**: only assign properties that cannot be deduced. Redundant satisfied assignments may be kept when the proof is trivial anyway, insightful, constructs (co)limits used later, avoids an overly complex automatic deduction, or establishes an intermediate result used later. Mark them with `check_redundancy: false`. Removing redundant assignments is not required but recommended, especially for unsatisfied properties.
+- **No redundant assignments**: only assign properties that cannot be deduced or inherited from the parent structure. Redundant satisfied assignments may be kept when the proof is trivial anyway, insightful, constructs (co)limits used later, avoids an overly complex automatic deduction, or establishes an intermediate result used later. Mark them with `check_redundancy: false`. Redundant unsatisfied assignments are almost always removed. All other redundant assignments must be removed, since `db:test` reports them as errors.
 - **Atomic implications**: do not add implications that follow from others, and do not add dual implications, since dualization is automatic. Prefer the "limit" variant over the "colimit" variant. When adding an implication, check whether it simplifies existing ones.
 - **Positive properties only**: never add negated properties (e.g. "large" for "not small"); record them as unsatisfied instead. Every category property must hold for the trivial category, and every functor property must hold for identity functors.
 - **Counterexamples**: every new property needs at least one structure that does not satisfy it. If none exists yet, add one.
@@ -122,7 +121,7 @@ Content:
 - **Classifications and equivalences**: when one direction is immediate, prove only the other one and say so ("For the non-trivial direction, ..."), as in most special-morphism proofs. In content pages, mark the two directions with `($\implies$)` and `($\impliedby$)`, and steps in a cycle of equivalences with `(1) $\implies$ (2)`.
 - **Building on known facts**: a proof may use properties of the same structure that are assigned earlier in the file or deduced from them ("We already know that ..."), as well as its classification of special morphisms ("(see below)"). Results about other structures may be used with a link to them. If a proof depends on the proof of another assignment, give that assignment a `label` of the form `<structure id>_<short description>` (e.g. `grp_no_cogenerator`) and list the label under `references`.
 - **Reuse instead of repetition**: put general lemmas in `content/` pages instead of repeating an argument in several YAML files, and apply them explicitly, e.g. "apply the contrapositive of the dual of Lemma 2 <a href="/content/subcategories">here</a> to the forgetful functor $\Ab \to \Grp$".
-- **Generalize concrete proofs**: once a proof for a specific structure works, check which features of the structure it really uses. If these are general properties (e.g. infinitary extensivity, existence of certain limits), state the result as an implication, or as a lemma in a `content/` page if it cannot be phrased with existing properties. An implication is much more powerful than a single assignment: the deduction system applies it, and its dual, to every structure, which decides further properties and makes existing direct proofs redundant. After adding one, run `pnpm db:redundancies` and remove the redundant assignments (or mark them with `check_redundancy: false` if other proofs cite them). Example: the proof that $\LRS_R$ is not coaccessible only used that $\LRS_R$ is infinitary extensive, which led to the implication `infinitary_extensive_not_coaccessible`. It also decided `Met_c` and made the proofs for `LRS_R`, `Sch_R`, `Top`, and `Quiv_fc` redundant.
+- **Generalize concrete proofs**: once a proof for a specific structure works, check which features of the structure it really uses. If these are general properties (e.g. infinitary extensivity, existence of certain limits), state the result as an implication, or as a lemma in a `content/` page if it cannot be phrased with existing properties. An implication is much more powerful than a single assignment: the deduction system applies it, and its dual, to every structure, which decides further properties and makes existing direct proofs redundant. After adding one, run `pnpm db:update` and remove the redundant assignments (or mark them with `check_redundancy: false` if other proofs cite them). Example: the proof that $\LRS_R$ is not coaccessible only used that $\LRS_R$ is infinitary extensive, which led to the implication `infinitary_extensive_not_coaccessible`. It also decided `Met_c` and made the proofs for `LRS_R`, `Sch_R`, `Top`, and `Quiv_fc` redundant.
 
 Format:
 
@@ -135,5 +134,5 @@ Format:
 
 1. Edit the YAML files in `database/data/` (or the `content/` pages).
 2. Run `pnpm db:update`, or `pnpm db:text` for text-only changes to existing structures, properties, and implications. If the schema changed, run `pnpm db:setup` first.
-3. If `db:update` fails, the cause is usually malformed YAML or a schema validation error, a contradiction found during deduction, or a failing data-quality test.
-4. Optionally run `pnpm db:redundancies`, and run `pnpm cspell`.
+3. If `db:update` fails, the cause is usually malformed YAML or a schema validation error, a contradiction found during deduction, a failing data-quality test, or a redundant assignment.
+4. Run `pnpm cspell`.