Dynamical Systems

Motivation

Boolean networks model gene regulatory networks by giving each gene an on/off value and updating all values synchronously by logical rules (Kauffman, 1969). Adding external Boolean inputs gives Boolean control networks (BCNs), in which a designer (a drug, an intervention) chooses the inputs over time. The basic control-theoretic question is controllability: can the inputs drive the network from any configuration to any other? Cheng and Qi (Automatica 2009) answered it for BCNs using the semi-tensor product of matrices, which rewrites a BCN as a linear recursion on canonical basis vectors.

Biological regulation is not instantaneous: transcription and translation introduce delays, so the next value of a gene can depend on several past values. Lu, Zhong, Ho, Tang and Cao (SIAM J. Control Optim. 2016) study delayed BCNs, in which the update reads the last $\mu$ states, and give criteria for two kinds of controllability, including the case where some configurations are dangerous and must be avoided (in biology, states corresponding to disease). The mission formalizes their criteria.

Setting

Write $\mathcal D=\{0,1\}$. A state is $x=(x_1,\dots,x_n)\in\mathcal D^n$ and an input value is $u\in\mathcal D^m$. Fix $\mu\ge1$. The delayed BCN (2.2) is

$$x_i(t+1)=f_i\big(u(t),x(t-\mu+1),\dots,x(t)\big),\qquad i=1,\dots,n,$$

with arbitrary Boolean functions $f_i:\mathcal D^{m+\mu n}\to\mathcal D$, collected into one map $F$ with $x(t+1)=F(u(t),X(t))$. A trajectory is the window $X(t)=(x(t-\mu+1),\dots,x(t))$ of the last $\mu$ states; its last entry is the current state. One step maps $X(t)$ under the input $u(t)$ to $X(t+1)=(x(t-\mu+2),\dots,x(t+1))$. A control sequence of length $k$ is $U=(u(0),\dots,u(k-1))$, with inputs chosen freely; $y(i)=X(i)$ denotes the trajectory after $i$ steps from an initial trajectory $y(0)$.

The transition-count matrix $Q$ has rows and columns indexed by trajectories: $Q_{b,a}$ is the number of input values $u$ taking trajectory $a$ to trajectory $b$ in one step. For a set $C_t$ of forbidden trajectories, $Q_{C_t}$ is $Q$ with the rows and columns of $C_t$ replaced by zeros, and $\mathbb Q_{C_t}$ is $Q$ with those rows and columns deleted.

The notions of controllability are:

• Trajectory controllable (Definition 3.1): from every initial trajectory, every trajectory $X_d$ equals $X(k)$ for some $k\ge1$ and some control sequence.
• Trajectory controllable under $C_t$ (Definition 3.11): for all trajectories $a,b\notin C_t$ there are $k\ge0$ and a control sequence steering $y(0)=a$ to $y(k)=b$ with $y(i)\notin C_t$ for $i=0,\dots,k$.
• State controllable (Definition 4.1): from every initial trajectory, every state equals $x(k)$ for some $k>0$ and some control sequence.

A real square matrix $A$ of size $N\ge2$ is reducible (Definition 3.7) if a simultaneous permutation of rows and columns brings it to block upper-triangular form $\begin{pmatrix}A_{11}&A_{12}\\0&A_{22}\end{pmatrix}$ with square diagonal blocks; it is irreducible otherwise, so every $1\times1$ matrix is irreducible.

$\mathbb N_1(k;y_a,y_b,C_t)$ counts the control sequences of length $k$ steering $y_a$ to $y_b$ while avoiding $C_t$; $\mathbb N_2(k;a,b_s)$ counts those steering the initial trajectory $a$ to $x(k)=b_s$; $\Xi^{p}_\mu$ is the set of trajectories with current state $p$.

Formalization targets

Goal: Theorem 3.12

$$\text{the delayed BCN is trajectory controllable under } C_t\iff \mathbb Q_{C_t}\ \text{is irreducible},$$

for every $\mu\ge1$, $n$, $m$, every update map and every forbidden set $C_t$. It is the most general criterion of the paper.

Milestones

• Proposition 3.5: for $k>0$, $\mathbb N_1(k;y_a,y_b,C_t)=y_b^{\mathsf T}(Q_{C_t})^ky_a$.
• Remark 3: $\mathbb N_1(k;y_a,y_b)=y_b^{\mathsf T}Q^ky_a$.
• Theorem 3.10: trajectory controllable $\iff$ $Q$ irreducible.
• Theorem 4.3: $\mathbb N_2(k;a,b_s)=\sum_{b\in\Xi^{b_s}_\mu}b^{\mathsf T}Q^ka$.
• Theorem 5.1: the same count while avoiding forbidden states $C_s$, with $Q$ zeroed on the trajectories containing a state of $C_s$.
• Corollary 5.3: trajectory controllability implies state controllability.

A supporting item, Lemma 3.9 (corrected form), relates Definition 3.7 to positivity of entries of powers for nonnegative matrices of size at least 2.

Significance

The criteria replace a question about control sequences of unbounded length by a finite test on one nonnegative integer matrix of size $2^{\mu n}$. The counting identities give more than a yes/no answer: they enumerate the control sequences achieving a transfer, which is what a designer choosing among interventions needs, and they handle forbidden states by passing to forbidden trajectories.

The results are proved in the paper; none of them has a machine-checked proof. Formalizing them yields a reusable Lean model of delayed (and, for $\mu=1$, ordinary) Boolean control networks defined directly through their dynamics, together with a checked bridge from dynamic reachability to the combinatorics of nonnegative matrices. A formal version also pins down points the printed text leaves loose: Lemma 3.9 as printed is false (it characterizes primitive, not irreducible, matrices), and the two different matrices $Q_{C_t}$ (zeroed) and $\mathbb Q_{C_t}$ (deleted) must not be confused.

Difficulty

The central step is the passage between three objects: reachability under the dynamics, positivity of entries of powers of $Q$, and the block-triangular definition of irreducibility. The counting identity for powers of $Q$ is a statement about sequences of inputs, not about paths in a graph, so the bijection between control sequences and weighted walks has to be established with the avoidance constraint carried at every intermediate time, including the endpoints. The equivalence between Definition 3.7 and strong connectivity is the classical graph-theoretic characterization, but it has edge cases the obvious argument misses: a $1\times1$ zero matrix is irreducible by Definition 3.7 yet has no positive power, which is exactly why Definition 3.11 allows $k=0$ while Definition 3.1 does not. A proof that routes through "some power of $\mathbb Q_{C_t}$ is entrywise positive", following the printed Lemma 3.9, proves a false intermediate statement.

Formalization scope

Conventions committed to in Lean:

• A state is Fin n → Bool (true is the paper's 1); a trajectory is Fin μ → State n with index 0 the oldest state and index $\mu-1$ the current state; $\mu\ge1$ is a standing assumption (NeZero μ); $n,m\ge0$ are arbitrary and no assumption is placed on the update functions.
• Matrices are indexed by trajectories rather than by the paper's index $j$ of $\delta^j_{2^{\mu n}}$. The paper's $Q=L\ltimes\mathbf 1_{2^m}$ is obtained by the simultaneous relabelling of Lemma 2.6, and every statement (entries of powers, sums over sets of trajectories, Definition 3.7) is invariant under it. $\mathbb Q_{C_t}$ is indexed by the subtype of allowed trajectories.
• Irreducibility is Definition 3.7 applied to the matrix with entries cast to $\mathbb R$; it is not Mathlib's Matrix.IsIrreducible, which differs on $1\times1$ matrices.
• Pinned readings: Definition 3.1 and Definition 4.1 use $k\ge1$; Definition 3.11 uses $k\ge0$; Proposition 3.5, Theorem 4.3 and Theorem 5.1 are stated for $k>0$ (Proposition 3.5 is false at $k=0$ when $y_a=y_b\in C_t$); Remark 3 holds for all $k\ge0$. "Avoiding $C_s$" in Theorem 5.1 means that no state $x(i)$, $i=1-\mu,\dots,k$, lies in $C_s$, which is the theorem's own middle term $\mathbb N_1(k;a,b,\Xi^{C_s})$. $\Xi^p_\mu$ is defined semantically by eq. (4.3), since the printed index range in (4.4) is a misprint. Lemma 3.9 is included in corrected form with $N\ge2$.

Controllability is defined through the dynamics and control sequences, never as positivity of entries of powers of $Q$; a formalization that defines reachability by $(Q^k)_{b,a}>0$ would reduce Theorems 3.10 and 3.12 to library facts and is ruled out.

Needed infrastructure: the correspondence between control sequences and products of entries of $Q$ (the core of Proposition 3.5), and the equivalence of Definition 3.7 with strong connectivity of the support graph for nonnegative matrices (Mathlib's Matrix.IsIrreducible, Matrix.isIrreducible_iff_exists_pow_pos and Matrix.pow_apply_pos_iff_nonempty_path cover much of the second part for sizes at least 2). Both are reusable beyond this mission, for ordinary BCNs, probabilistic BCNs and finite automata. Contributions of either piece, or of the semi-tensor-product bridge identifying $Q$ with $L\ltimes\mathbf 1_{2^m}$, are welcome.

Selected references

• J. Lu, J. Zhong, D. W. C. Ho, Y. Tang, J. Cao, On Controllability of Delayed Boolean Control Networks, SIAM J. Control Optim. 54(2):475–494, 2016. https://doi.org/10.1137/140991820
• D. Cheng, H. Qi, Controllability and observability of Boolean control networks, Automatica 45(7):1659–1667, 2009. https://doi.org/10.1016/j.automatica.2009.03.006
• S. A. Kauffman, Metabolic stability and epigenesis in randomly constructed genetic nets, J. Theoret. Biol. 22(3):437–467, 1969. https://doi.org/10.1016/0022-5193(69)90015-0
• A. Berman, R. J. Plemmons, Nonnegative Matrices in the Mathematical Sciences, SIAM Classics in Applied Mathematics 9, 1994. https://doi.org/10.1137/1.9781611971262

Motivation

This mission formalizes §4 of Cannon, Floyd and Parry's Introductory notes on Richard Thompson's groups, together with the definition of Thompson's group $F$ from their §1. The goal is their Theorem 4.5: the commutator subgroup $[F,F]$ is simple.

In the 1960s Richard Thompson defined three groups, now written $F$, $T$ and $V$, whose properties have kept them in use ever since as a source of examples at the edge of what groups can do. $F$ is the smallest of the three and the least understood. It is finitely presented (§3 of the source) and torsion-free, it has no free subgroup of rank two, and whether it is amenable — whether it carries a finitely additive left-invariant probability measure defined on all its subsets — is open. Cannon, Floyd and Parry record (§4, p. 227) that Geoghegan raised the question and conjectured in 1979 both that $F$ contains no non-Abelian free subgroup and that $F$ is not amenable.

That question is what makes $F$ worth pinning down precisely. Write $AG$ for the class of amenable discrete groups, $EG$ for the elementary amenable ones, and $NF$ for the groups with no free subgroup of rank two. That $AG \subset NF$ was noted by Day and follows from von Neumann; whether it is strict is the von Neumann–Day problem. It is: Olshanskii proved $AG \neq NF$ in a 1984 ICM address and Gromov gave an independent proof — but by examples that are not finitely presented. Brin and Squier proved in 1985 that $F \in NF$, and $F$ is not elementary amenable (Theorem 4.10 of the source, CannonFloydParry.not_elementaryAmenable_F). So $F$ is a finitely presented group in $AG \setminus EG$ if it is amenable and in $NF \setminus AG$ if it is not — a question with no other finitely presented candidate.

Setting

Call a real number dyadic if it has the form $m/2^{k}$ with $m \in \mathbb{Z}$ and $k \in \mathbb{N}$.

Thompson's group $F$, as §1 of the source defines it, is the set of piecewise linear homeomorphisms of the closed unit interval $[0,1]$ onto itself that are differentiable except at finitely many dyadic rationals, and whose derivatives, where they exist, are powers of $2$. Since those derivatives are positive, every element preserves orientation, so the elements of $F$ are increasing. Composition of two such maps is again one, and so is the inverse of one, so $F$ is a group.

The formalization calls such a map piecewise linear over the dyadics, and defines $F$ as the subgroup generated by those maps — so that closure under composition and inverses is a theorem rather than part of the construction, as the source has it. What the model fixes rather than derives is under Formalization scope below.

Two particular elements generate it. Write

$$A(x) = \begin{cases} x/2 & 0 \le x \le \tfrac12\\ x - \tfrac14 & \tfrac12 \le x \le \tfrac34\\ 2x-1 & \tfrac34 \le x \le 1\end{cases} \qquad B(x) = \begin{cases} x & 0 \le x \le \tfrac12 \\ x/2 + \tfrac14 & \tfrac12 \le x \le \tfrac34 \\ x - \tfrac18 & \tfrac34 \le x \le \tfrac78 \\ 2x-1 & \tfrac78 \le x \le 1.\end{cases}$$

An element of $F$ is trivial near $0$ if it fixes every point of some interval $[0,\varepsilon)$, and trivial near $1$ if it fixes every point of some $(1-\varepsilon, 1]$. The support of $f$ is the set of points of $[0,1]$ that $f$ moves. The commutator convention throughout is $[x,y] = xyx^{-1}y^{-1}$, and $[F,F]$ denotes the commutator subgroup.

Formalization targets

Goal

$$[F,F] \ \text{is a simple group.}$$

This is the capstone of §4: it says the commutator subgroup has no normal subgroup other than itself and the trivial one. It is the goal because the rest of the section feeds it — both halves of Theorem 4.1, Theorem 4.3, and both supporting lemmas below are consumed by its proof.

Theorem 4.1, which has two parts

$$[F,F] \;=\; \{\, f \in F : f \text{ is trivial near } 0 \text{ and near } 1 \,\}$$ $$F/[F,F] \;\cong\; \mathbb{Z} \oplus \mathbb{Z}$$

Theorem 4.3

$$N \trianglelefteq F,\ N \neq 1 \;\Longrightarrow\; F/N \text{ is Abelian}$$

So $F$ has no interesting proper quotients at all. With the first part of Theorem 4.1 this forces every nontrivial normal subgroup of $F$ to contain $[F,F]$.

Supporting results

That the piecewise-linear maps are already closed under composition and inverses, so that $F$ consists of exactly those maps; a transitivity lemma on dyadic partitions of $[0,1]$; the fact that the subgroup of elements supported in a dyadic interval $[a,b]$ of dyadic length is isomorphic to $F$ itself; triviality of the center; that $F$ contains no non-Abelian free group; and that $F$ admits a total order invariant under multiplication on both sides.

Significance

What the results give. Theorem 4.1 identifies $[F,F]$ concretely — a subgroup defined by a global algebraic condition turns out to be cut out by local behavior at the two endpoints — and computes the abelianization, making the pair of endpoint slopes a complete invariant of $F$ modulo commutators. Theorem 4.3 and the simplicity of $[F,F]$ together determine the whole normal subgroup lattice: every normal subgroup of $F$ is trivial or contains $[F,F]$. That lattice is the input to the elementary-amenability argument.

What formalizing adds. All of these are proved in the source; none is in Mathlib, which has no piecewise-linear homeomorphism API and no Thompson group. Four of the milestones are proved as part of this proposal: that the piecewise-linear maps form a subgroup, that elements of $F$ permute the dyadic rationals, that $F$ embeds in the group Brin and Squier work with, and the absence of a free subgroup of rank two, which follows from the already-formalized Brin–Squier theorem via that embedding. The rest are open. The piecewise-linear machinery built along the way — local affineness, dyadic-breakpoint bookkeeping, extension by the identity — is reusable for $T$, for $V$, and for the wider family of piecewise-linear homeomorphism groups.

Difficulty

The obvious approach to the goal is to argue that a normal subgroup of $[F,F]$ containing a nontrivial element must be everything, by conjugating that element around. It fails on its own: an element of $[F,F]$ is pinned down only by being trivial near the two endpoints, and one still has to manufacture — inside $[F,F]$, not merely inside $F$ — an element carrying a prescribed pair of neighborhoods into those. That construction is what the dyadic-partition transitivity lemma supplies, and it is where the combinatorics of dyadic subdivision enters.

The second difficulty was that the source proves §4 using the tree-diagram normal form of §2. That section is now formalized in its own mission, Cannon–Floyd–Parry §2: tree diagrams and the normal form (mission ffd1e4ea-9f9a-4cb6-8419-78e70f2545e8), all of whose milestones are proved. Corollary 2.6 — milestone 5 here, the same theorem object — is closed from there, and Theorem 2.5 (represents_word_exponents) and the normal form (existsUnique_normalForm) are available to a solver attacking Theorem 4.3, so the source's argument can now be followed. A solution file imports only definitions, so whatever it uses from §2 must be reproved inline; the §2 solutions are public and written to be reused that way. The piecewise-linear route — dyadic-partition transitivity, Lemma 4.4 and Theorem 4.1 — remains an alternative, and is what Theorem 4.5's own argument uses.

Formalization scope

The unit interval is $[0,1] \subseteq \mathbb{R}$ as a subtype, and an element of $F$ is an order isomorphism of it, so orientation preservation is built into the representation rather than derived — faithful to the source's set, but assuming one sentence CFP prove. Piecewise linearity is stated as: there is a finite set $B$ of dyadic reals such that the map is affine, with slope a power of two, on every closed interval whose interior misses $B$. Intercepts are not required to be dyadic — that is derived by induction along the breakpoints, not part of the definition.

The definition is not vacuous: $A$ and $B$ of Example 1.1 are constructed explicitly, and that $F$ is not the trivial group is one of the milestones below — so no statement here is satisfied by the trivial group. In particular the goal, which asserts simplicity and therefore nontriviality, is not trivially false.

A companion definition places the same data on the real line, each element extended by the identity outside $[0,1]$; that line realisation is what the bridge statement connects to Brin and Squier's group.

Selected references

• J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique (2) 42 (1996), 215–256. doi:10.5169/seals-87877
• M. G. Brin, C. C. Squier, Groups of piecewise linear homeomorphisms of the real line, Inventiones Mathematicae 79 (1985), 485–498. doi:10.1007/BF01388519
• C. Chou, Elementary amenable groups, Illinois Journal of Mathematics 24 (1980), 396–407. doi:10.1215/ijm/1256047608
• M. M. Day, Amenable semigroups, Illinois Journal of Mathematics 1 (1957), 509–544. doi:10.1215/ijm/1255380675
• J. von Neumann, Zur allgemeinen Theorie des Maßes, Fundamenta Mathematicae 13 (1929), 73–116. doi:10.4064/fm-13-1-73-116
• A. Yu. Olshanskii, On a geometric method in the combinatorial group theory, Proceedings of the International Congress of Mathematicians (Warsaw, 1983), vol. 1, 1984, pp. 415–424. IMU archive
• M. Gromov, Hyperbolic groups, in Essays in Group Theory (S. M. Gersten, ed.), MSRI Publications 8, Springer, 1987, pp. 75–263. doi:10.1007/978-1-4613-9586-7_3

Motivation

Markets with network externalities can support several levels of adoption at the same price. A consumer's willingness to buy may rise when many other consumers buy, while the ordinary price effect still works in the opposite direction. A price and an aggregate demand curve can therefore identify several self-consistent quantities without identifying which one consumers reach. In Network Externalities and Market Dominance, Akerlof, Holden and Rayo study this selection problem before analyzing firms' pricing decisions (accepted manuscript, §2.1).

The paper uses an introspective equilibrium: consumers begin with an impulse about firm 1's sales and repeatedly revise consumption in response to the previous level. The resulting limit gives a selection rule tied to an observable starting condition rather than to an arbitrary choice among fixed points. The mission formalizes Proposition 1 of the accepted manuscript, dated September 16, 2022. Its source is the repository manuscript; the numbering and printed pages here refer to that artifact, not the journal typesetting (Akerlof, Holden and Rayo, Proposition 1, p. 10).

Setting

There is a unit mass of consumers, each with unit demand. Write $p=p_1-p_2$ for firm 1's relative price, and let $Q\in[0,1]$ be its current total sales. The aggregate demand $D(p,Q)\in[0,1]$ is the quantity that would be demanded at price $p$ if consumers believed sales were $Q$. With one firm, the paper sets the second firm's price and quantity to zero, so the same two-argument demand map applies. With two firms, $p$ is the difference of their prices. An equilibrium quantity is a feasible fixed point,

$$Q=D(p,Q).$$

The inverse demand curve $P$ gives a price at which a given quantity is self-consistent: $D(P(Q),Q)=Q$ for $Q\in[0,1]$. The market assumptions say demand is continuous in price and feasible quantity, decreases with price, and increases with believed quantity. The formal market records weak monotonicity together with strict price comparisons at an inverse-demand point on the nonsaturated part of the range. These comparisons give the signs used in the paper's footnote 12 (§2, p. 5; footnote 12, p. 10).

An In/Out curve has two quantity thresholds $0<Q_L<Q_H<1$. The curve $P$ is strictly decreasing and convex on $[0,Q_L]$, strictly increasing on $[Q_L,Q_H]$, and strictly decreasing and concave on $[Q_H,1]$; convexity and concavity here are weak. Define $p_{\min}=P(Q_L)$ and $p_{\max}=P(Q_H)$. The endpoint conditions are $p_{\max}<P(0)$ and $P(1)<p_{\min}$. At a price between the thresholds, the intersections of $P(Q)=p$ with the three branches are $Q^{\mathrm{out}}(p)$, $Q^{\mathrm{mid}}(p)$, and $Q^{\mathrm{in}}(p)$. At either threshold price, two adjacent branch labels can name the same quantity (footnote 7, p. 6; §2.1, p. 8).

The consumers' impulse $I_0$ lies in $[0,1]$. Level-$k$ consumption is the actual iteration $I_k=D(p,I_{k-1})$, or $I_k=D(p,\cdot)^{\circ k}(I_0)$ with $I_0$ at level zero. An introspective equilibrium $Q_1^*$ is the limit of this sequence as $k\to\infty$ (Definition 1, p. 9).

Formalization targets

Equilibrium structure

For $p_{\min}<p<p_{\max}$, the three branch quantities are distinct and exhaust the feasible equilibrium quantities. At $p=p_{\min}$ or $p=p_{\max}$, two distinct quantities remain. The milestone from §2.1 also records uniqueness within each branch. Footnote 12 records where $D(p,Q)$ lies above or below $Q$ between these intersections (§2.1, p. 8; footnote 12, p. 10).

Selection rule

The goal is the full two-part Proposition 1. When $p_{\min}\le p\le p_{\max}$, the branch equilibria exist and

$$Q_1^*(p)= \begin{cases} Q^{\mathrm{in}}(p),&I_0>Q^{\mathrm{mid}}(p),\\ Q^{\mathrm{mid}}(p),&I_0=Q^{\mathrm{mid}}(p),\\ Q^{\mathrm{out}}(p),&I_0<Q^{\mathrm{mid}}(p). \end{cases}$$

When $p>p_{\max}$ or $p<p_{\min}$, exactly one feasible quantity solves $Q=D(p,Q)$, and $I_k$ converges to it for every $I_0\in[0,1]$. The proof's convergence and uniqueness passages are separate milestones, so the goal retains both claims without taking either as an extra assumption (Proposition 1 and proof, p. 10).

Significance

Proposition 1 ties a market's adoption outcome to the initial impulse. In the multiple-equilibrium price range, the middle equilibrium separates impulses that select the low and high quantities; outside that range, the selected quantity is independent of the impulse. This makes the refinement usable when the subsequent economic analysis asks how a price or a change in expectations can move the market between dominant firms (§2.1–§3).

The paper proves the result in ordinary mathematics. The remaining work here is a machine-checked proof of its precise selection statement and of the source passages that support it. The definition layer also supplies a reusable interface for continuous aggregate demand and inverse demand on a bounded quantity interval. There is no claim that this paper's later pricing-game propositions have already been formalized.

Difficulty

The inverse-demand picture shows three crossings, but a picture alone does not establish that every branch crossing exists or that no additional feasible fixed point is present. At a threshold, two branch labels meet, so a claim that always demands three distinct quantities would be false. Outside the threshold interval, the paper's reference to a unique intersection of $P(Q)=p$ fails at prices beyond $P(0)$ or $P(1)$: the equilibrium can instead be a saturated fixed point at $0$ or $1$. The formal statements must cover those prices with $D(p,Q)=Q$ (Proposition 1 and proof, p. 10).

The convergence claim concerns a specific recursive sequence from every allowed impulse. Fixed-point existence by itself does not identify that limit or its dependence on the impulse. The market assumptions also require care at the saturation endpoints: strict decrease in price on the whole real line would conflict with nonnegative demand at $Q=0$, while merely weak decrease permits extra fixed points that would defeat the selection claim.

Formalization scope

Lean represents prices and quantities by real numbers and restricts feasible quantities and impulses to $[0,1]$. A Market stores $D$, $P$, continuity of $D$ on real prices and feasible quantities, range bounds, weak monotonicity in quantity and price, the inverse-demand identity, and the strict nonsaturation signs from footnote 12. The paper says demand is strictly increasing in quantity below $1$; the formal interface uses weak increase because its own saturated consumer model can have a constant zero-demand segment. The strict price signs make explicit the stronger reading of “decreasing” needed at inverse-demand points. Both choices are disclosed in the setting item. The polynomial and clamped-demand example in the local verification file witnesses that the assumptions are consistent.

IsInOut retains every monotonicity, convexity, concavity, threshold-order, and endpoint condition of footnote 7, even when a clause is unused in a proof. The branch quantities are predicates that include their intervals and the equation $P(Q)=p$; the goal asserts their existence before quantifying over them. IsIntrospectiveEq uses Function.iterate and Tendsto for the prescribed $I_k$, so it cannot be satisfied by selecting an unrelated fixed point or sequence. Outside the threshold interval, uniqueness is over feasible fixed points of $D$, including $0$ and $1$. The assumptions apply to the aggregate map for either one or two firms; consumer types, their distribution, the micro-foundations, the firms' pricing game, profits, the WIN constraint, Corollary 1, and later sections are outside this mission.

A complete development needs continuity and intermediate-value results, monotonicity and convexity of real functions on intervals, and convergence of bounded sequences of real numbers. The market and level-$k$ definitions can be reused by later work on equilibrium selection. Contributions may prove the listed milestones, supply independent proofs of Proposition 1, or build the interval-dynamics lemmas they require, while retaining the statement's full price and impulse domains.

Selected references

• R. Akerlof, R. Holden and L. Rayo, Network Externalities and Market Dominance, author's accepted manuscript, WRAP 178238, dated September 16, 2022; published in Management Science (2024). Accepted manuscript; DOI.

Motivation

In 2018 New York City's Taxi and Limousine Commission adopted a minimum earnings rule for ride-hailing drivers: each platform must pay drivers, per hour spent with a passenger, at least a target hourly earnings level divided by the platform's measured driver utilization in the previous period. The rule ties next period's wage floor to this period's idle time, so a platform that over-recruits drivers must raise wages. Asadpour, Lobel and van Ryzin (SSRN 3502607, published in Manufacturing & Service Operations Management, 2022) model this rule as a dynamical system and ask when the regulated marketplace can stay stable, meaning wages stay bounded while the platform does not lose money.

Their main result (Theorem 1, a separate mission of this series) characterizes stability in a deterministic market. Real markets are hit by demand shocks: a sudden drop in ride requests lowers utilization in one period, and the rule then forces a high wage in the next. This mission formalizes the paper's answer (Theorem 2, §4.1) to whether a platform that may not subsidize rides can absorb such a one-time shock.

Setting

Time is discrete. In each period $t$ the platform chooses a price $p_t \ge 0$ per ride hour and a wage $w_t \ge 0$ per ride hour. The demand $D(p)$ is the number of ride hours requested at price $p$; the supply $S(z)$ is the number of driver hours offered when drivers earn $z$ per hour. Rides served are $Q(p,z) = \min\{D(p), S(z)\}$, the utilization is $u(p,z) = Q(p,z)/S(z)$, and drivers' hourly earnings $z_t$ solve the equilibrium condition

$$z_t = w_t \, u(p_t, z_t).$$

A price, wage and earnings sequence satisfying this in every period is an equilibrium-augmented policy. The platform's profit is $\pi(p,w,z) = (p-w)\,Q(p,z)$. With target $M > 0$, the minimum earnings rule requires

$$w_{t+1} \ge \frac{M}{u(p_t, z_t)} \quad \text{in every period.}$$

The revenue and cost functions are $R(p) = p\,D(p)$ and $C(z) = z\,S(z)$. The paper assumes $D$ positive, strictly decreasing and continuous; $S$ strictly increasing, continuous, and positive and differentiable away from $0$; $R$ unimodal with maximum at $p^*$; and demand and supply crossing at $w^*$, $D(w^*) = S(w^*)$. $H$ is the inverse of $C$, and $J$ is the inverse of $R$ on its decreasing branch: $J(r) = p$ iff $p \ge p^*$ and $R(p) = r$.

A shock lowers utilization to $u_0$ in one period. A marketplace absorbs a $u_0$ utilization shock (Definition 3) if some feasible equilibrium-augmented policy obeying the rule, with first post-shock wage $w_1 \ge M/u_0$, has bounded wages and non-negative profit in every period.

Formalization targets

Goal: Theorem 2

$$\text{the marketplace absorbs a } u_0 \text{ utilization shock} \iff u_0 \ge \frac{M}{J(C(M))}.$$

The threshold is explicit in the model primitives; no constant is chosen by the formalization.

Milestones (the steps of the published proof, Online Appendix p. 5)

1. If $u_0 < M/J(C(M))$ and $w_1 \ge M/u_0$, then $M/H(R(w_1)) \ge \phi(M,u_0) > 1$, where $\phi(M,u_0) = M/H(R(M/u_0))$.
2. Along a policy with $p = w$ after such a shock, $w_{t+1} \ge \phi(M,u_0)\,w_t$, hence $w_t \ge \phi(M,u_0)^{t-1} w_1$.
3. If $u_0 \ge M/J(C(M))$, then at $p = w = J(C(M))$ and $z = M$: $z/w = D(p)/S(z) = u(p,z)$, so $z = M$ is an equilibrium.

Significance

The result. Theorem 2 quantifies the fragility of a regulated marketplace whose platform cannot cross-subsidize: there is a sharp utilization level below which a single shock sends wages into unbounded growth, and above which the platform recovers immediately with a zero-profit stationary policy. Its threshold depends on the market only through the decreasing branch of revenue and the cost of paying $M$, which makes it a concrete design criterion for the target $M$: a regulator choosing $M$ also chooses how deep a utilization drop the market can survive. The remark after the theorem (p. 14) relates it to the stability threshold of Theorem 1.

Formalizing it. The result is proved in the paper; no machine-checked version exists. A formal proof must close points the published argument leaves implicit: the reduction to $p = w$ policies (the paper's Lemma 3, posed in mission I) must hold in the all-periods form used here; the wage recursion of Lemma 4 needs wages above $w^*$, which the proof does not check; and the sufficiency policy needs $J(C(M)) \ge M$, which holds only because utilizations are at most one. The mission also gives the platform a second, independent use of the shared marketplace model.

Difficulty

The sufficiency direction is a direct check of one stationary policy. The necessity direction is where the work lies. The natural attempt, to argue that a high first wage simply cannot be paid without loss, fails: profit only requires $p_t \ge w_t$, and a platform may raise its price along with the wage. The obstruction is dynamic. Raising the price above $J(C(M))$ lowers revenue below the cost of supplying earnings $M$, so equilibrium earnings fall below $M$, utilization falls, and the rule raises the next wage by a factor bounded away from one. Turning this into a proof requires controlling arbitrary policies with $p_t \ge w_t$, not just the convenient $p = w$, and carrying an induction hypothesis (wages stay above $M/u_0$) that the paper does not state.

Formalization scope

The Lean development lives in namespace MinEarnings.Shock. Demand and supply are functions D S : ℝ → ℝ; all regularity is required on $[0,\infty)$, and "differentiable" is read as differentiable on $(0,\infty)$, which is all the argument uses. "$R$ unimodal with maximum at $p^*$" is strict increase on $[0,p^*]$ and strict decrease on $[p^*,\infty)$. The points $p^*$, $w^*$ and the inverse cost $H$ are parameters carrying their defining properties. Time is 0-based: Lean's period $0$ is the paper's period $1$, so the shock constraint $w_1 \ge M/u_0$ is a bound on Lean's first wage and the rule constrains every later wage. Bounded wages means $\exists B\ \forall t,\ w_t \le B$, and profit is non-negative in every period.

Three conventions are pinned and disclosed in every statement:

• $J(C(M))$ is not defined as a function. It is passed as a price $q$ with $q \ge p^*$ and $R(q) = C(M)$, which determines it uniquely. The paper's $J$ is defined on $(0, R(p^*)]$, which presumes $R(p) \to 0$, an assumption the paper does not make.
• The shock utilization satisfies $0 < u_0 \le 1$. Without $u_0 \le 1$, which Definition 3 leaves implicit, the sufficiency direction fails when $p^* \le w^* < M$.
• Equilibrium earnings are positive, $z_t > 0$. Lean defines $0/0 = 0$, so a zero-earnings "equilibrium" with $S(0) = 0$ would have utilization $0$ and turn the rule into $M/0 = 0 \le w_{t+1}$; the positivity requirement rules out this trivializing reading, and the requirement that wages be bounded uniformly rules out a vacuous reading of stability.

The development needs only Mathlib's real analysis: monotonicity on intervals, inverse functions on $(0,\infty)$, and geometric growth of sequences. The setting file is shared, up to namespace, with the other two missions of the series. Contributions welcome: proofs of the milestones, a proof of the all-periods reduction to $p = w$ policies, and a general lemma that a sequence with $w_{t+1} \ge \phi w_t$, $\phi > 1$, $w_0 > 0$ is unbounded.

Selected references

• A. Asadpour, I. Lobel, G. van Ryzin, Minimum Earnings Regulation and the Stability of Marketplaces, SSRN 3502607 (version of August 24, 2022); Manufacturing & Service Operations Management, 2022. https://ssrn.com/abstract=3502607 · https://doi.org/10.1287/msom.2022.1150

Utilization-based minimum earnings rules

In 2018 New York City's Taxi and Limousine Commission (TLC) imposed a minimum pay formula on the largest ride-hailing platforms, following a proposal by Parrott and Reich (2018): the pay per minute and per mile driven is divided by the platform's utilization rate, the fraction of drivers' working time spent carrying passengers. Seattle adopted a similar rule in 2020. The rule targets drivers' hourly earnings while leaving them free to choose when and how much to work. Because utilization is only observed after the fact, the regulation computes the floor for the next measurement period (six months in New York) from the utilization of the current one.

Asadpour, Lobel and van Ryzin (2022) model this rule as a dynamic system and ask when a platform can comply with it while keeping wages bounded and profits non-negative. This mission formalizes their Theorem 3: the lag in the rule does not matter for stability, because the dynamic system is stable exactly when a single static system of equations has a solution. Two companion missions of the series formalize Theorem 1 (the threshold $z^*$ on stable earnings targets) and Theorem 2 (absorption of a utilization shock).

Setting

Time is discrete. In period $t$ the platform charges riders a price $p_t \ge 0$ per hour of driving and pays drivers a wage $w_t \ge 0$ per hour of driving riders. A demand function $D$ gives the ride hours demanded at price $p$, and a supply function $S$ gives the driver hours offered at expected hourly earnings $z$. The regularity assumptions are that $D$ is positive, strictly decreasing and continuous, and $S$ is strictly increasing, continuous, and positive and differentiable away from zero. The ride hours produced, the utilization and the platform's profit are

$$Q(p,z)=\min\{D(p),S(z)\},\qquad u(p,z)=\frac{Q(p,z)}{S(z)},\qquad \pi(p,w,z)=(p-w)\,Q(p,z).$$

Drivers earn $w_t$ only while busy, so earnings satisfy the equilibrium condition $z_t = w_t\,u(p_t,z_t)$. The minimum earnings rule with target $M>0$ is

$$w_{t+1}\ \ge\ \frac{M}{u(p_t,z_t)}\qquad\text{for every period } t.$$

The $M$-minimum-earnings marketplace is stable if some policy $(p_t,w_t,z_t)$ that is feasible, satisfies the equilibrium condition and obeys the rule has a bounded wage sequence and $\pi(p_t,w_t,z_t)\ge 0$ in all but finitely many periods. It is statically stable if there are $p,w,z\ge 0$ and $u\in(0,1]$ with

$$u=\frac{Q(p,z)}{S(z)},\qquad z=w\,u,\qquad w\ge\frac{M}{u},\qquad p\ge w. \tag{8}$$

Formalization targets

Goal: Theorem 3

$$\text{the } M\text{-minimum-earnings marketplace is stable}\iff\text{it is statically stable}.$$

The statement carries only the regularity assumptions on $D$ and $S$ and $M>0$.

Milestones

The milestones follow the proof in the Online Appendix.

1. A statically stable marketplace is stable.
2. Along a policy with $p_t = w_t$ that satisfies the equilibrium condition and the rule, if $u_{t+1}\ge u_t$ for some $t$, the marketplace is statically stable.
3. Along the same kind of policy, if $w_t\ge M/u_t$ for some $t$, the marketplace is statically stable.
4. If neither case occurs and wages are bounded, then $w_t\to w$ and $u_t\to u$, and the limits satisfy $0<u\le 1$, $w\ge M/u$ and $u = Q(w,wu)/S(wu)$.

Significance

Theorem 3 reduces a question about infinite sequences to a question about one system of four relations in four unknowns. The paper uses it to give a second proof of its threshold theorem, and it shows that the lag in the regulation cannot be blamed for instability: every earnings target that a real-time rule could sustain can also be sustained under the lagged rule, and conversely. This gives regulators and platforms a criterion that can be checked by solving equations rather than by simulating policies.

The result is proved in the paper. No machine-checked version of it or of the paper's other results exists. Formalizing it checks the passage to the limit in the dynamic-to-static direction, where the paper leaves one step implicit (the positivity of the limiting utilization), and it provides a Lean model of the regulated marketplace that the other two missions of the series share.

Difficulty

The static-to-dynamic direction is immediate. In the other direction, a stable policy is a sequence, and a solution of (8) is a single point. Fixing one period of a stable policy does not give such a point: the rule compares $w_{t+1}$ with $u_t$, while (8) compares $w$ with the utilization of the same point. A solution has to be extracted either from a period where the comparison happens to go the right way or from a limit. The limit is delicate because the utilization $Q(p,z)/S(z)$ is a ratio, and a limit with $u = 0$ would not solve (8). The positivity of the limiting utilization has to come from the rule and the bound on wages together. The reduction to policies with $p_t = w_t$ (Lemma 3 of the paper) also has to be carried out on the policy before the case analysis can start; that lemma is posed as a milestone of the first mission of this series and is not repeated here.

Formalization scope

Prices, wages and earnings are real numbers, and $D, S : \mathbb{R}\to\mathbb{R}$ are constrained on $[0,\infty)$. A policy is a triple of sequences indexed by $\mathbb{N}$ starting at $0$, so Lean's period $t$ is the paper's period $t+1$, and the rule constrains every wage except the first. "Bounded" is an upper bound on the wages, which are non-negative; "all but finitely many periods" is an eventually-along-atTop statement. "Differentiable" is read as differentiability on $(0,\infty)$ together with continuity on $[0,\infty)$.

The equilibrium condition requires $z_t>0$. Without it the encoding is trivial: if $S(0)=0$, which the assumptions allow, Lean evaluates $u(p,0)=0/0$ as $0$, the rule becomes $0\le w_{t+1}$, and every target $M$ would count as stable. For the same reason Definition 4's $u\in(0,1]$ is kept with its strict lower bound. The paper's standing assumptions that the revenue $pD(p)$ is unimodal and that $D$ and $S$ cross are not used by Theorem 3 or its proof and are not assumed, so the formal statements are slightly more general than the paper's.

A complete development needs basic real analysis from Mathlib (monotone convergence, continuity of $D$, $S$ and $\min$, limits of quotients) and the equilibrium construction behind Lemma 3, which uses the inverse of the cost function $C(z)=zS(z)$. That construction is reusable across the series. Proofs of the milestones, of the $p=w$ reduction, and of the goal are all welcome.

Selected references

• A. Asadpour, I. Lobel, G. van Ryzin, Minimum Earnings Regulation and the Stability of Marketplaces, SSRN 3502607 (version of August 24, 2022); Theorem 3 on p. 15, proof in Online Appendix pp. 5–6. https://ssrn.com/abstract=3502607
• A. Asadpour, I. Lobel, G. van Ryzin, Minimum Earnings Regulation and the Stability of Marketplaces, Manufacturing & Service Operations Management, 2022. https://doi.org/10.1287/msom.2022.1150
• J. A. Parrott, M. Reich, An Earnings Standard for New York City's App-based Drivers: Economic Analysis and Policy Assessment, report for the New York City Taxi and Limousine Commission, 2018 (cited in the paper as Parrott and Reich [2018]).