{ "schema_version": 1, "next_id": 29, "description": "Open questions and their settled ledger records. An OPEN conjecture is a compiling Lean statement with no proof and asserts nothing; every RESOLVED row separately names the checked proof that settled it. Conjecture modules live under AISafetyAtlas.Conjectures.*, are never on the atlas root import, and never enter theorem counts. Tag vocabulary is shared with registry.yaml.", "conjectures": [ { "id": "CONJ-002", "kind": "claim", "problem": "", "statement": "Wolpert 2008 section 8's collapse of stochastic inference complexity to Definition 6 at accuracy 1 genuinely needs its no-null-point hypothesis. `stochasticInferenceComplexity_eq` proves `C-bar_1(Gamma | C) = script-C(Gamma | C)` under the source's `P proportional to d-mu` condition, rendered as `hatom` in the single-measure formulation this atlas uses: no point of the space is null. The conjecture is that theorem with `hatom` deleted and nothing else changed, negated -- so a counterexample is a probability space, device, length function and target meeting every remaining hypothesis, including measurable agreement and positive mass on every realized setup fibre, at which the two complexities differ.", "refutation": "Prove `stochasticInferenceComplexity_eq` without `hatom`, leaving every other hypothesis in place. That shows the hypothesis was never needed and the theorem can simply be strengthened.", "prior_art": "D. H. Wolpert, Physical limits of inference, Physica D 237(9):1257-1281, 2008, §8 running text after Definition 10 (survey-ref-005). The source states the equality with the proportionality condition and gives no proof of either direction; the `≤` direction is `stochasticInferenceComplexity_le` and needs no such condition. No source consulted addresses necessity. The distinction is the standard measure-zero versus empty gap and is not specific to this paper, but the atlas found no statement of it for this quantity.", "lean": "AISafetyAtlas.Conjectures.StochasticComplexity.eq_needs_no_null_points", "lean_module": "AISafetyAtlas.Conjectures.StochasticComplexity", "answer_candidate": [], "answer_admissible": [], "answer_correct": [], "admissibility_status": "NotApplicable", "blocked_on": "", "absent_declarations": [], "tags": [ "information-theory", "computational-complexity" ], "proposed_by": "Atlas review of the Wolpert section 8 prose layer. The hypothesis is carried by `stochasticInferenceComplexity_eq`; its necessity is asserted nowhere in the source and is not proved here.", "status": "OPEN", "resolution": "", "source_ref": [ "survey-ref-005" ], "context_source_ref": [], "source_scope": "Beyond", "source_fidelity": "AtlasOriginal", "source_note": "Beyond/AtlasOriginal, corrected from Same/Literal on 2026-08-21. There is no printed sentence here to transcribe, and the entry's own fields said so two rows away: prior_art records that Wolpert 2008 section 8 'gives no proof of either direction' and that 'No source consulted addresses necessity', while proposed_by records that the hypothesis's necessity 'is asserted nowhere in the source'. Grading that Literal claimed a printed counterpart the paper does not contain. What the source does contain is the equality itself, which the atlas proves as stochasticInferenceComplexity_eq; the question of whether its hypothesis is needed is the atlas's, asked about that result. survey-ref-005 stays in source_ref as the artifact the question is about. One reading choice is worth recording and previously had nowhere to go: the negated universal is pinned at Type 0 rather than left polymorphic, because Checks.lean cannot name a universe-polymorphic Prop without metavariables. Restricting a *negated* universal makes the claim strictly stronger, so this is not a narrowing -- a Type 0 counterexample refutes the polymorphic theorem." }, { "id": "CONJ-003", "kind": "claim", "problem": "MAIS-O26", "statement": "MAIS-A2 Conjecture 4.4 (MAIS-O26), at print's own class: for every solution to MAIS-O24 and every skeleton over a finite set of binary chance variables with real tables, if the class MM(sk,lambda,mu) cut by that solution's polynomial list has a linear recovery modulus L below an explicit threshold over the printed identified set, and K is def:margin's chart maximum over the margin class, then the randomized exact-policy-probability minimax budget N(epsilon) is finite and Theta(K log(1/epsilon)) as epsilon tends to zero, under one uniform polynomial bound in 1/lambda, 1/mu and L whose coefficient and degree are chosen after the O24 solution is fixed but before the diagram, its size and the margins -- which is print's own order, since prob:effective closes \"Fix one list supplied by a solution\" and conj:exact asks for constants independent of m.", "refutation": "The route below is now provably unrunnable, and is kept as the record of what was tried. AISafetyAtlas.Examples.Causal.O24Refutation.isEmpty_o24Solution proves no O24Solution exists, so no instance of the antecedent can be supplied and the printed Prop is true rather than false. Conditional refutation route, formalized but not inhabited. Give an O24 solution, a skeleton and margins whose cut class is empty, satisfies O26ClassAssumptions, and has chart dimension K >= 1. AISafetyAtlas.Examples.Causal.Query.exactMinimalBudget_emptyClass proves that the actual randomized minimax budget is zero on every nonnegative target for an empty class. AISafetyAtlas.Examples.Conjectures.MAIS.not_isThetaWithMarginBound_emptyClass proves that this violates the lower half of the printed Theta rate whenever K > 0. AISafetyAtlas.Examples.Conjectures.MAIS.not_maisO26_exactRate_for_of_empty combines those facts into the negation of the corresponding O26 instance. What the route needs is an instance of the antecedent -- an inhabitant of Causal.O24Solution, hence an answer to prob:effective -- and isEmpty_o24Solution proves there is none, so the route can never be run. Whether the missing nonemptiness condition is a defect in MAIS-O26 is a question about the source; the atlas states the source literally rather than adding it.", "prior_art": "MAIS-A2, Conjecture 4.4 and MAIS-O26. conj:exact opens 'For N = MM(sk,lambda,mu) with mu fixed', which is prob:effective's cut -- the margin class intersected with |Q^G_j(theta,u)| >= mu for a solution's own polynomial list. Since 2026-08-21 the atlas has that object, so the Prop cuts by Causal.O24Solution.marginClass rather than by a supplied genericity family. Conclusion (a), behavioural injectivity on the class, is O24Solution.identifies, a field of the bundle rather than an added antecedent. The two guards required by the old supplied-witness version -- IsProperGenericityCut and IsTightGenericityCut -- are absent because they are not in print. O26 names the linear recovery modulus through L, so HasLinearRecoveryModulus remains. It does not state compact semialgebraicity or the richness condition, so neither is carried here; both remain on O25, where prob:exact prints them. The declaration quantifies over every zero-regret policy family the adversary may fix, including arbitrary tie behaviour, and chooses one polynomial constant bound outside all problem parameters.", "lean": "AISafetyAtlas.Conjectures.MAIS.maisO26_exactRate", "lean_module": "AISafetyAtlas.Conjectures.MAIS", "answer_candidate": [], "answer_admissible": [], "answer_correct": [], "admissibility_status": "NotApplicable", "blocked_on": "", "absent_declarations": [], "tags": [ "interpretability", "computational-complexity" ], "proposed_by": "Atlas statement-only formalization of MAIS-A2.", "status": "RESOLVED", "resolution": "Resolved affirmatively and vacuously by AISafetyAtlas.Examples.Conjectures.MAIS.maisO26_exactRate_holds. The printed conjecture opens 'for every solution to MAIS-O24', and CONJ-012 records that there are none (AISafetyAtlas.Examples.Causal.O24Refutation.isEmpty_o24Solution), so the universal quantifier ranges over an empty domain. Read this for exactly what it is: it is a fact about conj:exact as printed and says nothing about the Theta(K log(1/epsilon)) budget the conjecture is about. The non-vacuity question this row carried since 2026-08-23 is closed in the negative -- the proposition was vacuous, and the empty-class refutation route recorded below can never be run, because its antecedent needs an O24Solution. A MAIS-O26 that says something would have to be stated over a class that does not come from a solution to prob:effective.", "source_ref": [ "mais-a2-2026" ], "context_source_ref": [], "source_scope": "Same", "source_fidelity": "Literal", "source_note": "Scope is Same from 2026-08-23, because the compact-semialgebraic hypothesis was removed rather than explained away. O26ClassAssumptions now contains only the validity conditions, the definition of K, and the linear recovery modulus named through L. IsCompactSemialgebraicClass remains on CONJ-006/O25, where prob:exact states it explicitly, but it is absent here because conj:exact does not state it. If the literal MAIS-O26 statement is false, vacuous, or intended to inherit more from O25, that is recorded as a source issue rather than repaired by an atlas-added premise. Literal is retained because this row transcribes the conjecture rather than selecting one answer branch. O24Solution.exists_o26ClassAssumptions proves formally that, at valid margins and a supplied IsClassChartDim witness, any hypothetical O24 solution supplies the linear recovery modulus needed by this row. Non-vacuity is settled in the negative: the proposition IS vacuously true, by AISafetyAtlas.Examples.Causal.O24Refutation.isEmpty_o24Solution, so no O24Solution inhabitant can ever be exhibited. Scope stays Same and fidelity stays Literal, because the row transcribes conj:exact and the vacuity is print's, not the transcription's -- which is precisely why the source issue was recorded here rather than repaired by an atlas-added premise. The statement freeze fired on maisO26_exactRate in the same change and the answer is that fidelity did not move: the Prop's body is unchanged and only @[expose] was added, so the definition unfolds outside its own module the way every other graded MAIS Prop in this ledger already does. It had to, because maisO26_exactRate_holds lives in Examples and cannot discharge a Prop it cannot unfold." }, { "id": "CONJ-004", "kind": "claim", "problem": "MAIS-O23", "statement": "MAIS-O23 has a negative answer, at MAIS-A2 q:ident's own quantifier: for some skeleton over a finite set of binary chance variables and some valid positive margin, two distinct models in the full six-condition margin class have equal masked behavioral transforms under every real intervention mixture.", "refutation": "A refutation would prove that no such pair exists. The checked pair in AISafetyAtlas.Examples.Causal.margin_class_not_identifiable prevents that: both models satisfy the margin class, are unequal, and satisfy BehaviorEq.", "prior_art": "MAIS-A2 Question 4.1 and MAIS issue #6. The issue gives a three-DAG collision and credits the earlier construction in issue #4. The atlas contribution is the finite rational Lean check of all margin conditions and equality on every mixture, not priority for the construction. Both narrowing axes are now closed generically rather than per-statement. Model and Skeleton carry a value field; Skeleton.marginClass_mapRat and Skeleton.behaviorEq_mapRat transport a rational witness into any characteristic-zero ordered field, keeping all six margin conditions and the whole behavioural family. margin_class_not_identifiable_real therefore states the collision on the source's own real chart: real-valued CPTs and every real mixture, not a rational restriction of either. The behavioural half is not a cast of the rational hypothesis, since real mixtures are not images of rational ones; the transport routes through agreement at each deterministic profile, which is a finite rational identity. The earlier ad-hoc ΔmaskReal bridge is deleted, superseded by that transport. The witness construction is MAIS issue #6's and the atlas claims no priority for it; the issue is the provenance of the witness, not the statement being graded, which is q:ident itself.", "lean": "AISafetyAtlas.Conjectures.MAIS.maisO23_marginsDoNotSuffice", "lean_module": "AISafetyAtlas.Conjectures.MAIS", "answer_candidate": [], "answer_admissible": [], "answer_correct": [], "admissibility_status": "NotApplicable", "blocked_on": "", "absent_declarations": [], "tags": [ "interpretability" ], "proposed_by": "MAIS issue #6, transcribed and machine-checked by the atlas.", "status": "RESOLVED", "resolution": "Coverage: this row is all of q:ident. Unlike prob:boltzmann and prob:starter-set, MAIS-O23 is a single question with no clauses, so RESOLVED here is the status of both this row's Lean Prop and the printed question -- as a decide-whether answered on its negative branch, which is what the Selected fidelity records. Resolved negatively on the source's real chart by AISafetyAtlas.Examples.Causal.margin_class_not_identifiable_real. The theorem supplies two distinct margin-class models over the reals with equal complete masked behavior. The witness pair is computed at Q by margin_class_not_identifiable and carried to R by Skeleton.marginClass_mapRat and Skeleton.behaviorEq_mapRat; the transport is not a cast of the hypothesis, since real mixtures are not images of rational ones, and it runs through Model.Δmix_eq_on_probMixture_iff reducing behavioral equality to the finitely many deterministic profiles. The source repository's issue remains under its own review process.", "source_ref": [ "mais-a2-2026" ], "context_source_ref": [ "mais-o23-2026" ], "source_scope": "Same", "source_fidelity": "Selected", "source_note": "Two corrections on 2026-08-21, neither affecting the scope grade. Fidelity was Literal and is Selected: q:ident asks 'If M, M' in MM(sk,lambda) satisfy Delta_M = Delta_M', must M = M'?', and the paragraph after the question environment adds 'I do not conjecture an answer.', which sits outside the question environment. The question itself closes with a second phrasing, recorded below. That is a decide-whether, and the Prop states its negative branch -- the genre graded Selected at CONJ-005 and CONJ-008, so Literal would be an inconsistency in this ledger rather than a reading of the source. And the graded source is now the agenda alone: mais-o23-2026, the GitHub issue supplying the witness construction, moved to context_source_ref, because a grade that answers to two artifacts at once does not say which of them the verdict is about. The statement being graded is q:ident; the issue is the provenance of the witness, and the atlas claims no priority for the construction. Scope stays Same: the Prop is at q:ident's own quantifier over skeletons, valid margins and the full six-condition margin class, on the source's real chart. Print gives two phrasings and the atlas answers both. q:ident closes 'Equivalently (by Proposition prop:equiv): can two distinct models in the margin class share a common family of optimal policies for every observation mask?' The Prop transcribes the FIRST phrasing, equal masked transforms, because that is the numerical object the witness is computed against. The second is discharged separately and in the direction that matters: Examples.Causal.margin_class_not_identifiable_shared_optimal exhibits two distinct margin-class models with different graphs sharing a policy family admissible at level 0, which is a common family of optimal policies, so the answer to the second phrasing is negative too. Only prop:equiv's forward half is needed for that and it is what is proved; the converse reconstruction from an arbitrary optimal-policy oracle remains sourced rather than formalized and is not used here. Recording this is a correction in the UNDER-claiming direction: the row answered print's second question and said nothing about it." }, { "id": "CONJ-005", "kind": "claim", "problem": "MAIS-O34(a)", "statement": "MAIS-O34(a) has a negative answer to its margin-sufficiency subquestion: within the binary two-variable one-edge family, positive margin alone does not force the global behavioral fibre to be a singleton.", "refutation": "A refutation would prove singleton fibres throughout the two one-edge graph shapes under margin alone. AISafetyAtlas.Examples.Causal.margin_class_not_identifiable_two_graphs supplies opposite one-edge graphs in the class with equal behavior.", "prior_art": "MAIS-A2 Problem 5.2(a), MAIS-O34, and MAIS issue #4. The registered proposition covers only the precise yes/no margin-sufficiency clause, not O34's requested full semialgebraic classification, first-order constants, or graph-threshold program. margin_class_not_identifiable_two_graphs_real states the two-graph witness on the source's real chart through the same value-field transport used for O23, so both the model axis and the mixture axis are closed here as well.", "lean": "AISafetyAtlas.Conjectures.MAIS.maisO34_marginAloneDoesNotIdentify", "lean_module": "AISafetyAtlas.Conjectures.MAIS", "answer_candidate": [], "answer_admissible": [], "answer_correct": [], "admissibility_status": "NotApplicable", "blocked_on": "", "absent_declarations": [], "tags": [ "interpretability" ], "proposed_by": "MAIS issue #4/#6 construction, transcribed and machine-checked by the atlas.", "status": "RESOLVED", "resolution": "Coverage: this row is the margin-sufficiency subquestion of prob:starter-set(a) only. MAIS-O34 has two clauses and RESOLVED here is the status of this row's Lean Prop, not of the printed problem. The rest of (a) -- the explicit semialgebraic singleton criterion -- is CONJ-009's, and (b) is covered by neither. Resolved negatively for the margin-sufficiency clause on the source's real chart by AISafetyAtlas.Examples.Causal.margin_class_not_identifiable_two_graphs_real: two models over the reals with opposite one-edge graph shapes satisfy the same margin class and have equal complete behavior. The rational witness margin_class_not_identifiable_two_graphs is carried to R by the same two transport lemmas. The remainder of O34 is not resolved by this entry.", "source_ref": [ "mais-a2-2026" ], "context_source_ref": [ "mais-issue-4-2026" ], "source_scope": "Same", "source_fidelity": "Selected", "source_note": "Scope is Same, corrected on 2026-08-21 after a narrowing was found and removed. The Prop had asked for M.parents != M'.parents, and carried no M != M' clause at all -- the graph clause implied one, which is why the narrowing read as harmless. prob:starter-set(a) asks to decide 'when the global fiber {M' : Delta_M' = Delta_M} is the singleton {M}; in particular ... whether margin lambda > 0 alone suffices'. The negative branch needs a nonsingleton fibre, so two distinct models and nothing more; a same-orientation collision at equal graphs answers print just as well and the old statement excluded it. The clause is now M != M', and the existing witness -- which does carry different graphs -- discharges the weakened statement unchanged, via Model.ne_of_parents_ne. The ledger read Same while the Prop was Narrower; that is recorded here rather than silently overwritten. Scope is Same on the remaining axes: prob:starter-set is stated over def:twovar's family MM_2(lambda) -- two binary variables, O empty, Z = {X,Y}, sixteen profiles -- so the two-variable restriction is print's own, and HasGraphEdge on both models is that family's one-edge condition rather than an atlas demand. Fidelity is Selected because part (a) says 'in particular decide whether margin lambda > 0 alone suffices', and the Prop states the negative branch of that decision. Part (a)'s other half, the explicit semialgebraic singleton condition, is CONJ-009; part (b) is a different problem and is not touched. The graded statement is the agenda's clause, not MAIS issue #4's. The issue makes a strictly stronger claim on the same point -- for *every* margin range 0 < lambda <= 1/3, the gap table with three entries -lambda and one +lambda admits a forward/reverse pair with identical transforms -- which is a parametric family the atlas does not state and whose proof would be a construction in lambda rather than a single witness. Grading this entry against the issue would make it Narrower; it is graded against prob:starter-set, where it is Same." }, { "id": "CONJ-006", "kind": "claim", "problem": "MAIS-O25", "statement": "MAIS-O25's two decide-clauses, at print's own scope, taking the yes branch of the poly-log bound and the no branch of the adaptivity question: there is one polynomial, fixed before any diagram or class, such that for every compact semialgebraic class of real binary causal models whose margin-class chart dimension is K, which is behaviorally injective, which has linear recovery over the printed identified set below an explicit threshold, and whose table-parameter projection contains a K(G)-dimensional box of side rho inside one fixed graph, the minimal budget N(epsilon) of the randomized exact policy-probability minimax risk is finite and at most that polynomial in (K, 1/lambda, L, 1/rho) times log(1/epsilon) for every epsilon in (0,1) -- and non-adaptive queries cost at most a constant factor more than adaptive ones.", "refutation": "Give a class satisfying ExactClassAssumptions for which no polynomial in (K, 1/lambda, L, 1/rho) fixed independently of the class bounds Causal.exactMinimalBudget by that polynomial times log(1/epsilon) -- including the case where that budget is top, since an infeasible target refutes a finite bound -- or for which the non-adaptive budget is infinite, or exceeds every constant multiple of the adaptive budget, as epsilon tends to zero.", "prior_art": "MAIS-A2 Problem 4.3 and MAIS-O25. The source asks to determine the rate and, in particular, to decide two things: whether N(eps) <= poly(K, 1/lambda, L, 1/rho) log(1/eps), and whether adaptivity gives more than a constant factor. The Lean proposition states one branch of each, and they point OPPOSITE WAYS: IsPolyLogBudget is the YES to the first -- the bound holds -- and NonadaptiveWithinConstant is the NO to the second, since the non-adaptive budget being within a factor c of the adaptive one is adaptivity NOT outperforming by more than a constant. The three axes that would otherwise make it Mixed are closed: real tables, prob:exact's compact semialgebraic class with its literal K(G)-dimensional box, the printed identified set in the recovery modulus, and the randomized-analyst infimum of subsec:queries with an Nat-infinity-valued N(eps). The last axis, the estimator's output law, closed too: the PMF rendering is countably supported where print constrains it not at all, but Causal.measureMinimalBudget_eq_exactMinimalBudget proves N(eps) is the same number under either reading, so the restriction costs nothing and that axis is closed. The row is Same from 2026-08-21: IsPolyLogBudget and NonadaptiveWithinConstant both quantify over every eps in (0,1), which is prob:exact's own scope, and the eps_0 that had made this Narrower is deleted from the Prop rather than explained away. The argument that had justified eps_0 was itself wrong: it held that an unrestricted bound forces N(eps) = 0 near eps = 1 and that this is a demand the poly-log idiom does not address, but N(eps) = 0 there is expected -- the zero-query minimax risk is the error of the best fixed guess, which is below 1 on any class of positive diameter. This field states the current grade and its reason only.", "lean": "AISafetyAtlas.Conjectures.MAIS.maisO25_exactQueryRate", "lean_module": "AISafetyAtlas.Conjectures.MAIS", "answer_candidate": [], "answer_admissible": [], "answer_correct": [], "admissibility_status": "NotApplicable", "blocked_on": "", "absent_declarations": [], "tags": [ "interpretability", "computational-complexity" ], "proposed_by": "Atlas statement-only transcription of MAIS-O25's two decide-clauses, at the yes branch of the poly-log bound and the no branch of the adaptivity question.", "status": "OPEN", "resolution": "", "source_ref": [ "mais-a2-2026" ], "context_source_ref": [], "source_scope": "Same", "source_fidelity": "Selected", "source_note": "Scope is Same, and the epsilon range is gone from the Prop rather than explained away. IsPolyLogBudget and NonadaptiveWithinConstant both quantified over eps below a supplied eps_0. A second quantifier defect on the same predicate was closed on 2026-08-23: NonadaptiveWithinConstant bound its constant c existentially and was applied inside the for-all over sk and modelClass, so the Prop allowed one adaptivity constant per model class. prob:exact asks whether adaptive queries beat non-adaptive ones by more than a constant factor, with constants depending on (m, K, lambda, L, rho); a class is not among those, so a per-class constant states something weaker than print and the row had been graded Same against the easier statement. c is now a parameter of the predicate, quantified beside A and d before the skeleton and the class. Both now quantify over every eps in (0,1), which is prob:exact's own sentence and the domain on which log(1/eps) is positive. The argument that had justified eps_0 was wrong. It said an unrestricted bound would force N(eps) = 0 as eps approaches 1, since A * P * log(1/eps) falls to zero, and called that a demand the poly-log idiom does not address. N(eps) = 0 near eps = 1 is not absurd but expected: the zero-query minimax risk is the error of the best fixed guess, which is strictly below 1 on any class of positive diameter, so N(eps) is already 0 for every eps above it. Below that point N(eps) is positive and log(1/eps) is bounded away from zero, and A is existentially quantified before the diagram, so a large enough A satisfies the bound there. Examples.Causal.OneNodeClass makes the shape concrete: its class is the interval [lambda, 1-lambda] under one graph, the guess 1/2 is wrong by at most 1/2 - lambda, and N(eps) vanishes above that. A satisfiable printed sentence licenses no repair. Nor does conj:exact license one: it writes the same quantity as eps -> 0, so rendering the two halves of one decide-clause differently would itself be a defect. conj:exact is MAIS-O26 and prob:exact is MAIS-O25. They are different printed statements and the convention of one does not transcribe the other. not_isPolyLogBudget_of_top and not_nonadaptiveWithinConstant_of_top were restated against the wider predicate: any single infeasible target in (0,1) now refutes the bound, where before a witness could choose an eps_0 above it. Non-vacuity is closed. Fidelity is Selected and not Bridged, which would have recorded the epsilon range and nothing else: prob:exact attaches no range to eps, IsPolyLogBudget supplied an eps_0, and the tag recorded that the conventional reading was being used in place of the printed quantifier. Both predicates now quantify over every eps in (0,1), so there is no reading standing in for a quantifier any more. Selected stays, because this row states prob:exact's decide-clause and not the rest of the problem. The tag was also, by its own note, added 'for internal consistency with CONJ-003 and CONJ-010 rather than for a new fact' -- consistency with a tag CONJ-003 has now also dropped is not a reason to keep it. This field states the current grade and its reason only." }, { "id": "CONJ-008", "kind": "claim", "problem": "MAIS-O29(a)", "statement": "Negative branch of MAIS-O29(a), at MAIS-A2 prob:boltzmann's own quantifier: for every positive inverse temperature beta, some skeleton over a finite set of binary chance variables carries a pair of distinct models in one six-condition margin class with identical complete Boltzmann response probabilities under every real intervention mixture and observation mask.", "refutation": "Prove injectivity of the Boltzmann behavior map on the margin class of every skeleton at some positive finite beta. A proof of the registered existential collision instead resolves the source subquestion negatively; the existing equal-transform collision is the intended starting witness.", "prior_art": "MAIS-A2 Problem 4.8(a) and MAIS-O29 ask whether Boltzmann behavior is injective. The statement defines the conditional softmax response, including uniform answers on zero-mass observation fibres, and selects the negative branch. Parts (b)--(c), concerning sampled minimax rates, the beta crossover, and optimal design, still require the statistical-experiment layer. The colliding pair is MAIS issue #6's construction, reused here; the issue is the provenance of the witness, not the statement being graded, which is prob:boltzmann(a).", "lean": "AISafetyAtlas.Conjectures.MAIS.maisO29_boltzmannNotInjective", "lean_module": "AISafetyAtlas.Conjectures.MAIS", "answer_candidate": [], "answer_admissible": [], "answer_correct": [], "admissibility_status": "NotApplicable", "blocked_on": "", "absent_declarations": [], "tags": [ "interpretability" ], "proposed_by": "Atlas statement-only negative branch of MAIS-O29(a).", "status": "RESOLVED", "resolution": "Coverage: this row is prob:boltzmann(a) only. MAIS-O29 has three clauses and RESOLVED here is the status of this row's Lean Prop, not of the printed problem. Part (b) is answered at one instance by CONJ-016 and part (c) is blocked, and neither follows from (a): a negative answer to (a) constrains (b), since non-identifiability can floor the risk, but does not determine it, and it bears on (c) not at all. Resolved negatively on the source's real chart by AISafetyAtlas.Examples.Conjectures.MAIS.maisO29_boltzmannNotInjective_holds, at every positive beta, with the two-variable skeleton supplied as the witness for the source's existential over skeletons. The MAIS-O23 witness pair is also a Boltzmann collision at every positive inverse temperature: because the skeleton observes nothing, each response probability is a softmax of the full expectations E[u d], and the utility u d v = (1 +/- g v)/2 makes those expectations (1 +/- Delta)/2, so their sum is the total mass 1 and their difference is the behavioral transform. Equal transforms therefore pin both scores and hence the softmax, uniformly in beta. ATTRIBUTION: the colliding construction is MAIS issue #6's; the source does not connect MAIS-O29 to MAIS-O23, and the transfer step is the atlas's. modelError is print's own e. What this row does not claim: boltzmann_minimax_floor proves a deterministic estimator reading only the Boltzmann responses is maximally wrong on one of the two colliding models, at every positive temperature and independently of budget. That is not a lower bound on the randomized minimax risk prob:boltzmann(b) names -- deterministic strategies are a subset of randomized ones, so a lower bound on the larger infimum carries no information about the smaller. The two-point argument at print's own quantifier landed on 2026-08-23: AISafetyAtlas.Conjectures.MAIS.O29Experiment builds the sampled experiment -- the exact-oracle protocol with the policy-probability oracle replaced by one Bernoulli response and the adversarial policy family dropped, since the Boltzmann law is pinned by the model and beta -- and runBoltzmannTranscript_congr proves two Boltzmann-indistinguishable models induce the SAME transcript law at every budget, so no sampling separates them. half_le_boltzmannMinimaxRisk_of_collision then floors the randomized minimax risk at 1/2, and Examples...half_le_boltzmannMinimaxRisk_collision instantiates it on this row's own witness over the full margin class, uniformly in the budget and in beta. boltzmannMinimaxRisk_le_one supplies the other side, so Examples...boltzmannMinimaxRisk_collision_bounds DETERMINES prob:boltzmann(b)'s quantity up to a factor of two at this skeleton, uniformly in the budget and in beta: the rate is Theta(1), so there is nothing to deteriorate as beta -> 0 and no (N,beta) crossover to characterize, because the risk never decays. That is (b) at one print-legal instance and not at every one, the same standing as the MAIS-O27(a) negative instance; on a class where the risk does decay, none of (b) is touched. The floor's graph condition is load-bearing rather than incidental: without it modelError is the table supremum rather than 1, one_le_modelError_add does not apply, and the floor is not 1/2, so a same-graph Boltzmann collision does not floor the risk. This row remains prob:boltzmann(a) only: (b) is a determine-clause and no truth-valued Prop is Same as it. This row stays prob:boltzmann(a) only. Print's remark that large beta creates no regret floor is not contradicted: this obstruction is non-identifiability at every beta. The module header of AISafetyAtlas/Examples/Conjectures/MAIS/O29.lean states the same distinction beside the theorem.", "source_ref": [ "mais-a2-2026" ], "context_source_ref": [ "mais-issue-4-2026" ], "source_scope": "Same", "source_fidelity": "Selected", "source_note": "Scope is Same as of 2026-08-20: the Prop quantifies over beta on the outside and over skeletons over a finite binary chance-variable set inside, with real tables, utilities and mixture weights, which is how prob:boltzmann part (a) asks it. It was stated at the rationals until then. Fidelity is Selected because (a) says 'decide whether the map from models to Boltzmann behavior is injective on MM(sk,lambda)' and the Prop states the negative branch. Parts (b) and (c) -- minimax rates, the (N,beta) crossover, and the design problem -- need the sampled statistical-experiment layer and are not claimed." }, { "id": "CONJ-009", "kind": "answer", "problem": "MAIS-O34(a)", "statement": "Complete candidate for MAIS-O34(a) on the source's real three-parameter two-variable chart: for every valid utility-gap table, positive margin, and forward or reverse one-edge model, the global sixteen-coordinate behavioral fibre is a singleton exactly when the same-orientation companion set is a singleton and the explicit flat-row/flat-column criterion excludes an opposite-orientation mate.", "refutation": "Give a valid real gap table and model for which the submitted row/column and companion-set criterion holds but another valid model has the same sixteen transform coordinates, or for which the criterion fails although the global fibre is a singleton. Either direction refutes the registered equivalence without requiring a classification of the remaining O34(b) radius geometry.", "prior_art": "MAIS-A2 Problem 5.2(a), MAIS-O34, and the candidate solution in MAIS issue #4. The issue states a complete singleton criterion and remains open for maintainer and community review. The atlas declaration transcribes that candidate onto a dedicated real chart with the source's full local-map intervention semantics. It does not accept the candidate, claim a proof, or cover O34(b)'s first-order radius, singular classification, or graph-threshold program. The candidate is now adjudicated affirmatively; see the resolution field. An earlier exhaustive rational-grid screen over gap-and-margin pairs and model cases found no mismatch in either direction and is superseded by the proof.", "lean": "AISafetyAtlas.Conjectures.MAIS.maisO34_exactFiberCandidate", "lean_module": "AISafetyAtlas.Conjectures.MAIS", "answer_candidate": [ "AISafetyAtlas.Conjectures.MAIS.O34GlobalSingletonCandidate" ], "answer_admissible": [], "answer_correct": [ "AISafetyAtlas.Conjectures.MAIS.maisO34_exactFiberCandidate" ], "admissibility_status": "Unformalized", "blocked_on": "", "absent_declarations": [], "tags": [ "interpretability" ], "proposed_by": "Rob Sneiderman (Robby955), MAIS issue #4; statement transcribed by the atlas.", "status": "RESOLVED", "resolution": "Resolved affirmatively by AISafetyAtlas.Examples.Conjectures.O34Fiber.maisO34_exactFiberCandidate_holds: on the source's real two-variable chart the global sixteen-coordinate fibre is a singleton exactly under the criterion submitted in MAIS issue #4. Sufficiency was isSingletonFiber_of_candidate. Necessity splits, and both halves are proved. The same-direction half rests on behaviorEq_of_childDifference_eq_zero: a vanishing direction difference hides its child coordinate from all sixteen profiles, not only from the two profiles that read coordinates, so a failed companion clause supplies a distinct feasible value and hence a same-orientation mate; o34FlatRowGap and o34FlatRowModel witness that this clause can fail. The opposite-orientation half is the step that could have refuted the candidate, and does not: exactly one flat row together with exactly one flat column forces the gap table to be constant off a single entry, and on such a table behaviorEq_crossed_forward and behaviorEq_crossed_reverse show a forward and a reverse model collide as soon as the opposite root is the model's read child coordinate and the opposite model's own read coordinate is the model's root. The remaining opposite coordinate never enters any of the sixteen values, which is exactly why the printed criterion asks only that the root's companion set be inhabited. Both sides of the equivalence are shown reachable on valid data, so neither direction is vacuous: o34TwoFlatGap has one flat row and one flat column, so hasOppositeMate_o34TwoFlat holds and not_isSingletonFiber_o34TwoFlat concludes that model has a mate, while o34SharpGap has no flat line, so globalSingleton_o34Sharp holds and isSingletonFiber_o34Sharp concludes that model's fibre is a genuine singleton. Scope is the transcribed chart: two binary variables, one edge, real coordinates, the source's four local maps. Issue #4 part (b), its 136-segment reduction and threshold program, remains outside and is not claimed. Since 2026-08-23 the equivalence is also available at the printed comparison class: AISafetyAtlas.Examples.Conjectures.O34Fiber.o34_classFibre_iff_candidate states the criterion against every model of the printed class carrying an edge, resting on exists_pairModel_toModel_eq and PairModel.toModel_injective, so the singleton claim is about the fibre inside MM2(lambda) and not inside the atlas's chart. The printed adjective is also discharged: AISafetyAtlas.Examples.Conjectures.O34Fiber.isSemialgebraic_o34GlobalSingletonCandidate proves the criterion cuts a semialgebraic subset of the seven real coordinates def:twovar names, once an orientation fixes the structural choice. Its two real-quantifier clauses are eliminated by hand rather than by Tarski-Seidenberg: separatedValues_eq_singleton_iff and separatedValues_nonempty_iff replace them with explicit polynomial conditions, and separatedValues_ne_singleton_of_le_quarter records that the companion clause is unsatisfiable below margin 1/4, so at def:twovar's own simulation margin of 1/10 the same-orientation criterion collapses to its first disjunct. Coverage: this row is prob:starter-set(a) only. MAIS-O34 has two clauses and RESOLVED here is the status of this row's Lean Prop, not of the printed problem. Part (b) -- the first-order constant on the Lipschitz locus, the classification on its complement, and the edge-direction regret threshold -- is not covered here or anywhere in the atlas, and does not follow from (a).", "source_ref": [ "mais-issue-4-2026" ], "context_source_ref": [ "mais-a2-2026" ], "source_scope": "Same", "source_fidelity": "Literal", "source_note": "The graded source is MAIS issue #4 alone, corrected on 2026-08-21 from a pair that also named the agenda. A single Same cell cannot answer to both: prob:starter-set(a) reads 'Determine ... an explicit semialgebraic condition', which no truth-valued Prop is the same statement as, while issue #4 states a complete singleton criterion that this Prop does transcribe. The agenda moves to context_source_ref as the setting the criterion is stated in, where nothing claims to be Same as it. Scope is Same against the issue: the Prop is at the issue's own quantifier over valid real gap tables, positive margins, and forward or reverse one-edge models, on the source's real two-variable chart with its four local maps. Two things are read from the transcription rather than supplied, and are recorded here rather than only in the Lean docstring: the equivalence is stated in both directions because the issue asserts both, and the sixteen-coordinate fibre is the global one over both orientations, not the same-orientation companion set alone. PairModel.toModel_marginClass proves the chart points inhabit the printed kernel class, behaviorEq_iff_kernel proves chart transform equality is exactly kernel behavior, and hasSingletonFibre_iff_kernel transports the fibre claim in both directions. Issue #4 part (b), its 136-segment reduction and threshold program, is a different claim and is not graded here. The chart is now proved onto that class as well: exists_pairModel_toModel_eq shows every model of the printed family carrying an edge is toModel of a valid chart point, PairModel.toModel_injective shows no model is named twice, and hasSingletonFibre_iff_kernel_class therefore compares M against every model of the printed class rather than against the chart's own points. Surjectivity is load-bearing in exactly one direction: ruling out collisions gets easier as the comparison class shrinks, so an identification claim proved over chart points alone would have been weaker than print's, while the counterexample rows never needed it." }, { "id": "CONJ-010", "kind": "answer", "problem": "MAIS-O31", "statement": "Candidate complete answer to MAIS-O31 on a real binary chain, at MAIS issue #8's own quantifiers: for every chain model with strict table and edge-strength margins and every decision threshold t in (0,1), away from transfer-endpoint ties, interventions on one variable identify the observational mass r = P(C_j = 1) in the straddling chamber; and a literal table coordinate is identified exactly when the transfer straddles, the intervened variable is the root, and the coordinate is the root probability -- so the same-side chamber identifies none.", "refutation": "Give a real chain with strict margins, a threshold t in (0,1), and a strict straddling or same-side chamber at which either the r clause fails or a literal root or transition coordinate's pointwise identifiability disagrees with the stated classification. Behavioral compatibility quantifies over every real mixture of all four local maps at the selected node and permits arbitrary shared tie behavior, so a counterexample must preserve one complete restricted optimal-policy family.", "prior_art": "MAIS-A2 Question 4.10, MAIS-O31 (`q:chain`), and the candidate complete solution in MAIS issue #8. The issue derives four affine diagnostics and a generic chamber classification but remains open and explicitly claims no human or journal referee verification. The statement uses the full real chain chart, every threshold t in (0,1), the source's table margins, all four binary local interventions, and literal coordinate equality. It transcribes the issue's own Scope exclusions -- endpoint ties, CPT boundaries, exact margin boundaries -- as the chamber disjunct together with `O31ChainModel.Generic`. Both of the issue's bullets are stated; the r clause is the implication the issue asserts, not an equivalence it does not. The separate o31Threshold lemmas connect margin-admissible utilities from the surrounding agenda problem to examples of the issue's free threshold, but they no longer restrict this conjecture.", "lean": "AISafetyAtlas.Conjectures.MAIS.maisO31_chainClassificationCandidate", "lean_module": "AISafetyAtlas.Conjectures.MAIS", "answer_candidate": [ "AISafetyAtlas.Conjectures.MAIS.O31CoordinateCandidate" ], "answer_admissible": [], "answer_correct": [ "AISafetyAtlas.Conjectures.MAIS.maisO31_chainClassificationCandidate" ], "admissibility_status": "Unformalized", "blocked_on": "", "absent_declarations": [], "tags": [ "interpretability" ], "proposed_by": "Svyatoslav Novikov (kumino) with OpenAI Codex, MAIS issue #8; statement transcribed by the atlas.", "status": "OPEN", "resolution": "", "source_ref": [ "mais-issue-8-2026" ], "context_source_ref": [ "mais-a2-2026" ], "source_scope": "Same", "source_fidelity": "Literal", "source_note": "Scope is Same and fidelity is Literal, both from 2026-08-23, because the threshold bridge was removed rather than defended. MAIS issue #8 quantifies over t in (0,1), so maisO31_chainClassificationCandidate now quantifies directly over every such t. It no longer quantifies over a utility gap pair or substitutes the derived o31Threshold, whose margin bounds cover only a strict subinterval. The o31Threshold lemmas remain separate results connecting the agenda's utility formulation to concrete witnesses; they impose no restriction on the conjecture. The issue's own Scope exclusions -- endpoint ties, CPT boundaries, and exact margin boundaries -- remain the chamber disjunct and O31ChainModel.Generic. Both bullets are transcribed, including the r implication rather than an equivalence the issue does not assert. The chart is not left semantically detached, and since 2026-08-23 the embedding is proved in both directions: O31ChainModel.toModel_marginClass proves that every valid chain chart with a legal endpoint utility embeds in the printed margin class, and exists_O31ChainModel_toModel_eq proves the converse, that every model of the printed class carrying the chain graph is toModel of a valid chart point, with O31ChainModel.toModel_injective naming none twice. Only the first direction was needed while every O31 result here is a counterexample, since an existence claim is harder in a larger class; the converse is what the IDENTIFICATION half needs, because a uniqueness claim is EASIER in a smaller comparison class and proving one over chart points alone would have been weaker than print. that half is this row's. O31IdentifiesCoordinate and O31IdentifiesNodeMass quantify over O31ChainModel, while q:chain names its comparison class in print -- 'the models of MM(sk,lambda) carrying this chain graph, so that all the parameters are defined' -- and issue #8 answers that question without redefining the class. o31IdentifiesCoordinate_iff_class and o31IdentifiesNodeMass_iff_class prove the chart-quantified predicates EQUIVALENT to their statements against every model of the printed class carrying the chain graph, so the conjecture is about print's comparison class and not a smaller one. Before 2026-08-23 that equivalence did not exist and this row's Same grade rested on the chart quantifier alone. O31ChainModel.Δ_toModel_endpointGap proves the actual utility transform is the threshold-centered endpoint marginal up to its nonzero scale; o31BehaviorEqAt_threshold_iff_utilityKernel transports the chart relation to shared-optimum behavior computed from those kernel models; and shareBinaryOptimum_iff_exists_common_action proves that its sign condition means a shared optimal binary action. Non-vacuity is checked on both chambers by o31_antecedent_inhabited and o31_sameSide_antecedent_inhabited. What remains unsettled is the conjecture itself: the straddling positive identification claims, the node-mass claim, the two transition coordinates at n = 1, and the general n >= 2 classification." }, { "id": "CONJ-012", "kind": "target", "problem": "MAIS-O24", "statement": "MAIS-A2 prob:effective asks to exhibit an effective-genericity certificate: a class, a recovery modulus and the constants that make recovery quantitative. AISafetyAtlas.Causal.O24Solution is that object, with the proof obligations as fields, so a term of the type is a solution and there is nothing left to check separately. No term exists: the type is empty.", "refutation": "Already resolved negatively. To overturn the resolution, exhibit an O24Solution -- which is now the same as refuting isEmpty_o24Solution -- or break one of its three steps: the collision on the open box, the covering argument that forces a supplied polynomial to vanish identically at the collision utility, or the transfer of that vanishing to the nearby utilities at which conclusion (c) is asserted.", "prior_art": "MAIS-A2 prob:effective. MAIS issue #7 (Svyatoslav Novikov / kumino, generated by OpenAI Codex, 2026-08-04) argues that conclusions (a) and (c) are incompatible. That argument is the one checked here. Its collision family, utility gap, box and margin are the ones used; its final step is not, because as written it chooses the utilities first and builds the margin mu from the supremum the choice produces, while prob:effective quantifies over mu outside the three conclusions, leaving (c)'s almost-every null set free to depend on that mu. Reversing the two choices closes the gap and needs nothing beyond print.", "lean": "AISafetyAtlas.Causal.O24Solution", "lean_module": "AISafetyAtlas.Causal.EffectiveGenericity", "answer_candidate": [ "AISafetyAtlas.Causal.O24Solution" ], "answer_admissible": [ "AISafetyAtlas.Causal.O24Constructor" ], "answer_correct": [ "AISafetyAtlas.Causal.O24Solution" ], "admissibility_status": "Formalized", "blocked_on": "", "absent_declarations": [], "tags": [ "learning-theory", "computational-complexity" ], "proposed_by": "Atlas transcription of the printed determine-clause.", "status": "RESOLVED", "resolution": "Resolved negatively by AISafetyAtlas.Examples.Causal.O24Refutation.isEmpty_o24Solution: prob:effective has no solution, because conclusions (a) and (c) cannot both hold. AISafetyAtlas.Examples.Causal.O24Refutation.not_o24_identifies_and_excluded is the sharp form and takes only those two, so the obstruction survives dropping conclusion (b), the polynomial size bounds and the construction-time clause; O24Solution carries all of them and is empty a fortiori. The argument runs on the two-variable skeleton MAIS-O23 is answered with. AISafetyAtlas.Examples.Causal.O24Refutation.behaviorEq_box widens that collision from the single point MAIS-O23 needed to an open box of chart points: the printed gap g = 1/2 - 1_{(1,1)} reads the (1,1) cell alone, and there an X -> Y model and the edgeless model carrying its X = 1 row agree by construction, the source row being behaviourally invisible. Both models sit in the printed margin class at lambda = 1/10 throughout the box. AISafetyAtlas.Examples.Causal.O24Refutation.exists_spec_eq_zero then runs conclusion (a) at every box point: were no supplied polynomial to vanish there, a small enough mu would put both models in MM(sk,lambda,mu) and (a) would identify two models carrying different graphs. So the box is covered by the vanishing loci of one finite list, and by AISafetyAtlas.Analysis.volume_setOf_exists_eval_eq_zero a finite list of nonzero polynomials cannot cover a set of positive measure, so one of them is identically zero once the utility is frozen at the collision's. AISafetyAtlas.Examples.Causal.O24Refutation.not_o24ExcludedSetSmall_of_spec_eq_zero contradicts (c) from that. Not at the collision utility, which (c) is free to discard: a compact table box and a margin mu are fixed first, from S, a, b and the box's volume alone, and only then is a utility chosen from the positive-measure set on which (c) is asserted at that mu. Mathematics due to Svyatoslav Novikov (kumino) via OpenAI Codex, MAIS issue #7 (2026-08-04); the atlas supplied the transcription, the machine-check, and one repair, recorded in docs/provenance/mais-o24-refutation.md.", "source_ref": [ "mais-a2-2026" ], "context_source_ref": [ "mais-issue-7-2026" ], "source_scope": "Same", "source_fidelity": "DetermineProblem", "source_note": "Scope Same, fidelity DetermineProblem. prob:effective reads 'exhibit', which no truth-valued Prop is Same as -- existence is not exhibition, and a Prop asserting that a solution exists asks a different question from the instruction to produce one. The row therefore grades the *specification*: O24Solution's fields are print's own class, modulus and constants, which is why the coverage matrix already graded this object Same before the ledger had a row that could hold the verdict. admissibility_status is Formalized. O24Constructor is the admissibility condition: it carries a Turing machine, a time polynomial, and Turing.TM2OutputsInTime obligations requiring the machine to write the list within time(S) steps, so an inhabitant must carry a concrete machine and certified bounded runs producing the required lists. That is narrower than saying noncomputable choice cannot inhabit the type, which is false: classical choice can select an existing certified machine; what it cannot do is stand in for one. Print's 'exhibit ... in time polynomial in S' is enforced by the structure rather than left to a reader, which is the one place in this ledger where an admissibility demand is met rather than recorded as owed. answer_candidate and answer_correct name the same declaration, which is the exhibit-problem shape rather than an omission: O24Solution's fields ARE the correctness obligations -- print's conclusions (a), (b) and (c), the size bounds and the constructor -- so a term of the type is a checked solution and there is no separate predicate to name. Resolved negatively 2026-08-30, which does not change the grade: the row still grades the specification, and DetermineProblem is what 'exhibit' asks for whether or not anything satisfies it. The verdict now recorded is that nothing does. That settles the non-vacuity question CONJ-003 was carrying, in the unwelcome direction: AISafetyAtlas.Examples.Causal.EffectiveGenericity's section note distinguishes the acceptable reason for O24Solution to be empty -- prob:effective is open -- from the unacceptable one, its fields being jointly contradictory, and it is the second." }, { "id": "CONJ-013", "kind": "target", "problem": "MAIS-O27", "statement": "MAIS-A2 prob:floor asks to determine the asymptotics of the identified-set radius phi(delta; sk, lambda) as delta tends to zero, in three clauses: (a) decide whether phi(0+) = 0, which print says refines q:ident; (b) assuming it is zero, determine the first-order constant as an explicit function of (sk, lambda) together with the matching indistinguishable pair at distance c*delta; (c) determine the set of pairs (s, delta) at which an edge of strength at least s survives every model of the identified set, and exhibit an omitting pair at the complementary pairs. All three are stated at print's real quantifier; answer_correct carries one extensional correctness specification per clause in print's order. Clause (a)'s criterion packages which (sk, lambda) instances satisfy the printed equality; it imposes no human-readable, computable, or semialgebraic answer language, and admissibility remains unformalized.", "refutation": "Exhibit a skeleton and margin at which a proposed answer to any clause is wrong: a regret range where the radius behaves against a proposed characterization, a constant the limit does not match, or a pair the region misplaces.", "prior_art": "MAIS-A2 prob:floor. Clause (a) is settled negatively at one print-legal (sk, lambda) by Examples.Conjectures.MAIS.not_o27RealRadiusVanishes_collision, and clause (c) at (lambda, delta) on the same skeleton by not_realEdgesSurviveAt_collision, with print's exhibition half discharged by exists_strong_edge_omitted_collision. Clause (b) has no instance in either direction. The defective threshold encoding of (c) is retired as CONJ-007.", "lean": "AISafetyAtlas.Conjectures.MAIS.IsO27RadiusVanishingCriterion", "lean_module": "AISafetyAtlas.Conjectures.MAIS.O27", "answer_candidate": [ "Skeleton C dim Bool ℝ → ℝ → Prop", "Skeleton C dim Bool ℝ → ℝ → ℝ", "Set (ℝ × ℝ)" ], "answer_admissible": [ "", "", "" ], "answer_correct": [ "AISafetyAtlas.Conjectures.MAIS.IsO27RadiusVanishingCriterion", "AISafetyAtlas.Conjectures.MAIS.IsO27FirstOrderConstantFunction", "AISafetyAtlas.Conjectures.MAIS.IsO27EdgeSurvivalRegion" ], "admissibility_status": "Unformalized", "blocked_on": "", "absent_declarations": [], "tags": [ "learning-theory", "interpretability" ], "proposed_by": "Atlas transcription of the printed determine-clause.", "status": "OPEN", "resolution": "", "source_ref": [ "mais-a2-2026" ], "context_source_ref": [], "source_scope": "Same", "source_fidelity": "DetermineProblem", "source_note": "Scope Same, fidelity DetermineProblem. One row for one printed problem: prob:floor is a single problem environment with three clauses, and one row covers it, as CONJ-008 does for prob:boltzmann. Splitting by clause would be driven by the schema rather than by the source. The resolution field names the clause it reaches. The answer fields are lists now, one entry per clause in print's order, which is what a multi-clause determine-problem needs. CONJ-014 and CONJ-015 are retired and never reused. All three clauses are stated over def:margin's real class with a real regret range, which is prob:floor's own setting; the rational layer beside them is the instance a decidable witness is computed at, and a rational negative answer transports up to print while a positive one does not. Clause (a)'s specification is IsO27RadiusVanishingCriterion, a criterion on (sk, lambda) with the quantifiers inside the candidate. The row also pointed at o27RealProblemTargets, the fillable bundle this schema exists to discourage, and now points at a specification. Clause (b)'s specification takes the candidate as a FUNCTION of (sk, lambda) with the quantifiers inside it, which is print's order; O27RealHasFirstOrderConstant binds the constant after the skeleton and so states only the pointwise version, and a family of pointwise constants need not be a function anyone can write down. Clause (c)'s is find-all -- membership agrees with the printed survival condition at every pair -- since 'decide for which pairs' is not answered by an inclusion in one direction. admissibility_status is Unformalized for all three clauses, and the gap is PROVED rather than asserted: isO27EdgeSurvivalRegion_self shows the canonical region satisfies clause (c)'s specification by unfolding, so a circular answer passes. PRINT NAMES NO ANSWER LANGUAGE FOR ANY CLAUSE OF prob:floor, AND THE ATLAS DOES NOT SUPPLY ONE. Semialgebraic appears twice in MAIS-A2 and neither is here: as a hypothesis on the model class in prob:exact, and as a demand on the answer in prob:starter-set(a), 'Determine, as an explicit semialgebraic condition on (u, theta)'. prob:floor says only 'decide for which pairs (s, delta)', and for clause (b) 'as an explicit function of (sk, lambda)' without defining explicit. A hypothesis in one printed problem does not impose an answer language on another, so grading this row against a semialgebraic demand would make it NARROWER THAN PRINT. This field asserted that grading, and IsO27EdgeSurvivalAnswer was registered here, until it was corrected against the printed text; the declaration remains in the tree as an atlas strengthening offered for study and is named in no admissibility field. TWO REASONS IT WOULD NOT HAVE DONE THE JOB EVEN IF PRINT ASKED FOR IT. Causal.IsSemialgebraic is an existential, so the canonical region together with a proof that it happens to be semialgebraic satisfies the conjunction and the restatement survives; a language that excludes it must make the pieces DATA -- a finite list of polynomial sign conditions, its interpretation as a plane set, and a theorem equating that with the survival region. And whether the printed region IS semialgebraic is open: plausible, since the tables are finitely many reals and the margin and edge-strength conditions are polynomial inequalities and Tarski-Seidenberg carries real quantifiers, but InIdentifiedSet quantifies over a policy family indexed by every real intervention mixture, and reducing that function-valued existential to a first-order real formula is a step no theorem in the tree takes. WHAT A SOLVER SHOULD SETTLE. Clauses (a) and (b) are chartable, contrary to what this field said: with C, dim and the two Finsets fixed, a skeleton's utility field is finitely many reals cut out by utility_parents' linear equalities and the [0,1] box, so a fibrewise semialgebraic condition on the locus, or on the graph of the function, is definable. What is missing is the warrant to demand it, and -- for a criterion asked of every C and dim -- a decision about whether explicit should also mean uniform in the discrete data. Computable, semialgebraic-in-a-chart and closed-form are candidates and are not equivalent. The right resolution is to ask the MAIS authors whether prob:floor(b) and (c) intend an algorithmic, semialgebraic or merely exact answer. Formal Conjectures documents the same hole with the same example and declines to police it." }, { "id": "CONJ-016", "kind": "target", "problem": "MAIS-O29(b)", "statement": "MAIS-A2 prob:boltzmann(b) asks for the minimax risk at budget N up to constants for each fixed finite beta, including its deterioration as beta tends to zero, and then for the joint (N, beta) crossover from the smooth local rate to the noiseless adaptive-search regime. boltzmannMinimaxRisk is that quantity, over the sampled Boltzmann experiment.", "refutation": "Exhibit a class and a budget at which a proposed rate is wrong in either direction.", "prior_art": "MAIS-A2 prob:boltzmann(b). Examples.Conjectures.MAIS.boltzmannMinimaxRisk_collision_bounds pins the quantity between one half and one at the collision skeleton, uniformly in the budget and in beta, which answers (b) at one print-legal instance and at no other.", "lean": "AISafetyAtlas.Conjectures.MAIS.boltzmannMinimaxRisk", "lean_module": "AISafetyAtlas.Conjectures.MAIS", "answer_candidate": [ "ℕ → ℝ → ℝ" ], "answer_admissible": [], "answer_correct": [ "AISafetyAtlas.Conjectures.MAIS.IsBoltzmannRiskRate" ], "admissibility_status": "Unformalized", "blocked_on": "", "absent_declarations": [], "tags": [ "learning-theory", "information-theory" ], "proposed_by": "Atlas transcription of the printed determine-clause.", "status": "OPEN", "resolution": "", "source_ref": [ "mais-a2-2026" ], "context_source_ref": [], "source_scope": "Same", "source_fidelity": "DetermineProblem", "source_note": "Scope Same, fidelity DetermineProblem. The risk is print's own: an infimum over randomized adaptive analysts of the supremum over the class of the expected error, with print's error function and print's Boltzmann channel. IsBoltzmannRiskRate is the specification a candidate rate must satisfy, with the two constants quantified BEFORE the budget and the inverse temperature -- which is what 'up to constants' means, and what gives the statement content, since constants allowed to depend on (N, beta) could bracket anything. The specification is satisfied at one instance and that is checked: Examples.Conjectures.MAIS.isBoltzmannRiskRate_collision proves the risk is Theta(1) on the collision class -- it lies between one half and one at every budget and every positive beta -- so there is no deterioration as beta tends to zero and no (N, beta) crossover there, because the risk never decays. The three numbers are easy to confuse, and 'the constant rate 1' reads as a risk value when it is not one. The rate function is the constant 1 and the implied constants are one half and one, so the statement about the risk is that it lies in that interval. The lower half is over RANDOMIZED adaptive analysts and is the number with content; the upper one is trivial, since print's error is bounded by one. Neither is boltzmann_minimax_floor's one, which bounds a DETERMINISTIC estimator's error against the model it misses and is not a bound on print's quantity, since deterministic strategies are a subset of randomized ones and a lower bound on the larger infimum says nothing about the smaller. A specification nobody has satisfied is indistinguishable from one that cannot be. Where the risk does decay none of (b) is touched, and any answer with a square root of N in it lives on a class excluding graph-differing Boltzmann collisions. admissibility_status is Unformalized, AND WHAT IS MISSING IS A CHOICE RATHER THAN A PROOF. The answer is a rate function N -> beta -> R, and nothing in IsBoltzmannRiskRate stops a candidate from being defined as the minimax risk itself divided by a constant, which satisfies the specification and answers nothing. Excluding that needs a grammar the rate must be written in -- products of powers of N and beta with logarithms is the usual one, and print's own phrasing 'up to constants' and 'the smooth local rate' presumes something of the kind without naming it. The atlas does not impose one, because the grammar is a modelling decision about what MAIS-A2 accepts as a rate and print does not make it: too narrow a grammar makes the problem unanswerable, too wide readmits the circular answer. A SOLVER SHOULD STATE THE GRAMMAR THEIR ANSWER LIVES IN. The one rate this row does exhibit, fun _ _ => 1 in isBoltzmannRiskRate_collision, is a constant and therefore lies in every candidate grammar, so the instance already checked is not sensitive to the choice." }, { "id": "CONJ-017", "kind": "target", "problem": "MAIS-O31", "statement": "MAIS-A2 q:chain asks which of the 2(m-1)+1 table parameters of a directed-path chain are Sigma_W-identifiable for almost every theta, with W a single intervenable variable and the comparison class the margin-class models carrying that chain graph. IsO31IdentifiableSetAlmostEverywhere is the specification a candidate answer set must satisfy: one set of coordinates, quantified outside the parameter, whose membership agrees with identifiability at almost every parameter of the printed class.", "refutation": "Exhibit a coordinate and a positive-measure set of chain parameters inside the margin class on which a proposed answer set gets identifiability wrong in either direction.", "prior_art": "MAIS-A2 q:chain. Print offers a heuristic and labels it as such, declining to conjecture either half. Examples.Conjectures.MAIS.o31_endpointMarginal_not_identified_positiveMeasure refutes the heuristic's claim that the endpoint marginal is recoverable, on an explicit box of Lebesgue measure 1/500 at the two-node chain.", "lean": "AISafetyAtlas.Conjectures.MAIS.IsO31IdentifiableSetAlmostEverywhere", "lean_module": "AISafetyAtlas.Conjectures.MAIS.O31", "answer_candidate": [ "Finset (AISafetyAtlas.Conjectures.MAIS.O31Coordinate n)" ], "answer_admissible": [], "answer_correct": [ "AISafetyAtlas.Conjectures.MAIS.IsO31IdentifiableSetAlmostEverywhere" ], "admissibility_status": "Unformalized", "blocked_on": "", "absent_declarations": [], "tags": [ "interpretability", "learning-theory" ], "proposed_by": "Atlas transcription of the printed determine-clause.", "status": "OPEN", "resolution": "", "source_ref": [ "mais-a2-2026" ], "context_source_ref": [], "source_scope": "Same", "source_fidelity": "DetermineProblem", "source_note": "Scope Same, fidelity DetermineProblem. This row grades print's question; CONJ-010 instead grades the candidate classification submitted in MAIS issue #8. IsO31IdentifiableSetAlmostEverywhere places the answer set outside the parameter quantifier and states membership equivalence at almost every point of the real chain chart, matching q:chain's quantifier. O31Coordinate has exactly 2n+1 inhabitants by card_o31Coordinate, so Finset is a convenient concrete carrier for a proposed list, but it is not an admissibility condition: o31FinsetOfSet converts any Set to a Finset by classical filtering, and isO31IdentifiableAnswer_of_set proves that any correct Set specification therefore yields the Finset form. The answer_admissible list is empty and admissibility_status is Unformalized. Nothing requires an explicit combinatorial description in (G, W, O, Z), and print supplies no answer grammar for q:chain. The pointwise predicates remain infrastructure and CONJ-010 uses them; isO31IdentifiableSetAlmostEverywhere_of_forall records that an everywhere classification implies the printed almost-everywhere one. Print's composite transfer map belongs to its labelled heuristic, not to the literal coordinate question. NOT CLAIMED: that the margin class has positive measure at every (lam, t), or that any candidate answer set has been proved correct." }, { "id": "CONJ-023", "kind": "answer", "problem": "MAIS-O33", "statement": "MAIS-A2 prob:corruption asks for recovery of a controlled Markov process from first-action data under persistent corruption -- an adversary that commits in advance to one function rho on S x Psi_n differing from the agent's own first actions on at most eta|S x Psi_n| arguments -- with a randomized adaptive analyst, one polynomial query budget, and success probability 2/3. Determine eta* := sup{eta : eta uniformly tolerable}; is eta* > 0? The submitted answer, graded here, is eta* = 0.", "refutation": "Already resolved. To overturn it, exhibit a positive eta and a single randomized algorithm with a polynomial budget meeting the printed clause at every admissible instance -- which is the same as refuting AISafetyAtlas.Examples.Causal.O33Corruption.exists_not_tolerantAt -- or break one of its three steps: the two agents' boundedness on the action-independent worlds, the counting bound on composite goals carrying no immediate win, or the disjointness of the two reconstruction balls at n = 101, delta = 1/2.", "prior_art": "MAIS-A2 prob:corruption, and the goal-based setting of Theorem thm:rabe (Richens-Abel-Bellot-Everitt). The negative resolution eta* = 0 is MAIS issue #9 (Svyatoslav Novikov / kumino, generated by OpenAI Codex, 2026-08-04, CC BY 4.0), audited in docs/provenance/mais-o33-statability.md and machine-checked in docs/provenance/mais-o33-refutation.md. The atlas runs the candidate at delta = 1/2 rather than the delta = 0 the note chose, and on action-independent kernels rather than the note's one skewed row; both are admissible instances of prob:corruption and each removes a dependency. The atlas also holds one endpoint of the related O33 intersection through its Rivest-style noisy-search material, which is a different corruption model.", "lean": "AISafetyAtlas.Conjectures.MAIS.maisO33_etaStarIsZero", "lean_module": "AISafetyAtlas.Conjectures.MAIS", "answer_candidate": [ "AISafetyAtlas.Conjectures.MAIS.maisO33_etaStarCandidate" ], "answer_admissible": [], "answer_correct": [ "AISafetyAtlas.Conjectures.MAIS.maisO33_etaStarIsZeroGivenBaseline" ], "admissibility_status": "NoneRequired", "blocked_on": "", "absent_declarations": [], "tags": [ "learning-theory", "computational-complexity" ], "proposed_by": "Atlas coverage record; the printed problem has no Lean object.", "status": "RESOLVED", "resolution": "Resolved 2026-08-30. AISafetyAtlas.Examples.Conjectures.MAIS.not_uniformlyTolerable proves that no positive corruption fraction is uniformly tolerable; AISafetyAtlas.Examples.Conjectures.MAIS.not_maisO33_etaStarPos answers print's yes/no clause -- eta* is not positive -- and AISafetyAtlas.Examples.Conjectures.MAIS.maisO33_etaStarIsZeroGivenBaseline_holds grades the submitted value eta* = 0 correct, conditional on print's own cited baseline (that eta = 0 is tolerable, which needs thm:rabe together with the unnumbered paragraph after it that supplies the discovery algorithm and its |S|^2|A|n query count; neither is formalized here, and A2 proves neither -- thm:rabe is cited to Richens-Abel-Bellot-Everitt 2025). The unconditional AISafetyAtlas.Examples.Conjectures.MAIS.maisO33_etaStarIsZero_holds is also proved, but its 0 <= eta* half can come from Lean's supremum-of-the-empty-set convention, so it certifies this layer's totalized etaStar rather than print's value; the conditional is the one answer_correct names. The construction is AISafetyAtlas.Examples.Causal.O33Corruption.exists_not_tolerantAt: at n = 101 and delta = 1/2, where (n-1)(1-delta) = 50 clears print's constraint, two action-independent environments on Fin (m+2) states and two actions sit 4/5 apart while the target radius is only 2/sqrt 50. AISafetyAtlas.Causal.exists_isDeltaBounded_prescribing builds a (delta,n)-bounded agent in each that opens with the same action at every (start state, goal) pair whose goal carries a depth-one Now disjunct that pair already satisfies, and near-optimally elsewhere; near-optimality is ordinary supremum approximation (AISafetyAtlas.Causal.exists_achieveProb_ge), so no optimal-policy-attainment theorem is used. The two first-action maps therefore differ only on the goals carrying no such disjunct, which AISafetyAtlas.Causal.card_corruptionDomain_avoiding counts and AISafetyAtlas.Causal.exceptional_ratio_lt bounds by 2^(1-R) with R = 2^(2|S|-1) -- doubly exponentially small, so raising the state count clears any positive budget. One agent's honest first-action map is then an admissible eta-corruption of the other's (AISafetyAtlas.Causal.isCorruption_of_agree_off_avoiding), both worlds hand the analyst the same oracle, and AISafetyAtlas.Causal.not_tolerantAt_of_common_corruption finishes: one output law cannot put 2/3 on each of two disjoint reconstruction balls. No query bound is used anywhere, which is why the printed polynomial plays no role. ONE CAVEAT, and it is in the resolution rather than only the note: eta* = 0 is proved as the supremum of a set with no positive element, and the >= 0 half does not certify that print's eta = 0 endpoint is tolerable -- that is thm:rabe plus the unnumbered algorithm paragraph that follows it, neither of which this repository formalizes, so Real.sSup of the empty set carries the other half. The accuracy is not the obstacle: thm:rabe's bound is at most 1/sqrt(2(n-1)(1-delta)) since P(1-P) <= 1/4, against prob:corruption's target 2/sqrt((n-1)(1-delta)); the work is mechanizing the binomial-median sweep. not_maisO33_etaStarPos is the clause that does not depend on the distinction, and it is print's actual question. A SECOND STRENGTHENING: AISafetyAtlas.Examples.Conjectures.MAIS.not_uniformlyTolerableWithin refutes tolerability inside every subclass of analysts, so no reading of print's word 'algorithm' -- computable, finitely describable, or otherwise -- recovers a positive eta. THE CAVEAT IS ALSO A HYPOTHESIS, NOT ONLY A FOOTNOTE: AISafetyAtlas.Conjectures.MAIS.maisO33_baselineTolerable names print's baseline (that eta = 0 is tolerable, which is thm:rabe) as a Prop, and AISafetyAtlas.Examples.Conjectures.MAIS.maisO33_etaStarIsZeroGivenBaseline_holds proves the determine-clause from it with the 0 <= eta* half coming from an inhabitant of the tolerable set rather than from the supremum of the empty set. answer_correct is a one-entry positional list and it names the CONDITIONAL, because that is the honest grade: the unconditional equality is also proved, but its 0 <= eta* half can come from the empty-supremum convention, which certifies an atlas convention rather than print's value. The row's lean field stays maisO33_etaStarIsZero, print's determine-clause with no added hypothesis -- adding the baseline there would launder a narrowing, since print asserts the baseline rather than assuming it. So: the negative answer is machine-checked outright, and the numerical value is machine-checked conditional on print's cited, unformalized baseline. WHAT WAS CHECKED IS THE CANDIDATE'S CLAIM, NOT ITS PROOF: the Lean follows issue #9's strategy at a different instance, so several of the note's own steps have no counterpart here; docs/provenance/mais-o33-statability.md is the reading audit of the argument itself and is not a machine-check. Mathematics due to Svyatoslav Novikov (kumino) via OpenAI Codex, MAIS issue #9 (2026-08-04); the atlas supplied the transcription, the machine-check, and two instance changes recorded in docs/provenance/mais-o33-refutation.md.", "source_ref": [ "mais-a2-2026" ], "context_source_ref": [ "mais-issue-9-2026" ], "source_scope": "Same", "source_fidelity": [ "DetermineProblem", "Selected" ], "source_note": "Scope Same, with the one axis that is not literally identical closed by theorem rather than by prose -- see (5) below. Every printed quantifier is carried: all finite instances with |A| >= 2, n > 1 and (n-1)(1-delta) > 4; every communicating environment; every (delta,n)-bounded goal-conditioned agent at print's own history type; every eta-corruption; one randomized adaptive algorithm and one polynomial budget across all instances, carried as c*(|S|+|A|+n+1)^d, which dominates any polynomial in the three parameters and is what print's 'at most p(...) queries' asks for. THE ANALYST READS THE WHOLE INSTANCE: print's instance is (S,A,n,delta) and all four reach the strategy and the estimator; only the query bound is delta-free, matching print's p(|S|,|A|,n). Withholding delta from the protocol would narrow the analyst class and the refutation would not transfer, so it is passed. The adversary keeps print's power: rho is quantified after the strategy, so it may be chosen knowing the analyst, and it is a function fixed before the interaction, which is what persistent means. FIVE READINGS, all recorded and none laundered. (1) MAX VERSUS SUP. Print writes max_{pi'}, which presupposes attainment; AISafetyAtlas.Causal.optimalProb is the supremum. Since sup >= max, IsDeltaBoundedFull selects a sub-collection of print's A(E,n,delta), so the refutation is quantified over the weaker class and is the stronger result once proved; the two agree wherever the presupposition holds and diverge only at delta = 0, which is why the witness runs at delta = 1/2. (2) HISTORY. This axis is now CLOSED BY PROOF, not by prose: print's trajectory-prefix policy is AISafetyAtlas.Causal.FullPolicy, AISafetyAtlas.Causal.inducedPolicy computes the action it takes as a function of the states by running the same rule at earlier times, AISafetyAtlas.Causal.liftPolicy embeds back, and AISafetyAtlas.Causal.optimalProbFull_eq shows the two suprema coincide, so AISafetyAtlas.Causal.isDeltaBoundedFull_lift_iff makes the two boundedness clauses select the same agents and AISafetyAtlas.Causal.firstActionMapFull_lift makes them show the analyst the same data. Reading the history as states only is NOT a safe simplification and the direction argument for it fails: it compares agent classes and ignores that the boundedness threshold, a max over the same class, moves with them. That is why this axis is closed by proof. (3) EMPTY DISJUNCTION. compositeGoals excludes it, and print settles it rather than the atlas choosing: a composite goal's depth is the maximum over disjuncts, which the empty set has not, so the empty disjunction has no depth and lies in no Psi_n. This matters here in a way it did not for the counting alone: the corruption budget is eta|S x Psi_n|, and the two readings differ by |S| arguments with neither budget dominating the other. AISafetyAtlas.Causal.exceptional_ratio_lt_with_empty shows the counting survives either way. (4) TOTAL CORRUPTION MAP. FirstActionData is defined on every composite goal where print's rho is defined on S x Psi_n; nothing observes the difference, because queries range over corruptionDomain n = S x Psi_n and the budget is charged against exactly those arguments. THE GOAL EVENT IS MEASURABLE, AND THIS IS NOW PROVED RATHER THAN ASSERTED: AISafetyAtlas.Causal.measurableSet_compositeSatisfies shows the set AISafetyAtlas.Causal.achieveProb applies the trajectory law to is measurable, so the row transcribes print's P(tau |= psi | pi, s0) and not merely the measure's canonical extension to an arbitrary set. The proof is print's own semantics: a sub-goal reads one state-action pair, that pair is a function of the states up to its time because the policy is deterministic, Now and Next fix the time, Eventually is a countable union over it with a finite minimality condition, a sequential goal is a countable union over its head's achievement time, and a composite goal is a finite union over its disjuncts. No step of the refutation needs it -- every use of achieveProb is monotone or an almost-everywhere congruence -- but without it the row would transcribe a quantity only bounded by print's. (5) WHAT 'ONE RANDOMIZED ALGORITHM' MEANS. prob:corruption does not define the word, so it is read from the section that sets up every query problem in the agenda, subsec:queries: an analyst there 'adaptively issues queries t = 1,...,N' and the figure of merit is 'the infimum over (randomized) analyst STRATEGIES'. N bounds queries, not steps; A2 states no computational model anywhere -- no machine, no circuit, no time or space bound, no complexity class -- and its one lower-bound argument, rem:packing, is Fano and Yao, which are indifferent to computability. On the agenda's own vocabulary 'algorithm' is a randomized adaptive query strategy, which is exactly AISafetyAtlas.Conjectures.MAIS.UniformAnalyst: one strategy, one estimator and one polynomial, all chosen before the instance, which is the quantifier order the word 'single' fixes. THE ATLAS DOES NOT REST ON THAT READING. If the word is instead read as 'computable', UniformlyTolerable quantifies over a class wider than print's, since a Lean function is not a computable one, and a widening is a scope defect unless it is closed. It is closed: AISafetyAtlas.Conjectures.MAIS.UniformlyTolerableWithin restricts the analyst by an arbitrary predicate C -- computability, finite describability, any other reading -- and AISafetyAtlas.Examples.Conjectures.MAIS.not_uniformlyTolerableWithin refutes every one of them at once, because the witness defeats every strategy at a single instance and narrowing a class cannot rescue an existential. What is not formalized on that reading is a class-relative threshold eta*_C, and nothing needs one: the statement that carries the answer is 'no positive eta is tolerable', and that is proved for every C. A class-relative supremum would only repeat the empty-set question one level down -- if C admits no analyst meeting print's baseline, eta*_C is a supremum over a possibly empty set -- so no lower bound on it is claimed here. INSTANCE QUANTIFIER. UniformlyTolerable ranges over Type with Fintype, DecidableEq, MeasurableSpace and MeasurableSingletonClass instances. The instances do not widen it: Fintype and DecidableEq are subsingletons, and MeasurableSingletonClass on a finite type forces the sigma-algebra to be the full power set, so each finite S contributes exactly one instance as it does in print. Restricting to Type rather than every universe can only make a negative answer stronger. Fidelity is DetermineProblem and Selected: print asks to determine eta* and then asks a yes/no question. The determine-clause is graded by maisO33_etaStarIsZeroGivenBaseline, which answer_correct names; the yes/no branch is maisO33_etaStarPos, answered by AISafetyAtlas.Examples.Conjectures.MAIS.not_maisO33_etaStarPos and needing no baseline. admissibility_status is NoneRequired: print asks for a supremum's value and no explicit or computable form beyond the number itself. The 0 <= eta clause in etaStar is print's intent and not print's letter -- without it every negative eta joins the set vacuously, since no map differs from another on a negative number of arguments -- and it is the one word this row supplies that the source does not." }, { "id": "CONJ-025", "kind": "claim", "problem": "MAIS-O38", "statement": "MAIS-O38 has an affirmative answer at MAIS-A3 prob:samples's own hypotheses: for every sparsity law k(m) tending to infinity and every ambient dimension law n with n >= 2k, there is a sample count N(m) bounded by a single polynomial in m together with, at every dimension m where the printed sentence has content -- every m with 1 <= k(m) and k(m) < m -- a family of N(m) codes in R^m each having at most k(m) nonzero entries, such that for Lebesgue-almost every real n(m) x m matrix A satisfying the spark condition of order k(m) -- every set of at most 2k(m) columns linearly independent -- the dataset A generates from those codes is uniquely coded: any other matrix B and any other k(m)-sparse codes reproducing the same data differ from the originals only by a permutation matrix and an invertible diagonal rescaling. The two hypotheses are print's own and are the whole hypothesis list; 1 <= k(m) < m guards the conclusion and is not assumed.", "refutation": "A refutation exhibits a sparsity law k(m) -> infinity with k(m) < m eventually and an ambient law n >= 2k such that every polynomially bounded sample-count law fails to supply a uniquely coding design at some non-degenerate m with 2 <= m and 1 <= k(m) < m. No such refutation is recorded. What IS proved is a warning about the wider domain print leaves unwritten, and it is not this row: AISafetyAtlas.Examples.Conjectures.MAIS.not_maisO38_unboundedSparsityReading refutes AISafetyAtlas.Conjectures.MAIS.maisO38_unboundedSparsityReading at k(m) = m, where every vector in R^m is k-sparse and a transvection reproduces any dataset with rescaled codes. By AISafetyAtlas.Examples.Conjectures.MAIS.rows_gt_cols_of_full_sparsity_spark that witness is forced into m < n, an undercomplete dictionary where agenda A3's subject is m > n. It remains a reading finding, not an answer.", "prior_art": "MAIS-A3 Problem 4.8, labelled prob:samples, restated on the open-problems page MAIS-O38.md. Print names the classical uniqueness bounds it wants improved: N = (k+1)*binom(m,k) generic samples suffice for a fixed A (Aharon-Elad-Bruckstein 2006; Hillar-Sommer 2015), N = k*binom(m,k)^2 suffice universally over spark-condition A (Hillar-Sommer 2015), and the determination is noise-stable at N = m(k-1)*binom(m,k)+m (Garfinkle-Hillar 2019); all are polynomial in m only for fixed k. Print also names the two polynomial results that come close and miss: Spielman-Wang-Wright 2012 control rival ROW sparsity for square dictionaries where this problem allows every column-k-sparse competitor, and Awasthi-Vijayaraghavan 2018 give approximate rather than exact recovery under restricted isometry, a triple-occurrence hypothesis on supports, and n >> k polylog(m), which excludes both the almost-every-spark quantifier and the allowed regime n = 2k. None of these results is formalized in the atlas; they are recorded as the printed context, not as checked statements. MAIS issue #30 (2026-08-26, 26david26) submits a candidate complete solution claiming N = m^3 + 2m codes depending only on m and k suffice for every 1 <= k < m, together with a boundary theorem at k >= m. The boundary theorem is not transcribed; the main claim IS transcribed, as AISafetyAtlas.Conjectures.MAIS.o38PolynomialSampleCandidate, and is now PROVED as AISafetyAtlas.Examples.Conjectures.MAIS.o38PolynomialSampleCandidate_holds, which is what resolves this row. Its 15-page proof note is pinned in docs/provenance/mais-source-pin.md (sha256 2ba4179f312b7e5c9fa87bcecc0702b409d2ec4fdab7d0f06e9ae387eed422ca) and was read in full on 2026-08-30 without a gap being found; that is a triage by one reader, not a referee report, and no grade rests on it. The main claim would resolve this row affirmatively if correct and is stronger than the row asks, since its codes do not depend on n. The boundary theorem is the same statement as the atlas's own Examples...not_uniquelyCoded_of_full_sparsity_spark and is credited in source_note. The issue states it was produced and checked entirely by AI systems with no human verification.", "lean": "AISafetyAtlas.Conjectures.MAIS.maisO38_polynomialSamplesSuffice", "lean_module": "AISafetyAtlas.Conjectures.MAIS.O38", "answer_candidate": [ "AISafetyAtlas.Conjectures.MAIS.o38PolynomialSampleCandidate" ], "answer_admissible": [], "answer_correct": [ "AISafetyAtlas.Conjectures.MAIS.o38PolynomialSampleCandidate" ], "admissibility_status": "NotApplicable", "blocked_on": "", "absent_declarations": [], "tags": [ "interpretability", "learning-theory" ], "proposed_by": "MAIS-A3 Problem 4.8 (prob:samples); transcribed by the atlas.", "status": "RESOLVED", "resolution": "Coverage: this row is prob:samples under print's two hypotheses and no others -- k(m) -> infinity and n >= 2k -- with the conclusion required at every m satisfying 1 <= k(m) < m rather than on a tail. Resolved AFFIRMATIVELY by AISafetyAtlas.Examples.Conjectures.MAIS.maisO38_polynomialSamplesSuffice_holds. THE MATHEMATICS IS NOT THE ATLAS'S. AISafetyAtlas.Examples.Conjectures.MAIS.o38PolynomialSampleCandidate_holds proves the candidate submitted as MAIS issue #30 by 26david26: m^3 + 2m codes depending only on m and k work at every 2 <= m and 1 <= k < m, for every n >= 2k and almost every spark-condition dictionary. The row is the printed question at that strength; the candidate is stronger in two ways the printed question does not ask for, since its codes do not depend on n and one list serves every n >= 2k at once. TWO EARLIER FORMS OF THIS ROW WERE WEAKER AND ARE GONE. The first stated the conclusion at Filter.atTop, discarding the candidate's pointwise strength through filter_upwards. The second guarded the conclusion pointwise but still assumed an atlas-supplied premise, eventually k(m) < m, which print does not write and which the proof does not use; that premise narrowed a source claim by hypothesis, the mirror of weakening a conclusion. Print's k(m) -> infinity is retained and is unused, which is a finding about prob:samples recorded in the statement docstring rather than a licence to delete it. The issue states the construction and proof were produced and checked entirely by AI systems with no human verification; the atlas supplied the transcription, the kernel check, and four domain-neutral library facts. Every declaration named here depends only on propext, Classical.choice and Quot.sound.", "source_ref": [ "mais-a3-2026" ], "context_source_ref": [ "mais-o38-2026", "mais-issue-30-2026" ], "source_scope": "Same", "source_fidelity": "Selected", "source_note": "First MAIS row whose source is agenda A3 rather than A2, and the first with no causal content. Fidelity is Selected because prob:samples asks a decide-whether question and this Prop states its affirmative branch. Scope is Same at the guarded reading: print's hypotheses k(m) -> infinity and n >= 2k are retained and are the ENTIRE hypothesis list, while the conclusion is required at every individual m satisfying 1 <= k(m) < m. The domain reading for k appears only as a guard on that conclusion, never as a premise, so the row narrows the printed claim in no direction. 2 <= m is not stated because 1 <= k(m) and k(m) < m force it. This replaces two earlier and weaker forms: one requiring designs only eventually, and one which guarded the conclusion but still assumed an atlas-supplied premise that k(m) < m eventually. At the time, check_statement_freeze.py read only registry results from by-id.json and therefore covered no CONJ row at all; even a conjecture drift after grading would have been invisible, not only this pre-grade weakening. This change extends the lock to every graded conjecture declaration. The submitted candidate already has the pointwise strength: AISafetyAtlas.Examples.Conjectures.MAIS.o38PolynomialSampleCandidate_holds proves m^3 + 2m codes work for every 2 <= m and 1 <= k < m. The proof does not use k(m) -> infinity at all, so a version omitting it would be true and strictly stronger -- and Beyond/AtlasOriginal rather than Same, since print writes that hypothesis. The graded row therefore keeps it, unused, and the fact that it is unused is recorded here and in the statement docstring rather than acted on. The two genuinely wider readings remain separate findings: demanding a design at every m without non-degeneracy is false at m = 1, and leaving k unbounded is false at k(m) = m. The issue's boundary theorem agrees with the latter finding. The proof of the candidate, including its Lemma 6 dimension/null argument and Lemma 8 Tonelli step, remains unchanged and kernel-checked." }, { "id": "CONJ-026", "kind": "target", "problem": "MAIS-O70", "statement": "MAIS-A6 prob:calibration asks three things about reduced-rank regression y = BAx + noise with parameters (N, M, H) and realizable truth of rank r. P1: prove the local pair (lambda(w*), m(w*)) at a factorization w* = (A,B) in the zero fiber W_0 depends only on (rank A, rank B), graded by AISafetyAtlas.Conjectures.MAIS.O70DependsOnRanksOnly. P2: compute the resulting table, graded by IsO70RankTable, whose candidate is o70Pair. P3: hence characterize the strata on which lambda(w*) equals the minimum in thm:aw, graded by IsO70FiberMinimumTable together with IsO70AWValueStratumTable, whose candidate is o70Minimizers. All three are stated against print's own loss -- rrrLoss is the Gaussian expectation MAIS-O70.md prints, not the Frobenius form, which is derived -- and against the volume normalization def:local calls equivalent to its zeta definition. Progress: P3's arithmetic content is settled affirmatively and unconditionally by o70_fiber_minimum_correct: awLambda M N H r is a lower bound for the candidate table on every admissible rank stratum and is attained, at the uniform witness (a,b) = (r,r). Composed with admissible_of_mul_eq this reaches actual matrices in awLambda_le_of_factorization, so no factorization of any truth matrix carries a candidate value below the printed number. Because thm:aw itself glosses its minimum as the minimum of lambda(w) over W_0, this needs no Aoyagi-Watanabe hypothesis. P1 and P2 remain open unconditionally, and each stands behind two named frontier hypotheses rather than two unformalized arguments; it is the weaker two-sided volume order, not P1 or P2, that needs only the first of them. isO70VolumeOrderTable_o70Pair proves IsO70VolumeOrderTable o70Pair from EigenvalueLawStatement and nothing else: the two-sided volume order at the candidate's values, at every factorization of every truth matrix, with no admissibility hypothesis, since print's five feasibility inequalities hold at the actual ranks. The orbit reduction, the elimination chart, the Gaussian-to-compact localization and the chamber calculus are all formalized in AISafetyAtlas.SingularLearning. EigenvalueLawStatement is O70-EIGEN-LAW, the real Wishart density together with the eigenvalue Jacobian; the candidate cites it to Muirhead Theorems 3.2.1 and 3.2.17 after James 1954, and it is not proved in the atlas. From there isO70RankTable_o70Pair gives IsO70RankTable o70Pair and o70DependsOnRanksOnly_of_frontiers gives O70DependsOnRanksOnly, each under EigenvalueLawStatement together with the value-free hypothesis O70ExactLocalPairsExist, which asserts that some exact local pair exists and never what it is; isO70VolumeOrderTable_of_rankTable gives the converse direction. The two remaining frontiers are exactly O70-EIGEN-LAW and O70-EXACT-LOCAL, neither is formalized, and the atlas holds no unconditional inhabitant of IsO70RankTable o70Pair.", "refutation": "Refute P3's arithmetic content by exhibiting an admissible rank stratum with positive dimensions whose candidate value is strictly below awLambda, contradicting o70_fiber_minimum_correct, or one that equals awLambda yet is excluded from o70Minimizers, contradicting o70_aw_value_strata_correct. Refute P1 or P2 by exhibiting matrices A, B over R with B * A = C whose actual local pair, in the sense of HasExactLocalPair applied to rrrLossCoords at matrixPairCoords A B, differs from o70Pair at their ranks. Nothing in the atlas asserts that no such pair exists, so P1 and P2 are open rather than contradicted. Such a pair would also refute at least one of the two frontier hypotheses, since isO70VolumeOrderTable_o70Pair derives the candidate's order table from EigenvalueLawStatement alone.", "prior_art": "MAIS-A6 prob:calibration. MAIS issue #3 (Sneiderman, 2026) is the candidate whose Theorem 1.1 and Corollary 1.3 are transcribed as o70Pair; the atlas closes its discrete residual minimisation in residualMinCost_eq_argmin. thm:aw is Aoyagi-Watanabe 2005, transcribed as awLambda and awMultiplicity and asserted only as arithmetic. Two facts the pinned Mathlib lacks were proved here: Sylvester's rank inequality, absent in every form -- only upper bounds on the rank of a product are present -- in AISafetyAtlas.SingularLearning.ReducedRank; and currying for the product Lebesgue measure, in AISafetyAtlas.SingularLearning.Coordinates.", "lean": "AISafetyAtlas.Conjectures.MAIS.IsO70RankTable", "lean_module": "AISafetyAtlas.Conjectures.MAIS.O70", "answer_candidate": [ "ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℚ × ℕ", "ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℚ × ℕ", "Set AISafetyAtlas.Conjectures.MAIS.O70RankStratum" ], "answer_admissible": [], "answer_correct": [ "AISafetyAtlas.Conjectures.MAIS.O70DependsOnRanksOnly", "AISafetyAtlas.Conjectures.MAIS.IsO70RankTable", "AISafetyAtlas.Conjectures.MAIS.IsO70AWValueStratumTable" ], "admissibility_status": "Unformalized", "blocked_on": "", "absent_declarations": [], "tags": [ "learning-theory" ], "proposed_by": "Atlas transcription of the printed determine-clause.", "status": "OPEN", "resolution": "", "source_ref": [ "mais-o70-2026" ], "context_source_ref": [ "mais-a6-2026", "mais-issue-3-2026" ], "source_scope": "Same", "source_fidelity": "DetermineProblem", "source_note": "Graded against mais-o70-2026. MAIS-O70.md states the pair outright as the volume of {K <= eps} scaling as eps^lambda (log(1/eps))^(m-1), which is the weak sublevel form the graded predicates use, and it restates the printed problem. Agenda A6 is a context source: its def:local defines the local pair by the largest pole of a zeta integral and calls the ball-volume form equivalent afterwards, so it is the artifact thm:aw and rem:conventions are drawn from, and O70-ZETA-BRIDGE is what relates the two definitions. Scope Same, fidelity DetermineProblem. Three clauses, three graded propositions, quantified as print quantifies them. Clause three is positional against a candidate of type Set O70RankStratum, so its graded proposition is IsO70AWValueStratumTable, the predicate that consumes a stratum set; IsO70FiberMinimumTable grades the table object of clause two and is what makes the printed value a minimum rather than merely a number, and o70_fiber_minimum_correct proves it unconditionally. Quantifiers: over every truth matrix, every factorization of it, and every rank stratum, with dimensions positive because rem:conventions excludes the vacuous case K identically zero, which for reduced-rank regression is exactly a vanishing dimension. Two normalization decisions are recorded rather than hidden. First, the local pair is fixed by the ball-volume asymptotic eq:volume rather than by def:local's primary zeta poles; print licenses this in its own word 'equivalently', and the atlas states the substitution without proving the equivalence. Second, HasExactLocalPair asks for exact asymptotics at all but countably many small radii, which matches def:local's assertion that the pair does not depend on the radius while making no claim about the constant c, a claim print never makes. The parameter space is transported to Euclidean coordinates by a reindexing proved measure-preserving, so no Jacobian is absorbed silently." }, { "id": "CONJ-027", "kind": "answer", "problem": "MAIS-O7", "statement": "Candidate negative resolution of MAIS-A7 Problem 3.7: in the scalar reduced-rank instance M = N = r = 1 and H = 2 with any positive target singular value s, the complete critical ladder has two rungs. The rank-zero rung is the origin and has two-sided local pair (1,1) at its only point; the terminal exact-factorization fiber is nonempty and has pair (1/2,1) at every point. The sets of certified coefficients on the rungs are therefore {1} and {1/2}, both infima are attained, and the conjectured strict increase is false.", "refutation": "Overturn the answer by finding a positive s for which any clause of IsO7Counterexample fails: another rank-zero critical point, an empty terminal fiber, a point on either rung with a different two-sided volume order, a different rung infimum, failure of attainment, or restoration of the strict inequality.", "prior_art": "MAIS-A7 Problem 3.7 and the candidate negative resolution in MAIS issue #5. The candidate supplies the scalar instance and the two local calculations. The atlas transcribes the source loss as its Gaussian expectation, derives the scalar polynomial identity, proves the rank-zero band by an explicit frontier-free determinant integral, and transports the terminal calculation through the existing reduced-rank chart. No eigenvalue-density law, analytic Morse lemma, zeta-pole bridge, or candidate-shaped assumption is used.", "lean": "AISafetyAtlas.Conjectures.MAIS.O7CounterexampleAtEveryScale", "lean_module": "AISafetyAtlas.Conjectures.MAIS.O7", "answer_candidate": [ "ℝ" ], "answer_admissible": [], "answer_correct": [ "AISafetyAtlas.Conjectures.MAIS.IsO7Counterexample" ], "admissibility_status": "NoneRequired", "blocked_on": "", "absent_declarations": [], "tags": [ "learning-theory" ], "proposed_by": "MAIS issue #5; statement transcribed and proved by the atlas.", "status": "RESOLVED", "resolution": "Resolved negatively and unconditionally by AISafetyAtlas.Conjectures.MAIS.isO7Counterexample. The theorem quantifies over every positive scalar target and proves the full IsO7Counterexample certificate, not only the numerical comparison 1 > 1/2: it identifies the whole rank-zero rung, proves the terminal rung inhabited, proves the pair at every point of both rungs in weak and strict threshold conventions, computes both exponent sets and infima, proves both attainments, and concludes the printed inequality fails. The rank-zero proof is independent of O70's EigenvalueLawStatement and of any analytic Morse lemma. The certificate is a statement about o7RankZeroRung and o7TerminalRung, so each is tied to MAIS-A7's own C_k by a proved identity rather than by transcription; without that bridge a mis-specialization would be a valid theorem about the wrong two sets and no check could report it. Examples.Conjectures.MAIS.o7RankZeroRung_eq_saddleRung proves the rank-zero rung equal to IsO77SaddleRungPoint at the scalar frame -- the predicate isO77SaddleRungPoint_iff_critical proves equivalent to criticality-plus-membership in both directions -- and o7TerminalRung_eq_fiber proves the terminal rung is that frame's exact-factorization fibre. o7Loss_terminal_lt_rankZero adds the descending step of print's own setting, so the instance is shown to lie inside the setting the conjecture is stated over rather than assumed to. This settles MAIS-O7 but does not imply MAIS-O77(b), whose all-dimensional, all-saddle claim remains separate.", "source_ref": [ "mais-issue-5-2026" ], "context_source_ref": [ "mais-a7-2026", "mais-o7-2026" ], "source_scope": "Same", "source_fidelity": "Literal", "source_note": "Scope Same and fidelity Literal against the submitted answer in issue #5: IsO7Counterexample carries the same scalar family s > 0, both complete rungs, the universal pointwise pair claims, the two infima with attainment, and the failed strict inequality. The operational relation is two-sided volume order rather than A7's primary signed-zeta pole definition, and since 2026-09-06 that substitution is a Lean object rather than a remark: A7ZetaVolumeBridge, frozen as a7ZetaVolumeBridge_iff and registered as the frontier A7-ZETA-BRIDGE. This is not hidden: HasO7PairAt contains both the atlas weak-sublevel bounds and a separate strict-band predicate matching the source's strict inequality. A7 only states the band relation in order-comparison language, so neither side asserts an exact limiting constant. The atlas does not prove that this operational pair equals the leading pole of A7's meromorphic signed zeta function. What it now proves is the implication: o7_zeta_refutation gives both rung coefficients and the failure of the printed increase in A7's own definition, taking the bridge in its binders, so the conditionality is in the type rather than in this note. The grade remains against the volume form, which is what the submission itself computes." }, { "id": "CONJ-028", "kind": "target", "problem": "MAIS-O77", "statement": "MAIS-A7 Problem 3.9 has two clauses for the loss L(A,B) = (1/2)||BA-Phi||_F^2 when Phi has rank r < H and distinct positive nonzero singular values. Part (a) asks three things: the two-sided local pair at every exact factorization, the minimal stratum, and whether the pair depends only on (rank A, rank B). The first is graded by IsO77SourceFiberVolumeOrderTable with candidate o77Pair; the second by IsO77MinimizerCharacterization with candidate o77Minimizers; the third is answered by the shape of the first, whose table is a function of the two ranks alone, and is recorded separately as O77FiberDependsOnRanksOnlyAtVolumeOrder. Part (b) asks for the pair at every point of every nonterminal critical set C_k, graded by O77AllSaddlesHavePairOne; the submitted answer is (1,1). Part (b) is proved unconditionally. o77AllSaddlesHavePairOne_holds inhabits O77AllSaddlesHavePairOne at print's own quantifiers, with axioms propext, Classical.choice and Quot.sound only. It runs through O77Chart -- exists_o77_chart splits the parameter space with the variation block first, fderiv_o77_chart_eq_zero is criticality transported through the affine chart, and exists_o77_block_matrix identifies the chart's Hessian block with Kalpha up to congruence -- and then through hasLocalVolumeOrder_centeredBandGerm_of_indefinite_block, which states the candidate's argument away from O77. The steps that argument needs are proved rather than assumed. frobeniusSq_rung_blockVariation shows the loss on print's 2H block is exactly the Kalpha form plus a single quartic, every cubic cancelling. det_o77SaddleBlock_ne_zero is print's nonsingularity conclusion with nothing assumed: truncation_gram_no_eigenvector excludes s_alpha^2 from the spectrum of the truncation's Gram operator using only orthonormality of the right modes and the strict decrease of the singular values, and o77_saddle_spectral_det_ne_zero carries that across the UV/VU exchange. `o77HessianForm_indefinite_of_rung` gives transverse indefiniteness at every point of every nonterminal rung, transcribing the candidate's own argument on the two-parameter block. exists_gromoll_meyer_splitting builds equation (9): the critical fibre by the inverse function theorem, the congruence localized to a neighbourhood, returning a chart with invertible derivative at the origin and the germ g(zeta) = f(c zeta, zeta) - f(0), witnessed non-constant. hasLocalVolumeOrder_abs_matrixQuadForm_add_germ is Lemma 2 at print's own generality, an arbitrary nondegenerate indefinite form in n >= 3 variables plus an arbitrary continuous germ vanishing at the origin, which invokes Sylvester's law of inertia. fderiv_pairLoss_eq_zero_of and fderiv_fderiv_pairLoss_apply are the loss's first and second Frechet derivatives. isO77RungTangent_iff_null identifies the Hessian's null space at a rung point with the linearization of the three conditions cutting out C_k. That is not a Morse-Bott critical manifold, and loss_quartic_on_degenerateNull shows why: at the rank-zero rung of wideFrame the loss grows like t^4 along a null direction, so no Morse-Bott normal form exists there. A generalized splitting with a degenerate germ on the null space is unaffected -- the quartic is an instance of it, with g the quartic -- and that is the shape print's equation (9) already has: Q_alpha(xi) + g(zeta) with g(0)=0 and no nondegeneracy asked of g. The witnesses exercise the argument rather than a degenerate corner of it. IsO77SaddleRungPoint requires k < r, so a frame with r = 1 offers only the rank-zero rung, where both Gram blocks vanish, o77_saddle_spectral_det_ne_zero reduces to det(-s_alpha^2 I) != 0, and truncation_gram_no_eigenvector excludes s_alpha^2 from the spectrum of the zero operator, using neither orthonormality nor the strict decrease of the singular values. rank2Frame is a frame with a rung of its own; rungPoint_rank2 is a point of C_1; rank2_nondegenerate, rank2_gram_blocks_ne_zero and rank2_truncation_gram_ne_zero prove the configuration is not the degenerate one; and pair_rank2 is the pair (1,1) there. Part (a) is conditional on EigenvalueLawStatement, the Wishart frontier inherited from O70, and on nothing else. isO77SourceFiberVolumeOrderTable_o77Pair gives the order-level table; isO77MinimizerCharacterization_o77Minimizers gives the minimal stratum at the germs, which is what MAIS-O77.md's clause asks -- a stratum lies in the set exactly when the two-sided pair realized at its points has the least coefficient realized anywhere on the same fiber. That needs no existence frontier: the fiber table supplies a realized pair at every factorization and volumeOrder_unique pins its value. o77_aw_value_strata_correct is the arithmetic layer beneath it and holds by rfl, since o77Minimizers is defined as the admissible strata whose table value meets awLambda. zeroFrame and a Set.univ refutation in Examples/Conjectures/MAIS/O77.lean show the germ-level predicate has an inhabited hypothesis and is not satisfied by every set. The arithmetic minimum and the candidate's extra maximum-tie-multiplicity sentence are unconditional. The row is OPEN because part (a) rests on a frontier; the two parts are graded separately and only (b) is unconditional.", "refutation": "For part (a), exhibit a certified source target and exact factorization whose two-sided volume order differs from o77Pair at the factor ranks; this would refute the table or the inherited EigenvalueLawStatement. For part (b), exhibit a certified frame, a nonterminal rung, and a point satisfying the printed truncation and discarded-mode annihilation conditions whose pair is not (1,1). The scalar origin cannot be such a refutation because the atlas proves its pair unconditionally in the O7 development.", "prior_art": "MAIS-A7 Problem 3.9 and the candidate solution in MAIS issue #12. Part (a) explicitly credits and reconstructs the multiplication-slice calculation submitted earlier in MAIS issue #3 for MAIS-O70. The atlas therefore uses a thin dimension-name adapter around o70Pair and the O70 order theorem rather than duplicating that proof. Part (b)'s Hessian-block and splitting argument is now machine-checked, with one regularity gap named: the note asks for analytic coordinates and exists_gromoll_meyer_splitting delivers C-infinity ones. That is everything the note's Lemma 2 consumes, so the conclusion is unaffected, but analytic regularity of the chart is not checked and is not claimed. Neither the splitting nor the level-uniform band lemma existed in Mathlib or in this tree; both were built here, and the candidate's argument is followed rather than replaced. The O7 scalar proof supplies one independent specialization, not the universal result.", "lean": "AISafetyAtlas.Conjectures.MAIS.IsO77SourceFiberVolumeOrderTable", "lean_module": "AISafetyAtlas.Conjectures.MAIS.O77", "answer_candidate": [ "ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℚ × ℕ", "Set AISafetyAtlas.Conjectures.MAIS.O77RankStratum", "ℚ × ℕ" ], "answer_admissible": [], "answer_correct": [ "AISafetyAtlas.Conjectures.MAIS.IsO77SourceFiberVolumeOrderTable", "AISafetyAtlas.Conjectures.MAIS.IsO77MinimizerCharacterization", "AISafetyAtlas.Conjectures.MAIS.O77AllSaddlesHavePairOne" ], "admissibility_status": "Unformalized", "blocked_on": "", "absent_declarations": [], "tags": [ "learning-theory" ], "proposed_by": "Atlas transcription of MAIS-A7 Problem 3.9 and the issue #12 candidate.", "status": "OPEN", "resolution": "", "source_ref": [ "mais-o77-2026" ], "context_source_ref": [ "mais-a7-2026", "mais-issue-12-2026", "mais-issue-3-2026" ], "source_scope": "Same", "source_fidelity": "DetermineProblem", "source_note": "Scope Same, fidelity DetermineProblem, graded against mais-o77-2026. MAIS-O77.md defines the invariant by the volume asymptotics outright, which is the form the graded predicates use, and its Problem statement is unchanged from A7 Problem 3.9, so it is both the artifact this row transcribes and print. Agenda A7 is a context source: its def:llc defines the local pair by the largest pole of a zeta integral and only afterwards glosses the band volume, and A7-ZETA-BRIDGE is what relates the two definitions. O77 asks to compute families of local pairs and to identify a stratum, so no truth-valued Prop is literally the instruction; the three answer_correct entries are positional in print's order -- part (a)'s table, part (a)'s minimal stratum, part (b)'s saddle pair. The stratum entry is graded at the germs rather than against the table: MAIS-O77.md says the minimal stratum means the stratum on which lambda attains the Aoyagi-Watanabe value, and lambda there is the realized local invariant, not a table entry. IsO77AWValueStratumTable and IsO77FiberMinimumTable remain in the tree as the unconditional arithmetic layer beneath it. The source-facing part (a) predicate quantifies over positive input and output dimensions, rank r < H, a certified target with positive strictly decreasing singular values and orthonormal modes, and every exact factorization. O77SpectralFrame stores only those source facts plus the target expansion and rank; it grants no criticality, Hessian, coordinate splitting, or volume conclusion. Part (b)'s IsO77SaddleRungPoint carries exactly the top-k product and both discarded-mode annihilation clauses printed in A7, while O77AllSaddlesHavePairOne quantifies over every such point. O77AllSaddlesHavePairOne carries r < H and no dimension positivity, which is exactly Problem 3.9's hypothesis set. Positivity would add nothing: a zero input or output dimension forces the target rank, hence r, to zero, and IsO77SaddleRungPoint then has no inhabitant because it requires k < r, so the models it would exclude are already empty. Part (a)'s predicate does carry positivity, and that asymmetry is real: its proof passes it to the O70 fiber table, where rem:conventions excludes the vacuous model. Both pair predicates contain weak and strict volume-order formulations. As with O7, no zeta-pole equivalence is proved. It is stated: A7 def:llc defines the pair by the zeta pole and glosses the band volume afterwards, and that substitution is the frontier A7-ZETA-BRIDGE, which o77_saddle_zeta_pair and o77_all_saddles_zeta_pair_one carry in their binders to deliver part (b) at every point of every nonterminal critical set in print's own definition. It is a separate assumption from O70-ZETA-BRIDGE and strictly stronger: that one consumes HasExactLocalPair on a germ that vanishes, this one consumes HasLocalVolumeOrder on a germ centred at a saddle. The broad target-uniform theorem for part (a) is stronger than the graded source predicate and specializes to it using only target_rank. The part (a) table itself is issue #3's discrete minimisation, reused rather than restated because issue #12's part (a) is that same multiplication-slice theorem with the input and output dimension names exchanged. The step between the two representations is machine-checked rather than asserted: issue #12 prints a four-case closed formula with a parity correction, its equation (3), and o77Pair_eq_candidate_closed_form proves the minimisation computes it, at every stratum and with no feasibility hypothesis, through residualPair_eq_zeroTargetClosedFormPair. So what is checked for part (a) is the formula issue #12 printed. One byproduct: the note's leading special case, setting the pair to (0,1) when any of p, q, h vanishes, is redundant -- the four regimes already return it on every degenerate shape. o77Pair_candidate_check_table pins the note's own ten printed values, which is what makes a relabeling applied in the wrong direction break the build instead of producing a plausible table. Part (a)'s proof is conditional on EigenvalueLawStatement; part (b) is unconditional. The OPEN status is deliberate and tracks part (a) alone, since the row grades both clauses and one of them still rests on a frontier." } ] }