How a derivation is checked
Four steps, in order, and each one is reported separately because they prove different amounts. This page is the honest account of what this tool knows and what it is guessing.
1 · Exact search
Forward chaining over the formula graph: repeatedly apply any relation whose inputs are all known, absorbing what it produces, until the target appears. If it appears, the derivation is exact and the remaining steps are not needed. The chain is then pruned back to the steps that actually contributed, so an unrelated formula that happened to be computable does not appear in your answer.
2 · A proposed bridge
Only when the search fails. A language model is given what you know, what you want, the formulas the graph already holds nearby, and the base dimensions this tool assigns to the symbols involved. It is asked for one relation, written so a machine can check it — and it is asked explicitly to return nothing rather than invent something.
3 · The dimensional check
Both sides are reduced to the seven SI base dimensions and compared. This catches the most common shape of a wrong relation: a term added to another of a different kind, a constant with the wrong units, an exponent off by one. It is a real disproof when it fails. It is not a proof when it passes — dimensions cannot see a coefficient, so E = mc² and E = 7mc² are identical to this step.
4 · The numeric cross-check
Random values are drawn for every free symbol and the relation is evaluated. Two separate things are reported. Evaluable: did it produce a finite number at all — which catches a proposal that divides by something that is always zero over its own domain. Agreement: where the known formulas can derive the same target from the same values by their own route, do the two answers match. Agreement is the step with real teeth, and it is exactly the step that catches a wrong coefficient.
Why a check can say "unknown"
A check that could not run reports unknown, and unknown is never treated as a pass. If you did not declare a dimension for a symbol, step 3 says so instead of quietly succeeding. If the known formulas cannot derive your target independently, step 4 says nothing was compared — which is the ordinary result for a genuine bridge, and precisely when it would be most tempting to report success.
Questions
- What does "verified" actually mean here?
- That the dimensional check passed AND the numeric cross-check compared the relation against the known formulas on real values and they agreed. It does not mean the relation is a law of nature; it means this tool tried to disprove it in two independent ways and could not.
- What does "refused" mean?
- That a check actively disproved it. A refused proposal is never shown as an answer, because a relation that contradicts the formulas we already have is not a useful starting point for anybody.