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.
Operational model, data, calibration and uncertainty vocabulary of the experiment interface
Formulation vocabulary inside the flat special-relativity framework: it names run descriptions, operational models, data records, calibration declarations and uncertainty bounds built from the framework's own objects (events, worldlines, clocks, observers, ideal waves, radar readings, observer energies and frequencies) and its SI conventions. It asserts no measurement, no apparatus behaviour, no realized experiment, no sampling law, no statistical inference and no value of any physical constant; in particular it does not claim that any laboratory realizes an operational model.
Definition
Adopt the SI conventions of SI units and coordinate conventions of the special-relativity framework, the ideal-clock and ideal-light assumptions of Adopted ideal-clock and ideal-vacuum-light interpretation, the ideal plane-wave and frequency-reading model of Adopted ideal plane-wave and frequency-reading model, the operational radar protocol of The operational radar protocol of an ideal observer, the massive-particle measurement identification of Adopted massive-particle momentum, observer measurement and isolated-collision conservation clause (ii) and the massless-particle measurement identification of Adopted momentum model for an ideal massless particle clause (ii). This definition introduces the framework's experimental-interface vocabulary; it selects no experiment, records no value and asserts no comparison.
(a) Run descriptions. A run description is a finite tuple whose entries are framework objects of the following kinds, each declared with its domain and regularity as specified by the cited item, together with the frame, observer, event or unit convention required for a numerical reading where such a reading is used: a point of the affine Minkowski space (an event, Oriented time-oriented affine Minkowski space (the spacetime primitives)); a vector of of declared causal character (Timelike, null, spacelike and causal vectors of a Lorentz vector space); a future timelike worldline together with its proper-time function (Curves, regular causal curves and future timelike worldlines in affine Minkowski space, Proper time along a future timelike worldline); a future unit timelike vector or a smooth observer congruence (Charts, tetrads, observer congruences and adapted charts in affine Minkowski space); a future null wave covector with its affine phase (Affine phase functions and wave covectors on affine Minkowski space); a radar time or radar distance assigned by the operational radar protocol (The operational radar protocol of an ideal observer); an observer angular frequency (Null wave covectors, frame frequency data and the observer frequency of an ideal plane wave); an observer energy, spatial momentum, kinetic energy or invariant mass (Observer energy, spatial momentum, invariant mass, rest energy and kinetic energy of a four-momentum); and a real parameter vector in a declared subset of with declared units. A run description is a description of a model configuration; the tuple asserts nothing about any apparatus or about nature.
(b) Operational model. An operational model is a tuple in which: is a nonempty set, the preparation index set; is a nonempty parameter set and is a surjection, the parameter map; assigns to each a run description of (a); and for some integer the map is a prediction map for , subject to the declared interpretation : for every , each component of is a number that the framework's definitions, postulates and proved consequences assign to the description , with every intermediate quantity, frame, event, sign and unit declared. An operational model is called an operational model for the quantity whose values computes. Condition is a declared interpretation that reviewers check when the model is used; it is not a consequence of the tuple structure, and no clause of this definition asserts that any apparatus realizes or that is measured.
(c) Data records. A data record is a tuple with an integer ; with ; with ; and a finite tuple of condition annotations, each a finite string identifying the declared run condition of the datum and, when the datum is taken from a report, the bibliographic identification of that report. The record declares: for each , the value of the quantity of (b) under the condition annotated by lies in the closed box , in the declared units. A data record contains no probability space, random variable, distribution, sampling law, independence assumption, likelihood or coverage statement; it declares nothing about how the values were produced and nothing about the correctness of any calibration.
(d) Calibration declarations. Let be a nonempty set of declared instrument-output values. A calibration declaration is a tuple with , and a condition annotation; it declares that for every obtained under the condition annotated by , the value of the declared quantity lies in the closed box in the declared units. A calibration record is a data record of (c) whose declared quantity is the value of the calibration map's output. The declaration asserts no accuracy beyond the bound and no statistical property of or .
(e) Uncertainty vocabulary. For a data record of (c), the declared uncertainty of the -th datum is the vector ; a source label is an element of the finite declared set attached to a bound; and a total declared bound for a value computed from finitely many recorded values by a declared finite arithmetic expression is any for which the declaration states: whenever each recorded value lies in its declared closed box, the computed value lies in for the declared number (for instance, for a sum of recorded scalars the sum of the recorded bounds is such a bound). Every uncertainty entry is a declared constraint of the form in (c) and (d); no probability law, coverage probability, confidence level, p-value or posterior is defined by this vocabulary.
(f) Comparison claims are separate. A claim that a data record and an operational model are consistent, or that supports, refutes or fails to distinguish , is not part of (a)-(e): it requires its own statement, an explicitly declared comparison rule and adequate primary-report and analysis prerequisites. For the current stored-lithium-ion optical Doppler report, that research prerequisite, labelled M20 in the source design, is supplied by exp-sr-stored-lithium-ion-doppler-time-dilation-2014 and pthm-sr-specified-model-comparison. The comparison theorem distinguishes hard-bound records of (c) from separately defined source-reported estimates and standard-uncertainty scales; the latter are not hard bounds or coverage guarantees. It permits comparison with specified alternative prediction hypotheses, which are not thereby operational models of the SR framework and are not asserted to satisfy condition in (b). Other primary-report families remain subject to their own retrieval and analysis obligations. These are nonlogical status pointers to the separate empirical record and comparison claim; no clause of this vocabulary licenses a conclusion about the truth of a postulate or of the framework.
(g) Well-definedness and scope. All components of (a)-(e) are finite tuples of sets, maps and real numbers with declared domains and units; the constructions use no choice principle and no measurability, integrability, completeness or differentiability beyond the cited items, and clause (b) evaluates a prediction only at parameter values for which the cited items supply its ingredients. The vocabulary asserts no measurement, no apparatus behaviour, no empirical support or refutation, no value of the constant or of any other physical parameter, and no statistical inference.
Depends on
Oriented time-oriented affine Minkowski space (the spacetime primitives)
Timelike, null, spacelike and causal vectors of a Lorentz vector space
Inertial frames and inertial charts of the affine Minkowski model
SI units and coordinate conventions of the special-relativity framework
Adopted ideal-clock and ideal-vacuum-light interpretation
Curves, regular causal curves and future timelike worldlines in affine Minkowski space
Proper time along a future timelike worldline
Charts, tetrads, observer congruences and adapted charts in affine Minkowski space
The operational radar protocol of an ideal observer
Affine phase functions and wave covectors on affine Minkowski space
Null wave covectors, frame frequency data and the observer frequency of an ideal plane wave
Adopted ideal plane-wave and frequency-reading model
Observer energy, spatial momentum, invariant mass, rest energy and kinetic energy of a four-momentum
Adopted massive-particle momentum, observer measurement and isolated-collision conservation
Adopted momentum model for an ideal massless particle
Dependency tree · 2 levels
Sources
- B. Crowell, Special Relativity, revision 2020-12-10 (author-published undergraduate textbook, 246 PDF pages; the author's lightandmatter.com page links this Archive upload); signature (+---) converted to (-+++) and c = 1 formulas restored to x^0 = c t; Sections 1.3 'Measurement' and 1.4 'The Lorentz transformation', pp. 23-31 (operational definition of time and the operationalism passage p. 26), Sections 3.2-3.3 pp. 55-59, Section 5.1 pp. 121-123
- S. M. Carroll, Lecture Notes on General Relativity, arXiv:gr-qc/9712019v1 (1997), Chapter 1 'Special Relativity and Flat Spacetime' printed pp. 1-5: the operational construction of an inertial coordinate system from freely moving rigid rods and a set of synchronized clocks, the definition of an event, the interval and the metric