[chris-dare-dev]

Plan

• Keep I-02's no-topic-data pass branch; direct callers can still provide a literal zero-row emission.
• State precisely which zero-data shape the emission schema rejects before the CLI runs I-02.
• Keep the schema and pass/fail behavior unchanged.

Changes

• Clarify that constants: [] is rejected by CLI schema validation, while external-only rows can still leave I-02's filtered topic-name set empty.
• Update the I-02 finding field and pass reason to describe topic-scoped constants and in-scope declarations rather than the raw constants array.
• Narrow the CLI test name and docstring to the literal empty-array case.

Decisions

The parent repository is pinned to MFC bda0e613; it already contains the CLI validation test for constants: []. This source-level clarification does not warrant a pin bump, which would bring unrelated MFC commits. External-only rows remain schema-accepted; this PR does not change validation policy.

Verification

• python -m pytest -q contract/tests/test_ilean.py contract/tests/test_schemas.py — 73 passed, 1 skipped.
• git diff --check — passed.

Independent reviews

Mathematics, repository-boundary, abstraction, and Mathlib-style reviewers all passed commit c55240a5223b2f334b54b92f5d3032224ce2ff66.

Closes chris-dare-dev/derived-alg-geo-lean#189