all_signatures_minimal
plain-language theorem explainer
The theorem asserts that the enumerated list of fourteen virtue effect signatures satisfies the minimality condition of containing no duplicates. Framework auditors verifying the combinatorial structure of the ethical catalogue would cite this result when assembling the full minimality-completeness package. The proof is a direct one-line wrapper that invokes the prior distinctness theorem for the identical list.
Claim. Let $S$ be the list of fourteen effect signatures, each formed by pairing one of the four virtue categories with a natural-number index. Then $S$ is nodup: no element repeats.
background
The module proves structural properties of the virtue signature catalogue: the fourteen signatures are distinct, the full list meets a completeness condition, and removal of any signature breaks that completeness. An effect signature is a pair consisting of a virtue category (Relational, Systemic, Temporal or Facilitative) together with an index in the naturals. The definition allSignatures assembles the concrete list of fourteen such pairs, one per named virtue.
proof idea
The proof is a one-line wrapper that applies the upstream theorem all_signatures_distinct, which itself unfolds the list definition and invokes decidability of List.Nodup to conclude the absence of duplicates.
why it matters
This supplies the minimality conjunct inside the parent theorem virtue_signatures_minimality_complete, which packages minimality, completeness and non-redundancy into a single statement. The result therefore closes one structural requirement of the catalogue without invoking any semantic content of the virtues themselves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.