pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Sociology.VotingParadoxesFromSigma

show as:
view Lean formalization →

The module encodes Arrow's three conditions for voting rules as binary axes inside the Recognition Science framework. It supplies signatures for admissible rules and links them to spatial dimension three, thereby deriving paradoxes from the underlying sigma. The module consists of definitions plus short matching lemmas that connect social choice to the phi-ladder.

claimArrow's three conditions appear as binary axes $A_1,A_2,A_3$. A voting rule satisfies the signature if it is admissible under the three conditions; the only such rules are dictatorships, and the three conditions are equivalent to spatial dimension $D=3$.

background

In the Sociology domain, Recognition Science models social aggregation by treating Arrow's conditions (unanimity, independence of irrelevant alternatives, nondictatorship) as binary axes aligned with the phi-ladder. ArrowCondition and arrowConditionCount introduce the three axes; VotingRuleSignature and IsArrowAdmissible capture the functional form of a social welfare map; dictatorship isolates the degenerate case. The module imports only Mathlib and sits downstream of the J-uniqueness and eight-tick octave results.

proof idea

This is a definition module, no proofs. It declares ArrowCondition, VotingRuleSignature and the predicate IsArrowAdmissible, then supplies the short lemmas arrow_dictatorship_only, three_conditions_match_D and D_equals_spatial_dim that equate the axes to spatial dimension three, ending with the certification VotingParadoxesCert.

why it matters in Recognition Science

The module supplies the sociological counterpart to T8 (D=3) of the unified forcing chain. By showing that Arrow's three conditions match the spatial dimension, it explains voting paradoxes as direct consequences of the Recognition Composition Law applied outside physics. The declarations feed the broader claim that sigma-derived structures generate impossibility results in social domains.

scope and limits

declarations in this module (10)