[kim-em]

Ordinary imports could not reveal the graph encoder's literal output, blocking proofs that numerical tower packets match their reconstructed source records. Add Codec.graph_eq, entry_eq and node_eq for the existing encoders, and document exactly what their field equations establish. The existing ordinary-import HexSignDet.PublicCodec consumer checks the requested graph-header equation, the entry fields and all eleven node fields, with six exact ordinary-kernel axiom guards.

This addresses the concrete public-encoding request in #10378 (reproducer). It supplies equations for stored data; acceptance, context binding, root validation and the remaining frame/exporter work retain their existing contracts. Encoder/decoder implementations and the format are unchanged. No package, phase or computational performance claim changes.

Validation: core codec build (300 jobs), ordinary-public-import consumer (327 jobs), current DAG, all 67 Mathlib-free benchmark boundaries and 406 build-only proof probes, admission checks across 1,475 import cones / 2,387 local modules, and whitespace checks pass. Full integrated build passes (14,777 jobs). The six new guards check the permitted standard-three axiom closure. No new timings.

Refs #10575. Opened as a draft because the mandatory fresh Opus review must still be obtained; an isolated review attempt follows immediately after opening.

[kim-em]

The mandatory fresh isolated Opus review was launched immediately after opening. It exited1 with “You've hit your weekly limit · resets 4pm (UTC)”; no review was obtained. This PR remains draft pending actual independent review and exact-head green CI. The targeted codec and ordinary-public-import consumer, all six exact standard-three axiom guards, DAG, Mathlib-free benchmark boundaries and admission checks pass. The full integrated build is still running.