Biprofile Deviation Logic: Report-Replacement Frames and Audit Witnesses

TL;DR

This paper introduces biprofile deviation logic for modeling strategic social choice states, providing formal proofs, an audit layer for representation changes, and supporting tools for verification.

Contribution

It develops a new logical framework for social choice with audit witnesses, including formal soundness, completeness, and tools for verification.

Findings

Proves soundness and completeness of $H_{bp}$ for $ ext{Dev}(N)$.

Introduces an audit layer with typed manipulation witnesses.

Provides tools like Lean and Alloy companions for verification.

Abstract

Biprofile deviation logic models strategic social choice states as pairs $(R,P)$, where $R$ is the true profile used for welfare comparisons and $P$ is the submitted report profile used by the rule. Coalition modalities replace only the reports of the coalition, and their relations satisfy the fixed law $E_C \circ E_D = E_{C \cup D}$. The paper proves soundness and completeness of $H_{\mathrm{bp}}$ for the abstract frame class $\mathrm{Dev}(N)$, with the reverse-composition midpoint displayed inside the canonical proof. It then separates abstract $\mathrm{Dev}(N)$-components from genuine report-coordinate products by coordinate separation. On the social-choice side, the classical facts supply the source notions; the paper-specific contribution is the audit layer for representation changes: typed manipulation witnesses, a boundary-row theorem for off-domain extensions, and a factor-closure criterion for public deletions. The ancillary material contains the input formats, an executable certificate checker, Lean and Alloy companions for the finite relational lemmas and update patterns, recorded run logs, and checksums.