Frobenius Quantum Postprocessing Kernel

Abstract

Frobenius-observer fibers survive quantum encoding and deterministic observation.

Theorem 1.1 (Postprocessing preserves every Frobenius-observer fiber).

$$\begin{array}{c}\forall G:\mathrm{Type},Q:\mathrm{Type},O:\mathrm{Type},\\ [\mathrm{Monoid}\left(G\right)],U:Primes\to \mathrm{Prop},\\ Frob:\forall p:Primes,U\left(p\right)\to G,\\ eta:\mathrm{Option}\left(\mathrm{ConjClasses}\left(G\right)\right)\to Q,Sigma:Q\to O,\\ \ker \left(\mathrm{galoisPrimeObserver}\left(U,Frob\right)\right)\subseteq \ker \left(Sigma\circ eta\circ \mathrm{galoisPrimeObserver}\left(U,Frob\right)\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/FrobeniusQuantumPostprocessingKernel.frobenius_quantum_postprocessing_kernel (✓ std3). ∎

Source. Repository-derived.

Commentary.

The public source object is the canonical tagged Frobenius observer on rational primes. Its unramified predicate and Frobenius representatives remain explicit parameters.

An arbitrary encoding maps the complete tagged output to a quantum state, and an arbitrary deterministic observation maps that state to its final signature. Equality in the source kernel is preserved by both compositions.

The proof directly applies Mathlib’s factor-through composition law; no parallel observer or postprocessing primitive is introduced.

References

• Truth anchor: D5/S3/Factorization/Galois/FrobeniusQuantumPostprocessingKernel.frobenius_quantum_postprocessing_kernel
• Dependency: D5/S3/Factorization/Galois/GaloisPrimeObserver