Copy edit: multi-level editorial pass

TACTICAL (sentence-level):
- Improved issue-point positioning and topic-stress alignment
- Strengthened verb choices and eliminated weak constructions
- Tightened sentence flow and eliminated redundancies
- Enhanced clarity through better subordination

OPERATIONAL (paragraph/section):
- Improved transitions between paragraphs
- Enhanced coherence within sections
- Streamlined narrative flow
- Better connected ideas across subsections

STRATEGIC (document-level):
- Strengthened Heilmeier catechism alignment throughout
- Made Heilmeier questions more explicit in section summaries
- Improved section linkages and forward/backward references
- Enhanced global coherence of the proposal narrative

1-goals-and-outcomes/research_statement_v1.tex

@@ -1,17 +1,17 @@
 % GOAL PARAGRAPH
-I develop autonomous control systems that guarantee safe and correct behavior through mathematical proof.
+My research develops autonomous control systems with mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
-Nuclear reactors today depend on extensively trained human operators. These operators follow detailed written procedures and switch between control objectives as plant conditions change.
+Nuclear reactors today depend on extensively trained human operators who follow detailed written procedures and switch between control objectives as plant conditions change.
 % Gap
-Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants. This cost disparity threatens economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if safety assurance equals or exceeds that of human operators.
+Small modular reactors face a fundamental economic challenge: per-megawatt staffing costs significantly exceed those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of human operators.
 
 % APPROACH PARAGRAPH Solution
-I produce hybrid control systems that are correct by construction. This work unifies formal methods from computer science with control theory. 
+My approach produces hybrid control systems that are correct by construction, unifying formal methods from computer science with control theory. 
 % Rationale
-Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic but cannot handle continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete switching correctness. End-to-end correctness requires both approaches working together.
+Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic but cannot handle continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete switching correctness. End-to-end correctness requires both.
 % Hypothesis and Technical Approach
-Three stages bridge this gap. First, NASA's Formal Requirements Elicitation Tool (FRET) translates written operating procedures into temporal logic specifications. FRET structures requirements by scope, condition, component, timing, and response. Realizability checking exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata provably correct by construction. Third, reachability analysis verifies that continuous controllers satisfy the requirements each discrete mode imposes. Engineers design these continuous controllers using standard control theory techniques.
+Three stages bridge this gap. First, NASA's Formal Requirements Elicitation Tool (FRET) translates written operating procedures into temporal logic specifications structured by scope, condition, component, timing, and response. Realizability checking exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata provably correct by construction. Third, reachability analysis verifies that continuous controllers satisfy each discrete mode's requirements. Engineers design these continuous controllers using standard control theory techniques.
 
 Control objectives classify continuous modes into three types. Transitory modes drive the plant between conditions. Stabilizing modes maintain operation within regions. Expulsory modes ensure safety under failures. Barrier certificates and assume-guarantee contracts prove mode transitions are safe. This enables local verification without global trajectory analysis. I demonstrate this methodology on an Emerson Ovation control system—the industrial platform nuclear power plants already use.
 % Pay-off

1-goals-and-outcomes/v1.tex

@@ -1,21 +1,21 @@
 \section{Goals and Outcomes}
 
 % GOAL PARAGRAPH
-This research develops autonomous hybrid control systems that guarantee safe and correct behavior through mathematical proof.
+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.
 % Known information
-Nuclear plants today depend on extensively trained human operators. These operators follow detailed written procedures and strict regulatory requirements. They switch between control modes based on plant conditions and procedural guidance.
+Nuclear plants today depend on extensively trained human operators who follow detailed written procedures and strict regulatory requirements, 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. Small modular reactors face per-megawatt staffing costs far exceeding those of conventional plants. This cost disparity threatens economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of human operators.
+This reliance on human operators prevents autonomous control and creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face per-megawatt staffing costs far exceeding those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of human operators.
 
 % APPROACH PARAGRAPH Solution
-This work produces hybrid control systems that are correct by construction. It unifies formal methods with control theory.
+This work produces hybrid control systems that are correct by construction, unifying formal methods with control theory.
 % Rationale
-Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic from written requirements but cannot handle the continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. End-to-end correctness requires both approaches working together.
+Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic from written requirements but cannot handle the continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. End-to-end correctness requires both.
 % Hypothesis
-Two steps close this gap. First, reactive synthesis generates discrete mode transitions directly from written operating procedures. Second, reachability analysis verifies continuous behavior against discrete requirements. This approach transforms operating procedures into logical specifications that constrain continuous dynamics. The result: autonomous controllers provably free from design defects. 
+Two steps close this gap. First, reactive synthesis generates discrete mode transitions directly from written operating procedures. Second, reachability analysis verifies continuous behavior against discrete requirements. This approach transforms operating procedures into logical specifications that constrain continuous dynamics, producing autonomous controllers 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.
 
@@ -64,19 +64,10 @@ If successful, this approach produces three concrete outcomes:
 % IMPACT PARAGRAPH Innovation
 These three outcomes—procedure translation, continuous verification, and hardware demonstration—establish a complete methodology from regulatory documents to deployed systems.
 
-\textbf{What makes this research new?} No existing methodology achieves end-to-end correctness guarantees for hybrid systems. This work unifies discrete synthesis with continuous verification through a key innovation: discrete specifications become contracts that continuous controllers must satisfy. Each layer verifies independently while guaranteeing correct composition. Formal methods verify discrete logic, while control theory verifies continuous dynamics. Section 2 examines why prior work fails at this integration and identifies the limits of current practice. Section 3 details what is new in this approach and why it will succeed.
+\textbf{What makes this research new?} No existing methodology achieves end-to-end correctness guarantees for hybrid systems. This work unifies discrete synthesis with continuous verification through a key innovation: discrete specifications become contracts that continuous controllers must satisfy. Each layer verifies independently while guaranteeing correct composition. Formal methods verify discrete logic, while control theory verifies continuous dynamics.
 
 % Outcome Impact
-If successful, control engineers create autonomous controllers from
-existing procedures with mathematical proofs of correct behavior, making high-assurance
-autonomous control practical for safety-critical applications.
-% Impact/Pay-off
-This capability is essential for the economic viability of next-generation
-nuclear power. Small modular reactors, in particular, offer a promising solution to growing
-energy demands. Their success depends on reducing per-megawatt operating
-costs through increased autonomy. My research provides the tools to
-achieve that autonomy while maintaining the exceptional safety record the
-nuclear industry requires. 
+If successful, control engineers will create autonomous controllers from existing procedures with mathematical proofs of correct behavior, making high-assurance autonomous control practical for safety-critical applications. This capability is essential for the economic viability of next-generation nuclear power. Small modular reactors, in particular, offer a promising solution to growing energy demands, but their success depends on reducing per-megawatt operating costs through increased autonomy. This research provides the tools to achieve that autonomy while maintaining the exceptional safety record the nuclear industry requires. 
 
 This proposal follows the Heilmeier Catechism. Each section explicitly answers its assigned questions:
 \begin{itemize}

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

@@ -2,7 +2,7 @@
 
 \textbf{Heilmeier Questions: What has been done? What are the limits of current practice?} 
 
-No current approach provides autonomous control with end-to-end correctness guarantees. This section examines why. Human-centered operation cannot eliminate reliability limits. Formal methods verify discrete or continuous behavior but never both. 
+No current approach provides autonomous control with end-to-end correctness guarantees. Human-centered operation cannot eliminate reliability limits. Formal methods verify discrete or continuous behavior but never both. 
 
 Three subsections structure this analysis. First: reactor operators and their operating procedures. Second: fundamental limitations of human-based operation. Third: formal methods approaches that verify discrete logic or continuous dynamics but not both together.
 
@@ -14,7 +14,7 @@ Current practice rests on two critical components: procedures and operators. Thi
 
 Nuclear plant procedures form a strict hierarchy. Normal operating procedures govern routine operations. Abnormal operating procedures handle off-normal conditions. Emergency Operating Procedures (EOPs) manage design-basis accidents. Severe Accident Management Guidelines (SAMGs) address beyond-design-basis events. Extensive Damage Mitigation Guidelines (EDMGs) cover catastrophic damage. All 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. 10 CFR 55.59~\cite{10CFR55.59} requires rigorous assessment through technical evaluation, simulator validation testing, and biennial review. Yet key safety properties escape formal verification. No mathematical proofs confirm that procedures cover all possible plant states, that required actions complete within available timeframes, or that transitions between procedure sets maintain safety invariants.
+Procedure development relies on expert judgment and simulator validation—not formal verification. 10 CFR 55.59~\cite{10CFR55.59} requires rigorous assessment through technical evaluation, simulator validation testing, and biennial review, yet key safety properties escape formal verification. No mathematical proofs confirm 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.} No proof exists that procedures cover all
@@ -30,9 +30,9 @@ This division between automated and human-controlled functions reveals the funda
 
 \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. Perfect procedures cannot guarantee safe operation when humans execute them imperfectly.
+The previous subsection established that procedures lack formal verification despite rigorous development—only half the reliability challenge. 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. Operators determine when and how to act. This human discretion introduces persistent failure modes that training alone cannot eliminate.
+Human operators—the second pillar of current practice—introduce reliability limitations independent of procedure quality. While procedures define what to do, operators determine when and how to act. This discretion introduces persistent failure modes that training alone cannot eliminate.
 
 Current-generation nuclear power plants employ over 3,600 active NRC-licensed
 reactor operators in the United States~\cite{operator_statistics}. These
@@ -60,7 +60,7 @@ limitations are fundamental to human-driven control, not remediable defects.
 
 The previous two subsections established two fundamental limitations: procedures lack formal verification, and human operators introduce persistent reliability issues that training cannot eliminate. Both represent fundamental constraints, not remediable defects.
 
-Formal methods could potentially eliminate both limitations by providing mathematical guarantees of correctness. However, even the most advanced formal methods applications in nuclear control leave a critical verification gap.
+Formal methods could eliminate both limitations by providing mathematical guarantees of correctness. However, even the most advanced formal methods applications in nuclear control leave a critical verification gap.
 
 This subsection examines two approaches illustrating this gap. HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic handles hybrid verification only post-hoc. Each demonstrates the current state of formal methods while revealing the verification gap this research addresses.
 
@@ -155,10 +155,10 @@ design loop for complex systems like nuclear reactor startup procedures.
 
 This section answered two Heilmeier questions: What has been done? What are the limits of current practice?
 
-\textbf{What has been done?} Three approaches currently exist. Human operators provide operational flexibility but introduce persistent reliability limitations. HARDENS verified discrete logic but omitted continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis. Each approach has fundamental limitations. None addresses both discrete and continuous verification compositionally.
+\textbf{What has been done?} Three approaches currently exist, each with fundamental limitations. Human operators provide operational flexibility but introduce persistent reliability limitations. HARDENS verified discrete logic but omitted continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis. None addresses both discrete and continuous verification compositionally.
 
-\textbf{What are the limits of current practice?} The verification gap emerges clearly. No existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into design. Current approaches verify discrete logic or continuous dynamics but never both compositionally. Training improvements cannot overcome human reliability limits. Post-hoc verification cannot scale to system design.
+\textbf{What are the limits of current practice?} The verification gap emerges clearly: no existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into design. Current approaches verify discrete logic or continuous dynamics but never both compositionally. Training improvements cannot overcome human reliability limits, and post-hoc verification cannot scale to system design.
 
-Two forces create urgency. Economic necessity demands solutions: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Technical maturity enables solutions: formal methods tools have matured to enable compositional hybrid verification.
+\textbf{Why now?} Two forces create urgency. Economic necessity demands solutions—small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Technical maturity enables solutions—formal methods tools have matured to enable compositional hybrid verification.
 
-Section 3 closes this verification gap. It establishes what is new and why the approach will succeed.
+Section 3 closes this verification gap by establishing what is new and why the approach will succeed.

3-research-approach/v3.tex

@@ -4,9 +4,9 @@
 
 This section presents the complete technical approach for synthesizing provably correct hybrid controllers from operating procedures. 
 
-\textbf{What is new:} Compositional verification bridges discrete synthesis with continuous control. Three innovations enable this integration: contract-based decomposition, mode classification, and procedure-driven structure. 
+\textbf{What is new:} Compositional verification bridges discrete synthesis with continuous control through three innovations: contract-based decomposition, mode classification, and procedure-driven structure. 
 
-\textbf{Why it will succeed:} The approach leverages existing procedural structure. It bounds computational complexity through mode-level verification. It validates against real industrial hardware through the Emerson collaboration.
+\textbf{Why it will succeed:} The approach leverages existing procedural structure, bounds computational complexity through mode-level verification, and validates against real industrial hardware through the Emerson collaboration.
 
 % ============================================================================
 % STRUCTURE (maps to Thesis.RA tasks):
@@ -23,13 +23,13 @@ This section presents the complete technical approach for synthesizing provably
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches verified discrete switching logic or continuous control behavior but never both simultaneously. Engineers validate continuous controllers through extensive simulation trials. They test discrete switching logic through simulated control room testing and human factors research. Neither method provides rigorous guarantees. Both consume enormous resources.
+Previous approaches verified discrete switching logic or continuous control behavior but 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. Neither method provides rigorous guarantees, and both consume enormous resources.
 
-This approach bridges that gap. It composes formal methods from computer science with control-theoretic verification. Reactor operations are formalized as hybrid automata.
+This approach bridges that gap by composing formal methods from computer science with control-theoretic verification. Reactor operations are formalized as hybrid automata.
 
-Hybrid system verification faces a fundamental challenge: discrete transitions change the governing vector field, creating discontinuities through the interaction between discrete and continuous dynamics. Traditional verification techniques cannot handle this interaction directly.
+Hybrid system verification faces a fundamental challenge: discrete transitions change the governing vector field, creating discontinuities that traditional verification techniques cannot handle directly.
 
-This 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. Continuous controllers govern plant behavior within each mode.
+This 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.
 
 Hybrid systems require mathematical formalization. This work draws on automata theory, temporal logic, and control theory to provide that description.
 
@@ -144,7 +144,7 @@ These factors combine to demonstrate feasibility on production control systems w
 
 The previous subsection established the hybrid automaton formalism—a mathematical framework describing discrete modes, continuous dynamics, guards, and invariants. A critical question remains: where do these formal descriptions originate?
 
-The answer lies in existing practice. Nuclear operations already possess a natural hybrid structure. This structure maps directly to the automaton formalism through three control scopes: strategic, operational, and tactical. This approach constructs formal hybrid systems from existing operational knowledge rather than imposing artificial abstractions. It leverages decades of domain expertise already encoded in operating procedures.
+Nuclear operations already possess a natural hybrid structure that maps directly to the automaton formalism through three control scopes: strategic, operational, and tactical. This approach constructs formal hybrid systems from existing operational knowledge rather than imposing artificial abstractions, leveraging decades of domain expertise already encoded in operating procedures.
 
 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.
 
@@ -190,9 +190,9 @@ This structure reveals why the operational and tactical levels fundamentally for
 \end{figure}
 
 
-This operational control level explains why nuclear control requires human operators: the hybrid nature of this control system makes proving controller performance against strategic requirements difficult, and no unified infrastructure exists for building and verifying hybrid systems. Humans fill this layer because their general intelligence provides a safe way to manage the system's hybrid nature by 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.
+This operational control level explains why nuclear control requires human operators: the hybrid nature of this control system makes proving controller performance against strategic requirements difficult, and no unified infrastructure exists for building and verifying hybrid systems. Humans fill this layer because their general intelligence provides a safe way to manage the system's hybrid nature by following prescriptive operating manuals where strict procedures govern what control to implement at any given time.
 
-A HAHACS construction 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
+These procedures provide the key to HAHACS construction, which leverages two observations about current practice. First, operational scope control is effectively discrete control. Second, operating procedures describe implementation rules before construction begins, meaning a HAHACS's intended behavior can be completely specified before implementation. 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
@@ -528,25 +528,23 @@ This section answered two critical Heilmeier questions: What is new? Why will it
 
 \textbf{What is new in this research?} This work integrates reactive synthesis, reachability analysis, and barrier certificates into a compositional methodology for hybrid control synthesis through three innovations: 
 
-\textit{First: contract-based decomposition} inverts traditional global analysis. Discrete synthesis defines verification contracts that bound continuous verification. 
+\textit{Contract-based decomposition} inverts traditional global analysis. Discrete synthesis defines verification contracts that bound continuous verification. 
 
-\textit{Second: mode classification} enables mode-local analysis with provable composition guarantees by matching continuous modes to appropriate verification tools. 
+\textit{Mode classification} enables mode-local analysis with provable composition guarantees by matching continuous modes to appropriate verification tools. 
 
-\textit{Third: procedure-driven structure} leverages existing procedural decomposition, avoiding intractable state explosion.
+\textit{Procedure-driven structure} leverages existing procedural decomposition, avoiding intractable state explosion.
 
 Section 2 established that prior work verified discrete logic or continuous dynamics but never both compositionally. This compositional verification enables what global analysis cannot achieve.
 
 \textbf{Why will this approach succeed?} Three factors ensure practical feasibility: 
 
-\textit{First: existing structure.} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria, allowing formalization of existing structure without imposing artificial abstractions. 
+\textit{Existing structure.} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria, allowing formalization of existing structure without imposing artificial abstractions. 
 
-\textit{Second: bounded complexity.} Mode-level verification bounds each verification problem locally, avoiding the state explosion that makes global hybrid system analysis intractable. 
+\textit{Bounded complexity.} Mode-level verification bounds each verification problem locally, avoiding the state explosion that makes global hybrid system analysis intractable. 
 
-\textit{Third: industrial validation.} The Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility, ensuring solutions address real deployment constraints.
+\textit{Industrial validation.} The Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility, ensuring solutions address real deployment constraints.
 
-The complete technical methodology is now established. Section 2 answered what has been done and what limits current practice. This section answered what is new and why it will succeed.
-
-Three critical questions remain. Section 4 addresses measurement: \textit{How will success be measured?} Section 5 addresses risks: \textit{What could prevent success?} Section 6 addresses impact: \textit{Who cares? Why now? What difference will it make?}
+The complete technical methodology is now established. Section 2 answered what has been done and what limits current practice. This section answered what is new and why it will succeed. Three critical questions remain. Section 4 addresses measurement (\textit{How will success be measured?}), Section 5 addresses risks (\textit{What could prevent success?}), and Section 6 addresses impact (\textit{Who cares? Why now? What difference will it make?}).
 
 %%% NOTES (Section 5):
 % - Get specific details on ARCADE interface from Emerson collaboration

4-metrics-of-success/v1.tex

@@ -2,11 +2,9 @@
 
 \textbf{Heilmeier Question: How do we measure success?}
 
-Section 3 established the technical approach. It answered what is new: compositional verification bridging discrete synthesis with continuous control. It answered why the approach will succeed: existing procedural structure, bounded complexity, and industrial validation. This section addresses the next Heilmeier question: how to measure success. 
+Section 3 established the technical approach, answering what is new (compositional verification bridging discrete synthesis with continuous control) and why it will succeed (existing procedural structure, bounded complexity, and industrial validation). This section addresses the next Heilmeier question: how to measure success. 
 
-Success is measured by Technology Readiness Level advancement. The work advances from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5).
-
-This work begins at TRL 2--3 and targets TRL 5. At TRL 5, system components operate successfully in a relevant laboratory environment. TRL advancement provides the most appropriate success metric. It explicitly measures the gap between academic proof-of-concept and practical deployment. This section explains why TRLs measure success appropriately, then defines specific criteria for each level from TRL 3 through TRL 5.
+Success is measured by Technology Readiness Level advancement from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5). At TRL 5, system components operate successfully in a relevant laboratory environment. TRL advancement provides the most appropriate success metric because it explicitly measures the gap between academic proof-of-concept and practical deployment. This section explains why TRLs measure success appropriately, then defines specific criteria for each level from TRL 3 through TRL 5.
 
 Technology Readiness Levels provide the ideal success metric for work that bridges the gap between academic proof-of-concept and practical deployment. 
 

5-risks-and-contingencies/v1.tex

@@ -2,9 +2,9 @@
 
 \textbf{Heilmeier Question: What could prevent success?}
 
-Section 4 defined success as reaching TRL 5. The path requires component validation, system integration, and hardware demonstration. That definition assumes critical technical challenges can be overcome.
+Section 4 defined success as reaching TRL 5 through component validation, system integration, and hardware demonstration. That definition assumes critical technical challenges can be overcome.
 
-Every research plan rests on assumptions that might prove false. This section identifies three primary risks that could prevent reaching TRL 5. First: computational tractability of synthesis and verification. Second: complexity of the discrete-continuous interface. Third: completeness of procedure formalization. 
+Every research plan rests on assumptions that might prove false. This section identifies three primary risks that could prevent reaching TRL 5: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, and completeness of procedure formalization. 
 
 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 and clearly identifies remaining barriers to deployment even when full success proves elusive.
 

6-broader-impacts/v1.tex

@@ -2,15 +2,15 @@
 
 \textbf{Heilmeier Questions: Who cares? Why now? What difference will it make?}
 
-Sections 2--5 established the complete technical research plan. Section 2 answered what has been done. Section 3 answered what is new and why it will succeed. Section 4 answered how to measure success. Section 5 answered what could prevent success.
+Sections 2--5 established the complete technical research plan: what has been done (Section 2), what is new and why it will succeed (Section 3), how to measure success (Section 4), and what could prevent success (Section 5).
 
-This section addresses the remaining Heilmeier questions. It connects technical methodology to economic and societal impact: who cares, why now, and what difference this work will make.
+This section addresses the remaining Heilmeier questions, connecting technical methodology to economic and societal impact: who cares, why now, and what difference this work will make.
 
-Three stakeholder groups converge on one 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.
+\textbf{Who cares?} Three stakeholder groups converge on one 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.
 
-This research directly addresses a \$21--28 billion annual cost barrier by enabling economically viable small modular reactors for datacenter power and establishing a generalizable framework for safety-critical autonomous systems across critical infrastructure.
+\textbf{What difference will it make?} This research directly addresses a \$21--28 billion annual cost barrier by enabling economically viable small modular reactors for datacenter power and establishing a generalizable framework for safety-critical autonomous systems across critical infrastructure.
 
-Why now? Exponentially growing AI infrastructure demands have transformed this longstanding challenge into an immediate crisis, creating a market demanding solutions that did not exist before.
+\textbf{Why now?} Exponentially growing AI infrastructure demands have transformed this longstanding challenge into an immediate crisis, creating a market demanding 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. At this scale, nuclear power economics demand careful attention to operating costs.
 
@@ -60,28 +60,12 @@ establish both the technical feasibility and regulatory pathway for broader
 adoption across critical infrastructure.
 
 
-This section answered three critical Heilmeier questions: Who cares? Why now? What difference will it make?
+This section answered three critical Heilmeier questions:
 
-\textbf{Who cares?} Three stakeholder groups face the same constraint: 
+\textbf{Who cares?} Three stakeholder groups face the same constraint. The nuclear industry faces an economic crisis for small modular reactors due to per-megawatt staffing costs. Datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure. Clean energy advocates need nuclear power to be economically competitive. All three require autonomous control with safety guarantees.
 
-The nuclear industry faces an economic crisis for small modular reactors due to per-megawatt staffing costs. 
+\textbf{Why now?} Two forces converge to create urgency. \textit{First: exponentially growing demand.} AI infrastructure demands create immediate need for economical nuclear power at datacenter scale, with projections showing datacenter electricity demand reaching 1,050 terawatt-hours annually by 2030. \textit{Second: technical maturity.} Formal methods tools have matured sufficiently to make compositional hybrid verification computationally achievable. What was theoretically possible but practically intractable a decade ago is now feasible. The problem is urgent, and the tools exist.
 
-Datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure. 
+\textbf{What difference will it make?} This research addresses a \$21--28 billion annual cost barrier and enables autonomous control with mathematical safety guarantees. Beyond immediate economic impact, the methodology establishes a generalizable framework for safety-critical autonomous systems across critical infrastructure, extending beyond nuclear power to any safety-critical system requiring provable correctness.
 
-Clean energy advocates need nuclear power to be economically competitive. 
-
-All three groups require autonomous control with safety guarantees.
-
-\textbf{Why now?} Two forces converge to create urgency: 
-
-\textit{First: exponentially growing demand.} AI infrastructure demands create immediate need for economical nuclear power at datacenter scale. Projections show datacenter electricity demand reaching 1,050 terawatt-hours annually by 2030. 
-
-\textit{Second: technical maturity.} Formal methods tools have matured sufficiently to make compositional hybrid verification computationally achievable. What was theoretically possible but practically intractable a decade ago is now feasible. 
-
-The problem is urgent. The tools exist.
-
-\textbf{What difference will it make?} This research addresses a \$21--28 billion annual cost barrier and enables autonomous control with mathematical safety guarantees. Beyond immediate economic impact, the methodology establishes a generalizable framework for safety-critical autonomous systems across critical infrastructure. Impact extends beyond nuclear power to any safety-critical system requiring provable correctness.
-
-The complete research plan spans technical approach, success metrics, risk mitigation, and broader impact. One final Heilmeier question remains: How long will it take?
-
-Section 8 provides a structured 24-month research plan progressing through milestones tied to Technology Readiness Level advancement, demonstrating the proposed work is achievable within a doctoral timeline.
+The complete research plan now spans technical approach (Section 3), success metrics (Section 4), risk mitigation (Section 5), and broader impact (this section). One final Heilmeier question remains: \textit{How long will it take?} Section 8 provides a structured 24-month research plan progressing through milestones tied to Technology Readiness Level advancement, demonstrating the proposed work is achievable within a doctoral timeline.

8-schedule/v1.tex

@@ -2,7 +2,7 @@
 
 \textbf{Heilmeier Question: How long will it take?}
 
-The complete research plan is now established. Section 6 demonstrated that this work addresses a \$21--28 billion annual cost barrier and establishes a generalizable framework for safety-critical autonomous systems. The final Heilmeier question addresses timing and feasibility within a doctoral timeline.
+Section 6 demonstrated that this work addresses a \$21--28 billion annual cost barrier and establishes a generalizable framework for safety-critical autonomous systems. This final Heilmeier question addresses timing and feasibility within a doctoral timeline.
 
 This research will be conducted over six trimesters (24 months) of full-time effort following the proposal defense in Spring 2026. The University of Pittsburgh Cyber Energy Center and NRC Fellowship provide all computational and experimental resources. The work progresses sequentially through three main research thrusts, culminating in integrated demonstration and validation.