Updated: 2026-09-06
The fairness and policy results are proved on the stated policy domains.
Formalization gap: Theorem 3.1 assumes stability against profitable group entry; voluntary Lemma 4.1 assumes maximal participation. Deriving these refinements from the paper’s equilibrium definition remains unproved. Details.
cited publication with SHA-256
11fb7a52959948847ce19d85adf97256a30c3f1575941ff6efec0e33bf908e1c.| Result | Comparison with the paper |
|---|---|
| Fairness definitions and implications; score-ignoring policy | Exact. |
| Theorem 3.1 | Formalization gap: assume stability against profitable group entry with recalibrated school estimates; deriving this from source equilibrium remains unproved. Necessity is unknown. |
| Theorem 3.2 | Restricted scope: deterministic reported output; the memo’s randomized counterexample refutes the unrestricted conclusion. Determinism is sufficient, not shown necessary. |
| Theorem 3.2 summary | Typo fixed: “demographic” becomes “observable,” matching the argument. |
| Lemma 4.1, voluntary regimes | Formalization gap: select self-enforcing participation that no admissible candidate can strictly enlarge. The source equilibrium definition has not been shown to imply this selection; necessity is unknown. |
| Proposition 4.2 | Exact: the Gaussian observed-score model allows any base-only policy for students without access. |
| Proposition 4.3 | Exact conclusion: an unfair equilibrium in each regime refutes fairness, which the paper requires in every equilibrium. The variance comparison uses a direct calculation; voluntary equilibria use the Lemma 4.1 convention. |
| Lemma 4.1 cutoff | Typo fixed: c=(qtilde-intercept)/slope
on the positive-slope domain. |
| Theorem 4.4 and its reporting-conditioned generalization | Exact for mandatory participation; restricted voluntary equilibria: the latter use the same maximal-participation selection as Lemma 4.1. Necessity is unknown. |
Theorem 3.1’s stability against recalibrated group entry and the voluntary Lemma 4.1 maximal-participation restriction are not derived from the paper’s equilibrium definition. The corresponding conclusions for arbitrary source equilibria remain unproved. Selected equilibria do exist; the gap is extending the conclusions to the source equilibrium class.
The fixed-point argument also retains the analytic premises described in the memo; their source-model derivation remains open.
Theorem 3.2 restricts reported output to be deterministic; its randomized example shows that some restriction is needed, but not that determinism is necessary. The access law uses independence from the skill/noise block, beyond uncorrelated-access wording; necessity under the complete source model is unresolved. The equilibrium proof gaps have their main discussion in Section 5.
The Theorem 3.1 nonreport-mixture correction and Proposition 4.3 unconditional-variance calculation are detailed in the memo.
The positive-mass active-branch framework may be useful beyond Gaussian signals. No broader posterior calculation or unproved generalization is claimed here.
The memo gives the nonreport-mixture and cutoff correction, the randomized-policy example and checked operational blankness conclusion, and the unconditional Gaussian variance calculation.
The equilibrium coverage gaps are in Section 5. Section 6 distinguishes the supported randomized-output obstruction from conditions whose necessity is unknown.
PaperInterface.lean supplies the 15 selected transparent source-facing result specifications, and ProofInterface.lean supplies the corresponding checked endpoints. The selected surface covers the fairness implication, hidden- and observed-access protocols, optional and required reporting schedules, Theorems 3.1–3.2 and 4.4, and the reporting-conditioned supporting claims.
The fifteen paper prerequisites and one library prerequisite match their selected source connections. Result-specific assumptions and the equilibrium restrictions remain visible in the transparent specifications and Sections 4–6.
The statement map routes the paper’s access, signal, reporting, fairness, cutoff, and equilibrium formulas, including 19 formula presentations and two equation presentations. The four clarified Theorem 3.2 targets are identified in the source-to-Spec ledger and explained in the source clarification memo.
The reusable Gaussian signal-family primitive is source-screened in the library ledger. Paper-specific equilibrium, policy, access, reporting, and fairness statements remain in the paper layer.
DependencyDAG.pdf, generated from DependencyDAG.tex, distinguishes the source model, hidden-access and observed-access result families, the reporting-conditioned generalization, and open directions. The rendered PDF was visually inspected for readability and arrow/box overlap.
The focused-build receipt records the paper build, and the import-closure receipt records its Lean dependencies. The closeout record records acceptance evidence for its pinned inputs.
The checked definitions cover access actions and observation regimes, the hidden-access optional protocol, latent-skill, observable, demographic, and test-blank fairness, the access estimator, distributional equality, requirement policies, school information, the Gaussian student signal model, and the cutoff and local-candidate models used by Theorems 3.1–3.2. Exact routes are in the statement map.
| Source presentation | Transparent specification | Proof endpoint |
|---|---|---|
| Fairness implication chain | fairness_implication_chainSpec |
fairness_implication_chain_proof |
| Lemma 4.1 | lemma4_1_observed_access_strategy_proofness_source_coreSpec |
lemma4_1_observed_access_strategy_proofness_source_core_proof |
| Proposition 4.2 | proposition4_2_all_observed_access_requirement_protocols_source_coreSpec |
proposition4_2_all_observed_access_requirement_protocols_source_core_proof |
| Proposition 4.3 | proposition4_3_each_requirement_protocol_has_unfair_pbo_equilibriumSpec |
proposition4_3_each_requirement_protocol_has_unfair_pbo_equilibrium_proof |
| Reporting-conditioned generalization | reporting_conditioned_generalizationSpec |
reporting_conditioned_generalization_proof |
| Theorem 3.1: fairness failure | theorem3_1_hidden_access_pbo_fails_all_fairness_definitionsSpec |
theorem3_1_hidden_access_pbo_fails_all_fairness_definitions_proof |
| Theorem 3.1: optional reporting | theorem3_1_optional_reporting_source_timedSpec |
theorem3_1_optional_reporting_source_timed_proof |
| Theorem 3.1: reporting required | theorem3_1_report_required_source_timedSpec |
theorem3_1_report_required_source_timed_proof |
| Theorem 3.2: optional schedule | theorem3_2_optional_reporting_clarified_modelSpec |
theorem3_2_optional_reporting_clarified_model_proof |
| Theorem 3.2: report-required schedule | theorem3_2_report_required_clarified_modelSpec |
theorem3_2_report_required_clarified_model_proof |
| Theorem 4.4 | theorem4_4_all_observed_access_requirement_protocolsSpec |
theorem4_4_all_observed_access_requirement_protocols |
| Threshold acceptance interpretation | thompson_acceptance_interpretationSpec |
thompson_acceptance_interpretation_proof |
| Report-rule skill independence | report_decision_skill_independenceSpec |
report_decision_skill_independence_proof |
| Ignoring-test-scores witness | ignoring_test_scores_achieves_fairnessSpec |
ignoring_test_scores_achieves_fairness_proof |
| Theorem 3.2 observable summary | theorem3_2_observable_summary_clarifiedSpec |
theorem3_2_observable_summary_clarified_proof |
The source-to-Spec ledger contains 15 current judgments: 12 matches and three corrected-target matches for the clarified Theorem 3.2 rows. The human review packet presents the same selected claim surface.
The statement map retains 81 source items, including supporting model and formula presentations. Fifteen result claims, fifteen paper prerequisites, and one library prerequisite form the current selected semantic comparison; the same source scope appears in the packet.