Link to current text
MATH.12:3 - Forces
| Force | Tension |
|---|
| Existence and obtaining an answer | Existence may settle the mathematical question; a subsequent calculation can require the witness itself. |
| Concise proof and visible dependencies | An omitted intermediate value saves exposition but can prevent reconstruction of the operation. |
| General statement and available input | An argument for each input must retain the information on which its witness depends. |
| Mathematical correctness and execution | The proof’s logic and a program’s evaluation rules need a correspondence for the claimed computational use. |
| Equal outputs and affordable use | Two extracted expressions can return the same result while repeating different amounts of work. |
| Reusable proof and changed premises | A local assumption change can alter a branch, an output type or the computation that uses it. |