[ScriptRaccoon]

This PR adds a check for redundant implications to pnpm db:test, analogous to the existing check for redundant property assignments (cf. #155), and removes or restructures the implications it reported. It resolves #16.

Redundancy check for implications

• New test: pnpm db:test now fails if an implication can be deduced from the other implications. This also covers single conclusions of an implication and single directions of an equivalence. Each redundant implication is listed once, together with a deduction from the other implications.
• New YAML field: implications that are redundant but deliberately kept are marked with check_redundancy: false, as for property assignments. This is intended for implications that state a definition or a standard characterization, and for those whose removal would lead to an overly complex automatic deduction.
• Documentation: CONTRIBUTING.md has a new section "Redundant implications", and CLAUDE.md describes the new test.

Data changes

• Removed implications: the number of non-deduced implications drops from 444 to 428, and the number of conclusions from 565 to 534. Counting each conclusion and each reverse direction of an equivalence as a single statement P₁ + … + Pₙ ⟹ Q, the number drops from 612 to 576.
• Restructured implications: some equivalences are now one-sided implications, some redundant conclusions were removed, and some implications were split or rearranged. For example, "complete ⟺ equalizers + products" is now "equalizers + products ⟹ complete", and the conclusions of "Grothendieck topos" now include the subobject classifier and cartesian closedness, with references to Mac Lane–Moerdijk.
• Kept implications: the other reported implications, which are interesting or necessary, are marked with check_redundancy: false (53 in total), e.g. "cartesian closed + strict terminal object ⟹ thin".
• Alternative proof: the implication "binary products + pullbacks ⟹ equalizers" now also has the proof that the system found, via coreflexive equalizers.
• Proofs: some proofs are clearer now.

Removed implications

The following (in some cases, non-trivial) implications are among those that have been removed. It is remarkable that the system deduces them from the other implications in a non-circular way:

• additive + regular subobject classifier ⟹ trivial
• elementary topos ⟹ epi-regular
• elementary topos + locally essentially small ⟹ well-copowered
• Grothendieck topos ⟹ infinitary extensive
• locally finitely presentable ⟹ locally ℵ₁-presentable
• locally ℵ₁-presentable ⟹ locally presentable
• groupoid + essentially small ⟹ generalized variety
• coequalizers + finitely complete + locally cartesian closed ⟹ regular
• terminal object + wide pullbacks ⟹ complete

Search page

If the search requirements are inconsistent, each step in the proof of the contradiction now links to its implication. The search and the new redundancy check use the same deduction code.