Paper release: r1532 Released: July 11, 2026

Author af f iliations: ¹Pragma Research Inc.

Keywords: abstract rewriting, observation-determined normal forms, observational confluence, error bounds, metric subregularity, boundary reconstruction, refinement, local repair, Lean 4.

Mathematics Subject Classification (2020): Primary 68Q42; Secondary 49J53, 68Q25, 68Q85, 94B05.

Introduction

A confluent rewrite system has a familiar geometry: paths may split, but paths from the same source eventually rejoin. In many applications the source itself is hidden. What is fixed is an interface, input, conserved sector, sensor record, or boundary condition. The relevant question is then not \[ x\to^*y,\quad x\to^*z\quad\Longrightarrow\quad y\downarrow z, \] but rather \[ B(x)=B(x')\quad\Longrightarrow\quad \text{the settled observable outputs of }x\text{ and }x'\text{ agree}. \] The two statements have different proof obligations. Confluence is a property of paths. Observable reconstruction is a property of the consistent set and of the observation map on that set.

We use observation-determined normal form for a settled state determined through an observation map on the consistent set. This is distinct from the control-theory use of “observable normal form” for a state-space form obtained by coordinate transformation, including in Boolean control networks .

Let \(Q\) be a state space after quotienting representation changes that are regarded as silent, let \(C\subseteq Q\) be the consistent states, and let \[ B:Q\longrightarrow\mathcal B \] be protected observable data. For \(b\in\mathcal B\), set \[ C_b:=C\cap B^{-1}(b). \] The three possibilities \[ |C_b|=0,\qquad |C_b|=1,\qquad |C_b|>1 \] mean, respectively, that the observation is unrealizable, reconstructing, or ambiguous. Termination and confluence do not alter this trichotomy. They control how a computation reaches \(C\); they do not determine how many points of \(C\) share one observation.

The distinction becomes more consequential under perturbation. Exact injectivity of \(B|_C\) says nothing about conditioning. A sequence of finite systems may have injective observation maps at every stage and nevertheless become arbitrarily unstable under refinement. To capture the missing information, we use two moduli:

1. an error-bound modulus carrying a constraint residual to distance from \(C\);

2. an inverse-observation modulus carrying observation discrepancy within \(C\) to state discrepancy.

The first is an error-bound or metric-subregularity object in the sense of variational analysis . The second is the modulus of continuity of the inverse of \(B|_C\). We do not claim either notion as new. The object studied here is their use as an observation-determined normal-form certificate for constraint and rewrite systems and, especially, the uniform and multi-stage refinement calculus that results.

Main contributions

The manuscript has six technical contributions.

1. Correct exact interface. We state a canonical partial normalizer and a boundary-indexed unique-normal-form theorem with the empty-fiber case separated from weak normalization. An audited-terminal theorem further separates computational quiescence from semantic consistency. Identification modulo a silent equivalence is characterized exactly by cross-source endpoint agreement. The exact confluence implications are explicitly treated as classical.

2. Sharp observational stability. For a residual \(\Phi\) and an observation map \(B\), we define intrinsic moduli \(\eta_\Phi\) and \(\omega_B\). For arbitrary residual levels \(\delta_x,\delta_y\), \[ \begin{equation} \label{eq:intro-master} \begin{split} d_Q(x,y)\le{}&\eta_\Phi(\delta_x)+\eta_\Phi(\delta_y)\\ &+\omega_B\!\left( d_{\mathcal B}(Bx,By)+L_B[\eta_\Phi(\delta_x)+\eta_\Phi(\delta_y)] \right). \end{split} \end{equation} \] At zero residual the bound is exact by definition. Across all finite metric systems, the coefficient \(2\) in the equal-residual specialization cannot be lowered.

3. Uniform refinement towers. One-step approximate naturality follows from consistency and observation defects. We distinguish same-level receipt-conditioned agreement from genuinely cross-level comparison. An anchor-optimized theorem compares independently computed outputs at arbitrary refinement levels after restriction to a common level. Compatible nested inputs leave only the intervening defect segment, and summable pathwise defects yield an implementation-independent projective limit. A counterexample shows that stagewise injectivity is not enough without a uniform inverse modulus.

4. Repair and selection obstructions. A total exact local repair preserving an exterior collar exists if and only if the local consistency relation projects surjectively onto that collar. On a finite full-support probability space, observation-fiber resampling is the weighted orthogonal conditional-expectation projector and has a finite matrix recognition receipt. A stabilizer obstruction prevents an equivariant selector on ambiguous fibers. These results are elementary, but their integration prevents a normalizer from silently becoming a sector-selection axiom.

5. Constructive and linear classes. Ranked functional-audit systems have singleton-or-empty fibers, terminate under every effective asynchronous schedule with an explicit update bound, and settle synchronously in dependency depth; acyclic Boolean circuits compile directly into this class. Linear quotient systems admit rank tests and singular-value bounds that instantiate [eq:intro-master]; finite linear dynamics yield the usual observability matrix as a special case.

6. Receipts, complexity, and formal audit. A standard finite Markov drift lemma turns a row-wise kernel inequality into endpoint, stationary, and expected-occupation receipts, without asserting infinite-horizon confinement under persistent noise. For succinct Boolean systems, we record tight coNP- and \(\Pi_2^P\)-completeness classifications in this formulation; these supporting results are not part of the principal novelty claim. We audit the accompanying Lean sources theorem by theorem and state exactly which results remain to be formalized.

Novelty boundary and intended venue

The exact theory overlaps several established areas. Abstract rewriting supplies Newman’s lemma, Church–Rosser properties, unique normal forms, and normalization theory . Rewriting modulo equivalence and confluence under invariants already address quotient and relevant-state restrictions . Quantitative rewriting enriches rewrite relations themselves and proves metric analogues of classical confluence theorems . Error bounds and inverse stability are mature subjects in variational analysis . Functoriality of rewriting is also established in categorical graph transformation .

Accordingly, the paper makes no claim that a triangle inequality, an error bound, inverse continuity, a section criterion, or boundary-indexed unique normal forms are individually new. The contribution advanced for review is the integrated certificate architecture, particularly the explicit anchor-optimized cross-level receipt comparison and its cofinal-limit consequence, rather than the triangle inequality or Lipschitz telescope in isolation. Approximate inverse-system theory is important neighboring prior art, and the displayed estimate itself is elementary; we therefore claim an organizing synthesis, not priority for approximate commutativity or inverse limits. External specialist review remains necessary. The intended contribution is in mathematical theoretical computer science, with rewriting and semantics as the primary audience.

Relation to existing theories

Rewriting, invariants, and quotients

The classical properties of an abstract reduction system are standard . Confluence restricted to an invariant or taken modulo an equivalence has been developed in Constraint Handling Rules and graph transformation . Those frameworks are close to the first arrow in \[ \text{presentations}\longrightarrow Q\longrightarrow\mathcal B: \] they identify states that should count as the same or restrict attention to relevant states. Our observation map is the second arrow. It may be strictly coarser than equality in \(Q\), and it is required to be injective only on the consistent subset when exact reconstruction is desired.

Unique-normal-form properties weaker than confluence are well known and have been automated for term rewriting . The fiber trichotomy and partial-normalizer universal property here are elementary set theory; only the reachable-normal-form and fiberwise-confluence corollaries specialize classical rewriting theory.

Quantitative rewriting versus output stability

Gavazzo and Di Florio enrich rewriting relations over quantales and derive quantitative Newman, Church–Rosser, and critical-pair theorems . Here the rewrite relation remains ordinary. Distances are attached to two semantic interfaces: residual-to-solution error and inversion of observable data on the solution set. Thus the theory does not estimate a quantitative rewrite path; it estimates disagreement between settled outputs of possibly unrelated schedules or initial interiors.

Error bounds and inverse mappings

The inequality \[ \operatorname{dist}(x,C)\le \eta(\Phi(x)) \] is an error-bound property. In variational analysis, local linear versions are equivalent to metric subregularity or calmness of suitable set-valued mappings . The inverse-observation modulus is a global finite or compact analogue of inverse Lipschitz/calmness information. Our use of these notions is intentionally transparent: the novelty claim concerns their operational consequences for schedules and refinement towers, not their analytic origin.

Approximate inverse systems

Approximate inverse systems and almost-commuting diagrams have a substantial topological literature, including stability and resolution theorems for compacta . Those works perturb or relax compatibility of bonding data in topological or cover terms. Our setting keeps the ambient inverse system exact and instead gives pointwise metric bounds for normalizer defects, solver receipts, and protected-observation mismatch. The connection limits the novelty claim: the contribution is an explicit certificate adapted to observation-determined normalizers, not the invention of approximate inverse systems.

Static reconstruction and functional observability

Control-theoretic observability reconstructs a state, or a prescribed function of state, from an output history. Linear observability and functional observability supply rank and conditioning tests; recent nonlinear work characterizes when a nonlinear functional can be reconstructed from measurements and studies the quality of the inverse map . This is the closest neighboring language for the map \(B|_C\). Our setting is nevertheless static at the theorem interface: \(C\) is the already-settled consistent set, \(B\) may be any protected quotient observation, and the new questions are how residual error and inverse conditioning control schedule disagreement and how these certificates propagate through refinement towers.

Constraints, databases, and global sections

Acyclic database schemes and positive-semiring relations provide local-to-global consistency results . Constraint satisfaction studies local consistency as an algorithmic reduction . Database repair semantics distinguishes the existence of many consistent repairs from the answers invariant across them . Sheaf-theoretic contextuality similarly turns failure of a global section into an obstruction . Our empty-fiber certificate belongs to this broad lineage. The additional layer is the interaction with normal-form stability and refinement.

Asynchronous functional networks

Kahn process networks provide timing-independent determinacy for networks of functional components, while generalized Kahn principles treat broader abstract asynchronous, including nondeterministic, models under their stated hypotheses . Ranked functional systems below are a finite terminating special case with residual audits. Their purpose is not to reprove those principles, but to give a class in which the exact boundary hypotheses, update bound, and obstruction output are explicit.

Formalized rewriting

Formalized rewriting has established libraries such as CoLoR in Coq . Recent developments include a constructive Agda library for abstract rewriting , a Lean 4 framework for confluence and normalization of lambda calculi , and a Rocq library for adhesive-category graph rewriting . The accompanying standalone Lean artifact formalizes selected exact, stability, refinement, repair, ranked, and stochastic results from this paper; its coverage boundary is stated in 11.

Exact observable fibers

Let \(\to\) be a relation on \(Q\), write \(\to^*\) for its reflexive transitive closure, and let \(\operatorname{NF}(\to)\) be the normal forms.

The completeness hypothesis \(\operatorname{NF}(\to)=C\) is sometimes too strong: a computation may halt uniquely and then fail a separate semantic audit. The next theorem separates those two layers.

When \(T=C\), 12 reduces to the realizable part of 11. When \(T\supsetneq C\), it prevents an audit failure from being misreported as nontermination or as a consistent normal form.

Observational stability moduli

Let \((Q,d_Q)\) be a finite metric space, let \((\mathcal B,d_{\mathcal B})\) be any metric space, let \(\varnothing\ne C\subseteq Q\), and let \(\Phi:Q\to\mathbb R_{\ge0}\) satisfy \[ C=\Phi^{-1}(0). \] All maxima below therefore exist. The same formulas extend to compact spaces by replacing maxima with suprema and imposing the continuity hypotheses stated in 26; the displayed Lipschitz estimates continue to assume a finite Lipschitz constant for \(B\).

Let \(L_B\) be any Lipschitz constant for \(B\) on \(Q\).

The symmetric form used most often is \[ \begin{equation} \label{eq:symmetric-bound} d_Q(x,y)\le 2\eta_\Phi(\delta)+ \omega_B\!\left(\varepsilon+2L_B\eta_\Phi(\delta)\right). \end{equation} \]

Optimality and the exact observational modulus

Approximate schedule independence

A finite execution is a sequence \(x=x_0\to x_1\to\cdots\to x_n\). It is \((\delta,\beta)\)-settled if its endpoint \(z\) satisfies \[ \Phi(z)\le\delta, \qquad d_{\mathcal B}(Bz,Bx)\le\beta. \] No exact observation-preservation assumption is made.

The preceding result consumes a probabilistic settling receipt. The following standard drift calculation is one finite mechanism for producing such a receipt.

Compact and uniform families

Now let \(\{\mathfrak S_i\}_{i\in I}\) be a nonempty family of compact or finite metric systems with a common Lipschitz bound \(L\) for the maps \(B_i\). Define \[ H(t):=\sup_i\eta_i(t),\qquad \Omega(r):=\sup_i\omega_i(r). \] We assume these suprema are finite on the ranges under consideration; this uniform boundedness is not automatic when the diameters of the systems are unbounded.

A uniform settled-output modulus is a function \(\Psi(t,r)\) such that \(\Theta_{\Phi_i,B_i}(t,r)\le\Psi(t,r)\) for every \(i\in I\).

Parallel composition and observation design

Naturality and refinement towers

For an observable system define its reconstructing, realizable domain by \[ Q^{\mathrm{adm}} := \{q\in Q:\text{there exists a unique }c\in C \text{ with }B(c)=B(q)\}. \] Every normalizer in this section is understood to act on a chosen metric subspace of \(Q^{\mathrm{adm}}\), with the consistent set restricted to the corresponding normalizer image; every coarse map is assumed to preserve the chosen admissible subspaces. To avoid carrying restriction notation through every formula, we relabel those subspaces and restricted consistent sets as \(Q_s,Q_r,Q_n\) and \(C_s,C_r,C_n\). Thus \(B_n|_{C_n}\) is injective on the declared domain. Obstructed and ambiguous fibers remain governed by 3; they are not silently assigned a finite normalizer value in the metric estimates below.

Let \[ \mathfrak S_s=(Q_s,C_s,\mathcal B_s,B_s,\Phi_s), \qquad \mathfrak S_r=(Q_r,C_r,\mathcal B_r,B_r,\Phi_r) \] be finite or compact observable systems on the admissible domains declared above. Their normalizers \(N_s\) and \(N_r\) are therefore total on these domains. Let \(f:Q_s\to Q_r\) be a coarse state map and \(h:\mathcal B_s\to\mathcal B_r\) a coarse observation map.

Accumulation through arbitrary depth

Let \[ Q_0\xleftarrow{\rho_{1,0}}Q_1 \xleftarrow{\rho_{2,1}}Q_2\xleftarrow{}\cdots \] be an inverse sequence of nonempty finite or compact metric spaces with Lipschitz restriction maps, with \(\rho_{m,n}=\rho_{n+1,n}\circ\cdots\circ\rho_{m,m-1}\). Let \(N_n:Q_n\to Q_n\) be normalizers. The boundedness of each \(Q_n\) makes the following pathwise and uniform one-step normalization defects finite: \[ \alpha_n(q) := d_n(\rho_{n+1,n}N_{n+1}q,N_n\rho_{n+1,n}q), \qquad a_n:=\sup_{q\in Q_{n+1}}\alpha_n(q). \] For \(j\ge n\), write \[ K_{j,n}:=\operatorname{Lip}(\rho_{j,n}),\qquad K_{n,n}=1. \]

Combining 33 with 37 gives an explicit tower certificate in terms of residual, observation, and Lipschitz data at each stage.

For \(n\le h\le r\) and \(q_r\in Q_r\), define the amplified pathwise defect segment \[ \mathsf A_{r,h}^{(n)}(q_r) := \sum_{j=h}^{r-1} K_{j,n}\, \alpha_j\!\left(\rho_{r,j+1}q_r\right), \] with an empty sum equal to zero. By definition of \(a_j\), \[ \mathsf A_{r,h}^{(n)}(q_r) \le \sum_{j=h}^{r-1}K_{j,n}a_j. \]

The uniform hypotheses used earlier imply \(e_m^{(i)}\to0\) whenever \(\delta_m^{(i)},\beta_m^{(i)}\to0\), the observation maps have a common Lipschitz bound, and \(H(t),\Omega(t)\to0\) at zero. Uniform summability of \(\sum_j a_j\) implies the pathwise summability condition. Thus raw receipt parameters alone are not enough: uniform conditioning and the amplified restriction factors remain load-bearing.

Exact inverse limits

Assume now that all one-step defects vanish and that \(\rho_{n+1,n}(C_{n+1})\subseteq C_n\). Let \[ Q_\infty:=\varprojlim Q_n =\{(q_n):\rho_{n+1,n}q_{n+1}=q_n\}, \] and similarly let \(C_\infty=\varprojlim C_n\). Here \(Q_\infty\) is the inverse limit of the admissible domains fixed at the start of the section. It is the full ambient inverse limit only when every observation value is reconstructing and realizable.

Repairability and selection obstructions

The existence of a unique consistent state with a given observation does not imply that a prescribed local write support can construct it. This section separates extension, uniqueness, and repair support.

Let \(X_W\) be an interior write space, let \(X_D\) be a protected collar space, and let \[ R\subseteq X_W\times X_D \] be the locally consistent relation.

If \(R=\varnothing\) while \(X_W\times X_D\ne\varnothing\), nonexistence of a repair is immediate; when the domain is empty, the unique empty map is a vacuous repair. The next proposition assumes \(R\ne\varnothing\) because ordinary real-valued distance to the empty set is convention-dependent; an extended-distance formulation may instead assign that case margin \(+\infty\).

The definition prevents a one-site no-go from being misreported as a global inconsistency: increasing the transaction support may restore surjectivity.

Finite observation-conditioned resampling

There is nevertheless a canonical averaging operation once a reference measure is supplied; unlike a section, it does not select one state from an ambiguous fiber.

Symmetry and hidden tie-breaking

Let a group \(G\) act on \(C\) and \(\mathcal B\), and assume \(B|_C\) is equivariant.

Ranked functional-audit systems

We now give a broad constructive class in which the partial normalizer, asynchronous dynamics, and obstruction output are all explicit.

Write \[ Q=\prod_{v\in V}X_v, \qquad B:Q\longrightarrow\prod_{v\in V_0}X_v \] for the full state space and the boundary-coordinate projection. For a boundary value \(b\in\prod_{v\in V_0}X_v\), define \(E(b)\) recursively by rank.

Define recursively \[ M(v)=0\quad(v\in V_0), \qquad M(v)=1+\sum_{u\in P(v)}M(u)\quad(v\notin V_0). \]

Linear quotient systems and observability

Let \(V,W,Z\) be finite-dimensional real inner-product spaces. Let \[ A:V\to Z, \qquad C=\ker A, \qquad G\subseteq C \] be a gauge subspace. Let \(B:V\to W\) vanish on \(G\), so it descends to \(V/G\). Equip \(V/G\) with the quotient norm.

Let \[ H=C\cap G^\perp. \] Under the injectivity hypothesis, \(B|_H\) is injective. Let \[ \kappa_A:=\|A^\dagger\|, \qquad \kappa_B:=\|(B|_H)^\dagger\|, \] where \(\dagger\) denotes the Moore–Penrose pseudoinverse. Thus, when \(H\ne\{0\}\), \(\kappa_B\) is the reciprocal of the smallest singular value of \(B|_H\); on the zero space the pseudoinverse convention gives \(\kappa_B=0\). The constant \(\kappa_A\) is the global linear error-bound constant for \(C=\ker A\).

The finite-field version retains the rank criterion but not singular values. It is the quotient form of an information-set condition from coding theory .

Finite linear dynamics

Let \(T:U\to U\) be a linear update, let \(S:U\to Y\) be a sensor, and let \(G\subseteq U\) satisfy \(T(G)\subseteq G\) and \(S(G)=0\). Equip \(Y^{k+1}\) with its product inner product. The length-\(k\) observation map is \[ \mathcal O_kx=(Sx,STx,\ldots,ST^kx). \]

This is the classical observability matrix viewed through the quotient-boundary language; no novelty is claimed for the control-theoretic rank test .

Complexity of succinct boundary problems

The finite theory is elementary when \(Q\) and \(C\) are listed explicitly. It becomes computationally nontrivial when consistency is given by a Boolean circuit or formula.

Examples and separation results

Rule 90 as a regression test

No cellular automaton is used in the general theory. Rule 90 is retained because a three-cell instance simultaneously exhibits a hidden kernel, a proper information boundary, a deficient boundary, and a reverse-repair obstruction.

Over \(\mathbb F_2\), define \[ F(a,b,c)=(b,a+c,b). \] A one-step spacetime record is a pair \((s,t)\) satisfying \(t=F(s)\).

The accompanying standalone Lean artifact proves these exact width-three statements and includes theorem-level axiom-audit commands. Rule 90 is a regression test, not a rule selected by the theory or a load-bearing assumption.

Formal artifact and coverage

The accompanying ObservableNormalForms directory is a standalone Lean 4 project. It pins Lean and Mathlib at version 4.29.1, includes a pinned, checksummed Lake manifest, and builds both on its own and as a library of the parent formalization repository. Its theorem-bearing files contain no sorry or admit. The recorded #print axioms reports contain only standard Mathlib axioms—propext, Classical.choice, and Quot.sound where required—and no sorryAx.

The artifact’s proof index gives theorem-level names and labels; its build receipt records the parent and standalone commands, tool versions, and axiom audit. This is substantial coverage of the finite core, but it is not a complete mechanization of the manuscript. In particular, the intrinsic-modulus minimality and sharpness results, compact and uniform extensions, probability-event and occupation wrappers, the Hausdorff perturbation wrapper, dependent cofinal and inverse-limit constructions, equivariant sections, the circuit-specialization wrapper, asynchronous path-gain estimate, linear-algebraic certificates, and complexity classifications remain paper proofs. The status distinction is deliberate: only declarations listed in the proof index are claimed as machine checked.

Discussion

Why the factorization is useful

The estimate \[ \text{residual}\xrightarrow{\ \eta\ } \text{distance to consistency} \xrightarrow{\ \omega\ } \text{observable uniqueness} \] separates two burdens that are often mixed. A rewrite algorithm, numerical solver, or physical implementation controls \(\eta\) by showing that a small residual means closeness to \(C\). The observation architecture controls \(\omega\) by showing that \(B|_C\) is not merely injective but well conditioned. Critical-pair arguments may help establish exact completion or small residuals, but they are not required in the final output comparison.

Why finite uniqueness is not enough

In a refinement program, proving \(B_r|_{C_r}\) injective for every \(r\) does not prevent the inverse condition number from diverging. 28 is deliberately minimal. The correct limit-facing statement is uniform stable separation, not a list of stagewise singleton claims. This is the main stability requirement emphasized for refinement-sensitive applications.

Limitations

The theory assumes that a meaningful quotient, consistent set, residual, observation metric, and refinement map have already been declared. It does not select those objects. In particular:

• a normalizer is not a probability measure;

• an inverse-limit normalizer is not a continuum field theory;

• a finite update bound is not a wall-clock liveness theorem;

• a boundary pseudometric does not acquire additional semantics without a separate interpretation theorem;

• a small Rule-90 example does not establish cellular-automaton universality or generality.

These exclusions are necessary for both mathematical correctness and journal review.

Artifact and data availability

The repository artifact contains the PDF, LaTeX source, bibliography, and the standalone ObservableNormalForms Lean project. The formal directory includes a pinned toolchain and dependency manifest, theorem-to-source index, axiom audit, reproducible build receipt, archive manifest, and SHA-256 checksums. The mathematical proofs in this manuscript are self-contained; the Lean artifact checks the subset stated in 11. No empirical dataset is used.

Conclusion

Confluence is about paths from one state. Observable normalization is about what partial data determine after consistency is enforced. Their exact intersection is classical unique-normal-form theory: under observation preservation and \(\operatorname{NF}(\to)=C\), identification modulo any silent equivalence is equivalent to agreement of normal endpoints across all sources with the same observation. This does not by itself provide normalization or all-schedule settlement. Their robust intersection is governed by two analytic objects: an error bound to the consistent set and an inverse modulus for the observation map on that set.

The resulting estimate is universal and sharp in its two unavoidable components. More importantly, it survives refinement: one-step defects telescope, same-level solver agreement needs no tower term, and compatible cross-level computations differ by their receipt errors and the intervening normalizer-defect tail. For a compatible admissible input in complete spaces, nonexpansive restrictions, vanishing receipt errors, and summable pathwise tails give a common projective limit; exact compatibility recovers the inverse-limit normalizer. On finite probability spaces, fiber averaging supplies the canonical conditional-expectation projector, while its matrix receipt keeps that averaging distinct from representative selection or a spectral-gap claim. Empty fibers and ambiguous fibers remain visible rather than being hidden inside a repair operator. The theory therefore supplies a precise answer to three different questions: \[ \boxed{ \begin{array}{c} \text{Does a consistent extension exist?}\\ \text{Is it observably unique and stable?}\\ \text{Can the declared local support construct it?} \end{array}} \] No one of these questions answers the others. Keeping them separate is the central mathematical lesson and the reason the framework applies across rewrite, reconstruction, and distributed-inference models.

Statements and Declarations

Funding declaration: The authors declare that no external grants or dedicated third-party research funding were received for the preparation of this manuscript.

Author af f iliations declaration: Bernhard Mueller is af f iliated with Pragma Research Inc. No institutional af f iliations were declared for David Matscheko or Jonathan Hill in this submission. The corresponding-author email address is provided in the correspondence declaration.

Consent to Participate declaration: not applicable.

Consent to Publish declaration: not applicable.

Author Contribution declaration: Bernhard Mueller developed the observation-determined normal-form framework, the stability, refinement, repair, and complexity results, the manuscript text, and the accompanying Lean artifact. David Matscheko and Jonathan Hill contributed proof review, checking of the exact and stability results, and consistency review of the formal artifact and manuscript. All authors reviewed and approved the manuscript.

Correspondence declaration: Correspondence should be addressed to Bernhard Mueller, bernhard@floatingpragma.ai.

Data Availability declaration: No empirical dataset is used in this work. The LaTeX source, bibliography, and the standalone ObservableNormalForms Lean 4 project—with a pinned toolchain and dependency manifest, a theorem-to-source index, an axiom audit, a reproducible build receipt, and SHA-256 checksums—are available through the project repository.

Code Availability declaration: The standalone ObservableNormalForms Lean 4 project and its build sources are maintained in the project repository, together with a source bundle so that the manuscript and the formal artifact can be rebuilt without relying on private local paths.

Ethics declaration: not applicable.

Competing Interests declaration: The authors declare no competing financial or non-financial interests for this manuscript.

Use of AI-assisted tools declaration: AI-assisted tools were used for language editing, drafting assistance, formatting support, and submission-package preparation. The authors reviewed and remain responsible for all scientific content, claims, references, and declarations.