12. Declaration catalog: ExperimentalRobinMatrix
This chapter is generated from the Lean source. Every node denotes one explicit public declaration, and every Lean link is checked during the Blueprint build. Definitions appear in source order before later results whenever the source module does so.
Reader orientation: Compiled Robin-matrix research included in the full ASPBE gate; local results are separated from the broader paper route and external contracts. Each card separates an accessible reading cue from formal status, the source docstring, and the authoritative Lean panel. The standalone Library Explorer adds full-text search and filters across every chapter.
Research-module status. RobinMatrix.lean is compiled by the full ASPBE gate with zero proof holes. Its declarations include proved helper lemmas, explicit counterexamples, and typed external contracts. A compiled local declaration does not by itself certify the complete paper construction.