Structured spectral quantization (Lean + ML dual track)

Parent: README

This note ties together:

1. Lean — algebraic “tower truncation” splits for commutative merges (Gnosis.FrfWitnessTowerTruncation).
2. Runtime ML — falsifiable experiments using subspace structure already present in the pneuma stack (PCA standing bases, low-rank FFN/KV sidecars, rknot spectral blocks).

It does not claim that triadic/XOR witnesses replace INT4/INT8 kernels on their own. Witnesses pin quotient-level bookkeeping; bandwidth and perplexity wins require structured approximation plus measured parity.

Formal layer (what is proved)

Import path: Gnosis.FrfWitnessTowerTruncation.

• triad_merge_take_drop_split: for any digit list ds and cut k, triadMerge ds = triadAdd (triadMerge (take k ds)) (triadMerge (drop k ds)).
• xor_merge_take_drop_split: same pattern for the GF(2) fold on bit lists.
• xor_parity_track_take_drop_split: the parity-bit shadow of base‑3 digits splits compatibly with take/drop.

Interpretation: a “short tower” can be paired with an explicit tail condensate (the merge of dropped digits) such that the full triadic residue recombine is exact at the digit-list layer. Collisions still exist globally (triad_merge_not_injective).

ML layer (what to measure)

Hypothesis. Retaining weights (or factors) restricted to calibrated standing subspaces, plus a standard low-bit tail correction (fp16/bf16/int block), yields better quality vs bytes than unstructured rounding at the same resident footprint — because structure is moved into subspace choice, not into residue miracles.

Existing tooling (do not reinvent blindly).

Minimal A/B protocol.

1. Baseline: uniform per-tensor INT8 (or current GGUF-style) at target VRAM.
2. Candidate: same footprint budget → rank‑k / subspace-truncated weights for chosen layers plus witness telemetry on calibration tensors (optional MetricsRecord-style gestalt folds on sidecar checksum streams — tooling only).
3. Gates: perplexity / downstream accuracy; triple-surface-parity-style cosine/KL bars; no regression on kernel dispatch assumptions.

Falsification. If candidate loses to baseline at matched VRAM without exotic kernels, the bottleneck is implementation reality (decode cost, matmul shape), not the formal witness layer.

Next exploration

Track these as explicit backlog items (dependency order: Lean telescope packaging informs how we phrase invariants next to ML gates; it does not substitute measurement).

Formal (Lean)

• Multi-cut telescope certificate. Compose several prefix cuts (nested take/drop partitions of the same digit list) so that triadMerge over the full word equals an n-fold recombination along the same homomorphism spine as triad_merge_append, using triad_merge_fold_append (and/or repeated triad_merge_take_drop_split) to emit one longer calc / bundled theorem — an (n)-way generalization of the single-cut split in Gnosis.FrfWitnessTowerTruncation.
• Optional mirror: align that bookkeeping with iterated frf_telescope_quotient_step / Nat-digit telescopes where the narrative calls for “many floors.”

Empirical (Rust / benches)

• Single-layer FFN-down-only A/B at matched parameter bytes. Baseline: INT8 (or current GGUF-class) representation sized to a fixed byte budget for one layer’s ffn_down. Candidate: .lrfd (or equivalent rank‑(k) factors from weight-truncate-fit) plus a narrow tail correction chosen so total resident bytes match the baseline (same comparison discipline as byte-parity / rknot verify flows — no apples-to-oranges footprint).
• Log wall-clock and perplexity (or fixed-calibration negative log-likelihood / CE on a pinned prompt set if full perplexity is too heavy) alongside existing parity-style metrics (weight-truncate-parity, cosine/KL bars). Prefer artifact paths and CLI flags that mirror parity-binary honesty: reproducible commands, checked-in or recorded stderr/stdout, no narrative-only claims.

When either item lands, update this section with theorem names / binary invocations and fold the result into the rknot or weight-truncate README tables if the outcome is stable enough to cite.