DiagonalFockConstruction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The required faithful finite-diagonal Fock representation

This proves the precise structural representation input used in the projection-word estimates, from reduced centered words in the faithful tracial GNS Hilbert space.

theorem OAI.KadisonKastler.publishedDiagonalFockRepresentation line 18