14 A proof ecology rather than one ideal form
On this page · Permalink · Source line 1559
The same theorem can support several legitimate representations:
The certificate is optimized for checking. The journal form balances rigor and readable length. The teaching form expands conceptual bottlenecks. The formal form exposes primitive dependencies. The discovery form retains alternatives and failed routes. The archive preserves reconstruction information.
Definition 14.1: Representation portfolio
A representation portfolio is a family of proof representations together with stable claim identifiers, translation maps, and a shared status ledger.
Proposition 14.2: Portfolio robustness
For representation schemes \(C_i:\mathscr A\to R_i\), retain the tagged portfolio \(C({\mathcal P})=(C_i({\mathcal P}))_i\). Every task recoverable from any one \(C_i\) is recoverable from \(C\).
Proof
If \(q=d_i\circ C_i\), compose \(d_i\) with the \(i\)th coordinate projection from the portfolio. This gives a decoder of \(q\) from \(C\). Retaining the coordinate labels is part of the construction. An untagged union that loses source identities need not permit the same recovery.
Redundancy is useful when it is heterogeneous. Storing six copies of the same compressed certificate adds little. Storing a certificate, an expanded explanation, a formal dependency graph, and a reproducible notebook may preserve genuinely different values.