10 Compression relative to a task family
On this page · Permalink · Source line 1253
A representation is sufficient only relative to specified questions and a specified class of possible archives. Fix a set \(\mathscr A\) of admissible proof archives. A representation scheme is a map \(C:\mathscr A\to\mathscr R\). Its output for an archive \({\mathcal P}\) is \(C({\mathcal P})\). Distinguishing the scheme from one output is essential: a decoder chosen only after seeing one fixed archive could simply store the answer.
Definition 10.1: Task
A task is a map \(q:\mathscr A\to Y_q\) to a declared answer set. A task family \({\mathcal Q}\) is a set of such maps. Examples include asking for the target certificate, a dependency list, a specified boundary example, or the claims affected by a recorded revision. A teaching or discovery objective becomes an exact task only after its required output or acceptance criterion has been specified.
Definition 10.2: Task-sufficient representation
The scheme \(C:\mathscr A\to\mathscr R\) is sufficient for \(q\) when there is a single decoder \(d_q:C(\mathscr A)\to Y_q\) such that
It is \({\mathcal Q}\)-sufficient when this holds for every \(q\in{\mathcal Q}\). The decoder may depend on the task and the scheme, but not on hidden knowledge of the particular archive being decoded.
The decoder is defined on attained representations, so no arbitrary answer is required for an encoding that never occurs. Exact reconstruction is one possible task, not a requirement for every purpose. The basic definition is set theoretic and does not assert that a decoder is computable, efficient, or available to a particular reader. Those are additional conditions on a practical compiler.
Theorem 10.3: Task information loss criterion
Let \(C\) be a compression map and let \(q\) be a task. If there exist proof fields \({\mathcal P}_1\) and \({\mathcal P}_2\) such that
then the compressed representation is not sufficient for \(q\).
Proof
Suppose a decoder \(d_q\) existed. Applying it to the common compressed representation would have to produce both \(q({\mathcal P}_1)\) and \(q({\mathcal P}_2)\). Since these answers differ, no such decoder exists.
Definition 10.4: Recoverability preorder
For a fixed task family \({\mathcal Q}\), write
when every task in \({\mathcal Q}\) that factors through the representation scheme \(R_1\) also factors through \(R_2\). Both schemes have domain \(\mathscr A\), and each factorization uses one decoder valid on that whole domain.
Proposition 10.5: Recoverability is a preorder
The relation \(\preceq_{{\mathcal Q}}\) is reflexive and transitive.
Proof
Every representation supports every task it supports, so the relation is reflexive. If every task supported by \(R_1\) is supported by \(R_2\), and every task supported by \(R_2\) is supported by \(R_3\), then every task supported by \(R_1\) is supported by \(R_3\). Thus the relation is transitive.
Define \(R_1\sim_{{\mathcal Q}}R_2\) when both \(R_1\preceq_{{\mathcal Q}}R_2\) and \(R_2\preceq_{{\mathcal Q}}R_1\).
Corollary 10.6: Quotient poset
The recoverability preorder descends to a partial order on the equivalence classes under \(\sim_{{\mathcal Q}}\).
Proof
Reflexivity and transitivity pass to equivalence classes. Mutual recoverability has been quotiented out, so antisymmetry holds by construction.
10.1 Pure retention operators
On this page · Permalink · Source line 1319
The simplest compression removes nodes without rewriting the retained material. This baseline is useful because it separates information deletion from more complicated summarization or reinterpretation.
Definition 10.7: Retention projection
Fix a finite node universe \(V\). For a mask \(K\subseteq V\), define
Theorem 10.8: Retention projection algebra
For masks \(K,L\subseteq V\),
Consequently every retention projection is idempotent, and the masks form a Boolean lattice with meet \(K\cap L\) and join \(K\cup L\).
Proof
For every \(S\subseteq V\),
Intersection is associative and commutative, which gives the composition identity and commutativity. Taking \(L=K\) gives idempotence. The power set of \(V\) with intersection, union, complement, bottom \(\varnothing\), and top \(V\) is a Boolean lattice.
Corollary 10.9: Task monotonicity under retention
If \(K\subseteq L\), every task whose required nodes and metadata are retained by \(P_K\) is also supported by \(P_L\).
Proof
Every item retained by \(K\) is retained by \(L\). Hence every task requirement contained in \(K\) is contained in \(L\).
Pure retention operators commute. Noncommutativity in real proof workflows therefore requires an additional operation such as state-dependent summarization, renaming, quotienting, or reinterpretation. This distinction prevents simple deletion from being credited with structure it does not possess.
Theorem 10.10: Task-family dependence of minimal compression
There is a family of archives with a fixed mandatory certificate and two independently variable side records for which different task families have different least sufficient retention masks.
Proof
Let the archives be \({\mathcal P}_{xy}=(C_0,x,y)\) for \((x,y)\in\{0,1\}^2\), where \(C_0\) is a fixed certificate retained by every allowed mask. Let \(q_x({\mathcal P}_{xy})=x\) and \(q_y({\mathcal P}_{xy})=y\). Retaining \(x\) is sufficient for \(q_x\). Any mask omitting \(x\) identifies \({\mathcal P}_{0y}\) with \({\mathcal P}_{1y}\), so it is not sufficient for that task. Thus the least mask for \(\{q_x\}\) retains exactly \(C_0\) and \(x\). The same argument gives the least mask \(C_0\) and \(y\) for \(\{q_y\}\). Their joint task family requires both records. These masks are also the unique minima for unit cost per retained side record.
The example concerns pure retention. A general encoding may recode the records rather than delete them. Sufficiency for all archive queries requires an injective encoding, not literal preservation of the original file. The following theorem makes that distinction precise.
Theorem 10.11: All predicates distinguish exactly injective encodings
Let \(C:A\to B\). Every predicate \(q:A\to\mathrm{Prop}\) factors through \(C\) if and only if \(C\) is injective.
Proof
If \(C\) is injective, define the decoder of \(q\) at \(b\) by the predicate \(\exists a\ (C(a)=b\ \text{and}\ q(a))\). At \(b=C(a_0)\), injectivity makes this equivalent to \(q(a_0)\). Conversely, if \(C(a)=C(a')\), use the predicate \(q(z)\equiv(z=a)\). Its decoded values at the equal encodings must agree, giving \(a'=a\). This is the general collision criterion specialized to all predicates.
The formal result ProofPath.all_predicates_sufficient_iff_injective records the distinction between information loss and lossless recoding. It makes no assertion about how cheaply a decoder can be computed.
10.2 A complete factorization test on attained representations
On this page · Permalink · Source line 1390
The collision obstruction of Theorem 10.3 has a converse. It gives a complete test for exact task recovery at the level of sets. Write \(\operatorname{im}C=C(\mathscr A)\) for the attained output set. A decoder is required on this set and nowhere else.
Theorem 10.12: Attained factorization and unique decoding
For \(C:\mathscr A\to\mathcal R\) and \(q:\mathscr A\to Y\), the following are equivalent:
When a decoder exists it is unique on \(\operatorname{im}C\). Otherwise there are two archives with the same encoding and different task answers.
Proof
A decoder applied to equal encodings gives equal answers. Conversely, for an attained value \(r\), choose \(a\) with \(C(a)=r\) and define \(d(r)=q(a)\). Constancy on each fiber makes the value independent of the choice. At \(r=C(a)\) it gives the required answer. Any other decoder must give that same answer at every attained value, proving uniqueness. Negating fiber constancy supplies the pair in the last statement. The construction is set theoretic and uses classical choice in the Lean implementation. It does not provide an efficient decoder for arbitrary infinite archive classes.
Example 10.13: The empty-domain boundary
Take \(\mathscr A=\varnothing\), \(\mathcal R=\{*\}\), and \(Y=\varnothing\). There is one encoding and one task on the empty archive class. The attained set is empty, so its empty decoder exists. There is no total decoder \(\{*\}\to\varnothing\). Thus attained decoding and decoding on the entire output type are not equivalent without an additional hypothesis.
The earlier formal definition ProofPath.Sufficient asks for a total decoder. It is retained for compatibility and was not false, but it was stronger than the manuscript's stated domain convention. The new namespace ProofPath.Recovery matches the manuscript exactly. It proves that total decoding implies attained decoding, and that the two are equivalent whenever the answer type is nonempty. In the latter case choose one default answer for unattained outputs. The empty-domain example is also kernel checked.
The finite Python interface factor_task takes an explicitly declared table of archive encodings and a task table on the identical domain. It returns either a decoder table or two archive identifiers witnessing a collision. Its verifier checks the proposed result directly, including the empty domain, missing outputs, extra unattained entries, and contradictory records. The table strings are exact identifiers and answers, not a semantic equality procedure for arbitrary mathematical expressions. The existing retention-based task_sufficient function remains a different, narrower task model.
10.3 The least information for a family of tasks
On this page · Permalink · Source line 1420
Suppose tasks \(q_i:\mathscr A\to Y_i\) are indexed by \(i\in I\). Their joint representation is
It records every distinction asked for by the task family and makes no demand to recover the entire source archive.
Theorem 10.14: Joint task representation and compositional recovery
An encoding \(C\) is sufficient for every \(q_i\) if and only if it is sufficient for \(Q\). In particular every sufficient encoding recovers the joint representation on attained values, while \(Q\) itself recovers each task by projection.
If a representation \(R\) is recoverable from \(C\), then every task recoverable from \(R\) is recoverable from \(C\). Recovery of representations is reflexive and transitive.
Proof
If \(Q\) factors through \(C\), each coordinate factors by projection. Conversely, equal values of \(C\) give equal values of every \(q_i\). Function extensionality gives equal joint vectors, and Theorem 10.12 supplies the joint decoder. This argument allows a different answer type for each task and also covers an empty task family.
For the second assertion, write \(R=\pi\circ C\) and \(q=d\circ R\) on their attained sets. Then \(q=(d\circ\pi)\circ C\). The identity decoder proves reflexivity, and composition of two recovery maps proves transitivity. All maps are applied only to outputs in their declared domains.
The word least concerns retained distinctions, not bytes, running time, or the cognitive cost of reading an archive. Two archives are identified by \(Q\) precisely when every declared task gives the same answer on them. Any sufficient representation may retain more, but it cannot identify archives that \(Q\) distinguishes. For a finite archive family, the reference implementation labels these joint-answer classes and checks that every task is constant within a class. Costs remain a separate optimization problem.
This result also completes the formal justification of the recovery condition in Section 23. A refinement that reconstructs only the final theorem need not preserve the joint tasks of audit and discovery. A refinement with a checked recovery map for the preceding representation does preserve them. The distinction is between a longer proof and a genuinely more informative archive, not between short and long documents in general.