Copy-edit: multi-pass editorial review (tactical/operational/strategic)

- Tactical: Sentence-level improvements using Gopen principles
  - Improved issue-point structure (known→new info flow)
  - Strengthened verb choices (active voice, stronger verbs)
  - Enhanced topic-stress positioning (stress = end of sentence)
  - Simplified complex sentences for clarity

- Operational: Paragraph and section flow
  - Improved transitions between subsections
  - Strengthened coherence within sections
  - Removed redundant phrasing
  - Better connected related ideas

- Strategic: Document-level Heilmeier alignment
  - Sharpened section conclusions to answer Heilmeier questions explicitly
  - Improved transitions between major sections
  - Enhanced narrative flow through the complete argument
  - Strengthened connections: gaps→approach→metrics→risks→impact

Files edited:
- research_statement_v1.tex (intro version)
- 1-goals-and-outcomes/v1.tex
- 2-state-of-the-art/v2.tex
- 3-research-approach/v3.tex
- 4-metrics-of-success/v1.tex
- 5-risks-and-contingencies/v1.tex
- 6-broader-impacts/v1.tex

1-goals-and-outcomes/research_statement_v1.tex

@@ -2,14 +2,14 @@
 I develop autonomous control systems with mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
-Nuclear reactors today depend on human operators with extensive training. These operators follow detailed written procedures, switching between control objectives as plant conditions change.
+Nuclear reactors today depend on human operators with extensive training. These operators follow detailed written procedures and switch between control objectives as plant conditions change.
 % Gap
-Small modular reactors face a fundamental economic challenge: per-megawatt staffing costs significantly exceed those of conventional plants, threatening economic viability. Autonomous control systems could manage complex operational sequences without constant supervision—but only with assurance equal to or exceeding human-operated systems.
+Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening economic viability. Autonomous control systems could manage complex operational sequences without constant supervision—but only with safety assurance equal to or exceeding that of human-operated systems.
 
 % APPROACH PARAGRAPH Solution
-I produce hybrid control systems correct by construction, unifying formal methods from computer science with control theory. 
+I produce hybrid control systems correct by construction by unifying formal methods from computer science with control theory. 
 % Rationale
-Human operators already work this way: discrete logic switches between continuous control modes. Formal methods alone generate provably correct switching logic but cannot handle continuous dynamics governing transitions. Control theory alone verifies continuous behavior but cannot prove discrete switching correctness. End-to-end correctness requires both approaches working together.
+Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic but cannot handle the continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. End-to-end correctness requires both approaches working together.
 % 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. FRET structures requirements by scope, condition, component, timing, and response. Realizability checking then exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata provably correct by construction. Third, reachability analysis verifies that continuous controllers satisfy requirements imposed by each discrete mode. Engineers design these continuous controllers using standard control theory techniques.
 

1-goals-and-outcomes/v1.tex

@@ -6,9 +6,9 @@ I develop autonomous hybrid control systems with mathematical guarantees of safe
 % 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.
 % Known information
-Nuclear plants today depend on human operators with extensive training. These operators follow detailed written procedures and strict regulatory requirements, switching between control modes based on plant conditions and procedural guidance.
+Nuclear plants today depend on human operators with extensive training. These operators follow detailed written procedures and strict regulatory requirements. They switch between control modes based on plant conditions and procedural guidance.
 % Gap
-This reliance on human operators prevents autonomous control. It creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face per-megawatt staffing costs far exceeding those of conventional plants, threatening economic viability. Autonomous control systems could manage complex operational sequences without constant human supervision—but only with assurance equal to or exceeding that of human operators.
+This reliance on human operators prevents autonomous control and creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face per-megawatt staffing costs far exceeding those of conventional plants, threatening economic viability. Autonomous control systems could manage complex operational sequences without constant human supervision—but only with safety assurance equal to or exceeding that of human operators.
 
 % APPROACH PARAGRAPH Solution
 I produce hybrid control systems correct by construction, unifying formal methods with control theory.
@@ -64,7 +64,7 @@ If successful, this approach produces three concrete outcomes:
 % IMPACT PARAGRAPH Innovation
 These three outcomes—procedure translation, continuous verification, and hardware demonstration—establish a complete methodology from regulatory documents to deployed systems.
 
-\textbf{What makes this research new?} No existing methodology achieves end-to-end correctness guarantees for hybrid systems. This work unifies discrete synthesis with continuous verification. The 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. Section 2 examines why prior work fails at this integration. Section 3 details how this approach succeeds.
+\textbf{What makes this research new?} No existing methodology achieves end-to-end correctness guarantees for hybrid systems. 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. Section 2 examines why prior work fails at this integration. Section 3 details how this approach succeeds.
 
 % Outcome Impact
 If successful, control engineers create autonomous controllers from

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

@@ -2,15 +2,15 @@
 
 \textbf{Heilmeier Questions: What has been done? What are the limits of current practice?} 
 
-This section examines how nuclear reactors operate today. Current approaches—both human-centered and formal methods—cannot provide autonomous control with end-to-end correctness guarantees. 
+This section examines how nuclear reactors operate today. No current approach—whether human-centered or formal methods—provides autonomous control with end-to-end correctness guarantees. 
 
 Three subsections structure this analysis. First: reactor operators and their operating procedures. Second: fundamental limitations of human-based operation. Third: formal methods approaches that verify discrete logic or continuous dynamics but not both together. 
 
-These limits establish the verification gap that Section 3 addresses through compositional hybrid synthesis.
+These limits establish the verification gap that Section 3 addresses.
 
 \subsection{Current Reactor Procedures and Operation}
 
-Current practice has limits that constrain autonomous control. Understanding these limits requires examining how nuclear plants operate today. Three aspects structure this analysis: the hierarchy of procedures, the role of operators in executing them, and the operational modes that govern reactor control.
+Understanding the limits of current practice requires examining how nuclear plants operate today. Three aspects structure this analysis: the hierarchy of procedures, the role of operators in executing them, and the operational modes that govern reactor control.
 
 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. Extensive Damage Mitigation Guidelines (EDMGs) cover catastrophic damage. These procedures must comply with 10 CFR 50.34(b)(6)(ii); NUREG-0899 provides development guidance~\cite{NUREG-0899, 10CFR50.34}. 
 
@@ -86,7 +86,7 @@ implementations directly from Cryptol models---eliminating the traditional gap
 between specification and implementation where errors commonly arise.
 
 Despite its accomplishments, HARDENS has a fundamental limitation for hybrid control synthesis: the project addressed only discrete digital control logic. Continuous reactor dynamics remained unmodeled and unverified.
-The Reactor Trip System specification and verification covered discrete state transitions (trip/no-trip decisions), digital sensor input processing through discrete logic, and discrete actuation outputs (reactor trip commands). Continuous reactor physics remained unaddressed. Real reactor safety depends on the interaction between continuous processes—temperature, pressure, neutron flux—evolving in response to discrete control decisions. HARDENS verified the discrete controller in isolation. The closed-loop hybrid system behavior went unverified.
+The Reactor Trip System specification and verification covered discrete state transitions (trip/no-trip decisions), digital sensor input processing through discrete logic, and discrete actuation outputs (reactor trip commands). Continuous reactor physics remained unaddressed. Real reactor safety depends on interactions between continuous processes—temperature, pressure, neutron flux—evolving in response to discrete control decisions. HARDENS verified the discrete controller in isolation. The closed-loop hybrid system behavior remained unverified.
 
 \textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic without
 continuous dynamics or hybrid system verification.} Verifying discrete control
@@ -166,6 +166,6 @@ No existing approach addresses both discrete and continuous verification composi
 
 \textbf{What are the limits of current practice?} No existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into design. Current approaches verify either discrete logic or continuous dynamics—never both compositionally. This verification gap prevents autonomous nuclear control with end-to-end correctness guarantees. Training improvements cannot overcome human reliability limits. Post-hoc verification cannot scale to system design.
 
-Two imperatives converge. Economic necessity: small modular reactors cannot compete economically with per-megawatt staffing costs matching large conventional plants. Technical opportunity: formal methods tools have matured sufficiently to enable compositional hybrid verification. 
+Two imperatives converge. Economic necessity demands solutions: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Technical opportunity enables solutions: formal methods tools have matured sufficiently to enable compositional hybrid verification. 
 
-Section 3 closes this verification gap. It establishes what makes the approach new and why it will succeed.
+Section 3 closes this verification gap by establishing what makes the approach new and why it will succeed.

3-research-approach/v3.tex

@@ -25,7 +25,7 @@ This section presents the complete technical approach for synthesizing provably
 % ----------------------------------------------------------------------------
 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. Both consume enormous resources.
 
-I bridge that gap. My approach composes formal methods from computer science with control-theoretic verification. Reactor operations formalize as hybrid automata.
+My approach bridges that gap by composing formal methods from computer science with control-theoretic verification. I formalize reactor operations as hybrid automata.
 
 Hybrid system verification faces a fundamental challenge: discrete transitions change the governing vector field, creating discontinuities in system behavior through the interaction between discrete and continuous dynamics. Traditional verification techniques cannot handle this interaction directly.
 
@@ -279,7 +279,7 @@ Reactive synthesis has proven successful in robotics, avionics, and industrial c
 
 Recent applications include synthesizing robot motion planners from natural language specifications, generating flight control software for unmanned aerial vehicles, and creating verified controllers for automotive systems. These successes demonstrate that reactive synthesis scales beyond toy problems to real-world safety-critical applications.
 
-The discrete mode-switching logic now synthesizes from procedures. But what executes within each discrete mode? The next subsection addresses continuous control modes and their verification.
+Reactive synthesis produces discrete mode-switching logic from procedures. The next subsection addresses what executes within each discrete mode: continuous control and its verification.
 
 %%% NOTES (Section 3):
 % - Mention computational complexity of synthesis (doubly exponential worst case)
@@ -293,11 +293,9 @@ The discrete mode-switching logic now synthesizes from procedures. But what exec
 
 \subsection{Continuous Control Modes}
 
-The previous subsection established that reactive synthesis produces a provably correct discrete controller. This automaton determines when to switch between modes.
+Reactive synthesis produces a provably correct discrete controller that determines when to switch between modes. Hybrid control, however, requires more than correct mode switching. Continuous dynamics executing within each discrete mode must also verify against requirements. Without this continuous verification, the discrete controller cannot guarantee correct system behavior.
 
-Hybrid control requires more than correct mode switching. Continuous dynamics executing within each discrete mode must also verify against requirements. Without this continuous verification, the discrete controller cannot guarantee correct system behavior.
+This subsection describes continuous control modes and their verification. Control objectives determine the verification approach. Modes classify into three types—transitory, stabilizing, and expulsory—each requiring different verification tools matched to its distinct purpose. 
-
-This subsection describes continuous control modes executing within each discrete state. Control objectives determine the verification approach. Modes classify into three types—transitory, stabilizing, and expulsory. Each type requires different verification tools matched to its distinct purpose. 
 
 This methodology's scope requires clarification: this work verifies continuous controllers but does not synthesize them. The distinction parallels model checking in software verification. Model checking confirms whether a given implementation satisfies its specification without prescribing how to write the software. Engineers design continuous controllers using standard control theory techniques—this work assumes that design capability exists. The contribution lies in the verification framework that confirms candidate controllers compose correctly with the discrete layer to produce a safe hybrid system.
 
@@ -540,9 +538,9 @@ Section 2 established that prior work verified either discrete logic or continuo
 
 First, nuclear procedures already decompose operations into discrete phases with explicit transition criteria. The approach formalizes existing structure without imposing artificial abstractions. Second, mode-level verification bounds each verification problem locally. This avoids state explosion that makes global hybrid system analysis intractable. Third, the Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. Solutions address real deployment constraints.
 
-The methodology is complete. It encompasses procedure formalization, discrete synthesis, continuous verification across three mode types, and hardware implementation. 
+The complete methodology encompasses procedure formalization, discrete synthesis, continuous verification across three mode types, and hardware implementation. 
 
-Operational questions remain. Section 4 addresses \textit{How will success be measured?} Section 5 addresses \textit{What could prevent success?} Section 6 addresses \textit{Who cares? Why now? What difference will it make?}
+Three operational questions remain. Section 4 addresses \textit{How will success be measured?} Section 5 addresses \textit{What could prevent success?} Section 6 addresses \textit{Who cares? Why now? What difference will it make?}
 
 %%% NOTES (Section 5):
 % - Get specific details on ARCADE interface from Emerson collaboration

4-metrics-of-success/v1.tex

@@ -2,9 +2,9 @@
 
 \textbf{Heilmeier Question: How do we measure success?}
 
-Section 3 established the technical approach—what I will do and why it will work. This section addresses how I measure whether it actually succeeds. The answer: Technology Readiness Level advancement, progressing from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5).
+Section 3 established the technical approach—what I will do and why it will work. This section addresses how to measure success. The answer: Technology Readiness Level advancement from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5).
 
-My work begins at TRL 2--3 and aims to reach TRL 5, where system components operate successfully in a relevant laboratory environment. TRL advancement provides the most appropriate success metric. It explicitly measures the gap between academic proof-of-concept and practical deployment. This section explains why TRLs are the right metric, then defines specific criteria for each level from TRL 3 through TRL 5.
+My work begins at TRL 2--3 and aims to reach 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 are the right metric, then defines specific criteria for each level from TRL 3 through TRL 5.
 
 Technology Readiness Levels provide the ideal success metric. They explicitly measure the gap between academic proof-of-concept and practical deployment. This is precisely what my work bridges. 
 
@@ -83,12 +83,12 @@ controllers implementable with current technology.
 
 This section answered the Heilmeier question: How do we measure success?
 
-\textbf{Answer:} Technology Readiness Level advancement from 2--3 to 5. Success means demonstrating both theoretical correctness and practical feasibility through progressively integrated validation. 
+\textbf{Answer:} Technology Readiness Level advancement from 2--3 to 5 demonstrates both theoretical correctness and practical feasibility through progressively integrated validation. 
 
-TRL 3 proves component-level correctness. Each part works independently. TRL 4 demonstrates system-level integration in simulation. The parts compose correctly. TRL 5 validates hardware implementation in a relevant environment. The complete system works on real control hardware. 
+TRL 3 proves component-level correctness: each part works independently. TRL 4 demonstrates system-level integration in simulation: the parts compose correctly. TRL 5 validates hardware implementation in a relevant environment: the complete system works on real control hardware. 
 
-Achieving TRL 5 proves the methodology produces verified controllers implementable with current technology. This defines success.
+Achieving TRL 5 proves the methodology produces verified controllers implementable with current technology.
 
-Success depends on several critical assumptions. If these assumptions prove false, research could stall at lower readiness levels despite sound methodology. 
+Success, however, depends on several critical assumptions. If these assumptions prove false, research could stall at lower readiness levels despite sound methodology. 
 
-Section 5 addresses the complementary question: What could prevent success? It identifies primary risks, establishes early warning indicators, and defines contingency plans that preserve research value even when core assumptions fail.
+Section 5 addresses the complementary question: What could prevent success?

5-risks-and-contingencies/v1.tex

@@ -26,7 +26,7 @@ If computational tractability becomes the limiting factor, we reduce scope to a
 
 \subsection{Discrete-Continuous Interface Formalization}
 
-Computational tractability addresses whether synthesis can complete within practical time bounds—a practical constraint. The second risk proves more fundamental: whether boolean guard conditions in temporal logic can map cleanly to continuous state boundaries required for mode transitions. 
+Computational tractability addresses a practical constraint: whether synthesis can complete within reasonable time bounds. The second risk proves more fundamental: whether boolean guard conditions in temporal logic can map cleanly to continuous state boundaries required for mode transitions. 
 
 This interface represents the fundamental challenge of hybrid systems: relating discrete switching logic to continuous dynamics. Temporal logic operates on boolean predicates. Continuous control requires reasoning about differential equations and reachable sets. Guard conditions requiring complex nonlinear predicates may resist boolean abstraction. This would make synthesis intractable. Continuous safety regions that cannot be expressed as conjunctions of verifiable constraints would similarly create insurmountable verification challenges. 
 
@@ -138,8 +138,8 @@ Each risk has identifiable early warning indicators enabling detection before fa
 
 The staged project structure ensures partial success yields publishable results. It identifies remaining barriers to deployment. This design feature maintains contribution regardless of which technical obstacles prove insurmountable. Even "failure" advances the field by documenting precisely which barriers remain.
 
-The technical research plan is complete. Section 3 established what will be done and why it will succeed. Section 4 established how success will be measured. This section established what might prevent success and how to mitigate risks. 
+The technical research plan is complete. Section 3 established what will be done and why it will succeed. Section 4 established how to measure success. This section established what might prevent success and how to mitigate risks. 
 
 One critical Heilmeier question remains: Who cares? Why now? What difference will it make? 
 
-Section 6 connects technical methodology to urgent economic and infrastructure challenges facing the nuclear industry and broader energy sector.
+Section 6 connects this technical methodology to urgent economic and infrastructure challenges.

6-broader-impacts/v1.tex

@@ -14,7 +14,7 @@ This research directly addresses a \$21--28 billion annual cost barrier. It enab
 
 Why now? Exponentially growing AI infrastructure demands have transformed this longstanding challenge into an immediate crisis. The market demands solutions that did not exist before.
 
-Nuclear power presents both a compelling application domain and an urgent economic challenge. Recent interest in powering artificial intelligence infrastructure has renewed focus on small modular reactors (SMRs), particularly for hyperscale datacenters requiring hundreds of megawatts of continuous power. SMRs deployed at datacenter sites minimize transmission losses and eliminate emissions. Nuclear power economics at this scale, however, demand careful attention to operating costs.
+Nuclear power presents both a compelling application domain and an urgent economic challenge. Recent interest in powering artificial intelligence infrastructure has renewed focus on small modular reactors (SMRs), particularly for hyperscale datacenters requiring hundreds of megawatts of continuous power. SMRs deployed at datacenter sites minimize transmission losses and eliminate emissions. At this scale, however, nuclear power economics demand careful attention to operating costs.
 
 The U.S. Energy Information Administration's Annual Energy Outlook 2022 projects advanced nuclear power entering service in 2027 will cost \$88.24 per megawatt-hour~\cite{eia_lcoe_2022}. Datacenter electricity demand is projected to reach 1,050 terawatt-hours annually by 2030~\cite{eesi_datacenter_2024}. Nuclear power supplying this demand would generate total annual costs exceeding \$92 billion. Operations and maintenance represents a substantial component: the EIA estimates that fixed O\&M costs alone account for \$16.15 per megawatt-hour, with additional variable O\&M costs embedded in fuel and operating expenses~\cite{eia_lcoe_2022}. Combined, O\&M-related costs represent approximately 23--30\% of total levelized cost, translating to \$21--28 billion annually for projected datacenter demand.
 
@@ -72,4 +72,4 @@ This section answered three critical Heilmeier questions: Who cares? Why now? Wh
 
 The complete research plan spans technical approach, success metrics, risk mitigation, and broader impact. One final Heilmeier question remains: How long will it take? 
 
-Section 8 provides a structured 24-month research plan progressing through milestones tied to Technology Readiness Level advancement. This demonstrates the proposed work is achievable within a doctoral timeline.
+Section 8 provides a structured 24-month research plan progressing through milestones tied to Technology Readiness Level advancement, demonstrating the proposed work is achievable within a doctoral timeline.