Terminal Ledger Partition

Abstract

Terminal grades partition the semantic ledger into migrated, wall, and resident sets.

Theorem 1.1 (Terminal grades give a three-way ledger partition).

$$\begin{array}{c}\forall Statement,Grade:\mathrm{Type},\\ [\mathrm{Countable}(Statement)],[\mathrm{Finite}(Grade)],[\mathrm{PartialOrder}(Grade)],\\ \forall \sigma :\mathrm{LedgerHistory}\left(Statement,Grade\right),\\ (\forall s:Statement,\mathrm{Finite}\left(\mathrm{revisionTimesFrom}\left(\mathrm{enrolledAt}\left(\sigma ,s\right),(t:\mathbb{N}\mapsto \mathrm{grade}\left(\sigma ,s,t\right))\right)\right)),\\ \forall Gplus:\mathrm{Set}\left(Grade\right),\forall Sem,W,T:\mathrm{Set}\left(Statement\right),\\ W\subseteq Sem,\forall forbidden:\mathbb{N}\to Statement\to \mathrm{Prop},\\ (\forall t:\mathbb{N},g:Statement,g\in T\Rightarrow \mathrm{grade}\left(\sigma ,g,t\right)\in Gplus),\\ (\forall t:\mathbb{N},w:Statement,w\in W\Rightarrow \mathrm{grade}\left(\sigma ,w,t\right)\in Gplus\Rightarrow (\forall g:Statement,g\in T\Rightarrow \mathrm{grade}\left(\sigma ,g,t\right)\in Gplus)\Rightarrow \mathrm{forbidden}(t,w)),\\ (\forall t:\mathbb{N},w:Statement,w\in W\Rightarrow \neg \mathrm{forbidden}(t,w))\\ \Rightarrow \exists !{\sigma }_{\infty }:Statement\to Grade,\\ (\forall s,\exists N\ge \mathrm{enrolledAt}(s),\forall t\ge N,{\sigma }_t(s)={\sigma }_{\infty }(s))\wedge \\ M=\mathrm{intersection}(Sem,\mathrm{preimage}({\sigma }_{\infty },Gplus)),R=Sem\setminus (M\mathrm{union}W),\\ Sem=M\mathrm{union}W\mathrm{union}R\wedge \\ \mathrm{Disjoint}(M,W)\wedge \mathrm{Disjoint}(M,R)\wedge \mathrm{Disjoint}(W,R).\end{array}$$

Proof. Machine-checked in Lean as D5/S0/Computability/LedgerGovernance/TerminalLedgerPartition.terminal_ledger_three_way_partition (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let a countable statement ledger take values in a finite partially ordered grade space, and assume every post-enrollment grade track has finitely many revisions. The pointwise ledger-limit theorem therefore supplies a unique terminal grading.

Let Sem be the terminal semantic domain and W a wall contained in Sem. Every gatekeeper remains positive, joint positivity of a wall statement and all gatekeepers is forbidden, and consistency rules out forbidden wall configurations.

The migrated set M consists exactly of semantic statements with a positive terminal grade. The resident set R is Sem with M and W removed. The imported terminal-grade decomposition theorem gives the displayed cover equality and all three pairwise disjointness claims directly.

References

• Truth anchor: D5/S0/Computability/LedgerGovernance/TerminalLedgerPartition.terminal_ledger_three_way_partition
• Dependency: D5/S0/Computability/TerminalGradeDecomposition