Problem 13 Goal — Exponential boundary elementary density
OpenRybinAI2026.P13.exponential_boundary_elementary_densityFor every with and , there exists a finite elementary-expression tree , possibly depending on and , whose evaluation is continuous at every positive real number and satisfies for every . The permitted expression trees are generated from the variable , rational constants, arbitrary real constants, addition, subtraction, multiplication, division, negation, exponential, real logarithm, real square root, sine, cosine, and the operation , where ; each operation is applied pointwise to the evaluations of its subexpressions. These are total real operations: in particular, division by zero has value , the real logarithm has value at zero and agrees with for negative , and the real square root is on nonpositive inputs. With , the same function must satisfy, for every real , the exact Abel identity . These are Mathlib’s oriented real interval integrals with respect to Lebesgue measure; for , the left side uses the interval . At the endpoint , the reciprocal and the quotient are interpreted using totalized real division, so both are where appropriate and the displayed integrand has value there; this endpoint has measure zero. No separate integrability hypothesis is stated, so the integrals use Mathlib’s total integral convention, under which a nonintegrable integrand is assigned integral . Finally, as the real upper endpoint tends to , the oriented interval integrals must converge to . The assertion does not require a single expression working uniformly for all , does not assert uniqueness of , and imposes no continuity or nonnegativity requirement at or at negative times; values for negative do not affect the stated limit.
import Definitions.Def_rybin2026_p13_exponential_boundary open Filter MeasureTheory Set open scoped Topology
namespace RybinAI2026.P13
/-- The exponential-boundary first-passage density has a formula in the fixed elementary
expression language, is continuous and nonnegative on positive times, has total mass one, and
satisfies the characterizing Abel integral equation. -/
theorem exponential_boundary_elementary_density
(b₀ c : ℝ) (hb₀ : 0 < b₀) (hc : 0 < c) :
∃ expression : ElementaryExpr,
ContinuousOn expression.eval (Ioi 0) ∧
(∀ t, 0 < t → 0 ≤ expression.eval t) ∧
SolvesAbelEquation b₀ c expression.eval ∧
Tendsto (fun T : ℝ => ∫ t in (0 : ℝ)..T, expression.eval t) atTop (nhds 1) := by
sorry
end RybinAI2026.P13Read-back
What the Lean code literally says, in plain math · gpt-5.6-sol
For every with and , there exists a finite elementary-expression tree , possibly depending on and , whose evaluation is continuous at every positive real number and satisfies for every . The permitted expression trees are generated from the variable , rational constants, arbitrary real constants, addition, subtraction, multiplication, division, negation, exponential, real logarithm, real square root, sine, cosine, and the operation , where ; each operation is applied pointwise to the evaluations of its subexpressions. These are total real operations: in particular, division by zero has value , the real logarithm has value at zero and agrees with for negative , and the real square root is on nonpositive inputs. With , the same function must satisfy, for every real , the exact Abel identity . These are Mathlib’s oriented real interval integrals with respect to Lebesgue measure; for , the left side uses the interval . At the endpoint , the reciprocal and the quotient are interpreted using totalized real division, so both are where appropriate and the displayed integrand has value there; this endpoint has measure zero. No separate integrability hypothesis is stated, so the integrals use Mathlib’s total integral convention, under which a nonintegrable integrand is assigned integral . Finally, as the real upper endpoint tends to , the oriented interval integrals must converge to . The assertion does not require a single expression working uniformly for all , does not assert uniqueness of , and imposes no continuity or nonnegativity requirement at or at negative times; values for negative do not affect the stated limit.
Confirmed by the mission captain (proposal self-audit).