Biprofile Deviation Logic: Report-Replacement Frames and Audit Witnesses
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910213644222464 |
|---|---|
| author | Alpay, Faruk Basaran, Baris |
| author_facet | Alpay, Faruk Basaran, Baris |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_12537 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Biprofile Deviation Logic: Report-Replacement Frames and Audit Witnesses Alpay, Faruk Basaran, Baris Logic in Computer Science Computer Science and Game Theory 03B45, 03B70, 68Q60, 91B14 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. |
| title | Biprofile Deviation Logic: Report-Replacement Frames and Audit Witnesses |
| topic | Logic in Computer Science Computer Science and Game Theory 03B45, 03B70, 68Q60, 91B14 |
| url | https://arxiv.org/abs/2605.12537 |