frameworkCount
plain-language theorem explainer
The theorem establishes that exactly five canonical ethical frameworks exist in the Recognition Science model. Philosophers or ethicists citing the J-cost symmetry would reference this enumeration when grounding the structural options for ethical action. The proof is a one-line decision procedure that computes the cardinality of the inductive type EthicalFramework directly from its Fintype instance.
Claim. The finite set of ethical frameworks, consisting of consequentialism, deontology, virtue, care, and contractarianism, has cardinality five: $|$EthicalFramework$| = 5$.
background
The EthicsFromJCost module formalizes the Recognition Science ethical framework: an action is ethical precisely when it does not increase the recognition cost J on the agent's ledger and does not impose asymmetric sigma-cost on others. The golden rule is identified with the symmetry property J(r) = J(1/r) for any recognition ratio r > 0. Five canonical frameworks are introduced via the inductive type EthicalFramework whose constructors are consequentialism, deontology, virtue, care, and contractarianism; this enumeration is stated to equal the configuration dimension D = 5.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate Fintype.card on the EthicalFramework type, whose Fintype instance is derived automatically from the inductive definition and its DecidableEq, Repr, BEq instances.
why it matters
This result supplies the five_frameworks component of the downstream ethicsCert definition that assembles the full EthicsCert record. It realizes the module claim that the five frameworks correspond to configDim D = 5 and anchors the ethical symmetry in the J-cost properties inherited from the forcing chain (T5 J-uniqueness). The declaration closes the enumeration step required for the structural certification of ethical frameworks within the Recognition Science architecture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.