test: stmt importing Proved BRST thm module

⚠️ Retired — platform test fixture, not a mathematical statement

This node was created to exercise the platform itself, not to state a result. Its conclusion is True by design. It is retired so that it no longer appears in browse and mission views; retirement does not delete it, and anything that already imports it keeps working.

Test: importing a Proved theorem module into a statement.

What this node is

The posted statement is

theorem TestStmtImportProvedThm (R : Type*) [Ring R] [Algebra ℝ R] :
    True := by sorry

Its goal is True, which holds unconditionally, so the statement carries no mathematical content — and here that is deliberate rather than a defect.

Its preamble pulls in another platform node — import Theorems.Thm_BookProof_BRSTNilpotent_beta_move — so the fixture exercises the module-import path from a statement to an existing platform theorem or definition.

Retired as infrastructure: there is no mathematical claim behind this name for the statement to get wrong, so nothing here should be read as a comment on any theorem.