Why Problems Are Hard: The Fibred Order of Difficulty

Difficulty is often spoken of as though it were stored inside a problem. A conjecture is hard, a landscape is rugged, a system is complex. Yet the same calculation is routine with writable memory and impossible for a fixed finite machine that must retain an unbounded input. The same state is recoverable through one sensor and indistinguishable through another. The same target is reachable with one actuator and absent from the closure of another move set.

The object has not changed in these comparisons. The encounter with it has.

This does not make difficulty imaginary. A locked door does not open under a better description. A false conjecture does not become true for a weak prover. Noise can blur distinctions and can sometimes erase them exactly, whether or not an observer understands why. A path that exists may still pass through a forbidden state. The position of this book is relational and realist at once: difficulty depends on a specified relation, and the truth about that relation is not chosen by the agent.

The relation has three operational boundaries, each evaluated relative to a declared instance, environment, and model-uncertainty class. An information boundary determines which differences can enter a representation. An action boundary determines which states can be reached. A resource boundary determines which attainable performance can be realized in time, memory, communication, precision, or energy. Language matters too, but not as a mysterious fourth substance. A vocabulary changes which tasks and distinctions have been specified in the first place.

The organizing object is therefore not a universal scale but a fibred order. For each comparison context, all subsets of its performance space form an ambient order, while actual encounters realize only a subposet. Performance maps reindex the ambient orders by preimage and permit heterogeneous comparisons of given encounters. They reindex the realized difficulty classes only when a closure theorem says that the preimages are themselves realized.

The central claim is conditional:

A problem is hard only relative to a success condition, an admissible instance and environment family, and declared boundaries on information, action, and resources. Within one comparison context, smaller attainable regions mean greater difficulty. Across contexts, comparing given encounters requires a specified performance translation. Reindexing realized difficulty classes additionally requires preimage closure; choosing transported encounters requires stronger data.

This formulation gives difficulty degrees without pretending that all forms of resistance share one unit. It also separates changes that ordinary speech often confuses. A coordinate change can expose structure while preserving behavior. An abstraction used to return an executable solution can discard structure and therefore owes a return path. A new sensor changes the information boundary. A new actuator changes the action boundary. Discovering a faster algorithm improves achieved performance or our knowledge of the frontier; changing the admitted program class changes the frontier itself. These are different events, even when each is described as making the problem easier. They also support different context translations: some are exact, some reindex only ambient performance claims, and some provide no justified transport of actual problems at all.

The argument proceeds from representation and feedback, through robustness and fault, to reachability, abstraction, and complexity. The mathematics is used locally. No universal datatype is offered for every problem, and no machine-checked theorem is allowed to stand in for the philosophical argument that gives it a reading.

Chapter 1Representation is a state in a feedback loop

Description and operative state

A representation can be a sentence, diagram, coordinate system, probability distribution, learned feature vector, proof library, or physical mark. These objects differ too much for a single useful syntax. What matters here is a narrower role: an operative representation is whatever state carries selected consequences of past interaction into the next inference or action.

Let \(X\) be a task-relevant exogenous unknown and let \(Y_1,Y_2,\ldots\) be observations. The information theorem below does not cover a future target state that the actions themselves causally alter; such a problem needs a causal or directed-information formulation. Put every random coin used by the estimator or sensing policy into a random tape \(W\), assumed independent of the pair \((X,Z_0)\), and write \(H_0=(Z_0,W)\). At round \(t\), write the maintained representation as

\[ Z_t=q_t(H_0,Y_1,\ldots,Y_t). \]

The map \(q_t\) is causal. It may describe an observer state, a posterior, a compressed transcript, or an external notebook included in the agent's extended state. An estimate is

\[ \widehat X_t=g_t(Z_t), \]

and an action can be chosen as \(A_t=\pi_t(H_0,Y_{<t})\). The random tape does not initially supply information about the unknown, but it must remain in the history. Once it selects sensing actions, discarding it from a conditional mutual-information expression can make the expression false.

This formulation separates representation quality from the amount of prose used to describe it. A large state can preserve irrelevant distinctions. A small sufficient statistic can preserve exactly those needed by one loss function. Compression is therefore task-relative: the same quotient can be exact for one decision and destructive for another.

There is already a preorder here before probability enters. A deterministic experiment \(o_f\) refines \(o_c\) when \(o_c=k\circ o_f\) for some post-processing map \(k\). Equality of fine reports then forces equality of coarse reports, so the fine compatibility class is smaller. Consequently, every action robust under the coarse report remains robust under the fine one. Mutual factorization preserves the compatibility classes and every robust action set. A two-state quotient can make the inclusion strict by merging states that require different actions. Distinct relabelings can occupy the same position, so antisymmetry requires identifying mutually factoring reports. This deterministic refinement preorder is not the Shannon data-processing inequality used below.

Feedback cannot invent information

Because \(Z_t\) is constructed from the initial state and the transcript, the data-processing inequality gives

\[ I(X;Z_t) \le I(X;H_0,Y_{1:t}) =I(X;H_0)+\sum_{k=1}^{t} I(X;Y_k\mid H_0,Y_{<k}) =I(X;Z_0)+\sum_{k=1}^{t} I(X;Y_k\mid H_0,Y_{<k}). \]

The equality is the chain rule. In an adaptive experiment, the distribution of \(Y_k\) can depend on earlier actions. The conditional information terms must therefore be evaluated under the actual policy, with its random tape in the conditioning set. Calling a sensor noisy is not enough to determine them. Actions generated from the recorded history do not create information about \(X\) by themselves.

For a fixed policy, suppose each round contributes at most \(C\) units of task-relevant information. To obtain a lower bound for an entire experiment class, the same bound must hold uniformly over every admissible adaptive policy. Assume that \(I_0\) and \(C\) are finite, and measure all information with one logarithm base. Then

\[ I(X;Z_t)\le I_0+tC, \qquad I_0=I(X;Z_0). \]

This is an upper bound, not a convergence theorem. A poor update rule may lose information and do worse. The bound says only that no reconstruction can gain more information than entered its causal history.

To connect information with accuracy, fix a distortion \(d(x,\hat x)\) and define the rate-distortion function

\[ R_X(D)= \inf_{P_{\widehat X\mid X}:\,\mathbb E d(X,\widehat X)\le D} I(X;\widehat X). \]

For the real-valued subtraction and division below, also assume that \(R_X(D)\) is finite.

If \(\widehat X_t\) achieves expected distortion at most \(D\), its information about \(X\) is at least \(R_X(D)\). Since \(\widehat X_t\) is computed from \(Z_t\), another application of data processing gives

\[ R_X(D)\le I(X;\widehat X_t)\le I(X;Z_t). \]

For \(C>0\), any estimator meeting this expected-distortion criterion under the declared source law therefore obeys

\[ t\ge \left\lceil \frac{[R_X(D)-I_0]_+}{C} \right\rceil . \]

If the initial representation already contains enough information, this lower bound is zero. If \(C=0\) while \(R_X(D)>I_0\), the target accuracy is unattainable through that declared policy and feedback channel. If the bound on \(C\) is uniform over the admitted policy class, the impossibility is class-wide. The ceiling is not philosophical decoration: observations arrive in whole rounds.

The inequality is deliberately conditional. A defensible application must justify the source distribution, distortion, initial information, experiment class, and per-round bound. Without those choices, \(C\) is merely a letter and \(R_X(D)\) merely a name.

A scalar Gaussian reconstruction

The simplest exact example makes the dependence on noise visible. Let a fixed scalar state have prior

\[ X\sim\mathcal N(m_0,P_0), \]

and let independent observations be

\[ Y_k=X+V_k, \qquad V_k\sim\mathcal N(0,R), \qquad P_0>0, R>0. \]

Gaussian conjugacy adds precision. After \(t\) observations the posterior variance is

\[ P_t=\left(P_0^{-1}+tR^{-1}\right)^{-1}. \]

For a positive target variance \(D\), the condition \(P_t\le D\) requires

\[ t\ge R\left(D^{-1}-P_0^{-1}\right). \]

The integer lower bound is the ceiling of the positive part. Increasing the measurement-noise variance \(R\) increases the number of observations needed for the same reduction in uncertainty. This is the clean core of the Kalman analogy: reconstruction speed is limited by the precision entering through feedback.

Observability is local geometry; detectability is dynamics

The scalar formula is not a theorem about a dynamic Kalman filter. For an LTI system \(\dot x=Ax,\ y=Cx\), observability is tested by the rank of the vertical stack

\[ \mathcal O_L= \begin{bmatrix} C\\ CA\\ \vdots\\ CA^{n-1} \end{bmatrix}. \]

A smooth nonlinear system has no universal matrix with that finite form. For \(\dot x=f(x,u),\ y=h(x)\), let \(f_{\bar u}(x)=f(x,\bar u)\) for each constant admissible input. Let \(\mathcal G\) be the smallest real vector space that contains the output components and is closed under Lie differentiation by every \(f_{\bar u}\). Its observability codistribution is

\[ \mathcal O(x)= \operatorname{span}\{d\phi(x):\phi\in\mathcal G\} \subseteq T_x^*M. \]

For an autonomous system, this is the span of \(d(L_f^k h_j)(x)\). A coordinate matrix made from finitely many such covectors can be useful computationally, but there is no universal \(n-1\) truncation. Controlled systems can require mixed iterated Lie derivatives along all admitted system vector fields, not repeated derivatives along the drift alone.

The Hermann-Krener condition

\[ \dim\mathcal O(x_0)=\dim M \]

is sufficient for local weak observability at \(x_0\). It quantifies over the declared common input experiments; it does not show that one fixed input is informative. The implication is local and is not an unconditional converse. For example, \(\dot x=0,\ y=x^3\) is observable, although \(dh(0)=0\). Full rank near each point also need not imply global observability.

If the full codistribution has constant rank \(r<n\) on a neighborhood, its annihilator

\[ \mathcal N_x=\mathcal O(x)^\circ =\{v\in T_xM:\alpha(v)=0\text{ for every }\alpha\in\mathcal O(x)\} \]

is a smooth \((n-r)\)-dimensional distribution. It is involutive: vector fields that annihilate every \(\phi\in\mathcal G\) have a bracket that does too. Frobenius therefore integrates it into local connected leaves on which every function in \(\mathcal G\) is constant. Under the Hermann-Krener constant-rank hypotheses, points connected within such a leaf are strongly indistinguishable under the admitted controls. Frobenius alone does not make a local leaf a global indistinguishability class. These leaves are generally curved, not linear unobservable subspaces. Rank deficiency at one point supplies only a nonzero kernel of the differential test; it does not establish indistinguishable nearby states, a foliation, or a global quotient.

Observability asks whether output separates states. Detectability asks what happens to distinctions that output does not separate. One incremental form requires two forward-complete trajectories with the same admitted input and the same output history to satisfy

\[ d(x_a(t),x_b(t))\longrightarrow0. \]

In a regular observability decomposition, this is asymptotic convergence of hidden trajectories along each indistinguishability leaf. Mere boundedness is insufficient: two bounded hidden trajectories may remain separated. A fixed positive residual radius is practical detectability. A uniform estimate

\[ \limsup_{t\to\infty}d(x_a(t),x_b(t)) \le\rho(\lVert\delta\rVert_\infty), \qquad \rho(0)=0, \]

is a robust detectability bound relative to the declared disturbance class. Neither is exact asymptotic detectability when the right-hand side is positive. Detectability removes one obstruction to state reconstruction; it does not construct an observer or establish stabilizability, a nonlinear separation principle, or safety.

Indistinguishability is task-relative

Information bounds concern degree. A complementary boundary concerns exact ambiguity. Fix an admissible experiment class. Two states are observationally equivalent when every experiment in that class produces the same law of finite observation histories. No computation on such a history can distinguish the states.

Exact recovery may still be unnecessary. If each state \(x\) admits a set \(A^*(x)\) of acceptable actions, an observation class \(E\) permits a robust choice exactly when

\[ \bigcap_{x\in E} A^*(x)\ne\varnothing. \]

The relevant representation need only preserve distinctions on which acceptable action sets conflict. This is why information must be called task-relevant. Bits about an irrelevant coordinate can be plentiful while a single decision-critical distinction remains absent.

The experiment class is part of the claim. Equivalence under all mathematical history-dependent policies can be finer than equivalence under experiments that a bounded agent can implement. Forgetting that quantifier turns an exact theorem into a claim about a different interface.

Chapter 2Robust reconstruction has a margin

Nominal convergence is not robustness

An observer can converge perfectly inside the model used to design it and fail under small changes in the plant, sensor, or disturbance. This is not one more kind of noise. Noise perturbs observations inside a maintained model. Mismatch means that the maintained state transition or output map is wrong. A fault can be modeled as a disturbance, but only after a fault class and magnitude have been declared.

Consider a nonlinear plant and a Luenberger-type observer written schematically as

\[ x_{t+1}=f_t(x_t,u_t)+w_t, \qquad y_t=h_t(x_t)+v_t, \]

\[ \widehat x_{t+1} =\widehat f_t(\widehat x_t,u_t) +K_t(\widehat x_t) \bigl(y_t-\widehat h_t(\widehat x_t)\bigr). \]

The displayed form guarantees neither local observability nor convergence. Chapter 1's rank condition concerns the plant's output interface, not this observer. Detectability can make exact recovery of hidden directions unnecessary, but convergence of the chosen estimate still needs a separate argument. Suppose such an analysis yields a scalar comparison inequality for the estimation error \(e_t\ge0\):

\[ e_{t+1}\le(q_0+\mu)e_t+\bar d. \]

Here \(q_0\ge0\) is a certified nominal contraction factor, \(\mu\ge0\) bounds the part of model mismatch that scales with current error, and \(\bar d\ge0\) bounds additive effects such as disturbances, sensor noise after observer gain, bias, and bounded fault. There is no universal metric that makes every model difference into this \(\mu\). Deriving the comparison inequality is the system-specific work.

Write \(q=q_0+\mu\). If \(0\le q<1\), iteration gives

\[ e_t\le q^t e_0 +\bar d\sum_{k=0}^{t-1}q^k =q^t\left(e_0-\frac{\bar d}{1-q}\right) +\frac{\bar d}{1-q}. \]

The certified ultimate tube has radius

\[ r_\infty=\frac{\bar d}{1-q_0-\mu}. \]

The two effects of mismatch are now separate. Multiplicative mismatch consumes the nominal contraction margin. Additive disturbance enlarges the upper bound that this comparison argument can certify. The certified tolerance is

\[ \mu<1-q_0. \]

Crossing this boundary invalidates the contraction proof. It does not prove that the actual observer diverges; a sufficient certificate can fail while the system remains stable for other reasons.

The recurrence supplies no matching lower bound. In particular, it does not show that errors below \(r_\infty\) are impossible: cancellation, a smaller realized disturbance, or a sharper analysis may yield them. An actual accuracy floor would require a separate worst-case or minimax lower-bound argument.

The same inequality gives an accuracy condition. To certify \(\limsup_{t\to\infty}e_t\le D\) for \(D>0\), it is sufficient that

\[ \bar d\le D(1-q_0-\mu). \]

Thus faster nominal contraction, mismatch tolerance, and final accuracy share one margin. They cannot be read independently from \(q_0\), \(\mu\), and \(\bar d\). If \(r_\infty<D<e_0\) and \(0<q<1\), the transient bound reaches \(D\) once the natural-number time satisfies

\[ t\ge \left\lceil \frac{\log\bigl((D-r_\infty)/(e_0-r_\infty)\bigr)}{\log q} \right\rceil . \]

If \(D\ge e_0\), time zero already satisfies the bound. The formula makes a familiar tradeoff explicit. Increasing observer gain can reduce a nominal contraction factor while amplifying measurement noise and therefore increasing \(\bar d\). Speed in the noiseless model need not improve the certified robust accuracy guarantee. The finite \(\bar d\) premise is a deterministic bounded-disturbance assumption. Gaussian noise is unbounded and needs a moment or high-probability reformulation.

Changing models and switching regimes

A family of plants \(\{f_\theta,h_\theta:\theta\in\Theta\}\) admits a uniform robust claim only when one common error metric or Lyapunov function gives the comparison inequality over the declared family. If the same bounds \(q<1\) and \(\bar d\) hold at every step, including every admitted switch, then the error tube survives arbitrary variation inside that family. Equal constants proved separately in mode-dependent metrics do not establish that claim. A switching theorem may instead need common Lyapunov data, dwell time, or reset bounds.

Abrupt change can alter the observability codistribution, its rank, or the stability of dynamics along its hidden leaves. No choice of gain repairs a distinction that has disappeared from the output, and detectability of the old model does not automatically transfer. An observer bank can enlarge the hypothesis class and compare residuals across models, but it changes memory, computation, and identification assumptions. It is not robustness for free.

The phrase maximum degree of divergence is therefore meaningful only after a mismatch set and norm have been chosen. Inside a certified set, the comparison inequality supplies a maximum error tube. Outside it, silence is the honest conclusion. Extrapolating the same radius beyond its hypotheses disguises model change as arithmetic.

Accommodation, detection, and isolation

Fault tolerance divides into different claims. Accommodation means that the estimator or controller retains an accuracy or safety guarantee while the fault lies in an admissible class. The error tube above is an accommodation result when fault effects are included in \(\bar d\).

Detection asks whether a fault can be distinguished from ordinary uncertainty. Let a residual be

\[ r_t=y_t-\widehat h_t(\widehat x_t). \]

Suppose every healthy residual satisfies \(\lVert r_t^h\rVert\le\rho\), and a faulty residual has the additive form \(r_t^f=r_t^h+f\). Declare an alarm when \(\lVert r_t\rVert>\eta\). A threshold \(\eta\ge\rho\) avoids false alarms under that deterministic model. The reverse triangle inequality gives the worst-case sufficient condition

\[ \lVert f\rVert-\rho>\eta. \]

At the smallest threshold certified from this radius bound alone, \(\eta=\rho\), the familiar condition is

\[ \lVert f\rVert>2\rho. \]

This factor of two is a worst-case separation of uncertainty tubes. It can be conservative when healthy residuals occupy a smaller or asymmetric set, and it is not a probabilistic false-alarm guarantee unless a probability model is added.

Isolation asks which fault occurred. It requires the residual sets of candidate faults to be separated from one another, not merely from the healthy set. A fault may be detectable and still indistinguishable from another fault. If candidate \(i\) produces residuals in a closed ball of radius \(\rho\) around a signature \(f_i\), then \(\lVert f_i-f_j\rVert>2\rho\) makes the two candidate balls disjoint. This is a sufficient deterministic isolation margin, not an exhaustive diagnosis model. The same geometry that governs task-relevant representation returns here: diagnosis is possible only when the observation interface preserves the distinctions the diagnosis is asked to make.

Robust reconstruction therefore has an informational boundary and a dynamical boundary. Observability determines which distinctions can enter the output, and information rate limits how quickly recoverable uncertainty can contract. Detectability asks whether the remaining ambiguity decays; stability margin limits how much mismatch and disturbance that contraction can tolerate. Neither boundary can be replaced by confidence reported from inside the maintained model.

Chapter 3Knowing does not create a path

Reachability is generated by actions

Let \(X\) be a state space and let each primitive action \(u\in U\) induce a transition \(F_u:X\to X\). The states reachable from \(x\) are

\[ \operatorname{Reach}_U(x) =\{F_{u_n}\circ\cdots\circ F_{u_1}(x):n\ge0,\ u_i\in U\}. \]

The empty composition includes \(x\). This set depends on the action boundary, not on how clearly the agent represents it. A complete map can settle whether a target is reachable and can shorten search, but it does not add an endpoint to the closure.

A derived action \(g\) also need not enlarge reachability. If

\[ g(x)\in\operatorname{Reach}_U(x) \quad\text{for every }x, \]

then treating \(g\) as one primitive step changes program length but not the reachable set. This condition is weaker than having one uniform finite macro for \(g\): the witnessing path may depend on \(x\), may have no common length bound, and may be noncomputable. A genuinely new actuator can enlarge reachability, but then the action boundary has changed.

This separates epistemic and practical obstruction. A state can be perfectly known and unreachable. A state can be reachable while the agent lacks enough information to choose the path. The two failures can coexist, but neither explains the other.

Barrier depth is not search time

Reachability says that some path exists. It does not say what every path must cross. Let \(J:X\to\mathbb R\) be an objective, with larger values preferred, and let \(\gamma\) range over finite admissible paths from \(x\) to a goal set \(G\). Define the depth of a path relative to its starting value by

\[ \operatorname{depth}_J(\gamma) =\max_i [J(x)-J(\gamma_i)]_+, \]

and define the barrier

\[ B_J(x,G) =\inf_{\gamma:x\leadsto G}\operatorname{depth}_J(\gamma), \]

with value \(+\infty\) when there is no path.

A zero barrier means that paths can avoid a drop below the starting objective arbitrarily closely; under a witnessed monotone path it is exactly zero. A finite positive barrier means every path dips. An infinite barrier means no path exists. These are statements about the declared adjacency relation and objective.

Barrier depth is a bottleneck statistic, not a general cost. It does not count steps, integrate energy, give escape probability, or bound the computation needed to find a path. A path can have zero depth and astronomical length. A short path can have a deep dip. A stochastic local search rule can fail to find a shallow route. Search, traversal, and bottleneck depth require separate models.

The representation of a path can hide this distinction. An abstract edge may stand for a long concrete route. It preserves reachability if that route exists, but it preserves barrier depth only if the route satisfies an appropriate score bound. This is the point at which abstraction incurs a debt.

Chapter 4Behavior comes before its presentation

Systems as admitted trajectories

A differential equation, automaton, state-space realization, and input/output split are presentations of a system. The behavioral stance begins instead with a time domain \(T\), a declared signal space \(W\), and a set of admissible trajectories

\[ \Sigma=(T,W,\mathcal B), \qquad \mathcal B\subseteq W^T. \]

Equations matter insofar as they characterize \(\mathcal B\). Distinct internal models can present the same behavior at the declared signal boundary, even when one exposes a useful proof or algorithm that another hides. This is representation independence, not model independence: the chosen variables, boundary, and admitted trajectories can still misdescribe the plant.

When two components constrain the same signal universe, their behavioral interconnection is

\[ \mathcal B_1\parallel\mathcal B_2 =\mathcal B_1\cap\mathcal B_2. \]

If only some variables are shared, composition instead enforces compatibility over that interface, represented by a pullback or fibre product. Hiding a signal through \(\pi:W\to V\) takes the existential image

\[ \pi_*\mathcal B =\{\pi\circ w:w\in\mathcal B\}. \]

Interconnection removes trajectories; hiding identifies them. The operations do not generally commute:

\[ \pi_*(\mathcal B_1\cap\mathcal B_2) \subseteq \pi_*\mathcal B_1\cap\pi_*\mathcal B_2, \]

and the inclusion can be strict because the two projected memberships may use incompatible hidden witnesses. Two nonempty components can even have an empty interconnection. Composition therefore needs both compatibility and viability, not merely componentwise possibility.

An exact coordinate change transports a presentation while preserving the admitted behavior. An abstraction is many-to-one and can identify or introduce behavioral possibilities unless transfer conditions are proved. An extension adds a sensor, actuator, predicate, variable, oracle, or axiom and therefore changes the encounter.

The two directions of transfer

Let \(x\to_X x'\) and \(a\to_A a'\) be concrete and abstract step relations. Forward simulation requires

\[ x\to_X x' \quad\Longrightarrow\quad \phi(x)\to_A\phi(x'). \]

It maps every concrete path to an abstract path. With preservation of goals, it proves that concrete success implies abstract success. Its contrapositive can certify concrete impossibility from abstract impossibility.

It does not justify executing an abstract plan. For that direction, a local step-lifting condition is needed:

\[ \phi(x)\to_A a' \quad\Longrightarrow\quad \exists x',\ x\to_X x'\ \text{ and }\ \phi(x')=a'. \]

The quantifier starts from the particular current state \(x\). It is not enough that some convenient representative of the same abstract cell can realize the step. Induction then lifts a finite abstract path one step at a time.

Goals need both directions as well. For concrete goal \(G_X\) and abstract goal \(G_A\), exact reachability transfer uses

\[ x\in G_X\quad\Longleftrightarrow\quad\phi(x)\in G_A. \]

Forward simulation, step lifting, and goal equivalence together give

\[ x\leadsto_X G_X \quad\Longleftrightarrow\quad \phi(x)\leadsto_A G_A. \]

Each premise has distinct work. Forward simulation gives sound abstract images of concrete behavior. Lifting prevents spurious abstract plans. Goal reflection prevents a non-goal concrete state from being declared successful only because its cell contains a goal.

The conditions are intentionally strong. Approximate abstractions replace equalities with error, simulation, or value bounds. Probabilistic abstractions compare kernels or distributions. Safety, cost, and barrier preservation need their own premises. Reachability equivalence alone proves none of them.

Local behavior and safety

Let \(\mathcal B(U)\) denote trajectories admitted on a region \(U\) of time. Restriction to smaller regions gives presheaf-like data. Raw functions on two regions have a unique function-level glue when they agree on the overlap. For admitted local behaviors to form a sheaf, restrictions must remain admissible and compatible local members must have a unique admissible global glue. That property must be proved; arbitrary local and global constraints need not have it.

On a chosen site of time regions, sheaves form a topos whose internal logic is generally intuitionistic. This can provide a common semantic language for continuous, discrete, and hybrid behavior after their signal types, time structure, and solution concepts have been defined. Temporal modalities need additional temporal structure. Neither the topos nor its internal language proves a safety assertion merely by expressing it.

This logical geometry has named ancestors in the fibred order of difficulty. A tripos, in the sense of Hyland, Johnstone, and Pitts, is a fibred preorder with enough structure to build models of intuitionistic logic, which is a fibred order put to constructive work. And the subtopos classification theorem of Lawvere and Tierney shows that, inside a topos, the admissible closure operators on its logic correspond exactly to its subtoposes, the strongest classical instance of boundaries being classified by closure. The analogy is directional, not established: the closure operators of section 6 act on possibility sets, not on a subobject classifier, and no theorem here classifies difficulty classes by topologies of a fibred space. The resemblance locates the tradition; it does not borrow its proofs.

For a state predicate \(C\), define

\[ \operatorname{Safe}(C) =\{w:\forall t,\ C(w(t))\}. \]

Then the temporal safety claim is simply

\[ \mathcal B\models\Box C \quad\Longleftrightarrow\quad \mathcal B\subseteq\operatorname{Safe}(C). \]

For discrete deterministic dynamics, if \(\mathcal B_C\) contains every run starting in \(C\), then

\[ \mathcal B_C\models\Box C \quad\Longleftrightarrow\quad F(C)\subseteq C. \]

Thus an all-time safety statement reduces to a one-step invariant for this declared behavior. A plant-controller interconnection is safe only when its closed behavior satisfies the inclusion. Nonblocking or viability remains a separate obligation: the empty behavior satisfies every universal safety claim vacuously.

The same warning applies to compressed paths. Endpoint backing preserves reachability. Pathwise safety requires every hidden intermediate state to be safe, and barrier preservation requires its own score bound. A compressed edge supports only the properties certified by its backing trajectory. The return path is the mathematical content of claiming that an abstract solution solves the original task.

Chapter 5Complexity and the fibred order

A bound needs a family and a machine

An asymptotic resource bound concerns a family \(\{\mathcal I_n\}\), an encoding and size parameter \(n\), a machine or access model, a success or loss criterion, and a resource measure. Separately defined instance-level notions, including Kolmogorov and instance complexity, also exist. Time, workspace, queries, samples, communication, random bits, precision, and physical energy are not interchangeable until a conversion model is supplied.

The missing specifications matter. A one-pass stream and a rereadable array offer different information access. A random-access word machine and a Turing machine charge different primitive operations. Exact production and verification ask different questions. Worst-case, average-case, and smoothed analysis use different input quantifiers or distributions. A large search space by itself is not a lower bound under any of them.

Rather than force these resources into one number, fix a model and let each admissible program \(p\) have a resource vector \(\operatorname{Res}(p)\) and a loss vector \(\operatorname{Loss}(p)\), with the desired instance quantifiers already built into those functions. Take each coordinate in the extended nonnegative reals, order vectors componentwise, and treat smaller resource and loss values as better. Define

\[ \mathsf{Ach} =\{(r,\ell):\exists p, \operatorname{Res}(p)\preceq r, \ \operatorname{Loss}(p)\preceq\ell\}. \]

This attainable region is upward closed: a program meeting one pair of bounds also meets every looser pair. Its nondominated attainable points, when they exist, are Pareto-minimal. Limiting tradeoffs need not be attained; they lie on the lower boundary of the closure rather than necessarily in \(\mathsf{Ach}\). More time may buy lower error. More measurements may reduce time. More memory may replace recomputation. Some tradeoffs are impossible because the information or action boundary excludes them before computation begins.

For one resource called time and one distortion target \(D\), define the extended-valued slice \(\tau(D)\in[0,+\infty]\) by

\[ \tau(D) =\inf\{t:\exists p, \operatorname{Time}(p)\le t, \ \operatorname{Loss}(p)\le D\}. \]

If the set is empty, \(\tau(D)=+\infty\). The information lower bound from Chapter 1 is a lower bound on such a slice when observations are the limiting resource. The robust recurrence from Chapter 2 certifies an ultimate tube but, without a matching adversarial lower bound, does not make smaller errors unattainable. Reachability can make the goal loss unattainable regardless of computation. These results constrain different slices of an attainable region when they are assembled in one context. They are not competing definitions of a hidden scalar.

The fibred order of difficulty

A comparison context \(c\) fixes the common task, instance and environment quantifiers, uncertainty class, admissible programs, information and action interfaces, and resource and loss coordinates. Let \(P_c\) be its ordered performance space. The ambient fibre is the powerset

\[ \mathcal R_c=\mathcal P(P_c), \]

ordered by inclusion. Let \(\operatorname{Enc}(c)\) be the declared encounters to be compared. Attainability is a map

\[ \mathsf{Ach}_c:\operatorname{Enc}(c)\longrightarrow\mathcal R_c \]

whose values are upward-closed regions. Within this one context, define

\[ E_1\mathrel{\unrhd_c}E_2 \quad\Longleftrightarrow\quad \mathsf{Ach}_c(E_1)\subseteq\mathsf{Ach}_c(E_2), \]

and read \(E_1\unrhd_c E_2\) as "\(E_1\) is at least as hard as \(E_2\)." The relation is reflexive and transitive, but it need not be antisymmetric on encounters. Two different plants, observation channels, or presentations can have exactly the same attainable region. Quotient by

\[ E_1\sim_c E_2 \quad\Longleftrightarrow\quad \mathsf{Ach}_c(E_1)=\mathsf{Ach}_c(E_2). \]

The quotient is order-isomorphic to the realized image:

\[ \operatorname{Enc}(c)/{\sim_c} \ \cong\ \operatorname{im}(\mathsf{Ach}_c) \ \subseteq\ \mathcal R_c. \]

It is generally only a subposet of the ambient fibre. Equality with \(\mathcal R_c\) would claim that every subset of \(P_c\) is the attainable region of some encounter, which has not been assumed and is usually false. The quotient also forgets every distinction that the chosen performance coordinates fail to record; it is not identity of the underlying systems.

The realized order need not be total. Two encounters are incomparable when neither attainable region includes the other. Crossing Pareto frontiers are a common geometric witness: one encounter may be better at coarse accuracy and worse near exactness. A scalarization is extra structure and can reverse the ranking.

To relate ambient fibres, choose a category \(\mathcal C\) of contexts. An arrow \(f:c\to d\) includes a performance-point map \(u_f:P_c\to P_d\), compatible with identities and composition. Preimage gives

\[ f^*:\mathcal R_d\longrightarrow\mathcal R_c, \qquad f^*(A)=u_f^{-1}(A). \]

It is monotone and strictly contravariant:

\[ (\operatorname{id}_c)^*=\operatorname{id}_{\mathcal R_c}, \qquad (g\circ f)^*=f^*\circ g^*. \]

Thus the ambient data form a strict contravariant indexed poset

\[ \mathcal R:\mathcal C^{\mathrm{op}}\longrightarrow\mathbf{Pos}. \]

These are the data underlying a split fibred order. The ambient data construct the Grothendieck total category over the contexts, and the chosen splitting supplies the cartesian lifts that satisfy its universal property.

Preimage always preserves inclusion. It reflects inclusion whenever \(u_f\) is surjective:

\[ f^*(A)\subseteq f^*(B) \Longrightarrow A\subseteq B. \]

A bijection of performance coordinates is sufficient for reflection and gives an order isomorphism between ambient fibres, but bijectivity is stronger than reflection needs.

Even without closure of realized regions, \(f\) permits a heterogeneous comparison of two given encounters:

\[ E_c\mathrel{\unrhd_f}E_d \quad\Longleftrightarrow\quad \mathsf{Ach}_c(E_c) \subseteq u_f^{-1}\bigl(\mathsf{Ach}_d(E_d)\bigr). \]

This comparison does not turn the target encounter into an encounter of the source context.

Ambient reindexing does not by itself choose a source encounter. The preimage of a realized region in \(d\) also need not lie in \(\operatorname{im}(\mathsf{Ach}_c)\). To restrict \(f^*\) to the realized subposets, the minimal extra condition is preimage closure:

\[ A\in\operatorname{im}(\mathsf{Ach}_d) \quad\Longrightarrow\quad u_f^{-1}(A)\in\operatorname{im}(\mathsf{Ach}_c). \]

One sufficient way to prove this closure and choose source representatives is an encounter transport \(T_f:\operatorname{Enc}(d)\to\operatorname{Enc}(c)\) satisfying

\[ \mathsf{Ach}_c(T_fE) =u_f^{-1}\bigl(\mathsf{Ach}_d(E)\bigr). \]

The Lean companion packages this stronger witness. At the region level, identity and composition then follow from preimage; equality of the chosen raw encounter witnesses is unnecessary after equal regions have been identified. Without preimage closure, whether proved directly or through encounter transport, only the ambient powersets have been fibred.

This contravariant preimage must be separated from a lossy direct image. For a many-to-one map \(q:P_c\to P_d\), the covariant operation

\[ q_!:\mathcal R_c\longrightarrow\mathcal R_d, \qquad q_!(A)=\{q(x):x\in A\} \]

is monotone but can send distinct subsets to the same image and therefore fail to reflect inclusion. Noninjectivity causes that collapse. It does not, by itself, make inverse image fail reflection; surjectivity is the relevant condition there.

There is no canonical category of all contexts in this book. The objects, performance maps, and reindexing laws are part of each claim. A supplied map allows a heterogeneous comparison between given source and target encounters even when its preimage is not realized by another source encounter. A split fibred order on the realized classes requires preimage closure. Chosen transport of particular encounters is stronger data. Nor does fibred assert a topology, a manifold, a locally total order, or a global ranking.

One decategorification deserves a verdict rather than a temptation. Group completion sends a commutative monoid of difficulty classes to its Grothendieck group, and the result forgets everything the order carried. Attainable regions compose by union, union is idempotent, and the Grothendieck group of any commutative idempotent monoid is trivial, so the K-group of the region monoid over every performance space collapses to one element. The canonical map identifies two classes exactly when some common factor multiplies both into agreement, and the factors that do the interesting identifying are precisely the non-cancellable ones. Completion is injective on cancellative cost scales such as exact resource counts, and lossy where this chapter's subject matter lives: the saturating budget scale with an absorbing top has trivial completion too. A group-valued invariant obtained this way cannot distinguish any two difficulty classes at all, which is why the book keeps the order and does not pass to its K-theory.

A second decategorification temptation is the twist. In twisted K-theory, local invariants that fail to glue globally are governed by a cocycle, and the twist class measures the failure of any consistent global identification. The fibred order is in the gluing situation, and path-dependent performance translations, conversions between contexts that fail to compose on the nose, would be exactly such a cocycle. Both routes to a twist are closed here, and both closures are checked. The fibres are posets, and poset-valued indexed structures are strict on the nose, so there is no comparison data for a twist to live in. The coefficient K-groups are trivial by the collapse above, so a twist would in any case have nothing to act on. The moment the fibres carry genuine automorphisms the obstruction becomes real: a two-element-group example carries comparison data given by a cocycle that no re-choice of coefficients can flatten. A twisted theory of difficulty would need exactly that, fibres that remember more than the order, and coefficients drawn from the cancellative part where completion is faithful.

Finite envelopes and missing algorithms

Let \(E\) be a nonempty finite set of admissible programs and let \(V(p)\) be their value. A maximizer exists because the envelope is finite. If \(E\subseteq F\), the optimum over \(F\) cannot be worse. A strict gap can occur when an excluded program is better than every member of \(E\).

These elementary facts are useful because they expose a quantifier that is often hidden. An optimum relative to a search envelope is not a global optimum. Expanding the envelope may improve value, but searching the larger envelope may demand more resources. In an infinite envelope, even the existence of a maximizer can fail; the infimum or supremum need not be attained.

The same distinction applies to representation. A theorem that some compact sufficient statistic exists does not provide an algorithm to compute it. A coordinate equivalence can preserve behavior while being expensive to discover. Classical existence, computable construction, and efficient construction occupy different points on the attainable frontier.

State counts are information-retention bounds

Finite-state lower bounds become meaningful when the interface is exact. Say a target machine is output-separated when, for every distinct pair \(s\ne t\), there exists a finite input word \(w\) after which their outputs differ. Any machine tracking it exactly needs an injective encoding of those states. Thus

\[ |S_{\mathrm{target}}|\le |S_{\mathrm{tracker}}|. \]

This is a capacity condition, not a theory of understanding. Equal state counts do not guarantee a tracking map, and a smaller quotient may preserve everything needed for one task.

The positional multiplication example in the formal companion is even more specific. For \(b\ge2\) and \(n>0\), a one-pass register machine reads two \(n\)-digit base-\(b\) operands, retains \(k\) registers with \(r\) values each, and emits the product only from its final register state. Fixing the second operand to one turns the task into delayed reproduction of the first. Distinct first operands must therefore end in distinct configurations:

\[ b^n\le r^k. \]

If all configurations fit into \(m\) bits, then \(n\le m\). The lower bound is about retaining an operand under a one-pass, final-output interface. It is not a lower bound on multiplication in standard complexity classes. Rereadable input, auxiliary storage, or incremental output changes the model and can invalidate the argument.

The conversion from states to bits is essential. A machine with \(2^s\) states has \(s\) bits of state capacity, not \(2^s\) bits. Exponential state counts and linear bit bounds are the same statement in different units.

Where cost is paid

Representations can move work across time. An index, abstraction hierarchy, compiled circuit, or proof library may be expensive to construct and cheap to query. A fair resource vector separates preprocessing from online cost and states whether the artifact is amortized across instances. Treating a problem-specific artifact as free advice changes the computational model.

This does not make preprocessing illegitimate. It makes its quantifier visible. The right comparison may grant the same offline artifact to both agents, charge its construction once, or study nonuniform families that receive a different artifact at each size. Each convention defines a different attainable region.

Complexity theory earns objectivity not by removing models but by declaring them and proving invariance or simulation relations across a comparison class. The model dependence is controlled, not denied.

Chapter 6What remains objective

Relational realism

The claim that difficulty is relational can be made trivial by allowing the relation to change whenever a conclusion is inconvenient. It becomes substantive only when the comparison class is fixed before the comparison.

Within a fixed source prior, observation law, and admissible experiment class, mutual information and observational equivalence are objective properties of the model. Within a fixed action system, reachability and barrier depth are objective. Within a fixed machine and encoding, a resource lower bound is objective. Their statements contain relations, but so do velocity, controllability, and statistical sufficiency. Relational does not mean arbitrary.

Behavioral equality gives an extensional form of objectivity. Once \(T\), \(W\), and the signal boundary are fixed, two presentations with the same \(\mathcal B\) agree on every property stated solely of those trajectories. Exact coordinate equivalence, efficient machine simulations, and objective-preserving graph relabelings are other controlled invariances.

None supplies a view from nowhere. Hiding a signal, changing the admitted behavior, using a many-to-one abstraction, or adding a sensor, actuator, or predicate changes the claim unless a transfer theorem says otherwise. If the attainable frontier changes, that alteration is real, but it concerns a new relation. Comparing it with the old one requires a declared context map; without one, the proposed ordering is not yet a well-formed claim.

Four projections, not four substances

Ordinary uses of hard can still be sorted by the boundary they expose:

An epistemic obstruction leaves task-relevant alternatives indistinguishable or supplies information too slowly for the desired accuracy.
A practical obstruction places the target outside the action closure or forces every route through an inadmissible region.
A computational obstruction leaves success possible and representable but outside a resource budget.
An expressive obstruction means that the present vocabulary does not yet specify the distinction, invariant, or goal at issue.

These are projections of an encounter, not an exhaustive ontology. A changed model can create several at once. A missing state variable can appear as prediction error, poor control, and inefficient search. Conversely, one intervention can trade one obstruction for another: a richer representation can reduce online computation while increasing acquisition and storage cost.

Expressive limitation is the least amenable to a fixed formal test. For a declared finite vocabulary, definability can be studied through the partition it induces. But inventing a useful new predicate is not captured by adding the target predicate by fiat. The latter proves only that a language becomes more expressive when it is explicitly extended.

One shape behind three boundaries

The information, action, and behavior boundaries share an algebraic shape, and it is checked rather than suggestive. Each induces a closure operator on a poset of possibilities: reachable-set formation for the action boundary, observational saturation for the information boundary, and hiding followed by pullback for the behavior boundary. Extensivity, monotonicity, and idempotence hold in all three cases, in the standard sense of the order-theoretic literature rather than a private one.

Idempotence is the content of several results that earlier chapters proved separately. A transformation that is already pointwise reachable adds nothing when adjoined as a primitive. A statistic computed from an existing report separates no additional states. Both say the closure of a closure is the closure. In the other direction, a genuinely new primitive can strictly enlarge the closure, and a finer experiment never enlarges a saturation, so extension and refinement act on the closure itself rather than on effort inside it.

The unification has proved limits, and they carry information. Hiding preserves interconnection only up to a strict inclusion, so the behavioral closure is not a lattice homomorphism, and reasoning that silently commutes the two operations is unsound. And a closure operator given fibrewise need not commute with reindexing between contexts: the transport of a closure can differ from the closure of the transport, so a verdict computed in one context need not be the verdict of the transported problem. That failure is the closure-operator face of the earlier finding that realized regions need preimage closure before they reindex. What transports is the shape of the operator, not its verdicts.

This shape has classical ancestors, and the resemblance is precedent rather than authority. Lawvere and Tierney classified the subtoposes of a topos by exactly the closure operators on its subobject structure that respect the ambient logic, so "which boundaries can be drawn" became an order-theoretic question there too. Tripos theory builds models of logic from indexed preorders with structure, a fibred order put to constructive work. The companion checks none of that machinery; the citations locate the pattern, not the proofs.

No view from nowhere

There is no model-independent scalar difficulty of a bare problem waiting to be measured before a task and encounter are specified. A scalar becomes legitimate after a comparison class and scalarization are fixed. What can be measured are information rates, error tubes, reachable sets, barrier depths, proof lengths, circuit sizes, query counts, approximation losses, and the tradeoffs among them.

Nor does the relational view imply that every obstacle yields to a clever representation. Data processing forbids a representation from inventing evidence. Robustness margins bound tolerated mismatch. Reachability forbids inference from becoming action. Complexity lower bounds survive broad classes of algorithms. A more illuminating map can change search without changing the terrain it faithfully represents.

The book's thesis can now be stated without metaphor. For each declared context \(c\), actual difficulty occupies a realized subposet of an ambient powerset:

\[ \mathcal R_c=\mathcal P(P_c), \qquad \operatorname{Enc}(c)/{\sim_c} \cong\operatorname{im}(\mathsf{Ach}_c) \subseteq\mathcal R_c, \qquad [E_1]\unrhd_c[E_2] \Longleftrightarrow \mathsf{Ach}_c(E_1)\subseteq\mathsf{Ach}_c(E_2). \]

Performance-point maps give the ambient contravariant order

\[ f^*(A)=u_f^{-1}(A), \qquad \mathcal R:\mathcal C^{\mathrm{op}}\to\mathbf{Pos}. \]

The second display permits a heterogeneous comparison of two given encounters, but it does not say that realized difficulty classes reindex. That stronger claim requires closure of realized regions under preimage. Compatible encounter transport is one sufficient witness. These displays are a schema, not a universal construction or numerical identity. Before the context, performance map, and any claimed problem transport are fixed, harder is an invitation to ask which comparison has been left implicit.

Chapter 7What is machine checked

The Lean companion proves consequences of explicit finite, algebraic, and order-theoretic definitions. It does not contain a theorem called difficulty. The cards below state the hypotheses, conclusion, and boundary of each checked fragment. This avoids a misleading transfer from kernel verification to model adequacy. A theorem can be valid while its hypotheses fail to describe a physical observer, an admissible experiment, or the intended cost.

Deterministic information preorder, budgets, and scalar reconstruction

Hypotheses. A deterministic coarse report is obtained from a fine report by a post-processing map, and acceptable actions are declared state by state. Separately, a real-valued accumulated quantity starts below \(I_0\), grows by at most \(C\) per natural-number round, and has reached a required level \(R_*\) by round \(n\). A positive scalar prior variance \(P_0\) and positive measurement variance \(R\) are inserted into the algebraic posterior formula \(P_n=(P_0^{-1}+nR^{-1})^{-1}\).

Conclusion. Deterministic refinement is reflexive and transitive. Equality of fine reports forces equality of coarse reports, and every action robust for the coarse compatibility class remains robust for the fine class. Mutual factorization preserves the induced classes and robust action sets. An explicit two-state quotient makes the robust-action inclusion strict. More generally, any deterministic decision rule based on a statistic that merges two states with disjoint acceptable sets fails at one of them. The accumulated quantity is at most \(I_0+nC\), and for \(C>0\) the natural ceiling of \((R_*-I_0)/C\) is at most \(n\). If the scalar posterior variance is at most a positive \(D\), then \(R(D^{-1}-P_0^{-1})\le n\), with a positive lower bound when \(D<P_0\). (machine-checked)

Lean declarations and proofs (FeedbackBounds.lean, InformationBudget.lean, InformationOrder.lean, SystemsTheory.lean): HardProblems.InformationOrder.Indist, HardProblems.InformationOrder.indist_equivalence, HardProblems.InformationOrder.ExperimentRefines, HardProblems.InformationOrder.experimentRefines_refl, HardProblems.InformationOrder.experimentRefines_trans, HardProblems.InformationOrder.ExperimentRefines.indist, HardProblems.InformationOrder.RobustActions, HardProblems.InformationOrder.ExperimentRefines.robustActions_mono, HardProblems.InformationOrder.indist_iff_of_mutual_refinement, HardProblems.InformationOrder.robustActions_eq_of_mutual_refinement, HardProblems.InformationOrder.quotient_strict_decision_loss, HardProblems.statistic_based_rule_fails', HardProblems.InformationBudget.accumulated_le_initial_add_rounds_mul, HardProblems.InformationBudget.required_excess_le_rounds_mul, HardProblems.InformationBudget.required_excess_div_capacity_le_rounds, HardProblems.InformationBudget.required_rounds_ceiling_le, HardProblems.ScalarGaussian.posteriorVariance, HardProblems.ScalarGaussian.posteriorVariance_pos, HardProblems.ScalarGaussian.target_accuracy_requires_observations, HardProblems.ScalarGaussian.target_accuracy_nontrivial_boundrun run run run

-- LeanTest/HardProblems/InformationOrder.lean
/-- States are indistinguishable under an observation map when they produce
the same report. -/
def Indist {S : Type u} {O : Type v} (observe : S → O) (x y : S) : Prop :=
  observe x = observe y

-- LeanTest/HardProblems/InformationOrder.lean
/-- Equality of reports induces an equivalence relation on states. -/
theorem indist_equivalence {S : Type u} {O : Type v} (observe : S → O) :
    Equivalence (Indist observe) where
  refl _ := rfl
  symm h := h.symm
  trans hxy hyz := hxy.trans hyz

-- LeanTest/HardProblems/InformationOrder.lean
/-- `fine` refines `coarse` when the coarse report is obtained by deterministic
post-processing of the fine report. This orients the existing
`HardProblems.FactorsThrough` relation as an information preorder; it does not
introduce a second notion of factorization. -/
def ExperimentRefines {S : Type u} {F : Type v} {C : Type w}
    (fine : S → F) (coarse : S → C) : Prop :=
  FactorsThrough coarse fine

-- LeanTest/HardProblems/InformationOrder.lean
/-- Every experiment refines itself. -/
theorem experimentRefines_refl {S : Type u} {O : Type v}
    (observe : S → O) : ExperimentRefines observe observe := by
  exact ⟨id, by funext x; rfl⟩

-- LeanTest/HardProblems/InformationOrder.lean
/-- Deterministic experiment refinement is transitive. -/
theorem experimentRefines_trans {S : Type u} {A : Type v} {B : Type w}
    {C : Type z} {first : S → A} {second : S → B} {third : S → C}
    (h₁ : ExperimentRefines first second)
    (h₂ : ExperimentRefines second third) :
    ExperimentRefines first third := by
  rcases h₁ with ⟨post₁, rfl⟩
  rcases h₂ with ⟨post₂, rfl⟩
  exact ⟨post₂ ∘ post₁, by funext x; rfl⟩

-- LeanTest/HardProblems/InformationOrder.lean
/-- Refinement reverses inclusion of indistinguishability classes: equality of
fine reports forces equality of coarse reports. -/
theorem ExperimentRefines.indist {S : Type u} {F : Type v} {C : Type w}
    {fine : S → F} {coarse : S → C}
    (h : ExperimentRefines fine coarse) {x y : S}
    (hxy : Indist fine x y) : Indist coarse x y := by
  exact (show FactorsThrough coarse fine from h).eq_of_eq hxy

-- LeanTest/HardProblems/InformationOrder.lean
/-- Actions acceptable at every state compatible with the current report.
The acceptable-action predicate is part of the task, rather than part of the
observation alone. -/
def RobustActions {S : Type u} {O : Type v} {A : Type w}
    (observe : S → O) (Acceptable : S → A → Prop) (x : S) : Set A :=
  {a | ∀ y, Indist observe x y → Acceptable y a}

-- LeanTest/HardProblems/InformationOrder.lean
/-- A finer experiment weakly enlarges the set of robust acceptable actions.
The result is task-relevant but deterministic: it compares compatibility
classes, not probabilities or average information. -/
theorem ExperimentRefines.robustActions_mono
    {S : Type u} {F : Type v} {C : Type w} {A : Type z}
    {fine : S → F} {coarse : S → C}
    (h : ExperimentRefines fine coarse) (Acceptable : S → A → Prop) (x : S) :
    RobustActions coarse Acceptable x ⊆ RobustActions fine Acceptable x := by
  intro a ha y hxy
  exact ha y (h.indist hxy)

-- LeanTest/HardProblems/InformationOrder.lean
/-- Mutual deterministic factorization gives exactly the same induced
indistinguishability relation. The report types and report values themselves
need not be equal. -/
theorem indist_iff_of_mutual_refinement
    {S : Type u} {O₁ : Type v} {O₂ : Type w}
    {first : S → O₁} {second : S → O₂}
    (h₁₂ : ExperimentRefines first second)
    (h₂₁ : ExperimentRefines second first) (x y : S) :
    Indist first x y ↔ Indist second x y :=
  ⟨h₁₂.indist, h₂₁.indist⟩

-- LeanTest/HardProblems/InformationOrder.lean
/-- Mutual deterministic factorization preserves every robust action set for
every task predicate. -/
theorem robustActions_eq_of_mutual_refinement
    {S : Type u} {O₁ : Type v} {O₂ : Type w} {A : Type z}
    {first : S → O₁} {second : S → O₂}
    (h₁₂ : ExperimentRefines first second)
    (h₂₁ : ExperimentRefines second first)
    (Acceptable : S → A → Prop) (x : S) :
    RobustActions first Acceptable x = RobustActions second Acceptable x := by
  apply Set.Subset.antisymm
  · exact h₂₁.robustActions_mono Acceptable x
  · exact h₁₂.robustActions_mono Acceptable x

-- LeanTest/HardProblems/InformationOrder.lean
/-- A strict finite decision loss. The identity experiment separates the two
Bool states, while the quotient to `Unit` merges them. An action is acceptable
exactly when it names the true state. At state `false`, the fine report permits
the robust action `false`; the coarse report permits no robust action. -/
theorem quotient_strict_decision_loss :
    let fine : Bool → Bool := id
    let coarse : Bool → Unit := fun _ ↦ ()
    let Acceptable : Bool → Bool → Prop := fun state action ↦ state = action
    ExperimentRefines fine coarse ∧
      ¬ Indist fine false true ∧ Indist coarse false true ∧
      RobustActions coarse Acceptable false = ∅ ∧
      RobustActions fine Acceptable false = {false} ∧
      RobustActions coarse Acceptable false ⊂
        RobustActions fine Acceptable false := by
  dsimp
  refine ⟨⟨fun _ ↦ (), rfl⟩, by simp [Indist], by simp [Indist], ?_⟩
  have hCoarse : RobustActions (fun _ : Bool ↦ ())
      (fun state action : Bool ↦ state = action) false = ∅ := by
    ext action
    constructor
    · intro ha
      have hFalse := ha false (by rfl)
      have hTrue := ha true (by rfl)
      simp only [Set.mem_empty_iff_false]
      cases action <;> simp_all
    · simp
  have hFine : RobustActions id
      (fun state action : Bool ↦ state = action) false = {false} := by
    ext action
    simp [RobustActions, Indist]
  refine ⟨hCoarse, hFine, ?_⟩
  rw [hCoarse, hFine]
  exact Set.empty_ssubset.mpr (Set.singleton_nonempty false)

-- LeanTest/HardProblems/SystemsTheory.lean
/-- The statistic-factorization obstruction with an arbitrary statistic
codomain; nothing in the argument uses the real numbers. -/
theorem statistic_based_rule_fails' {Y : Type*} {m : S → Y} (Astar : S → Set A)
    {s s' : S} (hm : m s = m s') (hdisj : Disjoint (Astar s) (Astar s'))
    (α : Y → A) :
    α (m s) ∉ Astar s ∨ α (m s') ∉ Astar s' := by
  by_contra hc
  push Not at hc
  obtain ⟨h1, h2⟩ := hc
  rw [hm] at h1
  exact Set.disjoint_left.mp hdisj h1 h2

-- LeanTest/HardProblems/InformationBudget.lean
/-- An accumulated real-valued quantity with initial upper bound `I₀` and
one-round increment bounded above by `C` is at most `I₀ + n * C` after `n`
rounds.

No nonnegativity hypothesis is needed for this arithmetic statement.  An
information-theoretic application must separately establish that its chosen
quantities and bounds have the intended meaning. -/
theorem accumulated_le_initial_add_rounds_mul
    (accumulated : ℕ → ℝ) (I₀ C : ℝ)
    (hinitial : accumulated 0 ≤ I₀)
    (hstep : ∀ n, accumulated (n + 1) ≤ accumulated n + C) :
    ∀ n, accumulated n ≤ I₀ + (n : ℝ) * C := by
  intro n
  induction n with
  | zero => simpa using hinitial
  | succ n ih =>
      calc
        accumulated (n + 1) ≤ accumulated n + C := hstep n
        _ ≤ (I₀ + (n : ℝ) * C) + C := add_le_add_left ih C
        _ = I₀ + ((n + 1 : ℕ) : ℝ) * C := by
          push_cast
          ring

-- LeanTest/HardProblems/InformationBudget.lean
/-- If reaching the target requires at least `R` units of the accumulated
quantity, and the target has been reached at round `n`, then the required
amount above the initial budget is no larger than `n * C`.

This conclusion is conditional on `hrequired`: the lemma does not prove that a
distortion level really requires `R`, nor that the accumulated scalar is
mutual information. -/
theorem required_excess_le_rounds_mul
    (accumulated : ℕ → ℝ) (I₀ C R : ℝ) (n : ℕ)
    (hinitial : accumulated 0 ≤ I₀)
    (hstep : ∀ k, accumulated (k + 1) ≤ accumulated k + C)
    (hrequired : R ≤ accumulated n) :
    R - I₀ ≤ (n : ℝ) * C := by
  have hbudget :=
    accumulated_le_initial_add_rounds_mul accumulated I₀ C hinitial hstep n
  linarith

-- LeanTest/HardProblems/InformationBudget.lean
/-- With positive per-round capacity, the real-valued required excess divided
by that capacity is a lower bound on the number of rounds.

This is only division of the preceding scalar inequality.  In particular, it
does not identify `R` with a rate-distortion function or `C` with Shannon
capacity. -/
theorem required_excess_div_capacity_le_rounds
    (accumulated : ℕ → ℝ) (I₀ C R : ℝ) (n : ℕ)
    (hinitial : accumulated 0 ≤ I₀)
    (hstep : ∀ k, accumulated (k + 1) ≤ accumulated k + C)
    (hrequired : R ≤ accumulated n) (hC : 0 < C) :
    (R - I₀) / C ≤ (n : ℝ) := by
  apply (div_le_iff₀ hC).2
  exact required_excess_le_rounds_mul accumulated I₀ C R n
    hinitial hstep hrequired

-- LeanTest/HardProblems/InformationBudget.lean
/-- Since rounds are natural numbers, the natural ceiling of the real-valued
ratio is also a lower bound on the round count.

If `R ≤ I₀`, the ratio may be nonpositive and the ceiling is zero; the theorem
then correctly gives only the vacuous lower bound `0 ≤ n`. -/
theorem required_rounds_ceiling_le
    (accumulated : ℕ → ℝ) (I₀ C R : ℝ) (n : ℕ)
    (hinitial : accumulated 0 ≤ I₀)
    (hstep : ∀ k, accumulated (k + 1) ≤ accumulated k + C)
    (hrequired : R ≤ accumulated n) (hC : 0 < C) :
    Nat.ceil ((R - I₀) / C) ≤ n := by
  apply Nat.ceil_le.mpr
  exact required_excess_div_capacity_le_rounds accumulated I₀ C R n
    hinitial hstep hrequired hC

-- LeanTest/HardProblems/FeedbackBounds.lean
/-- Algebraic posterior variance for a scalar Gaussian prior of variance `P₀`
after `n` independent measurements with noise variance `R`.

This definition packages the standard conjugate-Gaussian calculation. It does
not itself prove that a physical measurement process is Gaussian, independent,
or correctly modeled. -/
noncomputable def posteriorVariance (P₀ R : ℝ) (n : ℕ) : ℝ :=
  1 / (1 / P₀ + (n : ℝ) / R)

-- LeanTest/HardProblems/FeedbackBounds.lean
/-- Positive prior and measurement variances give positive posterior variance. -/
theorem posteriorVariance_pos {P₀ R : ℝ} (hP₀ : 0 < P₀) (hR : 0 < R)
    (n : ℕ) : 0 < posteriorVariance P₀ R n := by
  unfold posteriorVariance
  positivity

-- LeanTest/HardProblems/FeedbackBounds.lean
/-- Reaching target variance `D` under the scalar posterior formula requires
at least `R * (1 / D - 1 / P₀)` measurements. The right side is real-valued;
an integer ceiling would be needed for a sharp natural-number statement.

This is an algebraic consequence of the displayed variance formula. It is not
a general Kalman-filter theorem and says nothing about model mismatch, process
noise, correlated measurements, or unobservable state directions. -/
theorem target_accuracy_requires_observations {P₀ R D : ℝ} {n : ℕ}
    (hP₀ : 0 < P₀) (hR : 0 < R) (hD : 0 < D)
    (hacc : posteriorVariance P₀ R n ≤ D) :
    R * (1 / D - 1 / P₀) ≤ (n : ℝ) := by
  have hden : 0 < 1 / P₀ + (n : ℝ) / R := by positivity
  have hcross : 1 ≤ D * (1 / P₀ + (n : ℝ) / R) := by
    exact (div_le_iff₀ hden).mp hacc
  have hprecision : 1 / D ≤ 1 / P₀ + (n : ℝ) / R := by
    apply (div_le_iff₀ hD).2
    nlinarith
  have hremaining : 1 / D - 1 / P₀ ≤ (n : ℝ) / R := by
    linarith
  simpa [mul_comm] using (le_div_iff₀ hR).mp hremaining

-- LeanTest/HardProblems/FeedbackBounds.lean
/-- If the target variance is strictly smaller than the prior variance, the
observation-count lower bound above is strictly positive rather than vacuous. -/
theorem target_accuracy_nontrivial_bound {P₀ R D : ℝ} {n : ℕ}
    (hP₀ : 0 < P₀) (hR : 0 < R) (hD : 0 < D) (hDlt : D < P₀)
    (hacc : posteriorVariance P₀ R n ≤ D) :
    0 < R * (1 / D - 1 / P₀) ∧
      R * (1 / D - 1 / P₀) ≤ (n : ℝ) := by
  constructor
  · exact mul_pos hR (sub_pos.mpr (one_div_lt_one_div_of_lt hD hDlt))
  · exact target_accuracy_requires_observations hP₀ hR hD hacc

Boundary. The refinement results concern deterministic partitions, not entropy, mutual information, statistical sufficiency, or stochastic channels. The information-budget result is scalar arithmetic: it does not prove data processing or a rate-distortion premise. The posterior result packages scalar Gaussian algebra; it does not formalize a probability space, independence, Kalman optimality, process noise, or observability.

Robust recurrence, switching, and fault margins

Hypotheses. A real sequence obeys \(e_{n+1}\le(q_0+\mu)e_n+d\), with nonnegative \(q_0\), \(\mu\), and \(d\), and \(q_0+\mu<1\). In a second scalar recurrence, each nonnegative error is multiplied by a possibly changing factor between zero and a common \(q_{\max}<1\), with the same additive bound. Separately, a faulted residual is the sum \(r^f=r^h+f\) of a healthy residual with norm at most \(\rho\) and an additive fault signature. Alarms use a strict threshold \(\eta\), and candidate signatures are centers of closed norm balls with nonnegative radius \(\rho\).

Conclusion. The mismatch satisfies \(\mu<1-q_0\), and every finite-time error obeys the geometric transient plus disturbance-tube upper bound. A separate theorem proves forward invariance of the radius \(d/(1-q)\) when \(d\ge0\) and the initial error is already inside it. Under arbitrary changes of the scalar factor, the common upper factor gives the corresponding finite geometric sum and, when it is strictly below one, the same closed-form tube transient. A threshold at least \(\rho\) raises no alarm on any admitted healthy residual; a fault norm greater than \(\eta+\rho\) guarantees an alarm, giving the \(2\rho\) condition at \(\eta=\rho\). Each admitted additive faulted residual lies in the closed ball centered at its fault signature. Candidate balls whose centers are more than \(2\rho\) apart are disjoint. (machine-checked)

Lean declarations and proofs (FaultMargins.lean, FeedbackBounds.lean): HardProblems.RobustFeedback.error_le_geometric_sum, HardProblems.RobustFeedback.error_le_tube_transient, HardProblems.RobustFeedback.error_le_tube, HardProblems.RobustFeedback.mismatch_le_margin_and_error_bound, HardProblems.FaultMargins.Alarm, HardProblems.FaultMargins.healthy_residual_not_alarm, HardProblems.FaultMargins.alarm_of_fault_norm_gt_threshold_add_radius, HardProblems.FaultMargins.alarm_of_fault_norm_gt_two_mul_radius, HardProblems.FaultMargins.faulted_residual_mem_closedBall, HardProblems.FaultMargins.closedBall_disjoint_of_norm_sub_gt_two_mul_radius, HardProblems.UniformSwitching.error_le_uniform_geometric_sum, HardProblems.UniformSwitching.error_le_uniform_tube_transientrun run

-- LeanTest/HardProblems/FeedbackBounds.lean
/-- Iterating a scalar robust contraction gives a geometric finite-time bound.
The error need not be generated by any particular observer, but nonnegativity
of `q` is needed to propagate the upper inequality. -/
theorem error_le_geometric_sum (e : ℕ → ℝ) (q d : ℝ)
    (hq : 0 ≤ q) (hstep : ∀ n, e (n + 1) ≤ q * e n + d) (n : ℕ) :
    e n ≤ q ^ n * e 0 + d * ∑ k ∈ Finset.range n, q ^ k := by
  induction n with
  | zero => simp
  | succ n ih =>
      calc
        e (n + 1) ≤ q * e n + d := hstep n
        _ ≤ q * (q ^ n * e 0 + d * ∑ k ∈ Finset.range n, q ^ k) + d :=
          add_le_add (mul_le_mul_of_nonneg_left ih hq) le_rfl
        _ = q ^ (n + 1) * e 0 + d * ∑ k ∈ Finset.range (n + 1), q ^ k := by
          rw [geom_sum_succ]
          ring

-- LeanTest/HardProblems/FeedbackBounds.lean
/-- With a strict contraction, the geometric sum can be written using the
disturbance tube `d / (1 - q)`. This is a finite-time statement, not an
asymptotic optimality claim. -/
theorem error_le_tube_transient (e : ℕ → ℝ) (q d : ℝ)
    (hq0 : 0 ≤ q) (hq1 : q < 1)
    (hstep : ∀ n, e (n + 1) ≤ q * e n + d) (n : ℕ) :
    e n ≤ q ^ n * (e 0 - d / (1 - q)) + d / (1 - q) := by
  have hqne : q ≠ 1 := ne_of_lt hq1
  have hbound := error_le_geometric_sum e q d hq0 hstep n
  rw [geom_sum_eq hqne n] at hbound
  calc
    e n ≤ q ^ n * e 0 + d * ((q ^ n - 1) / (q - 1)) := hbound
    _ = q ^ n * (e 0 - d / (1 - q)) + d / (1 - q) := by
      field_simp [sub_ne_zero.mpr hqne, sub_ne_zero.mpr hqne.symm]
      ring

-- LeanTest/HardProblems/FeedbackBounds.lean
/-- The disturbance tube is forward invariant: if the initial error is below
`d / (1 - q)`, every later error remains below it. The assumption `0 ≤ d`
makes the displayed radius nonnegative; it is not needed merely for the upper
inequality but records its intended error-bound interpretation. -/
theorem error_le_tube (e : ℕ → ℝ) (q d : ℝ)
    (hq0 : 0 ≤ q) (hq1 : q < 1) (hd : 0 ≤ d)
    (hstep : ∀ n, e (n + 1) ≤ q * e n + d)
    (hinit : e 0 ≤ d / (1 - q)) (n : ℕ) :
    0 ≤ d / (1 - q) ∧ e n ≤ d / (1 - q) := by
  constructor
  · exact div_nonneg hd (sub_nonneg.mpr (le_of_lt hq1))
  · have hpow : 0 ≤ q ^ n := pow_nonneg hq0 n
    have htransient := error_le_tube_transient e q d hq0 hq1 hstep n
    have hdiff : e 0 - d / (1 - q) ≤ 0 := sub_nonpos.mpr hinit
    have hnonpos : q ^ n * (e 0 - d / (1 - q)) ≤ 0 :=
      mul_nonpos_of_nonneg_of_nonpos hpow hdiff
    linarith

-- LeanTest/HardProblems/FeedbackBounds.lean
/-- Writing the effective contraction factor as `q₀ + μ` makes the robustness
margin explicit. A certified mismatch `μ` must remain below `1 - q₀`; under
that hypothesis the same finite-time disturbance-tube bound applies.

The result does not say that `μ` is a universal metric on model difference.
An observer analysis must first justify that the actual mismatch contributes
at most `μ` to this scalar one-step estimate. -/
theorem mismatch_le_margin_and_error_bound (e : ℕ → ℝ) (q₀ μ d : ℝ)
    (hq₀ : 0 ≤ q₀) (hμ : 0 ≤ μ) (hmargin : q₀ + μ < 1)
    (hstep : ∀ n, e (n + 1) ≤ (q₀ + μ) * e n + d) (n : ℕ) :
    μ < 1 - q₀ ∧
      e n ≤ (q₀ + μ) ^ n * (e 0 - d / (1 - q₀ - μ)) +
        d / (1 - q₀ - μ) := by
  constructor
  · linarith
  · have hq : 0 ≤ q₀ + μ := add_nonneg hq₀ hμ
    simpa [sub_sub] using
      error_le_tube_transient e (q₀ + μ) d hq hmargin hstep n

-- LeanTest/HardProblems/FaultMargins.lean
/-- A strict deterministic threshold test on a residual. Equality with the
threshold does not raise an alarm. -/
def Alarm (η : ℝ) (residual : E) : Prop :=
  η < ‖residual‖

-- LeanTest/HardProblems/FaultMargins.lean
/-- A residual certified inside the healthy radius cannot cross a threshold
that is at least that radius. This is a pointwise deterministic statement, not
a probabilistic false-alarm guarantee. -/
theorem healthy_residual_not_alarm {healthy : E} {ρ η : ℝ}
    (hhealthy : ‖healthy‖ ≤ ρ) (hthreshold : ρ ≤ η) :
    ¬ Alarm η healthy := by
  exact not_lt_of_ge (hhealthy.trans hthreshold)

-- LeanTest/HardProblems/FaultMargins.lean
/-- Reverse-triangle geometry for an additive fault: if the fault norm exceeds
the threshold plus the healthy-radius allowance, every admitted healthy
residual forces an alarm. The condition is sufficient, not necessary. -/
theorem alarm_of_fault_norm_gt_threshold_add_radius
    {healthy fault : E} {ρ η : ℝ}
    (hhealthy : ‖healthy‖ ≤ ρ) (hfault : η + ρ < ‖fault‖) :
    Alarm η (healthy + fault) := by
  have hreverse : ‖fault‖ ≤ ‖healthy + fault‖ + ‖healthy‖ := by
    calc
      ‖fault‖ = ‖(healthy + fault) - healthy‖ := by
        congr 1
        abel
      _ ≤ ‖healthy + fault‖ + ‖healthy‖ := norm_sub_le _ _
  unfold Alarm
  linarith

-- LeanTest/HardProblems/FaultMargins.lean
/-- At the smallest threshold certified from the declared healthy-radius bound
alone, `η = ρ`, the familiar separation condition is
`2 * ρ < ‖fault‖`. It still asserts only guaranteed detection under that
deterministic radius. -/
theorem alarm_of_fault_norm_gt_two_mul_radius
    {healthy fault : E} {ρ : ℝ}
    (hhealthy : ‖healthy‖ ≤ ρ) (hfault : 2 * ρ < ‖fault‖) :
    Alarm ρ (healthy + fault) := by
  apply alarm_of_fault_norm_gt_threshold_add_radius hhealthy
  simpa [two_mul] using hfault

-- LeanTest/HardProblems/FaultMargins.lean
/-- An additive faulted residual lies in the closed residual ball centered at
its fault signature whenever the healthy component lies inside the declared
radius. -/
theorem faulted_residual_mem_closedBall {healthy fault : E} {ρ : ℝ}
    (hhealthy : ‖healthy‖ ≤ ρ) :
    healthy + fault ∈ Metric.closedBall fault ρ := by
  rw [Metric.mem_closedBall, dist_eq_norm]
  simpa [add_sub_cancel_right]

-- LeanTest/HardProblems/FaultMargins.lean
/-- Closed candidate residual balls of common radius are disjoint when their
fault centers are separated by more than twice that radius. This supplies a
deterministic isolation margin for these two declared candidates; it does not
show that the candidate list is exhaustive or statistically identifiable.
The explicit nonnegativity hypothesis rules out vacuous negative-radius
balls. -/
theorem closedBall_disjoint_of_norm_sub_gt_two_mul_radius
    {fault₁ fault₂ : E} {ρ : ℝ}
    (hρ : 0 ≤ ρ) (hseparated : 2 * ρ < ‖fault₁ - fault₂‖) :
    Disjoint (Metric.closedBall fault₁ ρ) (Metric.closedBall fault₂ ρ) := by
  rw [Set.disjoint_left]
  intro residual hmem₁ hmem₂
  have h₁ : dist fault₁ residual ≤ ρ := by
    simpa [dist_comm] using (Metric.mem_closedBall.mp hmem₁)
  have h₂ : dist residual fault₂ ≤ ρ :=
    Metric.mem_closedBall.mp hmem₂
  have htriangle : dist fault₁ fault₂ ≤ dist fault₁ residual + dist residual fault₂ :=
    dist_triangle _ _ _
  have h₁max : dist fault₁ residual ≤ max ρ 0 :=
    h₁.trans (le_max_left _ _)
  have h₂max : dist residual fault₂ ≤ max ρ 0 :=
    h₂.trans (le_max_left _ _)
  have hcentersMax : ‖fault₁ - fault₂‖ ≤ 2 * max ρ 0 := by
    rw [← dist_eq_norm]
    linarith
  have hcenters : ‖fault₁ - fault₂‖ ≤ 2 * ρ := by
    simpa [max_eq_left hρ] using hcentersMax
  linarith

-- LeanTest/HardProblems/FaultMargins.lean
/-- A scalar recurrence may switch its nonnegative contraction factor at every
step and still obey the constant geometric bound for a declared uniform upper
factor. Nonnegativity of the error is what permits replacing each active factor
by the uniform upper bound.

This extends the constant-factor recurrence in `RobustFeedback`; it does not
establish that a switched observer or plant satisfies the scalar hypotheses. -/
theorem error_le_uniform_geometric_sum
    (e q : ℕ → ℝ) (qMax d : ℝ)
    (hqMax : 0 ≤ qMax)
    (hq : ∀ n, 0 ≤ q n ∧ q n ≤ qMax)
    (he : ∀ n, 0 ≤ e n)
    (hstep : ∀ n, e (n + 1) ≤ q n * e n + d)
    (n : ℕ) :
    e n ≤ qMax ^ n * e 0 + d * ∑ k ∈ Finset.range n, qMax ^ k := by
  apply RobustFeedback.error_le_geometric_sum e qMax d hqMax
  intro k
  calc
    e (k + 1) ≤ q k * e k + d := hstep k
    _ ≤ qMax * e k + d :=
      add_le_add (mul_le_mul_of_nonneg_right (hq k).2 (he k)) le_rfl

-- LeanTest/HardProblems/FaultMargins.lean
/-- Under a strict uniform contraction bound, arbitrary switching obeys the
same closed-form disturbance-tube transient as the constant-factor recurrence.
The theorem gives an upper certificate under uniform scalar hypotheses; it
does not establish those hypotheses for a particular switched system. -/
theorem error_le_uniform_tube_transient
    (e q : ℕ → ℝ) (qMax d : ℝ)
    (hqMax0 : 0 ≤ qMax) (hqMax1 : qMax < 1)
    (hq : ∀ n, 0 ≤ q n ∧ q n ≤ qMax)
    (he : ∀ n, 0 ≤ e n)
    (hstep : ∀ n, e (n + 1) ≤ q n * e n + d)
    (n : ℕ) :
    e n ≤ qMax ^ n * (e 0 - d / (1 - qMax)) + d / (1 - qMax) := by
  apply RobustFeedback.error_le_tube_transient e qMax d hqMax0 hqMax1
  intro k
  calc
    e (k + 1) ≤ q k * e k + d := hstep k
    _ ≤ qMax * e k + d :=
      add_le_add (mul_le_mul_of_nonneg_right (hq k).2 (he k)) le_rfl

Boundary. These are scalar comparison theorems and deterministic norm geometry. They do not construct a nonlinear observer, establish its one-step inequality, or supply a common Lyapunov metric for a switched plant. They do not prove probabilistic false-alarm rates, necessary detection limits, completeness of a fault catalogue, or a diagnosis algorithm. Crossing a sufficient margin removes the certificate; it does not prove divergence. The tube is an upper guarantee, not a lower accuracy bound or an optimality claim.

Observational equivalence and robust action

Hypotheses. A partially observed stochastic system has transition and observation kernels. Policies map finite observation histories to action distributions. Two initial states are equivalent when every such policy and finite horizon induce the same law of observation histories. Each state has a set of acceptable actions. Separately, one trajectory estimate in a pseudometric state space converges to each of two state trajectories.

Conclusion. Observational equivalence is an equivalence relation. The robustly acceptable actions at a state are the intersection of acceptable sets over its equivalence class. Robust action is infeasible exactly when that total intersection is empty; a disjoint pair is a sufficient witness. If one estimate converges to both state trajectories, their mutual distance converges to zero. A constant-action experiment is a special case of an adaptive probe, and an explicit pair of Boolean models agrees under one passive action at every horizon but is separated by an admitted probe. (machine-checked)

Lean declarations and proofs (Observability.lean, SystemsTheory.lean): HardProblems.PassivelyDistinguishable, HardProblems.ProbeDistinguishable, HardProblems.passively_imp_probe, HardProblems.exists_probe_only_distinguishable, HardProblems.ObsEquiv, HardProblems.obsEquiv_equivalence, HardProblems.common_estimate_forces_pairwise_convergence, HardProblems.DecisionCritical, HardProblems.RobustAcceptable, HardProblems.robustSet_eq_iInter, HardProblems.RobustlyInfeasible, HardProblems.robustlyInfeasible_iff_iInter_eq_empty, HardProblems.DecisionCritical.no_robust_actionrun run

-- LeanTest/HardProblems/SystemsTheory.lean
/-- Two models are distinguishable from `s` under the constant action `a₀`
when their observation-history laws differ at some horizon. The type does not
assert that `a₀` is inert; that interpretation is supplied by an application. -/
def PassivelyDistinguishable (M₁ M₂ : POSystem S A O) (a₀ : A) (s : S) : Prop :=
  ∃ n, obsProcess M₁ (fun _ => PMF.pure a₀) n s [] ≠
        obsProcess M₂ (fun _ => PMF.pure a₀) n s []

-- LeanTest/HardProblems/SystemsTheory.lean
/-- Two models are probe distinguishable from `s` when some policy of the
declared function type separates their observation-history laws. -/
def ProbeDistinguishable (M₁ M₂ : POSystem S A O) (s : S) : Prop :=
  ∃ (π : List O → PMF A) (n : ℕ),
    obsProcess M₁ π n s [] ≠ obsProcess M₂ π n s []

-- LeanTest/HardProblems/SystemsTheory.lean
/-- A constant-action policy is a special case of an observation-dependent
policy. -/
theorem passively_imp_probe {M₁ M₂ : POSystem S A O} {a₀ : A} {s : S}
    (h : PassivelyDistinguishable M₁ M₂ a₀ s) : ProbeDistinguishable M₁ M₂ s :=
  let ⟨n, hn⟩ := h
  ⟨fun _ => PMF.pure a₀, n, hn⟩

-- LeanTest/HardProblems/SystemsTheory.lean
/-- There are two Boolean models whose laws agree under the constant action
`false` at every horizon but differ under the constant action `true`. In these
witness models, `false` is inert and `true` changes one model only. -/
theorem exists_probe_only_distinguishable :
    ∃ (M₁ M₂ : POSystem Bool Bool Bool) (s : Bool),
      ¬ PassivelyDistinguishable M₁ M₂ false s ∧ ProbeDistinguishable M₁ M₂ s := by
  refine ⟨flipModel, inertModel, false, ?_, ?_⟩
  · rintro ⟨n, hn⟩
    exact hn (obsProcess_congr_null flipModel inertModel false rfl
      (fun s => by simp [flipModel, inertModel]) n false [])
  · refine ⟨fun _ => PMF.pure true, 2, ?_⟩
    have h₁ : obsProcess flipModel (fun _ => PMF.pure true) 2 false [] =
        PMF.pure [false, true] := by
      simp [obsProcess, flipModel, PMF.pure_bind]
    have h₂ : obsProcess inertModel (fun _ => PMF.pure true) 2 false [] =
        PMF.pure [false, false] := by
      simp [obsProcess, inertModel, PMF.pure_bind]
    rw [h₁, h₂]
    intro hcontra
    have := congrArg (fun p => p [false, true]) hcontra
    simp [PMF.pure_apply] at this

-- LeanTest/HardProblems/Observability.lean
/-- Observational equivalence: no policy of the declared function type
distinguishes the two states at any finite horizon. -/
def ObsEquiv (M : POSystem S A O) (s s' : S) : Prop :=
  ∀ (π : List O → PMF A) (n : ℕ), obsProcess M π n s [] = obsProcess M π n s' []

-- LeanTest/HardProblems/Observability.lean
/-- Observational equivalence is an equivalence relation, as the notation
`≡` silently promises. -/
theorem obsEquiv_equivalence (M : POSystem S A O) : Equivalence (ObsEquiv M) where
  refl _ := fun _ _ => rfl
  symm h := fun π n => (h π n).symm
  trans h₁ h₂ := fun π n => (h₁ π n).trans (h₂ π n)

-- LeanTest/HardProblems/Observability.lean
/-- A necessary metric condition for asymptotic reconstruction: if the same
estimate converges to each of two state trajectories, their mutual distance
converges to zero. To turn this into a detectability theorem, a system-specific
argument must show that observationally indistinguishable trajectories really
feed the same estimate. -/
theorem common_estimate_forces_pairwise_convergence
    {X : Type*} [PseudoMetricSpace X] (x₁ x₂ xhat : ℕ → X)
    (h₁ : Tendsto (fun t => dist (x₁ t) (xhat t)) atTop (𝓝 0))
    (h₂ : Tendsto (fun t => dist (x₂ t) (xhat t)) atTop (𝓝 0)) :
    Tendsto (fun t => dist (x₁ t) (x₂ t)) atTop (𝓝 0) := by
  refine squeeze_zero (fun _ => dist_nonneg) (fun t => dist_triangle _ (xhat t) _) ?_
  have h₂' : Tendsto (fun t => dist (xhat t) (x₂ t)) atTop (𝓝 0) :=
    h₂.congr' (Eventually.of_forall fun t => dist_comm (x₂ t) (xhat t))
  simpa only [zero_add] using h₁.add h₂'

-- LeanTest/HardProblems/Observability.lean
/-- Decision-critical ambiguity: two observationally equivalent states whose
acceptable-action sets `A*_M` are disjoint. -/
def DecisionCritical (M : POSystem S A O) (Astar : S → Set A) (s s' : S) : Prop :=
  ObsEquiv M s s' ∧ Disjoint (Astar s) (Astar s')

-- LeanTest/HardProblems/Observability.lean
/-- An action is robust at `s` when it is acceptable in every state
observationally equivalent to `s`. -/
def RobustAcceptable (M : POSystem S A O) (Astar : S → Set A) (s : S) (a : A) : Prop :=
  ∀ s', ObsEquiv M s s' → a ∈ Astar s'

-- LeanTest/HardProblems/Observability.lean
/-- Robust actions are exactly the intersection of the acceptable sets over
the equivalence class of `s`. -/
theorem robustSet_eq_iInter (M : POSystem S A O) (Astar : S → Set A) (s : S) :
    {a | RobustAcceptable M Astar s a} = ⋂ s' ∈ {s' | ObsEquiv M s s'}, Astar s' := by
  ext a
  simp [RobustAcceptable]

-- LeanTest/HardProblems/Observability.lean
/-- Robust choice is infeasible when no action is acceptable throughout the
observational equivalence class. -/
def RobustlyInfeasible (M : POSystem S A O) (Astar : S → Set A) (s : S) : Prop :=
  ¬ ∃ a, RobustAcceptable M Astar s a

-- LeanTest/HardProblems/Observability.lean
/-- The exact criterion for robust infeasibility is emptiness of the total
intersection of acceptable-action sets over the observational class. Pairwise
disjointness is sufficient but not necessary for this intersection to be empty. -/
theorem robustlyInfeasible_iff_iInter_eq_empty
    (M : POSystem S A O) (Astar : S → Set A) (s : S) :
    RobustlyInfeasible M Astar s ↔
      ⋂ s' ∈ {s' | ObsEquiv M s s'}, Astar s' = ∅ := by
  rw [← robustSet_eq_iInter]
  change (¬ ({a | RobustAcceptable M Astar s a} : Set A).Nonempty) ↔ _
  exact Set.not_nonempty_iff_eq_empty

-- LeanTest/HardProblems/Observability.lean
/-- A disjoint observationally equivalent pair certifies that no robust action
exists at the first state. -/
theorem DecisionCritical.no_robust_action
    {M : POSystem S A O} {Astar : S → Set A} {s s' : S}
    (h : DecisionCritical M Astar s s') :
    ¬∃ a, RobustAcceptable M Astar s a := by
  rintro ⟨a, ha⟩
  have h₁ : a ∈ Astar s := ha s ((obsEquiv_equivalence M).refl s)
  have h₂ : a ∈ Astar s' := ha s' h.1
  exact Set.disjoint_left.mp h.2 h₁ h₂

Boundary. The formal policy space contains every function of the stated type, not only efficiently implementable experiments. Pairwise intersections need not imply a nonempty total intersection. The theorem assumes the kernels are the relevant model. The metric result is only a necessary condition for a common asymptotically correct observer. It does not connect smooth output histories to the formal stochastic equivalence or prove that such an observer exists. The active-probe counterexample compares two models and does not solve probe design or establish a minimal informative experiment.

Reachability, barriers, and backed shortcuts

Hypotheses. Deterministic effectors generate finite-composition reachability. A directed adjacency relation and real objective define finite path depth and its infimum barrier. A shortcut relation is backed by original paths whose score does not fall below the required endpoint bound.

Conclusion. Adding a pointwise programmed transformation leaves reachable sets unchanged, while a genuinely new transformation can enlarge one in an explicit finite example. Absence of any path gives infinite barrier; a monotone path gives zero barrier; positive barrier forces a dip along every available path. Properly backed shortcuts preserve barrier depth, while mere endpoint backing can fail. (machine-checked)

Lean declarations and proofs (BoundedMachines.lean, Ruggedness.lean): HardProblems.Reach, HardProblems.traj_mem_reach, HardProblems.Programmed, HardProblems.reach_insert_programmed, HardProblems.exists_new_effector_enlarges_reach, HardProblems.PathBetween, HardProblems.barrier, HardProblems.exists_dip_of_barrier_pos, HardProblems.barrier_eq_top_of_no_path, HardProblems.barrier_eq_zero_of_monotone_path, HardProblems.barrier_lt_iff, HardProblems.pathBetween_shortcut_nonempty_iff, HardProblems.barrier_shortcut_eq, HardProblems.exists_shortcut_hiding_valleyrun run

-- LeanTest/HardProblems/BoundedMachines.lean
/-- Finite-composition reachability: `y` is reachable from `x` by
applying effectors drawn from `G`. -/
inductive Reach (G : Set (X → X)) (x : X) : X → Prop
  | refl : Reach G x x
  | tail : ∀ {y z : X} {g : X → X}, Reach G x y → g ∈ G → z = g y → Reach G x z

-- LeanTest/HardProblems/BoundedMachines.lean
/-- Any admissible trajectory stays inside the reachable set: at each
step some effector in `G` was applied, chosen by an arbitrary policy,
and no choice rule ever escapes the orbit. -/
theorem traj_mem_reach (G : Set (X → X)) (σ : ℕ → X)
    (hstep : ∀ n, ∃ g ∈ G, σ (n + 1) = g (σ n)) (n : ℕ) :
    Reach G (σ 0) (σ n) := by
  induction n with
  | zero => exact Reach.refl
  | succ n ih =>
      obtain ⟨g, hg, heq⟩ := hstep n
      exact Reach.tail ih hg heq

-- LeanTest/HardProblems/BoundedMachines.lean
/-- Pointwise realizability over `G`: from every state, the image under `g` is
already reachable with `G`. The definition supplies neither a uniform generator
word nor a computable dispatcher for the witnessing paths. -/
def Programmed (G : Set (X → X)) (g : X → X) : Prop :=
  ∀ y : X, Reach G y (g y)

-- LeanTest/HardProblems/BoundedMachines.lean
/-- Inserting a pointwise realizable transformation as a primitive leaves every
reachability orbit unchanged. -/
theorem reach_insert_programmed (G : Set (X → X)) {g : X → X}
    (hg : Programmed G g) (x z : X) :
    Reach (insert g G) x z ↔ Reach G x z := by
  constructor
  · intro h
    induction h with
    | refl => exact Reach.refl
    | @tail y z f hy hmem heq ih =>
        rcases hmem with (rfl | hmem)
        · rw [heq]
          exact Reach.trans ih (hg y)
        · exact Reach.tail ih hmem heq
  · intro h
    induction h with
    | refl => exact Reach.refl
    | tail hy hmem heq ih =>
        exact Reach.tail ih (Set.mem_insert_of_mem g hmem) heq

-- LeanTest/HardProblems/BoundedMachines.lean
/-- A transformation outside the prior reachability closure can strictly
enlarge reach in an explicit two-state example. -/
theorem exists_new_effector_enlarges_reach :
    ∃ (G : Set (Bool → Bool)) (g : Bool → Bool) (x z : Bool),
      Reach (insert g G) x z ∧ ¬ Reach G x z := by
  refine ⟨∅, Bool.not, false, true, ?_, ?_⟩
  · exact Reach.tail Reach.refl (Set.mem_insert _ _) rfl
  · intro h
    cases h with
    | tail hy hmem heq => exact hmem.elim

-- LeanTest/HardProblems/Ruggedness.lean
/-- An admissible path in the configuration graph `Adj`, from `x` to `y`,
recorded as its list of visited configurations. -/
structure PathBetween (Adj : X → X → Prop) (x y : X) where
  points : List X
  head_eq : points.head? = some x
  last_eq : points.getLast? = some y
  admissible : points.IsChain Adj

-- LeanTest/HardProblems/Ruggedness.lean
/-- Barrier height from `x` to `y`: the infimum, over admissible paths, of the
deepest dip below `J x` along the path (dips measured in `ℝ≥0∞`, so paths
that never dip contribute `0`). Empty infimum is `⊤`: no path, infinite
barrier. -/
noncomputable def barrier (Adj : X → X → Prop) (J : X → ℝ) (x y : X) : ℝ≥0∞ :=
  ⨅ γ : PathBetween Adj x y, ⨆ z ∈ γ.points, ENNReal.ofReal (J x - J z)

-- LeanTest/HardProblems/Ruggedness.lean
/-- A positive barrier means every admissible route to `y` contains a
configuration strictly worse than the start. No hypothesis here says that `y`
is better than the start or that the dip occurs before first reaching `y`. -/
theorem exists_dip_of_barrier_pos {Adj : X → X → Prop} {J : X → ℝ} {x y : X}
    (h : 0 < barrier Adj J x y) (γ : PathBetween Adj x y) :
    ∃ z ∈ γ.points, J z < J x := by
  have hγ : 0 < ⨆ z ∈ γ.points, ENNReal.ofReal (J x - J z) :=
    lt_of_lt_of_le h (iInf_le _ γ)
  obtain ⟨z, hz⟩ := lt_iSup_iff.mp hγ
  obtain ⟨hmem, hpos⟩ := lt_iSup_iff.mp hz
  refine ⟨z, hmem, ?_⟩
  have := ENNReal.ofReal_pos.mp hpos
  linarith

-- LeanTest/HardProblems/Ruggedness.lean
/-- No admissible path at all makes the barrier infinite. -/
theorem barrier_eq_top_of_no_path {Adj : X → X → Prop} {J : X → ℝ} {x y : X}
    (h : IsEmpty (PathBetween Adj x y)) :
    barrier Adj J x y = ⊤ :=
  iInf_of_empty _

-- LeanTest/HardProblems/Ruggedness.lean
/-- If some admissible path never dips below the start value, the barrier
vanishes: the converse companion to `exists_dip_of_barrier_pos`. (Also
proved independently by Harmonic's Aristotle prover; see `aristotle/`.) -/
theorem barrier_eq_zero_of_monotone_path {Adj : X → X → Prop} {J : X → ℝ}
    {x y : X} (γ : PathBetween Adj x y) (hγ : ∀ z ∈ γ.points, J x ≤ J z) :
    barrier Adj J x y = 0 := by
  refine le_antisymm ?_ zero_le
  refine le_trans (iInf_le _ γ) ?_
  refine iSup_le fun z => iSup_le fun hz => ?_
  simp [ENNReal.ofReal_eq_zero, hγ z hz]

-- LeanTest/HardProblems/Ruggedness.lean
/-- The barrier sits strictly below `d` exactly when some admissible path
keeps every dip strictly below `d`. The backward direction uses the
finiteness of a path's point list: finitely many quantities each below `d`
have supremum below `d`. -/
theorem barrier_lt_iff {Adj : X → X → Prop} {J : X → ℝ} {x y : X}
    {d : ℝ≥0∞} :
    barrier Adj J x y < d ↔
      ∃ γ : PathBetween Adj x y, ∀ z ∈ γ.points,
        ENNReal.ofReal (J x - J z) < d := by
  constructor
  · intro h
    obtain ⟨γ, hγ⟩ := iInf_lt_iff.1 h
    exact ⟨γ, fun z hz =>
      lt_of_le_of_lt (le_biSup (fun z => ENNReal.ofReal (J x - J z)) hz) hγ⟩
  · rintro ⟨γ, hγ⟩
    have hx : x ∈ γ.points := List.mem_of_mem_head? γ.head_eq
    have hd : 0 < d := lt_of_le_of_lt zero_le (hγ x hx)
    exact lt_of_le_of_lt (iInf_le _ γ) (biSup_list_lt _ hd γ.points hγ)

-- LeanTest/HardProblems/Ruggedness.lean
/-- Reachability form: shortcuts backed by mere admissible paths do not
change what is reachable. -/
theorem pathBetween_shortcut_nonempty_iff {Adj S : X → X → Prop}
    (hback : ∀ u w, S u w → Nonempty (PathBetween Adj u w)) (x y : X) :
    Nonempty (PathBetween (fun a b => Adj a b ∨ S a b) x y) ↔
      Nonempty (PathBetween Adj x y) := by
  constructor
  · rintro ⟨γ⟩
    have hback' : ∀ u w, S u w → ∃ δ : PathBetween Adj u w,
        ∀ z ∈ δ.points, min ((fun _ : X => (0 : ℝ)) u) ((fun _ : X => (0 : ℝ)) w)
          ≤ (fun _ : X => (0 : ℝ)) z := by
      intro u w h
      obtain ⟨δ⟩ := hback u w h
      exact ⟨δ, fun _ _ => by simp⟩
    obtain ⟨γ', -⟩ := exists_splice hback' γ
    exact ⟨γ'⟩
  · rintro ⟨γ⟩
    exact ⟨γ.inl⟩

-- LeanTest/HardProblems/Ruggedness.lean
/-- Sufficient barrier certificate: shortcuts whose witnesses never dip below
the lower of their endpoints leave every barrier height unchanged. The theorem
does not claim that this certificate is necessary. -/
theorem barrier_shortcut_eq {Adj S : X → X → Prop} {J : X → ℝ}
    (hback : ∀ u w, S u w → ∃ γ : PathBetween Adj u w,
      ∀ z ∈ γ.points, min (J u) (J w) ≤ J z) (x y : X) :
    barrier (fun a b => Adj a b ∨ S a b) J x y = barrier Adj J x y := by
  refine le_antisymm (le_iInf fun γ => ?_) (le_iInf fun γ => ?_)
  · exact iInf_le_of_le γ.inl le_rfl
  · obtain ⟨γ', hγ'⟩ := exists_splice hback γ
    refine iInf_le_of_le γ' (iSup_le fun z => iSup_le fun hz => ?_)
    obtain ⟨p, hp, hple⟩ := hγ' z hz
    have key : ENNReal.ofReal (J x - J z) ≤ ENNReal.ofReal (J x - J p) :=
      ENNReal.ofReal_le_ofReal (by linarith)
    exact key.trans (le_biSup (fun p => ENNReal.ofReal (J x - J p)) hp)

-- LeanTest/HardProblems/Ruggedness.lean
/-- Mere `Nonempty` backing is insufficient for barrier preservation: a
shortcut can hide a valley. On the
two-step chain with a dip in the middle, admitting the backed shortcut
`0 → 2` drops the barrier from `ENNReal.ofReal 1` to `0`. This does not show
that the sufficient depth condition of `barrier_shortcut_eq` is necessary. -/
theorem exists_shortcut_hiding_valley :
    ∃ (Adj S : Fin 3 → Fin 3 → Prop) (J : Fin 3 → ℝ),
      (∀ u w, S u w → Nonempty (PathBetween Adj u w)) ∧
      ∃ x y : Fin 3,
        barrier (fun a b => Adj a b ∨ S a b) J x y < barrier Adj J x y := by
  refine ⟨hideAdj, hideS, hideJ, ?_, 0, 2, ?_⟩
  · intro u w huw
    obtain ⟨rfl, rfl⟩ : u = 0 ∧ w = 2 := huw
    refine ⟨⟨[0, 1, 2], rfl, rfl, ?_⟩⟩
    refine List.isChain_cons_cons.2 ⟨Or.inl ⟨rfl, rfl⟩, ?_⟩
    exact List.isChain_cons_cons.2 ⟨Or.inr ⟨rfl, rfl⟩, List.isChain_singleton _⟩
  · have hunion : barrier (fun a b => hideAdj a b ∨ hideS a b) hideJ 0 2 = 0 := by
      refine barrier_eq_zero_of_monotone_path ⟨[0, 2], rfl, rfl, ?_⟩ ?_
      · exact List.isChain_cons_cons.2 ⟨Or.inr ⟨rfl, rfl⟩, List.isChain_singleton _⟩
      · intro z hz
        have hz' : z = 0 ∨ z = 2 := by simpa using hz
        rcases hz' with rfl | rfl
        · exact le_rfl
        · rw [hideJ_zero, hideJ_two]
    have hlow : ENNReal.ofReal 1 ≤ barrier hideAdj hideJ 0 2 := by
      refine le_iInf fun γ => ?_
      have hmem : (1 : Fin 3) ∈ γ.points := one_mem_of_path γ
      have hval : ENNReal.ofReal 1 = ENNReal.ofReal (hideJ 0 - hideJ 1) := by
        rw [hideJ_zero, hideJ_one]; norm_num
      rw [hval]
      exact le_biSup (fun z => ENNReal.ofReal (hideJ 0 - hideJ z)) hmem
    rw [hunion]
    exact lt_of_lt_of_le (ENNReal.ofReal_pos.mpr one_pos) hlow

Boundary. Pointwise programming need not yield a uniform computable macro. Barrier depth is not search time or total traversal cost. Shortcut preservation holds only for the witnessed path property.

Behavior, safety, and coordinate invariance

Hypotheses. A behavior is a set of trajectories on a declared signal space. Interconnection is intersection after component interfaces have been aligned, and hiding is direct image under a signal map. Discrete runs obey a deterministic step map. Local signal functions agree on overlaps. Separately, an equivalence of deterministic state spaces conjugates every input-indexed transition and transports outputs, adjacency, and objective where required.

Conclusion. Hiding an interconnection is contained in interconnecting the hidden behaviors, and an explicit finite example makes the inclusion strict. Visible safety after hiding is exactly safety of the pulled-back predicate. For the behavior generated from a safe set, all-time safety is equivalent to one-step invariance. The empty behavior is safe but not viable. Compatible raw functions have a unique glue, but an explicit nonempty admissibility constraint can reject it. Under exact coordinate equivalence, runs commute, observational indistinguishability is preserved, reachable sets correspond, and transported barrier values are equal. (machine-checked)

Lean declarations and proofs (Behavioral.lean, Representation.lean): HardProblems.Behavioral.Trajectory, HardProblems.Behavioral.Behavior, HardProblems.Behavioral.mapTrajectory, HardProblems.Behavioral.hide, HardProblems.Behavioral.interconnect, HardProblems.Behavioral.hide_interconnect_subset, HardProblems.Behavioral.hide_interconnect_strict_counterexample, HardProblems.Behavioral.hide_equiv_symm, HardProblems.Behavioral.IsSafe, HardProblems.Behavioral.IsViable, HardProblems.Behavioral.empty_behavior_safe, HardProblems.Behavioral.empty_behavior_not_viable, HardProblems.Behavioral.isSafe_mono, HardProblems.Behavioral.isSafe_hide_iff, HardProblems.Behavioral.isSafe_hide, HardProblems.Behavioral.IsRun, HardProblems.Behavioral.generatedBehavior, HardProblems.Behavioral.generatedBehavior_safe_of_invariant, HardProblems.Behavioral.generatedBehavior_safe_iff_invariant, HardProblems.Behavioral.restrict, HardProblems.Behavioral.Compatible, HardProblems.Behavioral.existsUnique_glue, HardProblems.Behavioral.admissible_glue_counterexample, HardProblems.Representation.run, HardProblems.CoordinateObservation.Indist, HardProblems.CoordinateObservation.run_conj, HardProblems.CoordinateObservation.indist_conj_iff, HardProblems.CoordinateReach.reachableSet, HardProblems.CoordinateReach.run_conj, HardProblems.CoordinateReach.image_reachableSet_conj, HardProblems.CoordinateBarrier.PathBetween, HardProblems.CoordinateBarrier.Relabel, HardProblems.CoordinateBarrier.PathBetween.map, HardProblems.CoordinateBarrier.PathBetween.relabel, HardProblems.CoordinateBarrier.PathBetween.unrelabel, HardProblems.CoordinateBarrier.pathDepth, HardProblems.CoordinateBarrier.barrier, HardProblems.CoordinateBarrier.pathDepth_relabel, HardProblems.CoordinateBarrier.pathDepth_unrelabel, HardProblems.CoordinateBarrier.path_nonempty_relabel_iff, HardProblems.CoordinateBarrier.barrier_relabel_eqrun run

-- LeanTest/HardProblems/Behavioral.lean
/-- A complete signal trajectory on time domain `T`. -/
abbrev Trajectory (T : Type u) (W : Type v) := T → W

-- LeanTest/HardProblems/Behavioral.lean
/-- A behavior is the set of trajectories admitted by a system model. -/
abbrev Behavior (T : Type u) (W : Type v) := Set (Trajectory T W)

-- LeanTest/HardProblems/Behavioral.lean
/-- Apply a signal map pointwise to a trajectory. -/
def mapTrajectory {T : Type u} {W : Type v} {V : Type w}
    (f : W → V) (x : Trajectory T W) : Trajectory T V :=
  f ∘ x

-- LeanTest/HardProblems/Behavioral.lean
/-- Hide or relabel signal coordinates by taking the direct image of a
behavior under the pointwise signal map. -/
def hide {T : Type u} {W : Type v} {V : Type w}
    (f : W → V) (B : Behavior T W) : Behavior T V :=
  mapTrajectory f '' B

-- LeanTest/HardProblems/Behavioral.lean
/-- On one already aligned signal boundary, behavioral interconnection imposes
both component constraints. -/
def interconnect {T : Type u} {W : Type v}
    (B₁ B₂ : Behavior T W) : Behavior T W :=
  B₁ ∩ B₂

-- LeanTest/HardProblems/Behavioral.lean
/-- Hiding after interconnection is contained in interconnecting after hiding.
The reverse inclusion can fail because the two projected witnesses need not be
the same hidden trajectory. -/
theorem hide_interconnect_subset {T : Type u} {W : Type v} {V : Type w}
    (f : W → V) (B₁ B₂ : Behavior T W) :
    hide f (interconnect B₁ B₂) ⊆
      interconnect (hide f B₁) (hide f B₂) := by
  rintro _ ⟨x, ⟨hx₁, hx₂⟩, rfl⟩
  exact ⟨⟨x, hx₁, rfl⟩, ⟨x, hx₂, rfl⟩⟩

-- LeanTest/HardProblems/Behavioral.lean
/-- Explicit strictness witness: each component admits a different hidden Bool
trajectory with the same visible projection. The components are individually
viable, their interconnection is empty, but their visible projections have a
nonempty interconnection. -/
theorem hide_interconnect_strict_counterexample :
    let f : Bool × Bool → Bool := Prod.fst
    let x₀ : Trajectory Unit (Bool × Bool) := fun _ ↦ (false, false)
    let x₁ : Trajectory Unit (Bool × Bool) := fun _ ↦ (false, true)
    let B₀ : Behavior Unit (Bool × Bool) := {x₀}
    let B₁ : Behavior Unit (Bool × Bool) := {x₁}
    B₀.Nonempty ∧ B₁.Nonempty ∧ interconnect B₀ B₁ = ∅ ∧
      hide f (interconnect B₀ B₁) ⊂
        interconnect (hide f B₀) (hide f B₁) := by
  dsimp
  refine ⟨Set.singleton_nonempty _, Set.singleton_nonempty _, ?_⟩
  have hEmpty :
      interconnect ({fun _ : Unit ↦ (false, false)} :
        Behavior Unit (Bool × Bool)) {fun _ : Unit ↦ (false, true)} = ∅ := by
    apply Set.eq_empty_iff_forall_notMem.mpr
    rintro z ⟨hz₀, hz₁⟩
    rw [Set.mem_singleton_iff] at hz₀ hz₁
    have hEq : (fun _ : Unit ↦ (false, false)) =
        fun _ : Unit ↦ (false, true) := hz₀.symm.trans hz₁
    have := congrFun hEq ()
    simp at this
  refine ⟨hEmpty, ?_⟩
  refine Set.ssubset_iff_subset_ne.mpr
    ⟨hide_interconnect_subset _ _ _, ?_⟩
  intro hEq
  have hVisible : (fun _ : Unit ↦ false) ∈
      interconnect
        (hide Prod.fst ({fun _ : Unit ↦ (false, false)} :
          Behavior Unit (Bool × Bool)))
        (hide Prod.fst ({fun _ : Unit ↦ (false, true)} :
          Behavior Unit (Bool × Bool))) := by
    exact ⟨⟨_, rfl, rfl⟩, ⟨_, rfl, rfl⟩⟩
  have hImpossible : (fun _ : Unit ↦ false) ∈
      hide Prod.fst
        (interconnect ({fun _ : Unit ↦ (false, false)} :
          Behavior Unit (Bool × Bool)) {fun _ : Unit ↦ (false, true)}) := by
    rw [hEq]
    exact hVisible
  rw [hEmpty] at hImpossible
  rcases hImpossible with ⟨_, hmem, _⟩
  exact hmem

-- LeanTest/HardProblems/Behavioral.lean
/-- Exact relabeling by an equivalence loses no behavior. -/
theorem hide_equiv_symm {T : Type u} {W : Type v} {V : Type w}
    (e : W ≃ V) (B : Behavior T W) :
    hide e.symm (hide e B) = B := by
  ext x
  constructor
  · rintro ⟨_, ⟨z, hz, rfl⟩, hzx⟩
    have hzx' : z = x := by
      simpa [mapTrajectory, Function.comp_def] using hzx
    simpa [← hzx'] using hz
  · intro hx
    refine ⟨mapTrajectory e x, ⟨x, hx, rfl⟩, ?_⟩
    funext t
    simp [mapTrajectory, Function.comp_def]

-- LeanTest/HardProblems/Behavioral.lean
/-- A temporal safety predicate holds at every time on every admitted
trajectory. -/
def IsSafe {T : Type u} {W : Type v}
    (B : Behavior T W) (Safe : W → Prop) : Prop :=
  ∀ x ∈ B, ∀ t, Safe (x t)

-- LeanTest/HardProblems/Behavioral.lean
/-- A behavior is viable when it admits at least one trajectory. -/
def IsViable {T : Type u} {W : Type v} (B : Behavior T W) : Prop :=
  B.Nonempty

-- LeanTest/HardProblems/Behavioral.lean
/-- Universal safety is vacuous on the empty behavior. -/
theorem empty_behavior_safe {T : Type u} {W : Type v} {Safe : W → Prop} :
    IsSafe (∅ : Behavior T W) Safe := by
  simp [IsSafe]

-- LeanTest/HardProblems/Behavioral.lean
/-- The empty behavior is not viable. -/
theorem empty_behavior_not_viable {T : Type u} {W : Type v} :
    ¬ IsViable (∅ : Behavior T W) := by
  simp [IsViable]

-- LeanTest/HardProblems/Behavioral.lean
/-- Refining a behavior preserves every universal safety property. -/
theorem isSafe_mono {T : Type u} {W : Type v}
    {B B' : Behavior T W} {Safe : W → Prop}
    (hsub : B' ⊆ B) (h : IsSafe B Safe) : IsSafe B' Safe := by
  intro x hx t
  exact h x (hsub hx) t

-- LeanTest/HardProblems/Behavioral.lean
/-- Direct-image hiding has an exact safety semantics: a visible predicate
holds on every projected trajectory exactly when its pullback holds on every
original trajectory. This says nothing about predicates on discarded signal
coordinates. -/
theorem isSafe_hide_iff {T : Type u} {W : Type v} {V : Type w}
    (f : W → V) (B : Behavior T W) (SafeV : V → Prop) :
    IsSafe (hide f B) SafeV ↔ IsSafe B (SafeV ∘ f) := by
  constructor
  · intro h x hx t
    simpa [mapTrajectory, Function.comp_def] using
      h (mapTrajectory f x) ⟨x, hx, rfl⟩ t
  · rintro h _ ⟨x, hx, rfl⟩ t
    simpa [mapTrajectory, Function.comp_def] using h x hx t

-- LeanTest/HardProblems/Behavioral.lean
/-- Hiding preserves a safety property only when the signal map carries the
declared internal safe set into the external one. -/
theorem isSafe_hide {T : Type u} {W : Type v} {V : Type w}
    {B : Behavior T W} {SafeW : W → Prop} {SafeV : V → Prop}
    (f : W → V) (hB : IsSafe B SafeW)
    (hmap : ∀ w, SafeW w → SafeV (f w)) :
    IsSafe (hide f B) SafeV := by
  rintro _ ⟨x, hx, rfl⟩ t
  exact hmap (x t) (hB x hx t)

-- LeanTest/HardProblems/Behavioral.lean
/-- A discrete trajectory follows `step` at every successor time. -/
def IsRun {S : Type u} (step : S → S) (x : Trajectory ℕ S) : Prop :=
  ∀ n, x (n + 1) = step (x n)

-- LeanTest/HardProblems/Behavioral.lean
/-- All runs whose initial state lies in `Init`. -/
def generatedBehavior {S : Type u} (step : S → S) (Init : Set S) :
    Behavior ℕ S :=
  {x | x 0 ∈ Init ∧ IsRun step x}

-- LeanTest/HardProblems/Behavioral.lean
/-- Forward invariance gives all-time safety for every generated run. -/
theorem generatedBehavior_safe_of_invariant {S : Type u}
    {step : S → S} {Init Safe : Set S}
    (hInit : Init ⊆ Safe) (hInv : Set.MapsTo step Safe Safe) :
    IsSafe (generatedBehavior step Init) Safe := by
  rintro x ⟨hx₀, hrun⟩ n
  induction n with
  | zero => exact hInit hx₀
  | succ n ih =>
      rw [hrun n]
      exact hInv ih

-- LeanTest/HardProblems/Behavioral.lean
/-- For the behavior generated from every state in `Safe`, temporal safety is
equivalent to one-step forward invariance. -/
theorem generatedBehavior_safe_iff_invariant {S : Type u}
    (step : S → S) (Safe : Set S) :
    IsSafe (generatedBehavior step Safe) Safe ↔
      Set.MapsTo step Safe Safe := by
  constructor
  · intro h s hs
    let x : Trajectory ℕ S := fun n ↦ Nat.rec s (fun _ current ↦ step current) n
    have hrun : IsRun step x := by
      intro n
      simp [x]
    have hx : x ∈ generatedBehavior step Safe := by
      exact ⟨by simpa [x] using hs, hrun⟩
    have hs₁ := h x hx 1
    change x 1 ∈ Safe at hs₁
    simpa [x] using hs₁
  · intro hInv
    exact generatedBehavior_safe_of_invariant (by exact fun _ h ↦ h) hInv

-- LeanTest/HardProblems/Behavioral.lean
/-- Restrict a local trajectory from `I` to a smaller time domain `J`. -/
def restrict {T : Type u} {W : Type v} {I J : Set T}
    (hJI : J ⊆ I) (x : I → W) : J → W :=
  fun t ↦ x ⟨t.1, hJI t.2⟩

-- LeanTest/HardProblems/Behavioral.lean
/-- Two local trajectories agree wherever their time domains overlap. -/
def Compatible {T : Type u} {W : Type v} {I J : Set T}
    (x : I → W) (y : J → W) : Prop :=
  ∀ (t : T) (htI : t ∈ I) (htJ : t ∈ J),
    x ⟨t, htI⟩ = y ⟨t, htJ⟩

-- LeanTest/HardProblems/Behavioral.lean
/-- Compatible functions on two time domains have a unique global function on
their union with the prescribed restrictions. -/
theorem existsUnique_glue {T : Type u} {W : Type v} {I J : Set T}
    (x : I → W) (y : J → W) (hxy : Compatible x y) :
    ∃! z : ↥(I ∪ J) → W,
      restrict Set.subset_union_left z = x ∧
      restrict Set.subset_union_right z = y := by
  classical
  let z : ↥(I ∪ J) → W := fun t ↦
    if htI : (t : T) ∈ I then x ⟨t, htI⟩
    else y ⟨t, t.property.resolve_left htI⟩
  have hzI : restrict Set.subset_union_left z = x := by
    funext t
    simp [restrict, z]
  have hzJ : restrict Set.subset_union_right z = y := by
    funext t
    by_cases htI : (t : T) ∈ I
    · simpa [restrict, z, htI] using hxy t htI t.property
    · simp [restrict, z, htI]
  refine ⟨z, ⟨hzI, hzJ⟩, ?_⟩
  intro z' hz'
  funext t
  by_cases htI : (t : T) ∈ I
  · have h := congrFun hz'.1 (⟨t, htI⟩ : I)
    simpa [restrict, z, htI] using h
  · have htJ : (t : T) ∈ J := t.property.resolve_left htI
    have h := congrFun hz'.2 (⟨t, htJ⟩ : J)
    simpa [restrict, z, htI] using h

-- LeanTest/HardProblems/Behavioral.lean
/-- Raw compatible functions glue, but a nonempty declared set of admissible
global trajectories need not contain that glue. Thus arbitrary local/global
admissibility data do not acquire the sheaf property for free. -/
theorem admissible_glue_counterexample :
    let I : Set Bool := {false}
    let J : Set Bool := {true}
    let x : I → Bool := fun _ ↦ false
    let y : J → Bool := fun _ ↦ true
    let G : Set (↥(I ∪ J) → Bool) := {fun _ ↦ false}
    Compatible x y ∧ G.Nonempty ∧
      ¬ ∃ z ∈ G,
        restrict Set.subset_union_left z = x ∧
        restrict Set.subset_union_right z = y := by
  dsimp
  refine ⟨?_, Set.singleton_nonempty _, ?_⟩
  · intro t htI htJ
    rw [Set.mem_singleton_iff] at htI htJ
    exact Bool.noConfusion (htI.symm.trans htJ)
  · rintro ⟨z, hz, ⟨_, hzJ⟩⟩
    subst z
    have h := congrFun hzJ (⟨true, by simp⟩ : (↑({true} : Set Bool)))
    simp [restrict] at h

-- LeanTest/HardProblems/Representation.lean
/-- Drive deterministic dynamics with a finite input word, applying its
leftmost input first. -/
def run {U X : Type*} (step : U → X → X) : List U → X → X
  | [], x => x
  | u :: us, x => run step us (step u x)

-- LeanTest/HardProblems/Representation.lean
/-- Two states have identical outputs after every finite input word. -/
def Indist (step : U → X → X) (out : X → Y) (x x' : X) : Prop :=
  ∀ us : List U, out (run step us x) = out (run step us x')

-- LeanTest/HardProblems/Representation.lean
/-- A conjugating equivalence commutes with every finite run. -/
theorem run_conj (e : X ≃ X') {step : U → X → X}
    {step' : U → X' → X'}
    (hstep : ∀ u x, e (step u x) = step' u (e x)) (us : List U) (x : X) :
    e (run step us x) = run step' us (e x) := by
  induction us generalizing x with
  | nil => rfl
  | cons u us ih =>
    simp only [run]
    rw [ih, hstep]

-- LeanTest/HardProblems/Representation.lean
/-- Coordinate change preserves finite-word indistinguishability in both
directions when it conjugates transitions and preserves outputs. -/
theorem indist_conj_iff (e : X ≃ X') {step : U → X → X}
    {step' : U → X' → X'} {out : X → Y} {out' : X' → Y}
    (hstep : ∀ u x, e (step u x) = step' u (e x))
    (hout : ∀ x, out x = out' (e x)) (x y : X) :
    Indist step out x y ↔ Indist step' out' (e x) (e y) := by
  constructor
  · intro h us
    rw [← run_conj e hstep, ← run_conj e hstep]
    rw [← hout, ← hout]
    exact h us
  · intro h us
    rw [hout, hout]
    rw [run_conj e hstep, run_conj e hstep]
    exact h us

-- LeanTest/HardProblems/Representation.lean
/-- States reachable from `x` by some finite input word. -/
def reachableSet (step : U → X → X) (x : X) : Set X :=
  {z | ∃ us : List U, run step us x = z}

-- LeanTest/HardProblems/Representation.lean
/-- A conjugating equivalence commutes with every finite run. -/
theorem run_conj (e : X ≃ X') {step : U → X → X}
    {step' : U → X' → X'}
    (hstep : ∀ u x, e (step u x) = step' u (e x)) (us : List U) (x : X) :
    e (run step us x) = run step' us (e x) := by
  induction us generalizing x with
  | nil => rfl
  | cons u us ih =>
    simp only [run]
    calc
      e (run step us (step u x)) = run step' us (e (step u x)) := ih _
      _ = run step' us (step' u (e x)) := congrArg (run step' us) (hstep u x)

-- LeanTest/HardProblems/Representation.lean
/-- Coordinate change carries the concrete reachable set exactly onto the
reachable set in the conjugate coordinates. -/
theorem image_reachableSet_conj (e : X ≃ X') {step : U → X → X}
    {step' : U → X' → X'}
    (hstep : ∀ u x, e (step u x) = step' u (e x)) (x : X) :
    e '' reachableSet step x = reachableSet step' (e x) := by
  ext z
  constructor
  · rintro ⟨y, ⟨us, hus⟩, rfl⟩
    exact ⟨us, (run_conj e hstep us x).symm.trans (congrArg e hus)⟩
  · rintro ⟨us, hus⟩
    refine ⟨run step us x, ⟨us, rfl⟩, ?_⟩
    exact (run_conj e hstep us x).trans hus

-- LeanTest/HardProblems/Representation.lean
/-- A finite path including both endpoints. -/
structure PathBetween {X : Type u} (Adj : X → X → Prop) (x y : X) where
  points : List X
  head_eq : points.head? = some x
  last_eq : points.getLast? = some y
  admissible : points.IsChain Adj

-- LeanTest/HardProblems/Representation.lean
/-- Relabel a graph along a state-space equivalence. -/
def Relabel {X : Type u} {Y : Type v} (e : X ≃ Y)
    (Adj : X → X → Prop) : Y → Y → Prop :=
  fun a b => Adj (e.symm a) (e.symm b)

-- LeanTest/HardProblems/Representation.lean
/-- Map a path through any edge-preserving function. -/
def PathBetween.map {X : Type u} {Y : Type v}
    {Adj : X → X → Prop} {Adj' : Y → Y → Prop}
    (f : X → Y) (hstep : ∀ {a b}, Adj a b → Adj' (f a) (f b))
    {x y : X} (γ : PathBetween Adj x y) : PathBetween Adj' (f x) (f y) where
  points := γ.points.map f
  head_eq := by rw [List.head?_map, γ.head_eq]; rfl
  last_eq := by rw [List.getLast?_map, γ.last_eq]; rfl
  admissible := (List.isChain_map f).mpr
    (γ.admissible.imp fun _ _ h => hstep h)

-- LeanTest/HardProblems/Representation.lean
/-- Transport a path through a coordinate equivalence. -/
def PathBetween.relabel {X : Type u} {Y : Type v} {Adj : X → X → Prop}
    (e : X ≃ Y) {x y : X} (γ : PathBetween Adj x y) :
    PathBetween (Relabel e Adj) (e x) (e y) :=
  γ.map e (by intro a b h; simpa [Relabel] using h)

-- LeanTest/HardProblems/Representation.lean
/-- Return a transported path to the original coordinates. -/
def PathBetween.unrelabel {X : Type u} {Y : Type v} {Adj : X → X → Prop}
    (e : X ≃ Y) {x y : X}
    (γ : PathBetween (Relabel e Adj) (e x) (e y)) : PathBetween Adj x y := by
  simpa [Relabel] using
    γ.map e.symm (by intro a b h; simpa [Relabel] using h)

-- LeanTest/HardProblems/Representation.lean
/-- The deepest dip below the score of the starting vertex along one path. -/
noncomputable def pathDepth {X : Type u} {Adj : X → X → Prop}
    (J : X → ℝ) (x : X) {y : X} (γ : PathBetween Adj x y) : ℝ≥0∞ :=
  ⨆ z ∈ γ.points, ENNReal.ofReal (J x - J z)

-- LeanTest/HardProblems/Representation.lean
/-- The least path depth; the empty infimum is `⊤`. -/
noncomputable def barrier {X : Type u} (Adj : X → X → Prop)
    (J : X → ℝ) (x y : X) : ℝ≥0∞ :=
  ⨅ γ : PathBetween Adj x y, pathDepth J x γ

-- LeanTest/HardProblems/Representation.lean
/-- Relabeling a path and objective preserves that path's depth exactly. -/
theorem pathDepth_relabel {X : Type u} {Y : Type v}
    {Adj : X → X → Prop} (e : X ≃ Y) (J : X → ℝ)
    {x y : X} (γ : PathBetween Adj x y) :
    pathDepth (fun z => J (e.symm z)) (e x) (γ.relabel e) =
      pathDepth J x γ := by
  simp only [pathDepth, PathBetween.relabel, PathBetween.map,
    Equiv.symm_apply_apply]
  apply le_antisymm
  · refine iSup_le fun z => iSup_le fun hz => ?_
    obtain ⟨a, ha, rfl⟩ := List.mem_map.mp hz
    simpa using
      (le_iSup_of_le a
        (le_iSup_of_le ha (le_refl (ENNReal.ofReal (J x - J a)))))
  · refine iSup_le fun a => iSup_le fun ha => ?_
    refine le_iSup_of_le (e a) (le_iSup_of_le ?_ ?_)
    · exact List.mem_map.mpr ⟨a, ha, rfl⟩
    · simp

-- LeanTest/HardProblems/Representation.lean
/-- Returning a relabeled path to the source coordinates also preserves its
depth exactly. -/
theorem pathDepth_unrelabel {X : Type u} {Y : Type v}
    {Adj : X → X → Prop} (e : X ≃ Y) (J : X → ℝ)
    {x y : X} (γ : PathBetween (Relabel e Adj) (e x) (e y)) :
    pathDepth J x (γ.unrelabel e) =
      pathDepth (fun z => J (e.symm z)) (e x) γ := by
  simp only [pathDepth, unrelabel_points, Equiv.symm_apply_apply]
  apply le_antisymm
  · refine iSup_le fun a => iSup_le fun ha => ?_
    obtain ⟨z, hz, rfl⟩ := List.mem_map.mp ha
    exact le_iSup_of_le z (le_iSup_of_le hz (le_refl _))
  · refine iSup_le fun z => iSup_le fun hz => ?_
    refine le_iSup_of_le (e.symm z) (le_iSup_of_le ?_ ?_)
    · exact List.mem_map.mpr ⟨z, hz, rfl⟩
    · rfl

-- LeanTest/HardProblems/Representation.lean
/-- Exact coordinate changes preserve the existence of a path. -/
theorem path_nonempty_relabel_iff {X : Type u} {Y : Type v}
    {Adj : X → X → Prop} (e : X ≃ Y) {x y : X} :
    Nonempty (PathBetween (Relabel e Adj) (e x) (e y)) ↔
      Nonempty (PathBetween Adj x y) := by
  constructor
  · rintro ⟨γ⟩
    exact ⟨γ.unrelabel e⟩
  · rintro ⟨γ⟩
    exact ⟨γ.relabel e⟩

-- LeanTest/HardProblems/Representation.lean
/-- Exact coordinate changes preserve every barrier height, including the
infinite value caused by unreachability. -/
theorem barrier_relabel_eq {X : Type u} {Y : Type v}
    (Adj : X → X → Prop) (e : X ≃ Y) (J : X → ℝ) (x y : X) :
    barrier (Relabel e Adj) (fun z => J (e.symm z)) (e x) (e y) =
      barrier Adj J x y := by
  apply le_antisymm
  · refine le_iInf fun γ => ?_
    exact iInf_le_of_le (γ.relabel e)
      (le_of_eq (pathDepth_relabel e J γ))
  · refine le_iInf fun γ => ?_
    exact iInf_le_of_le (γ.unrelabel e)
      (le_of_eq (pathDepth_unrelabel e J γ))

Boundary. Intersection presupposes an aligned signal space. Function-level gluing does not prove that admitted behaviors form a sheaf. The finite failure example uses disjoint regions, so its compatibility premise is vacuous even though rejection of the unique raw glue is not. Universal safety can hold vacuously for an empty behavior, so viability is separate. The formal predicate covers the all-time safety fragment, not temporal logic in general; no site, topos, internal logic, hybrid model, or verification algorithm is formalized. Discovering an exact coordinate equivalence is not free, and lossy abstraction requires additional transfer proofs.

Exact abstraction and path lifting

Hypotheses. A map from a concrete transition system to an abstract one has forward simulation, local step lifting from each concrete representative, and goal preservation and reflection.

Conclusion. Concrete paths map to abstract paths, abstract paths lift from the stated concrete start, and reachability of the corresponding goals is equivalent. Exact abstractions compose. A finite counterexample shows that forward simulation without lifting does not justify the reverse direction. (machine-checked)

Lean declarations and proofs (Representation.lean): HardProblems.SolutionTransfer.Reach, HardProblems.SolutionTransfer.Reach.map, HardProblems.SolutionTransfer.ReachTo, HardProblems.SolutionTransfer.ForwardSimulation, HardProblems.SolutionTransfer.StepLifting, HardProblems.SolutionTransfer.concrete_reach_maps, HardProblems.SolutionTransfer.lift_reach, HardProblems.SolutionTransfer.abstract_reach_lifts, HardProblems.SolutionTransfer.ExactAbstraction, HardProblems.SolutionTransfer.ExactAbstraction.reachTo_iff, HardProblems.SolutionTransfer.ExactAbstraction.comp, HardProblems.SolutionTransfer.forward_without_lifting_counterexamplerun

-- LeanTest/HardProblems/Representation.lean
/-- Finite reflexive-transitive reachability generated by `Adj`. -/
inductive Reach {X : Type u} (Adj : X → X → Prop) (x : X) : X → Prop
  | refl : Reach Adj x x
  | tail {y z : X} : Reach Adj x y → Adj y z → Reach Adj x z

-- LeanTest/HardProblems/Representation.lean
/-- A map that preserves single steps preserves finite reachability. -/
theorem map {X : Type u} {Y : Type v} {Adj : X → X → Prop}
    {Adj' : Y → Y → Prop} {f : X → Y} {x y : X}
    (hstep : ∀ {a b}, Adj a b → Adj' (f a) (f b))
    (h : Reach Adj x y) : Reach Adj' (f x) (f y) := by
  induction h with
  | refl => exact Reach.refl
  | tail hxy hyz ih => exact Reach.tail ih (hstep hyz)

-- LeanTest/HardProblems/Representation.lean
/-- Some state in `G` is reachable from `x`. -/
def ReachTo {X : Type u} (Adj : X → X → Prop) (G : Set X) (x : X) : Prop :=
  ∃ y, Reach Adj x y ∧ y ∈ G

-- LeanTest/HardProblems/Representation.lean
/-- Every concrete step has a corresponding abstract step. -/
def ForwardSimulation {X : Type u} {Y : Type v} (f : X → Y)
    (Adj : X → X → Prop) (Adj' : Y → Y → Prop) : Prop :=
  ∀ {x y}, Adj x y → Adj' (f x) (f y)

-- LeanTest/HardProblems/Representation.lean
/-- Every abstract step offered at `f x` can be implemented from that actual
concrete representative `x`. This is stronger than requiring some member of
the fibre to implement the step. -/
def StepLifting {X : Type u} {Y : Type v} (f : X → Y)
    (Adj : X → X → Prop) (Adj' : Y → Y → Prop) : Prop :=
  ∀ (x : X) (y' : Y), Adj' (f x) y' →
    ∃ y : X, Adj x y ∧ f y = y'

-- LeanTest/HardProblems/Representation.lean
/-- Forward simulation sends a concrete solution to the image of its concrete
goal set. -/
theorem concrete_reach_maps {X : Type u} {Y : Type v}
    {Adj : X → X → Prop} {Adj' : Y → Y → Prop}
    {f : X → Y} {G : Set X} {x₀ : X}
    (hmap : ForwardSimulation f Adj Adj') :
    ReachTo Adj G x₀ → ReachTo Adj' (f '' G) (f x₀) := by
  rintro ⟨y, hxy, hyG⟩
  exact ⟨f y, Reach.map hmap hxy, ⟨y, hyG, rfl⟩⟩

-- LeanTest/HardProblems/Representation.lean
/-- Local step lifting extends to a lift of every finite abstract path, with
the endpoint lying in the required fibre. -/
theorem lift_reach {X : Type u} {Y : Type v}
    {Adj : X → X → Prop} {Adj' : Y → Y → Prop}
    {f : X → Y} (hlift : StepLifting f Adj Adj')
    {x : X} {y' : Y} (h : Reach Adj' (f x) y') :
    ∃ y : X, Reach Adj x y ∧ f y = y' := by
  induction h with
  | refl => exact ⟨x, Reach.refl, rfl⟩
  | @tail y' z' hxy hyz ih =>
      rcases ih with ⟨y, hxy', hy⟩
      rcases hlift y z' (hy ▸ hyz) with ⟨z, hyz', hz⟩
      exact ⟨z, Reach.tail hxy' hyz', hz⟩

-- LeanTest/HardProblems/Representation.lean
/-- An abstract solution descends when paths lift and abstract goal membership
reflects concrete success. -/
theorem abstract_reach_lifts {X : Type u} {Y : Type v}
    {Adj : X → X → Prop} {Adj' : Y → Y → Prop}
    {f : X → Y} {G : Set X} {G' : Set Y} {x₀ : X}
    (hlift : StepLifting f Adj Adj')
    (hreflect : ∀ x, f x ∈ G' → x ∈ G) :
    ReachTo Adj' G' (f x₀) → ReachTo Adj G x₀ := by
  rintro ⟨y', hxy, hyG⟩
  rcases lift_reach hlift hxy with ⟨y, hxy', hy⟩
  exact ⟨y, hxy', hreflect y (hy.symm ▸ hyG)⟩

-- LeanTest/HardProblems/Representation.lean
/-- The hypotheses for exact reachability transfer. -/
structure ExactAbstraction {X : Type u} {Y : Type v} (f : X → Y)
    (Adj : X → X → Prop) (Adj' : Y → Y → Prop)
    (G : Set X) (G' : Set Y) : Prop where
  mapStep : ForwardSimulation f Adj Adj'
  liftStep : StepLifting f Adj Adj'
  goalExact : ∀ x, x ∈ G ↔ f x ∈ G'

-- LeanTest/HardProblems/Representation.lean
/-- Under the exact hypotheses, concrete and abstract goal reachability agree. -/
theorem ExactAbstraction.reachTo_iff {X : Type u} {Y : Type v}
    {f : X → Y} {Adj : X → X → Prop} {Adj' : Y → Y → Prop}
    {G : Set X} {G' : Set Y} (h : ExactAbstraction f Adj Adj' G G') (x : X) :
    ReachTo Adj G x ↔ ReachTo Adj' G' (f x) := by
  constructor
  · rintro ⟨y, hxy, hyG⟩
    exact ⟨f y, Reach.map h.mapStep hxy, h.goalExact y |>.mp hyG⟩
  · exact abstract_reach_lifts h.liftStep (fun y => (h.goalExact y).mpr)

-- LeanTest/HardProblems/Representation.lean
/-- Exact abstractions compose. -/
theorem ExactAbstraction.comp {X : Type u} {Y : Type v} {Z : Type w}
    {f : X → Y} {g : Y → Z}
    {AdjX : X → X → Prop} {AdjY : Y → Y → Prop}
    {AdjZ : Z → Z → Prop} {GX : Set X} {GY : Set Y} {GZ : Set Z}
    (h₁ : ExactAbstraction f AdjX AdjY GX GY)
    (h₂ : ExactAbstraction g AdjY AdjZ GY GZ) :
    ExactAbstraction (g ∘ f) AdjX AdjZ GX GZ := by
  constructor
  · intro x y hxy
    exact h₂.mapStep (h₁.mapStep hxy)
  · intro x z hz
    rcases h₂.liftStep (f x) z hz with ⟨y, hxy, hy⟩
    rcases h₁.liftStep x y hxy with ⟨x', hxx', hx'⟩
    exact ⟨x', hxx', by simp only [Function.comp_apply, hx', hy]⟩
  · intro x
    exact (h₁.goalExact x).trans (h₂.goalExact (f x))

-- LeanTest/HardProblems/Representation.lean
/-- A forward simulation can have a reachable abstract goal with no concrete
representative. This explicit finite example isolates the missing lifting
condition. -/
theorem forward_without_lifting_counterexample :
    let f : Unit → Bool := fun _ => false
    let Adj : Unit → Unit → Prop := fun _ _ => False
    let Adj' : Bool → Bool → Prop := fun a b => a = false ∧ b = true
    ForwardSimulation f Adj Adj' ∧
      ReachTo Adj' ({true} : Set Bool) (f ()) ∧
      ¬ ReachTo Adj {x | f x = true} () := by
  dsimp
  constructor
  · intro x y h
    exact False.elim h
  constructor
  · exact ⟨true, Reach.tail Reach.refl ⟨rfl, rfl⟩, by simp⟩
  · rintro ⟨y, _, hy⟩
    simp at hy

Boundary. The theorem preserves reachability. It does not preserve probabilities, safety, path length, barrier depth, or computational cost unless additional hypotheses are proved.

Finite memory and delayed output

Hypotheses. An exact tracker intertwines transitions and outputs of an output-separated finite machine. Separately, with \(2\le b\) and \(0<n\), a one-pass register machine must emit the exact product of two fixed-width base-\(b\) operands from its final finite configuration.

Conclusion. The tracking map is injective, so the tracker has at least as many states as the tracked machine. The register machine needs at least \(b^n\) final configurations for \(n\)-digit base-\(b\) inputs; a bit budget therefore grows at least linearly with \(n\). (machine-checked)

Lean declarations and proofs (BoundedMachines.lean, Positional.lean): HardProblems.Machine, HardProblems.Machine.run, HardProblems.Machine.Separated, HardProblems.Tracks, HardProblems.Tracks.run_eq, HardProblems.Tracks.injective, HardProblems.card_le_of_tracks, HardProblems.card_eq_of_mutual_tracks, HardProblems.RegisterMachine, HardProblems.RegisterMachine.run, HardProblems.RegisterMachine.multiplicationInput, HardProblems.RegisterMachine.ComputesMultiplicationAt, HardProblems.RegisterMachine.finalState_injective, HardProblems.RegisterMachine.state_capacity_lower_bound, HardProblems.RegisterMachine.linear_bit_lower_bound, HardProblems.RegisterMachine.no_constant_register_budgetrun run

-- LeanTest/HardProblems/BoundedMachines.lean
/-- A deterministic machine with inputs `I`, outputs `O`, and state
space `S`: a step function and an output map. -/
structure Machine (I O S : Type*) where
  step : S → I → S
  out : S → O

-- LeanTest/HardProblems/BoundedMachines.lean
/-- Run a machine from state `s` on an input word `w`. -/
def Machine.run (M : Machine I O S) (s : S) (w : List I) : S :=
  w.foldl M.step s

-- LeanTest/HardProblems/BoundedMachines.lean
/-- A machine is output-separated when any two states that agree on the
outputs along every input word are equal. -/
def Machine.Separated (M : Machine I O S) : Prop :=
  ∀ s t : S, (∀ w : List I, M.out (M.run s w) = M.out (M.run t w)) → s = t

-- LeanTest/HardProblems/BoundedMachines.lean
/-- `f` tracks machine `B` inside machine `A`: the encoding intertwines
the dynamics and reproduces the outputs. This is what it means for `A`
to maintain a faithful copy of `B`. -/
structure Tracks (A : Machine I O S) (B : Machine I O T) (f : T → S) : Prop where
  step_eq : ∀ t i, f (B.step t i) = A.step (f t) i
  out_eq : ∀ t, A.out (f t) = B.out t

-- LeanTest/HardProblems/BoundedMachines.lean
/-- A tracking map intertwines whole runs, not just single steps. -/
theorem Tracks.run_eq {A : Machine I O S} {B : Machine I O T} {f : T → S}
    (h : Tracks A B f) (t : T) (w : List I) :
    f (B.run t w) = A.run (f t) w := by
  induction w generalizing t with
  | nil => rfl
  | cons i w ih =>
    simp [Machine.run]
    rw [← h.step_eq]
    exact ih (B.step t i)

-- LeanTest/HardProblems/BoundedMachines.lean
/-- Tracking an output-separated machine is injective: the tracker must
hold distinct internal states for distinct tracked states. -/
theorem Tracks.injective {A : Machine I O S} {B : Machine I O T} {f : T → S}
    (h : Tracks A B f) (hB : B.Separated) : Function.Injective f := by
  intro t₁ t₂ hft
  apply hB t₁ t₂
  intro w
  have eq1 : f (B.run t₁ w) = A.run (f t₁) w := h.run_eq t₁ w
  have eq2 : f (B.run t₂ w) = A.run (f t₂) w := h.run_eq t₂ w
  rw [← h.out_eq (B.run t₁ w), ← h.out_eq (B.run t₂ w), eq1, eq2, hft]

-- LeanTest/HardProblems/BoundedMachines.lean
/-- The pigeonhole bound: a finite machine can exactly track an
output-separated machine only if it has at least as many states. This is a
capacity bound for the stated exact tracking relation. -/
theorem card_le_of_tracks [Fintype S] [Fintype T]
    {A : Machine I O S} {B : Machine I O T} {f : T → S}
    (h : Tracks A B f) (hB : B.Separated) :
    Fintype.card T ≤ Fintype.card S := by
  exact Fintype.card_le_of_injective _ (Tracks.injective h hB)

-- LeanTest/HardProblems/BoundedMachines.lean
/-- Mutual exact tracking forces cardinality parity for finite
output-separated machines. It does not by itself give an isomorphism between
their transition systems. -/
theorem card_eq_of_mutual_tracks [Fintype S] [Fintype T]
    {A : Machine I O S} {B : Machine I O T} {f : T → S} {g : S → T}
    (hf : Tracks A B f) (hg : Tracks B A g)
    (hA : A.Separated) (hB : B.Separated) :
    Fintype.card S = Fintype.card T := by
  exact le_antisymm (card_le_of_tracks hg hA) (card_le_of_tracks hf hB)

-- LeanTest/HardProblems/Positional.lean
/-- A streaming machine with `k` finite-range registers. -/
structure RegisterMachine (base range k : ℕ) where
  init : Fin k → Fin range
  step : (Fin k → Fin range) → Fin base → (Fin k → Fin range)
  output : (Fin k → Fin range) → ℕ

-- LeanTest/HardProblems/Positional.lean
/-- Run a register machine over a finite input stream. -/
def run {base range k : ℕ} (M : RegisterMachine base range k) :
    List (Fin base) → (Fin k → Fin range) :=
  List.foldl M.step M.init

-- LeanTest/HardProblems/Positional.lean
/-- The fixed-width input stream for multiplying `x` and `y`. -/
def multiplicationInput (base n x y : ℕ) [NeZero base] : List (Fin base) :=
  fixedDigits base n x ++ fixedDigits base n y

-- LeanTest/HardProblems/Positional.lean
/-- The machine computes `n`-digit multiplication when its final-state output
is the product for every pair in the full fixed-width range `[0, base^n)`.
In particular, this quantifies over the actual transition-based execution; it
is not the mere existence of an unconstrained function on inputs. -/
def ComputesMultiplicationAt {base range k : ℕ} [NeZero base]
    (M : RegisterMachine base range k) (n : ℕ) : Prop :=
  ∀ x y, x < base ^ n → y < base ^ n →
    M.output (M.run (multiplicationInput base n x y)) = x * y

-- LeanTest/HardProblems/Positional.lean
/-- If a machine computes multiplication at width `n`, fixing the second
operand to one makes final configurations for distinct first operands distinct. -/
theorem finalState_injective {base range k n : ℕ} [NeZero base]
    (M : RegisterMachine base range k) (hbase : 2 ≤ base) (hn : 0 < n)
    (hM : M.ComputesMultiplicationAt n) :
    Function.Injective (fun x : Fin (base ^ n) =>
      M.run (multiplicationInput base n x 1)) := by
  intro x y hxy
  have h1 : (1 : ℕ) < base ^ n := one_lt_pow₀ (by omega) (by omega)
  have hx := hM x 1 x.is_lt h1
  have hy := hM y 1 y.is_lt h1
  simp only [mul_one] at hx hy
  simp only at hxy
  rw [hxy] at hx
  exact Fin.ext (hx.symm.trans hy)

-- LeanTest/HardProblems/Positional.lean
/-- The central configuration-count lower bound: a correct width-`n` machine
needs at least `base^n` different register configurations. -/
theorem state_capacity_lower_bound {base range k n : ℕ} [NeZero base]
    (M : RegisterMachine base range k) (hbase : 2 ≤ base) (hn : 0 < n)
    (hM : M.ComputesMultiplicationAt n) :
    base ^ n ≤ range ^ k := by
  have hinj := finalState_injective M hbase hn hM
  simpa using Fintype.card_le_of_injective _ hinj

-- LeanTest/HardProblems/Positional.lean
/-- Quantitative binary form.  If all register configurations can be encoded
in at most `bits` bits, correctness forces at least `n` bits. -/
theorem linear_bit_lower_bound {base range k n bits : ℕ} [NeZero base]
    (M : RegisterMachine base range k) (hbase : 2 ≤ base) (hn : 0 < n)
    (hM : M.ComputesMultiplicationAt n)
    (hbits : range ^ k ≤ 2 ^ bits) :
    n ≤ bits := by
  have h1 : base ^ n ≤ range ^ k := state_capacity_lower_bound M hbase hn hM
  have h2 : base ^ n ≤ 2 ^ bits := h1.trans hbits
  have h3 : 2 ^ n ≤ base ^ n := Nat.pow_le_pow_left hbase _
  have h4 : 2 ^ n ≤ 2 ^ bits := h3.trans h2
  exact (Nat.pow_le_pow_iff_right (by decide : 1 < 2)).mp h4

-- LeanTest/HardProblems/Positional.lean
/-- For every fixed finite register count and fixed finite value range, some
positive digit width cannot be handled under `ComputesMultiplicationAt`. Thus
no fixed finite configuration space satisfies this interface at every width. -/
theorem no_constant_register_budget (base range k : ℕ) (hbase : 2 ≤ base) :
    ∃ n > 0, ∀ M : RegisterMachine base range k,
      letI : NeZero base := ⟨by omega⟩
      ¬ M.ComputesMultiplicationAt n := by
  letI : NeZero base := ⟨by omega⟩
  have hbase1 : 1 < base := hbase
  by_cases hk : k = 0
  · exact ⟨1, by norm_num, fun M hM => by
      have hcap := state_capacity_lower_bound M hbase (by norm_num : 0 < 1) hM
      simp [hk] at hcap
      omega⟩
  · by_cases hr : range = 0
    · exact ⟨1, by norm_num, fun M hM => by
        have hcap := state_capacity_lower_bound M hbase (by norm_num : 0 < 1) hM
        simp [hr, hk] at hcap
        omega⟩
    · have hk0 : k ≠ 0 := hk
      have hpos : 0 < range ^ k := by positivity
      exact ⟨range ^ k, hpos, fun M hM => by
        have hcap := state_capacity_lower_bound M hbase hpos hM
        exact (Nat.lt_pow_self hbase1).not_ge hcap⟩

Boundary. The multiplication argument fixes one operand to one and is a delayed-copy lower bound. It does not establish arithmetic hardness. Equal cardinality is not sufficient for tracking, and approximate task-specific quotients can be smaller.

Finite envelopes and context-indexed region orders

Hypotheses. A program envelope is nonempty and finite, and each program has a real value. Separately, a category carries a strict contravariant family of partial orders with monotone reindexing that obeys identity and composition. In the concrete construction, performance-coordinate types form a functor, all subsets are reindexed by preimage, and encounters are assigned regions. For the conditional realized construction, encounter transport is additionally supplied with exact region compatibility.

Conclusion. Finite envelopes attain internal optima, and enlarging an envelope cannot worsen its optimum. A finite envelope can have a strict gap to an excluded program. Preimage reindexing is monotone and obeys the stated laws. Inclusion pulled back to encounters is a preorder and is antisymmetric exactly when the encounter-to-region map is injective. Surjective performance maps preserve and reflect ambient inclusion. An explicit non-surjective map shows failure of preimage reflection, while an explicit noninjective direct image shows the separate many-to-one collapse. When encounter transport is supplied with exact region compatibility, the realized-image subposets inherit split preimage reindexing. A counterexample shows that preimage closure can fail without an extra hypothesis. (machine-checked)

Lean declarations and proofs (FibredOrder.lean, ResourceBounds.lean): HardProblems.Envelope, HardProblems.exists_bounded_optimum, HardProblems.bounded_optimum_mono, HardProblems.exists_strict_envelope_gap, HardProblems.FibredOrder.SplitIndexedOrder, HardProblems.FibredOrder.SplitIndexedOrder.reindexHom, HardProblems.FibredOrder.SplitIndexedOrder.reindex_id_apply, HardProblems.FibredOrder.SplitIndexedOrder.reindex_comp_apply, HardProblems.FibredOrder.performanceRegions, HardProblems.FibredOrder.CompatibleEncounterRegions, HardProblems.FibredOrder.CompatibleEncounterRegions.RealizedRegion, HardProblems.FibredOrder.CompatibleEncounterRegions.instPartialOrderRealizedRegion, HardProblems.FibredOrder.CompatibleEncounterRegions.reindexRealized, HardProblems.FibredOrder.CompatibleEncounterRegions.reindexRealized_val, HardProblems.FibredOrder.CompatibleEncounterRegions.realizedRegionOrder, HardProblems.FibredOrder.CompatibleEncounterRegions.realizedRegionOrder_reindex_val, HardProblems.FibredOrder.ambient_preimage_can_be_unrealized, HardProblems.FibredOrder.EncounterLE, HardProblems.FibredOrder.encounterLE_refl, HardProblems.FibredOrder.encounterLE_trans, HardProblems.FibredOrder.encounterLE_antisymmetric_iff_injective, HardProblems.FibredOrder.constant_region_not_antisymmetric, HardProblems.FibredOrder.surjective_preimage_subset_iff, HardProblems.FibredOrder.equiv_preimage_subset_iff, HardProblems.FibredOrder.equiv_preimage_preserves_inclusion, HardProblems.FibredOrder.equiv_preimage_reflects_inclusion, HardProblems.FibredOrder.nonsurjective_preimage_not_order_reflecting, HardProblems.FibredOrder.noninjective_image_not_order_reflectingrun run

-- LeanTest/HardProblems/ResourceBounds.lean
/-- A resource envelope specifies which programs are admitted and requires the
admitted set to be finite. -/
structure Envelope (P : Type*) where
  admits : P → Prop
  finite : Set.Finite {p | admits p}

-- LeanTest/HardProblems/ResourceBounds.lean
/-- A real-valued objective attains a maximum on any nonempty finite resource
envelope. This is an existence theorem, not an optimization procedure. -/
theorem exists_bounded_optimum {P : Type*} (E : Envelope P) (V : P → ℝ)
    (hne : ∃ p, E.admits p) :
    ∃ p, E.admits p ∧ ∀ q, E.admits q → V q ≤ V p := by
  obtain ⟨p, hp, hmax⟩ :=
    Set.exists_max_image {p | E.admits p} V E.finite hne
  exact ⟨p, hp, hmax⟩

-- LeanTest/HardProblems/ResourceBounds.lean
/-- If one finite envelope is included in another, the value of an optimum in
the larger envelope is at least that of an optimum in the smaller envelope. -/
theorem bounded_optimum_mono {P : Type*} (E F : Envelope P) (V : P → ℝ)
    (hEF : ∀ p, E.admits p → F.admits p)
    (p : P) (hp : E.admits p) (_hopt : ∀ q, E.admits q → V q ≤ V p)
    (q : P) (_hq : F.admits q) (hqopt : ∀ r, F.admits r → V r ≤ V q) :
    V p ≤ V q := by
  exact hqopt p (hEF p hp)

-- LeanTest/HardProblems/ResourceBounds.lean
/-- There is a nonempty finite envelope whose internal optimum is strictly
dominated by an excluded program. The witness's objective is unbounded, so the
statement deliberately does not claim that the excluded program is a global
optimum. -/
theorem exists_strict_envelope_gap :
    ∃ (E : Envelope ℕ) (V : ℕ → ℝ) (p : ℕ),
      E.admits p ∧ (∀ q, E.admits q → V q ≤ V p) ∧
      ∃ r, V p < V r := by
  use ⟨fun n => n = 0, by simp⟩
  use fun n => n
  use 0
  simp
  exact ⟨1, by norm_num⟩

-- LeanTest/HardProblems/FibredOrder.lean
/-- A strict contravariant family of partial orders over a category.

The pointwise identity and composition equations record a chosen splitting.
They are the only categorical coherence claimed in this file. -/
structure SplitIndexedOrder (C : Type u) [Category.{v} C] where
  /-- The carrier of the ordered fiber over a context. -/
  Fiber : C → Type w
  /-- The partial order in each fiber. -/
  fiberOrder : (c : C) → PartialOrder (Fiber c)
  /-- Contravariant transport along a context morphism. -/
  reindex : {c d : C} → (c ⟶ d) → Fiber d → Fiber c
  /-- Reindexing along an identity is the identity. -/
  reindex_id : ∀ (c : C) (x : Fiber c), reindex (𝟙 c) x = x
  /-- Reindexing reverses categorical composition. -/
  reindex_comp : ∀ {c d e : C} (f : c ⟶ d) (g : d ⟶ e)
    (x : Fiber e), reindex (f ≫ g) x = reindex f (reindex g x)
  /-- Every reindexing map is monotone in the fiber orders. -/
  reindex_mono : ∀ {c d : C} (f : c ⟶ d) {x y : Fiber d},
    (fiberOrder d).le x y → (fiberOrder c).le (reindex f x) (reindex f y)

-- LeanTest/HardProblems/FibredOrder.lean
/-- Reindexing as an order homomorphism. -/
def reindexHom (P : SplitIndexedOrder C) {c d : C} (f : c ⟶ d) :
    P.Fiber d →o P.Fiber c where
  toFun := P.reindex f
  monotone' := by
    intro x y hxy
    exact P.reindex_mono f hxy

-- LeanTest/HardProblems/FibredOrder.lean
@[simp]
theorem reindex_id_apply (P : SplitIndexedOrder C) (c : C) (x : P.Fiber c) :
    P.reindex (𝟙 c) x = x :=
  P.reindex_id c x

-- LeanTest/HardProblems/FibredOrder.lean
@[simp]
theorem reindex_comp_apply (P : SplitIndexedOrder C) {c d e : C}
    (f : c ⟶ d) (g : d ⟶ e) (x : P.Fiber e) :
    P.reindex (f ≫ g) x = P.reindex f (P.reindex g x) :=
  P.reindex_comp f g x

-- LeanTest/HardProblems/FibredOrder.lean
/-- The context-indexed partial order of all candidate performance regions
induced by a functor of performance-coordinate types. Context morphisms act
on points by `Perf.map`; candidate regions move in the opposite direction by
preimage. Realizability by an encounter or program is not part of this data. -/
def performanceRegions {C : Type u} [Category.{v} C] (Perf : C ⥤ Type w) :
    SplitIndexedOrder C where
  Fiber c := Set (Perf.obj c)
  fiberOrder _ := inferInstance
  reindex f A := Perf.map f ⁻¹' A
  reindex_id c A := by
    ext x
    simp
  reindex_comp f g A := by
    ext x
    simp
  reindex_mono := by
    intro c d f A B hAB
    exact Set.preimage_mono hAB

-- LeanTest/HardProblems/FibredOrder.lean
/-- Encounter data sufficient to make realized performance regions stable
under contravariant context change.

No identity or composition equation is imposed on `transport` at the level of
raw encounters. Only its observable effect on regions is stored. That exact
compatibility is enough to induce split reindexing after duplicate encounter
witnesses have been forgotten. -/
structure CompatibleEncounterRegions {C : Type u} [Category.{v} C]
    (Perf : C ⥤ Type w) where
  /-- The type of admitted encounters in each context. -/
  Encounter : C → Type e
  /-- The candidate region actually realized by an encounter. -/
  region : (c : C) → Encounter c → Set (Perf.obj c)
  /-- Contravariant transport of encounters along a context map. -/
  transport : {c d : C} → (c ⟶ d) → Encounter d → Encounter c
  /-- Transport realizes exactly the preimage of the target encounter's
  region. -/
  region_transport : ∀ {c d : C} (f : c ⟶ d) (E : Encounter d),
    region c (transport f E) = Perf.map f ⁻¹' region d E

-- LeanTest/HardProblems/FibredOrder.lean
/-- A region together with the proposition that some admitted encounter
realizes it. Different encounter witnesses with the same region determine the
same element of this subtype. -/
def RealizedRegion (D : CompatibleEncounterRegions Perf) (c : C) :=
  {A : Set (Perf.obj c) // ∃ E : D.Encounter c, D.region c E = A}

-- LeanTest/HardProblems/FibredOrder.lean
/-- Realized regions inherit the antisymmetric subset order from their
underlying sets; encounter witnesses do not participate in equality. -/
instance instPartialOrderRealizedRegion (D : CompatibleEncounterRegions Perf)
    (c : C) : PartialOrder (D.RealizedRegion c) :=
  PartialOrder.lift Subtype.val Subtype.val_injective

-- LeanTest/HardProblems/FibredOrder.lean
/-- Reindex a realized region by preimage. Compatibility supplies a transported
encounter witnessing that the resulting region is realized in the source
context. -/
def reindexRealized (D : CompatibleEncounterRegions Perf) {c d : C}
    (f : c ⟶ d) (A : D.RealizedRegion d) : D.RealizedRegion c :=
  ⟨Perf.map f ⁻¹' A.1, by
    rcases A.2 with ⟨E, hE⟩
    refine ⟨D.transport f E, ?_⟩
    rw [D.region_transport, hE]⟩

-- LeanTest/HardProblems/FibredOrder.lean
/-- The underlying set of a reindexed realized region is transparently the
ambient preimage. -/
@[simp]
theorem reindexRealized_val (D : CompatibleEncounterRegions Perf) {c d : C}
    (f : c ⟶ d) (A : D.RealizedRegion d) :
    (D.reindexRealized f A).1 = Perf.map f ⁻¹' A.1 :=
  rfl

-- LeanTest/HardProblems/FibredOrder.lean
/-- Realized regions form a split context-indexed partial order. The split laws
hold for region values; they do not assert coherent identity or composition
laws for the chosen raw encounter transports. -/
def realizedRegionOrder (D : CompatibleEncounterRegions Perf) :
    SplitIndexedOrder C where
  Fiber c := D.RealizedRegion c
  fiberOrder _ := inferInstance
  reindex := D.reindexRealized
  reindex_id c A := by
    apply Subtype.ext
    ext x
    simp [reindexRealized]
  reindex_comp f g A := by
    apply Subtype.ext
    ext x
    simp [reindexRealized]
  reindex_mono := by
    intro c d f A B hAB
    exact Set.preimage_mono hAB

-- LeanTest/HardProblems/FibredOrder.lean
/-- The reindexing stored in `realizedRegionOrder` has the same transparent
preimage value as `reindexRealized`. -/
@[simp]
theorem realizedRegionOrder_reindex_val
    (D : CompatibleEncounterRegions Perf) {c d : C}
    (f : c ⟶ d) (A : D.RealizedRegion d) :
    ((D.realizedRegionOrder).reindex f A).1 = Perf.map f ⁻¹' A.1 :=
  rfl

-- LeanTest/HardProblems/FibredOrder.lean
/-- Without compatible encounter transport, an ambient preimage need not be
among the regions declared realized in the source context. Both declared
families below are nonempty, yet the preimage of the realized target region is
not a realized source region. -/
theorem ambient_preimage_can_be_unrealized :
    let f : Unit → Bool := fun _ ↦ false
    let sourceRealized : Set (Set Unit) := {∅}
    let targetRegion : Set Bool := {false}
    let targetRealized : Set (Set Bool) := {targetRegion}
    sourceRealized.Nonempty ∧ targetRealized.Nonempty ∧
      targetRegion ∈ targetRealized ∧
      f ⁻¹' targetRegion ∉ sourceRealized := by
  simp

-- LeanTest/HardProblems/FibredOrder.lean
/-- Compare encounters by inclusion of their attainable regions. This is the
pullback of the fiber order along an encounter-to-region map. -/
def EncounterLE {E : Type u} {P : Type w} (region : E → Set P)
    (x y : E) : Prop :=
  region x ⊆ region y

-- LeanTest/HardProblems/FibredOrder.lean
/-- Region comparison pulled back to encounters is reflexive. -/
theorem encounterLE_refl {E : Type u} {P : Type w} (region : E → Set P)
    (x : E) : EncounterLE region x x :=
  Set.Subset.rfl

-- LeanTest/HardProblems/FibredOrder.lean
/-- Region comparison pulled back to encounters is transitive. -/
theorem encounterLE_trans {E : Type u} {P : Type w} (region : E → Set P)
    {x y z : E} (hxy : EncounterLE region x y)
    (hyz : EncounterLE region y z) : EncounterLE region x z :=
  hxy.trans hyz

-- LeanTest/HardProblems/FibredOrder.lean
/-- The pulled-back comparison is antisymmetric exactly when the
encounter-to-region map is injective. Without injectivity it is only a
preorder on encounters; quotienting encounters by equal regions restores a
partial order. -/
theorem encounterLE_antisymmetric_iff_injective {E : Type u} {P : Type w}
    (region : E → Set P) :
    (∀ ⦃x y : E⦄, EncounterLE region x y →
      EncounterLE region y x → x = y) ↔ Function.Injective region := by
  constructor
  · intro h x y hxy
    apply h
    · simp [EncounterLE, hxy]
    · simp [EncounterLE, hxy]
  · intro hinj x y hxy hyx
    exact hinj (Set.Subset.antisymm hxy hyx)

-- LeanTest/HardProblems/FibredOrder.lean
/-- Two distinct encounters assigned the same region witness the failure of
antisymmetry. The failure is in the encounter presentation, not in the subset
order on regions. -/
theorem constant_region_not_antisymmetric :
    let region : Bool → Set Unit := fun _ ↦ ∅
    EncounterLE region false true ∧ EncounterLE region true false ∧
      false ≠ true := by
  simp [EncounterLE]

-- LeanTest/HardProblems/FibredOrder.lean
/-- Preimage along a surjective point map preserves and reflects inclusion.
Bijectivity is therefore sufficient but not necessary for exact comparison
transport at the level of arbitrary candidate regions. -/
theorem surjective_preimage_subset_iff {X : Type u} {Y : Type w}
    (f : X → Y) (hf : Function.Surjective f) (A B : Set Y) :
    f ⁻¹' A ⊆ f ⁻¹' B ↔ A ⊆ B := by
  constructor
  · intro h y hy
    rcases hf y with ⟨x, rfl⟩
    exact h hy
  · exact Set.preimage_mono

-- LeanTest/HardProblems/FibredOrder.lean
/-- A bijective coordinate change preserves and reflects inclusion after
contravariant reindexing. Hence an exact relabeling neither creates nor erases
comparisons between candidate performance regions. -/
theorem equiv_preimage_subset_iff {X : Type u} {Y : Type w}
    (e : X ≃ Y) (A B : Set Y) :
    e ⁻¹' A ⊆ e ⁻¹' B ↔ A ⊆ B :=
  surjective_preimage_subset_iff e e.surjective A B

-- LeanTest/HardProblems/FibredOrder.lean
/-- The preservation direction of exact coordinate invariance. -/
theorem equiv_preimage_preserves_inclusion {X : Type u} {Y : Type w}
    (e : X ≃ Y) {A B : Set Y} (h : A ⊆ B) :
    e ⁻¹' A ⊆ e ⁻¹' B :=
  (equiv_preimage_subset_iff e A B).2 h

-- LeanTest/HardProblems/FibredOrder.lean
/-- The reflection direction of exact coordinate invariance. It depends on
surjectivity and is unavailable for a general non-surjective coordinate map. -/
theorem equiv_preimage_reflects_inclusion {X : Type u} {Y : Type w}
    (e : X ≃ Y) {A B : Set Y} (h : e ⁻¹' A ⊆ e ⁻¹' B) :
    A ⊆ B :=
  (equiv_preimage_subset_iff e A B).1 h

-- LeanTest/HardProblems/FibredOrder.lean
/-- Explicit failure of preimage order reflection for a non-surjective point
map. The injective constant map `Unit → Bool` misses `true`, so the whole Bool
region and `{false}` have equal preimages even though the former is not
contained in the latter. The issue here is failure of surjectivity, not
many-to-one collapse. -/
theorem nonsurjective_preimage_not_order_reflecting :
    let f : Unit → Bool := fun _ ↦ false
    let A : Set Bool := Set.univ
    let B : Set Bool := {false}
    ¬ Function.Surjective f ∧
      f ⁻¹' A = f ⁻¹' B ∧ f ⁻¹' A ⊆ f ⁻¹' B ∧ ¬ A ⊆ B := by
  dsimp
  constructor
  · intro hf
    rcases hf true with ⟨x, hx⟩
    simp at hx
  constructor
  · ext x
    simp
  constructor
  · intro x hx
    simp
  · intro h
    have : true ∈ ({false} : Set Bool) := h (Set.mem_univ true)
    simp at this

-- LeanTest/HardProblems/FibredOrder.lean
/-- Explicit failure of direct-image order reflection for a noninjective point
map. The constant map `Bool → Unit` merges `false` and `true`, so their
singleton regions have equal direct images although neither singleton is
contained in the other. This is the separate many-to-one failure mode. -/
theorem noninjective_image_not_order_reflecting :
    let f : Bool → Unit := fun _ ↦ ()
    let A : Set Bool := {false}
    let B : Set Bool := {true}
    ¬ Function.Injective f ∧
      f '' A = f '' B ∧ f '' A ⊆ f '' B ∧ ¬ A ⊆ B := by
  dsimp
  constructor
  · intro hf
    have h : false = true := hf rfl
    simp at h
  constructor
  · ext x
    simp
  constructor
  · intro x hx
    simp
  · intro h
    have : false ∈ ({true} : Set Bool) := h (by simp)
    simp at this

Boundary. Finiteness does not make an optimizer computable or cheap. The ambient construction uses all subsets, and the realized construction assumes a sufficient compatible encounter transport and derives closure from it; region-level closure alone would be enough to define reindexing. Neither construction requires or proves upward closure. The formalization constructs the Grothendieck total category and its cartesian lifts, but it does not construct the quotient of raw encounters. Coordinate-set invariance does not establish equivalence of programs or systems. The preimage and direct-image failure examples concern different operations and must not be conflated.

The total category and its cartesian lifts

Hypotheses. A split indexed order over a base category of contexts: a partial order in each fibre, contravariant monotone reindexing, and pointwise identity and composition laws.

Conclusion. The indexed data package as a contravariant functor into categories, and mathlib's contravariant Grothendieck construction yields a total category with a projection to the base. The projection is a fibration in the standard sense. The transport supplied as data is exactly the domain of the canonical cartesian lift, and each fibre poset is equivalent to the standard fibre category of the projection. (machine-checked)

Lean declarations and proofs (GrothendieckFibration.lean): HardProblems.FibredOrder.reindexFunctor, HardProblems.FibredOrder.toCatFunctor, HardProblems.FibredOrder.toCatPseudofunctor, HardProblems.FibredOrder.total, HardProblems.FibredOrder.projection, HardProblems.FibredOrder.totalObj, HardProblems.FibredOrder.cartesianLift, HardProblems.FibredOrder.cartesianLift_isStronglyCartesian, HardProblems.FibredOrder.projection_isFibered, HardProblems.FibredOrder.reindex_is_cartesian_lift, HardProblems.FibredOrder.fiberFunctor, HardProblems.FibredOrder.fiberFunctor_isEquivalence, HardProblems.FibredOrder.fiberEquivrun

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- Reindexing along one arrow, regarded as a functor between thin categories. -/
def reindexFunctor (P : SplitIndexedOrder C) {c d : C} (f : c ⟶ d) :
    P.Fiber d ⥤ P.Fiber c where
  obj := P.reindex f
  map h := homOfLE (P.reindex_mono f h.le)

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- Package the indexed poset as a genuine contravariant functor into `Cat`. -/
def toCatFunctor (P : SplitIndexedOrder C) : Cᵒᵖ ⥤ Cat.{w, w} where
  obj c := Cat.of (P.Fiber c.unop)
  map f := (reindexFunctor P f.unop).toCatHom
  map_id c := by
    apply Cat.Hom.ext
    apply CategoryTheory.Functor.ext (fun x => P.reindex_id c.unop x)
  map_comp f g := by
    apply Cat.Hom.ext
    apply CategoryTheory.Functor.ext (fun x => P.reindex_comp g.unop f.unop x)

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- The strict functor, promoted to the pseudofunctor expected by mathlib's
contravariant Grothendieck construction. -/
abbrev toCatPseudofunctor (P : SplitIndexedOrder C) :
    Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{w, w} :=
  (toCatFunctor P).toPseudoFunctor'

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- The total category of the indexed order. -/
abbrev total (P : SplitIndexedOrder C) : Type _ :=
  Pseudofunctor.CoGrothendieck (toCatPseudofunctor P)

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- Projection of the total category to the original base. -/
abbrev projection (P : SplitIndexedOrder C) : total P ⥤ C :=
  Pseudofunctor.CoGrothendieck.forget (toCatPseudofunctor P)

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- The total object represented by `x` in the fiber over `c`. -/
abbrev totalObj (P : SplitIndexedOrder C) (c : C) (x : P.Fiber c) : total P :=
  { base := c, fiber := x }

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- The canonical arrow from the reindexed object to the original object. -/
def cartesianLift (P : SplitIndexedOrder C) {c d : C} (f : c ⟶ d) (x : P.Fiber d) :
    totalObj P c (P.reindex f x) ⟶ totalObj P d x where
  base := f
  fiber := 𝟙 _

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- The canonical reindexing arrow is strongly cartesian. -/
theorem cartesianLift_isStronglyCartesian (P : SplitIndexedOrder C)
    {c d : C} (f : c ⟶ d) (x : P.Fiber d) :
    (projection P).IsStronglyCartesian f (cartesianLift P f x) := by
  change (projection P).IsStronglyCartesian f
    (Pseudofunctor.CoGrothendieck.cartesianLift (F := toCatPseudofunctor P) x f)
  exact Pseudofunctor.CoGrothendieck.isStronglyCartesian_homCartesianLift
    (F := toCatPseudofunctor P) x f

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- The projection is a fibration over the original base category. -/
theorem projection_isFibered (P : SplitIndexedOrder C) :
    (projection P).IsFibered := by
  infer_instance

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- The chosen transport is exactly the domain of the canonical cartesian lift,
and that lift satisfies mathlib's cartesian universal property. -/
theorem reindex_is_cartesian_lift (P : SplitIndexedOrder C)
    {c d : C} (f : c ⟶ d) (x : P.Fiber d) :
    (projection P).IsCartesian f (cartesianLift P f x) ∧
      Pseudofunctor.CoGrothendieck.domainCartesianLift
        (F := toCatPseudofunctor P) x f = totalObj P c (P.reindex f x) := by
  constructor
  · letI : (projection P).IsStronglyCartesian f (cartesianLift P f x) :=
      cartesianLift_isStronglyCartesian P f x
    exact Functor.IsStronglyCartesian.isCartesian_of_isStronglyCartesian
      (projection P) f (cartesianLift P f x)
  · rfl

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- The original thin category maps to the standard fiber of the projection. -/
abbrev fiberFunctor (P : SplitIndexedOrder C) (c : C) :
    P.Fiber c ⥤ (projection P).Fiber c :=
  CategoryTheory.Functor.Fiber.inducedFunctor
    (Pseudofunctor.CoGrothendieck.comp_const (toCatPseudofunctor P) c)

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- The standard fiber category of the projection is equivalent to the original
partial order regarded as a thin category. -/
theorem fiberFunctor_isEquivalence (P : SplitIndexedOrder C) (c : C) :
    (fiberFunctor P c).IsEquivalence := by
  exact HasFibers.equiv c

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- Goal 4 in explicit categorical form. -/
noncomputable def fiberEquiv (P : SplitIndexedOrder C) (c : C) :
    P.Fiber c ≌ (projection P).Fiber c := by
  letI : (fiberFunctor P c).IsEquivalence := fiberFunctor_isEquivalence P c
  exact (fiberFunctor P c).asEquivalence

Boundary. The data are used to construct a fibration and nothing more. An opfibration would need covariant transport, that is, left adjoints to reindexing, which the structure does not supply; none is constructed, and none is refuted. A later card shows the splitting itself was forced rather than chosen: with poset fibres, no non-split presentation exists. Thinness of the fibres makes uniqueness of fibrewise factorizations automatic, but the cartesian property itself is inherited from the general construction and does not depend on the fibres being posets. Nothing identifies objects of unrelated fibres without a supplied context morphism.

Boundaries as closure operators

Hypotheses. A set of primitive transformations on a state space; an observation map on states; behaviors with hiding along a signal projection; and, separately, two ordered sets of possibilities related by a monotone reindexing map, each carrying a closure operator.

Conclusion. Reachable-set formation, observational saturation, and hiding followed by pullback along the projection are closure operators in mathlib's sense: extensive, monotone, and idempotent. Inserting a transformation that is already pointwise reachable leaves the reachable set fixed, and refining the observation map never enlarges any saturation. Adjoining the constant-true move to the empty move set over the Booleans strictly enlarges the reach of one starting state, with the witness in the statement rather than behind an existential. Hiding preserves interconnection only up to inclusion, and an explicit example makes the inclusion strict. An explicit finite example shows a closure operator need not commute with a monotone reindexing map, which is how the fibrewise reading fails. Every local copy of a borrowed definition appearing in a statement here is pinned to its home-module original by an agreement lemma, so the statements cannot drift from what the rest of the companion proves. (machine-checked)

Lean declarations and proofs (BoundaryClosures.lean): HardProblems.ClosureUnification.reachSet, HardProblems.ClosureUnification.reachClosure, HardProblems.ClosureUnification.reachSet_insert_programmed, HardProblems.ClosureUnification.exists_strict_enlargement, HardProblems.ClosureUnification.indistSaturation, HardProblems.ClosureUnification.indistClosure, HardProblems.ClosureUnification.indistClosure_le_of_refines, HardProblems.ClosureUnification.behavioralClosure, HardProblems.ClosureUnification.hide_interconnect_subset_and_strict, HardProblems.ClosureUnification.ReindexCommutes, HardProblems.ClosureUnification.addFalseClosure, HardProblems.ClosureUnification.reindex_closure_need_not_commute, HardProblems.ClosureUnification.reachSet_insert_const_true_strict, HardProblems.ClosureUnification.reach_agrees, HardProblems.ClosureUnification.indist_agrees, HardProblems.ClosureUnification.hide_agrees, HardProblems.ClosureUnification.programmed_agrees, HardProblems.ClosureUnification.robustActions_agrees, HardProblems.ClosureUnification.interconnect_agreesrun

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- The set of states reachable from a set of starting states. -/
def reachSet {X : Type u} (G : Set (X → X)) (S : Set X) : Set X :=
  {z | ∃ x ∈ S, Reach G x z}

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- Goal 1. `reachSet G` is a closure operator on `Set X`. -/
def reachClosure {X : Type u} (G : Set (X → X)) : ClosureOperator (Set X) where
  toFun := reachSet G
  monotone' := by
    intro S T hST z hz
    rcases hz with ⟨x, hxS, hxz⟩
    exact ⟨x, hST hxS, hxz⟩
  le_closure' := by
    intro S x hx
    exact ⟨x, hx, .refl⟩
  idempotent' := by
    intro S
    apply Set.Subset.antisymm
    · rintro z ⟨y, ⟨x, hx, hxy⟩, hyz⟩
      exact ⟨x, hx, hxy.trans hyz⟩
    · rintro z hz
      exact ⟨z, hz, .refl⟩

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- Goal 2. A programmed transformation adds no reachability. -/
theorem reachSet_insert_programmed {X : Type u} (G : Set (X → X))
    {g : X → X} (hg : Programmed G g) (S : Set X) :
    reachSet (insert g G) S = reachSet G S := by
  apply Set.Subset.antisymm
  · rintro z ⟨x, hx, hreach⟩
    exact ⟨x, hx, hreach.insert_programmed hg⟩
  · rintro z ⟨x, hx, hreach⟩
    exact ⟨x, hx, by
      induction hreach with
      | refl => exact .refl
      | tail hstep hmem hz ih => exact .tail ih (Set.mem_insert_of_mem _ hmem) hz⟩

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- Goal 3. The concrete two-state system `Bool`, with no old primitives,
initial state `false`, and the new constant-`true` primitive, strictly enlarges
reachable closure. -/
theorem exists_strict_enlargement :
    ∃ (X : Type) (G : Set (X → X)) (g : X → X) (S : Set X),
      reachSet G S ⊂ reachSet (insert g G) S := by
  refine ⟨Bool, ∅, (fun _ => true), {false}, ?_⟩
  constructor
  · rintro z ⟨x, hx, hreach⟩
    exact ⟨x, hx, by
      induction hreach with
      | refl => exact .refl
      | tail hstep hmem hz => exact False.elim hmem⟩
  · intro hreverse
    have htrue : true ∈ reachSet (insert (fun _ : Bool => true) ∅) {false} :=
      ⟨false, by simp,
        Reach.tail (g := fun _ : Bool => true) Reach.refl (by simp) rfl⟩
    have hold : true ∈ reachSet (∅ : Set (Bool → Bool)) {false} := hreverse htrue
    rcases hold with ⟨x, hx, hreach⟩
    have hxfalse : x = false := by simpa using hx
    subst x
    have hempty : ∀ z : Bool, Reach (∅ : Set (Bool → Bool)) false z → z = false := by
      intro z hz
      induction hz with
      | refl => rfl
      | tail hstep hmem heq => exact False.elim hmem
    have : true = false := hempty true hreach
    cases this

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- Saturation of states under equality of observations. -/
def indistSaturation {S : Type u} {O : Type v} (observe : S → O)
    (T : Set S) : Set S :=
  {y | ∃ x ∈ T, Indist observe x y}

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- Goal 4. Saturation under observational indistinguishability is a closure
operator on `Set S`. -/
def indistClosure {S : Type u} {O : Type v} (observe : S → O) :
    ClosureOperator (Set S) where
  toFun := indistSaturation observe
  monotone' := by
    rintro A B h y ⟨x, hx, hxy⟩
    exact ⟨x, h hx, hxy⟩
  le_closure' := by
    intro A x hx
    exact ⟨x, hx, rfl⟩
  idempotent' := by
    intro A
    apply Set.Subset.antisymm
    · rintro y ⟨x, ⟨z, hz, hzx⟩, hxy⟩
      exact ⟨z, hz, hzx.trans hxy⟩
    · intro y hy
      exact ⟨y, hy, rfl⟩

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- Goal 4'. If `coarse = k ∘ fine`, fine observational saturation is contained
in coarse observational saturation: a finer experiment separates at least as
many states. -/
theorem indistClosure_le_of_refines {S : Type u} {F : Type v} {Cc : Type w}
    (fine : S → F) (coarse : S → Cc) (k : F → Cc) (hk : coarse = k ∘ fine) :
    ∀ T : Set S, indistClosure fine T ⊆ indistClosure coarse T := by
  intro T y hy
  rcases hy with ⟨x, hx, hxy⟩
  refine ⟨x, hx, ?_⟩
  show coarse x = coarse y
  rw [hk]
  exact congrArg k hxy

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- Pulling a hidden behavior back along the trajectory projection gives a
closure operator on behaviors. -/
def behavioralClosure {T : Type u} {W : Type v} {V : Type w} (f : W → V) :
    ClosureOperator (Behavior T W) where
  toFun B := {w | f ∘ w ∈ hide f B}
  monotone' := by
    rintro B C h w ⟨w', hw', heq⟩
    exact ⟨w', h hw', heq⟩
  le_closure' := by
    intro B w hw
    exact ⟨w, hw, rfl⟩
  idempotent' := by
    intro B
    apply Set.Subset.antisymm
    · rintro w ⟨w', ⟨w'', hw'', heq'⟩, heq⟩
      exact ⟨w'', hw'', heq'.trans heq⟩
    · intro w hw
      exact ⟨w, hw, rfl⟩

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- Goal 5. Hiding after interconnection is always contained in interconnecting
after hiding. The displayed `Bool`/`Unit` example makes this inclusion strict,
so hiding is not a meet (lattice) homomorphism. -/
theorem hide_interconnect_subset_and_strict :
    (∀ {T W V : Type} (f : W → V) (B₁ B₂ : Behavior T W),
      hide f (interconnect B₁ B₂) ⊆ interconnect (hide f B₁) (hide f B₂)) ∧
    (let B₁ : Behavior Unit Bool := {w | w () = false}
     let B₂ : Behavior Unit Bool := {w | w () = true}
     hide (fun _ : Bool => ()) (interconnect B₁ B₂) ⊂
       interconnect (hide (fun _ : Bool => ()) B₁)
         (hide (fun _ : Bool => ()) B₂)) := by
  constructor
  · intro T W V f B₁ B₂ v hv
    rcases hv with ⟨w, ⟨hw₁, hw₂⟩, rfl⟩
    exact ⟨⟨w, hw₁, rfl⟩, ⟨w, hw₂, rfl⟩⟩
  · dsimp
    constructor
    · intro v hv
      rcases hv with ⟨w, ⟨hw₁, hw₂⟩, rfl⟩
      exact ⟨⟨w, hw₁, rfl⟩, ⟨w, hw₂, rfl⟩⟩
    · intro hreverse
      let v : Unit → Unit := fun _ => ()
      have hv : v ∈ interconnect
          (hide (fun _ : Bool => ()) {w : Unit → Bool | w () = false})
          (hide (fun _ : Bool => ()) {w : Unit → Bool | w () = true}) := by
        constructor
        · exact ⟨(fun _ => false), rfl, rfl⟩
        · exact ⟨(fun _ => true), rfl, rfl⟩
      have hv' := hreverse hv
      rcases hv' with ⟨w, ⟨hwf, hwt⟩, _⟩
      simp only [Set.mem_setOf_eq] at hwf hwt
      rw [hwf] at hwt
      contradiction

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- A reindexing order homomorphism commutes with two fiberwise closures when
the two possible composites agree pointwise. -/
def ReindexCommutes {P : Type u} {Q : Type v} [Preorder P] [Preorder Q]
    (r : Q →o P) (cQ : ClosureOperator Q) (cP : ClosureOperator P) : Prop :=
  ∀ x, r (cQ x) = cP (r x)

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- The closure on `Set Bool` that adjoins `false`. -/
def addFalseClosure : ClosureOperator (Set Bool) where
  toFun S := S ∪ {false}
  monotone' := by
    intro A B h x hx
    exact hx.elim (fun hxA => Or.inl (h hxA)) Or.inr
  le_closure' := by
    intro A x hx
    exact Or.inl hx
  idempotent' := by
    intro A
    ext x
    simp only [Set.mem_union, Set.mem_singleton_iff]
    tauto

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- Reindexing by inverse image along the map `Unit → Bool` selecting `false`
does not commute with `addFalseClosure` and the identity closure on `Set Unit`.
Both carriers are nonempty, nontrivial finite posets. -/
theorem reindex_closure_need_not_commute :
    let r : Set Bool →o Set Unit :=
      { toFun := Set.preimage (fun _ : Unit => false)
        monotone' := by intro A B h; exact Set.preimage_mono h }
    ¬ ReindexCommutes r addFalseClosure (ClosureOperator.id (Set Unit)) := by
  intro r h
  have heq := h (∅ : Set Bool)
  have hunit : () ∈ r (addFalseClosure (∅ : Set Bool)) := Or.inr rfl
  rw [heq] at hunit
  exact hunit

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- The strict enlargement of Goal 3, restated with its witness in the
statement rather than behind an existential: adjoining the constant-`true`
move to the empty move set strictly enlarges what is reachable from
`{false}`. -/
theorem reachSet_insert_const_true_strict :
    reachSet (∅ : Set (Bool → Bool)) {false} ⊂
      reachSet (insert (fun _ => true) (∅ : Set (Bool → Bool))) {false} := by
  constructor
  · rintro z ⟨x, hx, h⟩
    refine ⟨x, hx, ?_⟩
    induction h with
    | refl => exact Reach.refl
    | tail _ hg hz ih => exact Reach.tail ih (Set.mem_insert_of_mem _ hg) hz
  · intro hrev
    have htrue : true ∈
        reachSet (insert (fun _ => true) (∅ : Set (Bool → Bool))) {false} :=
      ⟨false, rfl, Reach.tail Reach.refl (Set.mem_insert _ _) rfl⟩
    rcases hrev htrue with ⟨x, hx, h⟩
    cases h with
    | refl => simp at hx
    | tail _ hg _ => simp at hg

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- The local `Reach` is the project's `Reach`, definitionally. -/
theorem reach_agrees {X : Type u} (G : Set (X → X)) (x z : X) :
    ClosureUnification.Reach G x z ↔ HardProblems.Reach G x z := by
  constructor
  · intro h
    induction h with
    | refl => exact HardProblems.Reach.refl
    | tail hxy hg hz ih => exact HardProblems.Reach.tail ih hg hz
  · intro h
    induction h with
    | refl => exact ClosureUnification.Reach.refl
    | tail hxy hg hz ih => exact ClosureUnification.Reach.tail ih hg hz

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- The local `Indist` is `InformationOrder.Indist`, definitionally. -/
theorem indist_agrees {S : Type u} {O : Type v} (observe : S → O) (x y : S) :
    ClosureUnification.Indist observe x y ↔
      InformationOrder.Indist observe x y :=
  Iff.rfl

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- The local `hide` is `Behavioral.hide`, definitionally. -/
theorem hide_agrees {T : Type u} {W : Type v} {V : Type w}
    (f : W → V) (B : ClosureUnification.Behavior T W) :
    ClosureUnification.hide f B = Behavioral.hide f B := by
  rfl

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- The local `Programmed` is the project's `Programmed`: both quantify the
respective `Reach`, and `reach_agrees` bridges those. -/
theorem programmed_agrees {X : Type u} (G : Set (X → X)) (g : X → X) :
    ClosureUnification.Programmed G g ↔ HardProblems.Programmed G g := by
  constructor
  · intro h y
    exact (reach_agrees G y (g y)).mp (h y)
  · intro h y
    exact (reach_agrees G y (g y)).mpr (h y)

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- The local `RobustActions` is `InformationOrder.RobustActions`,
definitionally. -/
theorem robustActions_agrees {S : Type u} {O : Type v} {A : Type w}
    (observe : S → O) (Acceptable : S → A → Prop) (x : S) :
    ClosureUnification.RobustActions observe Acceptable x =
      InformationOrder.RobustActions observe Acceptable x :=
  rfl

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- The local `interconnect` is `Behavioral.interconnect`, definitionally. -/
theorem interconnect_agrees {T : Type u} {W : Type v}
    (B₁ B₂ : ClosureUnification.Behavior T W) :
    ClosureUnification.interconnect B₁ B₂ = Behavioral.interconnect B₁ B₂ :=
  rfl

Boundary. The closure operators act on possibility sets induced by the information, action, and behavior boundaries; no claim is made that every operator in the book has this shape, and the attainable-region map of the resource boundary is not among them. The lattice-homomorphism strengthening is refuted, not merely left open. Commutation with reindexing is an extra condition to be supplied for each context pair; the counterexample shows it does not follow from the closure laws alone.

Group completion forgets the order

Hypotheses. Difficulty classes form a commutative monoid; the concrete instances are subsets of a performance space under union, and the saturating cost scale obtained by adjoining an absorbing top element to the naturals.

Conclusion. The Grothendieck group of every commutative idempotent monoid is a one-element group, with no finiteness or nonemptiness assumption, so the region monoid over every performance space has trivial completion, and the distinct regions containing exactly true and exactly false collapse to the same element. The canonical map identifies two classes exactly when a common factor cancels them into agreement, and it is injective on every cancellative commutative monoid. The saturating cost scale also has trivial additive completion. (machine-checked)

Lean declarations and proofs (KTheoryCollapse.lean): HardProblems.KTheoryCollapse.RegionMonoid, HardProblems.KTheoryCollapse.grothendieckGroup_subsingleton_of_idempotent, HardProblems.KTheoryCollapse.grothendieckGroup_regionMonoid_subsingleton, HardProblems.KTheoryCollapse.grothendieckGroup_of_eq_iff, HardProblems.KTheoryCollapse.toGrothendieckGroup_injective_of_cancel, HardProblems.KTheoryCollapse.concrete_regions_collapse, HardProblems.KTheoryCollapse.withTop_cost_top_add_image, HardProblems.KTheoryCollapse.saturating_costs_grothendieckAddGroup_subsingletonrun

-- LeanTest/HardProblems/KTheoryCollapse.lean
/-- Attainable-performance regions over a performance space `P`, composing by
union. -/
abbrev RegionMonoid (P : Type u) := Set P

-- LeanTest/HardProblems/KTheoryCollapse.lean
/-- Goal 1': the Grothendieck group of every commutative idempotent monoid is
trivial. -/
theorem grothendieckGroup_subsingleton_of_idempotent
    (M : Type u) [CommMonoid M] (hidem : ∀ a : M, a * a = a) :
    Subsingleton (GrothendieckGroup M) := by
  refine ⟨fun x y => ?_⟩
  -- We'll show all elements equal GrothendieckGroup.of 1
  suffices ∀ z : GrothendieckGroup M, z = GrothendieckGroup.of 1 by rw [this x, this y]
  intro z
  -- Use Quot.induction_on to work with representatives
  induction z using Quot.induction_on with
  | h p => 
    -- p : M × ⊤, need to show Quot.mk oreEqv p = 1
    let ⟨a, b⟩ := p
    -- Need to show Quot.mk oreEqv (a, b) = GrothendieckGroup.of 1
    -- First show GrothendieckGroup.of 1 = Quot.mk oreEqv (1, 1)
    have of_one_eq : GrothendieckGroup.of 1 = Quot.mk (OreLocalization.oreEqv ⊤ M) (1, 1) := by
      rfl
    rw [of_one_eq]
    -- Now use Quot.eq
    apply Quot.sound
    unfold OreLocalization.oreEqv
    -- Need ∃ u v, u • (1,1).1 = v • (a,b).1 ∧ u * (1,1).2 = v * (a,b).2
    -- i.e., ∃ u v, u = v * a ∧ u = v * b
    -- Take v = a * b, u = a * b
    refine ⟨⟨a * b, ?_⟩, a * b, ?_⟩
    · simp
    · constructor
      · -- ⟨a * ↑b, _⟩ • 1 = (a * ↑b) • a
        simp only [Submonoid.mk_smul, smul_eq_mul]
        rw [mul_one]
        conv_rhs => rw [mul_assoc, mul_comm, mul_assoc, hidem]
        rw [mul_comm]
      · -- ↑⟨a * ↑b, _⟩ * ↑(1,1).2 = a * ↑b * ↑(a,b).2
        simp [mul_one]
        rw [mul_assoc, hidem]

-- LeanTest/HardProblems/KTheoryCollapse.lean
/-- Goal 1: the Grothendieck group of the region monoid is trivial, for every
performance type `P` (including the empty type). -/
theorem grothendieckGroup_regionMonoid_subsingleton (P : Type u) :
    Subsingleton (GrothendieckGroup (RegionMonoid P)) := by
  apply grothendieckGroup_subsingleton_of_idempotent
  exact Set.union_self

-- LeanTest/HardProblems/KTheoryCollapse.lean
/-- Goal 2: canonical images are equal exactly when the two elements become
equal after multiplying by a common slack element. -/
theorem grothendieckGroup_of_eq_iff (M : Type u) [CommMonoid M] (a b : M) :
    GrothendieckGroup.of a = GrothendieckGroup.of b ↔
      ∃ c : M, a * c = b * c := by
  change Localization.mk a 1 = Localization.mk b 1 ↔ _
  rw [Localization.mk_eq_mk_iff, Localization.r_iff_exists]
  simp only [Submonoid.coe_one, one_mul]
  constructor
  · rintro ⟨c, hc⟩
    exact ⟨c, by simpa [mul_comm] using hc⟩
  · rintro ⟨c, hc⟩
    exact ⟨⟨c, Submonoid.mem_top c⟩, by simpa [mul_comm] using hc⟩

-- LeanTest/HardProblems/KTheoryCollapse.lean
/-- Goal 3: for a cancellative cost monoid, the canonical map is injective. -/
theorem toGrothendieckGroup_injective_of_cancel
    (M : Type u) [CancelCommMonoid M] :
    Function.Injective (GrothendieckGroup.of : M → GrothendieckGroup M) := by
  exact GrothendieckGroup.of_injective

-- LeanTest/HardProblems/KTheoryCollapse.lean
/-- Goal 4: the concrete regions `{true}` and `{false}` are distinct but have
the same image in the Grothendieck group. -/
theorem concrete_regions_collapse :
    ({true} : RegionMonoid Bool) ≠ {false} ∧
      GrothendieckGroup.of ({true} : RegionMonoid Bool) =
        GrothendieckGroup.of ({false} : RegionMonoid Bool) := by
  haveI : Subsingleton (GrothendieckGroup (RegionMonoid Bool)) :=
    grothendieckGroup_regionMonoid_subsingleton Bool
  refine ⟨?_, Subsingleton.elim _ _⟩
  simp [Set.eq_singleton_iff_unique_mem]

-- LeanTest/HardProblems/KTheoryCollapse.lean
/-- Goal 5a: adding any cost to the absorbing overflow value does not change
its canonical image. -/
theorem withTop_cost_top_add_image (a : WithTop ℕ) :
    GrothendieckAddGroup.of (⊤ + a) =
      GrothendieckAddGroup.of (⊤ : WithTop ℕ) := by
  simp

-- LeanTest/HardProblems/KTheoryCollapse.lean
/-- Goal 5: because `⊤` is absorbing, the entire Grothendieck group of
`WithTop ℕ` is trivial, not merely the part at or above the cap. -/
theorem saturating_costs_grothendieckAddGroup_subsingleton :
    Subsingleton (GrothendieckAddGroup (WithTop ℕ)) := by
  have hof : ∀ a : WithTop ℕ, GrothendieckAddGroup.of a = 0 := by
    intro a
    apply add_right_cancel (b := GrothendieckAddGroup.of (⊤ : WithTop ℕ))
    rw [← map_add]
    simp
  constructor
  intro x y
  suffices ∀ z : GrothendieckAddGroup (WithTop ℕ), z = 0 by rw [this x, this y]
  intro z
  induction z using AddLocalization.induction_on with
  | _ p =>
    have h : AddLocalization.mk p.1 p.2 +
        GrothendieckAddGroup.of (p.2 : WithTop ℕ) =
        GrothendieckAddGroup.of p.1 := by
      change AddLocalization.mk p.1 p.2 +
          AddLocalization.mk (p.2 : WithTop ℕ) 0 = AddLocalization.mk p.1 0
      rw [AddLocalization.mk_add, AddLocalization.mk_eq_mk_iff,
        AddLocalization.r_iff_exists]
      use 0
      simp [add_comm]
    rw [hof _, hof _] at h
    simpa using h

Boundary. These results concern one decategorification, group completion of the composition monoid. They do not bar every group-valued or scalar invariant, only those factoring through this completion. Nothing here computes higher K-groups, and nothing identifies the composition operation with the only interesting one; a different monoid structure on encounters could complete differently. The collapse justifies keeping the order; it does not prove the order is the unique alternative.

No twist at the order level

Hypotheses. A pseudofunctor from a locally discrete base category whose value categories are thin and skeletal, that is, posets. Separately, the one-object base on the two-element group, with fibre the one-object groupoid on the same group and comparison cells built from the cup-product cocycle.

Conclusion. Poset-valued pseudofunctors are strict on the nose: identities and composition are preserved as equalities of functors, and every comparison isomorphism is an equality-induced isomorphism. The split indexed order was therefore forced, not chosen. Over the non-thin fibre the cocycle data assemble into a genuine pseudofunctor whose coherence proof is the cocycle identity, its comparison cells are the cocycle comparisons by definitional equality, and no re-choice of coefficients has coboundary matching them, because the cup-product cocycle is not a coboundary, by a kernel-decided finite check. The strictness half is also instantiated at the book's own split indexed order: its fibres are proved thin and skeletal, and both of its comparison isomorphisms are equality-induced. (machine-checked)

Lean declarations and proofs (TwistObstruction.lean): HardProblems.Twist.map_id_eq_of_thin_skeletal, HardProblems.Twist.map_comp_eq_of_thin_skeletal, HardProblems.Twist.mapComp_eqToIso_of_thin_skeletal, HardProblems.Twist.twoCocycle, HardProblems.Twist.twoCocycle_isCocycle, HardProblems.Twist.twoCocycle_not_coboundary, HardProblems.Twist.twistElementIso, HardProblems.Twist.twistNatIso, HardProblems.Twist.twistIdHom, HardProblems.Twist.twistComparison, HardProblems.Twist.twistedPseudofunctor, HardProblems.Twist.twistedPseudofunctor_mapComp, HardProblems.Twist.twist_is_essential, HardProblems.Twist.mapId_eqToIso_of_thin_skeletal, HardProblems.Twist.toCatPseudofunctor_fibre_thin, HardProblems.Twist.toCatPseudofunctor_fibre_skeletal, HardProblems.Twist.splitIndexedOrder_mapComp_eqToIso, HardProblems.Twist.splitIndexedOrder_mapId_eqToIsorun

-- LeanTest/HardProblems/TwistObstruction.lean
/-- Goal A1. If every value category of a pseudofunctor from a locally
discrete base is thin and skeletal, then the pseudofunctor preserves
identities on the nose: the underlying functor of `F.map (id)` equals the
identity functor. State with whatever locally-discrete encoding of the base
1-category `C` mathlib's `Pseudofunctor` needs. -/
theorem map_id_eq_of_thin_skeletal
    (F : Pseudofunctor (LocallyDiscrete C) Cat.{w, w})
    (hthin : ∀ c : C, Quiver.IsThin (F.obj ⟨c⟩))
    (hskel : ∀ c : C, Skeletal (F.obj ⟨c⟩)) (c : C) :
    F.map (𝟙 ⟨c⟩) = 𝟙 (F.obj ⟨c⟩) := by
  letI := hthin c
  apply Cat.Hom.ext
  exact Functor.eq_of_iso (hskel c) (Cat.Hom.toNatIso (F.mapId ⟨c⟩))

-- LeanTest/HardProblems/TwistObstruction.lean
/-- Goal A2. Same hypotheses: composition is preserved on the nose. -/
theorem map_comp_eq_of_thin_skeletal
    (F : Pseudofunctor (LocallyDiscrete C) Cat.{w, w})
    (hthin : ∀ c : C, Quiver.IsThin (F.obj ⟨c⟩))
    (hskel : ∀ c : C, Skeletal (F.obj ⟨c⟩))
    {a b c : C} (f : a ⟶ b) (g : b ⟶ c) :
    F.map (⟨f⟩ ≫ ⟨g⟩ : (⟨a⟩ : LocallyDiscrete C) ⟶ ⟨c⟩) =
      F.map ⟨f⟩ ≫ F.map ⟨g⟩ := by
  letI := hthin c
  apply Cat.Hom.ext
  exact Functor.eq_of_iso (hskel c) (Cat.Hom.toNatIso (F.mapComp ⟨f⟩ ⟨g⟩))

-- LeanTest/HardProblems/TwistObstruction.lean
/-- Goal A3. The comparison isomorphisms themselves are the identity
2-cells modulo the equalities above: each `mapComp` component is an
`eqToIso`. State the cleanest correct version; if a different phrasing of
"the comparison data is trivial" is more natural in mathlib's API, prove
that and rename. -/
theorem mapComp_eqToIso_of_thin_skeletal
    (F : Pseudofunctor (LocallyDiscrete C) Cat.{w, w})
    (hthin : ∀ c : C, Quiver.IsThin (F.obj ⟨c⟩))
    (hskel : ∀ c : C, Skeletal (F.obj ⟨c⟩))
    {a b c : C} (f : a ⟶ b) (g : b ⟶ c) :
    F.mapComp ⟨f⟩ ⟨g⟩ =
      eqToIso (map_comp_eq_of_thin_skeletal F hthin hskel f g) := by
  ext X
  have thin := hthin c
  exact Subsingleton.elim _ _

-- LeanTest/HardProblems/TwistObstruction.lean
/-- The cup-product 2-cocycle on `ZMod 2`: `c h h' = h * h'`. Its class
generates the degree-2 cohomology of Z/2 with Z/2 coefficients, and is the
obstruction separating the two extensions of Z/2 by Z/2. -/
def twoCocycle (h h' : ZMod 2) : ZMod 2 := h * h'

-- LeanTest/HardProblems/TwistObstruction.lean
/-- Goal B1. The cocycle identity, with trivial action:
`c(h',h'') - c(h+h',h'') + c(h,h'+h'') - c(h,h') = 0`. -/
theorem twoCocycle_isCocycle (h h' h'' : ZMod 2) :
    twoCocycle h' h'' - twoCocycle (h + h') h''
      + twoCocycle h (h' + h'') - twoCocycle h h' = 0 := by
  simp only [twoCocycle]
  ring

-- LeanTest/HardProblems/TwistObstruction.lean
/-- Goal B2. Not a coboundary: no 1-cochain `φ` has
`c(h,h') = φ h' - φ (h+h') + φ h` everywhere. This is the precise sense in
which the comparison data below cannot be normalized away. -/
theorem twoCocycle_not_coboundary :
    ¬ ∃ φ : ZMod 2 → ZMod 2,
      ∀ h h', twoCocycle h h' = φ h' - φ (h + h') + φ h := by
  decide

-- LeanTest/HardProblems/TwistObstruction.lean
def twistElementIso (x : ZMod 2) :
    (SingleObj.star TwistGroup : TwistFibre) ≅ SingleObj.star TwistGroup :=
  Iso.mk (Multiplicative.ofAdd x) (Multiplicative.ofAdd (-x))
    (by change -x + x = 0; exact neg_add_cancel x)
    (by change x + -x = 0; exact add_neg_cancel x)

-- LeanTest/HardProblems/TwistObstruction.lean
def twistNatIso (x : ZMod 2) : 𝟭 TwistFibre ≅ 𝟭 TwistFibre :=
  NatIso.ofComponents (fun _ => twistElementIso x) (by
    intro X Y f
    cases X
    cases Y
    first
      | exact mul_comm f (Multiplicative.ofAdd x)
      | exact mul_comm (Multiplicative.ofAdd x) f)

-- LeanTest/HardProblems/TwistObstruction.lean
def twistIdHom : (Cat.of TwistFibre) ⟶ Cat.of TwistFibre :=
  (𝟭 TwistFibre).toCatHom

-- LeanTest/HardProblems/TwistObstruction.lean
/-- The comparison 2-isomorphism whose distinguished component is literally
`twoCocycle h h'`.  The right-unitor only reconciles the wrapper used by
`Cat` for the composite of two identity functors. -/
def twistComparison (h h' : ZMod 2) :
    twistIdHom ≅ twistIdHom ≫ twistIdHom :=
  Cat.Hom.isoMk
    (twistNatIso (twoCocycle h h') ≪≫ (Functor.rightUnitor (𝟭 TwistFibre)).symm)

-- LeanTest/HardProblems/TwistObstruction.lean
noncomputable def twistedPseudofunctor :
    Pseudofunctor (LocallyDiscrete TwistBase) Cat :=
  LocallyDiscrete.mkPseudofunctor
    (fun _ => Cat.of TwistFibre)
    (fun _ => twistIdHom)
    (fun _ => Cat.Hom.isoMk (Iso.refl _))
    (fun f g => by
      cases ‹TwistBase›
      cases ‹TwistBase›
      cases ‹TwistBase›
      change TwistGroup at f g
      exact twistComparison (Multiplicative.toAdd f) (Multiplicative.toAdd g))
    (by
      intros b₀ b₁ b₂ b₃ f g h
      cases b₀; cases b₁; cases b₂; cases b₃
      show _
      simp only [Cat.of]
      show _
      change Multiplicative (ZMod 2) at f g h
      have hc := twoCocycle_isCocycle
        (Multiplicative.toAdd f) (Multiplicative.toAdd g) (Multiplicative.toAdd h)
      fin_cases f <;> fin_cases g <;> fin_cases h <;> simp_all [twistComparison, twistNatIso,
        twistElementIso, NatIso.ofComponents, Functor.rightUnitor, Bicategory.associator] <;>
        ext <;> simp_all [twistIdHom, twoCocycle] <;> norm_cast
      all_goals rename_i X
      all_goals cases X
      all_goals change (_ : TwistGroup) = _
      all_goals rfl)
    (by
      intros b₀ b₁ f
      cases b₀; cases b₁
      change Multiplicative (ZMod 2) at f
      fin_cases f <;> simp_all [twistComparison, twistNatIso,
        twistElementIso, NatIso.ofComponents] <;>
        ext <;> simp_all [twistIdHom, twoCocycle] <;> norm_cast)
    (by
      intros b₀ b₁ f
      cases b₀; cases b₁
      change Multiplicative (ZMod 2) at f
      fin_cases f <;> simp_all [twistComparison, twistNatIso,
        twistElementIso, NatIso.ofComponents, Functor.rightUnitor] <;>
        ext <;> simp_all [twistIdHom, twoCocycle] <;> norm_cast)

-- LeanTest/HardProblems/TwistObstruction.lean
/-- The comparison of `twistedPseudofunctor` is the cocycle comparison by
construction. -/
theorem twistedPseudofunctor_mapComp (h h' : TwistGroup) :
    twistedPseudofunctor.mapComp
        (⟨h⟩ : (⟨SingleObj.star TwistGroup⟩ : LocallyDiscrete TwistBase) ⟶ ⟨SingleObj.star TwistGroup⟩)
        (⟨h'⟩ : (⟨SingleObj.star TwistGroup⟩ : LocallyDiscrete TwistBase) ⟶ ⟨SingleObj.star TwistGroup⟩) =
      twistComparison (Multiplicative.toAdd h) (Multiplicative.toAdd h') := by
  rfl

-- LeanTest/HardProblems/TwistObstruction.lean
/-- Goal B4. No re-choice of comparison components has coboundary equal to
(the negative of, equivalently in `ZMod 2`, equal to) the coefficients of the
actual comparison cells of `twistedPseudofunctor`. -/
theorem twist_is_essential :
    (∀ h h' : TwistGroup,
      twistedPseudofunctor.mapComp
          (⟨h⟩ : (⟨SingleObj.star TwistGroup⟩ : LocallyDiscrete TwistBase) ⟶
            ⟨SingleObj.star TwistGroup⟩)
          (⟨h'⟩ : (⟨SingleObj.star TwistGroup⟩ : LocallyDiscrete TwistBase) ⟶
            ⟨SingleObj.star TwistGroup⟩) =
        twistComparison (Multiplicative.toAdd h) (Multiplicative.toAdd h')) ∧
    ¬ ∃ φ : ZMod 2 → ZMod 2,
      ∀ h h', twoCocycle h h' = φ h' - φ (h + h') + φ h := by
  exact ⟨twistedPseudofunctor_mapComp, twoCocycle_not_coboundary⟩

-- LeanTest/HardProblems/TwistObstruction.lean
/-- The identity comparison is also equality-induced, completing the pair:
with thin skeletal values, both comparison isomorphisms of a pseudofunctor
are `eqToIso`, which is the full content of "strict on the nose". -/
theorem mapId_eqToIso_of_thin_skeletal
    (F : Pseudofunctor (LocallyDiscrete C) Cat.{w, w})
    (hthin : ∀ c : C, Quiver.IsThin (F.obj ⟨c⟩))
    (hskel : ∀ c : C, Skeletal (F.obj ⟨c⟩)) (c : C) :
    F.mapId ⟨c⟩ = eqToIso (map_id_eq_of_thin_skeletal F hthin hskel c) := by
  ext X
  have thin := hthin c
  exact Subsingleton.elim _ _

-- LeanTest/HardProblems/TwistObstruction.lean
/-- Fibres of the book's indexed order are thin: their homs are proofs. -/
theorem toCatPseudofunctor_fibre_thin (P : SplitIndexedOrder.{v, u, w} C)
    (c : Cᵒᵖ) : Quiver.IsThin ((toCatPseudofunctor P).obj ⟨c⟩) := by
  show Quiver.IsThin (P.Fiber c.unop)
  intro X Y
  exact ⟨fun f g => Subsingleton.elim f g⟩

-- LeanTest/HardProblems/TwistObstruction.lean
/-- Fibres of the book's indexed order are skeletal: an isomorphism gives
inequalities both ways, and antisymmetry finishes. -/
theorem toCatPseudofunctor_fibre_skeletal (P : SplitIndexedOrder.{v, u, w} C)
    (c : Cᵒᵖ) : Skeletal ((toCatPseudofunctor P).obj ⟨c⟩) := by
  show Skeletal (P.Fiber c.unop)
  rintro X Y ⟨i⟩
  exact le_antisymm (leOfHom i.hom) (leOfHom i.inv)

-- LeanTest/HardProblems/TwistObstruction.lean
/-- The splitting of the book's indexed order was forced: its composition
comparison is equality-induced. -/
theorem splitIndexedOrder_mapComp_eqToIso (P : SplitIndexedOrder.{v, u, w} C)
    {a b c : Cᵒᵖ} (f : a ⟶ b) (g : b ⟶ c) :
    (toCatPseudofunctor P).mapComp ⟨f⟩ ⟨g⟩ =
      eqToIso (map_comp_eq_of_thin_skeletal (toCatPseudofunctor P)
        (toCatPseudofunctor_fibre_thin P) (toCatPseudofunctor_fibre_skeletal P)
        f g) :=
  mapComp_eqToIso_of_thin_skeletal (toCatPseudofunctor P)
    (toCatPseudofunctor_fibre_thin P) (toCatPseudofunctor_fibre_skeletal P) f g

-- LeanTest/HardProblems/TwistObstruction.lean
/-- And its identity comparison likewise. -/
theorem splitIndexedOrder_mapId_eqToIso (P : SplitIndexedOrder.{v, u, w} C)
    (c : Cᵒᵖ) :
    (toCatPseudofunctor P).mapId ⟨c⟩ =
      eqToIso (map_id_eq_of_thin_skeletal (toCatPseudofunctor P)
        (toCatPseudofunctor_fibre_thin P) (toCatPseudofunctor_fibre_skeletal P)
        c) :=
  mapId_eqToIso_of_thin_skeletal (toCatPseudofunctor P)
    (toCatPseudofunctor_fibre_thin P) (toCatPseudofunctor_fibre_skeletal P) c

Boundary. By general strictification every pseudofunctor is equivalent to some strict 2-functor, so no inequivalence is claimed; the result is about this presentation. The re-choices are quantified as coefficient functions on the group, and their identification with automorphisms of the identity functor is by construction rather than by a proved group isomorphism. Nothing here defines a twisted K-theory of difficulty: with poset fibres there is no twist to act, with the collapsed coefficients of the previous card there is nothing to act on, and the analogy is closed at the obstruction, in both directions, rather than developed.

NotesNotes and sources

The information argument uses the data-processing inequality, the chain rule for mutual information, and Shannon's rate-distortion function. The Lean companion checks the deterministic refinement preorder, its robust-decision consequences, and the final scalar accumulation lemma. It does not yet formalize measure-theoretic mutual information, a stochastic data-processing inequality, or Shannon's coding theorem.

The scalar posterior formula is the conjugate update for repeated independent measurements of one fixed Gaussian state. Kalman's 1960 filtering paper treats dynamic linear estimation through covariance recursions. Nair and Evans give a different, control-specific use of information rate: a lower data rate for stochastic stabilization. Neither result licenses replacing all feedback limits by one channel-capacity number.

Hermann and Krener construct the nonlinear observation space from iterated Lie derivatives and prove the full-rank implication to local weak observability. Their constant-rank analysis also explains why hidden directions are local leaves rather than, in general, a linear subspace or a well-behaved global quotient. Sontag and Wang's output-to-state formulation makes zero input and zero output imply asymptotic state decay, while nonzero input or output magnitudes produce corresponding state bounds. Interpreting those signals as observer disturbances requires a declared error-system model. The book does not formalize these differential-geometric results in Lean.

The nonlinear observer discussion is a comparison-system argument related to input-to-state robustness. Rajamani studies observers for Lipschitz nonlinear systems. Andrieu and Praly establish conditions for nonlinear Kazantzis-Kravaris/Luenberger observers. Shim and Liberzon formulate observer robustness to measurement disturbances in an ISS-like sense. The book's scalar recurrence is narrower than those observer-design results.

The residual-set distinction among accommodation, detection, and isolation is standard in model-based fault diagnosis. The \(2\rho\) threshold follows from deterministic norm-ball geometry and is only a worst-case sufficient separation condition. Patton and Chen discuss robust observer-based fault detection and isolation in a broader setting.

The finite-state arguments belong to the Myhill-Nerode tradition: behaviorally distinguishable histories require distinct states. The abstraction conditions are elementary path versions of simulation and lifting ideas used in abstract interpretation and state abstraction. The formal theorems are intentionally smaller than those general theories.

Willems's behavioral approach treats a system as its admitted trajectories rather than privileging an input/output or state-space presentation. The book's Lean module checks only the set-theoretic core: intersection, projection, universal safety, discrete invariance, and binary function gluing. Schultz and Spivak construct a substantially richer temporal type theory in a topos of sheaves. That work motivates the local semantics here; it does not make the book's elementary formalization a topos model.

The closure-operator reading of boundaries has classical precedents that fix its vocabulary. Grothendieck introduced fibred categories and their cartesian lifts; the split indexed presentation and the total-category construction the companion checks descend from that work. Lawvere and Tierney showed that the subtoposes of a topos correspond exactly to certain closure operators on its subobject structure, the strongest historical instance of boundaries being classified by closure. Tripos theory, after Hyland, Johnstone, and Pitts, builds models of intuitionistic logic from indexed preorders with structure, which is a fibred order made to carry logic. Jacobs's monograph develops fibred preorders as the general semantics of logic over a base. The twist vocabulary follows Donovan and Karoubi and Atiyah and Segal, where K-groups defined locally over a base fail to glue and the failure is measured by a cohomology class; here both routes to such a twist are proved closed, at the order level by strictness and at the coefficient level by the collapse. None of these external results is formalized in the companion; they are cited as the tradition the constructions belong to.

Appendix. Glossary

These definitions are local to Why Problems Are Hard. Each entry names the formal role of a term and the over-reading it does not support.

Abstraction: A generally many-to-one map from a concrete domain to a smaller or simpler domain, chosen to preserve specified answers. Forward preservation alone does not make an abstract plan executable; the reverse direction needs lifting and goal reflection. A smaller abstract state space does not establish that the abstraction is computable, cheap to construct, or faithful to cost and safety.
Action boundary: The declared set of primitive transformations, constraints, and policy permissions through which states can change. Better inference inside a fixed action boundary does not create a missing transformation. Adding an actuator changes the boundary rather than merely accelerating an old action.
Attainable region: The set of resource and loss bounds achieved by at least one admitted program under a fixed task and model. Nondominated points, when they exist, record attained tradeoffs; unattained limiting tradeoffs belong to the lower boundary of its closure. A finite resource envelope can guarantee an internal optimum without providing an algorithm or a global optimum. Quotienting encounters by equality of their regions gives only the realized image inside the ambient powerset, not the whole fibre. A region does not define a scalar degree of difficulty without a scalarization.
Barrier depth: The infimum, over admissible paths, of the greatest drop below the path's starting objective value. If no admissible path exists, the barrier is set to \(+\infty\). Barrier depth is a bottleneck statistic, not a general cost, search-time lower bound, path length, or stochastic escape time.
Behavioral system: A declared time domain, signal space, and set of admissible trajectories. Equations, state variables, and input/output partitions are presentations of that behavior. Interconnection and hiding require declared interfaces, and an arbitrary family of local behaviors need not satisfy sheaf gluing. Universal safety may hold vacuously when the admitted behavior is empty.
Comparison class: The descriptions, machines, interfaces, or coordinate changes across which a claim is intended to remain stable. Relational objectivity comes from invariance over a declared class. Changing the class after seeing the result does not establish robustness.
Closure operator: An extensive, monotone, idempotent map on a poset of possibilities. Reachable-set formation, observational saturation, and hiding followed by pullback are proved instances; idempotence is why programmed moves and post-processed statistics add nothing. Not every operator in the book has this shape, hiding is not a lattice homomorphism, and a fibrewise closure need not commute with reindexing between contexts.
Contraction margin: For a comparison inequality \(e_{t+1}\le(q_0+\mu)e_t+d\), the positive gap \(1-q_0-\mu\). It supports a geometric error bound while positive. Losing this sufficient margin invalidates the certificate; it does not prove actual divergence.
Coordinate change: An invertible relabeling that transports every structure named in a claim. Exact conjugacy preserves runs, reachability, and observation behavior; transporting adjacency and objective also preserves barrier depth. Discovering or computing the change is not thereby free.
Data-processing inequality: The principle that applying a channel or statistic to available data cannot increase its mutual information with an unknown. It bounds reconstruction but does not say that a particular update rule preserves all information already available.
Detectability: Decay of state ambiguity that the admitted output history does not remove. Mere boundedness is not exact detectability; a fixed residual tube is practical detectability, while a disturbance-dependent tube is robust only when its bound vanishes with the disturbance. Detectability does not construct an observer or imply stabilizability.
Distortion: A declared loss \(d(x,\widehat x)\) for reconstructing \(x\) as \(\widehat x\), often averaged under a distribution. Accuracy claims depend on this choice. Small distortion under one loss does not imply that every task-relevant distinction is preserved.
Error tube: A certified set or radius that contains estimation error under stated disturbance and mismatch bounds. In the scalar recurrence the persistent radius is \(d/(1-q)\). A tube is an upper guarantee, not an exact error distribution or proof of optimal accuracy.
Experiment class: The passive and active procedures quantified over when comparing states or models. Observational equivalence is indexed by this class. Equivalence under feasible bounded experiments need not equal equivalence under every function-typed policy.
Extension: Addition of a sensor, actuator, predicate, state coordinate, oracle, or axiom absent from the old setup. It can change information, reachability, or expressibility. It is not an invertible coordinate change and does not prove that the old formulation contained the new capacity.
Fault tolerance: Accommodation retains an estimation, control, or safety guarantee inside a declared fault class. Detection separates faulty behavior from healthy uncertainty. Isolation separates one candidate fault from the others. None implies the other two, and a deterministic threshold does not supply a false-alarm probability without a probability model.
Feedback capacity: An upper bound on task-relevant information entering through one feedback round under a specified policy and channel model. It is not determined by a noise variance alone, and the scalar Lean budget lemma does not prove that a physical channel has that capacity.
Fibred order: Ambient powersets of context-specific performance spaces, reindexed contravariantly by preimage with identity and composition laws. Preimage reflects inclusion under a surjective point map; a bijection of performance points is sufficient but stronger. Realized attainable regions form only subposets and require preimage closure to reindex; compatible encounter transport is one sufficient witness. A many-to-one direct image is a separate covariant operation that may collapse distinctions. The total category and its cartesian lifts are constructed, and the projection is a fibration in the standard sense; the term still supplies no canonical topology, manifold, or global total ranking, and no comparison of unrelated fibres without a supplied context morphism.
Forward simulation: A map sending each concrete step to a valid abstract step, hence each concrete path to an abstract path. It supports sound abstraction of concrete behavior. It does not ensure that an abstract step or plan can be realized from a particular concrete representative.
Group completion: The universal way to turn a commutative monoid of difficulty classes into a group, mathlib's Grothendieck group. It identifies two classes whenever some common factor multiplies both into agreement, so the identifying factors are the non-cancellable ones. It is injective on cancellative scales and trivial for idempotent composition such as regions under union. Triviality here rules out invariants factoring through this completion; it does not rule out every numerical summary.
Information boundary: The observations, experiment class, prior state, and channel restrictions governing which distinctions can enter a representation. Computation on the resulting transcript cannot recover a distinction absent from this boundary.
Local step lifting: The condition that every abstract step offered from the image of the concrete state actually reached has a concrete successor in the required fibre. It lifts finite paths by induction. Surjectivity of the abstraction map alone is not a substitute.
Machine model: A formal specification of operations, input access, memory, randomness, and output timing. A complexity bound is relative to this model. A one-pass lower bound does not automatically survive rereadable input or auxiliary storage.
Model mismatch: Difference between the actual transition or observation law and the law used by an estimator. A scalar mismatch factor \(\mu\) is meaningful only after a system-specific norm and comparison inequality have been justified.
Observability codistribution: The span, at a state, of differentials of outputs and their admissible iterated Lie derivatives. Full rank is the Hermann-Krener sufficient condition for local weak observability. Frobenius supplies local hidden leaves only with the required smooth constant-rank and involutivity hypotheses.
Observational equivalence: Equality of all admitted finite observation laws from two states or models. It is relative to an experiment class. It does not imply physical identity, and exact state recovery may be unnecessary when the class shares an acceptable action.
Operative representation: A causal state carrying selected consequences of past interaction into later inference or action, such as a posterior, observer state, compressed transcript, or external memory. Size alone does not establish sufficiency or task relevance.
Rate-distortion function: The infimum mutual information required by a reconstruction channel to attain a declared expected distortion. It converts an accuracy target into an information requirement. It does not determine a per-round observation capacity or construct an estimator.
Reachability: Membership in the closure generated by finite admissible steps from a starting state. It depends on the action boundary and constraints. Reachability does not measure how hard a path is to find, how long it is, or whether it preserves a pathwise cost.
Robust action: One action acceptable for every state in an observation equivalence class. Such actions form the intersection of the statewise acceptable sets. Pairwise intersections do not guarantee that the total intersection is nonempty.
State capacity: The number of distinct internal configurations available to a finite machine, often converted to bits by a logarithm. A state count of \(2^s\) represents \(s\) bits, not \(2^s\) bits. Equal capacity does not establish compatible dynamics or exact tracking.
Task-relevant information: Information that reduces uncertainty under the loss or decision actually being studied. A transcript can contain many bits about irrelevant coordinates while omitting one decision-critical distinction.
Twist: Comparison data of an indexed structure that no re-choice of components can flatten, measured by a cocycle that is not a coboundary. At the order level no twist exists, because poset-valued pseudofunctors are strict on the nose; over fibres with genuine automorphisms a nontrivial twist exists and is checked. Neither fact yields a twisted K-theory of difficulty, whose coefficients would also have to survive the collapse of group completion.

ReferencesSelected references

Andrieu, V., and Praly, L. "On the Existence of a Kazantzis-Kravaris/Luenberger Observer." SIAM Journal on Control and Optimization 45(2), 2006. DOI.
Blackwell, D. "Equivalent Comparisons of Experiments." Annals of Mathematical Statistics 24(2), 1953.
Atiyah, M., and Segal, G. "Twisted K-theory." Ukrainian Mathematical Bulletin 1(3), 2004. arXiv.
Donovan, P., and Karoubi, M. "Graded Brauer Groups and K-theory with Local Coefficients." Publications Mathematiques de l'IHES 38, 1970.
Grothendieck, A. "Categories fibrees et descente." In SGA 1: Revetements etales et groupe fondamental, Expose VI. Springer Lecture Notes in Mathematics 224, 1971.
Hyland, J. M. E., Johnstone, P. T., and Pitts, A. M. "Tripos Theory." Mathematical Proceedings of the Cambridge Philosophical Society 88(2), 1980. DOI.
Jacobs, B. Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics 141, North-Holland, 1999.
Cousot, P., and Cousot, R. "Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints." POPL, 1977.
Hermann, R., and Krener, A. J. "Nonlinear Controllability and Observability." IEEE Transactions on Automatic Control 22(5), 1977. DOI.
Kalman, R. E. "A New Approach to Linear Filtering and Prediction Problems." Journal of Basic Engineering 82(1), 1960. DOI.
Li, L., Walsh, T. J., and Littman, M. L. "Towards a Unified Theory of State Abstraction for MDPs." ISAIM, 2006.
Mac Lane, S., and Moerdijk, I. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer, 1992.
Myhill, J. "Finite Automata and the Representation of Events." Wright Air Development Center Technical Report, 1957.
Nair, G. N., and Evans, R. J. "Stabilizability of Stochastic Linear Systems with Finite Feedback Data Rates." SIAM Journal on Control and Optimization 43(2), 2004. DOI.
Nerode, A. "Linear Automaton Transformations." Proceedings of the American Mathematical Society 9(4), 1958.
Patton, R. J., and Chen, J. "Observer-Based Fault Detection and Isolation: Robustness and Applications." Control Engineering Practice 5(5), 1997. DOI.
Rajamani, R. "Observers for Lipschitz Nonlinear Systems." IEEE Transactions on Automatic Control 43(3), 1998. DOI.
Shannon, C. E. "Coding Theorems for a Discrete Source with a Fidelity Criterion." IRE National Convention Record 4, 1959.
Shim, H., and Liberzon, D. "Nonlinear Observers Robust to Measurement Disturbances in an ISS Sense." IEEE Transactions on Automatic Control 61(1), 2016. DOI.
Sontag, E. D., and Wang, Y. "Output-to-State Stability and Detectability of Nonlinear Systems." Systems & Control Letters 29(5), 1997. DOI.
Schultz, P., and Spivak, D. I. Temporal Type Theory: A Topos-Theoretic Approach to Systems and Behavior. 2017. arXiv.
Weibel, C. A. The K-book: An Introduction to Algebraic K-theory. Graduate Studies in Mathematics 145, AMS, 2013.
Willems, J. C. "The Behavioral Approach to Systems and Control." Journal of the Society of Instrument and Control Engineers 34(8), 1995. DOI.

CompanionFormal companion

The Lean source is organized by mathematical subject. The representation and feedback modules distinguish deterministic information preorder, scalar recurrences, and residual geometry from the stochastic information theory, differential geometry, and observer-design premises supplied in prose. Older modules remain in the source tree for independent results, but the book no longer treats every formalizable fragment as part of its conceptual spine.

Proofs are checked on the repository's pinned Lean 4 toolchain with no sorry, admit, or native_decide. Difficult new claims are also submitted to Aristotle under its pinned Lean and mathlib version. Returned proofs are rebuilt locally, audited, and their statements compared with the companion; the repository proof may be an independent equivalent proof. Kernel verification establishes derivability from formal hypotheses. It does not establish that those hypotheses are empirically adequate or philosophically exhaustive.