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.
Propagator call counts for the two-level MGRIT cycle
Statement
For the literal operations of A declared two-level MGRIT coarse-correction cycle, put and . One F-relaxation uses fine-propagator calls; one C-relaxation uses ; and one FCF-relaxation uses . The specified coarse forward substitution uses practical coarse-propagator applications, including the evaluation at . These counts concern completed operations without eliminating calls at zero inputs.
In an additive accounting model with nonnegative call costs , the modeled work is , where count all executed calls and accounts for all remaining work. Residuals, restriction, interpolation and stopping checks must contribute their actual calls and overhead; cached values incur no new call. A parallel schedule must respect the serial order within each F-interval and in the coarse solve, and its communication and synchronization. No measured speedup is asserted.
Facts & Assumptions
Given: The declared literal implementation, dividing , completed operations and the additive accounting convention of the Statement.
A declared two-level MGRIT coarse-correction cycle updates every F-index, using without a propagator; each other F-update and each C-update applies one fine propagator. FCF means F, then C, then F. The coarse solve computes for .
Proof
There are C-indices among unknowns, leaving F-indices. Exactly the boundary assignment in [F1] omits a fine call, giving calls. Each of the C-updates makes one call. Adding two F counts and one C count gives the stated FCF count, including , where the F count is zero.
The coarse loop in [F1] has iterations and executes one application per iteration, including . Summing the stipulated charge for every executed call and remaining operation gives the work formula. Each F-index uses the preceding index in its interval, and the coarse loop uses ; any execution schedule must preserve these dependencies and account for its other costs.
Depends on
Used by
Dependency tree · two levels
4 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.
Sources
- R. D. Falgout et al., Parallel Time Integration with Multigrid (standard reference, not scraped)