zheng: polynomial proof system

one IOP: SuperSpartan + sumcheck (CCS constraints, O(N) prover, O(log N) verifier). one folding: HyperNova (CCS-native, ~30 field ops per fold, one decider at the end). one hash: hemera (~3 calls per proof — binding, Fiat-Shamir seed, domain separation). five lenses: one trait, five algebras — each algebra sees through its own optic. five operations: commit, open, verify, fold, decide.

spec pages

lens — polynomial commitment (separate repo: ~/git/lens/)

sumcheck — the engine: O(N) prover reduces exponential sum to one evaluation

superspartan — CCS IOP via sumcheck: any-degree constraints, one Lens opening

recursion — HyperNova folding + proof-carrying computation + cross-algebra

accumulator — universal accumulator: fold all 5 structural sync layers

decider — decide(acc) → proof: ~825 constraints, O(1) cost regardless of N

tensor — tensor compression for O(√N) prover memory

verifier — standalone verification algorithm: sumcheck + Brakedown opening

constraints — CCS format, pattern table, state operations

transcript — Fiat-Shamir via hemera (~3 calls)

api — commit/open/verify/fold/decide entry points

architecture

zheng
├── IOP layer (field-generic, shared across all algebras)
│   ├── SuperSpartan          CCS constraint system
│   ├── sumcheck              exponential sum reduction
│   └── HyperNova             folding + composition
│
├── lens layer (external: ~/git/lens/)
│   ├── Brakedown lens        (nebu, F_p)       expander-graph codes, Merkle-free
│   ├── Binius lens           (kuro, F₂)        binary Reed-Solomon
│   ├── Ikat lens       (jali, R_q)       NTT batch, automorphisms, noise tracking
│   ├── Isogeny lens          (genies, F_q)     Brakedown over isogeny field
│   └── Tropical lens         (trop, min+)      witness-verify, delegates to Brakedown
│
├── hash layer
│   └── hemera                ~3 calls total
│                             Fiat-Shamir + binding hash
│
├── selector CCS (cross-algebra dispatch)
│   ├── sel_Fp                Goldilocks rows
│   ├── sel_F2                binary rows
│   ├── sel_ring              ring-structured rows
│   ├── sel_Fq                isogeny rows
│   └── sel_trop              tropical witness-verify rows
│
└── composition
    └── HyperNova folding     ~30 field ops + 1 hemera hash per fold
        └── decider           one SuperSpartan + sumcheck + Brakedown proof
                              covers ALL algebras, runs once in F_p

five lenses

specs live in lens repo (~/git/lens/).

five operations

cross-algebra composition

any nox program can mix algebras. each sub-trace proves via its native Lens. HyperNova folds all into one F_p accumulator. one decider, one proof, regardless of how many algebras participated.

boundary cost: ~766 F_p constraints per algebra crossing. at 5 algebras max: ~3,830 overhead for a fully heterogeneous computation. negligible vs execution cost.

for intuition, motivation, and learning paths see docs/explanation.