ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

One regularized Gauss–Newton step for exponential reaction kinetics

Example

For a first-order reaction with conversion fraction $F (c) = 1 - e^{- c}$ at unit time, use $X = Y = U = R$ , true rate $c^{†} = \log 2$ , exact datum $y = \frac{1}{2}$ , initial rate $c_{0} = 0$ , $α_{0} = \frac{1}{4}$ , $q = \frac{1}{2}$ , discrepancy factor $τ = 2$ , and budget $N = 1$ . For $0 < δ \leq \frac{1}{10}$ and $∣ ε ∣ \leq δ$ , the datum $y^{δ} = \frac{1}{2} + ε$ does not meet the initial discrepancy stopping condition. The single update gives $c_{1} = \frac{2}{5} + \frac{4}{5} ε$ ; the procedure returns this state with status discrepancy if its post-update residual is at most $2 δ$ , and otherwise with status budget-exhausted.

Facts & Assumptions

Given: $X = Y = U = R$ , $F (c) = 1 - e^{- c}$ , $c^{†} = \log 2$ , $c_{0} = 0$ , $ε \in R$ , $∣ ε ∣ \leq δ$ , $0 < δ \leq 1 / 10$ , $τ = 2$ , $α_{0} = 1 / 4$ , $q = 1 / 2$ , and $N = 1$ .

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): Countable Choice is assumed for the Hilbert adjoint in the assigned step.

[F1]

Unanchored Levenberg–Marquardt step with explicit early stopping: The scalar step is $c_{1} = c_{0} + (F^{'} (c_{0})^{2} + α_{0})^{- 1} F^{'} (c_{0}) (y^{δ} - F (c_{0}))$ .

[F2]

The exponential function is smooth and $(\exp)^{'} = \exp$ : $(e^{x})^{'} = e^{x}$ .

[F3]

The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ : $e^{c} > 0$ for real $c$ and $e^{- c} = 1 / e^{c}$ .

[F4]

The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ : The derivative of a composition is the product of the outer derivative and the inner derivative.

[F5]

Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ : A scalar multiple has derivative equal to that scalar times the original derivative.

[F6]

The natural logarithm as the inverse of the exponential function: $\log x$ is the inverse of the exponential for $x > 0$ , so $e^{\log 2} = 2$ .

Verification

Given: The model and parameter values above.

1.1givenF2F3F4F5F6algebra

By [F6], $e^{\log 2} = 2$ , and [F3] gives $e^{- \log 2} = 1 / 2$ ; hence $F (c^{†}) = 1 / 2$ and $F (c_{0}) = 0$ . The derivative of $c \mapsto - c$ is $- 1$ by its difference quotient. Therefore [F2], [F4], and [F5] give $(e^{- c})^{'} = - e^{- c}$ and $F^{'} (c) = e^{- c}$ , so $F^{'} (0) = 1$ .

2.1A1F1step 1.1givenalgebra

The initial residual satisfies $∣ y^{δ} - F (c_{0}) ∣ \geq 2 / 5$ , while $τ δ \leq 1 / 5$ , so the discrepancy test does not stop at $c_{0}$ . Substitution into [F1] gives $c_{1} = 0 + (1 + 1 / 4)^{- 1} (1 / 2 + ε) = \frac{2}{5} + \frac{4}{5} ε$ . Because $∣ ε ∣ \leq 1 / 10$ , $c_{1} \geq \frac{2}{5} - \frac{2}{25} = \frac{8}{25} > 0$ , so the returned rate lies in the physical rate domain $[0, \infty)$ .

3.1F1step 2.1given∎

Since the cap is $N = 1$ and $c_{1} \in U = R$ , the next check returns status discrepancy if its residual is at most $2 δ$ ; otherwise the cap branch returns budget-exhausted. In both cases the returned state is $c_{1}$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

38 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.