module public import AISafetyAtlas.Composition public import AISafetyAtlas.Examples.Composition.Observability public import AISafetyAtlas.Computability public import AISafetyAtlas.Analysis.Blackwell public import AISafetyAtlas.Analysis.MaximalMinor public import AISafetyAtlas.Analysis.NullImage public import AISafetyAtlas.Analysis.PolynomialGenericity public import AISafetyAtlas.Analysis.Semialgebraic public import AISafetyAtlas.Examples.Analysis.Semialgebraic public import AISafetyAtlas.Combinatorics.Cascade public import AISafetyAtlas.Combinatorics.CascadeFamily public import AISafetyAtlas.Combinatorics.KruskalKatona public import AISafetyAtlas.Combinatorics.PermInvariance public import AISafetyAtlas.Examples.Combinatorics.Cascade public import AISafetyAtlas.Examples.Combinatorics.CascadeFamily public import AISafetyAtlas.Examples.Combinatorics.KruskalKatona public import AISafetyAtlas.Order.FinsetRefinement public import AISafetyAtlas.Examples.Order.FinsetRefinement public import AISafetyAtlas.Compositional public import AISafetyAtlas.Compositional.AgentNetwork public import AISafetyAtlas.Control public import AISafetyAtlas.Control.OversightBudget public import AISafetyAtlas.Examples.Control.OversightBudget public import AISafetyAtlas.Examples.Control.RegulationCheck public import AISafetyAtlas.Decision.MDP public import AISafetyAtlas.Decision.Expect public import AISafetyAtlas.Decision.BoundedValue public import AISafetyAtlas.Decision.DiscountedValue public import AISafetyAtlas.Decision.Occupancy public import AISafetyAtlas.Examples.Wireheading.DelusionBox public import AISafetyAtlas.Examples.Wireheading.SelfMod public import AISafetyAtlas.Examples.Wireheading.ProgramPrior public import AISafetyAtlas.Examples.Wireheading.ValueBounds public import AISafetyAtlas.Examples.Wireheading.Mixture public import AISafetyAtlas.Examples.Wireheading.CRMDP public import AISafetyAtlas.Examples.Wireheading.Corruption public import AISafetyAtlas.Examples.Wireheading.GoalPreservation public import AISafetyAtlas.Examples.Wireheading.GoalPreservationCarrier public import AISafetyAtlas.Examples.Wireheading.GoalPreservationSource public import AISafetyAtlas.Examples.Wireheading.AgentEquations public import AISafetyAtlas.Examples.Wireheading.Objective public import AISafetyAtlas.Examples.Decision.MDP public import AISafetyAtlas.Examples.Decision.DiscountedValue public import AISafetyAtlas.Examples.Decision.Expect public import AISafetyAtlas.Examples.Decision.BoundedValue public import AISafetyAtlas.Examples.Decision.Occupancy public import AISafetyAtlas.Explainability public import AISafetyAtlas.Fairness.RiskAssignment public import AISafetyAtlas.Fairness.Tradeoff public import AISafetyAtlas.Examples.Fairness.RiskAssignment public import AISafetyAtlas.Goodhart.Regressional public import AISafetyAtlas.Examples.Goodhart.Regressional public import AISafetyAtlas.Goodhart.Overoptimization public import AISafetyAtlas.Examples.Goodhart.Overoptimization public import AISafetyAtlas.Goodhart.Extremal public import AISafetyAtlas.Examples.Goodhart.Extremal public import AISafetyAtlas.Goodhart.RegulatoryTarget public import AISafetyAtlas.Examples.Goodhart.RegulatoryTarget public import AISafetyAtlas.Goodhart.Hackability public import AISafetyAtlas.Examples.Goodhart.Hackability public import AISafetyAtlas.Fairness.ApproximateRiskAssignment public import AISafetyAtlas.Examples.Fairness.ApproximateRiskAssignment public import AISafetyAtlas.Learning public import AISafetyAtlas.Learning.Sharp public import AISafetyAtlas.LinearSystems public import AISafetyAtlas.Examples.LinearSystems.Criteria public import AISafetyAtlas.Examples.LinearSystems.Dynamics public import AISafetyAtlas.Examples.LinearSystems.Flow public import AISafetyAtlas.Knowledge public import AISafetyAtlas.Inference public import AISafetyAtlas.Causal.Model public import AISafetyAtlas.Causal.BayesianNetwork public import AISafetyAtlas.Causal.MarginClass public import AISafetyAtlas.Causal.Decision public import AISafetyAtlas.Causal.DecisionNetwork public import AISafetyAtlas.Causal.ParameterChart public import AISafetyAtlas.Causal.EffectiveGenericity public import AISafetyAtlas.Causal.Query public import AISafetyAtlas.Causal.ModelSpace public import AISafetyAtlas.Causal.StructuralModel public import AISafetyAtlas.Causal.DSep public import AISafetyAtlas.Causal.Requisite public import AISafetyAtlas.Causal.Incentive public import AISafetyAtlas.Causal.Knowability public import AISafetyAtlas.Causal.Goal public import AISafetyAtlas.Causal.ControlledProcess public import AISafetyAtlas.Causal.GoalDynamics public import AISafetyAtlas.Causal.Corruption public import AISafetyAtlas.Examples.Causal.Model public import AISafetyAtlas.Examples.Causal.BayesianNetwork public import AISafetyAtlas.Examples.Causal.BehavioralCollision public import AISafetyAtlas.Examples.Causal.Decision public import AISafetyAtlas.Examples.Causal.DecisionNetwork public import AISafetyAtlas.Examples.Causal.Query public import AISafetyAtlas.Examples.Causal.EffectiveGenericity public import AISafetyAtlas.Examples.Causal.O24Refutation public import AISafetyAtlas.Examples.Causal.Goal public import AISafetyAtlas.Examples.Causal.ControlledProcess public import AISafetyAtlas.Examples.Causal.GoalDynamics public import AISafetyAtlas.Examples.Causal.O33Corruption public import AISafetyAtlas.Examples.Causal.ModelSpace public import AISafetyAtlas.Examples.Causal.StructuralModel public import AISafetyAtlas.Examples.Causal.DSep public import AISafetyAtlas.Examples.Causal.Requisite public import AISafetyAtlas.Examples.Causal.Incentive public import AISafetyAtlas.Examples.Causal.OneNodeClass public import AISafetyAtlas.Examples.Causal.ParameterChart public import AISafetyAtlas.InformationTheory.PrefixCode public import AISafetyAtlas.Examples.InformationTheory.PrefixCode public import AISafetyAtlas.InformationTheory.ChannelCapacity public import AISafetyAtlas.InformationTheory.DataProcessing public import AISafetyAtlas.InformationTheory.Determinism public import AISafetyAtlas.InformationTheory.Fano public import AISafetyAtlas.Knowledge.Embedded public import AISafetyAtlas.Knowledge.Embedded.Composition public import AISafetyAtlas.Knowledge.Embedded.Finite public import AISafetyAtlas.Knowledge.Temporal public import AISafetyAtlas.Knowledge.Ambiguity public import AISafetyAtlas.Knowledge.SelfReference public import AISafetyAtlas.Knowledge.Accumulation public import AISafetyAtlas.Knowledge.Devices public import AISafetyAtlas.Knowledge.Entropy public import AISafetyAtlas.Knowledge.UniformAction public import AISafetyAtlas.Knowledge.Check public import AISafetyAtlas.Knowledge.Audit public import AISafetyAtlas.Knowledge.IncidentCount public import AISafetyAtlas.Knowledge.Access public import AISafetyAtlas.Logic public import AISafetyAtlas.Oversight.JointObservation public import AISafetyAtlas.Oversight.VarietyBound public import AISafetyAtlas.Oversight.VarietyCheck public import AISafetyAtlas.Preference public import AISafetyAtlas.Preference.Complexity public import AISafetyAtlas.Preference.Reasonable public import AISafetyAtlas.Preference.SourceComplexity public import AISafetyAtlas.Preference.Override public import AISafetyAtlas.Preference.Regret public import AISafetyAtlas.Preference.Knowability public import AISafetyAtlas.Preference.Trajectory public import AISafetyAtlas.Examples.Preference.Trajectory public import AISafetyAtlas.Examples.Preference.Override public import AISafetyAtlas.Examples.Preference.Regret public import AISafetyAtlas.Examples.Preference.SourceComplexity public import AISafetyAtlas.Examples.Preference.Complexity public import AISafetyAtlas.SelfAwareness public import AISafetyAtlas.Sovereignty.Arena public import AISafetyAtlas.Sovereignty.Separations public import AISafetyAtlas.Sovereignty.ConcurrentGameFrame public import AISafetyAtlas.Sovereignty.Boundary public import AISafetyAtlas.Sovereignty.Playability public import AISafetyAtlas.Sovereignty.PlayableConverse public import AISafetyAtlas.Sovereignty.TrulyPlayable public import AISafetyAtlas.Sovereignty.Retargetable public import AISafetyAtlas.Sovereignty.EUDetermined public import AISafetyAtlas.Sovereignty.Independence public import AISafetyAtlas.Sovereignty.Rights public import AISafetyAtlas.Sovereignty.Representation public import AISafetyAtlas.Sovereignty.Mandate public import AISafetyAtlas.Sovereignty.Steering public import AISafetyAtlas.Sovereignty.Service public import AISafetyAtlas.Sovereignty.Refusal public import AISafetyAtlas.Sovereignty.Quantifiers public import AISafetyAtlas.Sovereignty.Transfer public import AISafetyAtlas.Sovereignty.Catalogue public import AISafetyAtlas.Sovereignty.Enforcement public import AISafetyAtlas.Sovereignty.EnforcementCheck public import AISafetyAtlas.Sovereignty.ShutdownChannel public import AISafetyAtlas.Sovereignty.Conformity public import AISafetyAtlas.Sovereignty.ConformityCheck public import AISafetyAtlas.Sovereignty.Attestation public import AISafetyAtlas.Sovereignty.DelegationChain public import AISafetyAtlas.Sovereignty.Auditability public import AISafetyAtlas.Sovereignty.Communication public import AISafetyAtlas.Sovereignty.Constitution public import AISafetyAtlas.Sovereignty.AmendmentLog public import AISafetyAtlas.Sovereignty.Disturbance public import AISafetyAtlas.Sovereignty.Authority public import AISafetyAtlas.Sovereignty.Domination public import AISafetyAtlas.Sovereignty.Value public import AISafetyAtlas.Sovereignty.Influence public import AISafetyAtlas.Sovereignty.SafetyGame public import AISafetyAtlas.Sovereignty.ShieldCheck public import AISafetyAtlas.Sovereignty.Belief public import AISafetyAtlas.Sovereignty.Evidence public import AISafetyAtlas.Sovereignty.CogSov public import AISafetyAtlas.Sovereignty.Empowerment public import AISafetyAtlas.Sovereignty.Minimax public import AISafetyAtlas.Sovereignty.Outnumbered public import AISafetyAtlas.Sovereignty.VotingPower public import AISafetyAtlas.Sovereignty.Stability public import AISafetyAtlas.Sovereignty.Deontic public import AISafetyAtlas.Sovereignty.AATS public import AISafetyAtlas.Sovereignty.Institution public import AISafetyAtlas.Sovereignty.Capability public import AISafetyAtlas.Sovereignty.CapabilityAssessment public import AISafetyAtlas.Examples.Sovereignty.Arena public import AISafetyAtlas.Examples.Sovereignty.Separations public import AISafetyAtlas.Examples.Sovereignty.ConcurrentGameFrame public import AISafetyAtlas.Examples.Sovereignty.Boundary public import AISafetyAtlas.Examples.Sovereignty.Domination public import AISafetyAtlas.Examples.Sovereignty.Playability public import AISafetyAtlas.Examples.Sovereignty.PlayableConverse public import AISafetyAtlas.Examples.Sovereignty.TrulyPlayable public import AISafetyAtlas.Examples.Sovereignty.Retargetable public import AISafetyAtlas.Examples.Sovereignty.EUDetermined public import AISafetyAtlas.Examples.Sovereignty.Independence public import AISafetyAtlas.Examples.Sovereignty.Rights public import AISafetyAtlas.Examples.Sovereignty.Representation public import AISafetyAtlas.Examples.Sovereignty.Mandate public import AISafetyAtlas.Examples.Sovereignty.Steering public import AISafetyAtlas.Examples.Sovereignty.Service public import AISafetyAtlas.Examples.Sovereignty.Quantifiers public import AISafetyAtlas.Examples.Sovereignty.Transfer public import AISafetyAtlas.Examples.Sovereignty.Catalogue public import AISafetyAtlas.Examples.Sovereignty.Governance public import AISafetyAtlas.Examples.Sovereignty.Checkers public import AISafetyAtlas.Examples.DeployedAssistant public import AISafetyAtlas.Examples.Practitioner public import AISafetyAtlas.Examples.Sovereignty.Auditability public import AISafetyAtlas.Examples.Sovereignty.Communication public import AISafetyAtlas.Examples.Sovereignty.Constitution public import AISafetyAtlas.Examples.Sovereignty.Disturbance public import AISafetyAtlas.Examples.Sovereignty.Authority public import AISafetyAtlas.Examples.Sovereignty.Value public import AISafetyAtlas.Examples.Sovereignty.Influence public import AISafetyAtlas.Examples.Sovereignty.SafetyGame public import AISafetyAtlas.Examples.Sovereignty.Belief public import AISafetyAtlas.Examples.Sovereignty.Evidence public import AISafetyAtlas.Examples.Sovereignty.CogSov public import AISafetyAtlas.Examples.Sovereignty.Empowerment public import AISafetyAtlas.Examples.Sovereignty.Minimax public import AISafetyAtlas.Examples.Sovereignty.Outnumbered public import AISafetyAtlas.Examples.Sovereignty.VotingPower public import AISafetyAtlas.Examples.Sovereignty.Stability public import AISafetyAtlas.Examples.Sovereignty.Deontic public import AISafetyAtlas.Examples.Sovereignty.AATS public import AISafetyAtlas.Examples.Sovereignty.Institution public import AISafetyAtlas.Examples.Sovereignty.Capability public import AISafetyAtlas.SocialChoice public import AISafetyAtlas.SocialChoice.Utility public import AISafetyAtlas.Examples.SocialChoice.Utility public import AISafetyAtlas.Verification public import AISafetyAtlas.Verification.AgentBehavior public import AISafetyAtlas.Verification.Containment public import AISafetyAtlas.Verification.Robot public import AISafetyAtlas.Verification.RobotRun public import AISafetyAtlas.Verification.FullAccess public import AISafetyAtlas.Wireheading public import AISafetyAtlas.Examples.Wireheading.CRMDPModel public import AISafetyAtlas.Examples.Wireheading.StochasticCRMDP public import AISafetyAtlas.Examples.Wireheading.StochasticPolicy /-! # AI Safety Formalization Atlas Root import surface. Modules here compile without `sorry` and distinguish mathematical results from AI-safety bridge claims. ## Import contracts One import does not mean the same thing under every parent. Four patterns: | Pattern | What one import supplies | Parents | |---|---|---| | Aggregating facade | the domain's whole public surface | `Compositional`, `Control`, `Oversight.JointObservation`, `Wireheading` | | Partial aggregate | the mathematical base, without the bridge modules | `Verification` | | Kernel and specializations | a closed surface; each specialization is imported on its own | `Knowledge`, `Preference` | | Peer modules | no aggregating parent; import the one needed | `InformationTheory`, `Causal` | `Knowledge` and `Preference` withhold their specializations deliberately. A kernel that re-exported its own specializations could no longer state what it excludes: importing `Knowledge` yields the observation-factorization kernel and nothing embedded, temporal, or self-referential. The root import list below is the public closure and is expected to name specializations directly. **One published facade is deliberately outside it.** `AISafetyAtlas.Oversight.Debate` wraps a vendored development that declares roughly 157 names in the *root* namespace, so it is imported on its own and audited through `OFF_ROOT_FACADES` in `scripts/check_print_axioms.py` rather than through this closure; its module docstring gives the reason. ## Aggregating facades | Import | Domain | |---|---| | `AISafetyAtlas.Compositional` | Hyperproperties, rectangles, networks | | `AISafetyAtlas.Control` | Ashby's variety bounds and Touchette–Lloyd's information limits, in ten modules | | `AISafetyAtlas.Oversight.JointObservation` | Coalition evidence, coverage, collision, repair boundary | | `AISafetyAtlas.Wireheading` | Reward channels, self-modification | `Oversight.JointObservation` aggregates the evidence surface and stops there: `AISafetyAtlas.Oversight.VarietyBound` is a **bridge** module and does not arrive with it, the same contract `Verification` keeps with its two bridges below. ### What `Control` aggregates Ten modules, nine of them one printed development each and one a decision procedure. `AISafetyAtlas.Control` carries all of them; import one directly when only its result is wanted. | Import | Domain | |---|---| | `AISafetyAtlas.Control.RequisiteVariety` | Ashby's law: counting, logarithmic and entropy forms, and the sensor bound | | `AISafetyAtlas.Control.RegulationCheck` | The counting law decided on a finite table, with the agreement theorem behind `atlas-check`'s `regulation` kind. A `true` verdict witnesses that Ashby's column hypothesis is satisfiable at that table | | `AISafetyAtlas.Control.ChannelRate` | Ashby §9/12 and §9/15: channel capacity as an entropy rate, and the entropy of a length of Markov chain | | `AISafetyAtlas.Control.CompleteControl` | Ashby §11/14: perfect regulation makes complete control possible, and what that costs the regulator | | `AISafetyAtlas.Control.InformationLimits` | Touchette–Lloyd: control loss, and feedback bounded by what the sensor measured | | `AISafetyAtlas.Control.Observability` | Touchette–Lloyd Theorems 5 and 6 and Corollary 7: sensor loss and perfect observability | | `AISafetyAtlas.Control.OpenLoop` | Touchette–Lloyd Lemma 8 and Theorem 9: a pure open-loop controller is optimal | | `AISafetyAtlas.Control.OpenLoopAttainment` | Touchette–Lloyd eq. (48): the maximum over input distributions is attained, by simplex compactness | | `AISafetyAtlas.Control.PolicyKernel` | Touchette–Lloyd eq. (28) as a minimum over kernels, attained by deterministic state feedback | | `AISafetyAtlas.Control.Purification` | Touchette–Lloyd eq. (7): every actuation kernel is a deterministic map of an exogenous seed, so Theorems 9 and 10 hold at printed scope | ## Single-surface domains One module carries the domain. Vendored or external proofs are re-exported where the result is not proved here. | Import | Domain | |---|---| | `AISafetyAtlas.Decision.MDP` | A **rewardless** Markov decision process `⟨S, A, T⟩` with `T : S → A → PMF S`, Turner and Tadepalli's Definition D.6, and the run it induces: an MDP, an observation map, and a policy over what is observed. Domain-neutral, and deliberately without a reward or a policy field — the reward is what a consumer adds, and the policy type is not part of the dynamics because a bare Markov decision process has no observation channel. `Wireheading.CRMDP` is its consumer | | `AISafetyAtlas.Decision.Expect` | The expectation of a real function under a probability mass function, written once. The corrupt-reward cluster and the discounted value layer arrived at it independently -- a `tsum` there because a corrupt-reward MDP has no finiteness to spend, a `Finset.sum` here because the contraction argument fixes a finite state space -- and `expect_eq_sum` is the bridge that makes them the same function. Carries summability for a bounded integrand, the point-mass value, additivity and the constant | | `AISafetyAtlas.Decision.DiscountedValue` | The **discounted** value layer above that carrier, with the reward `r : State → Action → ℝ` and the discount `γ : ℝ≥0` as parameters rather than fields: the two Bellman operators, each a `ContractingWith γ` map on `State → ℝ`, `vPi` and `vStar` as `ContractingWith.fixedPoint`, the Bellman equations and their uniqueness as theorems, and value iteration. The two *fixed points* are `Fintype` on `State` where the carrier is not; the three operator definitions are not, since none of them ever used it. **A foundation and not a join**: Turner and Tadepalli's D.10 is AVERAGE-optimal, D.8 to D.10 are stated nowhere in this repository, and the identification of `vPi` with a discounted return along `MDP.run` is owed | `AISafetyAtlas.Decision.BoundedValue` | The same policy Bellman operator under a second completeness argument: `vPiBdd` values a stationary deterministic policy on an arbitrary **`Nonempty`** state type, in exchange for a uniform bound on the reward, with the Bellman equation and uniqueness **among bounded solutions**. `vPiBdd_eq_vPi` is the join — on a finite nonempty state type the two value functions are one function, which is what makes this a widening rather than a second development. No bounded counterpart of `vStar`: the optimality operator maximises over actions with `Finset.sup'`. Registry row `LAND-BELLMAN-BDD-001` | `AISafetyAtlas.Combinatorics.Cascade` | The cascade representation of a natural number -- the positional system whose digits are binomial coefficients -- with its greedy digit, that digit's uniqueness, and the two Kruskal-Katona shifts, which move only the lower index and are therefore smaller than the multicomplex shift the same representation carries for Macaulay's theorem. Domain-neutral. The greedy-step arithmetic is adapted from `anthropics/fermats-last-theorem` under Apache-2.0; see the file header | | `AISafetyAtlas.Combinatorics.CascadeFamily` | The colex rank of a finite set -- the combinatorial number system -- as a counting principle: it bounds by the ground set, respects colex, and so ranks each layer bijectively onto an interval, which cuts a colexicographic initial segment of any requested size. With that, `cascadeShadow_le_card_shadow'` is **Kruskal-Katona in cascade form over an arbitrary ground type**, the numeric statement Mathlib's own file records as an open task. Domain-neutral | | `AISafetyAtlas.Combinatorics.KruskalKatona` | The Lovasz form of Kruskal-Katona with the ground type left arbitrary, which Mathlib's own file records as an open task: a sized downward-closed family large at one order is forced large at every lower one. Domain-neutral, and with no consumer in this repository: it is here as the general form of a bound the library would otherwise restate locally | | `AISafetyAtlas.Combinatorics.PermInvariance` | What invariance under relabelling forces, for functions and for relations: orbits, the multiset-of-values invariant, the counts, and the fact that an invariant relation is constant off the diagonal. Domain-neutral; `Learning.Sharp` is its consumer | | `AISafetyAtlas.Analysis.Blackwell` | Blackwell's sufficient condition — monotone plus discounting gives the sup-norm contraction estimate — and the bounded-continuous-function bridge that turns it into a Banach certificate on a state type carrying **no topology and no finiteness**, by manufacturing a discrete one on a type synonym. `existsUnique_bdd_fixedPoint` is stated for an arbitrary boundedness-preserving operator, not for a Bellman shape. Adapted from danlyng/Econlib at `003655cc`, Apache-2.0; it names no MDP, reward or policy, and its consumer is `AISafetyAtlas.Decision.BoundedValue` | | `AISafetyAtlas.Analysis.MaximalMinor` | A linearly independent family of vectors in a real coordinate space has a nonzero maximal minor: some square submatrix on that many rows is invertible. Domain-neutral and written to be lifted upstream; Mathlib carries only the square case, where there is nothing to choose | | `AISafetyAtlas.Order.FinsetRefinement` | Refinement of finite sets over a preorder — `A ⊑ B` when every element of `B` is matched by one of `A` at or below it. The upper (Smyth) preorder, and the reason it earns a name: dropping an element and moving up the order are the same move, and on a discrete carrier it is exactly reverse inclusion. Domain-neutral and written to be lifted upstream; Mathlib carries the upper-set and lower-set constructions and `Finset.sups` but not this relation on `Finset` at the pinned revision. no consumer in this repository yet, and `Examples.Order.FinsetRefinement` is its worked model | | `AISafetyAtlas.Analysis.NullImage` | A set covered by the image of a locally Lipschitz map from a strictly lower-dimensional coordinate space is Lebesgue null. Domain-neutral and written to be lifted upstream; it is the substitute this repository uses where semialgebraic dimension theory would usually be quoted, since Mathlib has neither semialgebraic sets nor o-minimality at the pinned revision | | `AISafetyAtlas.Analysis.PolynomialGenericity` | A nonzero real polynomial in finitely many variables is nonzero almost everywhere, for any product of atomless measures, hence for Lebesgue and for any additive Haar measure. Domain-neutral and written to be lifted upstream; Mathlib carries only the finite-grid sibling `MvPolynomial.schwartz_zippel_totalDegree` | | `AISafetyAtlas.Analysis.Semialgebraic` | Semialgebraic subsets of a real coordinate space `ι → ℝ`, as a finite union of polynomial sign conditions, closed under the Boolean operations. Domain-neutral and written to be lifted upstream; Mathlib has no such notion at the pinned revision. `Causal.ParameterChart` is its consumer, for MAIS-A2 `prob:exact` | | `AISafetyAtlas.Computability` | Rice / halting (Mathlib wrappers) | | `AISafetyAtlas.Explainability` | Attribution impossibility | | `AISafetyAtlas.Fairness.RiskAssignment` | Kleinberg–Mullainathan–Raghavan Theorem 1.1: calibration within groups and balance for both classes force perfect prediction or equal base rates (`BY-010`) | | `AISafetyAtlas.Goodhart.Regressional` | Regressional Goodhart on a two-variable carrier: an independent goal and noise, the proxy their sum, and the theorem that selecting on the proxy raises the expected proxy-goal gap -- non-strictly for any integrable noise, strictly where the threshold cuts the noise law on a positive-mass set of goal values, and unconditionally strictly for `ProbabilityTheory.gaussianReal` at nonzero variance. Atlas-original: the model is Manheim and Garrabrant's equation (1) but the paper numbers no statement, so this is a sharpening of prose and not coverage of a printed theorem | | `AISafetyAtlas.Examples.Goodhart.Regressional` | A fair coin flip for the goal and another for the noise, threshold `1/2`: selected mass `3/4`, expected gap `1/2` unconditionally against `2/3` conditionally, all exact. Also shows the cut set has to be proper -- at goal value `1` the state is selected whatever the noise does | | `AISafetyAtlas.Goodhart.Overoptimization` | Zhuang and Hadfield-Menell Theorem 1 at print's binders: a proxy utility built from a nonempty strict subset of the attributes, completely optimized along a feasible convergent path, leaves every attribute it omits at that attribute's lower bound. The core is wider -- an arbitrary attribute type and a maximizer in place of the sequence -- and two corollaries say what it costs: the limit is the pointwise least feasible state carrying its proxy attributes, so the proxy-goal gap there is maximal on its own level set | | `AISafetyAtlas.Examples.Goodhart.Overoptimization` | Two attributes on a unit budget, the first of them the proxy, optimized along `![1 - Real.exp (-t), Real.exp (-t)]`: the unmentioned attribute lands on its floor, the principal's utility falls from `2` to `1` and the proxy-goal gap rises from `-2` to `0`, exactly. Also the empty proxy attribute set, where every hypothesis but nonemptiness holds and the conclusion fails | | `AISafetyAtlas.Goodhart.Extremal` | Extremal Goodhart, both of Manheim and Garrabrant's sub-variants: selection above the proxy's bound on the region where the goal-proxy relationship was fitted lands only outside that region, and there the observations underdetermine the goal by any amount you name -- for every goal fitting the learned relationship, a second one fits equally well, agrees with it on the whole observed region and is off by a prescribed constant on the whole selection event. Print's Change in Regime model is transcribed as `regimeGoal` and shown to realise that underdetermination, with the extrapolation error equal to the difference of its two offsets. Atlas-original, like `AISafetyAtlas.Goodhart.Regressional`: the paper numbers no statement | | `AISafetyAtlas.Examples.Goodhart.Extremal` | Print's own two examples, exactly: the underfitted cubic `x + x ^ 3 / 10`, within `1/10` of the linear fit on `[-1, 1]` and off by `100` at the selected state `10`; and the wind-speed instrument reading `5` low above its design tolerance of `30`, right at a measured `20` and wrong by exactly `5` at a measured `40`. Both selection events are shown non-empty | | `AISafetyAtlas.Goodhart.RegulatoryTarget` | Bridge: a bright-line rule over a measured indicator. Because a bar sits above everything its evidence base exhibits, every certified system is one that evidence never covered, and there the fitted indicator-risk link permits the risk to be off by any amount named. Raising the bar moves the certified set further from the evidence, not closer. The positive half is stated first: inside the evidence base the indicator predicts risk to the tolerance it was fitted at | | `AISafetyAtlas.Examples.Goodhart.RegulatoryTarget` | A link fitted exactly on systems scoring at most `1` and a bar at `2`: the fit is perfect where it was taken (`ε = 0`), `3` is certified and was never examined, and the displacement at every certified system is arbitrary -- at a bar of `100` as much as at `2` | | `AISafetyAtlas.Fairness.ApproximateRiskAssignment` | The same paper's Theorem 1.2: the `ε`-approximate conditions force an `f(ε)`-approximate form of one of the two conclusions (`BY-010`) | | `AISafetyAtlas.Inference` | Wolpert inference devices: weak/strong inference, Wolpert's own notion of control over a device, physical knowledge. **Not** Ashby or Touchette–Lloyd control — for those see `AISafetyAtlas.Control` | | `AISafetyAtlas.Learning` | Finite NFL cores | | `AISafetyAtlas.LinearSystems` | The Kalman rank criteria and the Hautus eigenvalue tests for observability and controllability of a linear time-invariant system, with the duality between the two sides. `Dynamics` carries print's two equations themselves -- `IsTrajectory` is `ẋ = Ax + Bu` and `outputSignal` is `y = Cx` -- and `Flow` carries the matrix exponential and variation of constants. **Both criteria are proved equivalent to the properties they are criteria for**: the output determines the state exactly when the observability matrix has full rank, and the system is completely state controllable exactly when the controllability matrix does. The Lean is adapted from `AnandGokhale/LeanForControl` (Apache-2.0); per-file headers carry the provenance | | `AISafetyAtlas.Learning.Sharp` | The closed-under-permutation NFL characterization, both directions (`CT-10`) | | `AISafetyAtlas.Logic` | Incompleteness / undefinability | | `AISafetyAtlas.SelfAwareness` | Bounded process-compositional limits on complete self-awareness | | `AISafetyAtlas.SocialChoice` | Arrow / Gibbard–Satterthwaite | | `AISafetyAtlas.SocialChoice.Utility` | Arrow over utility profiles | ## Partial aggregate `Verification` re-exports `Computability` and stops there: neither bridge module below arrives with it. | Import | Domain | |---|---| | `AISafetyAtlas.Verification` | Behavioral verification core | | `AISafetyAtlas.Verification.AgentBehavior` | Downstream consumer of `Verification.rice` | | `AISafetyAtlas.Verification.Containment` | Alfonseca et al. Theorem 1: no total decider for an arbitrary effect predicate | | `AISafetyAtlas.Verification.Robot` | Verification limits for reactive robot programs | | `AISafetyAtlas.Verification.FullAccess` | Bridge: two questions about one source at maximal access -- an extensional one no total verifier answers, and a syntactic one a verifier does. What Rice bounds is the behavioral half, and what fails is extensionality, not access | | `AISafetyAtlas.Oversight.VarietyBound` | Bridge: seeing and doing are independent oversight capacities, proved in both directions. Not re-exported by `Oversight.JointObservation` | | `AISafetyAtlas.Oversight.VarietyCheck` | The executable side of that bridge, with its agreement theorem. Backs `atlas-check`'s `variety` kind | ## Peer modules `InformationTheory` and `Causal` have no aggregating parent. Import the one needed. For `InformationTheory` that is because each module is one result and none is built on the others. For `Causal` the reason is stronger: the domain holds **two different objects**, and an aggregating parent would force a consumer of one to take the other. `Causal.Model` is a causal Bayesian network — a graph with conditional probability tables. `Causal.StructuralModel` is Everitt's structural causal model, influence diagram and SCIM, where all randomness sits in exogenous variables and the endogenous ones are related deterministically. Neither is a special case of the other as rendered here. The remaining modules are the MAIS-A2 support layer and are built on the network, not on the structural model. The two entropy modules take their entropy layer from PFR rather than from `AISafetyAtlas.Inference.entropyOn`, which is a separate Wolpert-specific development and is not migrated; | Import | Domain | |---|---| | `AISafetyAtlas.Causal.Model` | Finite categorical CBN construction over an ordered field: RE24 local maps and Pearl-style products, not Pearl Definition 1.3.1 | | `AISafetyAtlas.Causal.BayesianNetwork` | Pearl Definition 1.3.1 as a condition on a family of interventional distributions, the truncated product derived from it, and the kernel as an instance | | `AISafetyAtlas.Causal.MarginClass` | Conditions (M1)–(M6): categorical A2 composite, not a RE24 or Uhler definition | | `AISafetyAtlas.Causal.Decision` | Generic finite unmediated policies, expected utility, and regret; not a full CID or RE24 Theorems 1–2 | | `AISafetyAtlas.Causal.DecisionNetwork` | RE24 Definition 4 with the decision and the utility as **vertices**: expected utility, optimality and regret on the diagram, with Assumption 1 a hypothesis rather than a shape. `Causal.Decision` is its unmediated projection, and `DecisionNetwork.expectedUtility_eq_value` proves the two agree under Assumption 1 | | `AISafetyAtlas.Causal.ParameterChart` | MAIS-A2's `K(G)` free table coordinates and Lebesgue measure on them: the layer MAIS-O24 is phrased in, not any of its three conclusions | | `AISafetyAtlas.Causal.EffectiveGenericity` | MAIS-O24's rational polynomial certificate, the class `M(sk,lambda,mu)` it cuts, conclusions (a)-(c), the size and construction-time bounds, and the bundled `O24Solution` carrying all of them | | `AISafetyAtlas.Causal.Query` | MAIS-A2 `subsec:queries`: rational-weight queries against real tables, randomized adaptive analysts, expected error, and the minimax risk and `N(ε)` its query problems are stated over. The policy-probability oracle only; sampled and corrupted actions are not here | | `AISafetyAtlas.Causal.ModelSpace` | Rounding a model's tables onto a grid: the estimate moves by `O(ε)` and rounded models form a countable set, which is the mathematical content of the query layer's countable-support repair | | `AISafetyAtlas.Causal.Goal` | MAIS-A2's goal formalism: sub-goals over the three temporal operators, sequential goals with print's recursive achievement times, composite goals as **sets** of disjuncts, and the counting bound on the composite goals that carry no immediately winnable disjunct. Syntax and trajectory semantics only -- no environment, no policy, no probability | | `AISafetyAtlas.Causal.ControlledProcess` | MAIS-A2's environment: a finite stationary controlled Markov process, print's communicating condition and the one-step route to it, entrywise sup-norm separation, and the disjoint-reconstruction-ball fact any indistinguishability argument needs. No agents, no trajectory law | | `AISafetyAtlas.Causal.GoalDynamics` | Deterministic goal-conditioned policies, the trajectory law they induce by Ionescu-Tulcea, the achievement probability, and print's `(δ,n)`-bounded agents with the best achievable read as a supremum rather than the maximum print presupposes | | `AISafetyAtlas.Causal.Corruption` | MAIS-O33's query side: print's first-action data, `η`-corruption counted against `𝐒 × 𝚿_n`, a randomized analyst with no query budget, and the indistinguishability theorem a common corruption of two far-apart worlds discharges | | `AISafetyAtlas.Causal.StructuralModel` | Structural causal models with exogenous noise, submodels and soft interventions, causal influence diagrams, structural causal influence models and materiality: Everitt et al. 2021 Definitions 1-5. `CID.isWellFounded_of_fintype` records that at a finite vertex set the evaluability class follows from print's bare `acyclic`, so any statement already carrying `[Fintype V]` can drop it. A different object from `Causal.Model`, which is a causal Bayesian network | | `AISafetyAtlas.Causal.DSep` | Everitt et al. 2021 Definition 6, stated at print's generality: overlapping source, target and conditioning sets, which the paper's own footnote 5 flags as intended and which upstream's `dSep` excludes by requiring pairwise disjointness. Clauses 1 and 2 are carried from `Causalean`; clause 3, the endpoint rule, is this file's, together with the Bayes-Ball equivalence that makes the result decidable and the recovery of upstream's predicate at disjoint sets | | `AISafetyAtlas.Causal.Requisite` | Everitt et al. 2021 Definition 7, nonrequisite and requisite observations: d-separation of an observation from the utility nodes downstream of the decision, given the other observations and the decision. Stated at an arbitrary vertex rather than only at observations, and without print's single-decision restriction, neither of which the condition uses; the disjointness lemma does ask that the decision be a decision, because a utility node may have parents and would otherwise sit in its own conditioning set | | `AISafetyAtlas.Causal.Incentive` | Everitt et al. 2021 Definition 17 and Theorem 18, both directions: nested potential responses, conditioning on a decision context, the instrumental control incentive, and the witnessing model its completeness half constructs. The one incentive criterion in that paper that needs no d-separation, and stated wider than print -- soundness at no hypothesis, completeness at `DecisionFree` rather than at a single-decision diagram | | `AISafetyAtlas.Examples.Causal.Model` | A ternary-root, binary-child model exercising translation, a non-injective local map, and general normalization | | `AISafetyAtlas.Examples.Causal.BayesianNetwork` | The kernel as a Pearl causal Bayesian network, and a family whose members are truncated products but which is not one | | `AISafetyAtlas.Examples.Causal.BehavioralCollision` | Three models on two binary variables with one behavior. The construction submitted against MAIS-O23, machine-checked | | `AISafetyAtlas.Examples.Causal.O24Refutation` | MAIS-O24's conclusions (a) and (c) shown incompatible: an open box of behavioural collisions, a certificate polynomial forced to vanish on it, and (c) contradicted at the utilities beside the collision. `O24Solution` is empty | | `AISafetyAtlas.Examples.Causal.Goal` | The goal formalism on two states and two actions: each temporal operator exercised, the *Eventually* achievement time checked at the least hitting time, a depth-two goal satisfied and an unreachable one refuted, and the three counts evaluated | | `AISafetyAtlas.Examples.Causal.ControlledProcess` | The two separated environments of MAIS issue #9: positive everywhere hence communicating, `4/5` apart at one entry, and their reconstruction balls disjoint at `n = 101`, `δ = 1/2` — which is why the candidate does not need `δ = 0` | | `AISafetyAtlas.Examples.Causal.GoalDynamics` | The first-action map read off a branching agent, the empty goal achieved with probability zero, and `IsBounded` inhabited over a one-action environment — the non-vacuity check the predicate needs | | `AISafetyAtlas.Examples.Causal.O33Corruption` | MAIS-O33 refuted: two action-independent worlds `4/5` apart at `n = 101`, `δ = 1/2`, `(δ,n)`-bounded agents in each agreeing off a doubly exponentially small set of goals, and one corruption serving both. No positive corruption fraction is uniformly tolerable | | `AISafetyAtlas.Examples.Causal.Decision` | The collision's shared zero-regret policy family, plus two margin-class models with opposite optimal action at one mixture | | `AISafetyAtlas.Examples.Causal.ModelSpace` | A three-state table rounded by hand, and the witness that the `dim c` factor in the error bound is not slack | | `AISafetyAtlas.Examples.Causal.StructuralModel` | A two-variable structural model where evaluation needs a real recursion, and a diagram whose childless-utility clause is shown to bite | | `AISafetyAtlas.Examples.Causal.DSep` | The witness that Definition 6 is wider than the library under it: a configuration where a source node is conditioned on, at which print's d-separation holds by its endpoint clause and upstream's predicate fails because disjointness is one of its conjuncts. Stated once for every diagram, then run on a two-vertex diagram, with the d-connected case showing the definition is not vacuously true | | `AISafetyAtlas.Examples.Causal.Requisite` | Definition 7 run in both directions: a three-vertex prediction diagram whose observation feeds the utility node directly, so it is requisite by one exhibited path, and a diagram with no utility node at all, where every observation is nonrequisite for want of anywhere to go. The paper's own Figure 3a discrimination is **not** here and the module says why -- `cidToDAG` supplies classical decidability, so the Bayes-Ball computation cannot run and establishing nonrequisiteness on a real graph would quantify over every path | | `AISafetyAtlas.Examples.Causal.Incentive` | A chain `D → X → U` with a fourth vertex off it: Definition 17 met on `X` against every policy, and Theorem 18 run in both directions -- admitted on `X`, refused on the isolated vertex. A second, two-decision diagram that print's Theorem 18 does not quantify over and the widened criterion still decides | | `AISafetyAtlas.Examples.Causal.OneNodeClass` | One binary chance variable, unobserved, with a straddling utility gap. The margin class is the interval `[λ, 1-λ]`, and it meets all eight clauses of MAIS-O25's antecedent — the inhabitant that makes the conjecture non-vacuous | | `AISafetyAtlas.InformationTheory.PrefixCode` | A self-delimiting three-symbol code, the composition lemmas that build compound encoders from atomic ones, and print's sparse monomial syntax spelled out with them. Domain-neutral source coding; `Causal.EffectiveGenericity` is its consumer, for MAIS-O24's construction-time clause | | `AISafetyAtlas.InformationTheory.Fano` | Fano's inequality for an arbitrary estimate on any probability space | | `AISafetyAtlas.InformationTheory.DataProcessing` | Markov chains, the mutual-information chain rule, data processing and its equality case | | `AISafetyAtlas.InformationTheory.ChannelCapacity` | Capacity of a discrete noiseless channel, with repeated use and parallel composition as lemmas. `Control` is one consumer, not the owner | | `AISafetyAtlas.InformationTheory.Determinism` | One lemma: a function of a variable adds no uncertainty to it. Three consumers in two domains | ## Kernels and specializations Import the specialization needed; the parent does not supply it. | Import | Domain | |---|---| | `AISafetyAtlas.Knowledge` | Exact knowability and observation-factorization (kernel) | | `AISafetyAtlas.Knowledge.Embedded` | Abstract embedded-measurement and meshing limits | | `AISafetyAtlas.Knowledge.Embedded.Composition` | Product/equivalent complement ⇒ proper inclusion and the bijective positive boundary | | `AISafetyAtlas.Knowledge.Embedded.Finite` | Finite cardinality gap ⇒ proper inclusion (operational) | | `AISafetyAtlas.Knowledge.Temporal` | Time-indexed knowability, collisions, delayed knowledge | | `AISafetyAtlas.Knowledge.Ambiguity` | Finite fibre ambiguity and the counting obstruction | | `AISafetyAtlas.Knowledge.SelfReference` | The model as a component of the state it models | | `AISafetyAtlas.Knowledge.Accumulation` | Window ambiguity: never decreases, at most multiplies | | `AISafetyAtlas.Knowledge.Devices` | Transports between the knowability kernel and Wolpert inference devices | | `AISafetyAtlas.Knowledge.Entropy` | The kernel measured: knowability forces zero conditional entropy, positive conditional entropy certifies unknowability, and Fano through data processing bounds every decoder's error rate | | `AISafetyAtlas.Knowledge.UniformAction` | Acting acceptably without identifying the state: the uniform decision boundary, its fibre certificate, and the two repairs | | `AISafetyAtlas.Knowledge.Check` | Executable checkers for the kernel and the transports, with agreement theorems | | `AISafetyAtlas.Knowledge.Audit` | Bridge: a measurement taken at audit time and the version deployed later -- the *when* axis | | `AISafetyAtlas.Knowledge.Access` | Bridge: black-box, score and white-box access as three points of the informativeness order -- the *how much* axis | | `AISafetyAtlas.Preference` | Planner/reward unidentifiability, BY-011 (kernel) | | `AISafetyAtlas.Preference.Complexity` | Simplicity does not break the planner/reward tie | | `AISafetyAtlas.Preference.Reasonable` | Basic operations and Proposition 7 | | `AISafetyAtlas.Preference.SourceComplexity` | Propositions 7 and 8 in the source's own parameterization | | `AISafetyAtlas.Preference.Override` | Overriding human reward functions | | `AISafetyAtlas.Preference.Regret` | Half-maximal regret is not ruled out by observation | | `AISafetyAtlas.Preference.Knowability` | Reward unidentifiability as a `Knowledge.Knowable` obstruction | | `AISafetyAtlas.Causal.Knowability` | Behavioural identifiability as a `Knowledge.Knowable` factorization | | `AISafetyAtlas.Sovereignty.Boundary` | Sovereignty as immunity inside a boundary: the boundary is a view of the outcome rather than a set of them, and a coalition is sovereign when nothing outside it moves that view. Proves sovereignty is exclusive power over the boundary -- the holder forces its own view, and no coalition has power at any target the boundary expresses -- and adds a curtailment layer where an outsider shrinks the available actions, which is strictly stronger than any outcome-level reading. Neighbours named in the module: republican non-domination, rights as effectivity functions, and opportunity-set freedom | | `AISafetyAtlas.Sovereignty.Arena` | Power without a game form: one party settles `Ctl`, everything else is an opaque `Res`, and the two resolve to an outcome. Forcing, collapse, decisiveness, sovereignty and dictation are stated once at this level, so the game-form, mediated and oversight notions are instances rather than parallel developments. Sovereignty and dictation are shown to be the same predicate under `∀` and `∃`. Power-over is deliberately absent: comparing across another party's commitments needs the residue to be structured, which an arena does not carry | | `AISafetyAtlas.Sovereignty.Playability` | Checks coalition logic's playability conditions against `effectivity`: liveness, safety, N-maximality, outcome monotonicity, superadditivity, regularity, and a principal element at the empty coalition, which is `Set.range outcome`. Three conditions were already theorems under other names and regularity is Gaerdenfors' consistency condition reused, so what is new is liveness, N-maximality and the principal element. The correspondence is checked against Pauly 2002 page 152, read from the rendered page. This is the easy direction of his Theorem 3.2; the converse, its four-part construction and its refutation are in `PlayableConverse`. Also carries his **Theorem 3.3**: an effectivity function is individualistic -- everything the grand coalition forces, some individual already forces -- exactly when some player forces every reachable outcome. The whole is equal to the sum of its parts only when it equals one particular part | | `AISafetyAtlas.Sovereignty.PlayableConverse` | Pauly's Theorem 3.2 from the other side: playability as a predicate on an abstract effectivity function, his Lemma 3.1, superadditivity over a finite family of disjoint coalitions, and his whole page-153 construction -- strategies as `(f_i, t_i, h_i)`, the intersection `G(f)`, the dictator picked by summing indices, and the game. Both inclusions of `E_G = E` are proved with the side conditions print's argument needs: the first wants a non-empty coalition, the second one that is not everybody, so the equality holds off the two ends of the coalition lattice. Carries the **refutation of the converse**, which is Goranko, Jamroga and Turrini's (JAAMAS 26: 288-314, 2013) and not this atlas's -- the cofinite filter on the natural numbers is a playable effectivity function on one player that is no game form's, because `effectivity G` at the empty coalition always has a least element and a filter on an infinite set need not -- so the missing ends are false rather than unproved. Names the step of the printed proof that fails, and records that N-maximality is consumed by nothing | | `AISafetyAtlas.Sovereignty.TrulyPlayable` | Goranko, Jamroga and Turrini's repair of Pauly's Theorem 3.2 (JAAMAS 26: 288-314, 2013): the nonmonotonic core of a coalition's choices, its completeness, and truly playable as playable plus a complete core at the empty coalition. Their Proposition 1 -- `E(∅)` is a filter and its core is empty or a singleton -- with the load-bearing half stated on its own, that a **minimal** element of `E(∅)` is automatically a **least** one, which holds because `∅` is the only coalition superadditivity can apply against itself. Their Proposition 5 (1) iff (2) iff (3), so true playability, a non-empty core and a principal `E(∅)` all coincide. Their Proposition 2, that a game form's core at `∅` is the singleton of its reachable set. The separating fact in their own terms: the cofinite filter's core at `∅` is empty because no cofinite set is minimal, which re-proves `PlayableConverse`'s refutation by print's route. **Wider than the only other formalization**: `kaiobendrauf/cl-lean` reaches true playability from a finite outcome type, and the argument needs only a minimal element of the family, so the finite-type version is two corollaries down | | `AISafetyAtlas.Sovereignty.Retargetable` | Turner and Tadepalli 2022 section 3, whole: orbits under a group action on a parameter set, the `MostOrbit` counting relation, simple and multiple retargetability, and the theorem that an `n`-retargetable decision-maker favours `B` at `n` times as many orbit parameters as it favours `A`. Finite combinatorics -- no Markov decision process, no measure, no reward. Stated for an arbitrary group where print takes the symmetric group. **Not a result about power**: `A` and `B` are labels, and print's own footnote says no further structure is demanded | | `AISafetyAtlas.Sovereignty.EUDetermined` | Turner and Tadepalli 2022, appendix B.2 and theorem A.13: the chain from the section 3 counting theorem to expected-utility-determined decision-makers -- lemma B.7, definition B.8, lemma B.9, lemma B.10, definition A.12 and lemma B.11. Also definition A.7 with print's involution clause, which `Retargetable` drops and lemma B.7 needs. **Still not a result about power**: `A`, `B` and `C` are finite sets of vectors, and the paper's power reading is its appendix D, which instantiates them as recurrent state distributions in a Markov decision process | | `AISafetyAtlas.Sovereignty.Separations` | α-forcing countermodels: superadditivity holds under domination, wider targets are free, and the three readings of delegated authority are three obligations | | `AISafetyAtlas.Sovereignty.ConcurrentGameFrame` | Chen, Ju and Ågotnes (arXiv:2607.10567) at print's own carrier: an action frame with a state set, state-indexed availability and a joint action whose outcome is a **set** of successor states. Definition 1, Definition 5's alpha and actual effectivity functions, Definition 8's two conditions with `ActionFrame.ofGrand` making print's *"determined by the grand-coalition outcome function"* a construction, Definition 9's three conditions and the eight labels, and Fact 1's two items. Coalition monotonicity of alpha powers is proved **without** seriality, where the game-form version carries it. `gameFrame` is the bridge that places `GameForm` at the `SID` corner -- the state set is the outcome type with state-independent dynamics, not a point -- and identifies `Forces` and `ActualPower` as its alpha and actual effectivity functions. No representation theorem is claimed | | `AISafetyAtlas.Examples.Sovereignty.Playability` | The principal element at both extremes: `vetoGame` settles nothing so the empty coalition forces only the whole space, `pinnedForm` settles everything so it already forces the outcome. Playability holds either way, which is why it is not a strength claim | | `AISafetyAtlas.Examples.Sovereignty.PlayableConverse` | Both sides of the separation on concrete objects: the veto game's effectivity function is playable, Lemma 3.1 runs on it, and rebuilding the game from it through `paulyGame` returns the same power at each singleton coalition -- while the cofinite effectivity function is playable and no game form's. Also why the witness needs only one player: on one player there is no coalition meeting both side conditions | | `AISafetyAtlas.Examples.Sovereignty.TrulyPlayable` | Both sides of the separation: the veto game is truly playable and its core at the empty coalition is the singleton of its reachable set, while `cofiniteEff` is playable, is not truly playable, and has an empty core. The three routes to true playability -- minimal element, finite family, finite outcome type -- run on the same game, and the cofinite filter shows the hypothesis is not free | | `AISafetyAtlas.Examples.Sovereignty.Retargetable` | A two-parameter decision-maker the swap retargets, so the retargetability hypothesis is inhabited and the counting theorem says something about an actual object | | `AISafetyAtlas.Examples.Sovereignty.EUDetermined` | A Boltzmann-shaped selection weight on two coordinates that satisfies every hypothesis of theorem A.13, with a parameter at which the losing option set is strictly preferred, so the counting conclusion is not about an empty set | | `AISafetyAtlas.Examples.Sovereignty.Arena` | A two-choice arena separating dictation from sovereignty: one choice settles the outcome and the other surrenders it, so the party can set what the boundary shows without holding it. The witness that `Arena.Sovereign.dictates` is strict | | `AISafetyAtlas.Examples.Sovereignty.Boundary` | A two-coordinate game on which the boundary notions run: the holder is sovereign over its own coordinate, not over the whole outcome, still subject to power at a target the boundary cannot express, and sovereign while having power over the other party. Plus the action-set separation -- an outsider removes an option and the reach is unchanged, so losing options is invisible at the outcome layer | Each module docstring lists **primary** declarations (laws / instances / boundaries). Prefer those names over diving into `Upstream/` unless editing a vendored proof. -/