Editorial pass: multi-level improvements

Tactical (sentence-level):
- Eliminated choppy sentences by combining related ideas
- Improved topic-stress positioning (key info at sentence ends)
- Strengthened verb choices and reduced passive constructions
- Enhanced parallel structure in lists and enumerations

Operational (paragraph/section):
- Strengthened transitions between subsections
- Improved coherence within paragraphs
- Enhanced flow between related ideas
- Clarified connections between sequential arguments

Strategic (document-level):
- Strengthened Heilmeier catechism alignment
- Improved connections between 'what is new' and 'why will it succeed'
- Enhanced integration of economic imperative with technical approach
- Clarified how staged structure preserves value under partial success

1-goals-and-outcomes/research_statement_v1.tex

@@ -2,14 +2,14 @@
 This research develops autonomous control systems with mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
-Extensively trained operators run nuclear reactors today. They follow detailed written procedures. They switch between control objectives based on plant conditions.
+Extensively trained operators run nuclear reactors today, following detailed written procedures and switching between control objectives based on plant conditions.
 % Gap
-Small modular reactors face a fundamental economic challenge: per-megawatt staffing costs significantly exceed those of conventional plants. This cost gap threatens economic viability. Autonomous control systems could manage complex operational sequences without constant supervision—but only if they provide assurance equal to or exceeding human-operated systems.
+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 if they provide assurance equal to or exceeding human-operated systems.
 
 % APPROACH PARAGRAPH Solution
 This research combines formal methods from computer science with control theory to produce hybrid control systems correct by construction. 
 % Rationale
-Operators already work this way. Discrete logic switches between continuous control modes. Existing formal methods generate provably correct switching logic—but they fail when continuous dynamics govern transitions. Control theory verifies continuous behavior—but it cannot prove discrete switching correctness. End-to-end correctness requires both approaches together.
+Operators already work this way: discrete logic switches between continuous control modes. Existing formal methods generate provably correct switching logic but fail when continuous dynamics govern transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. End-to-end correctness requires both approaches together.
 % Hypothesis and Technical Approach
 Three stages bridge this gap. First, written operating procedures translate into temporal logic specifications using NASA's Formal Requirements Elicitation Tool (FRET). FRET structures requirements into scope, condition, component, timing, and response. Conflicts and ambiguities emerge through realizability checking—before implementation begins. Second, reactive synthesis generates deterministic automata provably correct by construction. Third, standard control theory designs continuous controllers for each discrete mode. Reachability analysis then verifies each controller. Transition objectives classify continuous modes. Transitory modes drive the plant between conditions. Stabilizing modes maintain operation within regions. Expulsory modes ensure safety under failures. Assume-guarantee contracts and barrier certificates prove safe mode transitions. This enables local verification without global trajectory analysis. The methodology demonstrates on an Emerson Ovation control system. 
 % Pay-off

1-goals-and-outcomes/v1.tex

@@ -4,9 +4,9 @@
 This research develops autonomous hybrid control systems with 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.
+Nuclear power plants require the highest levels of control system reliability, as control system failures risk economic losses, service interruptions, or radiological release.
 % Known information
-Extensively trained human operators run nuclear plants today. They follow detailed written procedures and strict regulatory requirements. They switch between control modes based on plant conditions and procedural guidance.
+Extensively trained human operators run nuclear plants today, following detailed written procedures and strict regulatory requirements while switching 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. Per-megawatt staffing costs for small modular reactors far exceed those of conventional plants. This gap threatens economic viability. Autonomous control systems could manage complex operational sequences without constant human supervision—but only if they provide assurance equal to or exceeding human operators.
 
@@ -65,7 +65,7 @@ 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?} This work unifies discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems. Formal methods verify discrete logic; control theory verifies continuous dynamics. No existing methodology bridges both with compositional guarantees. The bridge emerges by treating discrete specifications as contracts that continuous controllers must satisfy, allowing each layer to verify independently while guaranteeing correct composition. Section 2 (State of the Art) examines why prior work has not achieved this integration. Section 3 (Research Approach) details how this integration will be accomplished.
+\textbf{What makes this research new?} This work unifies discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems—a bridge that emerges by treating discrete specifications as contracts that continuous controllers must satisfy, allowing each layer to verify independently while guaranteeing correct composition. Formal methods verify discrete logic; control theory verifies continuous dynamics; no existing methodology bridges both with compositional guarantees. Section 2 (State of the Art) examines why prior work has not achieved this integration, and Section 3 (Research Approach) details how this integration will be accomplished.
 
 % Outcome Impact
 If successful, control engineers create autonomous controllers from

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

@@ -1,14 +1,14 @@
 \section{State of the Art and Limits of Current Practice}
 
-\textbf{What has been done? What are the limits of current practice?} This section answers these Heilmeier questions by examining how nuclear reactors operate today and why current approaches—both human-centered and formal methods—cannot provide autonomous control with end-to-end correctness guarantees. Three subsections structure this analysis. First, we examine reactor operators and their operating procedures. Second, we investigate the fundamental limitations of human-based operation. Third, we review formal methods approaches that verify discrete logic or continuous dynamics but not both together. Understanding these limits establishes the verification gap that Section 3 addresses through compositional hybrid synthesis.
+\textbf{What has been done? What are the limits of current practice?} This section answers these Heilmeier questions by examining how nuclear reactors operate today and why current approaches—both human-centered and formal methods—cannot provide autonomous control with end-to-end correctness guarantees. Three subsections structure this analysis: first, reactor operators and their operating procedures; second, the fundamental limitations of human-based operation; third, formal methods approaches that verify discrete logic or continuous dynamics but not both together. Understanding these limits establishes the verification gap that Section 3 addresses through compositional hybrid synthesis.
 
 \subsection{Current Reactor Procedures and Operation}
 
-Current practice must be understood before its limits can be identified. This subsection examines the hierarchy of nuclear plant procedures, the role of operators in executing them, and the operational modes that govern reactor control.
+Understanding current practice precedes identifying its limits. This subsection examines three aspects of nuclear plant operation: the hierarchy of procedures, the role of operators in executing them, and the operational modes that govern reactor control.
 
-Nuclear plant procedures form a 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}. 
+Nuclear plant procedures form a 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, and 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}. 
 
-Procedure development relies on expert judgment and simulator validation—not formal verification. Technical evaluation, simulator validation testing, and biennial review under 10 CFR 55.59~\cite{10CFR55.59} assess procedures rigorously. Yet key safety properties escape formal verification. No mathematical proof confirms that procedures cover all possible plant states. No proof exists that required actions complete within available timeframes or that safety invariants hold across procedure-set transitions.
+Procedure development relies on expert judgment and simulator validation—not formal verification. While technical evaluation, simulator validation testing, and biennial review under 10 CFR 55.59~\cite{10CFR55.59} assess procedures rigorously, 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 safety invariants hold across procedure-set transitions.
 
 \textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness
 and completeness.} Current procedure development relies on expert judgment and
@@ -21,7 +21,7 @@ could provide.
 
 Nuclear plants operate with multiple control modes. Automatic control maintains target parameters through continuous reactivity adjustment. Manual control allows operators to directly manipulate the reactor. Various intermediate modes bridge these extremes. In typical pressurized water reactor operation, the reactor control system automatically maintains a floating average temperature. It compensates for power demand changes through reactivity feedback loops alone. Safety systems already employ extensive automation. Reactor Protection Systems trip automatically on safety signals with millisecond response times. Engineered safety features actuate automatically on accident signals—no operator action required.
 
-The division between automated and human-controlled functions reveals the fundamental challenge of hybrid control. Highly automated systems handle reactor protection: automatic trips on safety parameters, emergency core cooling actuation, containment isolation, and basic process control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators retain control of strategic decision-making: power level changes, startup/shutdown sequences, mode transitions, and procedure implementation.
+The division between automated and human-controlled functions reveals the fundamental challenge of hybrid control: highly automated systems handle reactor protection (automatic trips on safety parameters, emergency core cooling actuation, containment isolation, and basic process control~\cite{WRPS.Description, gentillon_westinghouse_1999}), while human operators retain control of strategic decision-making (power level changes, startup/shutdown sequences, mode transitions, and procedure implementation).
 
 \subsection{Human Factors in Nuclear Accidents}
 
@@ -35,7 +35,7 @@ shift supervisors~\cite{10CFR55}. Staffing typically requires at least two ROs
 and one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor
 operator requires several years of training.
 
-Despite decades of improvements in training and procedures, human error persistently contributes to nuclear safety incidents. This persistence motivates formal automated control with mathematical safety guarantees. Under 10 CFR Part 55, operators hold legal authority to make critical decisions, including authority to depart from normal regulations during emergencies. The Three Mile Island (TMI) accident demonstrated how personnel error, design deficiencies, and component failures combine to cause disaster. Operators misread confusing and contradictory indications. They then shut off the emergency water system~\cite{Kemeny1979}. The President's Commission on TMI identified a
+Despite decades of improvements in training and procedures, human error persistently contributes to nuclear safety incidents—a persistence that motivates formal automated control with mathematical safety guarantees. Under 10 CFR Part 55, operators hold legal authority to make critical decisions, including authority to depart from normal regulations during emergencies. The Three Mile Island (TMI) accident demonstrated how personnel error, design deficiencies, and component failures combine to cause disaster: operators misread confusing and contradictory indications, then shut off the emergency water system~\cite{Kemeny1979}. The President's Commission on TMI identified a
 fundamental ambiguity: placing responsibility for safe power plant operations on
 the licensee without formally verifying that operators can fulfill this
 responsibility does not guarantee safety. This tension between operational
@@ -56,7 +56,7 @@ limitations are fundamental to human-driven control, not remediable defects.
 
 \subsection{Formal Methods}
 
-The previous two subsections revealed two critical limitations of current practice: procedures lack formal verification, and human operators introduce persistent reliability issues that four decades of training improvements have failed to eliminate. Training and procedural improvements cannot solve these problems—but formal methods might, offering mathematical guarantees of correctness that could eliminate both human error and procedural ambiguity.
+The previous two subsections revealed two critical limitations of current practice: procedures lack formal verification, and human operators introduce persistent reliability issues that four decades of training improvements have failed to eliminate. Training and procedural improvements cannot solve these problems—but formal methods might offer mathematical guarantees of correctness that could eliminate both human error and procedural ambiguity.
 
 Even the most advanced formal methods applications in nuclear control, however, leave a critical verification gap for autonomous hybrid systems. This subsection examines two approaches illustrating this gap: HARDENS, which verified discrete logic without continuous dynamics, and differential dynamic logic, which handles hybrid verification only post-hoc. Each demonstrates the current state of formal methods while revealing the verification gap this research addresses.
 

3-research-approach/v3.tex

@@ -21,7 +21,7 @@ This work bridges the gap by composing formal methods from computer science with
 
 Hybrid system verification faces a fundamental challenge. Discrete transitions change the governing vector field. This creates discontinuities in system behavior through the interaction between discrete and continuous dynamics. Traditional verification techniques fail to handle this interaction directly.
 
-Our methodology decomposes the problem by verifying discrete switching logic and continuous mode behavior separately, then composing them to establish guarantees for the complete hybrid system. This two-layer approach mirrors reactor operations: discrete supervisory logic determines which control mode is active, while continuous controllers govern plant behavior within each mode.
+Our methodology decomposes the problem by verifying discrete switching logic and continuous mode behavior separately, then composing them to establish guarantees for the complete hybrid system—a two-layer approach that mirrors reactor operations where discrete supervisory logic determines which control mode is active while continuous controllers govern plant behavior within each mode.
 
 Building a high-assurance hybrid autonomous control system requires
 a mathematical description of the system. This work draws on
@@ -56,7 +56,7 @@ where:
 
 Creating a HAHACS requires constructing 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?} Section 2 established that existing approaches verify either discrete logic or continuous dynamics—never both compositionally. Reactive synthesis, reachability analysis, and barrier certificates each exist independently. Three key innovations compose them into a complete methodology for hybrid control synthesis:
+\textbf{What is new in this research?} Section 2 established that existing approaches verify either discrete logic or continuous dynamics—never both compositionally. While reactive synthesis, reachability analysis, and barrier certificates each exist independently, no prior work has integrated them into a systematic design methodology spanning procedures to verified implementation. Three key innovations enable this integration:
 
 \begin{enumerate}
 \item \textbf{Contract-based decomposition:} Discrete synthesis defines entry/exit/safety contracts that bound continuous verification, inverting the traditional global hybrid system verification approach.
@@ -64,8 +64,6 @@ Creating a HAHACS requires constructing this tuple together with proof artifacts
 \item \textbf{Procedure-driven structure:} Existing procedural structure avoids global hybrid system analysis, making the approach tractable for complex systems like nuclear reactor startup.
 \end{enumerate}
 
-Prior work has not integrated these three techniques into a systematic design methodology spanning procedures to verified implementation.
-
 \textbf{Why will it succeed?} Three factors ensure practical feasibility:
 
 \begin{enumerate}
@@ -140,13 +138,13 @@ Feasibility demonstrates on production control systems with realistic reactor mo
 
 \subsection{System Requirements, Specifications, and Discrete Controllers}
 
-The previous subsection established the hybrid automaton formalism—a mathematical framework for describing discrete modes, continuous dynamics, guards, and invariants. But where do these formal descriptions come from? Nuclear operations already possess a natural hybrid structure that maps directly to the automaton formalism through three control scopes: strategic, operational, and tactical. This subsection shows how to construct formal hybrid systems from existing operational knowledge rather than imposing artificial abstractions.
+The previous subsection established the hybrid automaton formalism—a mathematical framework for describing discrete modes, continuous dynamics, guards, and invariants—but did not address where these formal descriptions originate. Nuclear operations already possess a natural hybrid structure that maps directly to the automaton formalism through three control scopes: strategic, operational, and tactical. This subsection shows how to construct formal hybrid systems from existing operational knowledge rather than imposing artificial abstractions.
 
 Human control of nuclear power divides into three scopes: strategic, operational, and tactical. Strategic control represents high-level, long-term decision making spanning months or years: managing labor needs and supply chains to optimize scheduled maintenance and downtime.
 
 The tactical level controls individual components—pumps, turbines, and chemistry. Nuclear power plants have already automated tactical control through ``automatic control'' systems. These continuous systems directly impact the physical state of the plant, maintaining pressurizer level, core temperature, and reactivity through chemical shim.
 
-The operational scope links these extremes, representing the primary responsibility of human operators today. Operational control implements tactical control sequences to achieve strategic objectives, bridging high-level goals with low-level execution. 
+The operational scope links these extremes and represents the primary responsibility of human operators today, implementing tactical control sequences to achieve strategic objectives and bridging high-level goals with low-level execution. 
 
 An example clarifies this three-level structure. Consider a strategic goal to perform refueling at a certain time. The tactical level currently maintains core temperature. The operational level issues the shutdown procedure, using several smaller tactical goals along the way to achieve this objective.
 
@@ -186,7 +184,7 @@ This structure reveals why the operational and tactical levels fundamentally for
 \end{figure}
 
 
-This operational control level is the main reason nuclear control requires human operators. The hybrid nature of this control system makes proving controller performance against strategic requirements difficult. Unified infrastructure for building and verifying hybrid systems does not currently exist. Humans fill this layer because their general intelligence provides a safe way to manage the system's hybrid nature. These operators follow prescriptive operating manuals. Strict procedures govern what control to implement at any given time. These procedures provide the key to the operational control scope.
+This operational control level is the main reason nuclear control requires human operators: the hybrid nature of this control system makes proving controller performance against strategic requirements difficult, and unified infrastructure for building and verifying hybrid systems does not currently exist. Humans fill this layer because their general intelligence provides a safe way to manage the system's hybrid nature, following prescriptive operating manuals where strict procedures govern what control to implement at any given time. These procedures provide the key to the operational control scope.
 
 Constructing a HAHACS leverages two key observations about current practice. First, operational scope control is effectively discrete control. Second, operating procedures describe implementation rules before construction begins. A HAHACS's intended behavior must be completely described before construction. Requirements define the behavior of any control system: statements about what
 the system must do, must not do, and under what conditions. For nuclear systems,
@@ -232,7 +230,7 @@ eventually reaches operating temperature''), and response properties (``if
 coolant pressure drops, the system initiates shutdown within bounded time'').
 
 
-This work uses FRET (Formal Requirements Elicitation Tool) to build these temporal logic statements. NASA developed FRET for high-assurance timed systems. FRET provides an intermediate language between temporal logic and natural language. It enables rigid definitions of temporal behavior through syntax accessible to engineers without formal methods expertise. This accessibility proves crucial for industrial feasibility. Reducing required expert knowledge makes these tools adoptable by the current nuclear workforce.
+This work uses FRET (Formal Requirements Elicitation Tool)—developed by NASA for high-assurance timed systems—to build these temporal logic statements. FRET provides an intermediate language between temporal logic and natural language, enabling rigid definitions of temporal behavior through syntax accessible to engineers without formal methods expertise. This accessibility proves crucial for industrial feasibility by making these tools adoptable by the current nuclear workforce without requiring extensive formal methods training.
 
 FRET's key feature is its ability to start with logically imprecise
 statements and refine them consecutively into well-posed specifications. We
@@ -267,7 +265,7 @@ Reactive synthesis offers a decisive advantage: the discrete automaton requires
 
 This shift carries two critical implications. First, complete traceability: the reasons the controller changes between modes trace back through specifications to requirements, establishing 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. Defining system behavior using temporal logics and synthesizing the controller using deterministic algorithms ensures strategic decisions always follow operating procedures exactly—no exceptions, no deviations, no human factors.
 
-The synthesized automaton translates directly to executable code through standard compilation techniques. Each discrete state maps to a control mode, guard conditions map to conditional statements, and the transition function defines the control flow. This compilation process preserves the formal guarantees: the implemented code is correct by construction because the automaton it derives from was synthesized to satisfy the temporal logic specifications.
+The synthesized automaton translates directly to executable code through standard compilation techniques where each discrete state maps to a control mode, guard conditions map to conditional statements, and the transition function defines the control flow. This compilation process preserves the formal guarantees by ensuring the implemented code is correct by construction—the automaton from which it derives was synthesized to satisfy the temporal logic specifications.
 
 Reactive synthesis has proven successful in robotics, avionics, and industrial control. 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.
 
@@ -283,9 +281,9 @@ Reactive synthesis has proven successful in robotics, avionics, and industrial c
 
 \subsection{Continuous Control Modes}
 
-The previous subsection established that reactive synthesis produces a provably correct discrete controller from operating procedures. This automaton determines when to switch between modes. But hybrid control requires more than correct mode switching. The continuous dynamics executing within each discrete mode must also verify to ensure correct system behavior.
+The previous subsection established that reactive synthesis produces a provably correct discrete controller from operating procedures—an automaton that determines when to switch between modes. Hybrid control, however, requires more than correct mode switching: the continuous dynamics executing within each discrete mode must also be verified to ensure correct system behavior.
 
-This subsection describes the continuous control modes executing within each discrete state and explains how they verify against requirements imposed by the discrete layer. Control objectives determine the verification approach. Modes classify into three types—transitory, stabilizing, and expulsory—each requiring different verification tools matched to their distinct purposes. 
+This subsection describes the continuous control modes executing within each discrete state and explains how they verify against requirements imposed by the discrete layer. Control objectives determine the verification approach: modes classify into three types—transitory, stabilizing, and expulsory—each requiring different verification tools matched to their distinct purposes. 
 
 This methodology's scope requires clarification: this work verifies continuous controllers but does not synthesize them. The distinction parallels model checking in software verification, where verification 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 is the verification framework confirming that candidate controllers compose correctly with the discrete layer to produce a safe hybrid system.
 
@@ -391,7 +389,7 @@ appropriate to the fidelity of the reactor models available.
 
 \subsubsection{Stabilizing Modes}
 
-The previous subsection addressed transitory modes—modes that drive the system toward exit conditions. Stabilizing modes do the opposite: they 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.
+Transitory modes drive the system toward exit conditions. Stabilizing modes, in contrast, 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.
 
 Where reachability analysis answers "can the system reach a target?", stabilizing modes ask "does the system stay within bounds?" Barrier certificates provide the appropriate tool.
 Barrier certificates analyze the dynamics of the system to determine whether
@@ -445,7 +443,7 @@ controller.
 
 \subsubsection{Expulsory Modes}
 
-The first two mode types handle nominal operations: transitory modes move the plant between conditions, while stabilizing modes maintain the plant within regions. Both assume plant dynamics match the design model. Expulsory modes handle the opposite case—when the plant deviates from expected behavior due to component failures, sensor degradation, or unanticipated disturbances.
+The first two mode types—transitory modes that move the plant between conditions and stabilizing modes that maintain the plant within regions—handle nominal operations under the assumption that plant dynamics match the design model. Expulsory modes handle the opposite case: situations where the plant deviates from expected behavior due to component failures, sensor degradation, or unanticipated disturbances.
 
 Expulsory controllers prioritize robustness over optimality. The control objective shifts from reaching targets or maintaining regions to driving the plant to a safe shutdown state from potentially anywhere in the state space, under degraded or uncertain dynamics. Examples include emergency core cooling, reactor SCRAM sequences, and controlled depressurization procedures.
 

5-risks-and-contingencies/v1.tex

@@ -122,6 +122,6 @@ extensions, ensuring they address industry-wide practices rather than specific
 quirks.
 
 
-This section answered the Heilmeier question \textbf{What could prevent success?} Four primary risks threaten project completion: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, completeness of procedure formalization, and hardware-in-the-loop integration challenges. Each risk has identifiable early warning indicators and viable mitigation strategies. The staged project structure ensures that partial success yields publishable results while clearly identifying remaining barriers to deployment. Even when core assumptions prove invalid, the research produces valuable contributions advancing the field.
+This section answered the Heilmeier question \textbf{What could prevent success?} Four primary risks threaten project completion: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, completeness of procedure formalization, and hardware-in-the-loop integration challenges. Each risk has identifiable early warning indicators and viable mitigation strategies that preserve research value even when core assumptions fail. The staged project structure ensures that partial success yields publishable results while clearly identifying remaining barriers to deployment—a critical design feature that maintains contribution to the field regardless of which technical obstacles prove insurmountable.
 
 The technical research plan is now complete: Section 3 established what will be done; Section 4 established how success will be measured; this section established what might prevent it. One critical Heilmeier question remains—\textbf{Who cares? Why now? What difference will it make?}—which Section 6 answers by connecting this technical methodology to urgent economic and infrastructure challenges facing the nuclear industry and broader energy sector.

6-broader-impacts/v1.tex

@@ -1,8 +1,6 @@
 \section{Broader Impacts}
 
-\textbf{Who cares? Why now? What difference will it make?} These three Heilmeier questions connect technical methodology to economic and societal impact. Sections 2--5 established the technical research plan: what has been done (Section 2), what is new and why it will succeed (Section 3), how success will be measured (Section 4), and what could prevent success (Section 5). This section addresses the remaining Heilmeier questions by connecting the technical methodology to urgent economic and infrastructure challenges.
-
-Three stakeholder groups face the same economic constraint: the nuclear industry, datacenter operators, and clean energy advocates. All confront high operating costs driven by staffing requirements. AI infrastructure demands, growing exponentially, have made this constraint urgent.
+\textbf{Who cares? Why now? What difference will it make?} These three Heilmeier questions connect technical methodology to economic and societal impact. Sections 2--5 established the technical research plan: what has been done (Section 2), what is new and why it will succeed (Section 3), how success will be measured (Section 4), and what could prevent success (Section 5). This section addresses the remaining Heilmeier questions by connecting the technical methodology to urgent economic and infrastructure challenges facing three convergent stakeholder groups—the nuclear industry, datacenter operators, and clean energy advocates—all confronting the same economic constraint: high operating costs driven by staffing requirements. Exponentially growing AI infrastructure demands have transformed this longstanding challenge into an immediate crisis.
 
 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, but nuclear power economics at this scale demand careful attention to operating costs.