Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablePipeline-generated
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

Physical scope

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 D=(d1,…,dr) 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 A (an event, Oriented time-oriented affine Minkowski space (the spacetime primitives)); a vector of V 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 Rm 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 M=(S,Θ,θ,D,F) in which: S is a nonempty set, the preparation index set; Θ⊆Rm is a nonempty parameter set and θ:S→Θ is a surjection, the parameter map; D assigns to each s∈S a run description D(s) of (a); and for some integer d≥1 the map F:Θ→Rd is a prediction map for D, subject to the declared interpretation (∗): for every s∈S, each component of F(θ(s)) is a number that the framework's definitions, postulates and proved consequences assign to the description D(s), with every intermediate quantity, frame, event, sign and unit declared. An operational model is called an operational model for the quantity whose values F 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 M or that F(θ(s)) is measured.

(c) Data records. A data record is a tuple R=(N,z,ε,a) with an integer N≥1; z=(z1,…,zN) with zk∈Rd; ε=(ε1,…,εN) with εk∈[0,∞)d; and a=(a1,…,aN) 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 k, the value of the quantity of (b) under the condition annotated by ak lies in the closed box ∏j=1d[zk,j−εk,j, zk,j+εk,j], 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 zk were produced and nothing about the correctness of any calibration.

(d) Calibration declarations. Let Z be a nonempty set of declared instrument-output values. A calibration declaration is a tuple C=(Z,c,δ,h) with c:Z→Rd, δ:Z→[0,∞)d and h a condition annotation; it declares that for every z∈Z obtained under the condition annotated by h, the value of the declared quantity lies in the closed box ∏j[cj(z)−δj(z), cj(z)+δj(z)] 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 c or δ.

(e) Uncertainty vocabulary. For a data record of (c), the declared uncertainty of the k-th datum is the vector εk; a source label is an element of the finite declared set {calibration, systematic, sampling-variability, rounding, other} 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 B∈[0,∞) for which the declaration states: whenever each recorded value lies in its declared closed box, the computed value lies in [y^−B,y^+B] for the declared number y^ (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 R and an operational model M are consistent, or that R supports, refutes or fails to distinguish M, 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 c or of any other physical parameter, and no statistical inference.

Depends on

Dependency tree · 2 levels

Sources