# Landscape Index First-class atlas formalizations and public Lean surface recorded in [`registry.yaml`](../../registry.yaml) — results the workbench develops, reproduces, or exposes on its own account. Statement-match grades are reported per catalogued source and are not affected by entries here. Narrative provenance remains in [`external-formalizations.md`](../provenance/external-formalizations.md). How these results stand to one another, and which are characterizations rather than point impossibilities, is in [`relations.md`](relations.md). | ID | Name | Framework | Atlas / source declarations | Root import | Reproduction | |---|---|---|---|---|---| | LAND-WOLPERT-KNOW-DEFECTS-001 | Countermodels to Wolpert 2018 epistemic claims | Lean | `AISafetyAtlas.Inference.corollary21_ii_repaired` | yes | `lake build AISafetyAtlas.Inference.PhysicalKnowledge.Event AISafetyAtlas.Examples.Inference.PhysicalKnowledge.Epistemic AISafetyAtlas.Examples.Inference.PhysicalKnowledge.Event` | | LAND-ATTR-001 | Attribution impossibility (DASH trilemma) | Lean | `AISafetyAtlas.Explainability.attribution_impossibility`
`AISafetyAtlas.Explainability.attribution_impossibility_weak` | yes | `lake build AISafetyAtlas (vendored axiom-free trilemma)` | | LAND-GS-001 | Gibbard–Satterthwaite theorem | Isabelle/HOL | `Gibbard_Satterthwaite` | no | `scripts/reproduce_isabelle.sh arrow` | | LAND-GS-002 | Gibbard–Satterthwaite theorem (Lean / SocialChoiceLean) | Lean | `AISafetyAtlas.SocialChoice.gibbard_satterthwaite` | yes | `lake build AISafetyAtlas; python3 scripts/check_print_axioms.py` | | LAND-NFL-001 | No-free-lunch theorem for machine learning (Shalev-Shwartz–Ben-David §5.1) | Isabelle/HOL | `no_free_lunch_ML` | no | `scripts/reproduce_isabelle.sh nfl` | | LAND-PE-001 | Parfit mere addition / conditional normative reasoning (Åqvist E) | Isabelle/HOL | `mere_addition` | no | `scripts/reproduce_isabelle.sh condnorm` | | LAND-DL-001 | Deep vs shallow network capacity (Cohen–Bentkamp) | Isabelle/HOL | `fundamental_theorem_network_capacity` | no | `scripts/reproduce_isabelle.sh deep-learning` | | LAND-VNM-001 | von Neumann–Morgenstern expected utility | Lean | `vNM.vNM_theorem` | no | `scripts/reproduce_vnm.sh` | | LAND-TCS-ARROW-001 | Fourier-analytic Arrow theorem (TCSLib) | Lean | `ArrowTheorem.arrow_theorem` | no | — | | LAND-DEBATE-001 | Doubly-efficient debate correctness (Brown-Cohen–Irving–Piliouras 2023) | Lean | `AISafetyAtlas.Oversight.Debate.alice_fast`
`AISafetyAtlas.Oversight.Debate.bob_fast`
`AISafetyAtlas.Oversight.Debate.completeness`
`AISafetyAtlas.Oversight.Debate.correctness`
`AISafetyAtlas.Oversight.Debate.soundness`
`AISafetyAtlas.Oversight.Debate.vera_fast` | no | `scripts/reproduce_debate.sh` | | LAND-DEBATE-001 | Doubly-efficient debate correctness (Brown-Cohen–Irving–Piliouras 2023) | Lean | `AISafetyAtlas.Oversight.Debate.alice_fast`
`AISafetyAtlas.Oversight.Debate.bob_fast`
`AISafetyAtlas.Oversight.Debate.completeness`
`AISafetyAtlas.Oversight.Debate.correctness`
`AISafetyAtlas.Oversight.Debate.soundness`
`AISafetyAtlas.Oversight.Debate.vera_fast` | no | `scripts/reproduce_debate.sh --in-tree` | | LAND-HYPER-001 | Trace-property and hyperproperty classes (Alpern–Schneider decomposition; Clarkson–Schneider hierarchy) | Rocq/Coq | `decomposition_theorem`
`safety_closed`
`liveness_dense`
`decomposition_safety_dense`
`Safety`
`Liveness`
`hprop`
`SSC`
`HSafe`
`H2Safe`
`HLiv` | no | `Exact build attempted 2026-07-28 with coqorg/coq:8.9.1@sha256:8e26609c5450aa795af6917cf169a65ab3952ba666d1b0c90e6b0179314a1149 and coqorg/coq:8.20@sha256:e50d77c4c5a9aa0d76ae1b343d79c5f922da3a75054b79c5dc635895438e4674: both fail at InternalNondet.v line 8 (`From Stdlib Require Import List`) after compiling the principal topology/property files.` | | LAND-HYPER-002 | k-safety self-composition and hyperproperty decomposition | Lean | `AISafetyAtlas.Compositional.Hyperproperties.k_safety_iff_finite_self_composition` | yes | `lake build AISafetyAtlas.Compositional.Hyperproperties AISafetyAtlas.Compositional.Hyperproperties.PrefixTopology AISafetyAtlas.Compositional.Hyperproperties.Product` | | LAND-ANGLUIN-001 | Port-labelled anonymous networks, views, and automorphisms | Lean | `AISafetyAtlas.Compositional.Networks.runFor_eq_of_view_eq` | yes | `lake build AISafetyAtlas.Compositional.Networks AISafetyAtlas.Examples.SixTargets` | | LAND-PREF-KNOW-001 | Reward unidentifiability as a knowability obstruction | Lean | `AISafetyAtlas.Preference.knowable_reward_of_isEmpty_state`
`AISafetyAtlas.Preference.not_knowable_reward` | yes | `lake build AISafetyAtlas.Preference.Knowability AISafetyAtlas.Examples.Preference.Knowability; python3 scripts/check_print_axioms.py` | | LAND-COMP-TRACE-001 | A network's runs as a trace system | Lean | `AISafetyAtlas.Compositional.Networks.not_electsLeader_of_fixedPointFree`
`AISafetyAtlas.Compositional.Networks.realizes_systemOf` | yes | `lake build AISafetyAtlas.Compositional.NetworkTraces; python3 scripts/check_print_axioms.py` | | LAND-HYPER-KNOW-001 | Finite-observation safety as a knowability factorization | Lean | `AISafetyAtlas.Compositional.Hyperproperties.knowable_of_isSafetyPredicate`
`AISafetyAtlas.Compositional.Hyperproperties.not_isSafetyPredicate_of_realizedSet_collision` | yes | `lake build AISafetyAtlas.Compositional.Hyperproperties.Knowability; python3 scripts/check_print_axioms.py` | | LAND-CAUSAL-KNOW-001 | Behavioural identifiability as a knowability factorization | Lean | `AISafetyAtlas.Causal.behaviorEq_iff_behavior_eq`
`AISafetyAtlas.Causal.exists_behaviorEq_pair_of_not_knowable` | yes | `lake build AISafetyAtlas.Causal.Knowability; python3 scripts/check_print_axioms.py` | | LAND-COMP-KNOW-001 | The Angluin view as a knowability factorization | Lean | `AISafetyAtlas.Compositional.Networks.knowable_runFor`
`AISafetyAtlas.Compositional.Networks.sameView_iff_view_eq` | yes | `lake build AISafetyAtlas.Compositional.Knowability AISafetyAtlas.Examples.Compositional.Knowability; python3 scripts/check_print_axioms.py` | | LAND-RECT-001 | Rectangle, exchange, and unary-contract equivalences | Lean | `AISafetyAtlas.Compositional.rectangle_iff_exchange_closed` | yes | `lake build AISafetyAtlas.Compositional.Rectangularity` | | LAND-WIRE-OBJ-001 | Ring-Orseau objective factorization | Lean | `AISafetyAtlas.Wireheading.AgentEquations.value_eq_of_agree_on_window` | yes | `lake build AISafetyAtlas.Wireheading.Objective AISafetyAtlas.Wireheading.AgentEquations AISafetyAtlas.Wireheading.DelusionBox AISafetyAtlas.Wireheading.SelfMod AISafetyAtlas.Examples.Wireheading.DelusionBox AISafetyAtlas.Examples.Wireheading.SelfMod` | | LAND-WIRE-AGENTHISTORY-001 | Ring-Orseau histories on the Decision carrier | Lean | `AISafetyAtlas.Wireheading.AgentEquations.value_runHistory_eq_of_agree_on_window` | yes | `lake build AISafetyAtlas.Wireheading.AgentHistory AISafetyAtlas.Examples.Wireheading.AgentEquations` | | LAND-WIRE-GOALCARRIER-001 | Self-modification on the Decision carrier | Lean | `AISafetyAtlas.Wireheading.GoalPreservation.scheduleModel_optimalAt` | yes | `lake build AISafetyAtlas.Wireheading.GoalPreservationCarrier AISafetyAtlas.Examples.Wireheading.GoalPreservationCarrier` | | LAND-PREF-TRAJECTORY-001 | Preference unidentifiability at a trajectory | Lean | `AISafetyAtlas.Preference.consistent_rewards_of_trajectory_eq_univ` | yes | `lake build AISafetyAtlas.Preference.Trajectory AISafetyAtlas.Examples.Preference.Trajectory` | | LAND-VERIF-ROBOTRUN-001 | A verified behaviour, run | Lean | `AISafetyAtlas.Verification.Robot.alwaysSatisfies_run` | yes | `lake build AISafetyAtlas.Verification.RobotRun AISafetyAtlas.Examples.Verification.RobotRun` | | LAND-COMP-RUNTRACES-001 | The trace system a policy set generates | Lean | `AISafetyAtlas.Compositional.Hyperproperties.exists_bad_trajectories_of_isKSafety` | yes | `lake build AISafetyAtlas.Compositional.TraceSystem AISafetyAtlas.Examples.Compositional.TraceSystem` | | LAND-GOAL-001 | Finite-percept on-policy goal-preservation induction step | Lean | `AISafetyAtlas.Wireheading.GoalPreservationSource.Model.selected_matches_initial` | yes | `lake build AISafetyAtlas.Wireheading.GoalPreservation AISafetyAtlas.Wireheading.GoalPreservationSource` | | LAND-VRL-001 | Value reinforcement learning and the consistency-preserving constraint | Lean | `AISafetyAtlas.Wireheading.ValueLearning.Beliefs.vrlValue_of_isCP` | yes | `lake build AISafetyAtlas.Wireheading.ValueLearning AISafetyAtlas.Examples.Wireheading.ValueLearning` | | LAND-GOAL-002 | Theorem 16 equation (13) over the whole trajectory, without naming surjectivity | Lean | `AISafetyAtlas.Wireheading.GoalPreservationRun.Model.equation_thirteen` | yes | `lake build AISafetyAtlas.Wireheading.GoalPreservationRun AISafetyAtlas.Examples.Wireheading.GoalPreservationRun` | | LAND-JOINTOBS-001 | Coalition-indexed joint observation and the emitted-interface coverage boundary | Lean | `AISafetyAtlas.Oversight.JointObservation.covers_iff_no_collision` | yes | `lake build AISafetyAtlas.Oversight.JointObservation AISafetyAtlas.Examples.Oversight.JointObservation.Procurement AISafetyAtlas.Examples.Oversight.JointObservation.Portfolio` | | LAND-SELFREF-001 | The self-model as a component of the state it models | Lean | `AISafetyAtlas.Knowledge.SelfReference.card_rest_le_one_of_selfComplete`
`AISafetyAtlas.Knowledge.SelfReference.not_selfComplete_of_two_rest`
`AISafetyAtlas.Knowledge.SelfReference.selfComplete_iff_subsingleton_rest` | yes | `lake build AISafetyAtlas.Knowledge.SelfReference` | | LAND-ACCUM-001 | Window ambiguity: accumulation bounds over a set of targets | Lean | `AISafetyAtlas.Knowledge.ambiguity_le_of_evidenceMonotone`
`AISafetyAtlas.Knowledge.ambiguity_le_pairTarget_left`
`AISafetyAtlas.Knowledge.ambiguity_le_pairTarget_of_evidenceMonotone`
`AISafetyAtlas.Knowledge.ambiguity_le_pairTarget_right`
`AISafetyAtlas.Knowledge.ambiguity_pairTarget_le_mul`
`AISafetyAtlas.Knowledge.not_knowable_pairTarget_of_not_knowable` | yes | `lake build AISafetyAtlas.Knowledge.Accumulation` | | LAND-AMBIG-001 | Finite fibre ambiguity and the counting obstruction | Lean | `AISafetyAtlas.Knowledge.ambiguity_le_of_comp`
`AISafetyAtlas.Knowledge.card_image_le_of_knowable`
`AISafetyAtlas.Knowledge.knowable_iff_ambiguity_le_one`
`AISafetyAtlas.Knowledge.not_knowable_of_card_lt` | yes | `lake build AISafetyAtlas.Knowledge.Ambiguity` | | LAND-TEMPORAL-001 | Time-indexed knowability, contemporaneous collisions, and delayed knowledge | Lean | `AISafetyAtlas.Knowledge.Temporal.collisionAt_of_not_knowableAt`
`AISafetyAtlas.Knowledge.Temporal.knowableFrom_mono`
`AISafetyAtlas.Knowledge.Temporal.not_knowableAt_of_collisionAt` | yes | `lake build AISafetyAtlas.Knowledge.Temporal` | | 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` | no | `scripts/reproduce_isabelle.sh chandy-lamport` | | LAND-SELFMEAS-001 | Self-measurement failure for an embedded observation | Lean | `AISafetyAtlas.Knowledge.knowable_id_iff_injective`
`AISafetyAtlas.Knowledge.not_knowable_state_of_nontrivial_remainder` | yes | `lake build AISafetyAtlas.Knowledge` | | LAND-SELFMEAS-002 | Breuer abstract embedded-measurement core | Lean | `AISafetyAtlas.Knowledge.Embedded.Meshing.restrict_surjective`
`AISafetyAtlas.Knowledge.Embedded.eq_restrict_of_infer_singleton_eq`
`AISafetyAtlas.Knowledge.Embedded.exists_singleton_infer_eq_of_infer_eq`
`AISafetyAtlas.Knowledge.Embedded.exists_state_not_exactly_measurable`
`AISafetyAtlas.Knowledge.Embedded.infer_singleton_eq_of_meshing`
`AISafetyAtlas.Knowledge.Embedded.no_meshing_inference_distinguishes`
`AISafetyAtlas.Knowledge.Embedded.no_meshing_inference_measures_all_states`
`AISafetyAtlas.Knowledge.Embedded.no_meshing_inference_measures_all_states_direct`
`AISafetyAtlas.Knowledge.Embedded.not_knowable_state_of_properInclusion` | yes | `lake build AISafetyAtlas.Knowledge.Embedded` | | LAND-SELFMEAS-003 | Physical complement and finite-cardinality bridges to Breuer proper inclusion | Lean | `AISafetyAtlas.Knowledge.Embedded.Composition.measuresAll_fibreInference_of_injective`
`AISafetyAtlas.Knowledge.Embedded.Composition.meshing_and_measuresAll_fibreInference_of_bijective`
`AISafetyAtlas.Knowledge.Embedded.Composition.meshing_fibreInference_of_surjective`
`AISafetyAtlas.Knowledge.Embedded.Composition.no_meshing_measures_all_of_nontrivial_remainder`
`AISafetyAtlas.Knowledge.Embedded.Composition.no_meshing_measures_all_of_nontrivial_remainder_of_equiv`
`AISafetyAtlas.Knowledge.Embedded.Composition.not_meshing_of_not_surjective`
`AISafetyAtlas.Knowledge.Embedded.Composition.properInclusion_iff_not_injective`
`AISafetyAtlas.Knowledge.Embedded.Composition.properInclusion_of_nontrivial_remainder`
`AISafetyAtlas.Knowledge.Embedded.Composition.properInclusion_of_nontrivial_remainder_of_equiv`
`AISafetyAtlas.Knowledge.Embedded.Finite.no_meshing_measures_all_of_card_lt`
`AISafetyAtlas.Knowledge.Embedded.Finite.properInclusion_of_card_lt`
`AISafetyAtlas.Knowledge.Embedded.Finite.properInclusion_product_of_card_rest_ge_two` | yes | `lake build AISafetyAtlas.Knowledge.Embedded.Composition AISafetyAtlas.Knowledge.Embedded.Finite` | | LAND-KNOW-001 | Exact knowability: the observation-factorization kernel | Lean | `AISafetyAtlas.Knowledge.Determines.trans`
`AISafetyAtlas.Knowledge.Knowable.mono`
`AISafetyAtlas.Knowledge.exists_witness_of_not_knowable`
`AISafetyAtlas.Knowledge.knowable_iff_factorsThrough`
`AISafetyAtlas.Knowledge.knowable_iff_no_collision`
`AISafetyAtlas.Knowledge.not_knowable_comp`
`AISafetyAtlas.Knowledge.not_knowable_of_collision`
`AISafetyAtlas.Knowledge.not_knowable_of_invariant_transform`
`AISafetyAtlas.Knowledge.not_knowable_of_witness` | yes | `lake build AISafetyAtlas.Knowledge` | | LAND-KNOW-DEVICE-001 | Transports between the knowability kernel and inference devices | Lean | `AISafetyAtlas.Knowledge.Devices.BlockwiseCollision.not_physicallyKnows`
`AISafetyAtlas.Knowledge.Devices.BlockwiseCollision.not_weaklyInfers`
`AISafetyAtlas.Knowledge.Devices.knowable_probe_of_forall_blockAnswers`
`AISafetyAtlas.Knowledge.Devices.not_blockAnswers_of_witness` | yes | `lake build AISafetyAtlas.Knowledge.Devices` | | LAND-CRMDP-KNOW-001 | True return does not factor through the observed history | Lean | `AISafetyAtlas.Wireheading.ObservationLimits.not_knowable_trueReturn`
`AISafetyAtlas.Wireheading.ObservationLimits.not_knowable_trueReturn_of_complement_mem`
`AISafetyAtlas.Wireheading.ObservationLimits.returnOver_zeroEnv_complement` | yes | `lake build AISafetyAtlas.Wireheading.ObservationLimits` | | LAND-CRMDP-GRID-001 | Everitt et al. Theorem 11 over the source's own uniform reward grid | Lean | `AISafetyAtlas.Wireheading.RewardGrid.everitt_theorem_eleven_gridClass` | yes | `lake build AISafetyAtlas.Wireheading.RewardGrid AISafetyAtlas.Examples.Wireheading.RewardGrid` | | LAND-FANO-001 | Fano's inequality at both printed constants, and its sharpness | Lean | `AISafetyAtlas.InformationTheory.entropy_le_fano`
`AISafetyAtlas.InformationTheory.fano`
`AISafetyAtlas.InformationTheory.fano_of_embedding`
`AISafetyAtlas.InformationTheory.fano_of_log_le`
`AISafetyAtlas.InformationTheory.fano_unrestricted` | yes | `lake build AISafetyAtlas.InformationTheory.Fano AISafetyAtlas.Examples.InformationTheory.Fano` | | LAND-OVERSIGHT-VARIETY-001 | Seeing and doing are independent oversight capacities | Lean | `AISafetyAtlas.Oversight.exists_cannotForce_false_and_forces`
`AISafetyAtlas.Oversight.forces_of_constant_effect`
`AISafetyAtlas.Oversight.forces_of_constant_effect_of_not_knowable`
`AISafetyAtlas.Oversight.not_forces_of_cannotForce` | yes | `lake build AISafetyAtlas.Oversight.VarietyBound AISafetyAtlas.Oversight.VarietyCheck AISafetyAtlas.Examples.Oversight.VarietyBound` | | LAND-KNOWENTROPY-001 | Knowability measured: zero conditional entropy, and Fano's floor on every decoder | Lean | `AISafetyAtlas.Knowledge.condEntropy_eq_zero_of_knowable`
`AISafetyAtlas.Knowledge.le_errorProb_of_decoder`
`AISafetyAtlas.Knowledge.not_knowable_of_condEntropy_ne_zero` | yes | `lake build AISafetyAtlas.Knowledge.Entropy AISafetyAtlas.Examples.Knowledge.Entropy` | | LAND-DPI-001 | The data-processing inequality, its equality case, and the conditioning counterexamples | Lean | `AISafetyAtlas.InformationTheory.condMutualInfo_le_mutualInfo`
`AISafetyAtlas.InformationTheory.isMarkovChain_iff_measure_factorizes`
`AISafetyAtlas.InformationTheory.isMarkovChain_iff_measure_factorizes_singleton`
`AISafetyAtlas.InformationTheory.measure_factorizes_of_isMarkovChain`
`AISafetyAtlas.InformationTheory.mutualInfo_comp_le`
`AISafetyAtlas.InformationTheory.mutualInfo_eq_iff_isMarkovChain`
`AISafetyAtlas.InformationTheory.mutualInfo_le_of_isMarkovChain` | yes | `lake build AISafetyAtlas.InformationTheory.DataProcessing AISafetyAtlas.Examples.InformationTheory.DataProcessing` | | LAND-CAUSAL-PEARLCBN-001 | Pearl causal Bayesian networks as a condition on an interventional family | Lean | `AISafetyAtlas.Causal.eq_family_of_isCausalBayesNetwork` | yes | `lake build AISafetyAtlas.Causal.BayesianNetwork AISafetyAtlas.Examples.Causal.BayesianNetwork` | | LAND-CAUSAL-DECISIONNET-001 | Decision tasks as causal influence diagrams, with the decision and the utility as vertices | Lean | `AISafetyAtlas.Causal.DecisionNetwork.mem_parents_utility_of_isUnmediated`
`AISafetyAtlas.Examples.Causal.DecisionNetwork.figIsUnmediated` | yes | `lake build AISafetyAtlas.Causal.DecisionNetwork AISafetyAtlas.Examples.Causal.DecisionNetwork` | | LAND-CAUSAL-COLLISION-001 | Margins do not imply behavioral identifiability | Lean | `AISafetyAtlas.Causal.Model.ancestors_eq_univ_iff`
`AISafetyAtlas.Causal.Model.jointProb_hardInterventionProfile`
`AISafetyAtlas.Causal.Model.Δ_fixProfile`
`AISafetyAtlas.Causal.Model.Δmix_congr`
`AISafetyAtlas.Causal.Skeleton.behaviorEq_of_observed_eq_empty`
`AISafetyAtlas.Examples.Causal.Model.jointProb_sum_shiftCollapse`
`AISafetyAtlas.Examples.Causal.behaviorEq_has_teeth`
`AISafetyAtlas.Examples.Causal.margin_class_not_identifiable`
`AISafetyAtlas.Examples.Causal.margin_class_not_identifiable_family`
`AISafetyAtlas.Examples.Causal.margin_class_not_identifiable_two_graphs`
`AISafetyAtlas.Examples.Causal.mm2_shape`
`AISafetyAtlas.Examples.Causal.transform_identity_edgeless`
`AISafetyAtlas.Examples.Causal.Δ_eq_half_sub_joint` | yes | `lake build AISafetyAtlas.Causal.Model AISafetyAtlas.Causal.MarginClass AISafetyAtlas.Examples.Causal.Model AISafetyAtlas.Examples.Causal.BehavioralCollision` | | LAND-CAUSAL-DECISION-001 | Causal decision policies, regret, and identified-set radius | Lean | `AISafetyAtlas.Causal.Model.regret_eq_zero_iff`
`AISafetyAtlas.Causal.Model.value_const_sub`
`AISafetyAtlas.Causal.Model.value_eq`
`AISafetyAtlas.Causal.Model.value_le_sign`
`AISafetyAtlas.Causal.inIdentifiedSet_zero_of_behaviorEq`
`AISafetyAtlas.Causal.modelError_eq_zero_iff`
`AISafetyAtlas.Causal.not_inIdentifiedSet_of_neg`
`AISafetyAtlas.Examples.Causal.OneNodeClass.modelError_le_ten_mul`
`AISafetyAtlas.Examples.Causal.card_fibreRep_empty`
`AISafetyAtlas.Examples.Causal.margin_class_not_identifiable_shared_optimal`
`AISafetyAtlas.Examples.Causal.not_inIdentifiedSet_high` | yes | `lake build AISafetyAtlas.Causal.Decision AISafetyAtlas.Examples.Causal.Decision` | | LAND-CAUSAL-STRUCTURAL-001 | Structural causal models, causal influence diagrams, and materiality | Lean | `AISafetyAtlas.Causal.SCIM.exists_isOptimalPolicy`
`AISafetyAtlas.Causal.SCIM.observableLaw_withPolicy_eq_of_notDownstream`
`AISafetyAtlas.Causal.SCIM.policy_ext_single`
`AISafetyAtlas.Causal.SCM.eval_eq_f`
`AISafetyAtlas.Causal.SCM.exoJoint_mul_prod`
`AISafetyAtlas.Examples.Causal.StructuralModel.figSCIM_opinion_isMaterial`
`AISafetyAtlas.Examples.Causal.StructuralModel.figSCIM_policy_not_const`
`AISafetyAtlas.Examples.Causal.StructuralModel.utility_childless_has_teeth` | yes | `lake build AISafetyAtlas.Causal.StructuralModel AISafetyAtlas.Examples.Causal.StructuralModel` | | LAND-SOV-TRULYPLAYABLE-001 | Truly playable effectivity functions, and the finite-domain corollary | Lean | `AISafetyAtlas.Sovereignty.Playable.trulyPlayable_of_finite` | yes | `lake build AISafetyAtlas.Sovereignty.TrulyPlayable` | | LAND-SOV-PLAYABILITY-001 | Pauly's playability conditions, the easy direction, and the converse that fails | Lean | `AISafetyAtlas.Sovereignty.not_exists_gameForm_cofiniteEff` | yes | `lake build AISafetyAtlas.Sovereignty.Playability` | | LAND-SOV-PLAYABILITY-001 | Pauly's playability conditions, the easy direction, and the converse that fails | Lean | `AISafetyAtlas.Sovereignty.not_exists_gameForm_cofiniteEff` | yes | `lake build AISafetyAtlas.Sovereignty.PlayableConverse` | | LAND-SOV-RETARGETABLE-001 | Retargetable decision-makers have orbit-level tendencies, up to theorem A.13 | Lean | `AISafetyAtlas.Sovereignty.MultiplyRetargetable.mostOrbit`
`AISafetyAtlas.Sovereignty.eu_determined_mostOrbit` | yes | `lake build AISafetyAtlas.Sovereignty.Retargetable` | | LAND-SOV-RETARGETABLE-001 | Retargetable decision-makers have orbit-level tendencies, up to theorem A.13 | Lean | `AISafetyAtlas.Sovereignty.MultiplyRetargetable.mostOrbit`
`AISafetyAtlas.Sovereignty.eu_determined_mostOrbit` | yes | `lake build AISafetyAtlas.Sovereignty.EUDetermined` | | LAND-DEC-MDP-001 | The rewardless Markov decision process, and the run it induces | Lean | `AISafetyAtlas.Decision.MDP.run_congr_obs` | yes | `lake build AISafetyAtlas.Decision.MDP` | | LAND-GOODHART-SELECTION-001 | Selection on a proxy: the inflated gap, and the region the link was never observed in | Lean | `AISafetyAtlas.Goodhart.Extremal.fits_underdetermined_off_observed`
`AISafetyAtlas.Goodhart.gap_selection_ge` | yes | `lake build AISafetyAtlas.Goodhart.Regressional` | | LAND-GOODHART-SELECTION-001 | Selection on a proxy: the inflated gap, and the region the link was never observed in | Lean | `AISafetyAtlas.Goodhart.Extremal.fits_underdetermined_off_observed`
`AISafetyAtlas.Goodhart.gap_selection_ge` | yes | `lake build AISafetyAtlas.Goodhart.Extremal` | | LAND-GOODHART-OVEROPT-001 | Optimizing a proxy over some of the attributes floors the rest | Lean | `AISafetyAtlas.Goodhart.zhuang_hadfield_menell_theorem_one` | yes | `lake build AISafetyAtlas.Goodhart.Overoptimization` | | LAND-SOV-POWER-001 | Peleg's game-form layer: alpha-effectivity, and the conditions it satisfies for free | Lean | `AISafetyAtlas.Sovereignty.Represents.surjective_outcome`
`AISafetyAtlas.Sovereignty.forces_superadditive`
`AISafetyAtlas.Sovereignty.retainsFamily_of_represents`
`AISafetyAtlas.Sovereignty.sov1_of_retainsFamily_singleton` | yes | `lake build AISafetyAtlas.Sovereignty.Rights` | | LAND-SOV-POWER-001 | Peleg's game-form layer: alpha-effectivity, and the conditions it satisfies for free | Lean | `AISafetyAtlas.Sovereignty.Represents.surjective_outcome`
`AISafetyAtlas.Sovereignty.forces_superadditive`
`AISafetyAtlas.Sovereignty.retainsFamily_of_represents`
`AISafetyAtlas.Sovereignty.sov1_of_retainsFamily_singleton` | yes | `lake build AISafetyAtlas.Sovereignty.Mandate` | | LAND-SOV-POWER-001 | Peleg's game-form layer: alpha-effectivity, and the conditions it satisfies for free | Lean | `AISafetyAtlas.Sovereignty.Represents.surjective_outcome`
`AISafetyAtlas.Sovereignty.forces_superadditive`
`AISafetyAtlas.Sovereignty.retainsFamily_of_represents`
`AISafetyAtlas.Sovereignty.sov1_of_retainsFamily_singleton` | yes | `lake build AISafetyAtlas.Sovereignty.Separations` | | LAND-SOV-POWER-001 | Peleg's game-form layer: alpha-effectivity, and the conditions it satisfies for free | Lean | `AISafetyAtlas.Sovereignty.Represents.surjective_outcome`
`AISafetyAtlas.Sovereignty.forces_superadditive`
`AISafetyAtlas.Sovereignty.retainsFamily_of_represents`
`AISafetyAtlas.Sovereignty.sov1_of_retainsFamily_singleton` | yes | `lake build AISafetyAtlas.Sovereignty.ConcurrentGameFrame` | | LAND-SOV-INDEPENDENCE-001 | The logical space of freedom, and the corner that cannot escape | Lean | `AISafetyAtlas.Sovereignty.Setting.not_independenceFree_of_universal_threat`
`AISafetyAtlas.Sovereignty.Setting.republicanFree_of_independenceFree` | yes | `lake build AISafetyAtlas.Sovereignty.Independence` | | LAND-SOV-STEERING-001 | Stepwise retention is not authorship: locally safe steps that lose the original mandate | Lean | `AISafetyAtlas.Examples.Sovereignty.steer_isSteering` | yes | `lake build AISafetyAtlas.Sovereignty.Steering` | | LAND-SOV-SERVICE-001 | Safety without service: a delegate that refuses everything keeps every guarantee it already satisfies | Lean | `AISafetyAtlas.Sovereignty.Refusal.safety_suite_admits_a_refusal`
`AISafetyAtlas.Sovereignty.retainsFamily_and_not_demandwise` | yes | `lake build AISafetyAtlas.Sovereignty.Service` | | LAND-SOV-SERVICE-001 | Safety without service: a delegate that refuses everything keeps every guarantee it already satisfies | Lean | `AISafetyAtlas.Sovereignty.Refusal.safety_suite_admits_a_refusal`
`AISafetyAtlas.Sovereignty.retainsFamily_and_not_demandwise` | yes | `lake build AISafetyAtlas.Sovereignty.Refusal` | | LAND-SOV-QUANT-001 | Two quantifier orders: a response is not a policy, and two guarantees are not one | Lean | `AISafetyAtlas.Sovereignty.forces_inter_of_shared_footprint` | yes | `lake build AISafetyAtlas.Sovereignty.Quantifiers` | | LAND-SOV-TRANSFER-001 | Resources, projections, and the refinement that carries a guarantee | Lean | `AISafetyAtlas.Sovereignty.forces_of_simulates` | yes | `lake build AISafetyAtlas.Sovereignty.Transfer` | | LAND-SOV-CATALOGUE-001 | Passing every demand separately is not being able to run | Lean | `AISafetyAtlas.Sovereignty.Conformity.passes_every_check_and_not_operable`
`AISafetyAtlas.Sovereignty.demandwise_iff_exists_selector` | yes | `lake build AISafetyAtlas.Sovereignty.Catalogue` | | LAND-SOV-CATALOGUE-001 | Passing every demand separately is not being able to run | Lean | `AISafetyAtlas.Sovereignty.Conformity.passes_every_check_and_not_operable`
`AISafetyAtlas.Sovereignty.demandwise_iff_exists_selector` | yes | `lake build AISafetyAtlas.Sovereignty.Conformity` | | LAND-SOV-CATALOGUE-001 | Passing every demand separately is not being able to run | Lean | `AISafetyAtlas.Sovereignty.Conformity.passes_every_check_and_not_operable`
`AISafetyAtlas.Sovereignty.demandwise_iff_exists_selector` | yes | `lake build AISafetyAtlas.Sovereignty.ConformityCheck` | | LAND-SOV-AUDIT-001 | What a channel can certify, and what it only has to be good enough to act on | Lean | `AISafetyAtlas.Sovereignty.exists_uniformDecision_iff` | yes | `lake build AISafetyAtlas.Sovereignty.Auditability` | | LAND-SOV-COMM-001 | Zero-error communication against an adversary is disjoint forceable regions | Lean | `AISafetyAtlas.Sovereignty.transmitsZeroError_iff_exists_code` | yes | `lake build AISafetyAtlas.Sovereignty.Communication` | | LAND-SOV-CONST-001 | An amendment chain is evidence about the amendment rule and nothing else | Lean | `AISafetyAtlas.Sovereignty.AmendmentLog.unbroken_chain_is_not_a_constraint`
`AISafetyAtlas.Sovereignty.authorizedFrom_of_total` | yes | `lake build AISafetyAtlas.Sovereignty.Constitution` | | LAND-SOV-CONST-001 | An amendment chain is evidence about the amendment rule and nothing else | Lean | `AISafetyAtlas.Sovereignty.AmendmentLog.unbroken_chain_is_not_a_constraint`
`AISafetyAtlas.Sovereignty.authorizedFrom_of_total` | yes | `lake build AISafetyAtlas.Sovereignty.AmendmentLog` | | LAND-SOV-DISTURB-001 | Reaching every state is not holding one: the quantifier a rank condition hides | Lean | `AISafetyAtlas.Sovereignty.Plant.exists_robustInput_iff` | yes | `lake build AISafetyAtlas.Sovereignty.Disturbance` | | LAND-SOV-AUTH-001 | Authority is an input, and the links it does not come with | Lean | `AISafetyAtlas.Sovereignty.Attestation.attestation_is_not_the_claim`
`AISafetyAtlas.Sovereignty.Attestation.properties_are_independent`
`AISafetyAtlas.Sovereignty.DelegationChain.power_over_a_matter_does_not_compose`
`AISafetyAtlas.Sovereignty.ShutdownChannel.obedience_does_not_give_authority`
`AISafetyAtlas.Sovereignty.not_exists_label_agreeing_with_both` | yes | `lake build AISafetyAtlas.Sovereignty.Authority` | | LAND-SOV-AUTH-001 | Authority is an input, and the links it does not come with | Lean | `AISafetyAtlas.Sovereignty.Attestation.attestation_is_not_the_claim`
`AISafetyAtlas.Sovereignty.Attestation.properties_are_independent`
`AISafetyAtlas.Sovereignty.DelegationChain.power_over_a_matter_does_not_compose`
`AISafetyAtlas.Sovereignty.ShutdownChannel.obedience_does_not_give_authority`
`AISafetyAtlas.Sovereignty.not_exists_label_agreeing_with_both` | yes | `lake build AISafetyAtlas.Sovereignty.Domination` | | LAND-SOV-AUTH-001 | Authority is an input, and the links it does not come with | Lean | `AISafetyAtlas.Sovereignty.Attestation.attestation_is_not_the_claim`
`AISafetyAtlas.Sovereignty.Attestation.properties_are_independent`
`AISafetyAtlas.Sovereignty.DelegationChain.power_over_a_matter_does_not_compose`
`AISafetyAtlas.Sovereignty.ShutdownChannel.obedience_does_not_give_authority`
`AISafetyAtlas.Sovereignty.not_exists_label_agreeing_with_both` | yes | `lake build AISafetyAtlas.Sovereignty.ShutdownChannel` | | LAND-SOV-AUTH-001 | Authority is an input, and the links it does not come with | Lean | `AISafetyAtlas.Sovereignty.Attestation.attestation_is_not_the_claim`
`AISafetyAtlas.Sovereignty.Attestation.properties_are_independent`
`AISafetyAtlas.Sovereignty.DelegationChain.power_over_a_matter_does_not_compose`
`AISafetyAtlas.Sovereignty.ShutdownChannel.obedience_does_not_give_authority`
`AISafetyAtlas.Sovereignty.not_exists_label_agreeing_with_both` | yes | `lake build AISafetyAtlas.Sovereignty.Attestation` | | LAND-SOV-AUTH-001 | Authority is an input, and the links it does not come with | Lean | `AISafetyAtlas.Sovereignty.Attestation.attestation_is_not_the_claim`
`AISafetyAtlas.Sovereignty.Attestation.properties_are_independent`
`AISafetyAtlas.Sovereignty.DelegationChain.power_over_a_matter_does_not_compose`
`AISafetyAtlas.Sovereignty.ShutdownChannel.obedience_does_not_give_authority`
`AISafetyAtlas.Sovereignty.not_exists_label_agreeing_with_both` | yes | `lake build AISafetyAtlas.Sovereignty.DelegationChain` | | LAND-SOV-VALUE-001 | Values on a game form, with sure winning sitting inside them | Lean | `AISafetyAtlas.Sovereignty.lowerValue_diracLaw_eq_one_iff` | yes | `lake build AISafetyAtlas.Sovereignty.Value` | | LAND-SOV-INFL-001 | Influence is a capacity, and it is not power | Lean | `AISafetyAtlas.Sovereignty.influenceCapacity_eq_zero_iff` | yes | `lake build AISafetyAtlas.Sovereignty.Influence` | | LAND-SOV-SAFETYGAME-001 | Holding a system inside a set forever, and getting back inside a budget | Lean | `AISafetyAtlas.Sovereignty.SafetyGame.mem_safetyKernel_iff_exists_maintaining` | yes | `lake build AISafetyAtlas.Sovereignty.SafetyGame` | | LAND-SOV-SAFETYGAME-001 | Holding a system inside a set forever, and getting back inside a budget | Lean | `AISafetyAtlas.Sovereignty.SafetyGame.mem_safetyKernel_iff_exists_maintaining` | yes | `lake build AISafetyAtlas.Sovereignty.ShieldCheck` | | LAND-SOV-BELIEF-001 | Deciding on one's own beliefs, while another party writes them | Lean | `AISafetyAtlas.Sovereignty.DoxasticAgent.mem_of_agent_forces` | yes | `lake build AISafetyAtlas.Sovereignty.Belief` | | LAND-SOV-EVIDENCE-001 | What a decision can achieve on the evidence it has | Lean | `AISafetyAtlas.Sovereignty.exists_success_le_inv` | yes | `lake build AISafetyAtlas.Sovereignty.Evidence` | | LAND-SOV-COGSOV-001 | The cognitive-sovereignty predicate, and what belief change does not prove | Lean | `AISafetyAtlas.Sovereignty.magnitude_does_not_decide_authorship` | yes | `lake build AISafetyAtlas.Sovereignty.CogSov` | | LAND-SOV-EMPOWER-001 | Empowerment of a deterministic channel is the capacity of its range | Lean | `AISafetyAtlas.Sovereignty.empowerment_eq_log_card_range` | yes | `lake build AISafetyAtlas.Sovereignty.Empowerment` | | LAND-SOV-MINIMAX-001 | Mixed strategies close the gap a pure commitment leaves | Lean | `AISafetyAtlas.Sovereignty.exists_mixed_value` | yes | `lake build AISafetyAtlas.Sovereignty.Minimax` | | LAND-SOV-OUTNUMBERED-001 | Being outnumbered is not being outmatched | Lean | `AISafetyAtlas.Sovereignty.safetyKernel_subset_of_adversaryLe` | yes | `lake build AISafetyAtlas.Sovereignty.Outnumbered` | | LAND-VERIF-AGENTBEHAVIOR-001 | No total verifier for a nontrivial behavioural safety specification | Lean | `AISafetyAtlas.Verification.AgentBehavior.no_behavioral_safety_verifier` | yes | `lake build AISafetyAtlas.Verification.AgentBehavior` | | LAND-LINSYS-001 | Kalman and Hautus: when a linear system's state is determined, and when it can be driven | Lean | `AISafetyAtlas.LinearSystems.isObservable_iff_hautus` | yes | `lake build AISafetyAtlas.LinearSystems` | | LAND-LINSYS-001 | Kalman and Hautus: when a linear system's state is determined, and when it can be driven | Lean | `AISafetyAtlas.LinearSystems.isObservable_iff_hautus` | yes | `lake build AISafetyAtlas.LinearSystems.MatrixLemmas` | | LAND-LINSYS-001 | Kalman and Hautus: when a linear system's state is determined, and when it can be driven | Lean | `AISafetyAtlas.LinearSystems.isObservable_iff_hautus` | yes | `lake build AISafetyAtlas.LinearSystems.Controllability` | | LAND-LINSYS-001 | Kalman and Hautus: when a linear system's state is determined, and when it can be driven | Lean | `AISafetyAtlas.LinearSystems.isObservable_iff_hautus` | yes | `lake build AISafetyAtlas.LinearSystems.Observability` | | LAND-LINSYS-001 | Kalman and Hautus: when a linear system's state is determined, and when it can be driven | Lean | `AISafetyAtlas.LinearSystems.isObservable_iff_hautus` | yes | `lake build AISafetyAtlas.LinearSystems.Hautus` | | LAND-LINSYS-001 | Kalman and Hautus: when a linear system's state is determined, and when it can be driven | Lean | `AISafetyAtlas.LinearSystems.isObservable_iff_hautus` | yes | `lake build AISafetyAtlas.LinearSystems.BlockBound` | | LAND-LINSYS-001 | Kalman and Hautus: when a linear system's state is determined, and when it can be driven | Lean | `AISafetyAtlas.LinearSystems.isObservable_iff_hautus` | yes | `lake build AISafetyAtlas.LinearSystems.Dynamics` | | LAND-LINSYS-001 | Kalman and Hautus: when a linear system's state is determined, and when it can be driven | Lean | `AISafetyAtlas.LinearSystems.isObservable_iff_hautus` | yes | `lake build AISafetyAtlas.LinearSystems.Flow` | | LAND-SOV-VOTINGPOWER-001 | A zero power index names a null player only where the marginals cannot cancel | Lean | `AISafetyAtlas.Sovereignty.SimpleGame.banzhafRaw_eq_swings_div`
`AISafetyAtlas.Sovereignty.SimpleGame.shapleyShubik_eq_zero_iff` | yes | `lake build AISafetyAtlas.Sovereignty.VotingPower` | | LAND-SOV-CAPABILITY-001 | A maintenance floor for fallback capability, and why assisted output does not report it | Lean | `AISafetyAtlas.Sovereignty.Enlarges.forces`
`AISafetyAtlas.Sovereignty.exists_output_rise_with_fallback_fall`
`AISafetyAtlas.Sovereignty.fallback_not_knowable_from_assistedOutput`
`AISafetyAtlas.Sovereignty.maintenanceFloor_of_practice_floor` | yes | `lake build AISafetyAtlas.Sovereignty.Capability` | | LAND-EVAL-BLINDSPOT-001 | What an evaluation that scores runs one at a time can and cannot see | Lean | `AISafetyAtlas.Compositional.Hyperproperties.Evaluation.sampling_misses_subsingleton`
`AISafetyAtlas.Compositional.Hyperproperties.Evaluation.traceProperty_knowable_of_score_decides` | yes | `lake build AISafetyAtlas.Compositional.Hyperproperties.Evaluation AISafetyAtlas.Examples.Compositional.Hyperproperties.Evaluation` | | LAND-AUDIT-REGISTRY-001 | Audit registries along a value chain: what publishing declarations can settle | Lean | `AISafetyAtlas.Oversight.JointObservation.consortium_covers_of_registry_covers`
`AISafetyAtlas.Oversight.JointObservation.not_registry_covers_of_emit_collision` | yes | `lake build AISafetyAtlas.Oversight.JointObservation.Registry AISafetyAtlas.Examples.Oversight.JointObservationRegistry` | | LAND-ACCESS-ORDER-001 | Forms of model access: three points on the informativeness order, and what no methodology repairs | Lean | `AISafetyAtlas.Knowledge.Access.exists_indistinguishable_behaviour`
`AISafetyAtlas.Knowledge.Access.no_blackBox_methodology`
`AISafetyAtlas.Knowledge.Access.whiteBox_determines_blackBox` | yes | `lake build AISafetyAtlas.Knowledge.Access AISafetyAtlas.Examples.Knowledge.Access` | | LAND-GOODHART-REGTARGET-001 | Regulatory targets: the bar certifies exactly the systems its evidence never covered | Lean | `AISafetyAtlas.Goodhart.RegulatoryTarget.certified_systems_were_never_examined`
`AISafetyAtlas.Goodhart.RegulatoryTarget.raising_the_bar_does_not_help`
`AISafetyAtlas.Goodhart.RegulatoryTarget.risk_unconstrained_on_certified` | yes | `lake build AISafetyAtlas.Goodhart.RegulatoryTarget AISafetyAtlas.Examples.Goodhart.RegulatoryTarget` | | LAND-SOV-ASSESSMENT-001 | Measuring unaided capability: withdrawal testing is forced, not chosen | Lean | `AISafetyAtlas.Sovereignty.CapabilityAssessment.no_procedure_on_output_recovers_fallback`
`AISafetyAtlas.Sovereignty.CapabilityAssessment.protocols_are_incomparable`
`AISafetyAtlas.Sovereignty.CapabilityAssessment.withdrawal_settles_and_no_output_procedure_does` | yes | `lake build AISafetyAtlas.Sovereignty.CapabilityAssessment AISafetyAtlas.Examples.Sovereignty.CapabilityAssessment` | | LAND-VERIF-FULLACCESS-001 | Full access to the code: Rice bounds the behavioral half and nothing else | Lean | `AISafetyAtlas.Verification.FullAccess.access_is_not_what_separates_them`
`AISafetyAtlas.Verification.FullAccess.fullAccessVerifier_exactArtifact`
`AISafetyAtlas.Verification.FullAccess.no_fullAccessVerifier_of_extensional` | yes | `lake build AISafetyAtlas.Verification.FullAccess AISafetyAtlas.Examples.Verification.FullAccess` | | LAND-AUDIT-LAG-001 | What an audit certifies: the audited version, not the deployed one | Lean | `AISafetyAtlas.Knowledge.Audit.audit_certifies_audited_not_deployed`
`AISafetyAtlas.Knowledge.Audit.later_audit_does_not_close_the_gap` | yes | `lake build AISafetyAtlas.Knowledge.Audit AISafetyAtlas.Examples.Knowledge.Audit` | | LAND-INCIDENT-COUNT-001 | Counting AI incidents: the number a regime publishes is a property of its filing schema | Lean | `AISafetyAtlas.Knowledge.IncidentCount.count_is_not_a_measurement`
`AISafetyAtlas.Knowledge.IncidentCount.count_not_determined_of_collision`
`AISafetyAtlas.Knowledge.IncidentCount.knowable_of_report_carries_count`
`AISafetyAtlas.Knowledge.IncidentCount.schema_fixes_the_count` | yes | `lake build AISafetyAtlas.Knowledge.IncidentCount AISafetyAtlas.Examples.Practitioner` | | LAND-KNOW-UNIFORM-001 | Acting acceptably without identifying the state: the uniform decision boundary | Lean | `AISafetyAtlas.Knowledge.knowable_iff_uniformlyActionable`
`AISafetyAtlas.Knowledge.not_uniformlyActionable_iff_exists_unservable`
`AISafetyAtlas.Knowledge.uniformlyActionable_iff_fibrewiseAgreeable`
`AISafetyAtlas.Knowledge.uniformlyActionable_of_pairwiseAgreeable_of_card_le_two` | yes | `lake build AISafetyAtlas.Knowledge.UniformAction` | | LAND-SOV-STABILITY-001 | Keiding's cycle, stated at this repository's effectivity families | Lean | `AISafetyAtlas.Sovereignty.gameFormAcyclic_iff`
`AISafetyAtlas.Sovereignty.not_gameFormAcyclic_of_cycle` | yes | `lake build AISafetyAtlas.Sovereignty.Stability AISafetyAtlas.Examples.Sovereignty.Stability` | | LAND-SOV-DEONTIC-001 | May, may not, can, and is empowered to are four different things | Lean | `AISafetyAtlas.Sovereignty.Enforcement.undetectable_norm_is_unenforceable`
`AISafetyAtlas.Sovereignty.InstitutionalSetting.exists_empowered_possible_not_permitted`
`AISafetyAtlas.Sovereignty.NormSystem.forbidden_iff_not_permitted_iff`
`AISafetyAtlas.Sovereignty.oughtImpliesCan_does_not_give_permission` | yes | `lake build AISafetyAtlas.Sovereignty.Deontic` | | LAND-SOV-DEONTIC-001 | May, may not, can, and is empowered to are four different things | Lean | `AISafetyAtlas.Sovereignty.Enforcement.undetectable_norm_is_unenforceable`
`AISafetyAtlas.Sovereignty.InstitutionalSetting.exists_empowered_possible_not_permitted`
`AISafetyAtlas.Sovereignty.NormSystem.forbidden_iff_not_permitted_iff`
`AISafetyAtlas.Sovereignty.oughtImpliesCan_does_not_give_permission` | yes | `lake build AISafetyAtlas.Sovereignty.Enforcement` | | LAND-SOV-DEONTIC-001 | May, may not, can, and is empowered to are four different things | Lean | `AISafetyAtlas.Sovereignty.Enforcement.undetectable_norm_is_unenforceable`
`AISafetyAtlas.Sovereignty.InstitutionalSetting.exists_empowered_possible_not_permitted`
`AISafetyAtlas.Sovereignty.NormSystem.forbidden_iff_not_permitted_iff`
`AISafetyAtlas.Sovereignty.oughtImpliesCan_does_not_give_permission` | yes | `lake build AISafetyAtlas.Sovereignty.EnforcementCheck` | | LAND-SOV-DEONTIC-001 | May, may not, can, and is empowered to are four different things | Lean | `AISafetyAtlas.Sovereignty.Enforcement.undetectable_norm_is_unenforceable`
`AISafetyAtlas.Sovereignty.InstitutionalSetting.exists_empowered_possible_not_permitted`
`AISafetyAtlas.Sovereignty.NormSystem.forbidden_iff_not_permitted_iff`
`AISafetyAtlas.Sovereignty.oughtImpliesCan_does_not_give_permission` | yes | `lake build AISafetyAtlas.Sovereignty.AATS` | | LAND-SOV-INSTITUTION-001 | A Horn derivation is not counts-as, and the proof is two theorems | Lean | `AISafetyAtlas.Sovereignty.Institution.exists_recognized_not_authorized`
`AISafetyAtlas.Sovereignty.countsAs_validates_refl_and_trans`
`AISafetyAtlas.Sovereignty.no_authority_from_ungrounded_cycles` | yes | `lake build AISafetyAtlas.Sovereignty.Institution` | | LAND-BELLMAN-BDD-001 | The bounded fixed point: a discounted policy value without a finite state space | Lean | `AISafetyAtlas.Decision.vPiBdd_eq_vPi` | yes | `lake build AISafetyAtlas.Analysis.Blackwell` | | LAND-BELLMAN-BDD-001 | The bounded fixed point: a discounted policy value without a finite state space | Lean | `AISafetyAtlas.Decision.vPiBdd_eq_vPi` | yes | `lake build AISafetyAtlas.Decision.BoundedValue` | | LAND-GOODHART-HACKABILITY-001 | Hackability: two reward functions that disagree about which policy is better | Lean | `AISafetyAtlas.Decision.J_linear`
`AISafetyAtlas.Goodhart.unhackable_of_simplifies_common` | yes | `lake build AISafetyAtlas.Decision.Occupancy` | | LAND-GOODHART-HACKABILITY-001 | Hackability: two reward functions that disagree about which policy is better | Lean | `AISafetyAtlas.Decision.J_linear`
`AISafetyAtlas.Goodhart.unhackable_of_simplifies_common` | yes | `lake build AISafetyAtlas.Goodhart.Hackability` |