Source
Aevyra (2026), LIT-1376, read in full in NOTE-1091 from the version 4.0 web page of 25 September 2026: §4.4 (Proposition 4 and its proof), with §4.1–4.3 for the definitions and §5.1 and Appendix A.9 for the examples. The archive’s checks were run and reproduce the saved results.
What was actually shown
Setting: a finite nonempty set H of states (histories, with any current law or status needed to make revision Markovian), closed under a finite family of total deterministic revisions J_z, z ∈ Z; a family D of targets T_d; a deterministic reduction ρ. For a word u = z₁…z_k, J_u applies the revisions in order.
- The relation. h ≈ h′ when T_d(J_u h) = T_d(J_u h′) for every d ∈ D and every word u, including the empty one. It is the coarsest equivalence that refines agreement on current targets (∼_D) and is invariant under every J_z.
- The criterion. ρ admits updates Ĵ_z on its image and decoders g_d with g_d(Ĵ_u(ρ(h))) = T_d(J_u h) for all h, d, u if and only if every fibre of ρ lies within one ≈-class. Necessity: equal retained states give equal decoded outputs after any word. Sufficiency: fix a representative of each fibre and update through it; invariance keeps the representative ≈-equivalent to the true revised state.
- The bound. With K classes of ∼_D and K* of ≈, K* ≥ K, and the current targets plus at most K* − K added nonempty revision words distinguish all K* classes: each added word splits at least one block, and every split respects ≈.
- Strictness, by example. In the paper’s four-state extension of §5.1 (two histories × a law index that one revision sets to 1), the current best action gives K = 2 and the revisions give K* = 3, with the one revision as the added witness. A state that keeps only today’s answer merges two histories that the next change of evaluative law separates.
- Update is weaker than representation. Exact outputs do not give the identity Ĵ_z ∘ ρ = ρ ∘ J_z; that holds only when ρ’s own fibres are invariant. A.9 gives a three-state case where every future target is recoverable and that identity fails.
The proof was checked on reading, and the archive’s exhaustive check of all 5,832 three-state, two-revision, binary-target systems and 3,000 seeded systems, against an independent pair-distinguishability closure, was rerun and agrees. A different result could have come out of these checks; none did.
What this does not say
- Not new mathematics. It is Moore–Nerode refinement applied to the expanded family {T_d ∘ J_u}, and the authors say so. Its interest to the record is that it states QUESTION-112’s sufficiency under changing families exactly, for the case where the family of changes is fixed in advance.
- Not a rule for choosing the revision family. “efficient selection for open-ended agents remains unresolved” (§4.4). For an inquiry whose questions change in response to what it finds, which is what QUESTION-112 asks about, it gives the form of an answer, not the answer.
- Not a size or cost bound. “it is not a token, runtime, or optimal storage bound” (§4.4). K* − K counts test words.
- Not about partial revisions, non-Markovian laws or infinite histories. The paper sets these aside.
- Not about what a bounded reader does. Sufficiency is information available, not information used; the paper keeps “Information availability and computational accessibility” apart (§5.2), as CLAIM-295 does.
- Not an argument that history should be kept. It says what must be kept for a declared family. Whether keeping it pays is CLAIM-295 and CLAIM-303.
Connections
- QUESTION-112. Answers it in part, as above.
- CLAIM-350. The one-step case: Proposition 2, exact sufficiency iff the targets are constant on the fibres, is CLAIM-350. This is that criterion closed under revision.
- CLAIM-294, CLAIM-300. CLAIM-294’s two histories with one marginal and different updates are a case where ∼_D is coarser than ≈. CLAIM-300 is the K* = K case: a state sufficient for a fixed family needs nothing more for it.
- CLAIM-295. The “wider family of decisions for which what is kept suffices” is, for a declared revision family, the move from ∼_D to ≈.
- TERM-067, CLAIM-407. The same factorization criterion with a different target family (responses to interventions on governance). An analogous closure for sequences of governance interventions is not shown here.
Note of 2026-10-30: the re-derivation, written out
The second check at the status review (ADR-065 §5) followed each step. H is finite, each J_z maps H to H, and words act left to right.
-
≈ is the coarsest revision-invariant refinement of ∼_D. It refines ∼_D, because the empty word is a word. It is invariant: if h ≈ h′, then for every z and every word u the word zu agrees on both, so J_z h ≈ J_z h′. And any invariant equivalence E that refines ∼_D lies inside ≈. If h E h′, then J_u h E J_u h′ for every u by invariance, so all their targets agree.
-
Necessity. Suppose ρ(h) = ρ(h′) and exact updates Ĵ and decoders g exist. Then Ĵ_u(ρ(h)) = Ĵ_u(ρ(h′)) for every u, so T_d(J_u h) = g_d(Ĵ_u ρ(h)) = T_d(J_u h′). Hence h ≈ h′, and each fibre lies in one ≈-class.
-
Sufficiency. Choose a representative rep(r) in each fibre, set Ĵ_z(r) = ρ(J_z(rep(r))) and g_d(r) = T_d(rep(r)). Claim: after any word u, the retained state is ρ(h′) for some h′ ≈ J_u h. This holds for the empty word. If it holds for u, then rep(ρ(h′)) shares a fibre with h′, so it is ≈ h′ ≈ J_u h. By invariance, J_z(rep(·)) ≈ J_z J_u h. Decoding reads T_d at a state ≈ J_u h, which equals T_d(J_u h).
-
The bound. ≈ refines ∼_D, so K* ≥ K. Start from the partition by current targets. While it is coarser than ≈, some block holds h and h′ with h ≉ h′, and some nonempty word u separates them. Adding T∘J_u splits that block, and never splits an ≈-class, since ≈-equivalent states agree after every word. Each added word adds at least one block, so at most K* − K are needed.
-
Strictness. Take states (a, 0), (b, 0), (a, 1), (b, 1), a history and a law index. Under law 0 the best action is 0 for both histories. Under law 1 it is 0 for a and 1 for b. One revision sets the law to 1. Then K = 2 and K* = 3, and the single revision is the added word.
A script (numpy and the standard library, in the session’s scratchpad, s884_closure.py) checked these steps. It enumerated all 5,832 systems with three states, two revisions and one binary target. On every one, ≈ by partition refinement equalled ≈ by an independent pair-distinguishability closure, and the greedy word count was at most K* − K. For each system and each of the five partitions of its states (29,160 cases), the criterion agreed with a brute-force search over every update map and decoder on ρ’s image. On 3,000 seeded systems with 4 to 7 states, 1 to 3 revisions and 1 or 2 targets, the closure, the bound and the representative construction held again. The script also found states where outputs are exact but the identity Ĵ∘ρ = ρ∘J has no solution, which is A.9’s point, including one with a non-constant target. The script had three controls, each of which had to find a disagreement, and each did. The criterion with ∼_D in place of ≈ disagreed with brute force on 3,024 systems. One round of refinement in place of the fixed point disagreed on 1,051 seeded systems; at three states it cannot differ. And K* > K held on 3,024 systems. The four-state example of step 5 came out at K = 2, K* = 3.