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.
The Picard operator and Picard iterates on a closed ball of continuous curves
Definition
Fix with , , , an initial state , and a radius . Let
Let be open and let be continuous. The domain of the Picard operator on consists of those whose whole graph lies in . For such a curve, continuity makes integrable on every interval with endpoints , and its Picard image is
The operator maps into ; it is a self-map of only when its image is known to remain in that ball. Starting from , define inductively whenever is defined and lies in the operator domain; if that condition first fails, no later iterate is defined. When a separate invariant-ball result makes a total self-map, The recursion theorem supplies the entire sequence. Every fixed point satisfies the corresponding Volterra equation. When , it is exactly a solution of the IVP by A first-order initial value problem is equivalent to its Volterra integral equation; for the fixed-point equation remains defined, but no derivative on the isolated one-point domain is asserted.