6. Multi-page source provenance
Source provenance may point at more than one page. The external markup witness is a compact Markdown extraction, while the source metadata records both PDF pages that reviewers should inspect.
Theorem6.1
Rendered from external Markdown source (statement): source/pages/page-15.md:20:0-39:0; no native Verso body is available.
Proposition 2.4
The imported Markdown extraction summarizes a result whose source spans two pages. The manifest keeps both source spans, while this witness records the textual extraction used for review.
Lean code for Theorem6.1●2 definitions
-
defdefined in Init/Prelude.leancomplete
def Nat.add : Nat → Nat → Nat
def Nat.add : Nat → Nat → Nat
Addition of natural numbers, typically used via the `+` operator. This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.
-
defdefined in Init/Prelude.leancomplete
def Nat.mul : Nat → Nat → Nat
def Nat.mul : Nat → Nat → Nat
Multiplication of natural numbers, usually accessed via the `*` operator. This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.