RECORD 1
Two sufficient supports
SAVED BEFORE THE CORRECTION
“C and D are supported.”
Which sources support them is not retained.
Formal systems
Correction-sufficient state
A finite model of what a compressed state must retain to support a valid response to later evidence.
Required changes and permitted changes.
A true state x, an observed event e and a compatible edit universe V determine the sets Me(x) ⊆ Ue(x). The controller sees an information cell rather than the full state. Its correction must work for every state still possible in that cell.
Finite common-correction criterion
A single correction Δ is valid for every possible state x in a retained information cell Xz exactly when every required edit is permitted throughout that cell.
∃ Δ: Me(x) ⊆ Δ ⊆ Ue(x), ∀ x ∈ Xz⇔ ⋃x ∈ Xz Me(x) ⊆ ⋂x ∈ Xz Ue(x).
M specifies required edits; U specifies permitted edits; e is the observed event. Allowed patches are the complete interval between M and U, and edit atoms are mutually compatible. The cell is nonempty. Under these assumptions, the union of required edits is the minimum common patch.
This elementary set criterion provides the baseline formulation.
The encoder is chosen before the event; the decoder observes the retained code and current event. A shared codebook and the complete interval of allowed patches are explicit assumptions.
One-shot coding has a precise boundary.
Connect two states when an event makes a shared correction impossible. Under the finite interval model, a code cell is feasible exactly when it is an independent set of this conflict graph. The minimum one-shot code count is its chromatic number.
This uses established graph-coloring machinery. Outside the interval model, pairwise compatibility can fail to guarantee a correction common to an entire cell. A one-shot encoding also need not admit consistent online updates.
The result characterizes one-shot encoding in the finite interval model. Practical construction, scaling, and comparative reliability remain empirical questions.
Grounded alternative support.
Independent supports can preserve a conclusion after one premise is withdrawn. Conjunctive rules require every premise; alternative rules require one grounded route. Circular support alone is insufficient. Unsupported conclusions reopen; they do not automatically become false.
The finite reference suite covers 32,768 support states: 4,096 subsets of twelve rule templates crossed with eight evidence subsets. It also records 98,304 transitions, including 49,152 removal scenarios. These are overlapping finite-corpus accounting units, not independent empirical experiments, and are not summed into a grand total.
Verification and scope
- Verification
- The stated finite model, written arguments and source-bound reference suite establish the local result. Audit replays check implementation behavior on the declared domain.
- Corrections
- The broader prototype passed authored tests while missing intended propagation and authority behavior. The kernel makes its narrower obligations explicit; prototype success is not transferred to the kernel or vice versa.
- Boundary
- The finite suite checks implementation behavior within its declared support model. Comparative reliability requires a separately specified empirical study.
Correction model
Finite illustration · no model calls
Identical answer summaries can require different corrections after a source is withdrawn.
Interactive source-withdrawal example
RECORD 2
One sufficient support
SAVED BEFORE THE CORRECTION
“C and D are supported.”
Which sources support them is not retained.
Each root independently supports C; C supports D. The decoder receives only the selected representation and the withdrawal event.
Keep C and D supported.
Record A’s withdrawal. B still supports C, and C still supports D, so neither claim-status record needs reopening.
Reopen C and D.
A was the last supporting root. Both claim-status records need reassessment. Neither claim has thereby been proven false.
Both histories justify the same saved answer.
Withdraw A to see whether the selected memory format preserves enough information for the next decision.
“Supported” means grounded under the example’s admitted rules. It is not an unrestricted guarantee of truth.
Computed check and assumptions
Rules: A ⇒ C; B ⇒ C; C ⇒ D. The required and permitted patch is exactly closure(before) − closure(after). The browser computes grounded closure, groups the histories by their saved symbol, and checks whether each group admits one common exact correction.
Reference patches after withdrawing A: Record 1 = ∅; Record 2 = {reopen C, reopen D}.Retrieving the original supporting record is a legitimate way to resolve the ambiguity. It supplies additional information, with its own retrieval and verification costs. This example does not establish that structured memory beats retrieval, or that a real system can construct the records correctly.
RR-ETI and sequential maintenance.
RR-ETI studies revision decisions under partial information and explicit decision assumptions. Its cost-universal statistic and fixed-cost tied optima have different boundaries. The missing historical RR validation code remains an evidence gap; the manuscript is not represented as freshly replayed.
Maintaining a compressed state through a sequence adds an update-consistency obligation. The finite release remains a compact note; any substantive later result requires its own version and review.
Study 14 asks whether actual systems can construct and maintain the distinctions the formal model assumes, and at what cost.
The separate note and implementation remain unpublished.