Cost Classical Results Complex Norm Exp Of Real

A theorem about complex exponentials

The complex exponential function is a standard tool in mathematics and physics, extending the familiar real exponential to complex numbers. For a real number r, the complex exponential exp(r) is simply the usual real exponential e^r. The theorem in question, complex_norm_exp_ofReal, states that the absolute value, or norm, of this complex number equals the real exponential itself: ‖exp(r)‖ = e^r. This is a foundational fact from complex analysis, and the declaration in the machine-checked library of formal theorems proves it directly from the definition of the complex norm and the properties of the real exponential.

The theorem is a classical mathematical result, not a new physical claim. It belongs to a module that formalizes well-established facts from real and complex analysis, such as the expansion of hyperbolic cosine and the norm of a complex exponential with a purely imaginary argument. These facts are used routinely in mathematical physics without re-proving them, and this declaration makes one of them available in a formally verified form. The proof is a short calculation: it rewrites the norm of the complex exponential using a known identity, then simplifies the real part, which is just r.

In Recognition Science, this theorem is a building block, not a statement about recognition or cost. The framework's own claims about forced cost functions and derived constants rest on a chain of theorems, and this result is part of the classical mathematical infrastructure that chain relies on. It does not, by itself, say anything about ledgers, ticks, or the golden ratio. It is a piece of standard mathematics, made explicit and machine-checked, that the framework can use without re-deriving it from scratch.

The theorem's scope is narrow and precise. It applies only to real inputs r, not to complex inputs. For a purely imaginary number, such as iθ, the norm of exp(iθ) is 1, a separate theorem in the same module. The declaration does not claim that the complex exponential is the only function with this property, nor does it say anything about the behavior of the exponential for complex arguments. It simply confirms a basic identity that any student of complex analysis knows, and it does so in a way that a computer can check.

theorem complex_norm_exp_ofReal (r : ℝ) : ‖Complex.exp r‖ = Real.exp r := by
  rw [Complex.norm_exp]
  simp [Complex.ofReal_re]

What this page does not claim

This theorem makes no physical claim about recognition or cost. It does not apply to complex inputs, only to real numbers. It does not say anything about the uniqueness or optimality of the exponential function.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cost/ClassicalResults.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: