# Formalization Status Sources: [`registry.yaml`](../../registry.yaml) and [`formalization-search.json`](../provenance/formalization-search.json). Regenerate: `python3 scripts/generate_registry_views.py`. Workbench capital vs statement-match grades: see [methodology](../guide/methodology.md#workbench-metrics-vs-statement-match-grades). `RELATED` is scoped capital (not failed match; not by itself finished). Statement-match is not the primary success score. | Metric | Current | |---|---:| | Results stating a source claim | 49 | | Results recording a formalization only | 95 | | Registry results with atlas Lean (any grade) | 111 | | Claim results with statement-match (`EXACT` or `EQUIVALENT`) | 16 | | Claim results with workbench formalizations (`RELATED` only) | 9 | | Formalization records | 210 | | … declaring reproduction (self-attested; see methodology) | 208 | | Atlas Lean theorem declarations (unique names) | 379 | | Registry Lean declaration records | 379 | | … of which `WRAPPER` | 29 | | … of which `BRIDGE` | 37 | | … of which `NEW_PROOF` | 311 | | … of which `REFERENCE` | 2 | | Registry rows whose atlas Lean is wrapper-only | 10 | | Registry rows with at least one `BRIDGE` declaration | 22 | | Structured `candidate_formalizations` leads | 5 | | Reproduced external formalization records | 8 across 7 registry results | | Claim results with reviewed AI-system bridges | 3 | | … statement-reviewed only, interpretation withheld | 1 | | Brcic–Yampolskiy survey rows catalogued (that source, complete) | 44 / 44 | | Survey rows with atlas Lean (any grade) | 20 | | … with six-corpus discovery evidence (that source, complete) | 44 / 44 | ## Registry Lean declarations | ID | Registry result | Formalization relationships | Source declarations | Atlas declarations and layers | |---|---|---|---|---| | BY-001 | Unobservability | `EXACT` | `AISafetyAtlas.LinearSystems.DeterminesStateSolOn`
`AISafetyAtlas.LinearSystems.IsSolution`
`AISafetyAtlas.LinearSystems.outputSignal`
`AISafetyAtlas.LinearSystems.IsObservable`
`AISafetyAtlas.Examples.LinearSystems.pairA`
`AISafetyAtlas.Examples.LinearSystems.firstB`
`AISafetyAtlas.Examples.LinearSystems.firstC`
`AISafetyAtlas.LinearSystems.DeterminesStateOn`
`AISafetyAtlas.LinearSystems.IsTrajectoryOn`
`AISafetyAtlas.LinearSystems.eigenTrajectory`
`AISafetyAtlas.LinearSystems.unobservableSubspace`
`AISafetyAtlas.Examples.LinearSystems.integratorA`
`AISafetyAtlas.Examples.LinearSystems.blindC` | `AISafetyAtlas.LinearSystems.determinesStateSolOn_iff_isObservable (NEW_PROOF)`
`AISafetyAtlas.Examples.LinearSystems.pair_not_determinesStateSolOn (NEW_PROOF)`
`AISafetyAtlas.LinearSystems.determinesStateOn_iff_isObservable (NEW_PROOF)`
`AISafetyAtlas.LinearSystems.not_determinesStateOn_of_not_isObservable (NEW_PROOF)`
`AISafetyAtlas.Examples.LinearSystems.blind_not_determinesStateOn (NEW_PROOF)` | | BY-002 | Uncontrollability of dynamical systems | `EXACT` | `AISafetyAtlas.LinearSystems.IsCompletelyReachableSol`
`AISafetyAtlas.LinearSystems.IsSolution`
`AISafetyAtlas.LinearSystems.IsControllable`
`AISafetyAtlas.Examples.LinearSystems.pairA`
`AISafetyAtlas.Examples.LinearSystems.firstB`
`AISafetyAtlas.LinearSystems.IsCompletelyReachable`
`AISafetyAtlas.LinearSystems.drivenState`
`AISafetyAtlas.LinearSystems.reachedSet`
`AISafetyAtlas.LinearSystems.IsReachable`
`AISafetyAtlas.LinearSystems.eigenTrajectory`
`AISafetyAtlas.Examples.LinearSystems.integratorA`
`AISafetyAtlas.Examples.LinearSystems.deafB` | `AISafetyAtlas.LinearSystems.isCompletelyReachableSol_iff_isControllable (NEW_PROOF)`
`AISafetyAtlas.Examples.LinearSystems.pair_not_isCompletelyReachableSol (NEW_PROOF)`
`AISafetyAtlas.LinearSystems.isCompletelyReachable_iff_isControllable (NEW_PROOF)`
`AISafetyAtlas.LinearSystems.not_isReachable_of_not_isControllable (NEW_PROOF)`
`AISafetyAtlas.Examples.LinearSystems.deaf_not_isCompletelyReachable (NEW_PROOF)` | | BY-004 | Law of Requisite Variety | `RELATED`
`EXACT` | `AISafetyAtlas.Control.admittedOutcomes`
`AISafetyAtlas.Control.card_le_mul_card_admittedOutcomes`
`AISafetyAtlas.Control.shiftTable`
`AISafetyAtlas.Control.card_admittedOutcomes_shiftTable`
`AISafetyAtlas.Control.card_le_mul_card_admittedOutcomes_mul`
`AISafetyAtlas.Control.entropy_ge_of_condEntropy_ge`
`AISafetyAtlas.Control.condEntropy_outcome_eq`
`AISafetyAtlas.Control.entropy_outcome_ge`
`AISafetyAtlas.InformationTheory.condEntropy_comp_self_left`
`AISafetyAtlas.Control.entropy_outcome_ge_of_strategy`
`AISafetyAtlas.InformationTheory.channelCapacity`
`AISafetyAtlas.Control.entropy_outcome_ge_sub_channelCapacity`
`AISafetyAtlas.InformationTheory.channelCapacity_eq_of_card_eq_pow`
`AISafetyAtlas.Control.two_le_card_admittedOutcomes` | `AISafetyAtlas.Control.ashby_variety_ge (NEW_PROOF)`
`AISafetyAtlas.Control.card_ceilDiv_le_admittedOutcomes (NEW_PROOF)`
`AISafetyAtlas.Control.ashby_variety_ge_isSharp (NEW_PROOF)`
`AISafetyAtlas.Control.ashby_logVariety_ge_mul (NEW_PROOF)`
`AISafetyAtlas.Control.ashby_logVariety_ge (NEW_PROOF)`
`AISafetyAtlas.Control.card_le_mul_card_admittedOutcomes_mul (NEW_PROOF)`
`AISafetyAtlas.Control.two_le_card_admittedOutcomes (NEW_PROOF)`
`AISafetyAtlas.Control.entropy_ge_of_condEntropy_ge (NEW_PROOF)`
`AISafetyAtlas.Control.condEntropy_outcome_eq (NEW_PROOF)`
`AISafetyAtlas.Control.entropy_outcome_ge (NEW_PROOF)`
`AISafetyAtlas.Control.entropy_outcome_ge_of_strategy (NEW_PROOF)`
`AISafetyAtlas.Control.entropy_ge_of_sensor (NEW_PROOF)`
`AISafetyAtlas.Control.entropy_outcome_ge_sub_channelCapacity (NEW_PROOF)`
`AISafetyAtlas.Control.entropy_le_channelCapacity_of_complete (NEW_PROOF)`
`AISafetyAtlas.InformationTheory.channelCapacity_fun (NEW_PROOF)`
`AISafetyAtlas.InformationTheory.channelCapacity_prod (NEW_PROOF)`
`AISafetyAtlas.InformationTheory.channelCapacity_eq_of_card_eq_two_pow (NEW_PROOF)`
`AISafetyAtlas.InformationTheory.channelCapacity_eq_of_card_eq_pow (NEW_PROOF)`
`AISafetyAtlas.Oversight.not_forces_of_card_lt (BRIDGE)` | | BY-005 | Information-theoretical control limits | `RELATED`
`EXACT` | `AISafetyAtlas.Control.controlLoss`
`AISafetyAtlas.Control.Purified`
`AISafetyAtlas.Control.OpenLoopBound`
`AISafetyAtlas.Control.IsPlant`
`AISafetyAtlas.Control.entropyReduction_le_of_condEntropy_ge`
`AISafetyAtlas.Control.entropy_noise_sub_controlLoss`
`AISafetyAtlas.Control.entropyReduction`
`AISafetyAtlas.Control.minControlLoss_le`
`AISafetyAtlas.Control.controlLoss_le_entropy_noise`
`AISafetyAtlas.Control.inputPolicies`
`AISafetyAtlas.Control.IsInputPolicy`
`AISafetyAtlas.Control.controlLoss_eq_condMutualInfo`
`AISafetyAtlas.Control.controlLoss_eq_mutualInfo_sub`
`AISafetyAtlas.Control.bddBelow_controlLoss_image`
`AISafetyAtlas.Control.minControlLoss`
`AISafetyAtlas.Control.plantOutcome`
`AISafetyAtlas.Control.controlLoss_eq_entropy_noise_iff`
`AISafetyAtlas.Control.kernelMeasure_prod`
`AISafetyAtlas.Control.condEntropy_atom_kernelMeasure`
`AISafetyAtlas.Control.kernelMinControlLoss_eq`
`AISafetyAtlas.Control.minControlLoss_inputPolicies_eq`
`AISafetyAtlas.Control.bestAction`
`AISafetyAtlas.Control.closedFormLoss_le_controlLoss`
`AISafetyAtlas.Control.entropyReduction_le_condEntropy_form`
`AISafetyAtlas.Control.condEntropy_fibre_eq_openLoopEntropy`
`AISafetyAtlas.Control.entropyReduction_const`
`AISafetyAtlas.Control.openLoopReduction`
`AISafetyAtlas.Control.condEntropy_ge_of_openLoopMax`
`AISafetyAtlas.Control.entropy_eq_zero_iff`
`AISafetyAtlas.Control.sensorLoss`
`AISafetyAtlas.Control.PerfectlyObservable`
`Oversight`
`blind_channel_buys_nothing`
`budget_is_the_channel_not_the_volume` | `AISafetyAtlas.Control.entropy_noise_sub_controlLoss (NEW_PROOF)`
`AISafetyAtlas.Control.entropyReduction_le_of_openLoopBound (NEW_PROOF)`
`AISafetyAtlas.Control.condEntropy_ge_of_openLoopBound (NEW_PROOF)`
`AISafetyAtlas.Control.controlLoss_le_entropy_noise (NEW_PROOF)`
`AISafetyAtlas.Control.controlLoss_eq_entropy_noise_iff (NEW_PROOF)`
`AISafetyAtlas.Control.controlLoss_eq_condMutualInfo (NEW_PROOF)`
`AISafetyAtlas.Control.controlLoss_eq_mutualInfo_sub (NEW_PROOF)`
`AISafetyAtlas.Control.condEntropy_le_condEntropy_of_forall (NEW_PROOF)`
`AISafetyAtlas.Control.entropyReduction_le_of_condEntropy_ge (NEW_PROOF)`
`AISafetyAtlas.Control.minControlLoss_le_entropy_noise (NEW_PROOF)`
`AISafetyAtlas.Control.minControlLoss_eq_sInf_condMutualInfo (NEW_PROOF)`
`AISafetyAtlas.Control.minControlLoss_eq_sInf_mutualInfo_sub (NEW_PROOF)`
`AISafetyAtlas.Control.minControlLoss_le (NEW_PROOF)`
`AISafetyAtlas.Control.minControlLoss_nonneg (NEW_PROOF)`
`AISafetyAtlas.Control.measurable_plantOutcome (NEW_PROOF)`
`AISafetyAtlas.Control.isPlant_plantOutcome (NEW_PROOF)`
`AISafetyAtlas.Control.minControlLoss_eq_entropy_noise_iff_of_attained (NEW_PROOF)`
`AISafetyAtlas.Control.kernelControlLoss_eq_sum (NEW_PROOF)`
`AISafetyAtlas.Control.minControlLoss_inputPolicies_eq_kernelMin (NEW_PROOF)`
`AISafetyAtlas.Control.minControlLoss_inputPolicies_attained (NEW_PROOF)`
`AISafetyAtlas.Control.entropyReduction_le_condEntropy_form (NEW_PROOF)`
`AISafetyAtlas.Control.entropyReduction_le_iSup_openLoopReduction (NEW_PROOF)`
`AISafetyAtlas.Control.exists_entropyReduction_const_eq_iSup_openLoopReduction (NEW_PROOF)`
`AISafetyAtlas.Control.entropyReduction_le_openLoopMax (NEW_PROOF)`
`AISafetyAtlas.Control.perfectlyObservable_iff_sensorLoss_eq_zero (NEW_PROOF)`
`AISafetyAtlas.Control.condMutualInfo_eq_zero_of_sensorLoss_eq_zero (NEW_PROOF)`
`AISafetyAtlas.Control.mutualInfo_prod_eq_of_sensorLoss_eq_zero (NEW_PROOF)`
`AISafetyAtlas.Control.OversightBudget.oversight_reduction_le_budget (BRIDGE)` | | BY-007 | Arrow's impossibility theorem | `EQUIVALENT` | `AISafetyAtlas.Upstream.Arrow.Impossibility` | `AISafetyAtlas.SocialChoice.arrow (WRAPPER)`
`AISafetyAtlas.SocialChoice.Utility.arrow (WRAPPER)` | | BY-010 | Fairness impossibility theorem | `RELATED` | `AISafetyAtlas.Fairness.Instance`
`AISafetyAtlas.Fairness.RiskAssignment`
`AISafetyAtlas.Fairness.Calibrated`
`AISafetyAtlas.Fairness.BalancedPositive`
`AISafetyAtlas.Fairness.BalancedNegative`
`AISafetyAtlas.Fairness.PerfectPrediction`
`AISafetyAtlas.Fairness.EqualBaseRates`
`AISafetyAtlas.Fairness.sum_assignedPos`
`AISafetyAtlas.Fairness.sum_score_eq_μ`
`AISafetyAtlas.Fairness.assigned_eq_add`
`AISafetyAtlas.Fairness.negativeScore`
`AISafetyAtlas.Fairness.ApproxCalibrated`
`AISafetyAtlas.Fairness.ApproxBalancedPositive`
`AISafetyAtlas.Fairness.ApproxBalancedNegative`
`AISafetyAtlas.Fairness.ApproxPerfectPrediction`
`AISafetyAtlas.Fairness.ApproxEqualBaseRates`
`AISafetyAtlas.Fairness.slack`
`AISafetyAtlas.Fairness.average_lower_bound`
`AISafetyAtlas.Fairness.approx_perfect_prediction_or_equal_base_rates`
`AISafetyAtlas.Fairness.continuous_slack`
`AISafetyAtlas.Fairness.tendsto_slack_zero`
`AISafetyAtlas.Fairness.ApproxCalibratedScoreRelative`
`AISafetyAtlas.Fairness.scoreRelativeSlack`
`AISafetyAtlas.Fairness.approx_tradeoff_of_score_relative_calibration`
`AISafetyAtlas.Fairness.continuous_scoreRelativeSlack`
`AISafetyAtlas.Fairness.sum_score_bounds`
`AISafetyAtlas.Fairness.baseRate`
`AISafetyAtlas.Fairness.approxCalibrated_zero_iff`
`AISafetyAtlas.Fairness.perfectPrediction_of_approx_zero` | `AISafetyAtlas.Fairness.perfect_prediction_or_equal_base_rates (NEW_PROOF)`
`AISafetyAtlas.Fairness.print_perfectPrediction_of_populated (NEW_PROOF)`
`AISafetyAtlas.Fairness.sum_score_eq_μ (NEW_PROOF)`
`AISafetyAtlas.Fairness.negativeScore_eq (NEW_PROOF)`
`AISafetyAtlas.Fairness.perfect_of_negativeScore_eq_zero (NEW_PROOF)`
`AISafetyAtlas.Fairness.approx_perfect_prediction_or_equal_base_rates (NEW_PROOF)`
`AISafetyAtlas.Fairness.exists_slack_function (NEW_PROOF)`
`AISafetyAtlas.Fairness.approx_tradeoff_of_score_relative_calibration (NEW_PROOF)`
`AISafetyAtlas.Fairness.exists_slack_function_score_relative (NEW_PROOF)`
`AISafetyAtlas.Fairness.average_lower_bound (NEW_PROOF)`
`AISafetyAtlas.Fairness.perfect_prediction_or_equal_base_rates_of_approx (NEW_PROOF)` | | BY-011 | Limits on preference deduction | `RELATED` | `AISafetyAtlas.Preference.Planner`
`AISafetyAtlas.Preference.Explains`
`AISafetyAtlas.Preference.exists_planner`
`AISafetyAtlas.Preference.greedyAction_max`
`AISafetyAtlas.Preference.greedyPlanner`
`AISafetyAtlas.Preference.rewardOf`
`AISafetyAtlas.Preference.Source.ReasonableForF.F₁_of_compatible`
`AISafetyAtlas.Preference.Source.ReasonableForF.F₂_of_compatible`
`AISafetyAtlas.Preference.Source.ReasonableForF.F₃_of_compatible`
`AISafetyAtlas.Preference.Source.ReasonableForF.F₄_F₄`
`AISafetyAtlas.Preference.op3_op4`
`AISafetyAtlas.Preference.ReasonableLanguage.policy_le_of_compatible`
`AISafetyAtlas.Preference.op3_op1_op5`
`AISafetyAtlas.Preference.op3_op2_op6`
`AISafetyAtlas.Preference.op3_op4_op2_op6`
`AISafetyAtlas.Preference.ReasonableLanguage.Compatible`
`AISafetyAtlas.Preference.plainK_le_of_partrec`
`AISafetyAtlas.Preference.partrec_evalPair`
`Kolmogorov.plainKMapLe`
`AISafetyAtlas.Preference.decodeBehaviour_encodeExplanation`
`AISafetyAtlas.Preference.computable_encodeExplanation`
`AISafetyAtlas.Preference.explanation_at_least_behaviour`
`AISafetyAtlas.Preference.degenerate_explanation_cheap`
`AISafetyAtlas.Wireheading.Corruption.ComplementedClass.halfMaximalRegretBound`
`AISafetyAtlas.Preference.OverrideModel.mixtureValue`
`AISafetyAtlas.Preference.OverrideModel`
`AISafetyAtlas.Preference.Source.ReasonableForF.NotAmongLowestCompatible`
`AISafetyAtlas.Preference.Source.ReasonableForF.proposition_seven`
`AISafetyAtlas.Preference.OverrideModel.regret` | `AISafetyAtlas.Preference.exists_planner (NEW_PROOF)`
`AISafetyAtlas.Preference.exists_reward (NEW_PROOF)`
`AISafetyAtlas.Preference.consistent_rewards_eq_univ (NEW_PROOF)`
`AISafetyAtlas.Preference.neg_twin (NEW_PROOF)`
`AISafetyAtlas.Preference.greedy_rewardOf (NEW_PROOF)`
`AISafetyAtlas.Preference.Source.ReasonableForF.proposition_seven (NEW_PROOF)`
`AISafetyAtlas.Preference.Source.ReasonableForF.proposition_eight (NEW_PROOF)`
`AISafetyAtlas.Preference.ReasonableLanguage.proposition_seven (NEW_PROOF)`
`AISafetyAtlas.Preference.ReasonableLanguage.proposition_eight (NEW_PROOF)`
`AISafetyAtlas.Preference.behaviour_le_of_evaluatesTo (NEW_PROOF)`
`AISafetyAtlas.Preference.explanation_at_least_behaviour (NEW_PROOF)`
`AISafetyAtlas.Preference.degenerate_explanation_cheap (NEW_PROOF)`
`AISafetyAtlas.Preference.explanation_complexity_eq_behaviour (NEW_PROOF)`
`AISafetyAtlas.Preference.RegretModel.cannot_rule_out_half_maximal_regret (NEW_PROOF)`
`AISafetyAtlas.Preference.OverrideModel.mixtureValue_rationalise (NEW_PROOF)`
`AISafetyAtlas.Preference.Source.ReasonableForF.theorem_two_conditional (NEW_PROOF)`
`AISafetyAtlas.Preference.OverrideModel.rationalise_strictly_better (NEW_PROOF)` | | BY-012 | Rice's theorem | `EQUIVALENT`
`EXACT` | `ComputablePred.rice`
`ComputablePred.rice₂` | `AISafetyAtlas.Computability.rice (WRAPPER)`
`AISafetyAtlas.Computability.rice_code_iff (WRAPPER)`
`AISafetyAtlas.Verification.rice (BRIDGE)` | | BY-013 | Unprovability | `EQUIVALENT`
`RELATED` | `LO.FirstOrder.Arithmetic.exists_true_but_unprovable_sentence`
`LO.FirstOrder.Arithmetic.consistent_unprovable` | `AISafetyAtlas.Logic.godel_first_incompleteness (WRAPPER)`
`AISafetyAtlas.Logic.godel_second_incompleteness (WRAPPER)` | | BY-014 | Undecidability | `RELATED`
`EXACT` | `ComputablePred.halting_problem_re`
`ComputablePred.halting_problem`
`ComputablePred.halting_problem_not_re` | `AISafetyAtlas.Computability.halting_re (WRAPPER)`
`AISafetyAtlas.Computability.halting_problem (WRAPPER)`
`AISafetyAtlas.Computability.nonhalting_not_re (WRAPPER)` | | BY-015 | Chaitin incompleteness | `EQUIVALENT` | `Kolmogorov.FormalSystem.chaitinIncompleteness`
`Kolmogorov.FormalSystem.chaitinBound` | `AISafetyAtlas.Logic.chaitin_incompleteness (WRAPPER)`
`AISafetyAtlas.Logic.chaitin_bound (WRAPPER)` | | BY-016 | Undefinability | `EQUIVALENT` | `LO.FirstOrder.Arithmetic.undefinability_of_truth` | `AISafetyAtlas.Logic.tarski_undefinability (WRAPPER)` | | BY-020 | No Free Lunch — supervised learning | `RELATED` | `AISafetyAtlas.Learning.sum_pointLoss_off_training`
`AISafetyAtlas.Learning.aggregateOffTrainingLoss_eq`
`AISafetyAtlas.Learning.HomogeneousLoss`
`AISafetyAtlas.Learning.lossConfig`
`AISafetyAtlas.Learning.lossConfig_sum_learner_indep`
`AISafetyAtlas.Learning.homogeneous_of_learner_indep` | `AISafetyAtlas.Learning.no_free_lunch_supervised (NEW_PROOF)`
`AISafetyAtlas.Learning.lossConfig_sum_learner_indep (NEW_PROOF)`
`AISafetyAtlas.Learning.ots_error_distribution_learner_indep (NEW_PROOF)`
`AISafetyAtlas.Learning.homogeneous_of_learner_indep (NEW_PROOF)`
`AISafetyAtlas.Learning.homogeneous_iff_learner_indep (NEW_PROOF)` | | BY-021 | No Free Lunch — optimization | `RELATED` | `AISafetyAtlas.Learning.nfl_adaptive_of_permInvariant`
`AISafetyAtlas.Learning.permInvariant_of_nfl`
`AISafetyAtlas.Learning.mixtureTrace`
`AISafetyAtlas.Learning.mixtureTrace_eq_sum_mul`
`AISafetyAtlas.Learning.stochasticTrace`
`AISafetyAtlas.Learning.induced`
`AISafetyAtlas.Combinatorics.closedUnderPermutationEquivSet`
`AISafetyAtlas.Combinatorics.spectrum`
`AISafetyAtlas.Combinatorics.forall_rel_of_permInvariant`
`AISafetyAtlas.Learning.sum_performance_eq_scaled_sum`
`AISafetyAtlas.Learning.aggregatePerformance_eq_scaled_sum`
`AISafetyAtlas.Learning.observed_of_consistent`
`AISafetyAtlas.Learning.adaptive_constraint_card`
`AISafetyAtlas.Learning.PermInvariant`
`AISafetyAtlas.Learning.weightedTrace`
`AISafetyAtlas.Learning.observed_eq_iff`
`AISafetyAtlas.Combinatorics.histogram`
`AISafetyAtlas.Combinatorics.basisClass`
`AISafetyAtlas.Combinatorics.permOrbit`
`AISafetyAtlas.Learning.exists_perm_ruleVisit`
`AISafetyAtlas.Learning.no_free_lunch_adaptive_of_sharp`
`AISafetyAtlas.Combinatorics.ClosedUnderPermutation`
`AISafetyAtlas.Learning.closedUnderPermutation_of_permInvariant`
`AISafetyAtlas.Learning.permRule`
`AISafetyAtlas.Learning.nfl_of_permInvariant`
`AISafetyAtlas.Learning.exists_perm_comp`
`AISafetyAtlas.Learning.weightedPerformance`
`AISafetyAtlas.Learning.weightedPerformance_indicator` | `AISafetyAtlas.Learning.nfl_adaptive_iff_permInvariant (NEW_PROOF)`
`AISafetyAtlas.Learning.nfl_mixture_of_permInvariant (NEW_PROOF)`
`AISafetyAtlas.Learning.nfl_stochastic_of_permInvariant (NEW_PROOF)`
`AISafetyAtlas.Combinatorics.card_closedUnderPermutation_nonempty (NEW_PROOF)`
`AISafetyAtlas.Combinatorics.exists_perm_rel_not_iff (NEW_PROOF)`
`AISafetyAtlas.Learning.no_free_lunch (NEW_PROOF)`
`AISafetyAtlas.Learning.no_free_lunch_adaptive (NEW_PROOF)`
`AISafetyAtlas.Learning.nfl_adaptive_of_permInvariant (NEW_PROOF)`
`AISafetyAtlas.Combinatorics.basisClass_histogram_eq_permOrbit (NEW_PROOF)`
`AISafetyAtlas.Learning.exists_observed_eq (NEW_PROOF)`
`AISafetyAtlas.Learning.card_observed_eq (NEW_PROOF)`
`AISafetyAtlas.Learning.closedUnderPermutation_of_permInvariant (NEW_PROOF)`
`AISafetyAtlas.Learning.no_free_lunch_adaptive_of_sharp (NEW_PROOF)`
`AISafetyAtlas.Learning.closedUnderPermutation_of_nfl (NEW_PROOF)`
`AISafetyAtlas.Learning.ruleVisit_permRule (NEW_PROOF)`
`AISafetyAtlas.Learning.observed_permRule (NEW_PROOF)`
`AISafetyAtlas.Learning.nfl_iff_permInvariant (NEW_PROOF)`
`AISafetyAtlas.Learning.nfl_of_permInvariant (NEW_PROOF)`
`AISafetyAtlas.Learning.permInvariant_of_nfl (NEW_PROOF)`
`AISafetyAtlas.Learning.permInvariant_of_closedUnderPermutation (NEW_PROOF)`
`AISafetyAtlas.Learning.no_free_lunch_embedding_of_sharp (NEW_PROOF)` | | BY-025 | Uncontainability | `RELATED` | `AISafetyAtlas.Computability.halting_problem` | `AISafetyAtlas.Verification.Containment.harming_undecidable (BRIDGE)` | | BY-027 | Löb's theorem (unverifiability) | `EQUIVALENT` | `LO.FirstOrder.Arithmetic.löb_theorem` | `AISafetyAtlas.Logic.loeb (WRAPPER)` | | BY-033 | Unverifiability of robot ethics | `RELATED` | `AISafetyAtlas.Computability.halting_problem` | `AISafetyAtlas.Verification.Robot.action_safety_unverifiable (BRIDGE)` | | BY-039 | Reward corruption unsolvability | `RELATED` | `AISafetyAtlas.Wireheading.CRMDP.Env.observed_complement`
`AISafetyAtlas.Wireheading.CRMDP.return_add_complement`
`AISafetyAtlas.Wireheading.Corruption.ComplementedClass.everitt_theorem_eleven` | `AISafetyAtlas.Wireheading.CRMDP.Model.everitt_theorem_eleven (NEW_PROOF)` | | BY-043 | Misaligned embodiment | `RELATED` | `Fleet`
`evaluating_one_covers_its_peers`
`no_designated_agent_emerges` | `AISafetyAtlas.Compositional.Symmetry.Protocol.no_unique_leader_from_symmetric_start (NEW_PROOF)`
`AISafetyAtlas.Compositional.AgentNetwork.symmetry_is_the_shared_cause (BRIDGE)` | | BY-044 | Limited self-awareness | `EQUIVALENT` | — | `AISafetyAtlas.SelfAwareness.Model.not_aware_of_le (NEW_PROOF)`
`AISafetyAtlas.SelfAwareness.Model.process_not_self_aware (NEW_PROOF)`
`AISafetyAtlas.SelfAwareness.Model.not_agentAware_of_maximal (NEW_PROOF)`
`AISafetyAtlas.SelfAwareness.Model.limited_self_awareness (NEW_PROOF)`
`AISafetyAtlas.SelfAwareness.Model.not_perfectlySelfAware (NEW_PROOF)` | | CLM-WOLPERT-KNOW-001 | Physical knowledge by inference devices | `EQUIVALENT` | — | `AISafetyAtlas.Inference.PhysicallyKnows.weaklyInfers (NEW_PROOF)`
`AISafetyAtlas.Inference.PhysicalKnowledgeWitness.eq_target_on_of_refinesOn (NEW_PROOF)`
`AISafetyAtlas.Inference.physicallyKnows_false_iff_not_true (NEW_PROOF)`
`AISafetyAtlas.Inference.not_physicallyKnows_true_and_false (NEW_PROOF)`
`AISafetyAtlas.Inference.exists_never_physicallyKnown (NEW_PROOF)` | | CLM-WOLPERT-EPISTEMIC-001 | Epistemic consequences of physical knowledge | `EQUIVALENT` | — | `AISafetyAtlas.Inference.corollary20_ii (NEW_PROOF)`
`AISafetyAtlas.Inference.exists_three_inequivalent_not_weaklyInfers (NEW_PROOF)`
`AISafetyAtlas.Inference.corollary23 (NEW_PROOF)`
`AISafetyAtlas.Inference.corollary24 (NEW_PROOF)` | | CLM-WOLPERT-APPROX-001 | Bounds on inference accuracy, and the collapse of the exact limits | `EQUIVALENT` | — | `AISafetyAtlas.Inference.identityDevice_weaklyInfers (NEW_PROOF)`
`AISafetyAtlas.Inference.exists_weaklyInfers_of_three_values (NEW_PROOF)`
`AISafetyAtlas.Inference.inferenceAccuracy_ge (NEW_PROOF)`
`AISafetyAtlas.Inference.fig5_accuracy_gap (NEW_PROOF)`
`AISafetyAtlas.Inference.exists_distinguishable_accuracy_near_one (NEW_PROOF)` | | LAND-WOLPERT-KNOW-DEFECTS-001 | Countermodels to Wolpert 2018 epistemic claims | | — | `AISafetyAtlas.Inference.corollary21_ii_repaired (NEW_PROOF)` | | CLM-LAWVERE-001 | Lawvere fixed-point theorem (types and functions) | `EQUIVALENT` | `Function.exists_fixed_point_of_surjective` | `AISafetyAtlas.Logic.lawvere_fixed_point (WRAPPER)` | | LAND-ATTR-001 | Attribution impossibility (DASH trilemma) | | `DASHImpossibility.attribution_impossibility`
`DASHImpossibility.attribution_impossibility_weak` | `AISafetyAtlas.Explainability.attribution_impossibility (WRAPPER)`
`AISafetyAtlas.Explainability.attribution_impossibility_weak (WRAPPER)` | | LAND-GS-002 | Gibbard–Satterthwaite theorem (Lean / SocialChoiceLean) | | `SocialChoice.gibbard_satterthwaite` | `AISafetyAtlas.SocialChoice.gibbard_satterthwaite (WRAPPER)` | | LAND-DEBATE-001 | Doubly-efficient debate correctness (Brown-Cohen–Irving–Piliouras 2023) | | `completeness`
`soundness`
`correctness`
`alice_fast`
`bob_fast`
`vera_fast` | `AISafetyAtlas.Oversight.Debate.completeness (WRAPPER)`
`AISafetyAtlas.Oversight.Debate.soundness (WRAPPER)`
`AISafetyAtlas.Oversight.Debate.correctness (WRAPPER)`
`AISafetyAtlas.Oversight.Debate.alice_fast (WRAPPER)`
`AISafetyAtlas.Oversight.Debate.bob_fast (WRAPPER)`
`AISafetyAtlas.Oversight.Debate.vera_fast (WRAPPER)` | | LAND-HYPER-002 | k-safety self-composition and hyperproperty decomposition | | `k_safety_iff_finite_self_composition`
`k_safety_iff_product_self_composition`
`self_composition_is_safety`
`isClosed_iff_hyperSafety`
`dense_iff_hyperLiveness`
`hyperSafety_of_isKSafety`
`hyperSafety_hyperLiveness_decomposition` | `AISafetyAtlas.Compositional.Hyperproperties.k_safety_iff_finite_self_composition (NEW_PROOF)` | | LAND-ANGLUIN-001 | Port-labelled anonymous networks, views, and automorphisms | | `runFor_eq_of_view_eq`
`step_equivariant`
`step_semiconj`
`invariant_iff_fixed`
`invariant_of_automorphism`
`no_unique_leader_of_fixedPointFree`
`invariant_of_constant` | `AISafetyAtlas.Compositional.Networks.runFor_eq_of_view_eq (NEW_PROOF)` | | LAND-PREF-KNOW-001 | Reward unidentifiability as a knowability obstruction | | — | `AISafetyAtlas.Preference.not_knowable_reward (NEW_PROOF)`
`AISafetyAtlas.Preference.knowable_reward_of_isEmpty_state (NEW_PROOF)` | | LAND-COMP-TRACE-001 | A network's runs as a trace system | | — | `AISafetyAtlas.Compositional.Networks.realizes_systemOf (NEW_PROOF)`
`AISafetyAtlas.Compositional.Networks.not_electsLeader_of_fixedPointFree (NEW_PROOF)` | | LAND-HYPER-KNOW-001 | Finite-observation safety as a knowability factorization | | — | `AISafetyAtlas.Compositional.Hyperproperties.knowable_of_isSafetyPredicate (NEW_PROOF)`
`AISafetyAtlas.Compositional.Hyperproperties.not_isSafetyPredicate_of_realizedSet_collision (NEW_PROOF)` | | LAND-CAUSAL-KNOW-001 | Behavioural identifiability as a knowability factorization | | — | `AISafetyAtlas.Causal.behaviorEq_iff_behavior_eq (NEW_PROOF)`
`AISafetyAtlas.Causal.exists_behaviorEq_pair_of_not_knowable (NEW_PROOF)` | | LAND-COMP-KNOW-001 | The Angluin view as a knowability factorization | | — | `AISafetyAtlas.Compositional.Networks.knowable_runFor (NEW_PROOF)`
`AISafetyAtlas.Compositional.Networks.sameView_iff_view_eq (NEW_PROOF)` | | LAND-RECT-001 | Rectangle, exchange, and unary-contract equivalences | | `rectangle_iff_exchange_closed`
`coordinate_product_iff_spliceClosed`
`not_isCoordinateProduct_finitelySupported`
`coordinate_product_iff_recombination_closed` | `AISafetyAtlas.Compositional.rectangle_iff_exchange_closed (NEW_PROOF)` | | LAND-WIRE-OBJ-001 | Ring-Orseau objective factorization | | `AgentEquations.value_eq_of_agree_on_window`
`AgentEquations.truncation_exact`
`AgentEquations.bestAction_max`
`Objective.value_eq_of_agree_on_window`
`Objective.value_scaleUtility`
`Objective.optimal_decisions_eq_of_pos_scaleUtility`
`Objective.value_congr`
`Objective.optimal_decisions_congr` | `AISafetyAtlas.Wireheading.AgentEquations.value_eq_of_agree_on_window (NEW_PROOF)` | | LAND-WIRE-AGENTHISTORY-001 | Ring-Orseau histories on the Decision carrier | | `AgentEquations.toDecisionHistory`
`AgentEquations.ofDecisionHistory`
`AgentEquations.ofDecisionHistory_toDecisionHistory`
`AgentEquations.toDecisionHistory_ofDecisionHistory`
`AgentEquations.toDecisionHistory_injective`
`AgentEquations.runHistory`
`AgentEquations.runHistory_length`
`AgentEquations.value_runHistory_eq_of_agree_on_window` | `AISafetyAtlas.Wireheading.AgentEquations.value_runHistory_eq_of_agree_on_window (NEW_PROOF)` | | LAND-WIRE-GOALCARRIER-001 | Self-modification on the Decision carrier | | `GoalPreservation.stepHistory`
`GoalPreservation.length_stepHistory`
`GoalPreservation.scheduleAct`
`GoalPreservation.scheduleAct_surjective`
`GoalPreservation.scheduleValue`
`GoalPreservation.scheduleValue_summable`
`GoalPreservation.scheduleValue_bellman`
`GoalPreservation.scheduleValue_le_of_isMax`
`GoalPreservation.scheduleModel`
`GoalPreservation.scheduleModel_optimalAt` | `AISafetyAtlas.Wireheading.GoalPreservation.scheduleModel_optimalAt (NEW_PROOF)` | | LAND-PREF-TRAJECTORY-001 | Preference unidentifiability at a trajectory | | `Preference.lastObs`
`Preference.lastObs_append`
`Preference.ofMemoryless`
`Preference.ofMemoryless_injective`
`Preference.lastObs_detHistoryUpTo`
`Preference.detStateAt_ofMemoryless_succ`
`Preference.trajectory_reward_unidentifiable`
`Preference.consistent_rewards_of_trajectory_eq_univ` | `AISafetyAtlas.Preference.consistent_rewards_of_trajectory_eq_univ (NEW_PROOF)` | | LAND-VERIF-ROBOTRUN-001 | A verified behaviour, run | | `Decision.detHistoryUpTo_length`
`Verification.Robot.ofBehavior`
`Verification.Robot.actionAt_ofBehavior`
`Verification.Robot.detStateAt_ofBehavior_succ`
`Verification.Robot.alwaysSatisfies_run` | `AISafetyAtlas.Verification.Robot.alwaysSatisfies_run (NEW_PROOF)` | | LAND-COMP-RUNTRACES-001 | The trace system a policy set generates | | `Hyperproperties.HistoryPrefix`
`Hyperproperties.detHistoryUpTo_prefix_succ`
`Hyperproperties.runTraces`
`Hyperproperties.mem_runTraces`
`Hyperproperties.runTraces_nonempty`
`Hyperproperties.runTraces_mono`
`Hyperproperties.bad_observation_prefixes_are_run_prefixes`
`Hyperproperties.exists_bad_trajectories_of_isKSafety` | `AISafetyAtlas.Compositional.Hyperproperties.exists_bad_trajectories_of_isKSafety (NEW_PROOF)` | | LAND-GOAL-001 | Finite-percept on-policy goal-preservation induction step | `RELATED` | `GoalPreservationSource.Model.selected_matches_initial`
`GoalPreservationSource.Model.safe_modification`
`GoalPreservationSource.Model.qValue_selected_eq_initial`
`next_policy_optimal`
`run_optimal`
`goal_preservation` | `AISafetyAtlas.Wireheading.GoalPreservationSource.Model.selected_matches_initial (NEW_PROOF)` | | LAND-VRL-001 | Value reinforcement learning and the consistency-preserving constraint | `RELATED` | `ValueLearning.Beliefs.isEEP_of_isCP`
`ValueLearning.Beliefs.vrlValue_of_isEEP`
`ValueLearning.Beliefs.vrlValue_of_isCP`
`ValueLearning.Beliefs.vrlValue_eq_prior_mixture`
`ValueLearning.Beliefs.posterior_expectation`
`ValueLearning.Beliefs.vrlValue_eq_rlValue`
`ValueLearning.Beliefs.sum_condReward`
`ValueLearning.Beliefs.marginalReward_nonneg` | `AISafetyAtlas.Wireheading.ValueLearning.Beliefs.vrlValue_of_isCP (NEW_PROOF)` | | LAND-GOAL-002 | Theorem 16 equation (13) over the whole trajectory, without naming surjectivity | `RELATED` | `GoalPreservationRun.Model.equation_thirteen`
`GoalPreservationRun.Model.run_optimal`
`GoalPreservationRun.Model.optimalAt_next`
`GoalPreservationRun.Model.contValue_le_initial`
`GoalPreservationRun.Model.run_contValue_eq_initial` | `AISafetyAtlas.Wireheading.GoalPreservationRun.Model.equation_thirteen (NEW_PROOF)` | | LAND-JOINTOBS-001 | Coalition-indexed joint observation and the emitted-interface coverage boundary | | `covers_iff_no_collision`
`not_covers_of_collisionWitness`
`exists_collisionWitness_of_not_covers`
`decideCoverage`
`decideCoverage_covered_iff`
`CoverageResult.covered_eq_true_iff`
`decidableCovers`
`postprocess_cannot_repair_collision`
`covers_of_refines`
`observe_truthful`
`PortfolioCovers`
`PortfolioIndistinguishable`
`portfolioCovers_implies_hazardEquivalent`
`InclusionMinimalCovering`
`PortfolioCost`
`CostOptimalCovering`
`inclusionMinimal_of_costOptimal` | `AISafetyAtlas.Oversight.JointObservation.covers_iff_no_collision (NEW_PROOF)` | | LAND-SELFREF-001 | The self-model as a component of the state it models | | — | `AISafetyAtlas.Knowledge.SelfReference.selfComplete_iff_subsingleton_rest (NEW_PROOF)`
`AISafetyAtlas.Knowledge.SelfReference.not_selfComplete_of_two_rest (NEW_PROOF)`
`AISafetyAtlas.Knowledge.SelfReference.card_rest_le_one_of_selfComplete (NEW_PROOF)` | | LAND-ACCUM-001 | Window ambiguity: accumulation bounds over a set of targets | | — | `AISafetyAtlas.Knowledge.ambiguity_le_pairTarget_left (NEW_PROOF)`
`AISafetyAtlas.Knowledge.ambiguity_le_pairTarget_right (NEW_PROOF)`
`AISafetyAtlas.Knowledge.ambiguity_pairTarget_le_mul (NEW_PROOF)`
`AISafetyAtlas.Knowledge.not_knowable_pairTarget_of_not_knowable (NEW_PROOF)`
`AISafetyAtlas.Knowledge.ambiguity_le_of_evidenceMonotone (NEW_PROOF)`
`AISafetyAtlas.Knowledge.ambiguity_le_pairTarget_of_evidenceMonotone (NEW_PROOF)` | | LAND-AMBIG-001 | Finite fibre ambiguity and the counting obstruction | | — | `AISafetyAtlas.Knowledge.card_image_le_of_knowable (NEW_PROOF)`
`AISafetyAtlas.Knowledge.not_knowable_of_card_lt (NEW_PROOF)`
`AISafetyAtlas.Knowledge.ambiguity_le_of_comp (NEW_PROOF)`
`AISafetyAtlas.Knowledge.knowable_iff_ambiguity_le_one (NEW_PROOF)` | | LAND-TEMPORAL-001 | Time-indexed knowability, contemporaneous collisions, and delayed knowledge | | — | `AISafetyAtlas.Knowledge.Temporal.knowableFrom_mono (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Temporal.not_knowableAt_of_collisionAt (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Temporal.collisionAt_of_not_knowableAt (NEW_PROOF)` | | LAND-SELFMEAS-001 | Self-measurement failure for an embedded observation | | — | `AISafetyAtlas.Knowledge.knowable_id_iff_injective (NEW_PROOF)`
`AISafetyAtlas.Knowledge.not_knowable_state_of_nontrivial_remainder (NEW_PROOF)` | | LAND-SELFMEAS-002 | Breuer abstract embedded-measurement core | `EQUIVALENT` | — | `AISafetyAtlas.Knowledge.Embedded.not_knowable_state_of_properInclusion (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Embedded.Meshing.restrict_surjective (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Embedded.no_meshing_inference_distinguishes (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Embedded.no_meshing_inference_measures_all_states (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Embedded.exists_state_not_exactly_measurable (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Embedded.infer_singleton_eq_of_meshing (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Embedded.exists_singleton_infer_eq_of_infer_eq (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Embedded.eq_restrict_of_infer_singleton_eq (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Embedded.no_meshing_inference_measures_all_states_direct (NEW_PROOF)` | | LAND-SELFMEAS-003 | Physical complement and finite-cardinality bridges to Breuer proper inclusion | `RELATED` | — | `AISafetyAtlas.Knowledge.Embedded.Composition.properInclusion_of_nontrivial_remainder (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Embedded.Composition.no_meshing_measures_all_of_nontrivial_remainder (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Embedded.Composition.properInclusion_of_nontrivial_remainder_of_equiv (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Embedded.Composition.no_meshing_measures_all_of_nontrivial_remainder_of_equiv (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Embedded.Composition.measuresAll_fibreInference_of_injective (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Embedded.Composition.meshing_and_measuresAll_fibreInference_of_bijective (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Embedded.Finite.properInclusion_of_card_lt (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Embedded.Finite.no_meshing_measures_all_of_card_lt (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Embedded.Composition.properInclusion_iff_not_injective (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Embedded.Composition.not_meshing_of_not_surjective (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Embedded.Composition.meshing_fibreInference_of_surjective (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Embedded.Finite.properInclusion_product_of_card_rest_ge_two (NEW_PROOF)` | | LAND-KNOW-001 | Exact knowability: the observation-factorization kernel | | `Function.factorsThrough_iff` | `AISafetyAtlas.Knowledge.knowable_iff_factorsThrough (WRAPPER)`
`AISafetyAtlas.Knowledge.knowable_iff_no_collision (WRAPPER)`
`AISafetyAtlas.Knowledge.not_knowable_of_collision (NEW_PROOF)`
`AISafetyAtlas.Knowledge.not_knowable_of_witness (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Determines.trans (NEW_PROOF)`
`AISafetyAtlas.Knowledge.not_knowable_of_invariant_transform (NEW_PROOF)`
`AISafetyAtlas.Knowledge.exists_witness_of_not_knowable (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Knowable.mono (NEW_PROOF)`
`AISafetyAtlas.Knowledge.not_knowable_comp (NEW_PROOF)` | | LAND-KNOW-DEVICE-001 | Transports between the knowability kernel and inference devices | | — | `AISafetyAtlas.Knowledge.Devices.not_blockAnswers_of_witness (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Devices.BlockwiseCollision.not_weaklyInfers (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Devices.BlockwiseCollision.not_physicallyKnows (NEW_PROOF)`
`AISafetyAtlas.Knowledge.Devices.knowable_probe_of_forall_blockAnswers (NEW_PROOF)` | | LAND-CRMDP-KNOW-001 | True return does not factor through the observed history | | — | `AISafetyAtlas.Wireheading.ObservationLimits.not_knowable_trueReturn_of_complement_mem (NEW_PROOF)`
`AISafetyAtlas.Wireheading.ObservationLimits.not_knowable_trueReturn (NEW_PROOF)`
`AISafetyAtlas.Wireheading.ObservationLimits.returnOver_zeroEnv_complement (NEW_PROOF)` | | LAND-CRMDP-GRID-001 | Everitt et al. Theorem 11 over the source's own uniform reward grid | `RELATED` | `RewardGrid.everitt_theorem_eleven_gridClass`
`RewardGrid.toComplementedClass`
`RewardGrid.exists_max_gridReturn`
`RewardGrid.exists_min_gridReturn`
`RewardGrid.gridVal_gridRev`
`RewardGrid.gridVal_strictMono`
`RewardGrid.gridReturn_add_complement`
`RewardGrid.run_congr_observed`
`RewardGrid.halfMaximalRegretBound` | `AISafetyAtlas.Wireheading.RewardGrid.everitt_theorem_eleven_gridClass (NEW_PROOF)` | | LAND-FANO-001 | Fano's inequality at both printed constants, and its sharpness | | `AISafetyAtlas.InformationTheory.condEntropy_eq_error_split`
`AISafetyAtlas.InformationTheory.condEntropy_le_error_bound`
`AISafetyAtlas.InformationTheory.entropy_errorIndicator`
`AISafetyAtlas.InformationTheory.fano_of_log_le` | `AISafetyAtlas.InformationTheory.fano_of_log_le (NEW_PROOF)`
`AISafetyAtlas.InformationTheory.fano (NEW_PROOF)`
`AISafetyAtlas.InformationTheory.fano_unrestricted (NEW_PROOF)`
`AISafetyAtlas.InformationTheory.fano_of_embedding (NEW_PROOF)`
`AISafetyAtlas.InformationTheory.entropy_le_fano (NEW_PROOF)` | | LAND-OVERSIGHT-VARIETY-001 | Seeing and doing are independent oversight capacities | | `AISafetyAtlas.Oversight.cannotForce`
`AISafetyAtlas.Oversight.not_forces_of_card_lt`
`AISafetyAtlas.Oversight.Forces`
`AISafetyAtlas.Oversight.forces_of_constant_effect`
`AISafetyAtlas.Knowledge.Knowable` | `AISafetyAtlas.Oversight.not_forces_of_cannotForce (NEW_PROOF)`
`AISafetyAtlas.Oversight.exists_cannotForce_false_and_forces (NEW_PROOF)`
`AISafetyAtlas.Oversight.forces_of_constant_effect (BRIDGE)`
`AISafetyAtlas.Oversight.forces_of_constant_effect_of_not_knowable (BRIDGE)` | | LAND-KNOWENTROPY-001 | Knowability measured: zero conditional entropy, and Fano's floor on every decoder | | `AISafetyAtlas.Knowledge.Knowable`
`AISafetyAtlas.InformationTheory.condEntropy_comp_self_left`
`AISafetyAtlas.Knowledge.condEntropy_eq_zero_of_knowable`
`AISafetyAtlas.InformationTheory.le_errorProb`
`AISafetyAtlas.InformationTheory.condEntropy_le_condEntropy_of_isMarkovChain`
`AISafetyAtlas.InformationTheory.isMarkovChain_comp` | `AISafetyAtlas.Knowledge.condEntropy_eq_zero_of_knowable (NEW_PROOF)`
`AISafetyAtlas.Knowledge.not_knowable_of_condEntropy_ne_zero (NEW_PROOF)`
`AISafetyAtlas.Knowledge.le_errorProb_of_decoder (NEW_PROOF)` | | LAND-DPI-001 | The data-processing inequality, its equality case, and the conditioning counterexamples | | `AISafetyAtlas.InformationTheory.isMarkovChain_iff_measure_factorizes`
`AISafetyAtlas.InformationTheory.measure_preimage_inter_eq_tsum`
`AISafetyAtlas.InformationTheory.IsMarkovChain`
`AISafetyAtlas.InformationTheory.mutualInfo_chain_rule`
`AISafetyAtlas.InformationTheory.mutualInfo_sub_eq`
`AISafetyAtlas.InformationTheory.isMarkovChain_iff_condMutualInfo_eq_zero`
`AISafetyAtlas.InformationTheory.mutualInfo_le_of_isMarkovChain`
`AISafetyAtlas.InformationTheory.isMarkovChain_comp`
`AISafetyAtlas.InformationTheory.mutualInfo_chain_rule'` | `AISafetyAtlas.InformationTheory.isMarkovChain_iff_measure_factorizes_singleton (NEW_PROOF)`
`AISafetyAtlas.InformationTheory.isMarkovChain_iff_measure_factorizes (NEW_PROOF)`
`AISafetyAtlas.InformationTheory.measure_factorizes_of_isMarkovChain (NEW_PROOF)`
`AISafetyAtlas.InformationTheory.mutualInfo_le_of_isMarkovChain (NEW_PROOF)`
`AISafetyAtlas.InformationTheory.mutualInfo_eq_iff_isMarkovChain (NEW_PROOF)`
`AISafetyAtlas.InformationTheory.mutualInfo_comp_le (NEW_PROOF)`
`AISafetyAtlas.InformationTheory.condMutualInfo_le_mutualInfo (NEW_PROOF)` | | LAND-CAUSAL-PEARLCBN-001 | Pearl causal Bayesian networks as a condition on an interventional family | `RELATED` | — | `AISafetyAtlas.Causal.eq_family_of_isCausalBayesNetwork (NEW_PROOF)` | | LAND-CAUSAL-DECISIONNET-001 | Decision tasks as causal influence diagrams, with the decision and the utility as vertices | `RELATED` | — | `AISafetyAtlas.Causal.DecisionNetwork.mem_parents_utility_of_isUnmediated (NEW_PROOF)`
`AISafetyAtlas.Examples.Causal.DecisionNetwork.figIsUnmediated (NEW_PROOF)` | | LAND-CAUSAL-COLLISION-001 | Margins do not imply behavioral identifiability | `RELATED` | `AISafetyAtlas.Causal.Skeleton.MarginClass`
`AISafetyAtlas.Causal.Model.Δmix`
`AISafetyAtlas.Examples.Causal.collision_mix_edgeless_arrowXY`
`AISafetyAtlas.Examples.Causal.arrowXY_mem`
`AISafetyAtlas.Examples.Causal.arrowYX_mem`
`AISafetyAtlas.Examples.Causal.collision_mix_arrowXY_arrowYX`
`AISafetyAtlas.Examples.Causal.Model.factor_root`
`AISafetyAtlas.Examples.Causal.Model.factor_child`
`AISafetyAtlas.Causal.Model.jointProb_sum`
`AISafetyAtlas.Causal.Skeleton.BehaviorEq`
`AISafetyAtlas.Causal.Model.Δmask_empty`
`AISafetyAtlas.Causal.Model.Δmix_eq_sum`
`AISafetyAtlas.Causal.Model.sum_weighted_congr`
`AISafetyAtlas.Causal.Model.factor_hardInterventionProfile`
`AISafetyAtlas.Causal.hardInterventionProfile`
`AISafetyAtlas.Causal.Model.jointProb_fixProfile`
`AISafetyAtlas.Causal.fixProfile`
`AISafetyAtlas.Causal.Model.ancestors`
`AISafetyAtlas.Causal.Model.ParentClosed`
`AISafetyAtlas.Causal.Model.Δ`
`AISafetyAtlas.Examples.Causal.g`
`AISafetyAtlas.Causal.jointProb_sum_two`
`AISafetyAtlas.Examples.Causal.collision_edgeless_arrowXYb`
`AISafetyAtlas.Examples.Causal.other_mem`
`AISafetyAtlas.Causal.Model.notMem_parents_self` | `AISafetyAtlas.Examples.Causal.margin_class_not_identifiable (NEW_PROOF)`
`AISafetyAtlas.Examples.Causal.margin_class_not_identifiable_two_graphs (NEW_PROOF)`
`AISafetyAtlas.Examples.Causal.Model.jointProb_sum_shiftCollapse (NEW_PROOF)`
`AISafetyAtlas.Causal.Skeleton.behaviorEq_of_observed_eq_empty (NEW_PROOF)`
`AISafetyAtlas.Causal.Model.Δmix_congr (NEW_PROOF)`
`AISafetyAtlas.Causal.Model.jointProb_hardInterventionProfile (NEW_PROOF)`
`AISafetyAtlas.Causal.Model.Δ_fixProfile (NEW_PROOF)`
`AISafetyAtlas.Causal.Model.ancestors_eq_univ_iff (NEW_PROOF)`
`AISafetyAtlas.Examples.Causal.transform_identity_edgeless (NEW_PROOF)`
`AISafetyAtlas.Examples.Causal.Δ_eq_half_sub_joint (NEW_PROOF)`
`AISafetyAtlas.Examples.Causal.margin_class_not_identifiable_family (NEW_PROOF)`
`AISafetyAtlas.Examples.Causal.behaviorEq_has_teeth (NEW_PROOF)`
`AISafetyAtlas.Examples.Causal.mm2_shape (NEW_PROOF)` | | LAND-CAUSAL-DECISION-001 | Causal decision policies, regret, and identified-set radius | `RELATED` | `AISafetyAtlas.Causal.Policy.const`
`AISafetyAtlas.Causal.Model.Δmix`
`AISafetyAtlas.Causal.Model.regret_decomp`
`AISafetyAtlas.Causal.Model.fibreScore_le_best`
`AISafetyAtlas.Causal.Model.fibreScore_true_sub_false`
`AISafetyAtlas.Causal.Model.signPolicy`
`AISafetyAtlas.Causal.Model.signPolicy_eq_of_behaviorEq`
`AISafetyAtlas.Causal.Model.regret_signPolicy_eq_zero`
`AISafetyAtlas.Examples.Causal.margin_class_not_identifiable`
`AISafetyAtlas.Causal.inIdentifiedSet_zero_of_behaviorEq`
`AISafetyAtlas.Causal.Model.regret_nonneg`
`AISafetyAtlas.Causal.Model.ext`
`AISafetyAtlas.Causal.not_inIdentifiedSet_of_opposite_sign`
`AISafetyAtlas.Examples.Causal.high_mem`
`AISafetyAtlas.Causal.InIdentifiedSet`
`AISafetyAtlas.Causal.modelError`
`AISafetyAtlas.Causal.fibreRep` | `AISafetyAtlas.Causal.Model.value_eq (NEW_PROOF)`
`AISafetyAtlas.Causal.Model.value_const_sub (NEW_PROOF)`
`AISafetyAtlas.Causal.Model.regret_eq_zero_iff (NEW_PROOF)`
`AISafetyAtlas.Causal.Model.value_le_sign (NEW_PROOF)`
`AISafetyAtlas.Causal.inIdentifiedSet_zero_of_behaviorEq (NEW_PROOF)`
`AISafetyAtlas.Examples.Causal.margin_class_not_identifiable_shared_optimal (NEW_PROOF)`
`AISafetyAtlas.Causal.not_inIdentifiedSet_of_neg (NEW_PROOF)`
`AISafetyAtlas.Causal.modelError_eq_zero_iff (NEW_PROOF)`
`AISafetyAtlas.Examples.Causal.not_inIdentifiedSet_high (NEW_PROOF)`
`AISafetyAtlas.Examples.Causal.OneNodeClass.modelError_le_ten_mul (NEW_PROOF)`
`AISafetyAtlas.Examples.Causal.card_fibreRep_empty (NEW_PROOF)` | | LAND-CAUSAL-STRUCTURAL-001 | Structural causal models, causal influence diagrams, and materiality | `RELATED` | `AISafetyAtlas.Causal.SCM.exoJoint`
`AISafetyAtlas.Causal.SCIM.Policy`
`AISafetyAtlas.Causal.CID.IsSingleDecision`
`AISafetyAtlas.Causal.SCIM.optimalValue`
`exoLaw`
`observableLaw`
`measurable_exo`
`observableLaw_withPolicy_eq_of_notDownstream`
`AISafetyAtlas.Causal.SCIM.IsMaterial`
`AISafetyAtlas.Causal.SCIM.removeInfoLink`
`AISafetyAtlas.Examples.Causal.StructuralModel.figCut_optimalValue`
`AISafetyAtlas.Causal.CID` | `AISafetyAtlas.Causal.SCM.eval_eq_f (NEW_PROOF)`
`AISafetyAtlas.Causal.SCM.exoJoint_mul_prod (NEW_PROOF)`
`AISafetyAtlas.Causal.SCIM.policy_ext_single (NEW_PROOF)`
`AISafetyAtlas.Causal.SCIM.exists_isOptimalPolicy (NEW_PROOF)`
`AISafetyAtlas.Causal.SCIM.observableLaw_withPolicy_eq_of_notDownstream (NEW_PROOF)`
`AISafetyAtlas.Examples.Causal.StructuralModel.figSCIM_opinion_isMaterial (NEW_PROOF)`
`AISafetyAtlas.Examples.Causal.StructuralModel.figSCIM_policy_not_const (NEW_PROOF)`
`AISafetyAtlas.Examples.Causal.StructuralModel.utility_childless_has_teeth (NEW_PROOF)` | | LAND-SOV-TRULYPLAYABLE-001 | Truly playable effectivity functions, and the finite-domain corollary | `RELATED` | `Playable.trulyPlayable_of_finite`
`Playable.trulyPlayable_of_exists_minimal`
`not_trulyPlayable_cofiniteEff` | `AISafetyAtlas.Sovereignty.Playable.trulyPlayable_of_finite (NEW_PROOF)` | | LAND-SOV-PLAYABILITY-001 | Pauly's playability conditions, the easy direction, and the converse that fails | `RELATED` | `not_exists_gameForm_cofiniteEff`
`effectivity_playable`
`individualistic_iff_exists_dictator` | `AISafetyAtlas.Sovereignty.not_exists_gameForm_cofiniteEff (NEW_PROOF)` | | LAND-SOV-RETARGETABLE-001 | Retargetable decision-makers have orbit-level tendencies, up to theorem A.13 | `RELATED` | `MultiplyRetargetable.mostOrbit`
`SimplyRetargetable.mostOrbit`
`eu_determined_mostOrbit`
`mostOrbit_of_orbitConditions`
`mostOrbit_of_supersetCopies` | `AISafetyAtlas.Sovereignty.MultiplyRetargetable.mostOrbit (NEW_PROOF)`
`AISafetyAtlas.Sovereignty.eu_determined_mostOrbit (NEW_PROOF)` | | LAND-DEC-MDP-001 | The rewardless Markov decision process, and the run it induces | `RELATED` | `MDP`
`MDP.run`
`MDP.run_congr_obs` | `AISafetyAtlas.Decision.MDP.run_congr_obs (NEW_PROOF)` | | LAND-GOODHART-SELECTION-001 | Selection on a proxy: the inflated gap, and the region the link was never observed in | `RELATED` | `gap_selection_ge`
`gap_selection_gt`
`gap_selection_gaussianReal_gt`
`tail_integral_ge`
`selected_disjoint_observed`
`fits_underdetermined_off_observed`
`regime_prediction_error`
`regime_underdetermines` | `AISafetyAtlas.Goodhart.gap_selection_ge (NEW_PROOF)`
`AISafetyAtlas.Goodhart.Extremal.fits_underdetermined_off_observed (NEW_PROOF)` | | LAND-GOODHART-OVEROPT-001 | Optimizing a proxy over some of the attributes floors the rest | `RELATED` | `zhuang_hadfield_menell_theorem_one`
`proxyMax_unmentioned_eq_lowerBound`
`gap_le_of_unmentioned_eq_lowerBound` | `AISafetyAtlas.Goodhart.zhuang_hadfield_menell_theorem_one (NEW_PROOF)` | | LAND-SOV-POWER-001 | Peleg's game-form layer: alpha-effectivity, and the conditions it satisfies for free | `RELATED` | `forces_superadditive`
`Forces.mono_coalition`
`Forces.mono`
`forces_univ`
`Represents`
`Constitution`
`Constitution.induced`
`retainsFamily_of_represents`
`effectivityEq_of_retainsFamily_univ`
`principalCoalition`
`SOV1`
`sov1_of_retainsFamily_singleton`
`Constitution.Standing`
`represents_ofGameForm`
`Represents.superadditive`
`Represents.upwardClosed`
`Represents.surjective_outcome` | `AISafetyAtlas.Sovereignty.forces_superadditive (NEW_PROOF)`
`AISafetyAtlas.Sovereignty.retainsFamily_of_represents (NEW_PROOF)`
`AISafetyAtlas.Sovereignty.sov1_of_retainsFamily_singleton (NEW_PROOF)`
`AISafetyAtlas.Sovereignty.Represents.surjective_outcome (NEW_PROOF)` | | LAND-SOV-INDEPENDENCE-001 | The logical space of freedom, and the corner that cannot escape | `RELATED` | `not_independenceFree_of_universal_threat`
`not_republicanFree_of_impermissible_threat`
`republicanFree_of_independenceFree`
`liberalFree_of_independenceFree`
`free_of_free_not_moralized`
`free_of_free_robust` | `AISafetyAtlas.Sovereignty.Setting.not_independenceFree_of_universal_threat (NEW_PROOF)`
`AISafetyAtlas.Sovereignty.Setting.republicanFree_of_independenceFree (NEW_PROOF)` | | LAND-SOV-STEERING-001 | Stepwise retention is not authorship: locally safe steps that lose the original mandate | `RELATED` | `steer_isSteering`
`steer_adjacentSafe`
`steer_originalLost`
`steer_retains_coarsened`
`RetainsFamily.trans` | `AISafetyAtlas.Examples.Sovereignty.steer_isSteering (NEW_PROOF)` | | LAND-SOV-SERVICE-001 | Safety without service: a delegate that refuses everything keeps every guarantee it already satisfies | `RELATED` | `Inert`
`Inert.forces_iff`
`inert_retainsFamily_iff`
`Demandwise`
`Separating`
`separating_not_demandwise_of_inert`
`Refusal.Audit`
`Refusal.refusal_passes_safety`
`Refusal.refusal_fails_catalogue`
`Refusal.admitsRefusal`
`Refusal.exists_refusal_hole_of_admitsRefusal`
`Refusal.not_exists_refusal_hole_of_admitsRefusal_eq_false` | `AISafetyAtlas.Sovereignty.retainsFamily_and_not_demandwise (NEW_PROOF)`
`AISafetyAtlas.Sovereignty.Refusal.safety_suite_admits_a_refusal (BRIDGE)` | | LAND-SOV-QUANT-001 | Two quantifier orders: a response is not a policy, and two guarantees are not one | `RELATED` | `ForcesResp`
`forcesResp_of_forces`
`forces_iInter_of_shared_footprint`
`DemandwiseResp`
`demandwiseResp_of_demandwise` | `AISafetyAtlas.Sovereignty.forces_inter_of_shared_footprint (NEW_PROOF)` | | LAND-SOV-TRANSFER-001 | Resources, projections, and the refinement that carries a guarantee | `RELATED` | `Simulates`
`demandwise_of_simulates`
`ForcesWithin`
`ForcesWithin.mono_resources`
`forces_map_iff_forces_preimage` | `AISafetyAtlas.Sovereignty.forces_of_simulates (NEW_PROOF)` | | LAND-SOV-CATALOGUE-001 | Passing every demand separately is not being able to run | `RELATED` | `DemandwiseUniform`
`demandwise_of_demandwiseUniform`
`not_forces_of_disjoint_of_shared`
`not_demandwiseUniform_of_disjoint`
`retainsFamily_refl`
`Conformity.Assessment`
`Conformity.PassesEach`
`Conformity.Operable`
`Conformity.passesEach_of_operable`
`Conformity.operable_meets_all_at_once`
`Conformity.conflicting_requirements_are_not_operable`
`Conformity.not_operable_of_subset_not_operable` | `AISafetyAtlas.Sovereignty.demandwise_iff_exists_selector (NEW_PROOF)`
`AISafetyAtlas.Sovereignty.Conformity.passes_every_check_and_not_operable (BRIDGE)` | | LAND-SOV-AUDIT-001 | What a channel can certify, and what it only has to be good enough to act on | `RELATED` | `UniformDecision`
`residualFree_iff_factors`
`auditable_iff_exists_detector`
`not_exists_recovery_of_collision`
`selectionAuditable_iff_separates` | `AISafetyAtlas.Sovereignty.exists_uniformDecision_iff (NEW_PROOF)` | | LAND-SOV-COMM-001 | Zero-error communication against an adversary is disjoint forceable regions | `RELATED` | `TransmitsZeroError`
`TransmitsZeroError.of_comp` | `AISafetyAtlas.Sovereignty.transmitsZeroError_iff_exists_code (NEW_PROOF)` | | LAND-SOV-CONST-001 | An amendment chain is evidence about the amendment rule and nothing else | `RELATED` | `AuthorizedFrom`
`authorizedFrom_of_stepwise`
`AuthorizedFrom.mono`
`AmendmentLog.ChangeLog`
`AmendmentLog.log_shows_only_rule_compliance`
`AmendmentLog.the_rule_carries_the_assurance` | `AISafetyAtlas.Sovereignty.authorizedFrom_of_total (NEW_PROOF)`
`AISafetyAtlas.Sovereignty.AmendmentLog.unbroken_chain_is_not_a_constraint (BRIDGE)` | | LAND-SOV-DISTURB-001 | Reaching every state is not holding one: the quantifier a rank condition hides | `RELATED` | `Plant`
`Plant.RobustInput`
`Plant.reachesEvery_iff_surjective`
`isControllable_iff_reachesEvery`
`Plant.robustReachesEvery_of_disturbance_constant` | `AISafetyAtlas.Sovereignty.Plant.exists_robustInput_iff (NEW_PROOF)` | | LAND-SOV-AUTH-001 | Authority is an input, and the links it does not come with | `RELATED` | `not_authority_implies_control`
`not_control_implies_authority`
`Veto`
`Dominates`
`not_forces_of_veto`
`not_dominates_of_controlled`
`exists_verified_untrue`
`exists_all_four_combinations`
`ShutdownChannel.RelayedCommand`
`ShutdownChannel.run_delivered`
`ShutdownChannel.principal_cannot_force`
`ShutdownChannel.relay_forces_idle`
`ShutdownChannel.undeclinable_iff_inert`
`Attestation.Record`
`Attestation.attested_does_not_transfer`
`Attestation.no_property_implies_another`
`DelegationChain.not_forces_of_free_coordinate`
`DelegationChain.forces_both_of_shared_commitment` | `AISafetyAtlas.Sovereignty.not_exists_label_agreeing_with_both (NEW_PROOF)`
`AISafetyAtlas.Sovereignty.ShutdownChannel.obedience_does_not_give_authority (BRIDGE)`
`AISafetyAtlas.Sovereignty.Attestation.attestation_is_not_the_claim (BRIDGE)`
`AISafetyAtlas.Sovereignty.Attestation.properties_are_independent (BRIDGE)`
`AISafetyAtlas.Sovereignty.DelegationChain.power_over_a_matter_does_not_compose (BRIDGE)` | | LAND-SOV-VALUE-001 | Values on a game form, with sure winning sitting inside them | `RELATED` | `OutcomeLaw`
`OutcomeLaw.lowerValue`
`OutcomeLaw.upperValue`
`OutcomeLaw.lowerValue_le_upperValue`
`OutcomeLaw.opponentLowerValue_eq_one_sub_upperValue`
`spliceProfile`
`forces_iff_forall_spliceProfile` | `AISafetyAtlas.Sovereignty.lowerValue_diracLaw_eq_one_iff (NEW_PROOF)` | | LAND-SOV-INFL-001 | Influence is a capacity, and it is not power | `RELATED` | `eventGap`
`eventGap_eq_zero_iff`
`eventGap_map_le`
`influenceCapacity`
`supportEffectivity`
`supportEffectivity_congr` | `AISafetyAtlas.Sovereignty.influenceCapacity_eq_zero_iff (NEW_PROOF)` | | LAND-SOV-SAFETYGAME-001 | Holding a system inside a set forever, and getting back inside a budget | `RELATED` | `SafetyGame`
`SafetyGame.cpre`
`SafetyGame.safetyKernel`
`SafetyGame.subset_safetyKernel`
`SafetyGame.recovery_reaches`
`SafetyGame.maintains_prodGame`
`SafetyGame.danger_le_of_rate` | `AISafetyAtlas.Sovereignty.SafetyGame.mem_safetyKernel_iff_exists_maintaining (NEW_PROOF)` | | LAND-SOV-BELIEF-001 | Deciding on one's own beliefs, while another party writes them | `RELATED` | `DoxasticAgent`
`DoxasticAgent.channel`
`DoxasticAgent.sender_forces`
`DoxasticAgent.beliefDecisive_not_sovereign` | `AISafetyAtlas.Sovereignty.DoxasticAgent.mem_of_agent_forces (NEW_PROOF)` | | LAND-SOV-EVIDENCE-001 | What a decision can achieve on the evidence it has | `RELATED` | `actionLaw`
`actionLaw_congr`
`exists_measure_le_inv_of_disjoint`
`success_add_le_one_add_eventGap`
`eventGap_ge_of_success` | `AISafetyAtlas.Sovereignty.exists_success_le_inv (NEW_PROOF)` | | LAND-SOV-COGSOV-001 | The cognitive-sovereignty predicate, and what belief change does not prove | `RELATED` | `CogSov`
`cogSov_of_witness`
`not_cogSov` | `AISafetyAtlas.Sovereignty.magnitude_does_not_decide_authorship (NEW_PROOF)` | | LAND-SOV-EMPOWER-001 | Empowerment of a deterministic channel is the capacity of its range | `RELATED` | `empowerment`
`mutualInfo_id_eq_entropy`
`mutualInfo_le_log_card_range`
`isUniform_section`
`empowerment_eq_channelCapacity_range` | `AISafetyAtlas.Sovereignty.empowerment_eq_log_card_range (NEW_PROOF)` | | LAND-SOV-MINIMAX-001 | Mixed strategies close the gap a pure commitment leaves | `RELATED` | `mixed`
`payoff`
`exists_mixed_saddlePoint` | `AISafetyAtlas.Sovereignty.exists_mixed_value (NEW_PROOF)` | | LAND-SOV-OUTNUMBERED-001 | Being outnumbered is not being outmatched | | `AdversaryLe`
`cpre_subset_of_adversaryLe`
`not_forces_of_veto_outside` | `AISafetyAtlas.Sovereignty.safetyKernel_subset_of_adversaryLe (NEW_PROOF)` | | LAND-VERIF-AGENTBEHAVIOR-001 | No total verifier for a nontrivial behavioural safety specification | `RELATED` | `no_behavioral_safety_verifier` | `AISafetyAtlas.Verification.AgentBehavior.no_behavioral_safety_verifier (NEW_PROOF)` | | LAND-LINSYS-001 | Kalman and Hautus: when a linear system's state is determined, and when it can be driven | `RELATED` | `isObservable_iff_hautus`
`isControllable_iff_hautus`
`isObservable_iff_observabilityMatrix_rank_eq`
`isControllable_iff_controllabilityMatrix_rank_eq`
`isControllable_iff_isObservable_transpose` | `AISafetyAtlas.LinearSystems.isObservable_iff_hautus (REFERENCE)` | | LAND-SOV-VOTINGPOWER-001 | A zero power index names a null player only where the marginals cannot cancel | `RELATED` | `SimpleGame`
`SimpleGame.shapleyShubik`
`SimpleGame.sum_weighted_eq_zero_iff`
`SimpleGame.banzhafRaw`
`SimpleGame.Pivotal` | `AISafetyAtlas.Sovereignty.SimpleGame.shapleyShubik_eq_zero_iff (NEW_PROOF)`
`AISafetyAtlas.Sovereignty.SimpleGame.banzhafRaw_eq_swings_div (NEW_PROOF)` | | LAND-SOV-CAPABILITY-001 | A maintenance floor for fallback capability, and why assisted output does not report it | `RELATED` | `AISafetyAtlas.Sovereignty.AffineCapability`
`AISafetyAtlas.Sovereignty.MaintenanceFloor`
`AISafetyAtlas.Knowledge.not_knowable_of_collision`
`AISafetyAtlas.Sovereignty.assistedOutput`
`AISafetyAtlas.Sovereignty.Forces` | `AISafetyAtlas.Sovereignty.maintenanceFloor_of_practice_floor (NEW_PROOF)`
`AISafetyAtlas.Sovereignty.fallback_not_knowable_from_assistedOutput (NEW_PROOF)`
`AISafetyAtlas.Sovereignty.exists_output_rise_with_fallback_fall (NEW_PROOF)`
`AISafetyAtlas.Sovereignty.Enlarges.forces (NEW_PROOF)` | | LAND-EVAL-BLINDSPOT-001 | What an evaluation that scores runs one at a time can and cannot see | | `AISafetyAtlas.Knowledge.Knowable`
`AISafetyAtlas.Knowledge.not_knowable_of_collision` | `AISafetyAtlas.Compositional.Hyperproperties.Evaluation.traceProperty_knowable_of_score_decides (BRIDGE)`
`AISafetyAtlas.Compositional.Hyperproperties.Evaluation.sampling_misses_subsingleton (BRIDGE)` | | LAND-AUDIT-REGISTRY-001 | Audit registries along a value chain: what publishing declarations can settle | | `AISafetyAtlas.Oversight.JointObservation.Covers`
`AISafetyAtlas.Knowledge.not_knowable_of_collision` | `AISafetyAtlas.Oversight.JointObservation.consortium_covers_of_registry_covers (BRIDGE)`
`AISafetyAtlas.Oversight.JointObservation.not_registry_covers_of_emit_collision (BRIDGE)` | | LAND-ACCESS-ORDER-001 | Forms of model access: three points on the informativeness order, and what no methodology repairs | | `AISafetyAtlas.Knowledge.Determines.trans`
`AISafetyAtlas.Knowledge.not_knowable_comp`
`AISafetyAtlas.Knowledge.exists_witness_of_not_knowable` | `AISafetyAtlas.Knowledge.Access.whiteBox_determines_blackBox (BRIDGE)`
`AISafetyAtlas.Knowledge.Access.no_blackBox_methodology (BRIDGE)`
`AISafetyAtlas.Knowledge.Access.exists_indistinguishable_behaviour (BRIDGE)` | | LAND-GOODHART-REGTARGET-001 | Regulatory targets: the bar certifies exactly the systems its evidence never covered | | `AISafetyAtlas.Goodhart.Extremal.selected_disjoint_observed`
`AISafetyAtlas.Goodhart.Extremal.fits_underdetermined_off_observed` | `AISafetyAtlas.Goodhart.RegulatoryTarget.certified_systems_were_never_examined (BRIDGE)`
`AISafetyAtlas.Goodhart.RegulatoryTarget.risk_unconstrained_on_certified (BRIDGE)`
`AISafetyAtlas.Goodhart.RegulatoryTarget.raising_the_bar_does_not_help (BRIDGE)` | | LAND-SOV-ASSESSMENT-001 | Measuring unaided capability: withdrawal testing is forced, not chosen | | `AISafetyAtlas.Knowledge.not_knowable_comp`
`AISafetyAtlas.Knowledge.not_knowable_of_collision`
`AISafetyAtlas.Sovereignty.fallback_not_knowable_from_assistedOutput` | `AISafetyAtlas.Sovereignty.CapabilityAssessment.no_procedure_on_output_recovers_fallback (BRIDGE)`
`AISafetyAtlas.Sovereignty.CapabilityAssessment.protocols_are_incomparable (BRIDGE)`
`AISafetyAtlas.Sovereignty.CapabilityAssessment.withdrawal_settles_and_no_output_procedure_does (BRIDGE)` | | LAND-VERIF-FULLACCESS-001 | Full access to the code: Rice bounds the behavioral half and nothing else | | `AISafetyAtlas.Computability.rice_code_iff`
`Primrec.eq`
`PrimrecPred.computablePred` | `AISafetyAtlas.Verification.FullAccess.no_fullAccessVerifier_of_extensional (BRIDGE)`
`AISafetyAtlas.Verification.FullAccess.fullAccessVerifier_exactArtifact (BRIDGE)`
`AISafetyAtlas.Verification.FullAccess.access_is_not_what_separates_them (BRIDGE)` | | LAND-AUDIT-LAG-001 | What an audit certifies: the audited version, not the deployed one | | `AISafetyAtlas.Knowledge.Temporal.KnowableFrom`
`AISafetyAtlas.Knowledge.not_knowable_of_collision`
`AISafetyAtlas.Knowledge.Temporal.knowableFrom_mono`
`AISafetyAtlas.Knowledge.Temporal.not_knowableAt_of_collisionAt` | `AISafetyAtlas.Knowledge.Audit.audit_certifies_audited_not_deployed (BRIDGE)`
`AISafetyAtlas.Knowledge.Audit.later_audit_does_not_close_the_gap (BRIDGE)` | | LAND-INCIDENT-COUNT-001 | Counting AI incidents: the number a regime publishes is a property of its filing schema | | `AISafetyAtlas.Knowledge.not_knowable_of_collision`
`AISafetyAtlas.Knowledge.IncidentCount.count_not_determined_of_collision`
`AISafetyAtlas.Knowledge.Knowable`
`AISafetyAtlas.Knowledge.knowable_iff_no_collision` | `AISafetyAtlas.Knowledge.IncidentCount.count_not_determined_of_collision (WRAPPER)`
`AISafetyAtlas.Knowledge.IncidentCount.count_is_not_a_measurement (BRIDGE)`
`AISafetyAtlas.Knowledge.IncidentCount.schema_fixes_the_count (WRAPPER)`
`AISafetyAtlas.Knowledge.IncidentCount.knowable_of_report_carries_count (WRAPPER)` | | LAND-KNOW-UNIFORM-001 | Acting acceptably without identifying the state: the uniform decision boundary | `RELATED` | `AISafetyAtlas.Knowledge.UniformlyActionable`
`AISafetyAtlas.Knowledge.FibrewiseAgreeable`
`AISafetyAtlas.Knowledge.Knowable`
`AISafetyAtlas.Knowledge.uniformlyActionable_iff_fibrewiseAgreeable`
`AISafetyAtlas.Knowledge.PairwiseAgreeable` | `AISafetyAtlas.Knowledge.uniformlyActionable_iff_fibrewiseAgreeable (NEW_PROOF)`
`AISafetyAtlas.Knowledge.knowable_iff_uniformlyActionable (WRAPPER)`
`AISafetyAtlas.Knowledge.not_uniformlyActionable_iff_exists_unservable (BRIDGE)`
`AISafetyAtlas.Knowledge.uniformlyActionable_of_pairwiseAgreeable_of_card_le_two (NEW_PROOF)` | | LAND-SOV-STABILITY-001 | Keiding's cycle, stated at this repository's effectivity families | `EXACT` | `AISafetyAtlas.Sovereignty.Cycle`
`AISafetyAtlas.Sovereignty.Acyclic`
`AISafetyAtlas.Sovereignty.effectivity` | `AISafetyAtlas.Sovereignty.not_gameFormAcyclic_of_cycle (NEW_PROOF)`
`AISafetyAtlas.Sovereignty.gameFormAcyclic_iff (BRIDGE)` | | LAND-SOV-DEONTIC-001 | May, may not, can, and is empowered to are four different things | `RELATED` | `AISafetyAtlas.Sovereignty.InstitutionalSetting.Separated`
`AISafetyAtlas.Sovereignty.OughtImpliesCan`
`Enforcement.Regime`
`Enforcement.Detectable`
`Enforcement.Enforces`
`Enforcement.unenforceable_of_indistinguishable`
`Enforcement.not_detectable_of_indistinguishable`
`Enforcement.detectable_of_enforcement` | `AISafetyAtlas.Sovereignty.NormSystem.forbidden_iff_not_permitted_iff (NEW_PROOF)`
`AISafetyAtlas.Sovereignty.InstitutionalSetting.exists_empowered_possible_not_permitted (NEW_PROOF)`
`AISafetyAtlas.Sovereignty.oughtImpliesCan_does_not_give_permission (NEW_PROOF)`
`AISafetyAtlas.Sovereignty.Enforcement.undetectable_norm_is_unenforceable (BRIDGE)` | | LAND-SOV-INSTITUTION-001 | A Horn derivation is not counts-as, and the proof is two theorems | `RELATED` | `AISafetyAtlas.Sovereignty.CountsAs`
`AISafetyAtlas.Sovereignty.Derives`
`AISafetyAtlas.Sovereignty.InstitutionalSetting.Separated` | `AISafetyAtlas.Sovereignty.countsAs_validates_refl_and_trans (NEW_PROOF)`
`AISafetyAtlas.Sovereignty.no_authority_from_ungrounded_cycles (NEW_PROOF)`
`AISafetyAtlas.Sovereignty.Institution.exists_recognized_not_authorized (NEW_PROOF)` | | LAND-BELLMAN-BDD-001 | The bounded fixed point: a discounted policy value without a finite state space | `RELATED` | `vPiBdd`
`vPiBdd_bellman`
`vPiBdd_unique`
`bddFixedPoint`
`existsUnique_bdd_fixedPoint`
`abs_sub_le_of_monotone_discounting` | `AISafetyAtlas.Decision.vPiBdd_eq_vPi (REFERENCE)` | | LAND-GOODHART-HACKABILITY-001 | Hackability: two reward functions that disagree about which policy is better | `RELATED` | `visitCount`
`actionEmbed`
`J`
`J_linear`
`sum_stateOcc_eq`
`Hackable`
`Unhackable`
`Simplifies`
`unhackable_not_transitive`
`unhackable_of_simplifies_common`
`simplifies_of_trivial` | `AISafetyAtlas.Decision.J_linear (NEW_PROOF)`
`AISafetyAtlas.Goodhart.unhackable_of_simplifies_common (NEW_PROOF)` | The generated declaration-presence checks live in [`AISafetyAtlas/Examples/Registry.lean`](../../AISafetyAtlas/Examples/Registry.lean). The hand-written `PublicAPI` examples separately protect the intended theorem signatures and root-import usability. ## Reproduced external formalization records | ID | Registry result | Framework | Declaration | Relationship | Reproduction command | |---|---|---|---|---|---| | BY-007 | Arrow's impossibility theorem | Isabelle/HOL | `Arrow` | EQUIVALENT | `scripts/reproduce_isabelle.sh arrow` | | BY-007 | Arrow's impossibility theorem | Isabelle/HOL | `dictator` | EQUIVALENT | `scripts/reproduce_isabelle.sh arrow` | | BY-012 | Rice's theorem | Isabelle/HOL | `Rice_2` | EQUIVALENT | `scripts/reproduce_isabelle.sh rice` | | LAND-GS-001 | Gibbard–Satterthwaite theorem | Isabelle/HOL | `Gibbard_Satterthwaite` | — | `scripts/reproduce_isabelle.sh arrow` | | LAND-NFL-001 | No-free-lunch theorem for machine learning (Shalev-Shwartz–Ben-David §5.1) | Isabelle/HOL | `no_free_lunch_ML` | RELATED | `scripts/reproduce_isabelle.sh nfl` | | LAND-PE-001 | Parfit mere addition / conditional normative reasoning (Åqvist E) | Isabelle/HOL | `mere_addition` | RELATED | `scripts/reproduce_isabelle.sh condnorm` | | LAND-DL-001 | Deep vs shallow network capacity (Cohen–Bentkamp) | Isabelle/HOL | `fundamental_theorem_network_capacity` | RELATED | `scripts/reproduce_isabelle.sh deep-learning` | | LAND-CL-001 | Chandy-Lamport distributed snapshot — termination, correctness, stable property detection | Isabelle/HOL | `snapshot_algorithm_must_terminate`
`snapshot_algorithm_is_correct`
`Stable_Property_Detection` | — | `scripts/reproduce_isabelle.sh chandy-lamport` | Additional reproduced variants and adjacent developments, including vNM expected utility, remain provenance rather than extra survey coverage; see [`external-formalizations.md`](../provenance/external-formalizations.md) and the [landscape index](landscape-index.md). ## Discovery coverage All 44 rows have a **baseline classical six-corpus** search (Mathlib, Isabelle AFP, Rocq Undecidability, HOL4, HOL Light, Agda stdlib); 13 rows produced raw candidate-file hits. That pass is **scoped** negative/positive evidence for those corpora only — it does not search third-party Lean packages (Foundation, KolmogorovMathlib, SocialChoiceLean, DASH, …). Manually discovered package leads are recorded as `candidate_formalizations` on a claim row, or as an artifact row when the formalization stands on its own account. Candidate hits are discovery evidence, not verified formalizations. Relationship labels are `EXACT`, `EQUIVALENT`, `RELATED`, `DEPENDENCY_ONLY`, and `UNCLEAR`. An AI-safety interpretation remains `HUMAN_REVIEW` unless it has been separately defined and reviewed.