发表机构
Universidad Nacional de Ingeniería; Departamento de Estatística, IME, Universidade de São Paulo（秘鲁国立工程学院; 圣保罗大学数学学院统计系）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究将Birnbaum定理形式化为有限样本表述，证明其归结为证据等价性沿条件性相关推断基链的传播，并用维恩图和有限示例阐明条件性与充分性关系，且指出似然不变程序类严格包含于充分性不变程序类。
AI 中文摘要
Birnbaum定理指出，充分性原则与条件性原则共同蕴含似然原则，且被似然原则所蕴含。为了在Lean中实现结果的正式认证，我们基于\cite{Evans2013}通过有限样本表述使条件性关系显式化。我们将该定理重新表述为关于保持统计关系的统计程序类别的命题，并证明其证明可归结为证据等价性沿条件性相关推断基（实验-观测对）链的传播。主要结果通过维恩图加以说明，一个具体的有限示例展示了两个推断基对：一对由条件性相关但非充分性相关，另一对由充分性相关但非条件性相关。对于至少含两个点的有限参数空间，值域为$[0,1]$的似然不变程序类严格包含于充分性不变程序类之中。
英文摘要
Birnbaum's theorem states that the sufficiency and conditionality principles jointly imply, and are implied by, the likelihood principle. To enable formal certification of the results in Lean, we make the conditionality relation explicit through a finite-sample formulation based on \cite{Evans2013}. We reformulate the theorem as a statement about classes of statistical procedures that preserve statistical relations, and show that the proof reduces to the propagation of evidential equality along chains of conditionality-related inference bases (experiment--observation pairs). The main results are illustrated by Venn diagrams, and a worked finite example exhibits two pairs of inference bases: one related by conditionality but not by sufficiency, and the other related by sufficiency but not by conditionality. For finite parameter spaces with at least two points, the class of likelihood-invariant procedures with codomain $[0,1]$ is strictly contained in the class of sufficiency-invariant procedures.
