All missions

Motivation

A seller learning demand from sales data also changes the conditions under which that data is generated. Customers may compare today's price with a reference formed from earlier prices. A price experiment can therefore affect both current sales and future demand. The seller observes prices and sales, while the reference price remains hidden. This mission concerns the slow-moving pricing policy in den Boer and Keskin, Dynamic Pricing with Demand Learning and Reference Effects, using the supplied April 19, 2021 artifact.

The relevant question is quantitative: how much cumulative revenue does this policy lose against a seller who knows the demand parameters and the reference mechanism? A guarantee must account for the cost of learning and the consequences of changing customers' reference prices. The target includes mechanisms whose smoothing coefficient changes over time and whose reference price can reset.

Setting

A price interval is the entire real interval $I=[\ell,u]$, with $0\le\ell<u$. The seller has a demand parameter $\theta=(\alpha,\beta,\eta^+,\eta^-)$ in a known bounded rectangle intersected with $\eta^+\le\eta^-$. Here $\alpha\ge0$, $\beta>0$ and the reference sensitivities are nonnegative. The expected demand and revenue are

$$d(p,r,\theta)=\alpha-\beta p+\eta^+(r-p)^+-\eta^-(p-r)^+, \qquad R(p,r,\theta)=p\,d(p,r,\theta).$$

For every allowed parameter vector, demand is nonnegative on $I^2$ and $\alpha/(2\beta)$ lies strictly inside $I$. Equality of the sensitivities and zero sensitivities are allowed. Observed demand adds an independent shock. The shocks are identically distributed, have mean zero and finite variance, and possess a finite moment generating function in some neighborhood of zero. Their law need not be Gaussian or bounded, and zero variance is allowed.

A reference mechanism is a continuous map from each finite price history to a reference in $I$. In the class $\mathcal R_{ES}$, one coefficient $\zeta\in[0,1)$ gives $r_{t+1}=\zeta r_t+(1-\zeta)p_t$. The larger class $\mathcal R_G$ has change times $\tau_1=1$ and coefficients $\zeta_k\in[0,1)$. Smoothing applies between changes; at a change the reference may reset continuously as a function of the full preceding price history. For some fixed finite $c>0$, every interval $(s,t]$ with positive integers $s<t$ contains at most $c\sqrt{t-s}$ changes. Infinitely many changes are permitted, as are coefficients tending to one. These are the mechanisms of Section 3.3, without an additional uniform contraction condition.

The slow-moving policy divides time into episodes $i\ge1$, each comprising two blocks of $2^i$ periods. With $\delta_i=c_0 2^{-i/4}$, it charges the previous price estimate minus or plus $\delta_i$, clipped at the appropriate price endpoint. At each completed episode it fits a linear demand model to that episode alone, projects the intercept and slope separately onto their known intervals, and updates its price estimate. The policy uses observed price-demand pairs, never the reference, unknown demand parameters or change schedule.

Formalization targets

The goal is Theorem 3 of the supplied source, printed and PDF page 17. Fix the model, an admissible noise process, a mechanism in $\mathcal R_G$, $\theta\in\Theta$, tuning $0<c_0<2^{-3/4}(u-\ell)$ and allowed initial estimates. The claim is

$$\exists c_6>0\quad\forall T\ge1:\quad \Delta_S(T,\rho,\theta)\le c_6\sqrt T.$$

The constant is finite and chosen before the horizon. Here regret compares the policy with the full dynamic clairvoyant benchmark

$$\Pi^*(T,\rho,\theta)=\sup_{(p_1,\ldots,p_T)\in I^T} \sum_{t=1}^{T}R(p_t,\rho_t(p_1,\ldots,p_{t-1}),\theta).$$

The three milestones retain their source numbering and dependency order. Proposition 2, page 17, asserts the same regret rate under two uniform sufficient conditions: the fixed price $\alpha/(2\beta)$ loses at most $c_4\sqrt T$, uniformly also over $\Theta$, and holding any price after any history incurs total reference deviation at most $c_5\sqrt{t-s}$. Theorem 1, page 10, gives a horizon-independent fixed-price loss bound for $\mathcal R_{ES}$. Proposition 1, page 13, bounds the sum of absolute reference deviations by one constant under the same exponential-smoothing class. Neither sufficient condition from Proposition 2 is a premise of the goal.

Significance

The printed result provides a square-root upper bound for a concrete learning rule when reference prices are hidden and can change their updating behavior. It compares that rule with all dynamic feasible price vectors, rather than with a fixed-price substitute. The claim applies to each finite prefix, including horizons that end before an episode or a block is complete.

Formalizing these statements makes the causal algorithm, the benchmark and the quantifier order explicit. The resulting definitions separate continuous reference mechanisms and iid noise from the specific demand model. All four theorem items are open statement targets in this mission; no machine-checked proofs of them are claimed. The source's description as asymptotic optimality is retained, but an independent minimax lower bound is outside the mission.

Difficulty

Holding a price fixed need not make its reference track it at a rate that is uniform across infinitely many regimes. Each coefficient being strictly below one does not place the entire sequence below a common number less than one. The source proof of Theorem 3 uses maxima over the regimes encountered before the horizon as though they yielded horizon-independent constants. The recorded finding supplies an allowed mechanism for which its intermediate tracking bound fails. This identifies a proof gap, not a disproof of the policy's regret conclusion.

The theorem remains the full printed target. Adding uniform contraction, limiting the number of changes or assuming the desired tracking bound would change the result. The nondifferentiable demand function, adaptive estimates and latent reference dynamics also have to be handled under the actual observation model.

Formalization scope

Prices remain real interval elements. Continuous maps describe references, extended naturals describe change times, and finite products describe histories. Internally, period zero represents source period one; positive horizons and source interval endpoints retain explicit guards. The algorithm is a causal recursion with compatible finite prefixes. Its least-squares update uses the explicit unique two-block solution, followed by the original coordinate projections. Prices are interval-valued; full clipping equals the printed one-sided clipping because the allowed projected center is interior. Real negative quarter powers determine perturbations.

The history domain is extended to real observations, agreeing with the printed nonnegative-history convention wherever it applies and accommodating the additive-noise model. Expected demand remains nonnegative; realized demand is not truncated. The benchmark is a real supremum of a continuous function on a nonempty compact box. Expected policy revenue is a Bochner integral of a bounded measurable finite-horizon random variable. Default values for unbounded suprema or nonintegrable functions therefore cannot trivialize the statements.

Definitions contain no regret or estimator-accuracy assumptions. The scope consists of the goal and its three specified milestones, with their shared foundations. Other results on incumbent pricing, gain-seeking behavior and statistical tests are intentionally excluded. Contributions establishing the full claims or resolving the recorded source findings must preserve these domains and quantifiers.

Selected references

• Arnoud V. den Boer and N. Bora Keskin, Dynamic Pricing with Demand Learning and Reference Effects, Management Science, supplied April 19, 2021 artifact marked “Forthcoming in Management Science,” first version December 23, 2017. DOI: 10.1287/mnsc.2021.4234. This mission preserves the repository's published citation basis and the supplied artifact's numbering: main pages 7–17 and electronic companion pages 1–17, PDF pages 33–49.

Motivation: paying once to remove a class of edges

A network failure can remove several connections at once. When the connections share a physical resource, paying for or disabling that resource acts on an entire class of edges. The minimum label s-t cut problem captures this distinction: edges carry labels, and the cost of removing a label is paid once, regardless of how many edges have that label. Zhang and Tang describe applications to attack graphs and network survivability in Appendix A of their paper.

Linear programming supplies lower bounds for many minimization problems. Its usefulness for an approximation guarantee depends on how far the fractional optimum can lie below the integral optimum. This mission concerns the strengthened label-cut relaxation LP2 and the paper's claim that its integrality gap grows nearly as the cube root of graph size. The source is the pinned 2019 preprint, rather than the later journal version.

Setting: label cuts and the distinct-label relaxation

Let G be a finite directed or undirected graph, with vertex set V, edge set E, distinct terminals s and t, and finite label set L. Each edge has exactly one label. Write n for the number of vertices and m for the number of edges. A label cut is a subset S of L such that deleting every edge carrying a label in S leaves no path from s to t. Its cost is the number of labels in S. The integral optimum OPT is the minimum of these costs.

For a simple terminal path P, let L(P) be the set of distinct labels appearing on P. The strengthened relaxation assigns a nonnegative real variable to each label:

$$\operatorname{OPT}_f=\min\left\{\sum_{\ell\in L}x_\ell: x_\ell\ge0,\quad \sum_{\ell\in L(P)}x_\ell\ge1\text{ for every simple }s\text{-}t\text{ path }P\right\}.$$

A repeated label contributes only once to a path constraint. There is no upper bound on an individual variable. These conventions distinguish LP2 from the edge-sum relaxation LP1 in Section 3. The all-label cut and all-ones fractional vector are feasible. For connected terminals, every fractional objective is at least one, so OPT/OPT_f has a positive, finite denominator.

Formalization targets

The goal is Theorem 1.1, with the directed extension in Section 7. For every real epsilon greater than zero, there are a positive constant C_epsilon and an integer threshold M_0, depending only on epsilon, such that every integer edge budget M at least M_0 admits an instance in each graph orientation satisfying

$$1\le m\le M,\qquad \frac{\operatorname{OPT}}{\operatorname{OPT}_f}\ge C_\epsilon M^{1/3-\epsilon}.$$

Each witness is a finite simple graph with connected, distinct terminals. The budget formulation specifies the asymptotic worst-case meaning of the printed Omega bound. It includes every positive epsilon and every sufficiently large budget, not just a single graph or an unbounded subsequence of isolated sizes.

The eight supporting targets are Lemmas 6.1–6.5, Lemmas 5.1–5.2, and Theorem 5.1. They concern chain-separation probability, configuration probability, the number of distinct configurations, an eventual analytic inequality, a choice of exponents, a realization with large integral optimum, the fractional optimum of every realization, and the analogous vertex-budget gap. Theorem 2.1 concerns LP1 and is outside this dependency chain.

Significance: a limitation of the fractional lower bound

The gap is a limitation of this particular LP lower bound. On the asserted instances, any guarantee comparing a returned integral solution directly with OPT_f must accommodate a factor at least as large as the displayed ratio. It does not rule out algorithms that exploit additional lower bounds or structural information. This is the interpretation given in Section 1.2.

The paper presents the result as proved. The formalization task is to supply checked proofs of the stated targets using explicit finite graphs, label cuts and fractional optimization. The current theorem declarations are open proof obligations. The reusable components include finite graph paths, label-based deletion, finite covering programs, and finite uniform permutation experiments. Distinguishing these definitions from the claimed bounds makes the result inspectable independently of the paper's argument.

Difficulty: shared labels across many paths

Ordinary edge-cut reasoning does not account for the cost sharing introduced by labels. A local deletion can remove many edges, while path constraints see the same label only once. The hard part is relating the global minimum number of labels to the concrete fractional program without replacing either optimum by a presumed bound.

The source also uses configurations derived from candidate label sets. A light ground element can have zero labels in a candidate; deleting such elements from the definition changes the subgraph whose disconnection is being measured. Distinct candidates can give the same displayed configuration. Formal statements must retain the relationship to the original candidate rather than silently identifying all associated events. Finally, real powers in the analytic estimates are not automatically integer cardinalities for graph gadgets. These are substantive interfaces between the combinatorics, probability and asymptotic statements in Sections 4–6.

Formalization scope

Finite sets use zero-based indices, which merely reindexes the source. A graph has named edges with endpoints and an orientation flag. Simple paths have injective vertex sequences. The goal requires simplicity, excludes loops and parallel edges, and counts each undirected edge once. The covering LP is a separate general definition with real variables. Its value is first an extended-real infimum; the label-cut specialization is feasible, bounded below and attained, and admissible ratio witnesses explicitly require a finite positive value.

The shutter construction is concrete. For each pair of ground elements and each chain index, a uniform independent permutation labels a chain of diamonds. Every diamond has two fresh route vertices and four edges. Internal junctions remain private to a chain; only the two global terminals are shared. For positive integer parameters k, d and h, its sizes are

$$m=4dh\binom{k}{2},\qquad n=2+(3d-1)h\binom{k}{2},\qquad |L|=kd.$$

Probabilities are exact counting ratios on the full product of permutation groups. Lemma 6.4 quantifies over all positive real beta and delta satisfying beta greater than delta minus one. The analytic vertex expression is the real extension of the displayed count, without declaring fractional numbers of vertices.

For the existential graph family, integer D with D at least 1/(3 epsilon) is an available witness when epsilon lies between zero and one third. Taking delta and beta equal to D gives integer parameters and size bounds n at most 48k^(2+3D), m at most 64k^(2+3D). With r=1/3-epsilon, possible constants are 48^(-r) for the integral bound and 2^(-D)64^(-D/(2+3D)) for the edge-budget bound; replace 64 by 48 for vertex budgets. Thresholds depend only on epsilon and must include the analytic eventuality threshold. These are witnesses to existential constants, not printed numerical constants or restrictions on Lemma 6.4. The recorded integrality issue in the source proof does not replace its theorem with a corrected target.

Selected references

• Peng Zhang and Linqing Tang, Minimum Label s-t Cut has Large Integrality Gaps, arXiv:1908.11491v1, 2019. Pinned preprint. Definition 1.1, Theorem 1.1, Sections 3–7 and Appendix A.

Stability under first-in, first-out service

In a queueing network, spare average capacity at every station does not by itself guarantee that queues remain stable. Jobs move between stations, and the service discipline affects how congestion propagates. Bramson gives examples of subcritical networks that are unstable, including examples with first-in, first-out service. The distinction matters when assessing whether a service system can sustain its offered traffic: comparing mean workloads with server capacities is useful only when the assumptions of a stability result apply. This mission concerns the class for which equal service means within each station restore that implication. The source is Bramson, Stability of Queueing Networks, Chapter 5, §5.3.

The FIFO discipline serves the oldest job at a station first. Kelly type requires that the mean service requirement be the same for all classes served at a particular station. It does not require equal service distributions, and it does not require exponential distributions. The target extends beyond the product-form setting discussed earlier in the book to general independent renewal and service primitives with finite means.

Networks, states and fluid paths

There are finitely many classes and stations. Each class belongs to one station. A completed class-$k$ job moves to class $l$ with probability $P_{kl}$, and otherwise exits. The routing matrix $P$ is substochastic and transient, so the network is open. External arrivals have rates $\alpha_k\ge0$, and service requirements have positive finite means $m_k$. With $Q=\sum_{n\ge0}(P^T)^n$, the vector $\lambda=Q\alpha$ gives total arrival rates. The load at station $j$ is

$$\rho_j=\sum_{k:s(k)=j}m_k\lambda_k.$$

Each station has unit capacity. A network is subcritical when every load is strictly below one. Queue lengths are unbounded. The stochastic state records ordered jobs and their ages, residual arrival clocks, residual head service requirements, and the allocation of service among classes. Its size is the sum of queue counts and residual arrival and service times. The state space is the general metric Borel space of §4.1, not a finite-state approximation.

A fluid path has six components: cumulative arrivals $A$, departures $D$, service effort $T$, workload $W$, idle time $Y$, and queue mass $Z$. They obey the basic conservation, capacity and non-idling equations. FIFO adds $D_k(t+W_{s(k)}(t))=Z_k(0)+A_k(t)$. The initial departure curve retains the initial service order; queue lengths alone do not determine it. All compatible solutions are included, even when they are not unique.

Formalization targets

The capstone is Theorem 5.9. For a subcritical FIFO Kelly network, assume that every positive size sublevel is petite: a probability mixture of its transition kernels over positive times has a common nonzero measure minorant on that set. The target is

$$\text{subcriticality and (5.1)}\quad\Longrightarrow\quad \text{positive Harris recurrence}.$$

Positive Harris recurrence combines almost surely infinite occupation of sets charged by a nonzero sigma-finite irreducibility measure with the existence of an invariant probability law. The conclusion concerns the stochastic process itself.

Theorem 5.10 supplies the corresponding fluid target: one constant $N>0$ works for every solution and every initial condition, with

$$Z(t)=0\quad\text{whenever}\quad t\ge N\sum_k Z_k(0).$$

The selected Chapter 4 milestones retain six-component subsequential compactness and both clauses of the transfer theorem from fluid stability to positive Harris recurrence. The entropy milestones retain nonnegativity, the full derivative identity, and all three bounds in Proposition 5.13. Lemma 5.14 retains its scope over every subcritical basic fluid model, with a single station-emptying bound uniform in the station, time and solution.

What the statements establish

The result identifies a service-mean condition under which subcritical FIFO networks are stable for general primitive distributions. Its conclusion is stronger than an inequality for expected queue size or the stability of a chosen deterministic trajectory. The full process can have continuous residual clocks and a state space that is neither finite nor countable. These features are part of Theorem 5.9 and its Chapter 4 setting.

The formalization separates reusable objects from their properties. General queueing parameter data are referenced from the published library. New definitions describe the ordered-job state, independent primitives, event dynamics, recurrence, petite sets, fluid paths and limits. The milestone statements and capstone are open proof obligations; compilation of their declarations is not a proof of the mathematical results.

Where care is required

Small average load is not a universal stability criterion, and an exponential-service model would omit the main distributional scope of this result. Likewise, a fluid path that drains does not establish a bound uniform over every solution. The source explicitly warns against inferring an unsupported strictly negative entropy derivative whenever entropy is positive. The selected statements preserve the actual quantitative assertions rather than that stronger shortcut.

The source also contains a domain issue: its entropy expression divides by total arrival rates, although zero rates are permitted. Under the declared full-domain reading, a two-station example contradicts two inequalities of Proposition 5.13, and a two-class, one-station example gives negative entropy in Lemma 5.11. Those printed assertions remain targets. The separate finding reports the concrete evidence; adding positive rates would remove source instances. A second finding concerns a state-dependent coefficient in the proof of Lemma 5.14, not its existential uniform-bound statement.

Formalization scope

Classes and stations use finite index types, while job lists have arbitrary finite length. Times are nonnegative; real-valued paths are constrained on that half-line, with right derivatives at its endpoint. Service means are positive, but external and total arrival rates may vanish. No Poisson, phase-type, second-moment or Feller assumption is imposed. The event description retains initial residuals and job order, and Harris recurrence is defined by occupation and invariant measures, independently of the fluid conclusions.

Emptying times use extended nonnegative reals, so never emptying means infinity rather than a default real infimum of zero. The fluid equations imply bounded derivatives on bounded time intervals, ensuring the entropy integrals have their intended analytic meaning. The zero-rate entropy reading uses the displayed real expression with total division and logarithm, giving $h_k(x)=0$ when $\lambda_k=0$; it is disclosed as a reading, not a repair.

There are no big-$O$ constants to instantiate in these selected results. The constants $N,c_2,c_6$ retain their source uniformity over initial data and solutions. The definition layer does not assume a stationary law, recurrence, fluid compactness or draining as a field of a network. Such an assumption would trivialize the mission. Further contributions can build the probability, measure-theoretic recurrence and fluid-analysis proofs on these independently specified objects.

Selected references

• Maury Bramson, Stability of Queueing Networks, Lecture Notes in Mathematics 1950, Springer, 2008, especially §§4.1, 4.3–4.4 and 5.3. DOI.

Why the complexity of clearing a puzzle matters

A puzzle can have simple local rules while the choice of moves has global consequences. Clickomania, also known as Same Game, is an example: a player removes adjacent blocks of one color, and the remaining blocks move into the vacated space. The computational question asks whether a given starting position can be cleared completely. Biedl, Demaine, Demaine, Fleischer, Jacobsen and Munro study how that question changes with the number of columns and colors in The Complexity of Clickomania, arXiv:cs/0107031v1, pp. 1–2.

The distinction matters for understanding what a general puzzle solver must accomplish. A board with few columns might appear to permit a short summary of everything relevant to future moves. Likewise, a small palette limits the immediate kinds of matching blocks. The selected theorem implies that a polynomial-time algorithm deciding solvability for all boards with five columns and three available colors would imply P = NP. The subject is the one-player decision problem; maximizing a score and determining the winner of a two-player game are different questions.

The board and its legal moves

A board begins as a finite, completely filled rectangle. Each cell holds one square block whose color belongs to a finite palette. Columns are ordered from left to right, and cells within each column are ordered from bottom to top. During play, columns can have unequal heights, but there are no internal gaps.

A group is a maximal edge-connected set of blocks of one color. Blocks meeting only at corners are not adjacent. Selecting one block selects its whole monochromatic component: the player cannot choose to remove just part of a larger group. A legal click requires at least two blocks in that group. All selected blocks disappear simultaneously. Each column then settles downward while retaining the vertical order of its surviving blocks. Any column with no remaining blocks disappears, and the surviving columns close together without changing their order. These are the operational rules on p. 1 of the pinned preprint.

A board is solvable if a finite sequence of legal clicks removes every block. Newly created groups remain until another click selects them. Solvability concerns whether some successful play exists, rather than whether every sequence of choices succeeds. An already empty board is solved by the empty sequence.

Formalization targets

Let $L$ be the language of valid finite encodings of solvable initial rectangular boards, and let $L_{5,3}$ be the corresponding language restricted to initial width five and palette size three. The target is the complete assertion of Theorem 15, p. 11:

$$\operatorname{NPComplete}(L)\quad\land\quad\operatorname{NPComplete}(L_{5,3}).$$

NP-completeness includes two requirements. Membership in NP means that yes-instances have polynomial-length certificates checked by a polynomial-time machine. Hardness means that every NP language over any finite nonempty alphabet has a polynomial-time many-one reduction to the puzzle language. A many-one reduction maps every input word to an output word, preserving both yes- and no-membership.

Height is any finite natural number. The palette has three available labels; a particular board may use fewer. Width five is a condition on the initial input, since empty columns disappear during play. Both complexity assertions are unconditional. The selected section has no numbered supporting results, so the mission has no additional milestone statements.

What the result and its formalization establish

The result places a precise boundary on the hope that limiting the board's width and palette automatically makes clearing it easy. The paper contrasts its hardness results with polynomial algorithms for the one-column case; those algorithms and the independent two-column, five-color theorem are outside this mission's scope (sections 2–4). The five-column, three-color assertion is retained with its numerical restrictions, rather than replaced by a less specific claim about arbitrary boards.

A completed formalization would connect the concrete game operations to a machine-based complexity classification. The present contribution supplies the definitions and the full target statement. Its definition modules and boundary checks compile, while the research theorem remains an open proof obligation. The published computational-complexity definitions are reused rather than changed to fit the puzzle.

What makes the formal proof demanding

It is not enough to exhibit boards whose intended play behaves correctly. A complexity proof must account for every legal click sequence and for the computational cost of producing and checking finite inputs. Changing group maximality, gravity or column shifting can change which boards are solvable. Similarly, a compact description of a tall repeated pattern cannot substitute for the explicitly represented blocks used to measure input size.

The source gives a construction in section 4, but its final equivalence is asserted without the detailed correctness argument, and several gadget parameters are not assigned sufficient polynomial bounds (pp. 11–14). Figure 2(a) also depicts two sentinel cells protruding above the common top line in column 4, whereas the initial model requires a full rectangle. These are missing details to reconcile in a formal proof; they do not establish that Theorem 15 is false. The target retains the printed theorem and the initial rectangle condition.

Formalization scope and conventions

The Lean model separates a finite colored grid, legal play, a general natural-number code, and the puzzle input languages. A board is an ordered list of columns of natural color labels. Missing coordinates have no color. Finite monochromatic paths define maximal components. Stable filtering implements simultaneous deletion, settling and column shifting; reflexive transitive closure expresses a finite play.

An input records width, height, palette size and every cell individually. Each natural number uses a canonical self-delimiting binary code. Dimensions and palette form the header; the payload lists cells column by column, bottom to top. A concrete decoder rejects truncated codes, noncanonical number codes, out-of-range labels, wrong cell counts and trailing data. No run-length compression is used. Unused palette entries are permitted, and declaring a large palette costs its binary representation rather than an enumeration of unused colors.

Zero-area rectangles are accepted as empty instances. Height-zero boards are normalized to the empty list while their declared width remains in the input record; a zero palette can occur only with zero area. These conventions impose no positive-height restriction. The theorem's languages are defined through this decoder and actual solvability, with no assumed verifier, assignment, reduction correctness or hardness conclusion.

The reusable CookPvsNP_defs module supplies finite-alphabet Turing machines, polynomial checking relations, NP and reductions. Polynomiality refers to input word length and actual machine steps. Contributions completing the complexity proof can build on the concrete model while preserving these conventions and both clauses of the target.

Selected references

• Therese C. Biedl, Erik D. Demaine, Martin L. Demaine, Rudolf Fleischer, Lars Jacobsen and J. Ian Munro, The Complexity of Clickomania, arXiv preprint, 2001. arXiv:cs/0107031v1, 21 July 2001. The operational model is on p. 1; Theorem 15 and its construction are on pp. 11–14. All source numbering in this mission uses this version.
• Stephen Cook, The P versus NP Problem, Clay Mathematics Institute problem description. Published complexity definition CookPvsNP_defs, following section 1, Definitions 3–4 and the Appendix. This is the imported formal complexity substrate, not a replacement citation for Theorem 15.

Motivation: accumulated rewards without discounting

An infinite sequence of decisions can be evaluated by the rewards accumulated over its entire lifetime. This criterion is useful when future rewards should retain their full weight, rather than being multiplied by a discount factor. It also exposes questions that discounting can obscure: a policy may incur an infinite loss, a supremum need not be attained, and a dynamic programming equation may have many solutions. Chapter 7 of Puterman's Markov Decision Processes studies these issues for the expected total-reward criterion.

This mission concerns positive bounded models, a class whose name requires care. Every policy has finite expected accumulated positive reward from each initial state, and every state offers at least one action with nonnegative immediate reward. Other actions may have negative rewards. The assumptions therefore cover more than models in which every one-step reward is nonnegative. The target is the convergence theorem in §7.2.4, with its pointwise conclusion and its prescribed initialization.

Setting: histories, policies, and signed rewards

A Markov decision process here has a nonempty finite or countably infinite state space $S$. Each state $s$ has its own nonempty finite or countably infinite action set $A_s$. Choosing $a\in A_s$ produces a real reward $r(s,a)$ and a successor state distributed according to $p(\cdot\mid s,a)$. Every transition row is a probability distribution of total mass one. Neither the transition probabilities nor the rewards depend on the decision epoch.

A history-dependent randomized policy observes all preceding states and actions, together with the current state, and assigns a probability distribution on the currently available actions. These policies form $\Pi^{HR}$. The smaller class $\Pi^{MR}$ of randomized Markov policies may depend on the epoch and current state, but does not use the rest of the history. Both classes allow randomization and infinitely many decision epochs.

Write $r^+(s,a)=\max(r(s,a),0)$ and $r^-(s,a)=\max(-r(s,a),0)$. For initial state $s$ and policy $\pi$, let

$$v^\pi_\pm(s)=\sum_{n=0}^{\infty}\mathbb E_s^\pi[r^\pm(X_n,Y_n)].$$

These nonnegative quantities can be infinite. Assumption 7.1.1 requires at least one of them to be finite for each policy and state, so their difference defines the total reward $v^\pi(s)$. The optimal value is the pointwise supremum $v^*(s)=\sup_{\pi\in\Pi^{HR}}v^\pi(s)$. Positive boundedness requires the positive part to be finite in every case and a nonnegative-reward action to exist at each state. No uniform bound across states is part of the definition. These conventions follow §§7.1–7.2, pp. 278–285.

Formalization targets

The first milestone is Proposition 7.1.1. Under Assumption 7.1.1, it identifies the two policy suprema separately at each state:

$$v^*(s)=\sup_{\pi\in\Pi^{HR}}v^\pi(s) =\sup_{\pi\in\Pi^{MR}}v^\pi(s).$$

This equality does not assert that a single policy attains all these suprema.

Define the Bellman operator by

$$(\mathcal Lv)(s)=\sup_{a\in A_s}\left(r(s,a)+\sum_t p(t\mid s,a)v(t)\right).$$

For positive bounded models, the next two milestones are Theorem 7.2.2 and Theorem 7.2.3(a). With $V^+$ the class of pointwise-finite nonnegative functions, their conclusions are

$$v\in V^+,\quad v\ge\mathcal Lv\ \Longrightarrow\ v\ge v^*;$$ $$v^*\in V^+,\qquad \mathcal Lv^*=v^*,\qquad \bigl(v\in V^+\ \text{and}\ \mathcal Lv=v\bigr)\Longrightarrow v^*\le v.$$

The goal is Theorem 7.2.12, printed p. 294:

$$v^0=0,\qquad v^{n+1}=\mathcal Lv^n \quad\Longrightarrow\quad v^n(s)\uparrow v^*(s)<\infty\qquad(s\in S).$$

Every iterate is finite and nonnegative at each state. The limit is the value defined from policy rewards, not a separately chosen solution of an operator equation.

Significance: identifying which fixed point matters

The goal connects a finite sequence of Bellman updates to the infinite-horizon optimization problem. The minimal-solution milestone explains why merely finding a fixed point would not identify the optimum: other nonnegative fixed points may exist. The supersolution milestone supplies a comparison principle for proposed upper bounds. Together these statements distinguish the expected-reward meaning of the value from the algebraic properties of the operator, as in Puterman, §§7.2.1 and 7.2.4.

The mathematical results are textbook results. The work posed here is to give machine-checked proofs against explicit probability and policy definitions. The draft theorem bodies remain open proof obligations. The reusable contribution includes a countable history-policy model, signed extended total rewards, and Bellman iteration whose definition does not presuppose convergence. The mission asserts no numerical stopping rule or convergence rate.

Difficulty: limits, unbounded functions, and policy classes

Discounted contraction arguments do not apply when the discount factor is one. Pointwise finiteness also does not supply a uniform domination bound on a countable state space. Replacing all policies by stationary deterministic policies at the definition stage would change the optimization problem before any reduction theorem had been proved. Similarly, taking an ordinary real infinite sum would conceal divergent losses by assigning a default value.

The printed proof of Theorem 7.2.12 contains a further issue recorded as finding F3: its assertion that one policy realizes every finite-horizon optimum need not hold. A three-state example with incompatible first-stage choices establishes the gap. This finding concerns the argument, not the convergence statement, and does not change the goal. The two disputed supporting clauses recorded as F1 and F2 are outside the selected milestones.

Formalization scope

The Lean namespace is PutermanMDP.TotalReward. The model stores real rewards and probability mass functions. Histories store past state–action pairs in chronological order and the current state; their length is the epoch, indexed from zero. History distributions are constructed recursively by sampling actions and transitions. Expected nonnegative rewards are actual extended nonnegative sums over these distributions. Their difference and the supremum over admissible policies are taken in the extended reals. Assumption 7.1.1 excludes subtraction of two infinite reward parts.

The class $V^+$ is represented by extended-real functions satisfying $0\le v(s)<\infty$ at every state. No closure of this entire class under Bellman is assumed. The algorithm starts at exactly zero, and the theorem proves finiteness of its orbit and finite pointwise limits. Convergence uses the extended-real order topology at a finite real limit, equivalent there to ordinary real convergence. The discrete state and action conventions come from §2.1.2, p. 18; no finite-state restriction is introduced.

No instance field assumes a Bellman solution, an optimal policy, or convergence, and the optimal value is never defined as the limit of the iterates. There are no asymptotic constants or probability tolerances to instantiate in these results. No variants are posed. Only part (a) of Theorem 7.2.3 is included; part (b) is not silently corrected. Mathlib's probability mass functions, extended real orders, nonnegative infinite sums, and filters supply the underlying libraries. Proofs connecting the recursive history laws to policy comparison and pointwise convergence are the remaining contributions sought.

Selected references

• Martin L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994, §§2.1–2.2 and 7.1–7.2, especially pp. 280, 285–286, 294–295. DOI: 10.1002/9780470316887. All source indices refer to this artifact; its PDF pages are the printed pages plus 16.

Motivation

Production plans often allow demand to be served late and charge a separate cost for restarting production. These choices interact: keeping a machine set up can avoid a later start-up charge, while delaying production creates backlog costs. A formulation that represents each feature separately need not give an exact linear relaxation when the features are combined. Chapter 10 of Pochet and Wolsey (2006) studies these interactions within finite-horizon, single-item lot-sizing. The target here is its joint optimization result for uncapacitated production under Wagner–Whitin carrying costs, Theorem 10.22.

The distinction between an optimization formulation and a full description of physical production plans matters. An extended linear program may determine the correct minimum cost while containing auxiliary production coordinates that do not themselves form a feasible production schedule. This mission keeps the original mixed-integer constraints and the displayed extended formulation as separate mathematical objects.

Setting

A finite-horizon lot-sizing instance has periods $1,\ldots,n$, where $n\ge1$, and nonnegative demands $d_t$. Production $x_t$ is nonnegative. Stock $s_t$ and backlog $r_t$ measure material held and demand outstanding at the end of a period. The balance equation is

$$s_{t-1}-r_{t-1}+x_t=d_t+s_t-r_t.$$

Initial backlog is zero. Initial stock and terminal stock and backlog are nonnegative decision variables. A binary setup $y_t$ enables production, with $x_t\le My_t$ and $M\ge\sum_{t=1}^n d_t$. Binary start-up and switch-off variables are denoted by $z_t$ and $w_t$. In the joint model they satisfy $z_t-w_{t-1}=y_t-y_{t-1}$ and $z_t\le y_t$, with given initial setup state $y_0\in\{0,1\}$. Switch-offs have indices $0,\ldots,n-1$; in particular, $w_0$ is a decision variable.

The transformed objective is

$$C(s,r,y,z)=\sum_{t=0}^n h_ts_t+\sum_{t=1}^n(b_tr_t+q_ty_t+g_tz_t).$$

Wagner–Whitin costs mean that both $h_t$ and $b_t$ are nonnegative. The fixed costs $q_t,g_t$ are real. The constant term arising when unit production costs are eliminated is omitted from both optimization problems. These conventions follow Sections 10.1 and 10.6 of the textbook.

The extended formulation adds nonnegative variables $\alpha_t,\beta_t$ for stock and backlog fractions. Where $d_t>0$, they satisfy $\alpha_t+y_t+\beta_t=1$. The displayed system also links adjacent backlog fractions and imposes stock and backlog inequalities over every interval. Its domains relax the three binary vectors to unit boxes. These inequalities define the set directly; no hull or integrality property is built into its definition.

Formalization targets

Three source milestones describe the start-up component. Observation 10.3 states, for an exact setup/start-up plan and $1\le k<t\le n$,

$$y_k+\sum_{j=k+1}^t z_j=0\iff y_k=\cdots=y_t=0.$$

The next milestone is the displayed stock inequality (10.11), valid for the original uncapacitated model without backlogging:

$$s_{k-1}\ge\sum_{u=k}^l d_u\left(1-y_k-\sum_{j=k+1}^u z_j\right).$$

Theorem 10.15 asserts that these inequalities, the two listed start-up inequalities, and the stated stock/setup bounds describe the convex hull of the Wagner–Whitin start-up set. The faithful item retains the printed omission of a lower bound on $z$. A two-period counterexample is recorded, and a separate corrected target adds $z\ge0$.

The goal, Theorem 10.22 on printed page 331, concerns the joint model. If $X(y_0,d,M)$ is its original mixed-integer feasible set and $Q(y_0,d)$ its displayed extended formulation, then

$$\min_{p\in X(y_0,d,M)}C(p)=\min_{v\in Q(y_0,d)}C(v),$$

with both minima attained. The statement asks for feasible minimizers in both problems, equality of their costs, and universal optimality inequalities. It does not assume the conclusion as a property of either feasible set. The source statements and their roles are in Chapter 10, Sections 10.4 and 10.6.

Significance

The joint result identifies a linear formulation that solves a planning model with both late service and start-up decisions. Its meaning is objective-specific: nonnegative transformed carrying costs are part of the result. The milestone hull statement, by contrast, concerns equality of entire sets in stock/setup/start-up coordinates and retains their unbounded nonnegative stock directions.

The formal development provides explicit finite coordinate spaces, original feasibility predicates, the extended constraints, and an attained-optimum statement. The theorem items are open formalization targets; compiling their statements does not prove them. The source presents the joint optimization result as established, whereas the literal wording of the start-up hull milestone has the documented defect. Keeping those statuses distinct prevents the corrected variant from obscuring what the textbook actually states.

Difficulty

Separate stock and backlog conditions must agree with the same setup and start-up decisions. A hull description for one component alone does not establish the joint optimization statement. Nor does equality of feasible objective infima by itself supply the attained minima required here. The original formulation includes production balances, while the extended formulation displayed on pages 330–331 omits them and leaves its nonnegative production coordinate unused.

There are also source conventions to resolve explicitly. The joint display omits the domains of $\alpha,\beta$ and abbreviates adjacent-period ranges as “for all $t$.” Their nonnegative fraction domains are inherited from Section 10.2.3, and the adjacency range here is $1\le t<n$. These choices are disclosed for review. Theorem 10.15's missing $z\ge0$ has a concrete counterexample and is expected to be disproved as printed; it must not be used as an unquestioned established lemma.

Formalization scope

Period arrays use finite index types of size $n$, with a one-based accessor; switch-off arrays use the zero-based labels $0,\ldots,n-1$. The setup accessor supplies the given binary $y_0$ at time zero, as specified on printed page 138. Stock and backlog arrays have size $n+1$, including index zero. Accessors return zero outside their declared ranges, and empty interval sums are zero. Every substantive theorem restricts its interval indices to the stated horizon. Demand may vanish in some or all periods; the fraction partition is imposed only where demand is positive. No terminal switch-off coordinate or condition is added, and terminal stock and backlog are not forced to vanish.

The definition layer contains real bodies and no proof placeholders. It uses Mathlib finite sums, real vector spaces, sets, and convex hulls. The original feasible sets are defined from their constraints rather than from the hull or LP theorem being sought; the goal is not specialized to zero demand or a singleton horizon. No asymptotic complexity theorem is selected, so there is no replacement of an $O(\cdot)$ claim by a constant.

Beyond the paper. One corrected variant of Theorem 10.15 adds only $z\ge0$. The evidence is the instance $y_0=0$, $n=2$, $d=(0,0)$, $s=0$, $y=(1,0)$, $z=(1,-1)$, which satisfies the printed inequalities but cannot belong to the hull of binary-start-up points. The faithful item remains the milestone. The proposed corrected hull requires its own proof.

The shortest-path and facility-location companion hulls, Theorems 10.2 and 10.14, are outside this mission's selected targets. Theorem 10.3 is also omitted: its printed projection includes an eliminated production coordinate, whose relationship to the stock/backlog ambient space is unresolved in the source wording. The joint formulation itself is transcribed directly, so these omissions do not alter the goal.

Selected references

• Yves Pochet and Laurence A. Wolsey, Production Planning by Mixed Integer Programming, Springer, 2006, Chapter 10, especially Sections 10.1, 10.2.3, 10.4.2–10.4.3, and 10.6. DOI: 10.1007/0-387-33477-7.

Motivation: capacity limits across a planning horizon

A production plan must meet demand on time while deciding which periods justify a setup. When each active period can supply at most the same amount, the capacity limit links setup decisions to cumulative demand. A linear relaxation that treats those decisions as fractional may admit plans that cannot be assembled from feasible binary setup schedules. Understanding the exact convex hull identifies which linear inequalities capture all of those restrictions. Chapter 9 of Pochet and Wolsey (2006) develops this question for several capacitated lot-sizing models.

The present target concerns the Wagner–Whitin feasible relaxation with constant capacity. It asks whether separately convexifying every initial-stock subproblem loses information when those hulls are intersected. This is a structural question about production-planning formulations, relevant before choosing particular setup and inventory costs. The selected results connect rounded demand requirements, a single continuous initial-stock variable, and the full collection of stock coordinates.

Setting: setups, demand, and entering stock

There are $n\ge1$ periods, indexed in the mathematical notation by $1,\ldots,n$. Demand in period $t$ is a real number $d_t\ge0$, and the common capacity is $C>0$. The chapter preprocesses demands so that $d_t\le C$; this convention is retained. Write $d_{kt}=\sum_{u=k}^t d_u$. A setup vector $y\in\{0,1\}^n$ records which periods are available for production. Each active period contributes capacity $C$.

The discrete lot-sizing set consists of binary vectors satisfying $C\sum_{u=1}^t y_u\ge d_{1t}$ at every period. Its initial-stock version has an additional decision $s_0\ge0$ and covering rows $s_0+C\sum_{u=1}^t y_u\ge d_{1t}$. These are the original formulations in Sections 9.3 and 9.4 of the book, rather than definitions using the hull inequalities being sought.

For the larger Wagner–Whitin set, retain stocks $s_0,\ldots,s_n\ge0$ and the same binary setup vector. Every interval obeys

$$s_{k-1}+C\sum_{u=k}^t y_u\ge d_{kt},\qquad 1\le k\le t\le n.$$

Denote this set by $X^{\mathrm{WW-CC}}$. Its component $X_k^{\mathrm{DLSI-CC}}$ retains only the interval rows beginning at $k$, while retaining every stock coordinate and every binary setup coordinate. All components therefore occupy the same ambient space. Neither endpoint stock is fixed to zero.

Formalization targets

The first milestone, Proposition 9.2, asserts that every feasible discrete setup vector satisfies

$$\sum_{u=1}^t y_u\ge\left\lceil d_{1t}/C\right\rceil.$$

The second, Theorem 9.3, gives the complete discrete hull:

$$\operatorname{conv}(X^{\mathrm{DLS-CC}}) =\{y\in[0,1]^n:\sum_{u=1}^t y_u\ge\lceil d_{1t}/C\rceil\text{ for every }t\}.$$

The explicit nonemptiness assumption in Section 9.3 is preserved for these two statements.

Theorem 9.4 is the third milestone. Put $b_t=d_{1t}/C$ and $f_t=b_t-\lfloor b_t\rfloor$. For each nonempty subset $T=\{i_1,\ldots,i_r\}$ ordered by nondecreasing fractional parts, with $f_{i_0}=0$, define

$$R_T(y)=C\sum_{\tau=1}^r(f_{i_\tau}-f_{i_{\tau-1}}) \left(\lfloor b_{i_\tau}\rfloor+1-\sum_{u=1}^{i_\tau}y_u\right).$$

Its hull description retains the original covering rows, nonnegative initial stock, and setup bounds, and adds both families

$$s_0\ge R_T(y),\qquad s_0\ge R_T(y)+C(1-f_{i_r})\left(\lfloor b_{i_1}\rfloor-\sum_{u=1}^{i_1}y_u\right).$$

All fractional-part ties are permitted. These targets are Proposition 9.2 and Theorems 9.3–9.4, printed pages 276 and 280.

The goal is Theorem 9.8, printed page 283:

$$\operatorname{conv}(X^{\mathrm{WW-CC}}) =\bigcap_{k=1}^n\operatorname{conv}(X_k^{\mathrm{DLSI-CC}}).$$

It is an equality of full feasible hulls, not merely equality of selected objective values.

Significance: compatible constituent hulls

The goal states that the separate initial-stock descriptions retain enough information to describe the joint feasible hull. Together with the one-stock description, it connects explicit mixing inequalities to the full constant-capacity formulation. The interpretation and subsequent inequality descriptions are developed in Section 9.5.2.

The mathematical results are textbook claims, not newly proposed conjectures. The remaining work is to supply machine-checked proofs of the stated identities and validity result. The definition layer gives reusable original feasible sets and explicit cut families. The theorem files are checked Lean statements with proof placeholders; successful compilation does not certify these mathematical claims. A completed development would make the distinction between model constraints and hull consequences explicit and available for later production-planning formalizations.

Difficulty: convexification and intersection

Convexification does not in general commute with intersection. Knowing the hull of each constituent therefore does not establish the reverse inclusion in the goal. Every component here shares the same setup vector, while constraining a different entering-stock coordinate. Dropping that shared-coordinate structure changes the question. Likewise, the one-stock hull cannot be described faithfully by rounding each original row independently: Theorem 9.4 specifies two families indexed by subsets with an order determined by fractional parts.

The source states Theorem 9.8 in this section without a full proof. No missing numbered lemma is invented. The general mixing results in Chapter 8 remain separate source results; their proofs may provide supporting infrastructure without duplicating their statements here.

Formalization scope

Lean uses Fin n for periods, with coordinate $j$ corresponding to printed period $j+1$. Stock coordinates use Fin (n+1) with the printed indices unchanged. Setups are real coordinates restricted to zero or one in the original sets; hull coordinates are real. The constant capacity is strictly positive in every theorem. Demands may vanish, all-zero demand is permitted, and a one-period horizon is included. The feasible sets retain their unbounded stock directions.

Nonempty subsets in the cut families are injective enumerations of Fin (m+1). Nondecreasing fractional parts allow every tie ordering; chronological order is not required. The initial zero fractional-part predecessor is represented by a separate first summand. Ordinary real convex hulls are used throughout, with no added closure operation. There are no complexity targets or asymptotic constants in scope.

The model sets are defined from their original inequalities, never by a claimed hull description, an assumed integrality property, or a special zero-demand instance. Theorems expand their sets and cut formulas so the displayed constraints can be audited directly. Mathlib supplies real arithmetic, finite sums, integer rounding, and convex hulls. Contributions completing the four proofs or establishing reusable finite-dimensional mixing machinery are within this scope. No variant theorem is included; the recorded zero-cost issue in Proposition 9.6 concerns an omitted optimization result.

Selected references

• Yves Pochet and Laurence A. Wolsey, Production Planning by Mixed Integer Programming, Springer Series in Operations Research and Financial Engineering, Springer, 2006. DOI: 10.1007/0-387-33477-7. Chapter 9, especially Sections 9.3–9.5.2, printed pages 276–283; PDF pages 289–296 in the pinned source.

Motivation: production timing with setup costs

A production planner must meet demand over several periods while deciding when to incur fixed setup costs. Producing early can combine several periods into one batch, but the resulting inventory carries a holding cost. Even for one item without a capacity limit, continuous production quantities interact with discrete setup decisions. An exact linear formulation offers a way to study those decisions without discarding their economic meaning. Chapter 7 of Pochet and Wolsey, Production Planning by Mixed Integer Programming develops this problem and its formulations.

This mission concerns Wagner–Whitin costs, where postponing production to a later available setup cannot increase the variable cost. In the stock-based objective used here, this condition is expressed by nonnegative holding costs. The central question is whether a compact collection of stock inequalities describes precisely the convex hull of the feasible mixed integer set. The target is Theorem 7.10, including its geometric equality and its consequence for optimization.

Setting: demand, stock, setups, and intervals

There are $n\ge1$ periods and a real demand $d_t\ge0$ in each period. Production $x_t$ and end-of-period stock $s_t$ are nonnegative real quantities. A setup variable $y_t$ takes value zero or one, with production permitted only when it is one. In the ordinary lot-sizing model, stock balance is

$$s_{t-1}+x_t=d_t+s_t.$$

The original feasible set $X^{LS-U}$ also requires $x_t\le My_t$, with $M$ sufficiently large, and fixes $s_0=s_n=0$. The transformed objective is $px+qy$, where $p$ incorporates holding costs and $q$ is the fixed setup cost. Costs can be negative, so a setup with no production must remain possible. These are the conventions of Sections 7.1–7.2 of the source.

Write $d_{kl}=\sum_{j=k}^l d_j$ for cumulative demand. The shortest-path formulation introduces a nonnegative variable $\varphi_{ut}$ for each interval $[u,t]$. Its flow moves one unit through a network with nodes $1,\ldots,n+1$. Interval flow determines production, and flow on intervals with positive demand is bounded by the corresponding setup variable. Existential elimination of the flow variables gives its projection onto production and setup coordinates.

For the Wagner–Whitin target, the variables instead are $(s,y)$. Initial stock is a decision variable, and terminal stock is nonnegative. Define $P^{WW-U}$ by $s\ge0$, $0\le y\le1$, and

$$s_{k-1}\ge\sum_{j=k}^l d_j\left(1-\sum_{u=k}^j y_u\right)\qquad(1\le k\le l\le n).$$

The mixed integer set $X^{WW-U}$ adds integrality of $y$ to these same constraints. This is the explicit formulation (7.30)–(7.32), not the zero-initial-stock set $X^{LS-U}$.

Formalization targets

The first two milestones are companion formulation results. Theorem 7.8 states that the shortest-path linear program attains an optimum with integral setups and that the resulting production and setup vectors extend to an optimal ordinary lot-sizing plan. Theorem 7.9 identifies the entire projection:

$$\operatorname{proj}_{x,y}Q^{SP-U}=\operatorname{proj}_{x,y}\operatorname{conv}(X^{LS-U}).$$

Observation 7.12 supplies the third milestone. It equates the stock inequality above with

$$s_{k-1}+\sum_{j=k}^l d_{jl}y_j\ge d_{kl}.$$

Under zero initial stock and the balance equations, it also equates this with the corresponding inequality expressed through cumulative production. That endpoint assumption belongs to this rewriting, not to the goal's stock variables.

The goal is Theorem 7.10:

$$P^{WW-U}=\operatorname{conv}(X^{WW-U}).$$

It also states that, for every $h\ge0$ and every real $q$, any optimal extreme point for $hs+qy$ over $P^{WW-U}$ solves the mixed integer formulation. The geometric assertion does not carry cost assumptions. The shortest-path milestones provide companion results on the same demand model; they are not presented as the direct proof of the goal.

Significance: an exact continuous description

The hull equality describes every fractional point obtainable by convex combination of feasible mixed integer plans. It is stronger than agreement of two objectives for one chosen cost vector. The optimization clause then identifies the role of extreme points when the cost condition holds. Section 7.5 of the source uses this formulation to distinguish the Wagner–Whitin regime from general uncapacitated lot-sizing costs.

The formalization supplies explicit interfaces for stock balance, triangular interval flows, projected feasible sets, and attained optimality. These are reusable in comparisons between formulations. The mathematical results are textbook claims; this proposal contains compiled theorem statements awaiting proofs, not newly established machine-checked proofs. Definitions have complete bodies, and every theorem states the claimed conclusion without taking that conclusion as an assumption.

Difficulty: mixed integrality and unbounded stock

Integral setups do not imply integral stock when demands are arbitrary real numbers. Moreover, the stock formulation is unbounded in nonnegative stock directions. Replacing it with a bounded polytope, fixing initial stock, or assuming stock minimality would change the result. The full hull, including its unbounded directions, is part of the target.

The proof on printed page 231 needs particular scrutiny. Its assertion of integrality for the full extended polyhedron does not hold for fractional demand, and the equality linking stock to demand-weighted auxiliary variables requires care when an entire demand tail vanishes. Numerical witnesses for both issues are recorded in the mission's findings. These observations concern the printed argument; the goal retains Theorem 7.10 without positive-demand or integer-demand restrictions.

Formalization scope

All vectors are finite-dimensional real vectors. Production and setup periods use Fin n; stock and flow nodes use Fin (n+1). A period index in Lean is one less than its printed index. Interval arcs contain only pairs with the start no later than the end, so there are no unconstrained extra flow coordinates. Theorems require a positive horizon and allow zero demand, including an entirely zero demand vector.

For the ordinary lot-sizing comparisons, $M>0$ and $M\ge\sum_t d_t$ make the source's large-bound convention explicit. The domain $x\ge0$ follows the production interpretation and equation (7.47); the missing nonnegativity marker in printed equation (7.4) is disclosed as finding F1. Negative fixed costs remain allowed. No running-time theorem is selected, so there is no asymptotic constant to instantiate.

The goal defines both feasible sets from the printed inequalities and uses the ordinary real convex hull and extreme-point notions. It does not define either feasible set as the claimed hull, assume integrality, or restrict the instance to a special demand pattern. Its locally bound sets and objective expose their complete code to the separate goal auditor. The reusable definition modules cover ordinary lot-sizing and the interval-flow formulation. Further work consists of proofs of the stated claims and explicit treatment of the recorded proof gaps; no variant theorem is posed.

Selected references

• Yves Pochet and Laurence A. Wolsey, Production Planning by Mixed Integer Programming, Springer Series in Operations Research and Financial Engineering, Springer, 2006. DOI: 10.1007/0-387-33477-7. Chapter 7, especially Sections 7.1, 7.4, 7.5 and 7.7; Theorems 7.8–7.10 and Observation 7.12.

Motivation

Observing a fluctuating process does not reveal whether its largest value has already occurred. A decision to stop must nevertheless use the observations available at that moment. Optimal prediction asks how well such a decision can approximate a quantity determined by the entire future path. Peskir and Shiryaev formulate a basic instance using a Brownian particle observed during a fixed unit interval: stop so that the particle's current position is as close as possible, in mean square, to its eventual maximum. The financial interpretation concerns decisions based on predictions of the highest observed price or position over a specified horizon (Section 30.1, pp. 441–442).

The horizon is known, but the maximum is not. The decision therefore depends on the evolving information, rather than on a deterministic time selected beforehand. The mission concerns the exact solution for a standard Brownian motion without drift, including both its expected loss and the stopping rule attaining that loss.

Setting

A standard Brownian motion $B=(B_t)_{t\ge0}$ starts at zero, has continuous paths, and has independent Gaussian increments with variance equal to elapsed time. Its natural filtration $\mathcal F_t^B=\sigma(B_s:0\le s\le t)$ records the observations through time $t$. A stopping time $\tau$ is a decision for which the event $\{\tau\le t\}$ can be determined from this information. The admissible class $\mathcal M$ consists of these times with $0\le\tau\le1$.

Define the running maximum and the resulting drawdown by

$$S_t=\sup_{0\le s\le t}B_s,\qquad D_t=S_t-B_t.$$

The target $S_1$ is the ultimate maximum, while the estimator is the stopped position $B_\tau$. The loss and value are

$$L(\tau)=(B_\tau-S_1)^2,\qquad V_* =\inf_{\tau\in\mathcal M}\mathbb E L(\tau).$$

This is the source's probability-space formulation, with a fixed horizon and no extra information about future observations (Eqs. (30.1.1)–(30.1.2)). Write $\varphi$ for the standard normal density and $\Phi$ for its cumulative distribution function.

Formalization targets

The goal is Theorem 30.1. Let $z_*$ be the unique root of

$$4\Phi(z_*)-2z_*\varphi(z_*)-3=0.$$

The root is positive. The theorem identifies the least loss and an attaining rule:

$$V_*=2\Phi(z_*)-1,\qquad \tau_*=\inf\{0\le t\le1:D_t\ge z_*\sqrt{1-t}\}.$$

The rule is itself an admissible stopping time, and its squared error is integrable with expectation equal to the displayed value (p. 442, Theorem 30.1).

Three supporting targets retain numbered source equations. The first is the explicit adapted representation

$$S_1=\mathbb ES_1+\int_0^1H_t\,dB_t,\qquad H_t=2\left[1-\Phi\left(\frac{D_t}{\sqrt{1-t}}\right)\right]\quad(t<1).$$

The second is the identity, for every $\tau\in\mathcal M$,

$$\mathbb E L(\tau)=1+\mathbb E\int_0^\tau(1-2H_t)\,dt.$$

These are Eqs. (30.1.7)–(30.1.8) and the final equality of Eq. (30.1.10), respectively (p. 442).

The third target concerns the analytic candidate

$$W(z)=\Phi(z_*)(1+z^2)-|z|\varphi(|z|)+(1-z^2)\Phi(|z|)-\frac32$$

for $|z|\le z_*$, extended by zero elsewhere. With $F=4\Phi-3$, it satisfies

$$W''+zW'-2W=-F(|z|)\quad (|z|<z_*),$$

and $W(\pm z_*)=W'(\pm z_*)=W'(0)=0$. The target includes global continuous differentiability and interior second differentiability (Eqs. (30.1.21)–(30.1.27), pp. 444–445).

Significance

The solution specifies a moving threshold for an observable quantity: the distance below the largest position already seen. It gives an exact benchmark for a prediction problem in which the eventual target is unavailable at the decision time. It also separates the objective, defined over every admissible time, from the particular rule whose performance realizes that objective (Theorem 30.1).

A formal development would connect the Brownian probability model, its information structure, an adapted stochastic integral, and analytic boundary conditions in a single result. The definition layer supplies reusable interfaces for bounded-horizon prediction losses and drawdown hitting rules. The source result is established mathematics; the theorem files in this mission are proof obligations, not completed machine-checked proofs. Compiling the statements checks their types and dependencies but does not prove the assertions.

Difficulty

The terminal maximum depends on the whole path. A rule that observes this maximum in advance solves a different problem. Likewise, equality in distribution between drawdown and absolute Brownian motion does not, by itself, transport arbitrary stopping decisions between information structures. The source explicitly invokes the filtration and Markov properties when making this passage (p. 443). The stated reduction therefore keeps the same Brownian natural filtration and the same stopping time on both sides.

The analytic candidate is another distinct object: satisfying differential and boundary conditions does not by definition make it the stochastic value. The final theorem must still identify the infimum and establish attainment. The mission does not assume the verification conclusion as a hypothesis. The later timing-prediction discussion and general-horizon remark contain the source issues recorded in the accompanying findings; neither is used as an unqualified additional target here.

Formalization scope

Time is represented by nonnegative real numbers. The driving process is defined for all such times, and the objective uses only its restriction to $[0,1]$. Mathlib supplies the Brownian law predicate and measure-theoretic foundations. Evaluation measurability and everywhere continuous paths specify the chosen continuous version. Admissibility is expressed directly by measurability of $\{\tau\le t\}$ in the sigma-algebra generated by the observed past, with an everywhere unit bound.

The objective uses a nonnegative extended integral and an extended-real infimum. The admissible class is nonempty because it contains the constant zero time. Continuity makes running suprema finite on compact intervals; the boundary hitting set contains time $1$. Real expectations in theorem conclusions come with integrability assertions. The endpoint value $H_1=0$ is a convention that does not affect either time integration or the left-sampled stochastic sums.

The unit-horizon integral is represented independently by the $L^2$ limit of left-endpoint dyadic sums for this explicit bounded integrand. This interface is not a general assertion that every predictable process admits such a sampling construction. The maximum representation establishes square integrability of the limit and sums. The general Itô–Clark uniqueness theorem is not separately posed. The transformed diffusion and its infinite-horizon stopping problem are left to subsequent proof development rather than introduced as additional mission items.

The exact root defines every constant; the descriptive decimals $1.12\ldots$ and $0.73\ldots$ are not substituted into any theorem. There are no asymptotic constants to instantiate. In particular, neither the value nor the optimizer is defined by assuming the claimed answer, and the filtration never includes the future maximum. Contributions can address the stochastic representation, the analytic candidate, or the complete optimality theorem while preserving these conventions.

Selected references

• Goran Peskir and Albert N. Shiryaev, Optimal Stopping and Free-Boundary Problems, Birkhäuser Verlag, 2006, Section 30.1, pp. 441–451. DOI: 10.1007/978-3-7643-7390-0. The fixed source PDF places these pages at PDF pages 457–467; the goal is printed p. 442 / PDF p. 458.

Motivation

Production planning combines continuous quantities with discrete decisions about when a machine is prepared to produce. A setup can incur a fixed charge even when the amount subsequently produced is small. Relaxing the setup decision to a fraction can therefore give a cost bound that is too optimistic. For a single product without capacity limits, a complete reformulation provides an exact benchmark for stronger formulations of larger planning systems. This is the role of the uncapacitated lot-sizing example in Pochet and Wolsey, Chapter 4.

The question concerns the entire family of feasible plans, rather than the numerical performance of one solver. An exact reformulation must retain every original feasible plan and exclude every point outside their convex hull after auxiliary variables are eliminated. It must also support the optimization claim actually made in the source: a linear program has an attained optimum whose setup variables are integral.

Setting

A finite planning horizon contains periods $1,\ldots,n$, with $n\ge1$. Demand $d_t$ in period $t$ is a nonnegative real number. Production $x_t$ and end-of-period stock $s_t$ are nonnegative real quantities. The binary variable $y_t$ indicates whether production is enabled. Inventory balance requires

$$s_{t-1}+x_t=d_t+s_t.$$

The initial inventory is fixed at $a$, where $0\le a\le d_1$, and final inventory is zero. Production is linked to setup by $x_t\le d_{tn}y_t$, where $d_{tn}=\sum_{k=t}^n d_k$. A setup may be unused. These are the original constraints in Chapter 4, equations (4.2)–(4.5).

The multi-commodity formulation distinguishes production by the demand period it serves. A quantity $w_{it}$ is produced in period $i$ for delivery in period $t\ge i$. Its inventory after period $i$ is $v_{it}$. Each commodity satisfies its own balance equations and has no inventory after its delivery period. Initial stock is assigned to the first commodity. The setup bound is $w_{it}\le\widehat d_ty_i$, with $\widehat d_1=d_1-a$ and $\widehat d_t=d_t$ otherwise. Relaxing setups gives $0\le y_i\le1$. Summing quantities over commodities defines a projection $\pi$ into the original production, stock, and setup coordinates.

Formalization targets

The goal is Theorem 4.1, printed page 121. If $X$ denotes the original feasible set and $Q$ the continuous multi-commodity formulation, it requires

$$\pi(Q)=\operatorname{conv}(X).$$

For real costs $p,h,q$, it also requires an attained minimum of

$$C(x,s,y)=\sum_{t=1}^n(px_t+qy_t)+\sum_{t=1}^{n-1}hs_t$$

over $Q$, with all setup variables binary. The projection of this minimizer must belong to $X$ and minimize the same objective there.

Three source milestones organize the supporting material from Chapter 7. Proposition 7.1 asserts an optimal plan satisfying $s_{t-1}x_t=0$ in every period. Proposition 7.4 asserts validity of the $(l,S)$ inequalities

$$\sum_{j\in S}x_j\le\sum_{j\in S}d_{jl}y_j+s_l, \qquad S\subseteq\{1,\ldots,l\}.$$

Theorem 7.5 asserts that these inequalities, together with the original continuous constraints and zero endpoint stocks, describe the convex hull of the integer feasible set. Their precise statements and their source-domain defect are kept separate from their corrected companions.

Significance

The goal identifies exactly what the additional commodity variables accomplish. Its geometric conclusion applies independently of an objective, while its optimization conclusion supplies an actual plan with binary setup decisions. Together they express why the relaxation solves this single-item model without a separate branching decision, as claimed in Chapter 4. They do not assert that adding arbitrary linking constraints across multiple items preserves that property.

The formalization makes quantities, endpoint inventories, and the direction of projection explicit. It also separates a literal printed statement from a correction justified by the surrounding model. These are proposed theorem statements, compiled with proof placeholders; they are not machine-checked proofs of the textbook results. The intended physical-model results are established mathematics, and completing their proofs is the formalization task.

Difficulty

A correct integer reformulation alone does not establish the convex-hull equality. Fractional setup vectors create additional cases, and equality of costs for one numerical instance cannot establish equality of sets. The distinction between existence of some binary optimal solution and integrality of every relaxed feasible point must also be maintained.

There is a source defect in the milestone model. Equation (7.4) prints unrestricted real production, although Chapter 4, the network interpretation, the validity proof, and equation (7.47) require nonnegative production. For $n=2$, $d=(1,1)$, $M=3$, the literal constraints admit $x=(3,-1)$, $s=(0,2,0)$, and $y=(1,0)$. This point violates the $(2,\{1\})$ inequality. With production costs $(-1,0)$ and all other costs zero, every optimum violates the zero-inventory condition. The faithful milestone statements are therefore retained as disproof targets, with their corrected companions available for the physical-model development.

Formalization scope

Production periods use Fin n, with index zero corresponding to source period one. Stocks use Fin (n+1), including both boundary values. The hypothesis $n>0$ excludes an empty horizon; singleton horizons and zero demands remain included. The milestone models have zero initial and final stocks. Their positive big-$M$ coefficient is at least total demand, making the source's “large” coefficient precise. Costs have no sign restrictions, so unused setups cannot be removed by definition.

Each theorem exposes its complete feasible constraints through binders or local let-bindings. The multi-commodity arrays are rectangular, with entries outside the source's triangular domain constrained to zero. The goal defines projection by existential elimination and summation. Its cost sum includes terminal stock, which is constrained to zero. No side of the hull equality is defined to be the other side, and neither integrality nor optimality is assumed. No algorithmic complexity claim is selected, so no asymptotic constant is instantiated.

Beyond the paper. Exactly three corrected variants restore production nonnegativity to the literal milestone model: zero-inventory optimality, inequality validity, and the hull description. They change only this domain condition. The numerical counterexample above supplies the evidence for each correction, and the corrected domain is explicitly printed in equation (7.47). The faithful numbered statements remain the milestone anchors. Separately, equation (7.17) has an extra demand factor in commodity aggregation; the goal uses the independently correct Chapter 4 equations and does not pose the later alias as another target.

The required library infrastructure is finite sums, finite ordered indices, real vector spaces, and convex hulls. Contributions can establish the corrected physical-model milestones, disprove the literal statements, or prove the goal's projection and attainment clauses. No external draft imports or unverified model definitions are prerequisites.

Selected references

• Yves Pochet and Laurence A. Wolsey, Production Planning by Mixed Integer Programming, Springer Series in Operations Research and Financial Engineering, Springer, 2006. DOI: 10.1007/0-387-33477-7. Chapters 4 and 7; Theorem 4.1, Propositions 7.1 and 7.4, and Theorem 7.5.

Motivation

A decision maker observes a fluctuating quantity and can collect its largest observed value when observation stops. Waiting can improve the record, but observation has a running cost. The decision depends on both the current state and the record already achieved: the same current observation can justify different decisions after different histories. This is the maximum-process stopping problem studied in Section 13 of Peskir and Shiryaev (2006).

The chapter connects this stochastic optimization problem with a differential equation for a stopping boundary. The equation can have several solutions. The substantive question is which solution represents the optimization problem, and what happens when there is no suitable global solution. The source also distinguishes an optimal rule from a sequence of admissible rules whose rewards only approach the value.

Setting

A diffusion $X$ is a continuous real-valued stochastic process satisfying

$$dX_t=\rho(X_t)\,dt+\sigma(X_t)\,dB_t,\qquad X_0=x,$$

where $B$ is standard Brownian motion, the drift $\rho$ is continuous, and the volatility $\sigma$ is continuous and strictly positive. The process exists for every nonnegative time and has state space $\mathbb R$. Its running maximum, initialized at $s\ge x$, is $S_t=s\vee\sup_{0\le r\le t}X_r$. A continuous strictly positive function $c$ specifies the cost per unit time at each state.

An admissible stopping time $\tau$ uses only the information generated by $X$, is almost surely finite, and satisfies $E\int_0^\tau c(X_t)dt<\infty$. The value function is

$$V_*(x,s)=\sup_{\tau\text{ admissible}}E_{x,s}\left[S_\tau-\int_0^\tau c(X_t)\,dt\right].$$

Expected rewards and the supremum may equal $+\infty$. These are the objects in Eqs. (13.1.1)–(13.1.5), with the book's almost sure finiteness convention from Definition 2.1.

The scale function $L$ is normalized by $L(0)=0$ and $L'(0)=1$, with $L'(y)=\exp(-\int_0^y2\rho(z)/\sigma(z)^2\,dz)$. The speed measure has density $2/[L'(y)\sigma(y)^2]$. These quantities encode the spatial behavior used in the boundary equation and candidate value formula.

Formalization targets

The first milestone is Proposition 13.1: the diagonal is a continuation region,

$$V_*(x,x)>x.$$

The second milestone is the equivalence following Eq. (13.2.21). For a continuously differentiable boundary $g(s)<s$, the integral candidate satisfies the generator equation, normal reflection, instantaneous stopping, and smooth fit exactly when

$$g'(s)=\frac{\sigma(g(s))^2L'(g(s))}{2c(g(s))[L(s)-L(g(s))]}.$$

The third milestone is Eq. (13.2.30), superharmonicity of the candidate minus accumulated cost for the specified admissible stopping class. All three targets retain the numbered source anchors in Section 13.

The goal is the complete statement of Theorem 13.2. A maximal admissible boundary $g_*$ is a global solution of the equation, strictly below the diagonal, which dominates every other such solution pointwise. The source identifies the finite value as

$$V_*(x,s)=s+\int_{g_*(s)}^x[L(x)-L(y)]c(y)m(dy)$$

for $g_*(s)\le x\le s$, and as $s$ for $x\le g_*(s)$. Its hitting rule is optimal when its expected cost is finite, and otherwise is approximated by admissible hitting rules as specified in Eq. (13.2.41). Whenever an admissible optimum exists, this rule is the smallest optimum almost surely. The source's alternative asserts infinite value and absence of an optimal stopping time when there is no maximal admissible boundary.

Significance

The finite-value part of Theorem 13.2 connects a stopping problem defined over random times with an analytic boundary selected by pointwise maximality. It gives both a value formula and a decision rule, while identifying exactly when admissibility is required for attainment. The distinction between exact and approximate optimality is part of the result, rather than an implementation detail.

The formalization supplies a reusable representation of diffusion coefficients, weak solutions, natural stopping information, accumulated costs, scale and speed, and global boundary comparison. The theorem items are proof obligations, not machine-checked proofs of the book. The definitions have genuine bodies, and the statements compile against the pinned environment. An independent representation of the stopping value makes comparison with the proposed formula a substantive mathematical claim.

Difficulty

Solving the boundary equation locally does not establish global admissibility, pointwise maximality, or admissibility of the associated stopping rule. The finite expected cost condition also does not automatically make every maximum payoff integrable. These issues prevent local analytic calculations alone from settling the stopping problem.

There is an additional source-level obstacle. Finding F4 records an explicit counterexample to the last nonattainment clause under the stated extended-real reward convention. A Brownian motion with positive unit drift and cost $c(y)=e^{-y}$ admits an almost surely finite rule with infinite expected reward and finite expected cost, while the boundary equation has no global admissible solution. The faithful printed goal is retained; this clause is expected to require a disproof or a separately stated correction. The finding does not silently replace the source statement, and no variant item is included.

Formalization scope

Time is nonnegative real, stopping times take values in $[0,\infty]$, and admissibility requires almost sure finiteness. The natural filtration is augmented by ambient measurable null sets and made right-continuous. The weak stochastic differential equation is specified by Brownian motion adapted to a witnessing filtration, independence of future increments, and convergence in probability of left dyadic stochastic-integral sums. No growth or Lipschitz assumption is added to the continuous coefficients; the given solution is nonexplosive.

Costs and maximum increments are integrated as nonnegative quantities, and rewards subtract only finite expected cost on the admissible class. Extended-real suprema retain the infinite-value alternative. Ordinary real suprema are used only for continuous paths on compact time intervals. The scale normalization is immaterial to the product of scale differences and speed measure in the formulas.

The value is not defined by the candidate formula, and maximality contains no optimality hypothesis. The boundary approximation includes decreasing ODE boundaries with finite diagonal contacts, increasing admissible hitting times, and convergence of their rewards. There are no asymptotic constants to instantiate in the selected statements. Exit-probability identities, the general signed occupation formula, nonnegative-state boundary classifications, and discounted variants are outside this mission. The three inherited Chapter III findings remain recorded without additional theorem items. Contributions can establish the finite-value clauses, the analytic equivalence, the stochastic comparison milestone, or a formal disproof of the identified source clause.

Selected references

• Goran Peskir and Albert Shiryaev, Optimal Stopping and Free-Boundary Problems, Birkhäuser Verlag, 2006. DOI: 10.1007/978-3-7643-7390-0. Section 13, printed pp. 199–213; Definition 2.1 and the filtration convention, printed p. 27. All source indices use this published edition.

Motivation

Optimal stopping problems often describe a value function separately in a continuation region and a stopping region. The two descriptions meet along a boundary that changes with time. Applying stochastic calculus to such a function requires knowing what happens at that boundary: continuity of the function does not imply continuity of its spatial derivative. A formula that only applies to globally smooth functions would miss precisely this issue. Chapter II of Peskir and Shiryaev's Optimal Stopping and Free-Boundary Problems, especially Section 3.5, supplies the change-of-variable formula for this setting.

The mission concerns a single continuous boundary in one spatial dimension. Its goal is the diffusion formula (3.5.9), with the hypotheses stated immediately before it. The general continuous-semimartingale formula and the Brownian Tanaka identity provide supporting targets. These are classical mathematical identities; the task is to express and ultimately prove them in Lean with their stochastic and analytic hypotheses intact.

Setting

A filtered probability space consists of a probability measure $P$ on a measurable sample space $\Omega$, together with increasing information sets $\mathcal F_t$. The filtration is right-continuous, the probability space is complete, and every null event belongs to $\mathcal F_0$. These are the usual conditions imposed in the book on printed pages 53–54.

A continuous semimartingale $X$ has a decomposition $X=X_0+M+A$, where $M$ is a continuous local martingale starting at zero and $A$ is continuous, adapted, and of finite variation on every finite interval. The random initial value need not have a finite expectation. Its quadratic variation $Q=\langle X,X\rangle$ is the continuous increasing adapted process characterized by $M^2-Q$ being a local martingale. Both definitions follow the framework of Section 3.1 and Eq. (3.3.6) in the book.

Let $c:[0,\infty)\to\mathbb R$ be continuous and of bounded variation on each finite interval. The function $F(t,x)$ is continuous everywhere and has one time derivative and two spatial derivatives separately on $x>c(t)$ and $x<c(t)$. Each derivative extends continuously to the closure of its own side. The boundary traces $F_x(t,c(t)+)$ and $F_x(t,c(t)-)$ are allowed to differ.

The symmetric local time on the curve is normalized by

$$\ell_t^c(X)=P\text{-}\lim_{\varepsilon\downarrow0} \frac{1}{2\varepsilon}\int_0^t \mathbf1_{\{c(s)-\varepsilon<X_s<c(s)+\varepsilon\}}\,dQ_s.$$

This probability limit is Eq. (3.5.6). Local time is represented by a continuous increasing adapted process, so integration against it is ordinary pathwise Lebesgue–Stieltjes integration.

Formalization targets

The first milestone references the existing time-dependent multidimensional Itô theorem, specialized to a time-independent test function, for Eq. (3.3.18). The next milestone is the Brownian Tanaka identity and its normalization, Eqs. (3.3.21)–(3.3.22):

$$|B_t-a|=|B_0-a|+\int_0^t\operatorname{sgn}(B_s-a)\,dB_s+L_t^a, \qquad L_t^a=\lim_{\varepsilon\downarrow0}\frac1{2\varepsilon} \int_0^t\mathbf1_{\{|B_s-a|\le\varepsilon\}}\,ds.$$

The third milestone is Eq. (3.5.5). Writing bars for the arithmetic mean of the two one-sided derivatives, it asserts

$$F(t,X_t)=F(0,X_0)+\int_0^t\bar F_t(s,X_s)\,ds +\int_0^t\bar F_x(s,X_s)\,dX_s +\frac12\int_0^t F_{xx}(s,X_s)\mathbf1_{\{X_s\ne c(s)\}}\,dQ_s +\frac12\int_0^t(F_x^+-F_x^-)(s,X_s)\mathbf1_{\{X_s=c(s)\}}\,d\ell_s^c.$$

For the goal, suppose additionally that $dX_t=b(X_t)\,dt+\sigma(X_t)\,dB_t$, with measurable locally bounded coefficients and $\sigma\ge0$. Fix $T\ge0$ and assume $P(X_s=c(s))=0$ at every deterministic time $0<s\le T$. Set $\mathcal L_XF=bF_x+\frac12\sigma^2F_{xx}$. The target, Eq. (3.5.9), is almost surely, simultaneously for $0\le t\le T$,

$$\begin{aligned} F(t,X_t)=F(0,X_0)&+\int_0^t(F_t+\mathcal L_XF)(s,X_s)\mathbf1_{\{X_s\ne c(s)\}}\,ds\\ &+\int_0^tF_x(s,X_s)\sigma(X_s)\mathbf1_{\{X_s\ne c(s)\}}\,dB_s\\ &+\frac12\int_0^t(F_x(s,X_s+)-F_x(s,X_s-))\mathbf1_{\{X_s=c(s)\}}\,d\ell_s^c. \end{aligned}$$

All three displayed nonsmooth identities and their hypotheses are taken from the published book, printed pages 67 and 74–75.

Significance

The goal separates the contribution from evolution away from the boundary from the contribution of the spatial derivative jump at the boundary. It permits a function to be treated using the smooth formulas valid in its two regions while retaining the additional local-time term prescribed by the source. It does not assume smooth fit, and it does not infer that a zero probability of occupying the boundary at each deterministic time makes local time vanish.

The formal development supplies reusable representations of continuous semimartingales, increasing integration clocks, stochastic integrals, side derivatives, and occupation local time. The theorem statements ask for existence of the integrals and local time together with the identities. The referenced Itô theorem is currently Open on Prove2Me; the new theorem items are also proof targets, not completed machine-checked proofs.

Difficulty

The analytic derivatives have two different boundary traces, while stochastic paths may visit the boundary repeatedly. Ordinary globally smooth Itô calculus does not directly state the required identity. The normalization of the occupation limit must agree with the one-half coefficient in the formula. The time integral, stochastic integral, quadratic-variation integral, and local-time integral also use different measures, so removing an indicator from one term cannot be justified merely by its irrelevance to another.

The book attributes proofs of Section 3.5 to its reference [163]. This mission retains the original stronger hypotheses (3.5.1)–(3.5.2). The separate relaxed extension (3.5.10)–(3.5.13) is outside the target; the notation issue in its final hypothesis is recorded for later review.

Formalization scope

Time is nonnegative real time and the state is real. Input Brownian and semimartingale paths are continuous at every sample point, as in the source. Local-martingale versions and identities are understood up to null sets. Brownian increments have explicit centered Gaussian laws and are independent of the past filtration. Finite variation is represented as the difference of two continuous increasing processes. Increasing clocks extend by zero to negative real times and carry actual Stieltjes measures; integration is over $(0,t]$. Their continuity removes endpoint atoms. Local pathwise integrability is required explicitly, preventing the default value of a nonintegrable Bochner integral from supplying an identity.

The stochastic integral is characterized independently by compensated products: for $J=\int H\,dM$, both $JM-\int H\,dQ$ and $J^2-\int H^2\,dQ$ are continuous local martingales starting at zero. Progressive measurability and local square integrability are included. The SDE is an integral equation using this same relation. No target change-of-variable formula appears inside these definitions.

Local time is defined by occupation limits, never by rearranging the asserted identity, and the two derivative traces are not identified. The Brownian normalization uses the closed strip printed in (3.3.22); the curve normalization uses the strict strip printed in (3.5.6). The sign at zero is zero. The goal's no-contact assumption excludes time zero and only applies through the selected horizon. All constants are exact: $1/(2\varepsilon)$ in occupation limits and $1/2$ in the derivative-jump and generator terms. There are no asymptotic constants or probability bounds to instantiate.

Selected references

• G. Peskir and A. N. Shiryaev, Optimal Stopping and Free-Boundary Problems, Birkhäuser Verlag, 2006, Chapter II, Sections 3.1, 3.3, and 3.5, especially printed pp. 67, 74–75. DOI.
• S. N. Ethier and T. G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 5, Theorem 2.9, printed p. 287. The existing formal statement supplies the classical Itô milestone. DOI.

Motivation

Boolean satisfiability asks whether a collection of logical requirements can hold simultaneously. Maximum satisfiability instead asks how many requirements can hold, while sometimes retaining a separate collection that must hold. Restricting the syntax of each requirement can substantially change the decision problem without removing the expressive power of the optimization problem. This distinction motivates the study of optimization over Horn clauses in Marques-Silva, Ignatiev and Morgado, arXiv:1705.05335v1, especially §§1–2 and 5.2.

The selected result concerns an explicit transformation of arbitrary finite satisfiability instances into Horn maximum-satisfiability instances. It specifies the output clauses and an exact threshold, so its content is more concrete than the existence of some reduction between the two problems. The mission covers this transformation and its uniform polynomial-time computability. Other reductions, the hitting-set solver, its abstraction claims and the experiments in the paper are independent of this target.

Setting

A Boolean variable takes one of the values false and true. A literal is a variable or its negation. A clause is a finite disjunction of literals, and a CNF formula is a finite conjunction of clauses. A total assignment assigns a Boolean value to every variable. It satisfies a clause when at least one literal is true and satisfies a formula when every clause is satisfied. An empty clause is false; a formula with no clauses is true. These are the conventions of §2, p. 2.

A Horn clause contains at most one distinct positive literal. Thus an all-negative clause, an empty clause and a positive unit clause are Horn. An unweighted partial MaxSAT instance consists of hard clauses $H$ and soft clauses $S$. A feasible assignment satisfies every hard clause. Its score is the number of satisfied soft clauses, each with unit weight. The associated threshold question asks whether there exists a feasible assignment whose score reaches a specified natural number. This preserves infeasibility separately from score zero, as required by the hard-clause convention in §2, pp. 2–3.

For a formula $F$ with $N$ variables, the dual-rail encoding introduces two distinct variables $p_i,n_i$ for each original variable $x_i$. HEnc includes the hard exclusion $(\neg p_i\lor\neg n_i)$ for each pair. Each source clause is also turned into a hard clause: positive $x_i$ becomes $\neg n_i$, and negative $\neg x_i$ becomes $\neg p_i$. The soft clauses are the positive units $(p_i)$ and $(n_i)$, one of each per original variable. The threshold is $N$. These clauses are the specific construction in §5.2, p. 8.

Formalization target

The single goal asserts that HEnc is computed by one fixed deterministic finite-control multi-stack Turing machine within one fixed polynomial in input length, uniformly for all finite source formulas. For every $F$, write $(H,S,N)=\operatorname{HEnc}(F)$. In addition to that efficiency assertion, the goal requires

$$\text{every clause of }H\text{ and }S\text{ is Horn},$$ $$F\text{ is satisfiable}\iff \exists b\;\bigl(b\models H\ \land\ \operatorname{score}_S(b)\ge N\bigr),$$

and the universal cap

$$\forall b,\quad b\models H\Longrightarrow\operatorname{score}_S(b)\le N.$$

The constant in both comparisons is exactly $N$. The quantifier over $b$ ranges over all total assignments on the $2N$ rails. No feasible assignment, satisfying source assignment or attained optimum is assumed. This is the unnumbered HEnc correctness claim, §5.2, p. 8, with the polynomial-reduction convention from §§1–2 made explicit. There are no numbered supporting milestones in this source argument.

Significance

The result gives a precise relationship between the answer to an arbitrary CNF satisfiability instance and an exact score threshold in its Horn output. Both directions of the equivalence matter: the output must neither lose a satisfiable source instance nor admit a threshold witness for an unsatisfiable one. The cap additionally describes every feasible target assignment. These are properties of the specified transformation, rather than properties of a solver chosen to process its output. They are the contribution of §5.2 selected here.

The mathematical claim is presented in the paper as an established reduction. The formal goal remains unproved. A completed development would connect a concrete finite syntax, a reusable hard/soft objective and actual machine execution within one checked statement. The general Horn and partial-MaxSAT definitions can support other encodings without assuming this reduction's correctness. The published CNF representation is reused; its unrelated complexity conjectures are not assumptions of this mission.

Difficulty

Hornness alone is insufficient: the semantic equivalence and exact score cap must concern the same computed clauses. Hard feasibility permits both rails in a pair to be false. Replacing it with an exactly-one condition would change the target. Empty hard clauses also prevent an optimization convention that assigns score zero to infeasibility from expressing the threshold question correctly when $N=0$.

The computational clause introduces a separate obligation. A short output or a terminating recursive definition does not establish a polynomial bound for a fixed machine. The formal target requires a machine that writes the complete encoded output, together with a polynomial bound on its actual steps. It does not request a polynomial-time SAT or MaxSAT solver.

Formalization scope

Variables use zero-based finite indices. Lists represent clause collections and clauses; repeated hard clauses or literals do not alter satisfaction, and Hornness counts distinct positive literals. HEnc's soft list contains each rail exactly once. All widths are admitted, including empty clauses, tautologies and contradictory units. The representation also admits unused declared variables; restricting the declared universe to the variables occurring in $F$ recovers the source domain without changing its threshold.

The finite alphabet has six tokens. Variable counts are unary headers; literal indices and the output threshold use terminated little-endian binary. Separate tokens delimit clauses and distinguish hard from soft collections. The header makes every declared variable contribute to input size. The formalization claims no polynomial bound in the logarithm of a hidden variable count. Mathlib's TM2ComputableInPolyTime supplies the concrete execution model and polynomial step bound. No source-specific numerical runtime constant is invented.

Definitions contain no satisfiability oracle, correctness certificate or assumed reduction property. The theorem retains efficiency, Hornness, the full equivalence and the universal cap in one item. The apparent $c_i$/$c_j$ index typo in §5.2 is read according to its literalwise construction and documented separately. Proof contributions must establish the full statement; neither a restricted source class nor an output-size calculation replaces it.

Selected references

• João Marques-Silva, Alexey Ignatiev and António Morgado, Horn Maximum Satisfiability: Reductions, Algorithms and Applications, preprint, 2017, arXiv:1705.05335v1, especially §2, pp. 2–3 and §5.2, p. 8. All page references use this pinned version.