Copy-edit: Multi-level editorial pass (tactical/operational/strategic)

Pass 1 (Tactical - Sentence-level):
- Strengthened verb constructions throughout
- Improved issue-point positioning per Gopen principles
- Enhanced topic-stress relationships for clearer flow
- Reduced redundant phrasing (e.g., 'either...or' instead of 'discrete or continuous')

Pass 2 (Operational - Paragraph/section):
- Tightened transitions between paragraphs
- Reduced redundancy in section transitions
- Improved coherence within major subsections
- Streamlined topic strings across paragraph boundaries

Pass 3 (Strategic - Document-level):
- Verified Heilmeier question alignment in each section
- Strengthened section-to-section linkages
- Ensured consistent logical flow throughout proposal
- Clarified 'who cares, why now, what difference' narrative

Focus: clarity and impact over nitpicking. Changes preserve technical accuracy while improving readability.

1-goals-and-outcomes/research_statement_v1.tex

@@ -1,15 +1,15 @@
 % GOAL PARAGRAPH
-This research develops autonomous control systems with mathematical guarantees of safe and correct behavior.
+This research develops autonomous control systems that provide mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
 Nuclear reactors today require human operators to follow detailed written procedures and switch between control objectives as plant conditions change.
 % Gap
-Small modular reactors face a fundamental economic challenge: their staffing costs per megawatt far exceed those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of human operators.
+Small modular reactors face a fundamental economic challenge: staffing costs per megawatt far exceed those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if safety assurance equals or exceeds that of human operators.
 
 % APPROACH PARAGRAPH Solution
-This research unifies formal methods from computer science with control theory to produce hybrid control systems that are correct by construction.
+This research unifies formal methods from computer science with control theory to produce hybrid control systems correct by construction.
 % Rationale
-Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic but cannot verify continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete logic correctness. End-to-end correctness requires both.
+Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic but cannot verify continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete logic correctness. Both are required for end-to-end correctness.
 % Hypothesis and Technical Approach
 Three stages bridge this gap. First, NASA's Formal Requirements Elicitation Tool (FRET) translates written operating procedures into temporal logic specifications, structuring requirements by scope, condition, component, timing, and response. Realizability checking then exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata that are provably correct by construction. Third, reachability analysis verifies that continuous controllers—designed by engineers using standard control theory—satisfy each discrete mode's requirements.
 

1-goals-and-outcomes/v1.tex

@@ -1,7 +1,7 @@
 \section{Goals and Outcomes}
 
 % GOAL PARAGRAPH
-This research develops autonomous hybrid control systems with mathematical guarantees of safe and correct behavior.
+This research develops autonomous hybrid control systems that provide mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
 Nuclear power plants require the highest levels of control system reliability. Control system failures risk economic losses, service interruptions, or radiological release.
@@ -13,7 +13,7 @@ This reliance on human operators prevents autonomous control and creates a funda
 % APPROACH PARAGRAPH Solution
 This research unifies formal methods with control theory to produce hybrid control systems correct by construction.
 % Rationale
-Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic from written requirements but cannot verify the continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Both are required for end-to-end correctness.
+Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic from written requirements but cannot verify continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Both are required for end-to-end correctness.
 % Hypothesis
 Two steps close this gap. First, reactive synthesis generates discrete mode transitions directly from written operating procedures. Second, reachability analysis verifies continuous behavior against discrete requirements. This transforms operating procedures into logical specifications that constrain continuous dynamics, producing autonomous controllers that are provably free from design defects. 
 
@@ -62,7 +62,7 @@ If successful, this approach produces three concrete outcomes:
 \end{enumerate}
 
 % IMPACT PARAGRAPH Innovation
-\textbf{What makes this research new?} No existing methodology achieves end-to-end correctness guarantees for hybrid systems. Section 2 will show that prior work verified discrete logic or continuous dynamics—never both compositionally. This work unifies discrete synthesis with continuous verification through a key innovation: discrete specifications become contracts that continuous controllers must satisfy. Each layer verifies independently while guaranteeing correct composition. Formal methods verify discrete logic. Control theory verifies continuous dynamics. Together, these three outcomes—procedure translation, continuous verification, and hardware demonstration—establish a complete methodology spanning from regulatory documents to deployed systems.
+\textbf{What makes this research new?} No existing methodology achieves end-to-end correctness guarantees for hybrid systems. Section 2 shows that prior work verified discrete logic or continuous dynamics—never both compositionally. This work unifies discrete synthesis with continuous verification through a key innovation: discrete specifications become contracts that continuous controllers must satisfy. Each layer verifies independently while guaranteeing correct composition. Formal methods verify discrete logic. Control theory verifies continuous dynamics. Together, these three outcomes—procedure translation, continuous verification, and hardware demonstration—establish a complete methodology spanning from regulatory documents to deployed systems.
 
 % Outcome Impact
 If successful, control engineers will create autonomous controllers from existing procedures with mathematical proofs of correct behavior. This makes high-assurance autonomous control practical for safety-critical applications—a capability essential for the economic viability of next-generation nuclear power. Small modular reactors offer a promising solution to growing energy demands. Their success depends on reducing per-megawatt operating costs through increased autonomy. This research provides the tools to achieve that autonomy while maintaining the exceptional safety record the nuclear industry requires. 

2-state-of-the-art/v2.tex

@@ -2,7 +2,7 @@
 
 \textbf{Heilmeier Questions: What has been done? What are the limits of current practice?} 
 
-No current approach provides end-to-end correctness guarantees for autonomous control. Human-centered operation cannot eliminate reliability limits. Formal methods verify discrete or continuous behavior—never both. 
+No current approach provides end-to-end correctness guarantees for autonomous control. Human-centered operation cannot eliminate reliability limits. Formal methods verify either discrete or continuous behavior—never both. 
 
 Three subsections structure this analysis: reactor operators and their operating procedures, fundamental limitations of human-based operation, and formal methods approaches that verify discrete logic or continuous dynamics but not both together.
 
@@ -14,7 +14,7 @@ Current practice rests on two critical components: procedures and operators. Pro
 
 Nuclear plant procedures form a strict hierarchy. Normal operating procedures govern routine operations. Abnormal operating procedures handle off-normal conditions. Emergency Operating Procedures (EOPs) manage design-basis accidents. Severe Accident Management Guidelines (SAMGs) address beyond-design-basis events, while Extensive Damage Mitigation Guidelines (EDMGs) cover catastrophic damage. All procedures must comply with 10 CFR 50.34(b)(6)(ii); NUREG-0899 provides development guidance~\cite{NUREG-0899, 10CFR50.34}. 
 
-Procedure development rests on expert judgment and simulator validation—not formal verification. Regulations mandate rigorous assessment: 10 CFR 55.59~\cite{10CFR55.59} requires technical evaluation, simulator validation testing, and biennial review. Yet key safety properties escape formal verification. No mathematical proof confirms that procedures cover all possible plant states, that required actions complete within available timeframes, or that transitions between procedure sets maintain safety invariants.
+Procedure development rests on expert judgment and simulator validation—not formal verification. Regulations mandate rigorous assessment: 10 CFR 55.59~\cite{10CFR55.59} requires technical evaluation, simulator validation testing, and biennial review. Yet key safety properties escape formal verification. No mathematical proof confirms that procedures cover all possible plant states, that required actions complete within available time, or that transitions between procedure sets maintain safety invariants.
 
 \textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness
 and completeness.} No proof exists that procedures cover all
@@ -30,9 +30,9 @@ Safety systems already employ extensive automation. Reactor Protection Systems t
 
 \subsection{Human Factors in Nuclear Accidents}
 
-Procedures lack formal verification despite rigorous development, but this represents only half the reliability challenge. Even perfect procedures cannot guarantee safe operation when humans execute them imperfectly.
+Procedures lack formal verification despite rigorous development, but this represents only half the reliability challenge. Even perfect procedures cannot guarantee safe operation when executed imperfectly.
 
-Human operators—the second pillar of current practice—introduce reliability limitations independent of procedure quality. While procedures define what to do, operators determine when and how to act. This discretion introduces persistent failure modes that training alone cannot eliminate.
+Human operators—the second pillar of current practice—introduce reliability limitations independent of procedure quality. Procedures define what to do; operators determine when and how to act. This discretion introduces persistent failure modes that training cannot eliminate.
 
 Current-generation nuclear power plants employ over 3,600 active NRC-licensed
 reactor operators in the United States~\cite{operator_statistics}. These
@@ -62,9 +62,9 @@ limitations are fundamental to human-driven control, not remediable defects.
 
 \subsection{Formal Methods}
 
-The previous subsections established two fundamental limitations. First, procedures lack formal verification. Second, human operators introduce persistent reliability issues that training cannot eliminate. Both represent fundamental constraints—not remediable defects.
+The previous subsections established two fundamental limitations: procedures lack formal verification, and human operators introduce persistent reliability issues that training cannot eliminate. Both represent fundamental constraints—not remediable defects.
 
-Formal methods could eliminate both limitations by providing mathematical guarantees of correctness. Yet even the most advanced formal methods applications in nuclear control leave a critical verification gap.
+Formal methods could eliminate these limitations by providing mathematical guarantees of correctness. Yet even the most advanced formal methods applications in nuclear control leave a critical verification gap.
 
 This subsection examines two approaches illustrating this gap. HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic handles hybrid verification only post-hoc. Each demonstrates the current state of formal methods while revealing the verification gap this research addresses.
 
@@ -163,6 +163,8 @@ This section addressed two Heilmeier questions: What has been done? What are the
 
 \textbf{What are the limits of current practice?} A clear verification gap emerges: no existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into design. Current approaches verify discrete logic or continuous dynamics—never both compositionally. Training improvements cannot overcome human reliability limits. Post-hoc verification cannot scale to system design.
 
-\textbf{Why now?} Two forces create urgency. Economic necessity: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Technical maturity: formal methods tools have matured sufficiently to enable compositional hybrid verification. These forces converge to make this work both necessary and achievable.
+\textbf{Why now?} Two forces create urgency: economic necessity and technical maturity. Small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants, while formal methods tools have matured sufficiently to enable compositional hybrid verification. These forces converge to make this work both necessary and achievable.
 
-This section established what has been done and the limits of current practice. The verification gap is clear: no existing methodology synthesizes provably correct hybrid controllers from operational procedures. The timing is right: economic pressures demand autonomous control while technical maturity enables it. Section 3 addresses the next two Heilmeier questions—what is new and why it will succeed—presenting the technical approach that closes this gap.
+This section established what has been done and the limits of current practice. The verification gap is clear: no existing methodology synthesizes provably correct hybrid controllers from operational procedures. The timing is right: economic pressures demand autonomous control while technical maturity enables it. 
+
+Section 3 addresses the next two Heilmeier questions—what is new and why it will succeed—presenting the technical approach that closes this gap.

3-research-approach/v3.tex

@@ -23,7 +23,7 @@ This section presents the complete technical approach for synthesizing provably
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches verified discrete switching logic or continuous control behavior—never both simultaneously. Engineers validate continuous controllers through extensive simulation trials. They test discrete switching logic through simulated control room testing and human factors research. Neither method provides rigorous guarantees. Both consume enormous resources.
+Previous approaches verified either discrete switching logic or continuous control behavior—never both simultaneously. Engineers validate continuous controllers through extensive simulation trials. They test discrete switching logic through simulated control room testing and human factors research. Neither method provides rigorous guarantees, and both consume enormous resources.
 
 This approach bridges that gap by composing formal methods from computer science with control-theoretic verification, formalizing reactor operations as hybrid automata.
 
@@ -58,7 +58,7 @@ where:
 
 A HAHACS requires this tuple together with proof artifacts demonstrating that the control system's actual implementation satisfies its intended behavior.
 
-\textbf{What is new in this research?} Existing approaches verify discrete logic or continuous dynamics—never both compositionally. Section 2 established this limitation: reactive synthesis, reachability analysis, and barrier certificates exist independently. They have never been integrated into a systematic design methodology. Prior work cannot span from procedures to verified implementation.
+\textbf{What is new in this research?} Existing approaches verify either discrete logic or continuous dynamics—never both compositionally. Section 2 established this limitation: reactive synthesis, reachability analysis, and barrier certificates exist independently and have never been integrated into a systematic design methodology. Prior work cannot span from procedures to verified implementation.
 
 Three innovations enable compositional verification:
 
@@ -267,7 +267,7 @@ Reactive synthesis bridges this gap by automatically constructing controllers gu
 Reactive synthesis solves a fundamental problem: given an LTL formula $\varphi$ specifying desired system behavior, automatically construct a finite-state machine (strategy) that produces outputs in response to environment inputs such that all resulting execution traces satisfy $\varphi$. If such a strategy exists, the specification is \emph{realizable}. The synthesis algorithm either produces a correct-by-construction controller or reports that no such controller exists. Unrealizable specifications indicate conflicting or impossible requirements in
 the original procedures—this realizability check catches errors before implementation. 
 
-Reactive synthesis offers a decisive advantage: the discrete automaton requires no human engineering of its implementation and is correct by construction. This eliminates human error at the implementation stage entirely, allowing human designers to focus effort where it belongs—on specifying system behavior rather than implementing switching logic.
+Reactive synthesis offers a decisive advantage: the discrete automaton is correct by construction and requires no human engineering of its implementation. This eliminates human error at the implementation stage entirely, allowing designers to focus on specifying system behavior rather than implementing switching logic.
 
 This shift carries two critical implications. First, complete traceability: the controller changes between modes for reasons that trace back through specifications to requirements. This establishes clear liability and justification for system behavior. Second, deterministic guarantees replace probabilistic human judgment. Human operators cannot eliminate error from discrete control decisions. Humans are intrinsically fallible. Temporal logics define system behavior. Deterministic algorithms synthesize the controller. Strategic decisions follow operating procedures exactly—no exceptions, no deviations, no human factors.
 
@@ -392,9 +392,9 @@ appropriate to the fidelity of the reactor models available.
 
 \subsubsection{Stabilizing Modes}
 
-Transitory modes drive the system toward exit conditions. Reachability analysis verifies whether the target can be reached.
+Transitory modes drive the system toward exit conditions, and reachability analysis verifies whether the target can be reached.
 
-Stabilizing modes address a different question: will the system stay within bounds? Unlike transitory modes, which aim to reach a target, stabilizing modes maintain the system within a desired operating region indefinitely. Examples include steady-state power operation, hot standby, and load-following at constant power level. This different control objective requires a different verification approach.
+Stabilizing modes address a different question: will the system stay within bounds? Unlike transitory modes that aim to reach a target, stabilizing modes maintain the system within a desired operating region indefinitely. Examples include steady-state power operation, hot standby, and load-following at constant power level. This different control objective requires a different verification approach.
 
 Reachability analysis answers "can the system reach a target?" Stabilizing modes instead ask "does the system stay within bounds?" Barrier certificates provide the appropriate verification tool for this question.
 Barrier certificates analyze the dynamics of the system to determine whether

4-metrics-of-success/v1.tex

@@ -2,7 +2,7 @@
 
 \textbf{Heilmeier Question: How will success be measured?}
 
-Section 3 established the technical approach: compositional verification bridges discrete synthesis with continuous control and will succeed because it leverages existing procedural structure, bounds computational complexity, and validates against industrial hardware. This section addresses the next Heilmeier question: How will success be measured? 
+Section 3 established the technical approach: compositional verification bridges discrete synthesis with continuous control. It will succeed because it leverages existing procedural structure, bounds computational complexity, and validates against industrial hardware. This section addresses the next Heilmeier question: How will success be measured? 
 
 Success is measured by Technology Readiness Level advancement from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5), where system components operate successfully in a relevant laboratory environment. TRL advancement provides the most appropriate success metric because it explicitly measures the gap between academic proof-of-concept and practical deployment. This section explains why TRLs measure success appropriately, then defines specific criteria for each level from TRL 3 through TRL 5.
 

5-risks-and-contingencies/v1.tex

@@ -2,7 +2,7 @@
 
 \textbf{Heilmeier Question: What could prevent success?}
 
-Section 4 defined success as reaching TRL 5 through component validation, system integration, and hardware demonstration—a definition that assumes critical technical challenges can be overcome.
+Section 4 defined success as reaching TRL 5 through component validation, system integration, and hardware demonstration. This definition assumes critical technical challenges can be overcome.
 
 Every research plan rests on assumptions that might prove false. Three primary risks could prevent reaching TRL 5: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, and completeness of procedure formalization.
 

6-broader-impacts/v1.tex

@@ -6,7 +6,7 @@ Sections 2 through 5 established the complete technical research plan: what has
 
 This section addresses the remaining Heilmeier questions by connecting technical methodology to economic and societal impact: who cares, why now, and what difference this work will make.
 
-\textbf{Who cares?} Three stakeholder groups face the same economic constraint—high operating costs driven by staffing requirements. The nuclear industry faces uncompetitive per-megawatt costs for small modular reactors. Datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure. Clean energy advocates need nuclear power to be economically competitive with fossil alternatives. All three stakeholders require autonomous control with safety guarantees.
+\textbf{Who cares?} Three stakeholder groups face the same economic constraint: high operating costs driven by staffing requirements. The nuclear industry faces uncompetitive per-megawatt costs for small modular reactors. Datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure. Clean energy advocates need nuclear power to be economically competitive with fossil alternatives. All three require autonomous control with safety guarantees.
 
 \textbf{What difference will it make?} This research directly addresses a \$21--28 billion annual cost barrier, enabling economically viable small modular reactors for datacenter power and establishing a generalizable framework for safety-critical autonomous systems across critical infrastructure.