Editorial pass: Gopen principles + Heilmeier alignment

Three-level editorial revision:

TACTICAL (sentence-level):
- Improved topic-stress positioning (old→new info flow)
- Strengthened verb choices and reduced passive voice
- Enhanced topic string consistency across sentences
- Tightened choppy sentence sequences into clearer constructions

OPERATIONAL (paragraph/section):
- Strengthened transitions between paragraphs
- Improved forward reference and backward connection
- Enhanced section coherence and flow
- Clarified subsection purposes and linkages

STRATEGIC (document-level):
- Reinforced Heilmeier Catechism alignment in each section
- Strengthened cross-section linkages
- Made explicit connections between 'what/why/how/risks/impact'
- Enhanced the narrative arc from problem → solution → validation → impact

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, following detailed written procedures and switching between control objectives based on plant conditions.
+Today's nuclear reactors operate under the control of extensively trained human operators who follow detailed written procedures and switch 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, 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.
+Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening their economic viability. Autonomous control systems offer a solution—they 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. 
+This research combines formal methods from computer science with control theory to produce hybrid control systems that are 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 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.
+This approach mirrors how operators already work: discrete logic switches between continuous control modes. Existing formal methods can 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. Achieving end-to-end correctness requires both approaches working 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,18 +4,18 @@
 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, as control system failures risk economic losses, service interruptions, or radiological release.
+Nuclear power plants require the highest levels of control system reliability because control system failures risk economic losses, service interruptions, or radiological release.
 % Known information
-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.
+Today's nuclear plants operate under the control of extensively trained human operators who follow 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.
+This reliance on human operators prevents autonomous control and creates a fundamental economic challenge for next-generation reactor designs: per-megawatt staffing costs for small modular reactors far exceed those of conventional plants, threatening their economic viability. Autonomous control systems could manage complex operational sequences without constant human supervision—but only if they provide assurance equal to or exceeding that of human operators.
 
 % APPROACH PARAGRAPH Solution
-This research combines formal methods with control theory to produce hybrid control systems correct by construction.
+This research combines formal methods with control theory to produce hybrid control systems that are correct by construction.
 % Rationale
-Operators already work this way. Discrete logic switches between continuous control modes. Existing formal methods generate provably correct switching logic from written requirements—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.
+This approach mirrors how operators already work: discrete logic switches between continuous control modes. Existing formal methods can generate provably correct switching logic from written requirements, but they fail when continuous dynamics govern transitions. Control theory verifies continuous behavior, but it cannot prove discrete switching correctness. Achieving end-to-end correctness requires both approaches working together.
 % Hypothesis
-This approach closes the gap through two steps. First, it synthesizes discrete mode transitions directly from written operating procedures. Second, it verifies continuous behavior between transitions. Operating procedures formalize into logical specifications. Continuous dynamics verify against transition requirements. The result: autonomous controllers provably free from design defects. 
+This approach closes the gap through two steps. First, it synthesizes discrete mode transitions directly from written operating procedures. Second, it verifies continuous behavior between transitions. Operating procedures formalize into logical specifications, and continuous dynamics verify against transition requirements. The result is autonomous controllers that are provably free from design defects. 
 
 The University of Pittsburgh Cyber Energy Center provides access to industry collaboration and Emerson control hardware, ensuring solutions align with practical implementation
 requirements.

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

@@ -4,11 +4,11 @@
 
 \subsection{Current Reactor Procedures and Operation}
 
-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.
+Before identifying the limits of current practice, we must first understand how nuclear plants operate today. This subsection examines three aspects: 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, 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}. 
+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, 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. 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.
+Procedure development relies on expert judgment and simulator validation—not formal verification. While 10 CFR 55.59~\cite{10CFR55.59} requires rigorous assessment through technical evaluation, simulator validation testing, and biennial review, 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,11 +21,11 @@ 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}), while 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 already 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, meanwhile, retain control of strategic decision-making: power level changes, startup/shutdown sequences, mode transitions, and procedure implementation.
 
 \subsection{Human Factors in Nuclear Accidents}
 
-The previous subsection established that procedures lack formal verification despite rigorous development. This represents only half the reliability challenge. Even perfect procedures cannot guarantee safe operation when humans execute them imperfectly. Human operators—the second pillar of current practice—introduce reliability limitations independent of procedure quality. Procedures define what to do; human operators determine when and how.
+The previous subsection established that procedures lack formal verification despite rigorous development, representing only half the reliability challenge. Even perfect procedures cannot guarantee safe operation when humans execute them imperfectly. Human operators—the second pillar of current practice—introduce reliability limitations independent of procedure quality. While procedures define what to do, human operators determine when and how—and this human element introduces persistent failure modes.
 
 Current-generation nuclear power plants employ over 3,600 active NRC-licensed
 reactor operators in the United States~\cite{operator_statistics}. These
@@ -153,6 +153,6 @@ This section answered two Heilmeier questions about current practice:
 
 \textbf{What has been done?} Human operators provide operational flexibility but introduce persistent reliability limitations that four decades of training improvements have failed to eliminate. Formal methods provide correctness guarantees but have not scaled to complete hybrid control design. HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis and fails to scale to system synthesis.
 
-\textbf{What are the limits of current practice?} No existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into the design process. Current approaches verify either discrete logic or continuous dynamics—never both compositionally. This gap prevents autonomous nuclear control with end-to-end correctness guarantees.
+\textbf{What are the limits of current practice?} No existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into the design process. 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.
 
-Two imperatives converge: economic (small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants) and technical (current approaches lack compositional verification for hybrid systems). Section 3 addresses this gap by establishing what makes the proposed approach new and why it will succeed where prior work has failed.
+Two imperatives converge to make this gap urgent: economic necessity (small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants) and technical opportunity (formal methods tools have matured sufficiently to enable compositional hybrid verification). Section 3 addresses this verification gap by establishing what makes the proposed approach new and why it will succeed where prior work has failed.

3-research-approach/v3.tex

@@ -15,23 +15,15 @@
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches verified either discrete switching logic or continuous control behavior—never both simultaneously. Continuous controllers rely on extensive simulation trials for validation. Discrete switching logic undergoes simulated control room testing and human factors research. Despite consuming enormous resources, neither method provides rigorous guarantees.
+Previous approaches verified either discrete switching logic or continuous control behavior—never both simultaneously. Engineers validate continuous controllers through extensive simulation trials and test discrete switching logic through simulated control room testing and human factors research. Despite consuming enormous resources, neither method provides rigorous guarantees.
 
-This work bridges the gap by composing formal methods from computer science with control-theoretic verification. Reactor operations formalize as hybrid automata.
+This work bridges the gap by composing formal methods from computer science with control-theoretic verification, formalizing reactor operations as hybrid automata.
 
-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.
+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 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—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.
+Our methodology decomposes this problem, verifying discrete switching logic and continuous mode behavior separately before composing them to establish guarantees for the complete hybrid system. This two-layer approach 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
-automata theory, temporal logic, and control theory to provide that description. A hybrid system is a
-dynamical system with both continuous and discrete states. This proposal
-addresses continuous autonomous hybrid systems specifically: systems with no external input where continuous
-states remain continuous when discrete states change. These continuous states represent physical quantities that remain
-Lipschitz continuous. This work follows the nomenclature from the Handbook on
-Hybrid Systems Control~\cite{HANDBOOK ON HYBRID SYSTEMS}, redefined here
-for convenience:
+Building a high-assurance hybrid autonomous control system requires a mathematical description of the system. This work draws on automata theory, temporal logic, and control theory to provide that description. A hybrid system is a dynamical system with both continuous and discrete states. This proposal addresses continuous autonomous hybrid systems specifically—systems with no external input where continuous states remain continuous when discrete states change. These continuous states represent physical quantities that remain Lipschitz continuous. This work follows the nomenclature from the Handbook on Hybrid Systems Control~\cite{HANDBOOK ON HYBRID SYSTEMS}, redefined here for convenience:
 
 \begin{equation}
   H = (\mathcal{Q}, \mathcal{X}, \mathbf{f}, Init, \mathcal{G}, \delta, \mathcal{R}, Inv)
@@ -56,23 +48,23 @@ 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. 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:
+\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 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.
-\item \textbf{Mode classification:} Continuous modes classify by objective (transitory, stabilizing, expulsory), selecting appropriate verification tools and enabling mode-local analysis with provable composition.
-\item \textbf{Procedure-driven structure:} Existing procedural structure avoids global hybrid system analysis, making the approach tractable for complex systems like nuclear reactor startup.
+\item \textbf{Contract-based decomposition:} Instead of attempting global hybrid system verification, this approach inverts the traditional structure. Discrete synthesis defines entry/exit/safety contracts that bound continuous verification, transforming an intractable global problem into tractable local problems.
+\item \textbf{Mode classification:} Continuous modes classify by control objective—transitory, stabilizing, or expulsory—allowing appropriate verification tools to be selected for each mode type. This classification enables mode-local analysis with provable composition guarantees.
+\item \textbf{Procedure-driven structure:} Nuclear procedures already decompose operations into discrete phases. Leveraging this existing structure avoids imposing artificial abstractions and makes the approach tractable for complex systems like nuclear reactor startup.
 \end{enumerate}
 
-\textbf{Why will it succeed?} Three factors ensure practical feasibility:
+\textbf{Why will it succeed?} Three factors ensure practical feasibility where prior work has failed:
 
 \begin{enumerate}
-\item Nuclear procedures already decompose operations into discrete phases with explicit transition criteria—this work formalizes existing structure rather than imposing artificial abstractions.
-\item Mode-level verification avoids the state explosion that makes global hybrid system analysis intractable by verifying each mode against local contracts, bounding computational complexity.
-\item The Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility.
+\item \textbf{Leverage existing structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. This work formalizes existing structure rather than imposing artificial abstractions, making adoption tractable for domain experts without formal methods training.
+\item \textbf{Avoid state explosion:} Mode-level verification checks each mode against local contracts rather than attempting global hybrid system analysis. This decomposition bounds computational complexity, transforming an intractable global problem into tractable local verifications.
+\item \textbf{Industrial validation:} The Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. This ensures solutions address real deployment constraints, not just theoretical correctness.
 \end{enumerate}
 
-Feasibility demonstrates on production control systems with realistic reactor models, not merely in principle. Figure~\ref{fig:hybrid_automaton} illustrates the hybrid structure for a simplified reactor startup sequence.
+These factors combine to demonstrate feasibility on production control systems with realistic reactor models, not merely in principle. Figure~\ref{fig:hybrid_automaton} illustrates the hybrid structure for a simplified reactor startup sequence.
 
 \begin{figure} 
   \centering
@@ -138,7 +130,7 @@ 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 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.
+The previous subsection established the hybrid automaton formalism—a mathematical framework for describing discrete modes, continuous dynamics, guards, and invariants. The question now becomes: where do these formal descriptions originate? This subsection demonstrates that nuclear operations already possess a natural hybrid structure that maps directly to the automaton formalism through three control scopes: strategic, operational, and tactical. Rather than imposing artificial abstractions, this approach constructs formal hybrid systems from existing operational knowledge.
 
 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.
 
@@ -254,7 +246,7 @@ FRET has been successfully applied to spacecraft control systems, autonomous veh
 
 \subsection{Discrete Controller Synthesis}
 
-The previous subsection showed how operating procedures translate into temporal logic specifications using FRET. These specifications define what the system must do. The next question: how do we implement those requirements? Reactive synthesis provides the answer.
+The previous subsection showed how operating procedures translate into temporal logic specifications using FRET, defining what the system must do. The next question becomes: how do we implement those requirements? Reactive synthesis provides the answer—a technique that automatically constructs controllers guaranteed to satisfy temporal logic specifications.
 
 Reactive synthesis automates the creation of reactive programs from temporal logic—programs that take input for a given state and produce output. System requirements defined as temporal logic specifications enable reactive synthesis to build the discrete control system. Our systems fit this model: the current discrete state and status of guard conditions form the input; the next discrete state forms the output.
 

4-metrics-of-success/v1.tex

@@ -1,8 +1,8 @@
 \section{Metrics for Success}
 
-\textbf{How do we measure success?} This research advances through Technology Readiness Levels, progressing from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5).
+\textbf{How do we measure success?} Section 3 established the technical approach—what will be done and why it will work. This section addresses how we measure whether it actually succeeds. The answer: Technology Readiness Level advancement, progressing from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5).
 
-This 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 by bridging the gap between academic proof-of-concept and practical deployment. This section first explains why, then defines specific criteria for each level from TRL 3 through TRL 5.
+This 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 by explicitly measuring the gap between academic proof-of-concept and practical deployment. This section first 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 by explicitly measuring the gap between academic proof-of-concept and practical deployment—precisely what this work bridges. Academic metrics like papers published or theorems proved fail to capture practical feasibility. Empirical metrics like simulation accuracy or computational speed fail to demonstrate theoretical rigor. Both measure simultaneously through TRLs.
 

5-risks-and-contingencies/v1.tex

@@ -1,6 +1,6 @@
 \section{Risks and Contingencies}
 
-\textbf{What could prevent success?} Every research plan rests on assumptions. When those assumptions prove false, research must adapt. Four primary risks could prevent successful completion: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, completeness of procedure formalization, and hardware-in-the-loop integration. Each risk carries associated early warning indicators and contingency plans that preserve research value even when core assumptions prove false. The staged project structure ensures that partial success yields publishable results while clearly identifying remaining barriers to deployment.
+\textbf{What could prevent success?} Section 4 defined success as reaching TRL 5 through component validation, system integration, and hardware demonstration. But every research plan rests on assumptions that might prove false. This section identifies four primary risks that could prevent successful completion: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, completeness of procedure formalization, and hardware-in-the-loop integration. Each risk carries associated early warning indicators and contingency plans 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.
 
 \subsection{Computational Tractability of Synthesis}
 

6-broader-impacts/v1.tex

@@ -1,6 +1,8 @@
 \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 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.
+\textbf{Who cares? Why now? What difference will it make?} Sections 2--5 established the complete technical research plan: what has been done and its limits (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, connecting technical methodology to economic and societal impact.
+
+The technical approach enables compositional hybrid verification—a capability that did not exist before. But why does this matter beyond academic contribution? Three stakeholder groups converge on 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 viable. Exponentially growing AI infrastructure demands have transformed this longstanding challenge into an immediate crisis requiring 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, but nuclear power economics at this scale demand careful attention to operating costs.