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.

翻译：双轮廓偏差逻辑将策略性社会选择状态建模为对偶 $(R,P)$，其中 $R$ 是用于福利比较的真实轮廓，$P$ 是规则所使用的提交报告轮廓。联盟模态算子仅替换联盟的报告，其关系满足固定律 $E_C \circ E_D = E_{C \cup D}$。本文证明了 $H_{\mathrm{bp}}$ 对于抽象框架类 $\mathrm{Dev}(N)$ 的可靠性与完备性，并在规范证明中展示了反向组合中点。随后通过坐标分离将抽象的 $\mathrm{Dev}(N)$ 分量与真实的报告坐标积区分开来。在社会选择层面，经典事实提供了源概念；本文的具体贡献在于表示变更的审计层：类型化操纵证据、领域外扩展的行边界定理，以及公开删除的因子闭包准则。附录材料包含输入格式、可执行证书验证器、有限关系引理与更新模式的 Lean 与 Alloy 辅助验证、运行日志记录及校验和。