Editorial pass: Gopen structure + Heilmeier alignment

Three-pass editorial review:

TACTICAL (sentence-level):
- Improved topic-stress positioning throughout
- Changed weak 'cannot' to stronger 'fail to'
- Converted passive constructions to active voice
- Removed unnecessary em-dashes, replaced with commas/colons
- Split overly complex sentences for clarity
- Strengthened verb choices

OPERATIONAL (paragraph/section):
- Enhanced transitions between subsections
- Improved paragraph coherence and flow
- Added explicit backward references ('defined above', etc.)
- Clarified progression of ideas within sections
- Split semicolon-joined sentences for better rhythm

STRATEGIC (document-level):
- Made Heilmeier questions more explicit throughout
- Strengthened section-to-section bridges
- Ensured each section clearly answers its assigned questions
- Improved parallel structure in summaries
- Enhanced roadmap/signposting between sections

Focus: clarity and impact without changing technical content.

1-goals-and-outcomes/research_statement_v1.tex

@@ -2,9 +2,9 @@
 This research develops autonomous control systems with mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
-Extensively trained operators manage nuclear reactors by following detailed written procedures. Plant conditions guide their decisions when they switch between control objectives.
+Extensively trained operators manage nuclear reactors by following detailed written procedures. When operators switch between control objectives, plant conditions guide their decisions.
 % Gap
-Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening viability. Autonomous control systems must manage complex operational sequences safely—without constant supervision—while providing assurance equal to or exceeding that of human-operated systems.
+Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening viability. Autonomous control systems must manage complex operational sequences safely without constant supervision while providing assurance equal to or exceeding that of human-operated systems.
 
 % APPROACH PARAGRAPH Solution
 We combine formal methods from computer science with control theory to
@@ -12,9 +12,9 @@ build hybrid control systems that are correct by construction.
 % Rationale
 Hybrid systems mirror how operators work: discrete
 logic switches between continuous control modes. Existing formal methods
-generate provably correct switching logic but cannot handle continuous dynamics
+generate provably correct switching logic but fail to handle continuous dynamics
 during transitions. Control theory verifies continuous behavior but
-cannot prove the correctness of discrete switching decisions. 
+fails to prove the correctness of discrete switching decisions. 
 % Hypothesis and Technical Approach
 Our methodology bridges this gap through three stages. First, we translate written
 operating procedures into temporal logic specifications using NASA's Formal
@@ -24,8 +24,8 @@ checking identifies conflicts and ambiguities before implementation.
 Second, reactive synthesis generates deterministic automata that are provably
 correct by construction.
 Third, we design continuous controllers for each discrete mode using standard
-control theory and verify them using reachability analysis. We classify continuous modes by their transition objectives. Assume-guarantee contracts and barrier certificates prove that mode transitions occur safely. Local verification of continuous modes
-becomes possible without requiring global trajectory analysis across the entire hybrid system. This methodology is demonstrated on an
+control theory and verify them using reachability analysis. Continuous modes are classified by their transition objectives. Assume-guarantee contracts and barrier certificates prove that mode transitions occur safely. This approach enables local verification of continuous modes
+without requiring global trajectory analysis across the entire hybrid system. We demonstrate this methodology on an
 Emerson Ovation control system. 
 % Pay-off
 Autonomous control can then manage complex nuclear

1-goals-and-outcomes/v1.tex

@@ -8,14 +8,14 @@ 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 plant operations rely on extensively trained human operators who follow detailed written procedures and strict regulatory requirements to manage reactor control. When operators switch between different control modes, plant conditions and procedural guidance inform their decisions.
+Nuclear plant operations rely on extensively trained human operators who follow detailed written procedures and strict regulatory requirements to manage reactor control. Plant conditions and procedural guidance inform operator decisions when switching between different control modes.
 % Gap
 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 that far exceed those of conventional plants, threatening economic viability. The nuclear industry needs autonomous control systems that manage complex operational sequences safely without constant human supervision while providing assurance equal to or exceeding that of human-operated systems.
 
 % APPROACH PARAGRAPH Solution
 We combine formal methods with control theory to build hybrid control systems that are correct by construction.
 % Rationale
-Hybrid systems mirror how operators work: discrete logic switches between continuous control modes. Existing formal methods generate provably correct switching logic from written requirements but cannot handle continuous dynamics during transitions. Control theory verifies continuous behavior but cannot prove the correctness of discrete switching decisions. No existing approach provides end-to-end correctness guarantees.
+Hybrid systems mirror how operators work: discrete logic switches between continuous control modes. Existing formal methods generate provably correct switching logic from written requirements but fail to handle continuous dynamics during transitions. Control theory verifies continuous behavior but fails to prove the correctness of discrete switching decisions. No existing approach provides end-to-end correctness guarantees.
 % Hypothesis
 Our approach closes this gap by synthesizing discrete mode transitions directly
 from written operating procedures and verifying continuous behavior between
@@ -72,8 +72,8 @@ If this research is successful, we will be able to do the following:
 % 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 is new?} We unify discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems.
-Formal methods verify discrete logic; control theory verifies
+\textbf{What is new in this research?} We unify 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. This work establishes that bridge by treating discrete specifications
 as contracts that continuous controllers must satisfy, enabling independent

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

@@ -4,7 +4,7 @@
 
 \subsection{Current Reactor Procedures and Operation}
 
-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 scenarios. These procedures must comply with 10 CFR 50.34(b)(6)(ii); NUREG-0899 provides development guidance~\cite{NUREG-0899, 10CFR50.34}. However, their 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 this rigor cannot provide formal verification of key safety properties. No mathematical proof exists that procedures cover all possible plant states, that required actions complete within available timeframes, or that transitions between procedure sets maintain safety invariants.
+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 scenarios. These procedures must comply with 10 CFR 50.34(b)(6)(ii); NUREG-0899 provides development guidance~\cite{NUREG-0899, 10CFR50.34}. Their 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 this rigor cannot provide formal verification of key safety properties. No mathematical proof exists that procedures cover all possible plant states, that required actions complete within available timeframes, or that transitions between procedure sets maintain safety invariants.
 
 \textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness
 and completeness.} Current procedure development relies on expert judgment and
@@ -36,7 +36,7 @@ startup/shutdown sequences, mode transitions, and procedure implementation.
 
 \subsection{Human Factors in Nuclear Accidents}
 
-Procedures lack formal verification despite rigorous development. This represents only half the reliability challenge. The second pillar of current practice—human operators who execute these procedures—introduces additional reliability limitations. Procedures define what to do; human operators determine when and how to apply them. Even perfectly written procedures cannot eliminate human error.
+Procedures lack formal verification despite rigorous development, but this represents only half the reliability challenge. The second pillar of current practice—human operators who execute these procedures—introduces additional reliability limitations independent of procedure quality. Procedures define what to do. Human operators determine when and how to apply them. Even perfectly written procedures fail to eliminate human error.
 
 Current-generation nuclear power plants employ over 3,600 active NRC-licensed
 reactor operators in the United States~\cite{operator_statistics}. These
@@ -54,7 +54,7 @@ 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
-flexibility and safety assurance remains unresolved—the person responsible for
+flexibility and safety assurance remains unresolved. The person responsible for
 reactor safety often becomes the root cause of failures.
 
 Multiple independent analyses converge on a striking statistic: human error accounts for 70--80\% of nuclear power plant events, compared to approximately 20\% for equipment failures~\cite{WNA2020}. More significantly, human factors—poor safety management and safety culture—caused all severe accidents at nuclear power plants: Three Mile Island, Chernobyl, and Fukushima Daiichi~\cite{hogberg_root_2013}. A detailed analysis
@@ -141,7 +141,7 @@ primary assurance evidence.
 
 \subsubsection{Differential Dynamic Logic: Post-Hoc Hybrid Verification}
 
-HARDENS verified discrete control logic but omitted continuous dynamics—a fundamental limitation for hybrid systems. Recognizing this gap, other researchers pursued a complementary approach: extending temporal logics to handle hybrid systems directly. This work produced differential dynamic logic (dL). dL introduces two additional operators
+HARDENS verified discrete control logic but omitted continuous dynamics, a fundamental limitation for hybrid systems. Recognizing this gap, other researchers pursued a complementary approach: extending temporal logics to handle hybrid systems directly. This work produced differential dynamic logic (dL). dL introduces two additional operators
 into temporal logic: the box operator and the diamond operator. The box operator
 \([\alpha]\phi\) states that for some region \(\phi\), the hybrid system
 \(\alpha\) always remains within that region. In this way, it is a safety
@@ -176,8 +176,8 @@ design loop for complex systems like nuclear reactor startup procedures.
 
 This section answered two Heilmeier questions:
 
-\textbf{What has been done?} Human operators provide operational flexibility but introduce persistent reliability limitations—four decades of training improvements have failed to eliminate them. 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 does not scale to system synthesis.
+\textbf{What has been done?} Human operators provide operational flexibility but introduce persistent reliability limitations. Four decades of training improvements have failed to eliminate them. 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 does not 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. This gap—between discrete-only formal methods and post-hoc hybrid verification—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. This gap between discrete-only formal methods and post-hoc hybrid verification prevents autonomous nuclear control with end-to-end correctness guarantees.
 
-Two imperatives are now clear. The economic imperative: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. The technical capability gap: current approaches verify either discrete logic or continuous dynamics, never both compositionally. Section 3 presents our methodology for bridging this gap. We establish what is new and why it will succeed where prior work has not.
+Two imperatives are now clear. First, the economic imperative: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Second, the technical capability gap: current approaches verify either discrete logic or continuous dynamics, never both compositionally. Section 3 presents our methodology for bridging this gap, establishing what is new and why it will succeed where prior work has not.

3-research-approach/v3.tex

@@ -15,15 +15,15 @@
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches to autonomous control 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 of control system behavior. HAHACS bridges this gap by composing formal methods from computer science with control-theoretic verification to formalize reactor operations using hybrid automata.
+Previous approaches to autonomous control 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. Neither method provides rigorous guarantees of control system behavior despite consuming enormous resources. HAHACS bridges this gap by composing formal methods from computer science with control-theoretic verification to formalize reactor operations using hybrid automata.
 
-Hybrid system verification faces a fundamental challenge: the interaction between discrete and continuous dynamics. Discrete transitions change the governing vector field, creating discontinuities in system behavior. Traditional verification techniques—designed for purely discrete or purely continuous systems—cannot handle this interaction directly. Our methodology decomposes the problem by verifying discrete switching logic and continuous mode behavior separately, then composes 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.
+Hybrid system verification faces a fundamental challenge: the interaction between discrete and continuous dynamics. Discrete transitions change the governing vector field, creating discontinuities in system behavior. Traditional verification techniques, designed for purely discrete or purely continuous systems, fail to handle this interaction directly. Our methodology decomposes the problem by verifying discrete switching logic and continuous mode behavior separately, then composes 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.
 
 Building a high-assurance hybrid autonomous control system (HAHACS) requires
 a mathematical description of the system. This work draws on
 automata theory, temporal logic, and control theory. A hybrid system is a
 dynamical system with both continuous and discrete states. This proposal
-discusses continuous autonomous hybrid systems specifically—systems with no external input where continuous
+discusses continuous autonomous hybrid systems specifically: systems with no external input where continuous
 states do not change instantaneously when discrete states change. These continuous states are physical quantities that remain
 Lipschitz continuous. We follow the nomenclature from the Handbook on
 Hybrid Systems Control~\cite{HANDBOOK ON HYBRID SYSTEMS}, redefined here
@@ -52,7 +52,7 @@ where:
 
 Creating a HAHACS requires constructing such a tuple together with proof artifacts that demonstrate the control system's actual implementation satisfies its intended behavior.
 
-\textbf{What is new?} Reactive synthesis, reachability analysis, and barrier certificates each exist independently. Our contribution is the architecture that composes them into a complete methodology for hybrid control synthesis. Three innovations provide the novelty:
+\textbf{What is new in this research?} Reactive synthesis, reachability analysis, and barrier certificates each exist independently. Our contribution is the architecture that composes them into a complete methodology for hybrid control synthesis. Three innovations provide the novelty:
 
 \begin{enumerate}
 \item Discrete synthesis defines entry/exit/safety contracts that bound continuous verification, inverting the traditional approach of verifying a complete hybrid system globally.
@@ -60,7 +60,7 @@ Creating a HAHACS requires constructing such a tuple together with proof artifac
 \item Existing procedural structure is leveraged to avoid global hybrid system analysis, making the approach tractable for complex systems like nuclear reactor startup.
 \end{enumerate}
 
-No prior work integrates these techniques into a systematic design methodology from procedures to verified implementation.
+No prior work integrates these three techniques into a systematic design methodology spanning procedures to verified implementation.
 
 \textbf{Why will it succeed?} Three factors ensure practical feasibility:
 
@@ -136,7 +136,7 @@ We demonstrate feasibility on production control systems with realistic reactor
 
 \subsection{System Requirements, Specifications, and Discrete Controllers}
 
-The eight-tuple hybrid automaton formalism provides a mathematical framework for describing discrete modes, continuous dynamics, guards, and invariants. This subsection shows how to construct such systems from existing operational knowledge rather than imposing artificial abstractions. Nuclear operations already possess a natural hybrid structure that maps directly to this automaton formalism.
+The hybrid automaton formalism defined above provides a mathematical framework for describing discrete modes, continuous dynamics, guards, and invariants. This subsection shows how to construct such systems from existing operational knowledge rather than imposing artificial abstractions. Nuclear operations already possess a natural hybrid structure that maps directly to this automaton formalism.
 
 Human control of nuclear power divides into three scopes: strategic, operational, and tactical. Strategic control represents high-level, long-term decision making for the plant. Objectives at this level are complex and economic in scale, such as managing labor needs and supply chains to optimize scheduled maintenance and downtime. These decisions span months or years. The lowest level—the
 tactical level—controls individual components: pumps, turbines, and
@@ -147,7 +147,7 @@ physical state of the plant. Tactical control objectives include maintaining
 pressurizer level, maintaining core temperature, or adjusting reactivity with a
 chemical shim.
 
-The operational control scope links these two extremes and represents the primary responsibility of human operators today. Operational control takes the current strategic objective and implements tactical control objectives to drive the plant toward strategic goals—bridging high-level and low-level objectives. 
+The operational control scope links these two extremes and represents the primary responsibility of human operators today. Operational control takes the current strategic objective and implements tactical control objectives to drive the plant toward strategic goals, bridging high-level and low-level objectives. 
 
 Consider an example: a strategic goal may be to
 perform refueling at a certain time, while the tactical level of the plant is
@@ -195,13 +195,12 @@ which tactical control law to apply. We target this operational level for autono
 \end{figure}
 
 
-This operational control level is the main reason human operators are required in nuclear control today. The hybrid nature of this control system makes it difficult to prove a controller will perform according to strategic requirements. 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 hybrid nature of the system. These operators use prescriptive operating
+This operational control level is the main reason human operators are required in nuclear control today. 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 use prescriptive operating
 manuals to perform their control with strict procedures on what control to
 implement at a given time. These procedures are 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 the rules for implementing this control before implementation. A HAHACS's intended behavior must be completely described before construction begins. The
-behavior of any control system originates in requirements: statements about what
+Constructing a HAHACS leverages two key observations about current practice. First, operational scope control is effectively discrete control. Second, operating procedures describe the implementation rules before construction. A HAHACS's intended behavior must be completely described before construction begins. 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,
 these requirements derive from multiple sources including regulatory mandates,
 design basis analyses, and operating procedures. The challenge is formalizing
@@ -226,10 +225,10 @@ continuous state space: $p_i: \mathcal{X} \rightarrow \{\text{true},
 temperature exceeds 315°C'' or ``pressurizer level is between 30\% and 60\%.''
 We do not impose this discrete abstraction artificially. Operating
 procedures for nuclear systems already define go/no-go conditions as discrete
-predicates. Design basis safety analysis determined these thresholds; decades of operational experience have
+predicates. Design basis safety analysis determined these thresholds. Decades of operational experience have
 validated them. Our methodology assumes
 this domain knowledge exists and provides a framework to formalize it. The approach is feasible for nuclear applications because generations
-of nuclear engineers have already done the hard
+of nuclear engineers have already completed the hard
 work of defining safe operating boundaries. 
 
 Linear temporal logic (LTL) is particularly well-suited for
@@ -411,7 +410,7 @@ appropriate to the fidelity of the reactor models available.
 
 \subsubsection{Stabilizing Modes}
 
-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. The different control objective requires a different verification approach: reachability analysis answers "can the system reach a target?" while stabilizing modes must prove "does the system stay within bounds?" Barrier certificates provide the appropriate tool.
+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. Reachability analysis answers "can the system reach a target?" Stabilizing modes must instead prove "does the system stay within bounds?" Barrier certificates provide the appropriate tool for this question.
 Barrier certificates analyze the dynamics of the system to determine whether
 flux across a given boundary exists. They evaluate whether any trajectory leaves
 a given boundary. This definition exactly matches what defines the validity of a
@@ -542,11 +541,11 @@ outcomes can align best with customer needs.
 
 This section answered two Heilmeier questions:
 
-\textbf{What is new?} We integrate reactive synthesis, reachability analysis, and barrier certificates into a compositional architecture for hybrid control synthesis. The methodology inverts traditional approaches by using discrete synthesis to define verification contracts, classifies continuous modes to select appropriate verification tools, and leverages existing procedural structure to avoid intractable global analysis.
+\textbf{What is new in this research?} We integrate reactive synthesis, reachability analysis, and barrier certificates into a compositional architecture for hybrid control synthesis. The methodology inverts traditional approaches by using discrete synthesis to define verification contracts, classifies continuous modes to select appropriate verification tools, and leverages existing procedural structure to avoid intractable global analysis.
 
-\textbf{Why will it succeed?} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria—the methodology formalizes existing structure rather than imposing artificial abstractions. Mode-level verification avoids state explosion by bounding each verification problem locally. The Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate practical implementation.
+\textbf{Why will this approach succeed?} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. The methodology formalizes existing structure rather than imposing artificial abstractions. Mode-level verification avoids state explosion by bounding each verification problem locally. The Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate practical implementation.
 
-We have now established the complete methodology—from procedure formalization through discrete synthesis to continuous verification and hardware implementation. The next question is: how do we measure success? Section 4 defines Technology Readiness Level advancement as the primary metric, demonstrating both theoretical correctness and practical implementability as the system progresses from component validation to integrated hardware testing.
+We have now established the complete methodology from procedure formalization through discrete synthesis to continuous verification and hardware implementation. Section 4 addresses the next Heilmeier question: how do we measure success? Technology Readiness Level advancement serves as the primary metric, demonstrating both theoretical correctness and practical implementability as the system progresses from component validation to integrated hardware testing.
 
 %%% NOTES (Section 5):
 % - Get specific details on ARCADE interface from Emerson collaboration

4-metrics-of-success/v1.tex

@@ -4,7 +4,7 @@
 Technology Readiness Levels, 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. This section explains why TRL advancement provides the most appropriate success metric. We then define specific criteria for 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. This section first explains why TRL advancement provides the most appropriate success 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 aims to bridge. Academic metrics like papers published or theorems proved cannot capture practical feasibility. Empirical metrics like simulation accuracy or computational speed cannot demonstrate theoretical rigor. Only TRLs measure both simultaneously.
 Advancing from TRL 3 to TRL 5 requires maintaining theoretical rigor while

5-risks-and-contingencies/v1.tex

@@ -143,6 +143,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—computational tractability, discrete-continuous interface complexity, procedure formalization completeness, and hardware integration—each have identifiable early indicators and viable mitigation strategies. The staged approach ensures valuable contributions even if core assumptions prove invalid. Partial success yields publishable results that clearly identify remaining barriers to deployment.
+This section answered the Heilmeier question \textbf{What could prevent success?} Four primary risks—computational tractability, discrete-continuous interface complexity, procedure formalization completeness, and hardware integration—each have identifiable early indicators and viable mitigation strategies. The staged approach ensures valuable contributions even if core assumptions prove invalid. Even partial success yields publishable results that clearly identify remaining barriers to deployment.
 
-We have now established technical feasibility through the methodology (Section 3), defined success metrics (Section 4), and addressed risks with contingency plans (Section 5). The research plan is complete from a technical perspective. Section 6 addresses the remaining Heilmeier questions that establish broader impact: \textbf{Who cares? Why now? What difference will it make?}
+The research plan is now complete from a technical perspective. We have established technical feasibility through the methodology (Section 3), defined success metrics (Section 4), and addressed risks with contingency plans (this section). Section 6 addresses the remaining Heilmeier questions establishing broader impact: \textbf{Who cares? Why now? What difference will it make?}

6-broader-impacts/v1.tex

@@ -1,6 +1,6 @@
 \section{Broader Impacts}
 
-\textbf{Who cares? Why now?} The nuclear industry, datacenter operators, and clean energy advocates all face the same economic constraint: 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?} The nuclear industry, datacenter operators, and clean energy advocates all face the same economic constraint: high operating costs driven by staffing requirements. AI infrastructure demands, growing exponentially, have made this constraint urgent.
 
 Nuclear power presents both a compelling application domain and an urgent
 economic challenge. Recent interest in powering artificial intelligence
@@ -68,10 +68,10 @@ adoption across critical infrastructure.
 
 This section answered three Heilmeier questions:
 
-\textbf{Who cares?} The nuclear industry, datacenter operators, and anyone facing high operating costs from staffing-intensive safety-critical control.
+\textbf{Who cares?} The nuclear industry, datacenter operators, and anyone facing high operating costs from staffing-intensive safety-critical control all care.
 
-\textbf{Why now?} AI infrastructure demands have made nuclear economics urgent. Formal methods tools have matured to the point where compositional hybrid verification is achievable.
+\textbf{Why now?} AI infrastructure demands have made nuclear economics urgent. Formal methods tools have matured to where compositional hybrid verification is now achievable.
 
-\textbf{What difference will it make?} Enabling autonomous control with mathematical safety guarantees addresses a \$21--28 billion annual cost barrier. It also establishes a generalizable framework for safety-critical autonomous systems.
+\textbf{What difference will it make?} Enabling autonomous control with mathematical safety guarantees addresses a \$21--28 billion annual cost barrier while establishing a generalizable framework for safety-critical autonomous systems.
 
-Section 8 addresses the final Heilmeier question: \textbf{How long will it take?} We present a structured 24-month research plan with milestones tied to Technology Readiness Level advancement.
+Section 8 addresses the final Heilmeier question: \textbf{How long will it take?} A structured 24-month research plan progresses through milestones tied to Technology Readiness Level advancement.