Named Cognitive-State Forgetting Certificate

Abstract

Finite forgetting and recall histories preserve irreversible ledger marks and incompatible-claim separation.

Theorem 1.1 (The cognitive alphabet has six named states).

$$\mathrm{card}(CognitiveState)=6.$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/FiniteForgettingCertificate.cognitive_state_card (✓ std3). ∎

Source. Repository-derived.

Commentary.

The inductive alphabet consists exactly of Remember, NeverKnown, Forgotten, Misremember, Recall, and AccessRevoked. These are semantic constructors, not points of a coordinate product. The count supports the certificate but does not serve as its principal invariant.

Theorem 1.2 (Remember-forget-recall is a nonempty certified history).

$$\begin{gathered} \mathrm{Coherent}(r0)\wedge \mathrm{FiniteHistory}(r0,r2)\wedge \\ \mathrm{ForgottenLogged}(r2)\wedge \neg (\mathrm{MisrememberOpen}(r2)\wedge \mathrm{RecallOpen}(r2)). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/FiniteForgettingCertificate.remember_forget_recall_certificate (✓ std3). ∎

Source. Repository-derived.

Commentary.

A concrete coherent Remember certificate executes Forget and then Recall as two distinct admitted transitions through Forgotten. The final Recall certificate still carries forgottenLogged and cannot simultaneously carry an open Misremember claim. This supplies an occupied, non-reflexive history rather than relying on the reflexive case of finite closure.

Theorem 1.3 (Access revocation is terminal).

$$\forall s,t,\mathrm{state}(s)=\mathrm{AccessRevoked}\Rightarrow \neg \mathrm{Transition}(s,t).$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/FiniteForgettingCertificate.access_revoked_terminal (✓ std3). ∎

Source. Repository-derived.

Commentary.

AccessRevoked has no outgoing admitted action. Its certificate carries a typed revocation reason; this reason-bearing entry separates administrative loss of access from epistemic Forgotten and cannot be silently rewritten.

Theorem 1.4 (Misremember cannot jump directly to Recall).

$$\forall s,t,(\mathrm{state}(s)=\mathrm{Misremember}\wedge \mathrm{state}(t)=\mathrm{Recall})\Rightarrow \neg \mathrm{Transition}(s,t).$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/FiniteForgettingCertificate.misremember_cannot_recall_directly (✓ std3). ∎

Source. Repository-derived.

Commentary.

A false-memory claim must first be retracted to Forgotten. The dynamics has no direct Misremember-to-Recall arc, preventing a single transition from treating incompatible false and accurate claims as interchangeable.

Theorem 1.5 (Finite histories preserve the certificate invariants).

$$\begin{gathered} \forall s,t,(\mathrm{Coherent}(s)\wedge \mathrm{FiniteHistory}(s,t))\Rightarrow \\ \mathrm{Coherent}(t)\wedge (\mathrm{ForgottenLogged}(s)\Rightarrow \mathrm{ForgottenLogged}(t))\wedge \\ (\mathrm{RevokedLogged}(s)\Rightarrow \mathrm{reason}(t)=\mathrm{reason}(s))\wedge \\ \neg (\mathrm{MisrememberOpen}(t)\wedge \mathrm{RecallOpen}(t)). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/FiniteForgettingCertificate.finite_history_certificate (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every coherent source and every finite chain of admitted transitions, the target remains coherent. A prior Forgotten mark stays set; a prior reason-bearing AccessRevoked entry keeps the same reason; and the target cannot carry simultaneous active Misremember and Recall claims. This closure and monotonicity result is the certificate’s principal theorem.

References

• Truth anchor: D5/S3/ObserverMemory/FiniteForgettingCertificate.access_revoked_terminal
• Truth anchor: D5/S3/ObserverMemory/FiniteForgettingCertificate.cognitive_state_card
• Truth anchor: D5/S3/ObserverMemory/FiniteForgettingCertificate.finite_history_certificate
• Truth anchor: D5/S3/ObserverMemory/FiniteForgettingCertificate.misremember_cannot_recall_directly
• Truth anchor: D5/S3/ObserverMemory/FiniteForgettingCertificate.remember_forget_recall_certificate