all_virtues_independent
plain-language theorem explainer
The declaration shows that removing any one of the 14 virtue effect signatures from their complete list leaves the removed signature absent from the remainder. Researchers formalizing ethical structures in Recognition Science cite this to verify the catalogue's minimality and lack of internal repetition. The proof relies on the list's distinctness property together with case analysis on index positions to contradict membership via injective indexing.
Claim. For every index $i$ in the finite set of 14 positions, the effect signature at position $i$ in the enumerated list of fourteen signatures does not belong to the list obtained by erasing the element at $i$.
background
The module records combinatorial properties of a fixed catalogue of fourteen effect signatures. Each EffectSignature is a pair consisting of a VirtueCategory (Relational, Systemic, Temporal, or Facilitative) and a natural-number index within that category. The list allSignatures enumerates them explicitly as three relational, three systemic, three temporal, and five facilitative entries. SignatureIndependent(sig, sigs) asserts that sig does not occur as an element of sigs. The upstream theorem all_signatures_distinct states that this list satisfies Nodup.
proof idea
The proof unfolds SignatureIndependent to a negated membership statement. It obtains the nodup fact from all_signatures_distinct and the length equality. After introducing the membership hypothesis, it rewrites via mem_iff_getElem, extracts the index j in the erased list, and performs case distinction on whether j lies before or after the removal position i. Each case maps back to a distinct original index k, then invokes nodup_iff_injective_getElem to obtain an injection on getElem; equality of values at distinct indices produces an immediate contradiction on the indices.
why it matters
This theorem completes the independence section by confirming each signature is absent after its own removal, thereby establishing that the fourteen-element catalogue is minimal and repetition-free. It supplies the terminal structural lemma for the virtue signatures inside the Recognition Science monolith, mirroring basis-independence arguments that appear in the number-theoretic and foundational layers. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.