Constructing Theorem-Level Questions: A Declaration Discipline for Bounded Inquiry

This paper develops a domain-independent methodology for constructing theorem-level questions under bounded inquiry. It argues that theorem-level statements can be expressed through six declared components: the object, admissible transformations, observable, equivalence relation, verdict class, and stopping condition. Together these form a declaration discipline that transforms an under-specified prompt into a mathematically well-typed question. The paper distinguishes four activities that are often conflated—asking, typing, computing, and interpreting—and organizes them into a pipeline in which each stage produces a well-defined artifact consumed by the next. Three reusable tools form the methodological core: a six-component question type, a proof-obligation checklist for auditing drafts, and a five-layer status discipline separating mathematics, derived consequence, interpretation, speculation, and open problems. A worked example from program equivalence demonstrates the methodology independently of the author’s broader research program. Beginning with the informal question “Is this the same program after refactoring?”, the paper progressively introduces the required declarations until the question becomes a decidable bisimulation computation. The same refactoring receives different verdicts under different declared observables, illustrating that disagreement can arise from undeclared regimes rather than inconsistent reasoning. The paper makes a bounded claim: not that every meaningful question should be formalized, but that theorem-level resolution requires sufficient declaration of its governing mathematical objects. The methodology is intended as a reusable engineering discipline for constructing, auditing, and interpreting formal questions across scientific and technical domains.