What an Empty Result Licenses: A Sound Calculus of Absence Claims for Phone Evidence

1 Introduction

A report that says “no messages were found on 3 March” is a statement about a search. Readers take it as a statement about the world. The step between the two is the subject of this report: what an empty result licenses a reader to conclude about an event on a phone, and what it does not.

A motivating example. Take a synthetic case. A phone is acquired on 28 June and the question is whether a messaging application was opened on 3 March. The usage store returns nothing for that day. Three facts produce the same empty result. The phone was set up on 20 May, so it did not exist on 3 March. The usage store keeps ten days. And the only other store that mentions the application, the App Ops access record, holds the time of the last access and nothing else. Table 1 gives the verdict of the checker described below for six claims on this item. Both the claim and its negation are undetermined for 3 March, and the checker names the three reasons. For 10 June the last-use record establishes a use. For 20 and 27 June the usage store observes both days and finds nothing, so their absence is established. The sentence “no events on 3 March” is true in all three readings of the empty result and informative in none of them.

The problem. Absence claims are the weakest and the most consequential statements in a phone report. A claim that nothing happened is read as exculpatory, and a claim that something did is read against its source. The literature treats a negative result as open to several readings [1], and as worth what the probability is that the event would have left a trace [2]. What is missing for phones is a semantics: a precise statement of when an absence claim follows from an evidence item, with the reasons when it does not, rules for combining several stores and several claims, and a statement of what can go wrong.

Relation to our earlier reports. LAB-TR-0019 [3] gives each phone setting one accountable state with a typed reason when no value was established. Its unit is a setting at the time of acquisition, it has no dates, and it does not combine claims. LAB-TR-0029 [4] defines a date-bound question as answerable, partly answerable or not answerable from three limits, with a rule function, and measures how often that holds. It answers one question about one date at a time and states no guarantee. The present report differs in three ways. It gives a semantics for claims, with negation, conjunction and disjunction over many cells and stores. It proves what the semantics guarantees and where it fails, with counterexamples. And it adds a test of its own assumptions: two stores that should agree can contradict each other, and the calculus names the contradiction. Both earlier reports are special cases (Section 4.6 for answerability, Section 2.5 for settings).

We ask four research questions.

• RQ1 (Semantics). Can absence claims over several stores receive a compositional semantics with typed reasons for what cannot be observed?
• RQ2 (Guarantees). What can be proved about it, under which assumptions, and what fails when they are false?
• RQ3 (Checker). Does an executable implementation agree with the proofs, and how do violated assumptions show up?
• RQ4 (Devices). On real phones, which claims can be established, which reasons block the others, and do the model’s assumptions hold?

Contributions. This report makes four contributions.

• A semantics for absence claims over phone stores with typed reasons for what cannot be observed, composition rules, and a checker that implements it (Section 3).
• Theorems with proofs and counterexamples: soundness, exactness for read-once claims, stability under added evidence, explanations by blocking cells, and the relation to answerability (Section 4).
• A validation by exhaustive enumeration and by fault injection that shows how violated assumptions appear (Sections 6.1 and 6.2).
• An evaluation on 54 real items, including two tests of the model’s own assumptions, one of which found an incomplete witness of calls (Sections 6.3 and 6.4).

Scope. The semantics concerns the capacity of an evidence item to support a claim, given a model of its stores. It does not estimate how likely an event is, does not weigh evidence, and does not say that a store is complete beyond what the model states. The corpus results describe the Lab’s research corpus: 33 iOS and 14 Android full file system extractions and 7 Android bug reports; most iPhones run iOS 26, most Android phones Android 16, and 12 of the 14 Android phones are Samsung. Section 8 states the limits.

2 Background and Related Work

2.1 Negative evidence in legal and forensic science

Two jury experiments varied the probability that a test would have detected gunshot residue if a gun had been fired, and found that jurors gave a negative result less weight when detection was unlikely [2]. The point is the one the maxim “absence of evidence is not evidence of absence” makes in medicine [5]: what an empty result shows depends on whether the finding would have been made. Biedermann and Vuille analysed a Swiss case in which digital data were presented from one side only, and used probability and graphical models to show how partial presentation misleads [1]. Horsman proposed certainty descriptors for stating how sure an examiner is of a digital finding [6]. Casey and others set out a Bayesian framework for location-related mobile evidence that separates what was observed from how it bears on competing propositions [7]; our calculus works one level below, on what can be observed at all. These works treat negative findings as a problem of reasoning and communication. They do not give a rule that decides, from a device and a date, whether the device could have recorded the event.

2.2 Closed worlds, local closed worlds and completeness statements

Reiter’s closed-world assumption reads the failure to find a fact in a database as its negation [8], and Clark’s negation as failure gives it a logical reading [9]. Applied to a phone, the assumption would say that every event left a record, which no store satisfies. Motro separated the validity of a database (nothing false in it) from its completeness (nothing true missing) and gave a model in which the integrity of an answer is certified [10]. Etzioni, Golden and Weld introduced local closed-world information for planning: a statement that the agent knows every instance of a pattern, here every file in one directory, which permits a sound conclusion that a fact outside the known set is false [11]. Razniewski and Nutt model a partial database as a pair, an ideal database and the available one that it contains, and use table completeness statements to decide whether a query answer is complete; they show that the statements identify the parts of a database that matter for a query [12]. Darari and others carry the idea to RDF sources [13], and a survey covers completeness, recall and negation in knowledge bases under partial closed-world semantics [14].

Our observed region of a store is a completeness statement in this sense, and our consistent worlds are their ideal databases. We use these ideas and do not claim them. What we add is the derivation of the statement from the device (its life, its retention and the meaning of its records), a positive-only region that the database literature does not need, and the use of disagreement between two statements as a test of the model.

2.3 Many-valued logics and certain answers

Kleene’s strong three-valued logic gives a third value to what cannot be decided [15]. Belnap’s four-valued logic adds a value for contradictory information from several sources [16]. Libkin showed that SQL’s three-valued evaluation over nulls can return answers that are not certain, and that sorting answers into certainly true, certainly false and unknown restores a guarantee [17]. Our values are Kleene’s, our conflict is Belnap’s fourth value used as an alarm, and our entailment is certain-answer semantics over the consistent worlds. The reasons attached to the unknown value are the contribution of this report to that line.

2.4 Explaining missing answers

Why-not provenance explains why a tuple is missing from a query result. One approach finds the manipulation that discarded it [18]; another gives provenance-style explanations for non-answers over extracted data [19]. Our blocking sets and reasons play the same role for a claim that cannot be decided, and Theorem 5 states when they are exact. Recent work on language models draws the same line between a justified negative and insufficient evidence, and finds that models often treat partial coverage as complete [20].

2.5 Formal models in digital forensics

Gladyshev and Patel proposed a finite state machine approach to digital event reconstruction [21]; James and others use the approach to test whether an evidential statement is feasible against a system model [22]. Gruber and Humml give formal definitions of the relevance and expressiveness of digital evidence and compute the expressiveness of facets with temporal logic and a model checker [23]. Their evidence collection consists of found facets and facets that could not be retrieved, and completeness is defined relative to a set of hypotheses; the unretrieved facets carry no stated reason [23]. Gruber and others define sufficient evidence, the states whose observation proves that an event occurred, and necessary evidence, the states whose negation refutes the claim that it occurred, in linear temporal logic and compute both with a model checker [32]. Freiling and others give a formal model of evidence collection through abstraction layers and show that layers make evidence harder to acquire [24]. Hornung and others give a formal model of timestamp normalization and show that normalization does not guarantee comparability [25], and Dreier and others integrate sequence numbers and line numbers into a partial order of events [26]. These models reason about when events happened and in what order. None of the abstracts or texts we read gives a semantics for what an empty result means.

Our own reports are inputs. LAB-TR-0019 [3] is the case of a cell with no time dimension: a setting at acquisition is one cell, and its determined states correspond to P or A, its not-determined states R2 to R4 (store not in the item, present but not read, not carried by the class) to U with reason X, R1 (absent at a documented default) to an absence that documentation licenses, and its inconclusive state, in which copies disagree, to a conflict. LAB-TR-0029 [4] is the answerability profile of a cell (Section 4.6). LAB-TR-0021 [27] measured retention horizons, LAB-TR-0028 [28] the start of a device’s life, LAB-TR-0022 [29] clock anomalies and LAB-TR-0023 [30] what SQLite leaves of a deleted row; the first two supply the regions of the stores, the others motivate the extensions K and D.

Position of this work. The logic of partial closed worlds and completeness statements, the three-valued and four-valued treatment of unknown and contradictory information, and the explanation of missing answers are established in database theory and artificial intelligence. Formal models of digital evidence address time, order, relevance, feasibility and the sufficiency of an evidence collection. Negative findings are studied as a problem of reasoning in court. We found no semantics for absence claims over device stores that derives typed reasons from the life of the device, the retention of the store and the meaning of its records; that combines several stores and claims with a soundness theorem; and that uses a conflict between stores as a test of its own model. Nor did we find an evaluation of such a calculus on real devices. The search covered the arXiv, Zenodo, OpenAlex and Crossref interfaces, with dblp and Semantic Scholar blocked or rate-limited, and web search (29 October 2026; the private notes log the queries). The logical core is an instance of known ideas; the instantiation, the checker and the measurements are new here, as far as we found.

3 The Calculus

3.1 Cells, worlds and claims

A cell is a triple (type, subject, granule): an event type such as app use, a subject such as one application or one person, and a time granule such as one UTC day. C is a finite set of cells. A world w ⊆ C is the set of cells in which at least one event occurred. A claim is a formula over the atoms occ(c) with ¬, ∧ and ∨. “No use of the application on any of seven days” is the negation of the disjunction of seven atoms. Claims describe the activity of the device’s user, not of one device: an event on an earlier handset is in the world, and an item that began later cannot see it (reason B).

3.2 Stores

A store s is a quadruple (P_s, O_s, ρ_s, Rec_s) with O_s ⊆ P_s ⊆ C and Rec_s ⊆ P_s. The positive region P_s holds the cells in which a record that was found is evidence that the event occurred. The observed region O_s holds the cells in which the absence of a record is evidence that it did not. Rec_s are the cells in which the examiner found a record; a record outside P_s is discarded and counted. The function ρ_s assigns to every cell outside O_s a non-empty set of reasons (Table 3) and to every cell inside it the empty set. A last-use store has O_s = ∅ with reason S and one cell in Rec_s: it can confirm and never deny.

The regions come from three limits that earlier reports measured. Boundary: no cell before the earliest evidence that the device existed is in O_s (B). Horizon: no cell before the oldest record of the store is in O_s (H). Semantics: a store of last use or of state has an empty observed region (S). A store that is absent or cannot be decoded has empty regions (X). Figure 1 shows the effect of the three limits on the status of a cell, and Listing 1 gives the construction used in Section 5.

regions(store s, cell c):
  rho = {}
  if s absent / unreadable / not in the class:   rho += X
  elif s has no dated record:                    rho += S
  else:
    if e0 < oldest(s):                            rho += H
    if device-bound type:
      if no indicator:                            rho += B
      elif e1 < lo:   rho += B; c not in P_s
      elif e0 < hi:   rho += B
    elif e0 < lo:                                 rho += B
    if semantics(s) in {last use, state}:         rho += S
    if clock check failed and semantics = history: rho += K
    if removal extension and s is erasable:       rho += D
    c in P_s  iff  e0 >= oldest(s)
                 and not (device-bound and e1 < lo)
  c in O_s  iff  rho is empty

3.3 Evidence items and assumptions

An evidence item E is a finite set of stores over C. A world w is consistent with E if, for every store, A1 every record found is true: Rec_s ⊆ w, and A2 every event in the observed region has a record: w ∩ O_s ⊆ Rec_s. A3, that a record sits in the cell of its event, is part of the definition of a cell: a date or a subject that is wrong puts the record in the wrong cell. W(E) is the set of consistent worlds. A1 to A3 are the assumptions of the model; Section 4.5 shows what each failure does.

3.4 Status of a cell and value of a claim

The status of a cell c on E is conflict if one store has a record in c and another observes c with none; otherwise P (present) if some store has a record in c; A (absent and observable) if some store observes c and holds none; otherwise U(ρ), where ρ is the union of the reasons of all stores. The value of a claim on a conflict-free item is T, F or U(b), by the rules of Table 4: the three values of the strong Kleene logic, with the set b of cells that block the claim. A cell has the value T when P, F when A and U({c}) when U. We write [φ]_E for the value. A claim of absence is established when its value is T.

3.5 Extensions

Two reasons beyond the core handle failures of A2 and A3 without changing the proofs. A store whose records a user can delete is downgraded: its observed region becomes empty, every cell it observed gets the reason D, and its records still count as evidence. A store whose dates failed a clock check is downgraded the same way with reason K. A downgraded store is still a store, so every statement of Section 4 applies; the soundness it gives is against a larger class of histories, in which the store may have lost records or misdated them, at the price of fewer decided cells.

4 Properties

All statements below are for an evidence item E without conflict unless stated. The worlds consistent with E are characterised first. Entailment is truth in all consistent worlds: E entails φ if every w in W(E) satisfies φ, refutes it if none does, and leaves it open otherwise. This is certain-answer semantics [17] and the possible-worlds reading of knowledge [31]. Table 6 in Section 6.1 lists the enumerations that check each statement mechanically; the proofs are for all sizes.

4.1 Consistent worlds

Lemma 1 (consistent worlds). Let F⁺ be the union of the sets Rec_s and F⁻ the union of the sets O_s − Rec_s. Then W(E) = {w : F⁺ ⊆ w and w ∩ F⁻ = ∅}, and W(E) is empty iff some cell has the status conflict.

Proof. A1 for all stores says F⁺ ⊆ w. A2 for all stores says that no cell of O_s − Rec_s is in w, that is w ∩ F⁻ = ∅. A set with both properties exists iff F⁺ ∩ F⁻ = ∅. A cell lies in the intersection iff some store has a record in it and some store observes it with none, which is the definition of conflict. □

Thus, without conflict, the cells of F⁺ are P, those of F⁻ are A, and every other cell is free: membership in w is unconstrained and independent of all other cells.

4.2 Soundness and exactness

Theorem 1 (soundness). If [φ]_E = T then every consistent world satisfies φ; if it is F then none does. In particular, if the real history of the user is a consistent world, every decided claim is true of it.

Proof. By induction on φ. For an atom, T means P and the cell is in F⁺; F means A and the cell is in F⁻; Lemma 1 gives the claim. For ¬φ′ the value swaps, as does truth. For φ′ ∧ φ″: the value is T only if both are T, and then both hold in every consistent world by the induction hypothesis; it is F only if one is F, and that conjunct fails in every consistent world. The case of ∨ is dual. □

Theorem 2 (exactness). (a) If φ is read-once, that is, no cell occurs in it twice, then its Kleene value is exact: it is T iff E entails φ, F iff E refutes it, and U iff both a consistent world that satisfies φ and one that does not exist. (b) For claims that repeat a cell the Kleene value may be U although the claim is entailed or refuted. (c) Let rep(φ) be the free cells that occur more than once. Evaluating φ with each assignment of truth values to rep(φ) substituted and combining the results (T if all are T, F if all are F, otherwise U) equals entailment for every claim.

Proof. (a) Let Val(φ) be the set of truth values of φ over the consistent worlds. We show Val = {1} if the value is T, {0} if F and {0,1} if U, by induction. For an atom this is the description after Lemma 1: a free cell is in some consistent worlds and not in others. Negation maps Val to {1−v}. For a conjunction the two conjuncts mention disjoint sets of cells; by Lemma 1 the membership of distinct cells is independent, so the pair of truth values ranges over Val(φ₁) × Val(φ₂) and Val(φ₁∧φ₂) = {ab : a ∈ Val(φ₁), b ∈ Val(φ₂)}. Checking the table: {1}{1} = {1} (T and T give T); {0}·anything = {0} (F); {1}·{0,1} = {0,1} and {0,1}·{0,1} = {0,1} (U). Disjunction follows by De Morgan, which the Kleene rules satisfy. (b) φ = occ(c) ∨ ¬occ(c) with c free is true in every world, and the rules give U ∨ U = U. The conjunction occ(c) ∧ ¬occ(c) is the refuted case. (c) The worlds with a given assignment to rep(φ) form a product over the remaining free cells. Under an assignment, φ becomes a claim in which only resolved cells repeat, and the induction of (a) applies unchanged to it, because a resolved cell has a one-element Val and is independent of every other cell. Val(φ) is the union over assignments, and entailment is T iff every assignment gives T, F iff every one gives F. □

The exact evaluation takes time exponential in |rep(φ)|. No polynomial algorithm is to be expected in general: with no cell observed, deciding whether φ is entailed is deciding whether a propositional formula is valid, which is coNP-complete.

4.3 Added evidence and pooling

Theorem 3 (stability under added evidence). Let E′ extend E: it adds stores, or replaces a store by one whose positive and observed regions are at least as large and whose records agree with the old store on the old positive region. If E′ has no conflict, then every atom that is P or A on E keeps its status, and the value of every claim can only change from U to T or F. A decided value never changes.

Proof. If a cell is P on E, some store has a record in it; its counterpart in E′ still has the record, so the cell is P or conflict on E′. If it is A, some store observes the cell with no record; the counterpart observes it and, agreeing on the old positive region, holds none, so the cell is A or conflict. Without conflict the statuses are kept, and the U atoms may become P or A. Define the information order U ⊑ T and U ⊑ F. The Kleene connectives are monotone for it, because a T or F result depends only on decided inputs, and decided inputs do not change. A decided value is maximal, so it is kept. □

Corollary (assumption relativity). If a decided claim is false of the real history, then some store violates A1 or A2 (a record in the wrong cell, a violation of A3, misleads only through a violation of A1 at the wrong cell or of A2 at the right one). Adding a store that observes the affected cell and satisfies A1 and A2 there exposes the violation as a conflict; a violation in a cell that no other store observes cannot be seen from the evidence.

Proof. The first sentence is the contrapositive of Theorem 1. A violated A1 is a record c ∈ Rec_s with no event in c; a second store s′ that observes c and satisfies A1 and A2 there has no record in c, so c ∈ O_s′ − Rec_s′, a conflict. A violated A2 is an event in c ∈ O_s without a record; s′ holds a record in c while c ∈ O_s − Rec_s, again a conflict. □

Proposition 4 (pooling). (i) The status of a cell on the pooled item E₁ ⊎ E₂ is the join of its statuses: U with the union of the reasons joined with P or A gives P or A; P joined with A is a conflict. (ii) For claims, if the pooled item has no conflict, [φ] on it is at least the join of [φ]_E1 and [φ]_E2 in the information order, and can be strictly more.

Proof. (i) is the definition of status applied to the union of the stores. (ii) The lower bound is Theorem 3. For strictness let φ = occ(a) ∧ occ(b); E₁ records a and does not observe b, E₂ records b and does not observe a. Each gives U for φ and the pooled item gives T. □

The practical reading of (ii) is that conclusions must be drawn from the pooled evidence.

4.4 Explanations

Theorem 5 (explanations). Let φ be read-once with [φ]_E = U(b). Then (a) b is exactly the set of pivotal cells: the free cells c for which two consistent worlds that differ only in c disagree on φ; (b) if an extension E′ of E without conflict leaves every cell of b free, then [φ]_E′ is still U. Hence any evidence that settles φ must observe or record at least one cell of b, and the reasons of the cells of b say what kind of source that is.

Proof. (a) By induction. An atom: b = {c} and c is pivotal. Negation: the same cells. A conjunction φ₁∧φ₂ with value U has the value pairs (U,U), (U,T) or (T,U). In (U,U), b = b₁ ∪ b₂. A cell of b₁ is pivotal for φ₁ by the hypothesis; choose the cells of φ₂ so that φ₂ holds, which is possible by Theorem 2a since its Val is {0,1}; then it is pivotal for the conjunction. Conversely a pivotal cell of the conjunction lies in φ₁ or φ₂ (read-once) and changes that conjunct, so it is in the corresponding b_i by the hypothesis. In (U,T), b = b₁; cells of φ₂ are not pivotal because φ₂ is true in every consistent world, and the cells of φ₁ are as before. Disjunction is dual. (b) By induction on the same cases: in (U,U) each side keeps its blocking cells free and stays U by the hypothesis, so the conjunction stays U; in (U,T) the T side stays T by Theorem 3 and the U side stays U; disjunction is dual, with F in place of T. □

4.5 Assumptions and counterexamples

Table 5 lists what happens when each assumption fails, and the rows that are properties of the calculus. Soundness is relative: the theorems say nothing about a model that is wrong. The failures of A1 and A2 produce wrong decided verdicts in a single store, which the enumeration finds in every case, and a second store that observes the cell turns each of them into a conflict. The calculus is also incomplete relative to reality: a rule of the world that the model omits, such as “an application was installed before it was used”, decides claims the calculus leaves open. We leave such rules out because each needs its own validation.

4.6 Answerability as the profile of a claim

LAB-TR-0029 classified a question as answerable, partly answerable or not answerable before looking at any record [4]. In the calculus this is the set of values a cell can take over all ways the item can come out. A completion of a model of stores without records is a world w and, for each store, a record set between w ∩ O_s and w ∩ P_s. The profile of a claim is the set of values it takes over the completions.

Proposition 6 (profile). The profile of a cell is {T, F} if some store observes it (answerable), {T, U} if no store observes it and some store has it in its positive region (partly answerable, confirm only), and {U} otherwise (not answerable). For a read-once claim the profile is obtained by applying the Kleene rules to the profiles of its cells.

Proof. If a store observes c, every completion has a record iff c ∈ w, and both cases occur. If no store observes c but a store has it in its positive region, a record may or may not be present when c ∈ w, and none can be present otherwise, so T and U occur and F does not. If no store has it in a positive region, records at c are discarded. For a read-once claim, the choices for distinct cells are independent in a completion, so the argument of Theorem 2a gives the set. □

Thus the three verdicts of LAB-TR-0029 are the profiles of a cell, and the calculus adds what that report lacks: the value an item actually returns, negation and combination, a flavour that the earlier report had no name for (deny only, the profile {F, U}, which a conjunction of an answerable cell and an unobservable one has), a guarantee, and reasons as sets.

5 Checker and Evaluation Design

5.1 The checker

The checker is a Python module of about 470 lines using only the standard library. It represents stores and items as in Section 3, evaluates claims by the Kleene rules, evaluates exactly by case splitting on repeated free cells, returns the blocking cells and their reasons, computes pivotal cells and profiles, and reads a claim from text (not any(a,b) and c). The same module is applied to the synthetic instances and, through a second module that builds stores from device records, to the corpus.

5.2 Synthetic checks

Two sets of synthetic checks test the proofs and the behaviour under faults. The exhaustive checks enumerate, for items over three, four and five cells, every status vector and every claim up to a stated size (for four cells a random sample of 6,000 of the claims up to three leaves, for five cells random claims), and, for two stores over three cells, every pair of store specifications, every world and every faithful record set. They check each statement of Section 4 against an enumeration of the consistent worlds, which Lemma 1 characterises; Lemma 1 itself is checked against the definitions A1 and A2 by enumerating all sets of cells. The fault injection generates 20 worlds of 20 subjects and 90 days with a use probability per subject, builds a history store that keeps 30 days, a second that keeps 14 days and a last-use store, loses a share of the records of the first store or adds phantom records, and compares every verdict with the generating world.

5.3 Corpus evidence

The frame is the 54 items of LAB-TR-0029 [4]: 33 iOS and 14 Android full file system extractions and 7 Android bug reports of the Lab’s research corpus, read once in that study for the dates of three to twelve stores per item and for the start-of-life indicators. We build the stores of each item from those dates with Listing 1 and the witness stores of that report for five question types (installed, used, permission used, contact, place), and apply the calculus to profiles, that is, to what each item can and cannot decide. The place type is measured on iOS only. A cell is a day or, for the comparison with LAB-TR-0029, the instant that many days before acquisition. The clock check, the start-of-life indicators and the device-bound and person-bound types are those of that report. The construction was fixed before the results were read; the variants of Table 12 are post hoc.

5.4 Tests of the model assumptions

Two further readings test the assumptions rather than apply them. The hole test asks whether a store that keeps one file per day has a file for every day between its oldest and newest, which is the assumption that its observed region is an interval; it uses the times of the files: neighbouring files should lie one day apart (23 to 25 hours at a clock change) and a larger spacing counts the days in between as missing. Counting the expected days from UTC day numbers would be wrong for files named by a local midnight, because the time of day of the file names can shift inside the span (here by 2.6 hours over nine days on one phone, from an unexamined cause such as a clock-offset change), which moves the newest file across a UTC day boundary and adds a day that is not missing. The conflict test takes two stores of one iPhone that both claim to observe contact, the message store and the call history against interactionC (the iOS database that holds one row per recorded interaction, with a start date and an application identifier), and asks whether the days on which one holds a record are also days on which the other holds one. For this reading we collected, for each of the 33 iPhones, the set of UTC days on which each store holds at least one record, and for interactionC separately the days of records whose application identifier is the system messaging application, the system telephone application, or another. Only day numbers were kept. The conflict count is that of the calculus on the cells both stores observe, with interactionC restricted to the records attributed to the messaging or the telephone application. Records of other applications are not records of messages or calls; their coverage is reported only as a bound.

6 Results

6.1 Exhaustive checks

Every statement of Section 4 held on every enumerated instance (Table 6). The incompleteness of Theorem 2b is common among claims that repeat a cell: the Kleene value was U although the claim was decided in 9.6% of the non-read-once pairs over three cells, 9.0% over four and 6.6% over five. Exact evaluation removed all of them. On the faithful two-store items the pooled item was never in conflict, and an example of Proposition 4 (a claim decided only by pooling) was found at once. Breaking A1 or A2 in one store produced a wrong decided verdict in every case examined, and a second store that observed the same cell flagged every one.

6.2 Fault injection

Without faults no verdict was wrong, with one store or two. With records lost from the first store, wrong verdicts followed (Table 7): of the cells with absence established, 4.4% were wrong at 5% loss and 14.6% at 20%, and the share of wrong claims was higher for windows (the 7-day absence claims that were established were wrong in 23.4% of cases at 20%, against 14.6% for single days). A second witness flagged 47% of the injected errors at 20% loss, those inside its 14-day reach; the rest lay outside it and went unseen. The share of wrong absence verdicts fell from 14.6% to 8.9%. Treating the first store as confirm-only (extension D) removed every wrong absence verdict, at the price of deciding fewer cells: with two witnesses, 2,925 cells had absence established where the naive model established 6,910. Phantom records are a different fault: they produce wrong presence verdicts, which the extension D does not remove, because D weakens only absence.

6.3 Real devices

Reproduction of the earlier verdicts. The calculus agreed with the rule function of LAB-TR-0029 on 2,405 of 2,420 cells (the measured device-by-type combinations, ten lags, instants); the 15 differences were all of one kind. A last-use or state store older than the lag counts as partly answerable in the rule function; in the calculus it has no record that old, so the cell is not answerable. Our reimplementation of the rule function equals the original on all 2,700 cells (0 differences). At 30 days before acquisition, 91 of 242 cells (device by question type) were answerable (Table 8).

Reasons. 151 cells could not be answered at 30 days (Table 9, Figure 2). 92 had one reason and 59 had two or three, so the single binding limit that the earlier report named for each cell is one of several for about a third of them (39%). Store semantics (S) was among the reasons of 102 cells, the horizon (H) of 50, an absent or unreadable store (X) of 21, the device-life boundary (B) of 22 and an untrusted clock (K) of 21.

Windows and conjunctions. An absence claim over a window needs every cell of the window observed (Section 4). The window over which absence of any app use could be established fell with its width (Table 10, Figure 3): on the iPhones, from 24 of 33 at one day to 15 at 30 days and 5 at 60 days, and on the Android phones from 11 of 14 at one day to none from ten days. Contact windows were far more durable: 21 of 33 iPhones at 60 days, 12 of 14 Android phones. Conjunctions of absences are weaker still (Table 11). The claim that nothing of four kinds (installed, used, permission used, contact) happened on the day 30 days before acquisition could be established on 0 of 47 phones, because on the iPhones permission use and on the Android phones the installed state is never answerable from the stores read (a state or last-use store), and the claim could still be refuted on 31 of 33 iPhones. Without the permission type it could be established on 10 of 47 phones, and the three measured kinds could be established on 0 of 7 bug reports. A report that says “no activity on that day” therefore asserts, for these four kinds, more than any of these items can support.

Variants. Table 12 shows how much the answerable counts depend on model choices. Reading the boundary at the earliest indicator rather than the latest raises the iOS use count from 17 to 20 and the place count from 21 to 25. Removing the clock cap raises contact from 25 to 30 on iPhones. Treating the message and call stores and geotagged photographs as erasable (reason D) cuts the Android contact count from 12 to 0 and the iOS place count from 21 to 19; the iOS contact count stays at 25 only because interactionC is counted as an observing witness. With D and interactionC both confirm-only the iOS contact count is 0: the absence of contact would then rest on stores the user can edit.

6.4 Tests of the model

Holes. The Android daily usage files cover every day of their span on 13 of 14 phones; 1 phone lacks 4 of 116 day cells. The iOS power-log archives, one per day, lack 48 of 188 day cells on 8 of 28 phones. The assumption that the observed region of a history store is an interval is therefore false for some devices, and the cells in the holes are overstated as observed. The data kept do not locate the holes, so the profile tables of Section 6.3 are not corrected for them.

Conflicts. On the 30 iPhones that hold a message store and interactionC, the message store has a record on 3,864 of the 6,007 days both stores reach, and interactionC records attributed to the messaging application on 2,313; 1,558 days are conflicts in which only the message store has a record, on 16 devices, and 7 are conflicts in which only interactionC has one, on 3 devices. For calls, the call history has a record on 2,922 days and interactionC records attributed to the telephone application on 427; 2,500 days (86%) are conflicts in which only the call history has a record, on 28 devices, and 5 the other way. Records of any application cover 94% of the call-history days (2,744 of 2,922) and 85% of the message days (3,267 of 3,864), but interactionC holds records of many kinds of interaction, so this coverage does not show that calls or messages are recorded. The finding is therefore narrow: interactionC records attributed to the telephone application, and to a lesser degree to the messaging application, are not a complete witness of calls and messages. The earlier model counted all interactionC records as a witness of contact, a broader event, so the test checks part of that use and does not refute it. A day on which only interactionC has a record is consistent with a message deleted from the message store; it is the pattern that the removal reason D describes, and the data do not separate deletion from other causes. Treating interactionC as confirm-only removes the first kind of conflict by construction and changes no verdict of Section 6.3 at 30 days on these phones (Table 12).

7 Discussion

7.1 What a negative statement should say

A report that finds no record can state, for each claim, one of three things, with the reasons attached: established (a store observed the cells and found nothing), refuted (a record exists), or undetermined because of B, H, S, X, R, K or D. Table 1 is the template. The reasons turn “nothing found” into an instruction about what to look for next. The fix for B is an earlier handset or the account that carried data over, for H a source that keeps its records longer, for S a store with history, and for X, K and D a readable copy, a time anchor or a witness the user cannot edit.

7.2 Compound claims need pooled evidence

Proposition 4 and Table 11 point the same way. A conclusion that combines several claims cannot be assembled from the conclusions of separate sources. Two stores that each say “cannot tell” may together decide the claim, and a single claim that nothing at all happened is no stronger than its weakest part. The practical rule is that a report should state the largest window and the widest set of event types for which absence is established, not a blanket statement.

7.3 Conflicts as a test of the model

Soundness is relative to the model, and a model can only be tested against the data. A conflict between stores is a symptom of a violated assumption that the stores themselves can show. The interactionC finding is an instance in part: records attributed to the telephone application, taken as a witness of calls, are contradicted by the call history. Treating the store as confirm-only changes no verdict on these phones at 30 days, but it would change a verdict on a phone where interactionC was the only store that reached a date.

8 Threats to Validity and Limitations

Internal. The theorems are proved for the model, not for phones. The regions of the stores come from documentation, earlier reports and file schemas, and were not tested with known events; Table 5 shows what happens if they are wrong. The exhaustive checks cover three to five cells; the proofs cover all sizes, and the checks guard against errors in the proofs and in the implementation, not against the model. The fault injection uses invented parameters. The corpus profile is built from the dates collected for LAB-TR-0029, so errors in those readings carry over. The conflict reading is a direct read of the stores, and its counts depend on how a day and an application identifier are read.

Construct. A cell is a day with at least one event; the calculus cannot express counts, order or time of day. A claim is about a user’s activity; the corpus items show the device, not the user. Established absence means that the model says the store would have recorded the event, not that the event did not occur.

External. The corpus is not a random sample. Most iPhones run iOS 26 and most Android phones Android 16, 12 of 14 Android phones are Samsung, and bug reports are seven items whose relation to the extractions was not established. The conflict test covers iOS only, on the stores for which a second witness exists.

Conclusion validity. The corpus counts are counts of devices, with no test; they describe the sample. The model variants are post hoc.

Limitations. The calculus does not weigh evidence or estimate probabilities, does not include world rules such as install before use, and does not use the negative information that a last-use record carries about later days. Redaction (R) is defined and checked but not measured on these items. No controlled event was run on any device, so the store semantics are not validated against known activity; that, and a larger sample, are the next steps.

9 Conclusion

An empty result licenses a conclusion only where the evidence could have shown the event. We made that statement precise as a calculus: cells are present, absent and observable, or unobservable for reasons; claims compose by the Kleene rules; the calculus is sound relative to three assumptions, exact when no cell repeats, stable under added evidence, and its failures are exposed by a second store. On 54 real items it reproduced the earlier answerability verdicts, showed that a third of the undecided cells have two or more reasons, and showed that a claim of no activity of four kinds on a day 30 days before acquisition could not be established on any phone. A report that adopts the calculus says, for each negative claim, whether it is established, refuted or undetermined, and why.

Future work, in order of value: (1) controlled events on Lab-owned devices to test the regions of the stores; (2) world rules, so that a use implies an install; (3) the negative information in a last-use record; (4) an interval version of the cells for clock error; (5) a study of whether a report that states reasons changes what examiners conclude.