AIXC / docsProject documentation

Reference

Correctness Conditions

Look up syntax, contracts, layouts, algorithms, and exact behavior.

Lossless decoding depends on three independent equalities: the seed must reconstruct the initial context, the predictor must produce the same ordered candidates, and the residual stream must be consumed in the same positions. If any equality fails, a decoder can still parse the archive but cannot guarantee the original text.

∀i,  u^<i=u<i⇒pred⁡(u^<i)=pred⁡(u<i)\forall i,\; \hat{u}_{<i}=u_{<i} \Rightarrow \operatorname{pred}(\hat{u}_{<i})=\operatorname{pred}(u_{<i})
Decode invariant. If the decoded prefix equals the original prefix and the predictor is deterministic, the next prediction is reproducible.
ji=∑t<i(1−dt)j_i = \sum_{t < i}(1-d_t)
Residual consumption. The residual pointer before position i equals the number of misses before i.

By induction over positions, a hit reconstructs the original unit from the deterministic predictor, and a miss reconstructs it from the residual at pointer j. Feeding the reconstructed actual unit back into context preserves the induction hypothesis for the next position.