pith. sign in
module module high

IndisputableMonolith.Decision.ArrowViolationFromJCost

show as:
view Lean formalization →

Module ArrowViolationFromJCost shows that the J-cost function violates Arrow's four axioms in social choice. It imports the CanonicalJBand template to secure J(1)=0 and non-negativity on positive ratios, then defines the axioms and a violation certificate. Decision theorists and Recognition Science researchers cite it to link the J-function to impossibility results. The module is purely definitional, building directly on the six-clause J-cost template without further lemmas.

claimLet $J(x) = (x + x^{-1})/2 - 1$. No social welfare function satisfies the conjunction of unrestricted domain, Pareto efficiency, independence of irrelevant alternatives, and non-dictatorship when individual preferences are ranked by J-cost; the incompatibility is witnessed by ArrowViolationCert.

background

In the Decision domain, Recognition Science evaluates preference aggregation using the J-cost function that satisfies the Recognition Composition Law. The upstream CanonicalJBand supplies the reusable six-clause template that proves matched-zero (J(1)=0) and nonnegativity (J(x) ≥ 0 for x > 0). This module applies that template to the classical Arrow axioms: unrestricted domain (UD), Pareto, independence of irrelevant alternatives (IIA), and non-dictatorship. It imports Mathlib for basic structures and CanonicalJBand for the J properties, then introduces the corresponding definitions and certificate.

proof idea

This is a definition module, no proofs. It declares ArrowAxiom as the conjunction of the four properties, arrow_axiom_count as the integer 4, ArrowViolationCert as the structure witnessing the violation under J-cost, and arrowViolationCert as the concrete instance obtained from the CanonicalJBand template.

why it matters in Recognition Science

The module feeds the decision-domain certificates in the Recognition Science master cert chain by exhibiting an Arrow violation forced by the J-cost band. It aligns with T5 J-uniqueness and supports the claim that the phi-ladder constrains aggregation rules, consistent with the six-clause template used across B-tier openings and Plan v7 domain certs.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)