Copy-edit: multi-level editorial pass

TACTICAL (sentence-level):
- Applied Gopen's issue-point and topic-stress positioning
- Strengthened verb choices (active voice preferred)
- Improved clarity and directness
- Removed unnecessary passive constructions
- Tightened wordy phrases

OPERATIONAL (paragraph/section):
- Improved transitions between paragraphs and sections
- Enhanced flow within sections
- Added paragraph breaks for clarity
- Moved supporting evidence closer to main claims

STRATEGIC (document-level):
- Strengthened Heilmeier question framing throughout
- Improved consistency in section summaries
- Enhanced forward/backward references between sections
- Clarified parallel structure in lists and explanations

1-goals-and-outcomes/research_statement_v1.tex

@@ -2,18 +2,18 @@
 This research develops autonomous control systems with mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
-Human operators control today's nuclear reactors through extensive training, following detailed written procedures and switching between control objectives based on plant conditions.
+Today's nuclear reactors depend on human operators who control them through extensive training, following detailed written procedures and switching between control objectives based on plant conditions.
 % Gap
-Small modular reactors face a fundamental economic challenge: per-megawatt staffing costs significantly exceed those of conventional plants, threatening economic viability. Autonomous control systems could manage complex operational sequences without constant supervision—but only if they provide assurance equal to or exceeding that of human-operated systems.
+Small modular reactors face a fundamental economic challenge: per-megawatt staffing costs significantly exceed those of conventional plants, threatening economic viability. Autonomous control systems could manage complex operational sequences without constant supervision—but only if they provide assurance equal to or exceeding human-operated systems.
 
 % APPROACH PARAGRAPH Solution
-This research combines formal methods from computer science with control theory to produce hybrid control systems that are correct by construction. 
+This research combines formal methods from computer science with control theory to produce hybrid control systems correct by construction. 
 % Rationale
-Human operators already work this way: discrete logic switches between continuous control modes. Formal methods can generate provably correct switching logic but fail when continuous dynamics govern transitions. Control theory can verify continuous behavior but cannot prove discrete switching correctness. Both approaches must work together to achieve end-to-end correctness.
+Human operators already work this way: discrete logic switches between continuous control modes. 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. Both approaches must work together to achieve end-to-end correctness.
 % 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, structuring requirements by scope, condition, component, timing, and response. Realizability checking then exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata that are provably correct by construction. Third, reachability analysis verifies that continuous controllers—designed using standard control theory—satisfy the requirements that each discrete mode imposes.
 
-Continuous modes classify by control objective. 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 safe mode transitions, enabling local verification without global trajectory analysis. The methodology demonstrates on an Emerson Ovation control system. 
+Continuous modes classify by control objective. 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 safe mode transitions, enabling local verification without global trajectory analysis. The methodology will demonstrate on an Emerson Ovation control system. 
 % Pay-off
 This approach manages complex nuclear power operations autonomously while maintaining safety guarantees, directly addressing the economic constraints that threaten small modular reactor viability.
 

1-goals-and-outcomes/v1.tex

@@ -6,14 +6,14 @@ This research develops autonomous hybrid control systems with mathematical guara
 % 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
-Human operators control today's nuclear plants through extensive training, following detailed written procedures and strict regulatory requirements while switching between control modes based on plant conditions and procedural guidance.
+Today's nuclear plants depend on human operators who control them through extensive training, following detailed written procedures and strict regulatory requirements while switching between control modes based on plant conditions and procedural guidance.
 % Gap
 This reliance on human operators prevents autonomous control 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 that are correct by construction.
+This research combines formal methods with control theory to produce hybrid control systems correct by construction.
 % Rationale
-Human operators already work this way: discrete logic switches between continuous control modes. Formal methods can generate provably correct switching logic from written requirements, but they fail when continuous dynamics govern transitions. Control theory can verify continuous behavior but cannot prove discrete switching correctness. Both approaches must work together to achieve end-to-end correctness.
+Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic from written requirements, but they fail when continuous dynamics govern transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Both approaches must work together to achieve end-to-end correctness.
 % 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 that constrain continuous dynamics. The result: autonomous controllers provably free from design defects. 
 
@@ -65,7 +65,7 @@ This approach produces three concrete outcomes:
 % IMPACT PARAGRAPH Innovation
 These three outcomes—procedure translation, continuous verification, and hardware demonstration—establish a complete methodology from regulatory documents to deployed systems.
 
-\textbf{What makes this research new?} This work unifies discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems—no existing methodology achieves this. The key innovation: treating discrete specifications as contracts that continuous controllers must satisfy. This allows each layer to verify independently while guaranteeing correct composition. Formal methods verify discrete logic. Control theory verifies continuous dynamics. No existing methodology bridges both with compositional guarantees. Section 2 (State of the Art) examines why prior work has not achieved this integration. Section 3 (Research Approach) details how this integration will be accomplished.
+\textbf{What makes this research new?} This work unifies discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems—no existing methodology achieves this. The key innovation: treating discrete specifications as contracts that continuous controllers must satisfy, allowing each layer to verify independently while guaranteeing correct composition. Formal methods verify discrete logic. Control theory verifies continuous dynamics. No existing methodology bridges both with compositional guarantees. Section 2 examines why prior work has not achieved this integration. Section 3 details how this integration will be accomplished.
 
 % Outcome Impact
 If successful, control engineers create autonomous controllers from

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

@@ -8,7 +8,7 @@ Understanding the limits of current practice requires first examining how nuclea
 
 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. 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 safety invariants hold across procedure-set transitions.
+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.} Current procedure development relies on expert judgment and
@@ -25,7 +25,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. 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. This human determination introduces persistent failure modes that training alone cannot eliminate.
+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. This human determination 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
@@ -38,7 +40,7 @@ operator requires several years of training.
 Despite decades of improvements in training and procedures, human error persistently contributes to nuclear safety incidents—a persistence that motivates formal automated control with mathematical safety guarantees. Under 10 CFR Part 55, operators hold legal authority to make critical decisions, including authority to depart from normal regulations during emergencies. The Three Mile Island (TMI) accident demonstrated how personnel error, design deficiencies, and component failures combine to cause disaster: operators misread confusing and contradictory indications, then shut off the emergency water system~\cite{Kemeny1979}. The President's Commission on TMI identified a
 fundamental ambiguity: placing responsibility for safe power plant operations on
 the licensee without formally verifying that operators can fulfill this
-responsibility does not guarantee safety. This tension between operational
+responsibility guarantees nothing. This tension between operational
 flexibility and safety assurance remains unresolved. The person responsible for
 reactor safety often becomes the root cause of failure.
 
@@ -116,7 +118,9 @@ primary assurance evidence.
 
 \subsubsection{Differential Dynamic Logic: Post-Hoc Hybrid Verification}
 
-HARDENS verified discrete control logic without continuous dynamics—leaving half the hybrid system unverified. Other researchers attacked the problem from the opposite direction: extending temporal logics to handle hybrid systems directly. This complementary approach produced differential dynamic logic (dL), which addresses continuous dynamics but encounters different limitations. dL introduces two additional operators
+HARDENS verified discrete control logic without continuous dynamics—leaving half the hybrid system unverified. Other researchers attacked the problem from the opposite direction: extending temporal logics to handle hybrid systems directly. This complementary approach produced differential dynamic logic (dL). 
+
+While dL addresses continuous dynamics, it encounters different limitations. 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
@@ -149,10 +153,10 @@ design loop for complex systems like nuclear reactor startup procedures.
 
 \subsection{Summary: The Verification Gap}
 
-This section answered two Heilmeier questions about current practice.
+This section answered two Heilmeier questions:
 
 \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. No existing approach addresses both discrete and continuous verification compositionally.
 
 \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. Training improvements cannot overcome human reliability limits. Post-hoc verification cannot scale to system design.
 
-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.
+Two imperatives converge to make this gap urgent. First, economic necessity: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Second, 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.

3-research-approach/v3.tex

@@ -15,13 +15,13 @@
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches verified either discrete switching logic or continuous control behavior—never both simultaneously. Engineers validate continuous controllers through extensive simulation trials. They test discrete switching logic through simulated control room testing and human factors research. 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. They test discrete switching logic through simulated control room testing and human factors research. Neither method provides rigorous guarantees despite consuming enormous resources.
 
-This work bridges the gap by composing formal methods from computer science with control-theoretic verification, formalizing reactor operations as hybrid automata.
+This work bridges that 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, creating 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 cannot handle this interaction directly.
 
-Our methodology decomposes this 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; continuous controllers govern plant behavior within each mode.
 
 A high-assurance hybrid autonomous control system requires a mathematical description. 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:
 
@@ -222,7 +222,7 @@ eventually reaches operating temperature''), and response properties (``if
 coolant pressure drops, the system initiates shutdown within bounded time'').
 
 
-This work uses FRET (Formal Requirements Elicitation Tool)—developed by NASA for high-assurance timed systems—to build these temporal logic statements. FRET provides an intermediate language between temporal logic and natural language, enabling rigid definitions of temporal behavior through syntax accessible to engineers without formal methods expertise. This accessibility proves crucial for industrial feasibility by making these tools adoptable by the current nuclear workforce without requiring extensive formal methods training.
+This work uses FRET (Formal Requirements Elicitation Tool)—developed by NASA for high-assurance timed systems—to build these temporal logic statements. FRET provides an intermediate language between temporal logic and natural language, enabling rigid definitions of temporal behavior through syntax accessible to engineers without formal methods expertise. This accessibility proves crucial for industrial feasibility: the current nuclear workforce can adopt these tools without extensive formal methods training.
 
 FRET's key feature is its ability to start with logically imprecise
 statements and refine them consecutively into well-posed specifications. We
@@ -259,10 +259,10 @@ This shift carries two critical implications. First, complete traceability: the
 
 The synthesized automaton translates directly to executable code through standard compilation techniques. Each discrete state maps to a control mode, guard conditions map to conditional statements, and the transition function defines the control flow. This compilation process preserves the formal guarantees by ensuring the implemented code is correct by construction—the automaton from which it derives was synthesized to satisfy the temporal logic specifications.
 
-Having established how discrete mode-switching logic synthesizes from procedures, the question becomes: what executes within each discrete mode? The next subsection addresses continuous control modes and their verification.
-
 Reactive synthesis has proven successful in robotics, avionics, and industrial control. Recent applications include synthesizing robot motion planners from natural language specifications, generating flight control software for unmanned aerial vehicles, and creating verified controllers for automotive systems. These successes demonstrate that reactive synthesis scales beyond toy problems to real-world safety-critical applications.
 
+Having established how discrete mode-switching logic synthesizes from procedures, the question becomes: what executes within each discrete mode? The next subsection addresses continuous control modes and their verification. Recent applications include synthesizing robot motion planners from natural language specifications, generating flight control software for unmanned aerial vehicles, and creating verified controllers for automotive systems. These successes demonstrate that reactive synthesis scales beyond toy problems to real-world safety-critical applications.
+
 %%% NOTES (Section 3):
 % - Mention computational complexity of synthesis (doubly exponential worst case)
 % - Discuss how specification structure affects synthesis tractability
@@ -279,7 +279,7 @@ The previous subsection established that reactive synthesis produces a provably
 
 This subsection describes the continuous control modes executing within each discrete state and explains how they verify against requirements imposed by the discrete layer. Control objectives determine the verification approach: modes classify into three types—transitory, stabilizing, and expulsory—each requiring different verification tools matched to their distinct purposes. 
 
-This methodology's scope requires clarification: this work verifies continuous controllers but does not synthesize them. The distinction parallels model checking in software verification, where verification confirms whether a given implementation satisfies its specification without prescribing how to write the software. Engineers design continuous controllers using standard control theory techniques—this work assumes that design capability exists. The contribution lies in the verification framework that confirms candidate controllers compose correctly with the discrete layer to produce a safe hybrid system.
+This methodology's scope requires clarification: this work verifies continuous controllers but does not synthesize them. The distinction parallels model checking in software verification. Model checking confirms whether a given implementation satisfies its specification without prescribing how to write the software. Engineers design continuous controllers using standard control theory techniques—this work assumes that design capability exists. The contribution lies in the verification framework that confirms candidate controllers compose correctly with the discrete layer to produce a safe hybrid system.
 
 The operational control scope defines go/no-go decisions that determine what
 kind of continuous control to implement. The entry or exit conditions of a
@@ -332,13 +332,12 @@ Continuous controllers classify into three types based on their control objectiv
 
 Transitory modes—the first of three continuous controller types—execute transitions between operating conditions. Their purpose is to move the plant from one discrete operating condition to another: start from entry conditions, reach exit conditions, and maintain safety invariants throughout. Examples include power ramp-up sequences, cooldown procedures, and load-following maneuvers.
 
-We can state the control objective for a transitory mode formally. Given entry conditions $\mathcal{X}_{entry}$, exit conditions $\mathcal{X}_{exit}$, safety invariant $\mathcal{X}_{safe}$, and closed-loop dynamics $\dot{x} = f(x, u(x))$, the controller must satisfy:
+The control objective for a transitory mode has a formal statement. Given entry conditions $\mathcal{X}_{entry}$, exit conditions $\mathcal{X}_{exit}$, safety invariant $\mathcal{X}_{safe}$, and closed-loop dynamics $\dot{x} = f(x, u(x))$, the controller must satisfy:
 \[
 \forall x_0 \in \mathcal{X}_{entry}: \exists T > 0: x(T) \in \mathcal{X}_{exit}
 \land \forall t \in [0,T]: x(t) \in \mathcal{X}_{safe}
 \]
-From any valid entry state, the trajectory must eventually reach the
-exit condition without ever leaving the safe region.
+This requirement is straightforward: from any valid entry state, the trajectory must eventually reach the exit condition without ever leaving the safe region.
 
 Reachability analysis provides the natural verification tool for transitory modes.
 It computes the set of all states reachable from a given
@@ -514,15 +513,13 @@ of transferring technology directly to industry with a direct collaboration in
 this research, while getting an excellent perspective of how our research
 outcomes can align best with customer needs.
 
-This section answered two critical Heilmeier questions about the research approach:
+This section answered two critical Heilmeier questions:
 
-\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. Three innovations enable this integration: contract-based decomposition (using discrete synthesis to define verification contracts that bound continuous verification, inverting traditional global analysis), mode classification (classifying continuous modes by objective to select appropriate verification tools, enabling mode-local analysis with provable composition guarantees), and procedure-driven structure (leveraging existing procedural structure to avoid intractable state explosion). Section 2 established that prior work verified either discrete logic or continuous dynamics—never both compositionally. Compositional verification enables what global analysis cannot achieve.
+\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. Three innovations enable this integration. First, contract-based decomposition uses discrete synthesis to define verification contracts that bound continuous verification, inverting traditional global analysis. Second, mode classification classifies continuous modes by objective to select appropriate verification tools, enabling mode-local analysis with provable composition guarantees. Third, procedure-driven structure leverages existing procedural structure to avoid intractable state explosion. Section 2 established that prior work verified either discrete logic or continuous dynamics—never both compositionally. Compositional verification enables what global analysis cannot achieve.
 
-\textbf{Why will this approach succeed?} Three factors ensure practical feasibility: nuclear procedures already decompose operations into discrete phases with explicit transition criteria (allowing the approach to formalize existing structure rather than impose artificial abstractions), mode-level verification bounds each verification problem locally (avoiding the state explosion that makes global hybrid system analysis intractable), and the Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility—ensuring solutions address real deployment constraints, not just theoretical correctness.
+\textbf{Why will this approach succeed?} Three factors ensure practical feasibility. First, nuclear procedures already decompose operations into discrete phases with explicit transition criteria, allowing the approach to formalize existing structure rather than impose artificial abstractions. Second, mode-level verification bounds each verification problem locally, avoiding the state explosion that makes global hybrid system analysis intractable. Third, the Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility, ensuring solutions address real deployment constraints, not just theoretical correctness.
 
-The methodology is now complete: procedure formalization, discrete synthesis, continuous verification across three mode types, and hardware implementation. What remains are operational questions about executing this research plan.
-
-Section 4 addresses \textit{How will success be measured?} through Technology Readiness Level advancement. Section 5 addresses \textit{What could prevent success?} through risk analysis and contingency planning. Section 6 addresses \textit{Who cares? Why now? What difference will it make?} through economic and societal impact analysis.
+The methodology is now complete: procedure formalization, discrete synthesis, continuous verification across three mode types, and hardware implementation. What remains are operational questions about executing this research plan. Section 4 addresses \textit{How will success be measured?} through Technology Readiness Level advancement. Section 5 addresses \textit{What could prevent success?} through risk analysis and contingency planning. Section 6 addresses \textit{Who cares? Why now? What difference will it make?} through economic and societal impact analysis.
 
 %%% NOTES (Section 5):
 % - Get specific details on ARCADE interface from Emerson collaboration

4-metrics-of-success/v1.tex

@@ -2,7 +2,7 @@
 
 \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 explicitly measuring the gap between academic proof-of-concept and practical deployment. This section explains why TRLs are the right metric, then defines specific criteria for each level from TRL 3 through TRL 5.
+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: it explicitly measures the gap between academic proof-of-concept and practical deployment. This section explains why TRLs are the right metric, then defines specific criteria for each level from TRL 3 through TRL 5.
 
 Technology Readiness Levels provide the ideal success metric 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. TRLs measure both simultaneously.
 

5-risks-and-contingencies/v1.tex

@@ -4,7 +4,7 @@
 
 \subsection{Computational Tractability of Synthesis}
 
-Computational tractability represents the first major risk. The assumption: formalized startup procedures will yield automata small enough for efficient synthesis and verification. This assumption may fail. Reactive synthesis scales exponentially with specification complexity. Temporal logic specifications derived from complete startup procedures may produce automata with thousands of states, requiring synthesis times exceeding days or weeks—preventing completion of the methodology within project timelines. Reachability analysis for continuous modes with high-dimensional state spaces may similarly prove computationally intractable. Either barrier would constitute a fundamental obstacle to achieving research objectives.
+Computational tractability represents the first major risk. The assumption: formalized startup procedures will yield automata small enough for efficient synthesis and verification. This assumption may fail. Reactive synthesis scales exponentially with specification complexity. Temporal logic specifications derived from complete startup procedures may produce automata with thousands of states, requiring synthesis times exceeding days or weeks and preventing completion of the methodology within project timelines. Reachability analysis for continuous modes with high-dimensional state spaces may similarly prove computationally intractable. Either barrier would constitute a fundamental obstacle to achieving research objectives.
 
 Several indicators would provide early warning of computational tractability
 problems. Synthesis times exceeding 24 hours for simplified procedure subsets
@@ -22,7 +22,9 @@ If computational tractability becomes the limiting factor, we reduce scope to a
 
 Computational tractability addresses whether synthesis can complete within practical time bounds—a practical constraint. The second risk proves more fundamental: whether boolean guard conditions in temporal logic can map cleanly to continuous state boundaries required for mode transitions. 
 
-This interface represents the fundamental challenge of hybrid systems: relating discrete switching logic to continuous dynamics. Temporal logic operates on boolean predicates. Continuous control requires reasoning about differential equations and reachable sets. Guard conditions requiring complex nonlinear predicates may resist boolean abstraction, making synthesis intractable. Continuous safety regions that cannot be expressed as conjunctions of verifiable constraints would similarly create insurmountable verification challenges. The risk extends beyond static interface definition to dynamic behavior across transitions. Barrier certificates may fail to exist for proposed transitions. Continuous modes may be unable to guarantee convergence to discrete transition boundaries.
+This interface represents the fundamental challenge of hybrid systems: relating discrete switching logic to continuous dynamics. Temporal logic operates on boolean predicates. Continuous control requires reasoning about differential equations and reachable sets. Guard conditions requiring complex nonlinear predicates may resist boolean abstraction, making synthesis intractable. Continuous safety regions that cannot be expressed as conjunctions of verifiable constraints would similarly create insurmountable verification challenges. 
+
+The risk extends beyond static interface definition to dynamic behavior across transitions. Barrier certificates may fail to exist for proposed transitions. Continuous modes may be unable to guarantee convergence to discrete transition boundaries.
 
 Early indicators of interface formalization problems would appear during both
 synthesis and verification phases. Guard conditions requiring complex nonlinear

6-broader-impacts/v1.tex

@@ -8,7 +8,7 @@ The nuclear industry faces uncompetitive per-megawatt costs for small modular re
 
 What has changed? Exponentially growing AI infrastructure demands have transformed this longstanding challenge into an immediate crisis—the market now demands solutions that did not exist before.
 
-Nuclear power presents both a compelling application domain and an urgent economic challenge. Recent interest in powering artificial intelligence infrastructure has renewed focus on small modular reactors (SMRs), particularly for hyperscale datacenters requiring hundreds of megawatts of continuous power. SMRs deployed at datacenter sites minimize transmission losses and eliminate emissions, but nuclear power economics at this scale demand careful attention to operating costs.
+Nuclear power presents both a compelling application domain and an urgent economic challenge. Recent interest in powering artificial intelligence infrastructure has renewed focus on small modular reactors (SMRs), particularly for hyperscale datacenters requiring hundreds of megawatts of continuous power. SMRs deployed at datacenter sites minimize transmission losses and eliminate emissions. Nuclear power economics at this scale, however, demand careful attention to operating costs.
 
 The U.S. Energy Information Administration's Annual Energy Outlook 2022 projects advanced nuclear power entering service in 2027 will cost \$88.24 per megawatt-hour~\cite{eia_lcoe_2022}. Datacenter electricity demand is projected to reach 1,050 terawatt-hours annually by 2030~\cite{eesi_datacenter_2024}. Nuclear power supplying this demand would generate total annual costs exceeding \$92 billion. Operations and maintenance represents a substantial component: the EIA estimates that fixed O\&M costs alone account for \$16.15 per megawatt-hour, with additional variable O\&M costs embedded in fuel and operating expenses~\cite{eia_lcoe_2022}. Combined, O\&M-related costs represent approximately 23--30\% of total levelized cost, translating to \$21--28 billion annually for projected datacenter demand.
 
@@ -58,11 +58,11 @@ establish both the technical feasibility and regulatory pathway for broader
 adoption across critical infrastructure.
 
 
-This section answered three critical Heilmeier questions about impact.
+This section answered three critical Heilmeier questions:
 
 \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 need autonomous control with safety guarantees.
 
-\textbf{Why now?} Two forces converge: exponentially growing AI infrastructure demands have created immediate need for economical nuclear power at datacenter scale (projections show datacenter electricity demand reaching 1,050 terawatt-hours annually by 2030), and formal methods tools have matured, making compositional hybrid verification computationally achievable. What was theoretically possible but practically intractable a decade ago is now feasible.
+\textbf{Why now?} Two forces converge. First, exponentially growing AI infrastructure demands have created immediate need for economical nuclear power at datacenter scale—projections show datacenter electricity demand reaching 1,050 terawatt-hours annually by 2030. Second, formal methods tools have matured, making compositional hybrid verification computationally achievable. What was theoretically possible but practically intractable a decade ago is now feasible.
 
 \textbf{What difference will it make?} This research addresses a \$21--28 billion annual cost barrier by enabling autonomous control with mathematical safety guarantees. Beyond immediate economic impact, the methodology establishes a generalizable framework for safety-critical autonomous systems across critical infrastructure.