Glyphic Residuum: Exact Structural Factorization and Self-Certifying DAG Compression for Formal Proofs, Reasoning Traces, and Symbolic State Trajectories

Background & Problem: Machine-checked formal verification corpora, autonomous AI reasoning trees, and symbolic state trajectories exhibit massive structural redundancy across documents, yet resist conventional byte-stream compression. Because sealed proof artifacts (such as Lean 4 kernel receipts and content-addressed intermediate representations) bind every syntax node and document envelope with 64-character SHA-256 digests, standard statistical and dictionary compressors (gzip, zstd, LZMA2) treat deterministic cryptographic hashes as incompressible high-entropy literals—achieving only 3.6× to 14.0× compression while duplicating identical reasoning subgraphs across files. Method (Structural Factorization and the Residuum Law): This paper presents Glyphic Residuum, a partial, injective, and self-certifying domain codec that achieves two-orders-of-magnitude compression by factoring admitted corpora into four persistence classes (G0–G3). Rather than compressing serialized text, the encoder strips all decoder-owned grammar (G0) and deterministically regenerable SHA-256 node/seal digests (G1), collapses cross-file subgraph isomorphism into a single content-addressed bulk DAG, and persists only the irreducible structural remainder (G2, the residuum ρ). To break the circular dependency between graph adjacency and node ordering without storing explicit pointer tables, we introduce a self-certifying incremental Kahn replay governed by a gated topological priority functional. Weighting each internal constructor by its RED-child count establishes a strict priority gap between internal constructors and zero-arity leaves—guaranteeing by our Leaf-Suffix Theorem that all leaf nodes flush as a contiguous topological suffix whose 1-byte wire span never overflows whenever unique leaves satisfy B ≤ 256. Results & Verification: On the frozen 24-file Lean 4 reference corpus (2,598,463 bytes), the codec produces a 13,303-byte standalone archive (195.3×) and a 13,157-byte wrapped container (197.5×)—a 54.5× improvement over gzip -9 (716,622 B) and a 14.1× improvement over XZ/LZMA9e (185,600 B)—while guaranteeing 100% source-free, byte-for-byte reconstruction of every filename, JSON body, and cryptographic seal across bit-identical Python and Rust implementations. On incremental workloads, our marginal novelty engine demonstrates that appending a 53,193-byte proof sharing 74.2% of its structure with an existing archive requires only +253 marginal archive bytes (210.2×). Extending the same structural factorization above the core wire format to multi-frame procedural animations and UI session trajectories yields 303.8× to 427.0× compression (12,747 B to 16,622 B for 75–90 frames) with sub-millisecond warm seeks under a strict 1 MiB retained-content memory ceiling. Correctness is backed by 27 mechanized Lean 4 theorems, TLA+ safety models, and an adversarial test gauntlet spanning 211,680 exhaustive single-bit flips and 128 checksum-repaired wire mutations with zero partial outputs. Scope & Theoretical Boundaries: Nothing in this construction violates Shannon information theory or the pigeonhole counting bound: high ratios are achieved strictly by restricting the domain D and eliminating representational and cross-document redundancy. We conclude with rigorous boundary audits and falsification controls, proving why trajectory indirection obeys an index-amortization law, why bounded-width resolution saturates on K4 Tseitin parity counterexamples without collapsing NP, and why already entropy-coded media bitstreams (H.264/MP4 at H0 = 8.0000 bits/byte) cannot be structurally factored without access to their pre-rendered symbolic scene state.