PhysicsLogic · Paper-first editionLean-extracted article 149

Formal reconstruction · driven magnetic transitions, gradient-field refocusing, calibrated detector minima, cross-molecule isotope assignment, nuclear moments, precision scope, and qualified theory comparison

The Molecular Beam Resonance Method for Measuring Nuclear Magnetic Moments

How a weak transverse drive becomes a calibrated nuclear-moment measurement—while deferred calculations, representation bridges, line-shape obligations, sign limitations, and unresolved interpretations remain visible

Original work encoded in Lean: I. I. Rabi, S. Millman, P. Kusch, and J. R. Zacharias Edition: human-readable logical reconstruction
Formal objectPhysicsLogic.Papers.Rabi1939
Physical resultA molecule carrying a nucleus with angular momentum and magnetic moment traverses a known homogeneous field and a weak perpendicular oscillating field. Supplied Larmor and transition calculations distinguish cumulative on-resonance reorientation from small off-resonance reorientation. Geometry-weighted opposite gradients refocus an unchanged magnetic projection. A positive populated set of detector-resolved transitions lowers the mean intensity under explicit preparation and detector-control conditions. Observed readings require separate accuracy bounds; locating a field-scan minimum remains observational. With alignment, baseline, frequency, and field calibration, minima and curves are recorded for Li-6, Li-7, and F-19. Constant frequency-to-field ratios, recurrence across molecular carriers, abundance evidence, known spins, and the retained p. 533 conversion law assign the resonances and establish represented moments whose Table II displays are 0.820, 3.250, and 2.622 nuclear magnetons. The Li-7 formula supplies a performed, represented estimate, without identifying it as the exact physical moment. Precision claims retain a symmetric-broadening assumption; detailed line shapes remain open, and the method determines neither moment sign nor angular momentum. The comparison with hyperfine inference leaves physical-effect and experimental-error alternatives unresolved and treats the apparently better alpha-particle model only as a qualified interpretation.
Argument architecture6 dependent routes · 36 semantic claims · 36 sourced steps · 5 deferred calculations · 2 retained value-level formula bundles · full magnetic-sublevel transition kernel · molecular energy-gap control · reported approximations and a separate tentative judgment · 2 open-obligation inputs · 2 interpretive inputs · 8-part complete conclusion · 3 philosophy-layer bridges · grounded and source-sensitive shared spectroscopy · 52 formal countermodels

Definitions, structures, and assumptions

Structures, classes, and inductive alternatives

  • structureThe phase rates are angular frequencies, after dividing energy by hbar. No evolution equation or physical identification is stored as a proof.
  • structureThe selected resonance-based quantity-extraction phenomenon. Its fields name the physical objects that occur in the result but carry no proof that the drive produced a transition, the readout located resonance, or the quantity was extracted.
  • inductive
  • structureThe selected spectroscopy data constrained by the complete transition, readout, and quantity-extraction route. This structure stores no route proof and no spectroscopy output.
  • structureContext-owned semantics from which the exact selected model is built.
  • inductive
  • inductive
  • inductive
  • inductive
  • inductive
  • inductive
  • inductive
  • inductive
  • inductive
  • structureSource-valued AMO audit data, outside the neutral spectroscopy contract.
  • inductive
  • inductive
  • structure
  • structure
  • structureScope of the selected spectroscopy explanation.
  • structure
  • structureProof-free selected data and relation families for the repeated route.
  • structure
  • structure
  • structureThe distinct outcomes of a normalized selected two-state experiment.
  • structure
  • structure
  • structure
  • inductive
  • inductive
  • inductive
  • structure
  • inductive
  • structure
  • structureA selected claim must depend on exactly these source-map steps.
  • structureA selected claim must retain exactly these epistemic statuses.
  • structureA selected route must name exactly these immediate predecessor routes.
  • structure
  • structure
  • inductive
  • structure
  • structure
  • structure
  • structure
  • structure
  • structureSeparate observed readings and deterministic error bounds. No statistical coverage or finite-run equality with a model mean is implicit in these data.
  • structure
  • structure
  • structure
  • inductive
  • structureThe source and outgoing joint-state distributions are kept separate from slit transmission and detector acceptance. No finite spectator cutoff or spectator-independent preparation is imposed.
  • structure
  • structure
  • structure
  • structure
  • structurePhysical Review 55 p. 533 and Table II on p. 534. Rabi first converts the observed resonance ratio `f/H` into a nuclear `g` factor using `4 pi/(e/Mc)`, then obtains the magnetic moment in nuclear magnetons by multiplying `g` by the known nuclear spin `i`. The exact calculated quantities are separated from the three-decimal table display, whose last printed digit does not specify a rounding tie-break convention.
  • inductive
  • inductive
  • inductive
  • inductiveThe paper-local source of Rabi's selected spectroscopy extraction.
  • inductive
  • inductive
  • structure
  • structureSelected real-valued content of Rabi et al.'s equations (1) and (2). It is paper-local because Ramsey's later separated-field calculation has a different transition formula.
  • structureProof-free relation families for one selected experimental problem.
  • structure
  • structureProof-free relation families for one uncertainty-assessment problem.
  • structure
  • structure
  • structure
  • structure
  • structure
  • structure
  • structure
  • structure

Definitions and domain choices

  • definition
  • definitionExact frame transport for a populated, normalized state history. Only the specified energy-basis probabilities are asserted unchanged.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionA physical initial vector at an arbitrary entrance time must first be expressed in the rotating frame at that same time.
  • definition
  • definition
  • definitionAn actual normalized preparation, unitary evolution, and selected Born outcome.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionEvolution after removing the common energy and laboratory drive phases.
  • definitionHamiltonian divided by hbar; `frequency*c` is detuning and `frequency*s/2` is the off-diagonal coupling.
  • definitionA two-state unitary when the two complex coefficients have total norm one.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe exact selected resonance-based extraction phenomenon.
  • definition
  • definition
  • definitionA source-sensitive explanation of resonance-based quantity extraction.
  • definitionThe exact pre-calculation setup shared by the two source adapters. Grounding a spectroscopy model requires the selected model, two distinct states, and an actually applied controlled drive, but no calculated frequency or readout.
  • definitionExact retention of all selected objects and all nine relation families.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe complete spectroscopy route with an actual normalized outcome pair.
  • definitionThe realized stopping point of the shared spectroscopy route, stated directly on one model. It retains the controlled transition, all calculated response facts, the resonance readout, and the extracted quantity without allowing implication-valued calculations to pass merely because setup is absent.
  • definitionThe quantity bridge may be a value extraction or operational access.
  • definitionThe apparatus-specific readout calculation is separate from dynamics.
  • definition
  • definition
  • definitionThe paper-local dynamics calculation remains an explicit input.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe proof-free resonance-based quantity extraction selected by the model.
  • definitionThe proof-free selected data constrained by this spectroscopy model.
  • definitionThe exact paper-local derivation selected for this spectroscopy route.
  • definitionThe exact system and regime in which the spectroscopy route is used.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionBoth selected outcomes are physically admissible and exhaust the sector.
  • definitionThe nontransition outcome must complement the selected transition.
  • definition
  • definition
  • definition
  • definitionImmediate predecessor routes. Claims established by their transitive predecessors are inherited by the dependency closure.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionTemporary reductio-introduction steps discharged by this inference. Discharge removes only those exact origins from the conclusion's epistemic basis; it does not assert the temporary hypotheses globally.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionA source-mapped claim holds when its declared formula evaluates under the given paper-local semantic interpretation.
  • definition
  • definition
  • definition
  • definition
  • definitionEvery claim in the supplied identifier list holds.
  • definitionA source-mapped step is semantically sound when the interpreted premises imply the interpreted conclusion. Physical principles and imported calculations therefore remain explicit hypotheses of paper-specific certificates rather than acquiring truth from their source-map labels. A reductio hypothesis is different: it introduces a temporary assumption into a subargument and therefore is not required to hold globally. Its later uses remain ordinary premise-sensitive steps, and discharging it into a negated conclusion remains an ordinary semantic obligation.
  • definitionEvery step in the supplied identifier list is semantically sound.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe formula declared for a claim identifier, when that claim is present.
  • definition
  • definitionEvery source-mapped step whose justification contributes to the claim through declared premise-to-conclusion steps.
  • definitionAll justification statuses contributed by the exact source-mapped origins of a claim. This records epistemic provenance; it does not assert any paper claim or discharge any physical assumption.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe declared argument step with the requested identifier, when present.
  • definition
  • definitionThe premise list and conclusion attached to a declared step identifier.
  • definition
  • definition
  • definition
  • definition
  • definitionThe complete Lean-side fidelity certificate. The first conjunct is computed from source-map data; the second is supplied by checked route semantics; the third requires each declared independence boundary to have a countermodel.
  • definition
  • definition
  • definition
  • definition
  • definitionA typed countermodel matrix avoids string-keyed audit rows. Each index selects one proposition-valued separation obligation.
  • definition
  • definitionEvery route actually declared in the source map has a semantic certificate under the paper-local interpretation.
  • definition
  • definition
  • definitionOne countermodel row retains a weaker proposition while rejecting a stronger upgrade. This is a proposition, not a structure carrying proof fields.
  • definition
  • definition
  • definitionIndependent dependency and epistemic ledgers must review the same actual source claims, including every public conclusion and the selected paper conclusion. Empty, duplicated, nonexistent, or one-sided entries are invalid.
  • definitionEvery actually declared source route must have exactly one independently reviewed predecessor row. Correct rows for a selected subset are insufficient.
  • definitionThe declared main conclusion must be exposed by at least one public route output, rather than existing only as an unexported source-map claim.
  • definition
  • definition
  • definitionTwo finite lists describe the same dependency set. Duplicate expected entries are rejected so a ledger cannot pass by repeating a label.
  • definitionEvery paper-level, claim-level, and step-level source reference is present and has a nonempty work and locator. PaperArgument.auditable separately checks that every claim and step carries at least one source.
  • definitionA source reference is usable for review only when both the work and its locator are nonempty.
  • definitionStatic fidelity checks that can be evaluated from a paper's source map alone. They do not assert the truth of any physical premise.
  • definitionEvery declared output of a named source route holds under the semantic interpretation. This is the proof obligation discharged by paper-specific Lean theorems.
  • definition
  • definitionA route is fully certified only when both its individual steps and its declared outputs are semantically checked.
  • definitionEvery source-mapped inference step in a named route is semantically sound.
  • definitionEvery route named in the supplied identifier list is semantically certified.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe source-mapped route with the requested identifier, when present.
  • definition
  • definitionThe public semantic interface inherited from predecessor routes. Descendants receive only declared route outputs, not every internal intermediate claim. Outputs still carrying a temporary reductio origin are excluded.
  • definitionAll direct and inherited route dependencies. The route-order check separately ensures that the declared graph is acyclic and topologically ordered.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe two unnumbered deflections printed on journal p. 528. The second one is subtracted because the gradients point in opposite directions.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionOpposite gradients do not require opposite directions of the magnetic field.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionPredicted mean flux, not a finite-run integer detection count.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe transition probability weights the mean detected flux of the same beam.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionA finite control near the reported 95 percent baseline, not a fitted experimental efficiency or a claim that the paper states an exact fraction.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionSpeed and magnetic projections before/after the selected transition. An arbitrary measure allows continuous beams as well as finite controls.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionParaxial constant-gradient motion with fixed longitudinal speed.
  • definitionLi-7/Li-6 table centers are used as diagnostic estimates, not as unrounded source outputs or assertions about the historical calibration.
  • definition
  • definition
  • definition
  • definitionA conditional diagnostic bound at the reported absolute-accuracy scale, not an assertion that the paper establishes a hard bound for the true error.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe raw apparatus conditions downstream of the driven transition. They do not contain an established dynamics or detector result.
  • definitionSource-calculation and apparatus inputs, not the desired detector loss. Uniform baseline transmission is a sufficient preparation condition; neither perfect experimental recovery nor a universal beam profile is asserted.
  • definition
  • definition
  • definitionThe same field history and interaction length set the auxiliary pulse at each populated speed. The full target matrix is computed in MultipletBeam.
  • definitionThe raw calibration and apparatus conditions downstream of gradient refocusing. They contain no established beam readout or observed minimum.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe selected real-valued readout retains Rabi et al.'s printed equations (1) and (2), rather than treating their Larmor and transition outputs as names.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe raw accepted-observation and formula conditions used after the Li-7 assignment. They contain no established nuclear-moment package.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe source's molecular interaction calculation supplies this spectral bound. Electronic first-order neutrality alone does not supply it.
  • definitionThe spectrum and dynamics share an independently interpreted physical moment parameter. This does not identify it with a calibrated estimate.
  • definition
  • definitionThe selected typed ratios, `g` factors, spins, and moments retain Rabi's printed p. 533 conversion law and p. 534 Table II readout.
  • definition
  • definitionThe independent confirming minima and frequency-field ratios used after the calibrated primary observations. No isotope assignment or moment output is stored here.
  • definition
  • definition
  • definition
  • definitionThe actual measured source formula admits an opposite-sign physical moment.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionReported accuracy scales on pp. 533-534, not certified hard error bounds, standard deviations, or confidence coverage for the actual moments.
  • definitionCalibration and repeatability estimates, with the source's explicit assumption about unmodeled asymmetric broadening.
  • definition
  • definition
  • definition
  • definitionThe detected phenomenon is some reorientation within the selected Li-7 multiplet, conditional on its physical interpretation. A minimum does not identify one initial/final pair or independently assign the nuclear isotope.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionFailure of exact point refocusing is distinct from exclusion by a finite detector aperture; the latter enters the measured rejected-transition weight.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionA lower calibrated mean requires some populated off-diagonal transition, not a uniquely identified pair. Finite readings and a field-scan minimum remain separate observational inputs.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe source higher-spin calculation now has actual magnetic sublevels, moment projections, and a selected entry of the reconstructed Majorana kernel. It does not identify this entry with the auxiliary spin-half probability.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe raw Rabi route retained by the source-sensitive explanation.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe source's tentative judgment about a line-center shift is an evidential attitude toward a bound, not its physical establishment.
  • definition
  • definition
  • definition
  • definition
  • definitionThe paper's precision discussion assesses absolute calibration and relative reproducibility separately while retaining the unresolved line-shape physics. The pair of uncertainties is data; none of the required assessment relations is stored as a proof field.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe physical force law is a separate input; an energy derivative by itself is not an identification of the force acting on the beam.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThis acts trivially on the nucleus and uses the separately selected spectator-resonant pulse, not the source's nuclear-resonant drive.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe target nuclear transition law must be the actual marginal for each populated spectator branch, not an average auxiliary probability.
  • definition
  • definition
  • definition
  • definitionExact conditions inside the selected secular, constant-gradient adiabatic model. A high-field moment-error bound alone supplies none of the force-law, zero-slope, or spectator-transport conditions.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionAn actual expectation over discrete spectral branches. The type of spectators need not be finite; each PMF has countable support.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionOriented gap in cycles per unit time, using h rather than hbar.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionUnits with hbar = 1, so h = 2*pi. The internal energy has an actual adjacent gap of four, rather than a named shift unrelated to the spectrum.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe same reading data used by the selected-channel diagnostic, now compared with the actual population-weighted multiplet means.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionA three-decimal table entry resolves a displayed value to within one unit in its last printed digit. This deliberately avoids assuming an unprinted round-to-nearest rule: for example, the displayed Li-7 values do not satisfy `2.167 * (3/2) = 3.250` as exact real numbers.
  • definitionJournal p. 533: `g = (4 pi/(e/Mc)) (f/H) = 1.3122 x 10^(-3) (f/H)`. The three selected ratios are the constant values inferred from the corresponding resonance minima, not individual rows of Table I.
  • definitionThe paper reports positive moment magnitudes; its oscillating-field method does not determine the sign.
  • definitionJournal p. 533: the nuclear moments are obtained directly by multiplying `g` by the known nuclear spin `i`.
  • definition
  • definitionJournal p. 534, Table II: Li-6, Li-7, and F-19 have spins `1`, `3/2`, and `1/2`; the displayed `g` factors are `0.820`, `2.167`, and `5.243`; and the displayed magnetic moments are `0.820`, `3.250`, and `2.622` nuclear magnetons.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe printed numerical form of `4 pi/(e/Mc)` in the paper's units: `1.3122 x 10^(-3)`.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionPositive fields/frequencies, an admissible probability, and a positive detuning factor do not by themselves supply either printed resonance formula.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionJournal p. 527, equation (1): `nu = mu H_0/(J h)`.
  • definitionJournal p. 529, equation (2), for a weak oscillating field and the selected spin-one-half transition. The rotating-field equation and Majorana higher-spin formula remain separate paper-local calculation hypotheses.
  • definitionPositive apparatus and frequency data do not themselves assert that a selected output is already a physically admissible probability.
  • definitionThe strengthened readout additionally records an admissible transition; equation (2) derives this stronger domain from the apparatus-only domain.
  • definitionAll quantities accessible to the pure oscillating-field experiment.
  • definitionA rotating component resonates only with its matching signed precession.
  • definition
  • definition
  • definition
  • definitionThe off-diagonal angular-frequency coupling of one rotating component.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe paper's `Delta = H_1/(2 H_0)` in equation (2).
  • definition
  • definitionThe paper's `q = f/nu` in equation (2).
  • definitionThe field-strength prefactor multiplying the squared sine in (2).
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionApply the ratio convention of Rabi 1937, p. 654, equation (14), to the same selected weak-field frequencies. This does not identify the exact 1937 precession in the total tilted field with the static-field Larmor value.
  • definition
  • definitionSpin-one-half laboratory Hamiltonian divided by hbar for the actual linearly oscillating transverse field, in the static-field basis.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe auxiliary transition and its remaining spin-half outcome.
  • definition
  • definitionThe auxiliary spin-half system has the target's gyromagnetic ratio, field history, and interaction time. The supplied scalar probability is the auxiliary probability; the target multiplet requires the Majorana map.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionOne considered alternative is excluded by a witnessed control result and an explicit paper-local exclusion relation.
  • definitionThe experiment is admissible, the declared calibration was performed and applies to the target record, and that record supplies the selected readout.
  • definitionA witnessed outcome of one paper-local control.
  • definitionA calibrated readout together with explicit selected control exclusions.
  • definitionEstablished detection retains the calibrated readout, selected control exclusions, interpretation, and final physical detection claim.
  • definitionA selected alternative family is nonempty and genuinely considered.
  • definitionEvery selected alternative has an explicit excluding control witness.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionA scoped assessment that explicitly retains at least one open source.
  • definitionThe result is established, an uncertainty is assigned, every selected source is assessed, and the result is stable under that scoped assessment.
  • definitionA selected source family is nonempty and every selected source is relevant.
  • definitionEvery source in the selected nonempty family has been assessed.
  • definitionA relevant source remains explicitly unquantified in this assessment.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionA concrete mathematical assignment whose state, quantity, and value all have the selected representation relations. This proposition deliberately stops before asserting that the physical quantity possesses the represented value.
  • definitionThe universal soundness law for assignments made through the selected quantity representation. Every application consumes the complete state and quantity representation setup. The law may still hold vacuously when no complete represented assignment exists; `FaithfullyRepresentsAt` separately requires a concrete witness.
  • definitionA selected mathematical quantity faithfully represents a physical quantity when it has a concrete value-bearing representation instance and every such assignment is physically sound in the stated system and regime.
  • definition
  • definitionThe selected mathematical and physical quantities have at least one complete state-and-value representation instance. Unlike an established represented value, this witness contains no physical-value conclusion.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionAn actual measurement is a performed procedure that is directed at the selected quantity of the selected system. Availability of some apparatus is not part of this definition; connecting performance to operational support is a separate bridge below.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionAn operationally established value combines the recorded measurement assignment with its physical-value conclusion. Faithfulness is one sufficient way to justify that conclusion; performance alone supplies neither it nor universal soundness of the interpretation.
  • definitionAn actual accessible procedure produced the mathematical state used in the represented value assignment. No physical-value conclusion occurs here.
  • definition
  • definition
  • definition
  • definition
  • definitionA model-to-world interpretation law. It does not assert that the model has produced a conclusion; use `GroundedModelConclusionAt` for that.
  • definitionA model-to-theory interpretation law. It does not assert that the model has produced a conclusion; use `GroundedModelConclusionAt` for that.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionBuild the epistemic dependency basis in paper order. A conclusion inherits the justification origin of its own step and every origin already attached to its premises.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionExpand a set of route identifiers by one dependency edge, iterated with enough fuel to traverse any acyclic graph on the declared routes.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition

Selected instances and coercions

  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance

Source mappings and interpretation choices

  • inductive
  • definition
  • instance
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • recursor
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • constructor
  • definition
  • checked statement
  • inductive
  • definition
  • instance
  • constructor
  • definition
  • checked statement
  • definition
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • recursor
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • constructor
  • definition
  • checked statement
  • inductive
  • definition
  • instance
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • recursor
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • checked statement
  • instance
  • checked statement
  • checked statement
  • instance
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • checked statement
  • checked statement
  • inductive
  • definition
  • instance
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • recursor
  • definition
  • constructor
  • definition
  • checked statement
  • definition
  • inductive
  • definition
  • instance
  • constructor
  • definition
  • checked statement
  • definition
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • recursor
  • definition
  • definition
  • structure
  • definition
  • instance
  • checked statement
  • checked statement
  • checked statement
  • definition
  • checked statement
  • checked statement
  • definition
  • checked statement
  • checked statement
  • checked statement
  • definition
  • definition
  • definition
  • definition
  • definition
  • checked statement
  • checked statement
  • constructor
  • definition
  • checked statement
  • checked statement
  • definition
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • definition
  • definition
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • recursor
  • definition
  • checked statement
  • checked statement**Alias** of `PhysicsLogic.Papers.Rabi1939.SemanticContext.all_routes_are_semantically_realizable`.
  • inductive
  • definition
  • instance
  • definition
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • checked statement
  • recursor
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • checked statement
  • definition
  • checked statement
  • checked statement
  • checked statement
  • definition
  • checked statement
  • checked statement
  • checked statement
  • definition
  • checked statement
  • definition
  • checked statement
  • checked statement
  • checked statement
  • instance
  • checked statement
  • checked statement
  • instance
  • checked statement
  • checked statement
  • instance
  • checked statement
  • checked statement
  • instance
  • checked statement
  • checked statement
  • instance
  • checked statement
  • checked statement
  • instance
  • definition
  • definition
  • instance
  • definition
  • definition
  • instance
  • definition
  • definition
  • instance
  • definition
  • definition
  • instance
  • definition
  • definition
  • checked statement
  • checked statement
  • definition
  • checked statement
  • checked statement
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • definition
  • checked statement
  • checked statement
  • definition
  • definition
  • definition
  • definition
  • checked statement
  • checked statement
  • checked statement
  • definition
  • definition
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement

Checked statements: parameters, hypotheses, and interpretation

  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementFrom the same Larmor relation and known spin, using a calibrated rather than actual field multiplies the inferred moment by H_actual/H_calibrated.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementThis rejects a deductive inference from width and symmetry alone, not the author's tentative judgment about which physical interactions are likely.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementPhysical Review 55 pp. 527-534 also exhibit the direct shared stopping point: the selected LiCl transition, detector-minimum resonance readout, and Li-7 moment extraction hold together on one spectroscopy model.
  • checked statementRabi's actual weak-field transition supplies the normalized outcome pair for the same nonvacuous LiCl spectroscopy and Li-7 extraction route.
  • checked statementPreserve the existing complete-result API through the narrower stage adapter.
  • checked statement
  • checked statementThe completed shared spectroscopy route reaches operational access only through Rabi's calibrated apparatus facts. The extracted `T.Moment` value is not identified with the accessed `T.Quantity`; the paper-local bridge relates the Li-7 moment value to the Li-7 moment quantity. Primary-source anchors: Physical Review 55 pp. 527-534, especially the calibrated resonance minima and magnetic-moment extraction.
  • checked statement
  • checked statement
  • checked statement
  • checked statementThis is a bound for moments inferred from individual adjacent energy gaps. A measured field-scan minimum still requires its independent line-shape and calibration hypotheses. The bound does not establish a free-spin pulse.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementThe certified source dynamics retains the normalized complex pulse behind the printed weak-field probability, without an exact-laboratory claim.
  • checked statement
  • checked statement
  • checked statementExact dynamics for the auxiliary spin-one-half corotating field do not upgrade the printed weak-oscillating-field calculation to exact dynamics.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementThis isolates the possession relation. An arbitrary alternative is not asserted to satisfy every separately supplied dynamics/calibration model.
  • checked statementThe uncertain moment-extraction route does not supply this exact assignment-soundness premise. It must be justified independently.
  • checked statement
  • checked statement
  • checked statement
  • checked statementThe paper's distinct magnetic states and applied weak perpendicular drive realize the exact shared setup before any Larmor-frequency, transition, detector, or moment calculation is used.
  • checked statement
  • checked statement
  • checked statement
  • checked statementOnly the independent shift is varied, not a complete molecular model. The supported judgment is retained while the actual bound fails.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementThe source's arbitrary-precision extrapolation requires both a uniform interaction bound and access to large enough fields within the valid regime.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementPositive moment magnitudes and the exact moment-equals-`g`-times-spin relations do not supply the printed frequency-field conversion or Table-II spin/display readout.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementPositive fields, positive frequencies, and even a strictly positive detuning denominator do not themselves constrain an assigned probability.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementPositive measured frequency cannot make the physical signed moment zero.
  • checked statementThe actual printed equation, not an assumed output range, establishes both probability bounds and therefore the strengthened physical domain.
  • checked statement
  • checked statement
  • checked statement
  • checked statementAn exact solution for the retained rotating component is not an exact solution of the linearly oscillating source field. The initial lower state has a nonzero omitted upper-state derivative, not merely a different matrix.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementPages 527-528: opposite moment signs give identical oscillating data.
  • checked statement
  • checked statement
  • checked statement
  • checked statementThe detuning envelope is a physically bounded response factor.
  • checked statementA nonzero weak oscillating field makes the printed denominator strictly positive even at exact resonance; its positivity need not be assumed.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementThe response envelope reaches its maximal value exactly when the drive frequency equals the Larmor frequency.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement

Constructors, projections, and other meaning dependencies

  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • constructor
  • recursor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor

External mathematical declarations

  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary

The semantics and provenance come from Rabi1939.lean, SourceMap.lean, Coverage.lean, and Fidelity.lean; the separately labeled constructed client is checked in CheckIndependentReuse.lean. The Larmor and weak-field pulse formulas, reconstructed Majorana kernel, and ratio-to-moment readout retain their actual mathematical content. Physical identification of the effective spin evolution, calibration, isotope assignment, uncertainty, and comparison remain explicit hypotheses. Original Majorana 1932 equation (4), Rabi 1937 equation (17), and Rabi 1939 equation (3) are distinguished rather than silently harmonized. Each coverage step reconstructs its conclusion from the exact premise map; route certificates are not mined for output witnesses.

01

Six routes carry a transition from magnetic dynamics to a qualified physical conclusion

The argument is a dependency chain, but it is not a chain of one epistemic kind. Driven dynamics, beam readout, calibrated observation, and moment inference each require a supplied calculation. The four function-shaped calculation contracts are independent hypotheses; each established physical output still consumes its selected setup together with the corresponding contract. Precision adds a controlled approximation and an open line-shape obligation. The final discussion combines direct comparison evidence with two interpretations and an unresolved choice. Only after those distinctions are retained does the source map compose the complete conclusion.

1 · Resonant transition dynamicsknown field · weak transverse drive · Larmor and transition calculations · sign-insensitive response
2 · Beam refocusing readoutordered regions · weighted gradient matching · finite aperture · mean signal loss
3 · Calibrated observationalignment · baseline · fixed-frequency field scan · three minima and curves · performed measurement
4 · Isotope assignment and moment extractionconstant f/H · cross-molecule recurrence · printed g law · known spins · estimated moments · value-bearing Li-7 formula
5 · Precision and method scopecontrolled broadening assumption · detailed line shape open · sign and angular momentum limits
6 · Qualified discussion and complete synthesisdirect–hyperfine discrepancy · two unselected alternatives · qualified model comparison · all seven results retained
Figure 1. The six source-mapped routes. The final route receives earlier claims through the certified dependency graph and reconstructs the complete result from its checked premise list, even though its direct dependency is the precision route.
Epistemic ledger
TransitionStatus in the source mapWhat remains explicit
Known-field setup to driven-transition outputdeferred calculation with retained formulaValue-level equations (1)-(2), plus rotating-field, representation, higher-spin, resonance, decomposition, and sign-insensitivity facts.
Projection-sensitive apparatus to lower mean signalexplicit model inputs and checked deductionPrepared beam measure, interpreted probabilities, integral domains, localized drive, populated aperture rejection, and detector control; observed readings have separate error bounds.
Aligned apparatus to recorded minimadeferred observational calculationScan, calibrations, stability, reproducibility, minima, and curves.
Cross-molecule observations to isotope momentsdeferred calculation with retained formulaRatios, recurrence, assignments, the printed f/H-to-g law, exact g-times-spin relation, finite-resolution Table II values, and estimated moment magnitudes.
Curve width to precision boundcontrolled approximationNo asymmetric shift from unmodeled broadening is assumed.
Recorded minimum to detailed profileopen obligationThe simple model is explicitly insufficient; interaction analysis is deferred.
Discrepancy to possible explanationsinterpretive inferencePhysical effect and experimental error are distinct proposals, neither selected.
Apparently improved nuclear modelinterpretive inferenceImprovement is not known to be nonaccidental.
02

A weak transverse drive turns a known-field magnetic system into a selective transition problem

The setup fixes two distinct magnetic states, a LiCl molecule carrying Li-7, the selected angular momentum, a homogeneous field in the resonance region, and a weaker oscillating field perpendicular to it. These are physical premises; the transition theory is supplied separately.

distinct magnetic states + LiCl carrying Li-7 + angular momentum and moment
+ known homogeneous field H + weak transverse oscillating field H1 → driven-transition setup. ResonanceDynamicsSetup; journal pp. 526–528 (1)

The deferred calculation returns ten logically separate outputs: a calculated Larmor relation; rotating-field and weak-oscillating-field transition calculations; a statement that the calculated probability represents the physical state transition; a higher-spin extension; cumulative reorientation on resonance; small net reorientation off resonance; decomposition of the oscillating field into counter-rotating components; insensitivity of a pure oscillating field to the sign of the moment; and the selected value-level equation bundle.

ν = μH0/(Jh),
Δ = H1/(2H0), q = f/ν,
p_aux = Δ2/((1-q)2 + Δ2) · sin2(πtf √((1-q)2 + Δ2)). journal p. 527 equation (1), journal p. 529 equation (2) · EquationsOneAndTwoResonanceFormulaAt (R1-R2)
setup + supplied Larmor/transition calculation
→ computed νL and controlled resonant response + P_selected is a physically interpreted entry of the higher-spin matrix + off-resonance response remains small + moment sign remains unresolved. ResonanceDynamicsCalculation · resonance_dynamics_calculation_retains_equations_one_and_two · larmor_and_transition_calculations_establish_resonance_dynamics (2)

The printed probability now has an actual complex two-state realization. printedPulseMatrix uses the normalized coefficients Delta/sqrt((1-q)2+Delta2) and (1-q)/sqrt((1-q)2+Delta2), with the literal printed phase. equation_two_realizes_actual_coherent_pulse proves that its unitary evolution has the selected Born probability. This is an effective realization, not an exact laboratory solution. oscillating_laboratory_generator_has_both_rotating_components retains the co-rotating and counter-rotating terms, and a weak resonant example with field ratio 1/100 and probability one still rejects equality with the co-rotating Hamiltonian.

physical_corotating_source_realizes_nonvacuous_frame_dynamics separately derives an exact laboratory solution for the retained rotating component. It differentiates the actual frame phases, keeps the resulting diagonal correction, and restores an arbitrary entrance vector at its specified entrance time. In the literal 1939 convention, the physical generalized frequency is 2 pi nu sqrt((1-f/nu)2+Delta2); the printed effective frequency has f in place of nu. physical_corotating_frequency_agrees_with_printed_frequency_only_at_resonance proves the distinction rather than silently replacing the printed formula.

exact_corotating_history_is_not_the_full_oscillating_history tests the actual equations of motion. Starting from the populated lower state, the omitted counterrotating term changes the upper-state derivative at entrance. Thus the normalized exact corotating trajectory does not solve the full oscillating-field equation, even for the weak resonant control. established_resonance_dynamics_retains_the_corotating_auxiliary_boundary exposes this result for the source's spin-one-half reference. These are exact statements within a constant-drive segment, not a rotating-wave error bound or an exact replacement of the experimental field.

The cited 1937 source uses the reciprocal frequency ratio nu/f. the_two_printed_frequency_ratio_conventions_agree_only_at_resonance keeps that convention distinct from the 1939 prose's f/nu. The formalization neither silently repairs the printed equation nor promotes the weak near-resonance approximation to an exact result. The certified dynamics route retains the concrete pulse through certified_resonance_route_retains_actual_coherent_pulse.

Auxiliary probability and actual higher-spin transitions

MagneticSublevels supplies actual finite sublevels and moment projections. The auxiliary spin-half system has the target gyromagnetic ratio, not its magnetic moment. The Li-7 interpretation identifies the source states with J=3/2 sublevels and connects its selected transition to an entry of the full matrix. These are physical interpretation hypotheses with explicit content; the matrix is not an assigned detector response.

N=2J; i,j in {0,...,N}; m_i=J-i; mu_i=(mu/J)m_i.
J_aux=1/2; mu_aux=mu/(2J); mu_aux/J_aux=mu/J.
A nonzero moment distinguishes every magnetic sublevel.
The selected Li-7 matrix has N=3, not two target states.
F_ij=(N-i)! i! (N-j)! j!; e_nu=2nu+i-j.
D_nu=nu! (nu+i-j)! (N-i-nu)! (j-nu)!.
Admissible terms satisfy j<=nu+i<=N and nu<=j.
P_ij=F_ij [sum_nu (-1)^nu c^(N-e_nu) s^e_nu / D_nu]^2.
c=sqrt(1-p_aux); s=sqrt(p_aux); 0<=p_aux<=1.
Every probability is nonnegative; rows sum to one for N=1,2,3.
The polynomial is continuous, including c=0; its tangent form requires c!=0.

The reconstruction follows the original Majorana four-factorial expression. Rabi 1939 equation (3) omits the factorial on (nu-m+m'); Rabi 1937 equation (17) instead changes the third factorial to (J-m-nu)!. Separate literal diagnostics retain these differences: the former is undefined on the extremal test, and the latter fails a spin-half transition comparison under a finite-support reading. This is not an author-approved erratum. General-spin row normalization remains an explicit external mathematical obligation; all entries and row sums for the three source nuclear spins are proved.

Calculation is not representation

larmor_relation_does_not_supply_transition_calculation keeps the Larmor relation distinct from a driven-transition calculation. calculated_probability_does_not_supply_transition_representation keeps a computed probability distinct from the claim that it represents the physical transition. named_resonance_outputs_do_not_supply_equations_one_and_two retains positive fields/frequencies, an admissible probability, and positive detuning while falsifying the two printed equalities.

03

Actual beam transport connects a projection change to detector loss

The readout uses one constant-gradient paraxial apparatus and one beam measure. The two deflecting gradients have opposite signs; the magnetic fields themselves need not point in opposite directions. The chosen ray passes through an ideal point collimating slit before entering the second magnet.

The free drifts and magnet maps compose actual transverse position and slope. Their derivatives satisfy the constant-curvature equations. Here l_0 is the source drift, l_A and l_B are magnet lengths, l_1 and l_2 border the slit, and l_3 is the final detector drift. Positive mass and longitudinal speed, ordered nonnegative drifts, and positive magnet lengths are explicit.

Drift_L(z,theta)=(z+L theta,theta).
Magnet_(L,k)(z,theta)=(z+L theta+k L^2/2,theta+k L).
k_A=mu_before g_A/(m v^2); k_B=-mu_after g_B/(m v^2).
The selected initial slope passes through the collimating slit.
S=l_0+l_A+l_1; T=l_2+l_B+l_3.
G_A=l_A(2l_0+l_A)T/S; G_B=l_B(l_B+2l_3).
z_D=mu_before g_A G_A/(2m v^2)-mu_after g_B G_B/(2m v^2).
If g_A G_A=g_B G_B, z_D=(mu_before-mu_after)g_A G_A/(2m v^2).
These G factors are a constant-gradient, point-source/slit reconstruction of the printed deflections.

composed_ray_transport_has_the_printed_detector_deflection derives the two deflections from that transport. matched_fields_refocus_exactly_the_unchanged_projection proves exact return to the reference point precisely when the two projections agree. This uses the weighted products g_A G_A and g_B G_B, not equality of the gradients alone. Finite source width, slit width, fringe fields, nonparaxial motion, and numerical accuracy of the idealization are not established by this reconstruction.

Total molecular force and the nuclear-only reduction

The projections in the deflection formulas are total molecular branch projections. The same spectator energy that cancels in a nuclear transition frequency can contribute to force. The new joint-state model uses the very same spectrum as the high-field precision argument, but requires separate force and transport controls. The derivative-force correspondence is an explicit adiabatic input inside the chosen constant-gradient paraxial approximation.

E_i,s(B)=-h gamma B m_i+E_s(B)+V_i,s(B).
mu_A(i,s)=h gamma m_i-E'_s(B_A)-V'_i,s(B_A).
mu_B(j,t)=h gamma m_j-E'_t(B_B)-V'_j,t(B_B).
Adiabatic force law: F_A=mu_A g_A; F_B=-mu_B g_B.
The force-derived ray uses mu_before=F_A/g_A and mu_after=-F_B/g_B.
Accurate nuclear energy gaps alone do not identify these total forces. AdiabaticForceAt · the_spectral_calculations_determine_both_actual_forces
At each v,i: w_s is a spectator PMF and K_(j,t|i,s) is a joint outgoing PMF.
The discrete spectator support need not be finite; 0<=eta_i,s<=1.
I_0^mol=integral sum_i rho_i sum_s w_s eta_i,s A_(i,s;i,s) dnu(v).
I_R^mol=integral sum_i rho_i sum_s w_s eta_i,s sum_(j,t) K_(j,t|i,s) A_(i,s;j,t) dnu(v).
Spectator-dependent preparation, joint transitions, and aperture acceptance are averaged separately.
Conditional expectations and the outer speed integrals have explicit integrability results. incoherent joint preparation · ConditionalExpectationsDefinedAt
Match g_A G_A=g_B G_B and the nuclear scale mu=J h gamma.
In the selected secular model V'_A=V'_B=0; baseline spectator slopes agree.
On populated outgoing support, E'_s(B_A)=E'_t(B_B).
For every populated spectator branch, sum_t K_(j,t|i,s)=P_ij.
Calculate eta_i=sum_s w_s eta_i,s from the actual prepared beam.
Then z_D^mol=z_D^nuc on controlled channels and I_0^mol=I_0, I_R^mol=I_R.
These are required readout inputs, not consequences of a high-field moment-error bound. EstablishedMolecularBeamReduction · JointReadoutCalculationAt

The reduction preserves a spectator's contribution to the entrance-slit selection. It cancels that contribution only in the matched detector endpoint under the stated conditions. The nuclear marginal must be calculated for each populated spectator branch: averaging an auxiliary probability before applying a higher-spin kernel is not justified. A physical-interpretation input identifies the selected molecular model, and the measured mean signals are calibrated to that model before the nuclear-only formulas are used.

C(v)=g_A G_A/(2m v^2)>0.
Delta=E'_s(B_A)+V'_i,s(B_A)-E'_t(B_B)-V'_j,t(B_B).
z_D^mol-z_D^nuc=-C(v) Delta; |Delta|<=d implies |z_D^mol-z_D^nuc|<=C(v)d.
If |z_D^nuc|+C(v)d<=w, the molecular ray is accepted.
If w+C(v)d<|z_D^nuc|, the molecular ray is rejected.
No unchanged-aperture conclusion follows inside the unresolved boundary band.
This is a force-slope budget, not a frequency-gap budget or a bound on fringe-field errors. a_force_error_budget_preserves_aperture_decisions_only_with_a_margin
Constructed J=1 target and spin-half spectator: nu_n=B, nu_s=2B.
Deleting spectator energy preserves the nuclear gaps but changes total force.
The separate spectator-resonant pulse U=I_3 tensor (-i sigma_x) is unitary and supplies the actual joint Born kernel.
It leaves the nucleus unchanged while S_0=1 and S_R=0; the bare nuclear model gives both means 1.
A conserved spectator has the same matched endpoint but initial slopes -1/2 and 0 for molecular and bare rays.
A source-direction window [-3/4,1/4] transmits one of two equally populated spectator branches: mean eta=1/2, not 1.
In a mismatched apparatus, zero mean spectator projection coexists with mean acceptance 0 and bare-ray acceptance 1.
The spectator-resonant drive is not the source's selected nuclear-resonant drive; these are constructed diagnostics.
Independent joint client: J=3/2, h=2, gamma=1/2, mu=3/2; mass=2 and v=2.
G_A=G_B=5; g_A=g_B=2; w=1/2; B_A=5000 and B_B=7000.
Three spectator weights are (1/2,1/3,1/6), with transmissions (1,1/2,0); mean eta=2/3.
An actual auxiliary pulse has p_aux=1/4; the populated extremal nuclear row is (27/64,27/64,9/64,1/64).
The aperture accepts only unchanged nuclear sublevels; I_0=2/3 and I_R=9/32.
Gain 6 and background 2 give S_0=6 and S_R=59/16 for the full joint molecular model.
Readings 6 and 59/16 with separate errors 1/10 resolve some populated nuclear reorientation.
Fresh data exercise the force and joint-state APIs without importing production countermodels.

The sixteen-theorem RabiForceClient constructs this spin-three-half beam with three spectator states and nonuniform slit transmission. It checks the auxiliary effective generator, all nuclear transition rows, actual spectral forces, conditional joint probabilities, and resolved readout. It does not provide a microscopic LiF Hamiltonian, a full laboratory propagator, arbitrary incoming quantum coherences, or a validated error budget for the apparatus approximation.

After this reduction, the nuclear-only detector formulas below use finite half-width w and the same finite speed measure nu on both branches. At each speed, rho_i are normalized nonnegative initial sublevel populations and eta_i are the calculated effective transmission factors. Every final sublevel has its computed probability P_ij and ray acceptance A_ij. The same field history and interaction length set the auxiliary pulse time L/v, and a physical interpretation identifies the entire target matrix. The integrals predict mean fluxes, not individual counts.

rho_i(v)>=0; sum_i rho_i(v)=1; 0<=eta_i(v)<=1.
A_ij(v)=1_{|z_D(v,i,j)|<=w}; P_ij(v)=Majorana_N(p_aux(L/v);i,j).
I_0=integral sum_i rho_i eta_i A_ii dnu(v).
I_R=integral sum_i rho_i eta_i sum_j P_ij A_ij dnu(v).
Matched fields give A_ii=1; normalized rows give sum_j P_ij=1.
I_0-I_R=integral sum_i rho_i eta_i sum_j P_ij(1-A_ij) dnu(v).

the_actual_signal_loss_sums_over_all_initial_and_final_sublevels derives the loss identity using the same populations and matrix as the forward readout. A changed projection can still hit the aperture. Strict loss requires positive measure of speeds having a populated, transmitted, positive-probability rejected channel; existence of a hypothetical channel is insufficient.

nu{v: exists i,j with rho_i>0, eta_i>0, P_ij>0, |z_D(v,i,j)|>w}>0 implies I_R<I_0.
S_0=g I_0+b_0; S_R=g I_R+b_R.
With g>0 and b_R=b_0, the same beam loss gives S_R<S_0.
A controlled drop excludes: for almost every v, rho_i P_ij=0 for every i!=j.
This indicates some populated reorientation, not one identified pair.
Locating a minimum in the field scan remains a separate observational step.

a_populated_resolved_multiplet_lowers_the_controlled_signal derives both mean inequalities. a_controlled_multiplet_signal_drop_requires_populated_reorientation supplies the qualified inverse inference. The original fixed-frequency scan avoids a frequency-dependent amplifier offset; this does not eliminate every possible background change.

I_0 and I_R are mean fluxes; S_0 and S_R are mean signals, not individual readings.
eps_0>=0; eps_R>=0; |Y_0-S_0|<=eps_0; |Y_R-S_R|<=eps_R.
eps_0+eps_R<S_0-S_R implies Y_R<Y_0.
eps_0+eps_R<Y_0-Y_R implies S_R<S_0.
Under the multiplet and detector controls, resolved observed loss requires some populated reorientation.
These are conditional deterministic bounds, not asserted statistical coverage.

SignalObservation separates readings from the molecule- and regime-indexed model means. MultipletBeam.Data.ObservationAccurateAt supplies the two absolute-error bounds for the full population model. The forward theorem needs a mean loss exceeding both errors; the inverse theorem needs resolved observed loss. Neither premise supplies an empirical error estimate or finite-shot sampling law. The same reading data remain usable by the older selected-channel diagnostic.

Normalized rho and eta_i(v)=eta_0>0 almost everywhere give I_0=eta_0 I_ref.
Normalized baseline speed averages equal the reference averages.
Equality of normalized velocity laws does not imply I_0=I_ref.
The 19/20 control is illustrative; the source reports about 95 percent, not an exact fraction.

Velocity-independent transmission is a sufficient preparation condition, not a consequence of matched ray geometry or a claim inferred from the approximate reported recovery. The ideal eta_0=1 case and a nonperfect experimental baseline remain distinct. The actual driven distribution can also be velocity-selected even when the baseline distribution is preserved.

The retained selected-channel controls below test limited binary response models. They are not the main higher-spin beam model.

Equal gradient magnitudes do not compensate unequal geometric factors.
With m=1, v=3, mu_before=1, mu_after=-1, g_A G_A=2, w=1/4: z_D=2/9, so the changed ray is accepted.
At populated v=3 with P=1/2, I_0=I_R=1: positive transition probability alone gives no loss.
A resolvable v=1 transition has no source weight in a beam supported only at v=3.
For speeds 1 and 3 with P=1/2, I_0=2 and I_R=3/2; mean detected speeds are 2 and 7/3.
Uniform eta=19/20 preserves the baseline velocity law while I_0=19/10 and I_ref=2.
With P=0, unchanged beam mean intensities, and drifting background, S_0=3 and S_R=2.
Equal zero transmission through the separate magnets need not imply g_A G_A=g_B G_B.
S_0=2, S_R=3/2; Y_0=Y_R=7/4 with errors 1/4: mean loss need not order readings.
With P=0 and controlled background, S_0=S_R=2; Y_0=21/10, Y_R=19/10 with errors 1/10: the observed drop is unresolved.
For J=3/2 and p_aux=1/2, the extremal row is (1/8,3/8,3/8,1/8).
The slow beam has unit baseline and loss 7/8, not p_aux=1/2 or full reversal 1/8.
The same field history gives p_aux=1/2 at speeds 1 and 5; the fast aperture accepts every final sublevel.
Different initial sublevels give the same detector loss but different selected-pair intensities.
Mean signals 1 and 1/8 admit equal readings 9/16 with errors 7/16.
A zero-pulse beam has both means 1 and no reorientation; readings 11/10 and 9/10 with errors 1/10 have an unresolved drop.

BeamReadoutCalculation supplies preparation, physical interpretation of the multiplet and velocity-resolved matrix, localized drive, integrability, uniform baseline transmission, responsive population, and calibration to the joint molecular mean signals. Its explicit molecular force setup and calculation are required by the source route. It does not supply the desired loss. Distinct nuclear projection values and the molecular reduction are derived before the detector inference. The shared spectroscopy adapter still describes a selected transition probability, but its detector condition indicates some multiplet reorientation, not equality of signal loss with that pair's probability.

Independent client: J=3/2, mu=3/2, mass=2; G_A=4, G_B=3; g_A=3, g_B=4; w=1/5.
Speed weights are 1 at v=1 and 2 at v=5; rho=(2/3,1/3,0,0); eta=3/4.
One length L=5/6 computes p_aux(v)=sin(5pi/(6v))^2, equal to 1/4 at both speeds.
The slow aperture accepts only i=j; the fast aperture accepts |j-i|<=1.
Driven densities are 57/256 and 163/256; I_ref=3, I_0=9/4, I_R=383/256; loss=193/256.
Gain 2 and background 5 give S_0=19/2 and S_R=1023/128.
Readings 47/5 and 81/10 with errors 1/8 resolve some populated reorientation.
This constructed client imports no production countermodel and is not historical data.

The independent RabiMultipletClient checks these values using public paper-local APIs. It supplements the retained twenty-theorem binary client rather than relabeling it as higher-spin dynamics. Neither is a new primary-paper benchmark or an additional external-consumer package.

04

Alignment, calibration, and a field scan turn the readout mechanism into observations

The observation route adds an operational measurement setup: the resonance procedure measures the Li-7 moment quantity in LiCl; the apparatus implements the procedure and is accessible to the selected agent; and the agent performs it. The apparatus is aligned, equal separate weakening of the two gradient fields is satisfied, and a refocused baseline is established.

procedure measures quantity + apparatus implements procedure + agent can access apparatus + agent performs procedure
→ operational accessibility + measurement performed. apparatus_and_performance_realize_operational_measurement (4)

The supplied observational calculation holds the radiofrequency fixed while scanning the homogeneous field, calibrates frequency and field, keeps the frequency stable through the Li-7 primary curve, and requires field reproducibility. It then records minima and curves for Li-6 and Li-7 in LiCl and F-19 in NaF.

established readout + operational setup + alignment + baseline
+ fixed-frequency field scan + frequency/field calibration → calibrated Li-6, Li-7, and F-19 minima and resonance curves. CalibrationAndObservationCalculation · aligned_apparatus_and_calibrations_establish_observed_resonances; journal pp. 530–533 (5)

li7_moment_operational_access_exposes_foundation_relation identifies the accessibility claim with the exact access context. Actual performance is supplied separately by the operational setup and the performance context. The paper carries no generic observer-independent existence relation.

05

Constant ratios and recurrence across molecules support isotope assignment and moment extraction

The inference setup supplements the three primary observations with confirming minima: Li-6 in Li2, Li-7 in LiF, and F-19 in LiF. It also supplies the frequency-to-field ratio attached to each primary observation.

The deferred inference calculation establishes that all three ratios remain constant under field variation. For Li-7, the constant ratio identifies nuclear reorientation and excludes a molecular transition. The same nuclear ratio recurs across the primary and confirming molecular carriers for all three nuclei. Abundance and intensity support the Li-7 assignment, while a definite assignment for each isotope requires two molecules. The calculation then assigns all observations, computes g factors from the ratios, uses known spins, computes the moments, and retains them as calibrated estimates.

g = (4π/(e/Mc))(f/H) = 1.3122×10-3(f/H),
μ = gi,
Table II: (g, i, μ)Li-6 = (0.820, 1, 0.820), (g, i, μ)Li-7 = (2.167, 3/2, 3.250), (g, i, μ)F-19 = (5.243, 1/2, 2.622). journal p. 533 and p. 534 Table II · NuclearMomentExtractionSourceFormulaAt · displayed decimals retained at three-decimal resolution, not asserted as false exact products (R3)

The source graph stores this retained formula as atom nuclearMomentFormula, claim momentFormula, and step retainNuclearMomentFormula. moment_route_exposes_ratio_g_factor_and_moment_formula checks that the step consumes the selected moment setup and calculation, while moment_route_recovers_ratio_g_factor_and_moment_source_formula reconstructs the formula from those checked premises. Within the value-level readout, li7_moment_uses_known_three_halves_spin recovers the exact Li-7 relation before the three-decimal display is applied.

constant f/H under variation + same ratio across molecular carriers + abundance/intensity evidence + two-carrier requirement
→ nuclear assignment → g factor + known spin → represented moment estimate,
Table II displays the magnitudes 0.820 (Li-6), 3.250 (Li-7), and 2.622 (F-19) nuclear magnetons, not exact physical values. values and dependency chain encoded by NuclearMomentInferenceCalculation and its source map · nuclear_moment_inference_calculation_retains_ratio_g_factor_and_moment_formula · cross_molecule_resonances_and_known_spins_establish_nuclear_moments (6)

The theorem established_nuclear_moments_retain_li7_assignment_and_calculated_estimate extracts two facts needed downstream: the Li-7 observation is assigned to the Li-7 nucleus, and the Li-7 moment estimate has been calculated from its g factor and known spin.

A calculated moment becomes a recorded estimate

The Li-7 representation route requires an accepted primary observation, an admissible moment formula, and a formula calculation assigning the selected moment. The observation, nuclear assignment, formula, and represented value form a concrete value-bearing instance; the performed detector record supplies the operational record link. This proves a represented estimate, not exact physical possession. The source does not supply a universal exact assignment-soundness law.

accepted Li-7 observation + nuclear assignment + admissible calculated formula + performed detector record
→ value-bearing assigned representation + recorded moment estimate. calculated_li7_moment_realizes_assigned_quantity_representation · calibrated_record_and_representation_record_li7_estimate (7)

complete_result_does_not_depend_on_exact_moment_possession proves that the complete source result is unchanged when the independent exact-moment relation changes. recorded_estimate_allows_a_distinct_physical_moment retains an actual recorded estimate and an inhabited different physical value while rejecting exact-value establishment. It does not assert that an arbitrary alternative satisfies every separately supplied dynamics or calibration model. The optional recorded_li7_estimate_and_faithfulness_establish_exact_value requires a separate soundness premise.

Absolute calibration versus relative precision

The actual and calibrated fields enter the same Larmor conversion differently: the inferred moment is the physical moment multiplied by Hactual/Hcalibrated. A common scale cancels in a ratio but not in either absolute value. FieldCalibration checks this implication and three inhabited failures: a source-sized common error preserves the estimates while changing the actual moments; internal ratio agreement does not control the absolute standard; and two bounded but unequal scale errors fail to cancel.

ReportedMomentPrecisionAt retains the nominal 0.5% absolute and 0.1% relative assessments. These are not certified hard bounds or statistical coverage. The calibration countermodels isolate one error source; they do not assert that frequency, line-center, field-shape or reproducibility errors vanish experimentally. The actual extracted source values enter the_source_moment_estimates_allow_an_absolute_scale_ambiguity, while the molecular dynamics use an independently interpreted physical moment rather than the estimated central value.

one_molecule_minimum_does_not_supply_definite_isotope_assignment, named_nuclear_moment_calculation_does_not_supply_ratio_g_factor_and_moment_formula, and mathematical_assignment_does_not_supply_physical_moment make the assignment, formula, and physical-value boundaries explicit. The formula countermodel retains positive moment magnitudes and exact moment = g × spin relations while falsifying the independent frequency-field conversion and Table-II spin/display readout.

06

Precision is conditional, detailed line shape is open, and the method has two built-in limits

Electronic sector, molecular spectrum, and moment error

The molecular high-field argument on original p. 529 now enters the precision route through separate setup and interaction-calculation claims. A nonempty electronic sector is specified by its actual projector and moment operator, not a term label. The effective molecular spectrum has an explicit physical-interpretation premise. Its h, spin, signed moment, and field agree with the selected Li-7 readout.

P^dagger=P; P^2=P; P!=0; mu_e^dagger=mu_e; P mu_e P=0.
First-order neutrality is a restriction to a nonempty electronic sector.
It does not imply mu_e P=0: coupling to other sectors may remain. ElectronicSector.FirstOrderNeutralAt · a_nonempty_first_order_neutral_sector_retains_couplings_to_other_states
N=2J; m_i=N/2-i; E_i,s(B)=-h gamma B m_i+E_s(B)+V_i,s(B).
nu_i,s=gamma B+(V_(i+1),s-V_i,s)/h; positive frequency=|nu_i,s|.
Adjacent sublevels have unit spacing; the same spectator energy cancels.
h>0, B>0, N>0, gamma!=0; |V_(i+1),s-V_i,s|<=h D for every branch and spectator.
mu=(N/2)h|gamma|; mu_hat=(N/2)h|nu_i,s|/B.
|mu_hat-mu|/mu<=D/(|gamma|B)<epsilon when B>D/(|gamma|epsilon), epsilon>0.
This controls individual spectral moment estimates, not a measured line minimum or a pulse probability. MolecularHighFieldSetup · MolecularInteractionCalculation · molecular_regime_and_interaction_control_establish_relative_moment_precision
Uniform gap control for every valid B, plus: for every threshold R there is a valid B>R.
Together these imply: for every epsilon>0 there is a valid field with relative moment error<epsilon.
A result at one high field does not supply unbounded valid-field access.
Constructed bounded regime: 0<B<=1000; relative error=4/B.
At B=1000 it meets tolerance 1/200, but no valid field meets tolerance 1/251. a_uniform_interaction_bound_and_unbounded_valid_fields_allow_any_relative_precision · selected_high_field_precision_does_not_supply_arbitrary_precision_in_the_valid_regime
Constructed effective model: h=2pi, J=1/2, gamma=1/(2pi), V=-4m; angular resonance=B+4.
The inferred relative moment error is 4/B, arbitrarily small at sufficiently large B.
Driving at angular frequency B with Rabi rate 3 for time pi gives P_shifted=9/25.
Deleting the interaction gives P_ideal=1; their difference remains 16/25.
Both selected rotating-frame generators have checked Schrodinger solutions.
Small relative moment error does not imply accurate unshifted-pulse prediction. arbitrarily_small_relative_carrier_shift_does_not_control_transition_probability · constructed model, not historical data or exact laboratory evolution
Independent client: J=3/2, h=3, gamma=2; a spin-1 spectator; V=-6 m_n m_s+m_n^2.
The nine adjacent interaction gaps have magnitude at most 8; frequency budget D=8/3.
A rank-two electronic projector has P mu_e P=0 but mu_e P!=0.
At B=1000 within 0<B<2000, every relative moment error is below 1/700.
A selected inferred moment is 2253/250 instead of 9, with relative error 1/750.
These are computed from fresh data through the public molecular API, not imported countermodel witnesses.

RabiMolecularClient supplies independent spectator, interaction, and electronic-sector data. Its twelve checked theorems exercise the actual gap, regime, and moment inference. The conditional force and joint-state reduction above does not supply microscopic validity of this spectrum, quantitative laboratory pulse-error control, or the observed curve minimum.

The reported 0.5 percent absolute and 0.1 percent relative precision are distinct from the tentative 0.2 or 0.3 percent line-shift assessment. Relative precision assumes that unmodeled broadening does not shift the minimum asymmetrically. Separately, the roughly 1 percent half-widths and symmetric appearance motivate the authors' judgment that a larger displacement seems unlikely. No numerical probability or certified physical bound follows.

reported absolute precision (0.5%) + relative precision (0.1%) + the stated no-asymmetric-broadening assumption + separate tentative line-shift assessment (0.2-0.3%)
→ scoped precision assessment, not a certified line-center bound. PrecisionCalculationAssessment · reported approximation plus tentative support (8)

Symmetry does not fix the line center

LineMinimumProfile supplies a diagnostic dip with a positive 1 percent half-width, nonnegative signal, and a unique minimum displaced by 0.4 percent. Its signal is symmetric about that minimum and reaches half-depth one half-width away. These physical properties do not imply displacement below 0.3 percent. This is not a historical fit or a refutation of the authors' tentative judgment; it blocks treating width and symmetry alone as a deductive bound.

The paper adapter separately uses EvidentialStatusContext for the supported judgment and EstablishmentStatusContext for the actual shift inequality. Changing the independent shift leaves the complete source result unchanged. No arbitrary shift is asserted to solve the separately supplied molecular dynamics.

The line-shape scope contains a negation and a deferral: the simple model does not describe the detailed Li-7 line shape, and the required interaction analysis is deferred. Separately, the pure oscillating field is insensitive to moment sign. The selected angular momentum is known input, while the procedure does not measure it.

established_precision_realizes_open_scoped_uncertainty_assessment classifies absolute calibration and relative reproducibility as distinct assessed sources. It proves stability only in that selected scope and retains detailed line-shape interactions as a relevant unquantified source, so the precision result is explicitly nonexhaustive.

recorded moment estimates + qualified precision assessment + molecular high-field moment bound + open detailed-line-shape scope + sign and angular-momentum limitations → established precision scope with all qualifications retained. established_moments_and_qualifications_retain_precision_scope · precision_scope_retains_open_line_shape_and_method_limitations (9)

pure_oscillating_field_does_not_determine_moment_sign, relative_precision_does_not_supply_absolute_calibration, and resonance_location_does_not_supply_detailed_line_shape prohibit three familiar overreadings.

07

The direct–hyperfine discrepancy produces alternatives, not a selected explanation

The paper-local comparison takes the direct lithium-isotope moment ratio and a hyperfine-derived ratio, compares them, and records a discrepancy. Two distinct interpretations are then proposed: a physical effect or an experimental error.

The unresolved-comparison scope explicitly negates unique selection of either alternative and requires further work. In a separate model comparison, the alpha-particle model is judged more satisfactory, but its improvement is not known to be nonaccidental; other differences among theories remain within claimed accuracy.

direct and hyperfine-based ratios compared + discrepancy observed → {physical effect, experimental error} proposed as distinct alternatives,
but neither uniquely selected + further work required;
alpha-particle model more satisfactory, but nonaccidental improvement not established. comparison_retains_open_physical_and_error_alternatives · evidence, interpretation, and open obligation remain distinct (10)

lithium_discrepancy_open_alternatives_expose_foundation_status realizes the pair as an open-alternative relation. qualified_discussion_retains_open_and_model_comparison_scope preserves both the open comparison and qualified model assessment, while qualified_discussion_separates_interpretation_from_open_obligation extracts their distinct statuses. The countermodel two_discrepancy_explanations_do_not_select_one blocks explanatory overclaim.

08

The complete result preserves eight conclusions and realizes a grounded shared spectroscopy route

The complete conclusion is not merely “moments were measured.” It is the conjunction of established resonance dynamics, beam readout, calibrated observation, nuclear moment estimates, assigned Li-7 representation, recorded estimate, qualified precision scope, and qualified discussion.

dynamics + readout + calibrated observation + nuclear moments + assigned Li-7 representation + recorded estimate + precision scope + qualified discussion → complete scoped Rabi conclusion. all_routes_establish_complete_rabi_conclusion · CompleteRabiConclusion (11)

Controlled experimental inference

The theorem calibrated_resonance_realizes_controlled_experimental_detection maps the paired frequency and field calibrations, observed Li-7 minimum, strong-field suppression of uncontrolled path transitions, detector interpretation, and magnetic-projection-changing transition into the neutral experimental-inference paradigm. The observed minimum, its physical interpretation, and detection of the selected transition remain separate propositions.

Shared resonant-transition spectroscopy

The primary Lean file then maps the paper-local result into a reusable spectroscopy framework. The selected shared model consists of LiCl, the two magnetic states, the oscillating drive and its frequency, the Larmor frequency, transition probability, detector minimum, Li-7 moment, and selected regime. resonance_dynamics_setup_realizes_shared_selected_transition_setup maps the distinct states and applied weak perpendicular drive into the shared pre-output setup. The adapter preserves the paper semantics and consumes each shared predecessor in order: the shared controlled setup is replayed through the retained resonance-dynamics calculation; the shared driven transition is replayed through retained gradient-readout and calibrated-observation calculations; and the shared located readout supplies the Li-7 minimum and Larmor relation used by quantity extraction. The output-led result stores the realized chain and reconstructs its calculation route.

rabi_spectroscopy_stages_make_shared_route_applicable is the narrow stage adapter used by the legacy complete-result wrapper. The source-sensitive theorem single_region_refocusing_realizes_source_structural_spectroscopy_explanation starts earlier: raw weak-drive, gradient-refocusing, calibration, cross-molecule assignment, and Li-7 formula conditions construct every established stage internally. It retains singleRegionGradientRefocusingAndCrossMoleculeMomentExtraction and does not accept CompleteRabiConclusion or an established shared spectroscopy endpoint.

complete paper-local result → shared spectroscopy route applicable → established direct nonvacuous resonant-transition spectroscopy. resonant_transition_spectroscopy_model_retains_paper_semantics · resonance_dynamics_setup_realizes_shared_selected_transition_setup · complete_rabi_result_makes_shared_spectroscopy_route_applicable · complete_rabi_result_realizes_shared_resonant_spectroscopy · complete_rabi_result_exhibits_nonvacuous_shared_resonant_spectroscopy (12)

A second adapter relates the molecular-beam magnetic-resonance theory and the lithium-beam apparatus world to that same model. Grounding reuses the actual resonance-dynamics setup but consumes no Larmor, response, detector, or moment output. Combining that setup-bounded grounding with the established shared spectroscopy transfers every shared claim both to theory entailment and truth in the represented world.

established shared spectroscopy + theory/model/world grounding → grounded shared spectroscopy → every shared claim is transferred to theory and represented world. rabi_spectroscopy_model_inputs_establish_theory_model_grounding · complete_rabi_result_establishes_grounded_shared_spectroscopy · grounded_rabi_spectroscopy_transfers_every_shared_claim (13)
Reader aids and formal audit
A

Concept guide

Terms linked throughout the article resolve to these paper-local meanings.

Driven-transition setup

Distinct magnetic states in LiCl, a Li-7 nucleus with angular momentum and moment, a known homogeneous field, and a weaker perpendicular oscillating field.

ResonanceDynamicsSetup

Resonant transition dynamics

The supplied Larmor, transition, probability-representation, higher-spin, selectivity, decomposition, and sign-insensitivity results.

EstablishedResonanceDynamics

Represented transition probability

A calculated weak-drive probability together with the separate proposition that it represents the selected physical state transition.

calculatedProbabilityRepresentsTransitionAt

Gradient-field refocusing

Geometry-weighted opposite gradients refocus an unchanged projection to the reference point. A changed projection has nonzero displacement, but may still hit a finite detector.

EstablishedBeamResonanceReadout

Mean detector loss and observed minimum

Resolved populated transition weight lowers the controlled mean signal. Separate accurate readings must exceed their combined error budget to infer some multiplet reorientation, not a unique pair. Locating a field-scan minimum and assigning its isotope require further inputs.

detectorMinimumIndicatesSomeMultipletTransitionAt

Calibrated observation

An aligned apparatus, established baseline, fixed-frequency field scan, frequency and field calibration, stability, reproducibility, minima, and recorded curves.

EstablishedCalibratedResonanceObservation

Operational measurement

A measuring procedure implemented by an accessible apparatus and actually performed by the selected agent; accessibility, performance, and existence remain distinct.

OperationalMeasurementSetup

Cross-molecule isotope assignment

Constant frequency-to-field ratios recur across carriers and are combined with abundance, intensity, and a two-molecule requirement to assign nuclei.

NuclearMomentInferenceCalculation

Established nuclear moments

Assigned observations, the retained f/H-to-g conversion, known spins, exact g-times-spin calculation, finite-resolution Table II values, and calibrated moment estimates for Li-6, Li-7, and F-19.

EstablishedNuclearMoments

Assigned Li-7 representation

The bridge from an accepted observation and admissible calculated formula to a performed, represented Li-7 estimate; exact physical possession remains independent.

AssignedLi7MomentRepresentation

Controlled precision assessment

Absolute and relative uncertainty claims conditional on symmetric broadening and absence of an asymmetric minimum shift.

PrecisionCalculationAssessment

Open line-shape scope

The explicit failure of the simple model to describe detailed shape and the deferral of interaction analysis.

LineShapeOpenScope

Method limitations

The procedure does not measure moment sign or angular momentum; angular momentum is supplied as known input.

MethodLimitationScope

Open discrepancy alternatives

Physical effect and experimental error are distinct proposed interpretations, neither uniquely selected, with further work required.

LithiumDiscrepancyOpenAlternatives

Grounded shared spectroscopy

The adapter from the complete paper-local result to a direct nonvacuous reusable resonant-transition result and its explicit theory/model/world interpretation.

complete_rabi_result_establishes_grounded_shared_spectroscopy

Complete Rabi conclusion

The eight-part conjunction of dynamics, readout, observation, moment estimates, assigned representation, recorded estimate, precision scope, and qualified discussion.

CompleteRabiConclusion
B

Complete route, claim, step, theorem, and non-implication inventory

The source map declares six routes, twenty-five claims, and twenty-five sourced steps. Coverage assigns every atom proposition-valued paper-local semantics and certifies each route from its declared predecessor outputs plus explicit hypotheses, while every result and predecessor-bearing setup is rebuilt from its checked premise map.

Complete route inventory
RouteDirect dependencyOutputProfile
Driven dynamics
resonantTransitionDynamics
larmorAndDrivenTransition		—Equation (1)-(2) formula bundle and dynamics resultphysical setup + deferred calculation + retained formula projection
Beam readout
beamRefocusingReadout
gradientRefocusingAndIntensityMinimum		Driven dynamicsReadout resultapparatus principles + deferred calculation
Calibrated observation
calibratedObservation
alignedCalibratedFieldScan		Beam readoutObservation resultoperational setup + deferred evidence calculation
Isotope moments
isotopeMomentInference
crossMoleculeAssignmentAndMomentExtraction		Calibrated observationMoments and Li-7 representationcross-carrier inputs + deferred inference
Precision and method
precisionAndMethodScope
precisionLineShapeAndMethodLimits		Isotope momentsPrecision scopeapproximate + tentative + open and physical scope
Qualified discussion
qualifiedDiscussion
openComparisonWithHyperfineTheory		Precision and methodDiscussion and complete conclusionevidence + interpretations + open obligation + logical synthesis
Driven dynamics · resonant_transition_dynamics_route_is_semantically_realized
stateDynamicsSetup and supplyDynamicsCalculation establish the independent inputs; retainResonanceFormula reconstructs both checked premises and exposes dynamicsFormula; deriveDynamicsResult then certifies the established dynamics.
Beam readout · beam_refocusing_readout_route_is_semantically_realized
stateReadoutSetup reconstructs established dynamics from its checked premise before adjoining the ordered-gradient apparatus facts; supplyReadoutCalculation stays independent, and deriveReadoutResult then consumes only the checked setup and calculation.
Calibrated observation · calibrated_observation_route_is_semantically_realized
stateObservationSetup reconstructs the readout result from its checked premise before adjoining operational, alignment, weakening, and baseline facts; supplyObservationCalculation stays independent, and deriveObservationResult then consumes only the checked setup and calculation.
Isotope moments · isotope_moment_inference_route_is_semantically_realized
stateMomentSetup and stateRepresentationSetup reconstruct their inherited observation and moment claims from checked premises. supplyMomentCalculation stays independent; deriveMomentResult consumes the checked moment setup and calculation; and deriveRepresentationResult uses li7_formula_setup_establishes_representation_and_recorded_estimate to produce both route outputs from the checked formula setup.
Precision and method · precision_and_method_scope_route_is_semantically_realized
stateReportedPrecision and stateTentativeShiftAssessment separately retain the reported approximation and author expectation. statePrecisionAssessment combines their exact checked premises; the later precision result inherits the tentative, open, and physical qualifications.
Qualified discussion · qualified_discussion_route_is_semantically_realized
stateDirectComparison, stateAlternativeInterpretation, stateUnresolvedComparison, and stateModelComparison remain independent local inputs. deriveDiscussionResult reconstructs precision and all four discussion inputs from its checked premise map. composeCompleteConclusion reconstructs all seven declared predecessor claims before producing the final conjunction.

Core source-mapped claims

AtomPaper-local meaningRole/status
resonanceDynamicsSetupKnown-field weak transverse-drive problemSetup · physical principle
resonanceDynamicsCalculationLarmor and transition calculationIntermediate · deferred calculation
resonanceFormulaValue-level equations (1)-(2) for the selected Larmor and weak-drive readoutIntermediate · paper derivation
establishedResonanceDynamicsSelective transition dynamics and sign scopeMain conclusion · paper derivation
beamReadoutSetupOrdered matched-gradient apparatusSetup · physical principle
beamReadoutCalculationBeam preparation, probability interpretation, integral domains, and calibrationIntermediate · explicit model inputs
establishedBeamResonanceReadoutRefocusing, baseline velocity law, and controlled mean detector lossMain conclusion · checked deduction
calibratedObservationSetupOperational, aligned, baseline apparatusSetup · physical principle
calibrationAndObservationCalculationScan, calibration, stability, minima, curvesEvidence · deferred calculation
establishedCalibratedResonanceObservationCalibrated performed observationsMain conclusion · paper derivation
nuclearMomentInferenceSetupPrimary and confirming carrier observationsSetup · physical principle
nuclearMomentInferenceCalculationRatio, assignment, g-factor, spin, and moment inferenceIntermediate · deferred calculation
establishedNuclearMomentsAssigned isotope moment estimatesMain conclusion · paper derivation
li7FormulaSetupAccepted Li-7 observation and admissible calculated formulaSetup · physical principle
establishedLi7MomentRepresentationAssigned formula and recorded moment estimateMain conclusion · paper derivation
reportedPrecisionAssessmentAbsolute/relative precision with the stated broadening assumptionIntermediate · reported approximation
tentativeLineShiftAssessmentTentative support for a 0.2-0.3 percent shift scaleEvidence · author expectation
precisionCalculationAssessmentComposition retaining both inputs and their different scalesIntermediate · checked deduction
lineShapeOpenScopeSimple profile insufficient; interactions deferredIntermediate · open obligation
methodLimitationScopeNo sign or angular-momentum measurementIntermediate · physical principle
establishedPrecisionScopeMoments with precision and method qualificationsMain conclusion · paper derivation
directHyperfineComparisonDirect/hyperfine ratio comparison and discrepancyEvidence · paper derivation
alternativeInterpretationScopePhysical-effect and experimental-error proposalsIntermediate · interpretive inference
unresolvedComparisonScopeNeither proposal selected; further workIntermediate · open obligation
modelComparisonScopeQualified alpha-particle-model assessmentIntermediate · interpretive inference
establishedQualifiedDiscussionComparison with interpretation and open scope separatedMain conclusion · paper derivation
completeRabiConclusionEight-part complete scoped resultMain conclusion · logical rule

The corresponding ClaimId values, in the same order as the atom table, are dynamicsSetup, dynamicsCalculation, dynamicsFormula, dynamicsResult, readoutSetup, readoutCalculation, readoutResult, observationSetup, observationCalculation, observationResult, momentSetup, momentCalculation, momentResult, representationSetup, representationResult, reportedPrecision, tentativeShiftAssessment, precisionAssessment, lineShapeScope, methodScope, precisionResult, directComparison, alternativeInterpretation, unresolvedComparison, modelComparison, discussionResult, and completeConclusion.

Ten formally blocked shortcuts

Available factConclusion not suppliedLean witness
Positive resonance domain, admissible probability, and positive detuningPrinted equations (1)-(2)named_resonance_outputs_do_not_supply_equations_one_and_two
Larmor relationDriven-transition calculationlarmor_relation_does_not_supply_transition_calculation
Calculated weak-drive probabilityPhysical transition representationcalculated_probability_does_not_supply_transition_representation
Transition probabilityDetector minimumtransition_probability_does_not_supply_detector_minimum
Pure oscillating-field responseMoment signpure_oscillating_field_does_not_determine_moment_sign
One molecular-carrier minimumDefinite isotope assignmentone_molecule_minimum_does_not_supply_definite_isotope_assignment
Mathematical formula assignmentPhysical momentmathematical_assignment_does_not_supply_physical_moment
Relative precisionAbsolute calibrationrelative_precision_does_not_supply_absolute_calibration
Resonance locationDetailed line shaperesonance_location_does_not_supply_detailed_line_shape
Two proposed explanationsSelection of onetwo_discrepancy_explanations_do_not_select_one

Primary theorem inventory beyond the six route conclusions

The measurement and representation bridges are li7_moment_operational_access_exposes_foundation_relation, apparatus_and_performance_realize_operational_measurement, recorded_li7_moment_iff_shared_assignment, calibrated_record_and_representation_record_li7_estimate, li7_formula_setup_establishes_representation_and_recorded_estimate, calibrated_li7_formula_faithfully_represents_physical_moment, lithium_discrepancy_open_alternatives_expose_foundation_status, established_nuclear_moments_retain_li7_assignment_and_calculated_estimate, calculated_li7_moment_realizes_assigned_quantity_representation, and assigned_li7_representation_exposes_foundation_assignment. Scope and discussion are retained by established_moments_and_qualifications_retain_precision_scope, precision_scope_retains_open_line_shape_and_method_limitations, comparison_retains_open_physical_and_error_alternatives, qualified_discussion_retains_open_and_model_comparison_scope, and qualified_discussion_separates_interpretation_from_open_obligation. The paper-local synthesis is all_routes_establish_complete_rabi_conclusion.

The shared adapters are checked by calibrated_resonance_realizes_controlled_experimental_detection, established_precision_realizes_open_scoped_uncertainty_assessment, resonant_transition_spectroscopy_model_retains_paper_semantics, resonance_dynamics_setup_realizes_shared_selected_transition_setup, rabi_spectroscopy_stages_make_shared_route_applicable, complete_rabi_result_makes_shared_spectroscopy_route_applicable, single_region_refocusing_realizes_source_structural_spectroscopy_explanation, complete_rabi_result_realizes_shared_resonant_spectroscopy, complete_rabi_result_exhibits_nonvacuous_shared_resonant_spectroscopy, complete_rabi_shared_spectroscopy_realizes_li7_moment_operational_access, rabi_spectroscopy_model_inputs_establish_theory_model_grounding, complete_rabi_result_establishes_grounded_shared_spectroscopy, and grounded_rabi_spectroscopy_transfers_every_shared_claim.

Inherited-status audits

routes_have_exact_predecessor_graph fixes the six-route chain, and routes_have_exact_dependency_closure fixes its transitive closure. dynamics_route_exposes_equations_one_and_two verifies that the formula projection consumes the selected setup and calculation and is advertised as a dynamics-route output. transition_calculations_retain_deferred_status preserves the deferred transition calculation. local_inputs_are_independent_hypotheses and calculation_contracts_are_independent_hypotheses keep local propositions and all four function-shaped calculations independent. dependent_setup_steps_consume_predecessor_semantics, established_results_consume_setup_and_calculation, downstream_results_apply_selected_inputs, and dependent_routes_consume_certified_predecessor_outputs fix the checked dependency direction. precision_result_retains_controlled_assumption preserves the controlled approximation. line_shape_retains_open_obligation preserves the line-shape obligation. alternative_pair_retains_interpretive_status preserves the status of the two proposals. comparison_retains_open_obligation carries nonselection into the discussion result. model_comparison_retains_interpretive_status keeps the model assessment interpretive.

Machine-checked audit boundary

argument_wellFormed, argument_auditable, and routes_wellFormed certify the source structure. every_source_claim_has_semantics covers all 31 claims. Every nontrivial coverage step recovers semantics with atomOfPremise, and all_routes_are_semantically_realizable, aliased by route_semantic_realization_is_exhaustive, constructs all six routes from raw paper-local inputs rather than accepting completed route certificates. The five deferred calculations, molecular regime, controlled broadening assumption, open obligations, and interpretive inputs remain explicit. The molecular error bound is derived from its setup and interaction calculation; it does not discharge pulse-error or line-minimum physics.

Lean-encoded bibliographic record

I. I. Rabi, S. Millman, P. Kusch, and J. R. Zacharias, The Molecular Beam Resonance Method for Measuring Nuclear Magnetic Moments, Physical Review 55 (1939), 526–535.

Current checked semantic identifiers

These complete lists follow current Lean declaration order. Historical and selected explanatory lists elsewhere retain their separate scope.

Primary semantic theorems (310)

magnetic_sublevels_lie_between_minus_and_plus_spin, equal_magnetic_quantum_numbers_are_the_same_sublevel, a_nonzero_moment_distinguishes_every_magnetic_sublevel, admitted_terms_have_unsaturated_factorial_indices, each_factorial_denominator_is_strictly_positive, the_missing_factorial_makes_the_extremal_printed_expression_undefined, totalizing_the_undefined_extremal_row_gives_zero, a_nonzero_cosine_clears_the_admissible_tangent_power, the_majorana_tangent_formula_agrees_with_the_polynomial_on_its_domain, the_polynomial_transition_probability_is_nonnegative, the_polynomial_transition_kernel_is_continuous, row_normalization_bounds_each_actual_transition, the_general_spin_half_kernel_has_the_two_state_entries, the_general_spin_one_kernel_has_all_nine_entries, the_general_spin_three_half_kernel_has_all_sixteen_entries, the_actual_spin_half_kernel_is_row_normalized, the_actual_spin_one_kernel_is_row_normalized, the_actual_spin_three_half_kernel_is_row_normalized, an_admissible_auxiliary_probability_selects_a_normalized_rotation, the_three_source_nuclear_spins_have_normalized_transition_rows, the_three_source_nuclear_spins_have_bounded_transition_probabilities, spin_three_half_probabilities_depend_on_the_auxiliary_probability, the_general_kernel_recovers_the_extremal_half_probability_column, the_1937_printed_index_change_does_not_reproduce_spin_half_transfer, the_polynomial_endpoint_has_full_reversal_despite_totalized_tangent_zero, physical_field_domain_has_positive_detuning_factor, physical_field_domain_bounds_transition_envelope, transition_envelope_is_maximal_iff_drive_matches_larmor, the_spin_half_reference_retains_the_actual_gyromagnetic_ratios, a_physical_target_supplies_a_physical_spin_half_reference, the_spin_half_reference_has_the_same_larmor_frequency, the_target_parameter_formula_is_a_spin_half_auxiliary_calculation, physical_formula_domain_realizes_normalized_transition_outcomes, equation_two_transition_probability_is_bounded_by_resonance_envelope, equation_two_derives_admissible_transition_probability, equation_two_realizes_normalized_transition_outcomes, printed_equation_two_mixing_is_normalized, equation_two_realizes_actual_coherent_pulse, printed_pulse_solves_its_effective_schrodinger_equation, the_two_printed_frequency_ratio_conventions_agree_only_at_resonance, physical_corotating_frequency_agrees_with_printed_frequency_only_at_resonance, corotating_frame_restores_the_physical_laboratory_generator, physical_corotating_source_realizes_nonvacuous_frame_dynamics, exact_corotating_history_is_not_the_full_oscillating_history, oscillating_laboratory_generator_has_both_rotating_components, nonzero_oscillating_field_is_not_exactly_its_corotating_component, equation_one_has_nonzero_signed_magnetic_moment, oscillating_source_formula_admits_opposite_signed_moment, weak_resonant_source_satisfies_the_printed_transition_formula, coherent_weak_field_probability_does_not_supply_exact_laboratory_evolution, weak_detuned_source_does_not_identify_reciprocal_frequency_ratios, positive_fields_do_not_imply_admissible_transition_probability, bounded_transition_probability_does_not_supply_outcome_complement, opposite_signed_moments_have_identical_oscillating_observations, paper_signed_moment_ambiguity_realizes_shared_source_specific_witness, rotating_field_direction_distinguishes_the_two_signed_moments, signed_moment_cannot_replace_its_positive_measured_magnitude, positive_magnitude_does_not_permit_a_zero_signed_physical_moment, a_single_rotating_sense_does_not_retain_both_moment_signs, named_resonance_outputs_do_not_supply_equations_one_and_two, li7_moment_uses_known_three_halves_spin, named_nuclear_moment_calculation_does_not_supply_ratio_g_factor_and_moment_formula, larmor_conversion_exposes_the_field_scale, the_estimate_ratio_retains_the_differential_scale, common_scale_cancels_from_the_moment_ratio, positive_estimates_allow_a_nonexact_common_scale, source_sized_common_error_preserves_estimates_but_not_exact_moments, internal_ratio_agreement_does_not_bound_the_absolute_standard, two_bounded_scale_errors_need_not_cancel_in_a_ratio, the_signal_is_symmetric_about_its_center, the_signal_is_nonnegative, a_positive_width_gives_a_unique_minimum, a_narrow_symmetric_dip_does_not_bound_its_displacement, magnet_transport_satisfies_the_actual_constant_gradient_equations, physical_geometry_has_positive_slit_distance, physical_geometry_has_positive_deflection_factors, the_selected_initial_slope_passes_through_the_actual_slit, composed_ray_transport_has_the_printed_detector_deflection, matched_gradient_geometry_computes_the_projection_difference, matched_fields_refocus_exactly_the_unchanged_projection, matched_fields_transmit_each_unchanged_positive_speed_ray, aperture_acceptance_is_a_bounded_indicator, a_resolved_projection_change_misses_the_actual_detector, actual_refocusing_makes_baseline_acceptance_one, the_actual_readout_loss_is_the_rejected_transition_integral, a_populated_resolved_transition_has_strictly_positive_loss, populated_resolved_transitions_lower_the_controlled_detector_signal, uniform_transmission_computes_the_actual_baseline_flux, uniform_baseline_loss_preserves_the_actual_velocity_law, zero_transition_probability_preserves_the_actual_beam_intensity, a_controlled_signal_drop_excludes_an_almost_everywhere_absent_transition, the_control_geometry_has_actual_positive_unequal_geometric_factors, the_unequal_gradients_match_the_actual_geometry, equal_gradient_magnitudes_do_not_establish_refocusing, a_changed_projection_need_not_miss_a_finite_detector, the_two_speed_integral_uses_both_actual_packets, every_two_speed_integrand_is_integrable, the_two_speed_beam_is_inhabited_physical_and_integrable, the_actual_aperture_distinguishes_slow_and_fast_changed_rays, the_beam_integrates_its_actual_baseline_driven_and_rejected_weights, the_resolved_subset_of_the_actual_beam_has_positive_source_measure, the_generic_readout_deduction_applies_to_the_partly_resolved_beam, the_resonant_loss_changes_the_actual_detected_velocity_mean, a_uniform_baseline_loss_preserves_velocity_shape_but_not_total_intensity, a_detector_signal_drop_alone_does_not_establish_quantum_transitions, a_positive_populated_probability_does_not_supply_resolved_detector_loss, an_unpopulated_resolvable_transition_does_not_reduce_an_inhabited_beam, equal_separate_weakening_does_not_universally_establish_matched_geometry, matched_baseline_velocity_statistics_do_not_survive_resonant_selection, a_mean_loss_larger_than_the_error_budget_forces_observed_ordering, a_resolved_observed_loss_implies_a_mean_signal_loss, a_controlled_resolved_observed_loss_excludes_absent_transitions, a_positive_mean_signal_loss_need_not_order_every_admissible_reading, an_unresolved_observed_drop_does_not_establish_transitions_even_with_controlled_background, the_source_spins_have_actual_normalized_multiplet_transitions, every_multiplet_channel_has_nonnegative_probability, every_unchanged_sublevel_refocuses, normalized_rows_give_the_population_weighted_loss_identity, the_actual_signal_loss_sums_over_all_initial_and_final_sublevels, every_rejected_population_density_is_nonnegative, an_actually_populated_resolved_channel_has_positive_density, a_populated_resolved_multiplet_lowers_the_controlled_signal, absent_populated_reorientation_has_zero_rejected_density, a_controlled_multiplet_signal_drop_requires_populated_reorientation, uniform_transmission_computes_the_multiplet_baseline_density, uniform_transmission_computes_the_multiplet_baseline_flux, an_incoherent_normalized_population_preserves_the_uniform_baseline_velocity_law, a_resolved_multiplet_mean_loss_orders_accurate_readings, a_resolved_observed_loss_requires_a_multiplet_mean_loss, a_controlled_resolved_multiplet_readout_requires_populated_reorientation, the_common_source_pulse_has_the_target_larmor_frequency, the_two_speeds_receive_the_same_auxiliary_probability_from_one_field_history, the_auxiliary_half_spin_has_a_different_moment_but_the_same_ratio, the_constructed_beam_uses_the_source_pulse_moment_and_auxiliary_probability, the_beam_has_an_actual_normalized_initial_population, the_finite_multiplet_beam_is_physical_and_integrable, the_actual_ray_deflection_is_set_by_the_two_sublevels, the_slow_beam_detector_accepts_exactly_unchanged_sublevels, the_fast_beam_detector_accepts_every_final_sublevel, the_half_auxiliary_probability_fills_the_actual_spin_three_half_matrix, the_dirac_beam_integral_uses_its_actual_speed, the_slow_beam_densities_include_every_final_sublevel, the_fast_beam_densities_include_every_final_sublevel, the_slow_beam_loss_is_neither_auxiliary_nor_full_reversal_probability, a_fast_reorienting_multiplet_need_not_lower_the_detector_signal, the_same_multiplet_loss_does_not_identify_a_particular_populated_pair, a_multiplet_mean_loss_need_not_order_accurate_readings, the_zero_pulse_has_a_physical_multiplet_and_no_populated_reorientation, an_unresolved_multiplet_observed_drop_need_not_be_reorientation, adjacent_magnetic_sublevels_have_unit_spacing, the_actual_adjacent_gap_retains_the_interaction_correction, the_interaction_gap_controls_the_oriented_ratio_error, the_positive_frequency_controls_the_magnitude_ratio_error, the_known_nuclear_spin_converts_the_ratio_bound_to_a_moment_bound, the_physical_moment_magnitude_is_strictly_positive, the_relative_moment_error_is_controlled_by_the_internal_to_zeeman_ratio, a_valid_high_field_threshold_supplies_the_requested_relative_moment_precision, a_nonempty_first_order_neutral_sector_retains_couplings_to_other_states, electronic_suppression_and_controlled_gap_calculations_establish_moment_precision, the_established_precision_retains_a_populated_spectator_and_valid_regime, a_uniform_interaction_bound_and_unbounded_valid_fields_allow_any_relative_precision, both_nuclear_spectra_are_physical, the_actual_internal_energy_gap_has_a_field_independent_bound, the_actual_spectra_determine_the_two_rotating_frame_detunings, the_two_spectra_produce_the_actual_pulses, the_measured_positive_frequency_has_the_actual_relative_moment_error, both_effective_pulses_are_actual_schrodinger_solutions, the_same_drive_and_duration_give_distinct_actual_transition_probabilities, arbitrarily_small_relative_carrier_shift_does_not_control_transition_probability, the_bounded_field_regime_has_a_genuine_controlled_precision_result, selected_high_field_precision_does_not_supply_arbitrary_precision_in_the_valid_regime, average_const, average_mul_const, average_congr_on_support, average_map, average_finite, average_pure, bounded_branch_observables_have_genuine_probability_averages, differentiating_the_actual_spectrum_retains_both_corrections, the_adiabatic_force_law_and_energy_slope_determine_the_transverse_force, the_spectral_calculations_determine_both_actual_forces, the_force_readout_ray_uses_the_actual_spectral_projections, the_joint_transition_acceptance_is_a_genuine_bounded_expectation, bounded_spectator_transmission_gives_defined_conditional_expectations, the_same_signed_moment_calibrates_the_spectral_nuclear_projection, the_detector_correction_retains_actual_spectator_and_interaction_slopes, a_force_slope_budget_bounds_the_actual_detector_position_error, a_force_error_budget_preserves_aperture_decisions_only_with_a_margin, matched_forces_and_conserved_spectator_projection_reduce_the_detector_position, conserved_spectator_projection_reduces_actual_aperture_acceptance, the_joint_transition_average_uses_the_source_nuclear_marginal, actual_spectator_preparation_reduces_the_baseline_density, joint_marginals_and_spectator_control_reduce_the_driven_density, force_and_joint_population_controls_reduce_both_measured_densities, the_molecular_baseline_and_driven_integrals_have_actual_integration_domains, the_spectator_resolved_beam_has_the_derived_nuclear_only_mean_signals, controlled_molecular_signal_loss_requires_populated_nuclear_reorientation, a_resolved_observed_molecular_loss_requires_populated_nuclear_reorientation, both_spin_spectra_are_physical_with_exact_nuclear_gap_control, both_spectra_give_the_same_actual_nuclear_frequencies, the_positive_frequency_infers_the_exact_intrinsic_nuclear_moment, the_total_projection_is_derived_from_the_actual_energy, deleting_spectator_energy_changes_the_actual_force_projection, every_constructed_ray_uses_the_spectral_energy_slopes, matched_transport_retains_both_nuclear_and_spectator_changes, a_conserved_spectator_cancels_at_the_matched_detector, the_spectator_resonance_is_distinct_from_the_target_nuclear_resonance, a_selected_unitary_pulse_really_flips_the_spectator, the_spectator_pulse_has_an_actual_rotating_frame_generator, the_apparatuses_are_physical_but_only_one_is_matched, exact_nuclear_frequency_and_matching_do_not_exclude_a_spectator_only_deflection, cancellation_of_the_endpoint_does_not_preserve_the_selected_initial_ray, the_spectator_population_is_normalized_and_has_zero_mean_projection, the_mismatched_aperture_resolves_both_spectator_branches, zero_mean_spectator_moment_does_not_justify_averaging_before_aperture_selection, the_zero_drive_nuclear_kernel_is_the_identity, the_nuclear_reference_beam_has_physical_normalized_preparation_and_controlled_detection, the_joint_force_rays_are_the_spectrally_calculated_molecular_rays, the_joint_beam_satisfies_the_actual_spectral_force_calculations, the_joint_beam_realizes_adiabatic_forces_in_both_magnets, both_joint_beams_have_correct_nuclear_marginals_and_preparation, the_unchanged_spectator_model_satisfies_all_joint_readout_controls, the_spectator_flip_model_violates_the_actual_joint_control, neither_joint_beam_has_any_nuclear_reorientation, the_reference_and_static_spectator_beams_have_unit_mean_signals, the_spectator_only_flip_lowers_the_actual_joint_beam_signal, the_spectator_only_joint_pulse_is_actually_unitary, the_joint_flip_kernel_is_the_actual_born_probability_of_the_unitary_pulse, the_source_direction_filter_selects_one_of_two_populated_spectator_branches, matching_with_unchanged_spectators_does_not_supply_the_prepared_source_weights, a_computed_force_error_budget_without_aperture_margin_does_not_preserve_acceptance, the_velocity_resolved_source_formula_normalizes_the_actual_target_matrix, li7_moment_operational_access_exposes_foundation_relation, apparatus_and_performance_realize_operational_measurement, recorded_li7_moment_iff_shared_assignment, recorded_li7_estimate_and_faithfulness_establish_exact_value, calibrated_li7_formula_faithfully_represents_physical_moment, lithium_discrepancy_open_alternatives_expose_foundation_status, the_source_formula_normalizes_the_auxiliary_and_li7_transition_matrix, resonance_formula_derives_opposite_signed_moment_ambiguity, larmor_and_transition_calculations_establish_resonance_dynamics, resonance_dynamics_calculation_retains_equations_one_and_two, established_resonance_dynamics_realizes_normalized_transition_outcomes, established_resonance_dynamics_realizes_actual_coherent_pulse, established_resonance_dynamics_retains_the_corotating_auxiliary_boundary, established_resonance_dynamics_uses_the_auxiliary_spin_half_system, established_resonance_dynamics_has_the_actual_li7_transition_matrix, established_resonance_dynamics_retains_actual_magnetic_projections, molecular_force_and_joint_calculations_establish_the_actual_detector_reduction, beam_calculation_retains_explicit_molecular_force_and_population_inputs, beam_model_inputs_derive_the_actual_readout_output, matched_gradients_and_projection_change_establish_detector_minimum, established_readout_has_the_actual_rejected_transition_identity, established_readout_has_positive_rejected_transition_weight, established_readout_retains_the_actual_baseline_velocity_law, established_readout_has_the_actual_baseline_transmission_factor, established_readout_excludes_an_absent_actual_transition, established_readout_retains_the_molecular_force_and_joint_population_controls, established_readout_requires_distinct_magnetic_states, established_readout_calibrates_the_actual_detector_signals, aligned_apparatus_and_calibrations_establish_observed_resonances, calibrated_resonance_realizes_controlled_experimental_detection, the_source_moment_estimates_allow_an_absolute_scale_ambiguity, cross_molecule_resonances_and_known_spins_establish_nuclear_moments, nuclear_moment_inference_calculation_retains_ratio_g_factor_and_moment_formula, established_nuclear_moments_retain_li7_assignment_and_calculated_estimate, calculated_li7_moment_realizes_assigned_quantity_representation, assigned_li7_representation_exposes_foundation_assignment, calibrated_record_and_representation_record_li7_estimate, li7_formula_setup_establishes_representation_and_recorded_estimate, molecular_regime_and_interaction_control_establish_relative_moment_precision, the_molecular_spectrum_retains_the_same_li7_moment_parameter, established_molecular_precision_bounds_the_actual_li7_moment_error, the_molecular_precision_result_retains_the_conditional_arbitrary_precision_extension, reported_precision_and_tentative_shift_assemble_assessment, precision_assessment_retains_distinct_reported_accuracy_scales, precision_assessment_retains_tentative_shift_support_at_a_distinct_scale, established_precision_realizes_open_scoped_uncertainty_assessment, established_moments_and_qualifications_retain_precision_scope, precision_scope_retains_open_line_shape_and_method_limitations, established_precision_retains_the_molecular_high_field_error_bound, comparison_retains_open_physical_and_error_alternatives, qualified_discussion_retains_open_and_model_comparison_scope, qualified_discussion_separates_interpretation_from_open_obligation, complete_result_does_not_depend_on_exact_moment_possession, complete_result_does_not_establish_the_actual_line_shift, tentative_shift_support_is_not_a_certified_actual_bound, recorded_estimate_allows_a_distinct_physical_moment, all_routes_establish_complete_rabi_conclusion, resonant_transition_spectroscopy_model_retains_paper_semantics, resonance_dynamics_setup_realizes_shared_selected_transition_setup, rabi_spectroscopy_stages_make_shared_route_applicable, complete_rabi_result_makes_shared_spectroscopy_route_applicable, single_region_refocusing_realizes_source_structural_spectroscopy_explanation, complete_rabi_result_realizes_shared_resonant_spectroscopy, complete_rabi_result_exhibits_nonvacuous_shared_resonant_spectroscopy, complete_rabi_result_exhibits_normalized_shared_resonant_spectroscopy, complete_rabi_shared_spectroscopy_realizes_li7_moment_operational_access, rabi_spectroscopy_model_inputs_establish_theory_model_grounding, complete_rabi_result_establishes_grounded_shared_spectroscopy, grounded_rabi_spectroscopy_transfers_every_shared_claim, larmor_relation_does_not_supply_transition_calculation, calculated_probability_does_not_supply_transition_representation, transition_probability_does_not_supply_detector_minimum, pure_oscillating_field_does_not_determine_moment_sign, one_molecule_minimum_does_not_supply_definite_isotope_assignment, mathematical_assignment_does_not_supply_physical_moment, relative_precision_does_not_supply_absolute_calibration, resonance_location_does_not_supply_detailed_line_shape, two_discrepancy_explanations_do_not_select_one

Coverage theorems (17)

dynamics_atom_retains_actual_coherent_pulse, molecular_precision_atom_retains_the_actual_li7_moment_error_bound, molecular_precision_atom_retains_the_conditional_valid_field_family_extension, molecular_force_atom_retains_the_actual_joint_readout_and_integration_domains, every_source_claim_has_semantics, resonant_transition_dynamics_route_is_semantically_realized, beam_refocusing_readout_route_is_semantically_realized, calibrated_observation_route_is_semantically_realized, isotope_moment_inference_route_is_semantically_realized, moment_route_recovers_ratio_g_factor_and_moment_source_formula, precision_and_method_scope_route_is_semantically_realized, qualified_discussion_route_is_semantically_realized, all_routes_are_semantically_realizable, readout_atom_retains_the_actual_detector_count_identity, readout_atom_retains_the_actual_baseline_velocity_law, readout_atom_excludes_an_absent_actual_transition, dynamics_atom_retains_the_actual_higher_spin_transition_matrix

Source-map audit theorems (23)

argument_wellFormed, argument_auditable, routes_wellFormed, routes_have_exact_predecessor_graph, routes_have_exact_dependency_closure, transition_calculations_retain_deferred_status, dynamics_route_exposes_equations_one_and_two, dynamics_route_exposes_opposite_signed_moment_ambiguity, moment_route_exposes_ratio_g_factor_and_moment_formula, molecular_precision_requires_its_regime_and_interaction_calculation, the_readout_route_requires_the_molecular_force_and_joint_population_reduction, local_inputs_are_independent_hypotheses, precision_scope_retains_a_separate_tentative_judgment, calculation_contracts_are_independent_hypotheses, dependent_setup_steps_consume_predecessor_semantics, established_results_consume_setup_and_calculation, downstream_results_apply_selected_inputs, dependent_routes_consume_certified_predecessor_outputs, precision_result_retains_controlled_assumption, line_shape_retains_open_obligation, alternative_pair_retains_interpretive_status, comparison_retains_open_obligation, model_comparison_retains_interpretive_status

Semantic atoms (36)

resonanceDynamicsSetup, resonanceDynamicsCalculation, resonanceFormula, normalizedDrivenTransitionOutcomes, oscillatingSignedMomentAmbiguity, establishedResonanceDynamics, beamReadoutSetup, beamReadoutCalculation, molecularBeamForceSetup, molecularBeamForceCalculation, establishedMolecularBeamReduction, establishedBeamResonanceReadout, calibratedObservationSetup, calibrationAndObservationCalculation, establishedCalibratedResonanceObservation, nuclearMomentInferenceSetup, nuclearMomentInferenceCalculation, nuclearMomentFormula, establishedNuclearMoments, li7FormulaSetup, establishedLi7MomentRepresentation, molecularHighFieldSetup, molecularInteractionCalculation, establishedMolecularMomentPrecision, reportedPrecisionAssessment, tentativeLineShiftAssessment, precisionCalculationAssessment, lineShapeOpenScope, methodLimitationScope, establishedPrecisionScope, directHyperfineComparison, alternativeInterpretationScope, unresolvedComparisonScope, modelComparisonScope, establishedQualifiedDiscussion, completeRabiConclusion

Claim identifiers (36)

dynamicsSetup, dynamicsCalculation, dynamicsFormula, dynamicsProbability, dynamicsSignAmbiguity, dynamicsResult, readoutSetup, readoutCalculation, forceSetup, forceCalculation, forceReduction, readoutResult, observationSetup, observationCalculation, observationResult, momentSetup, momentCalculation, momentFormula, momentResult, representationSetup, representationResult, molecularSetup, molecularCalculation, molecularPrecision, reportedPrecision, tentativeShiftAssessment, precisionAssessment, lineShapeScope, methodScope, precisionResult, directComparison, alternativeInterpretation, unresolvedComparison, modelComparison, discussionResult, completeConclusion

Step identifiers (36)

stateDynamicsSetup, supplyDynamicsCalculation, retainResonanceFormula, deriveNormalizedTransitionProbability, deriveOscillatingSignedMomentAmbiguity, deriveDynamicsResult, stateReadoutSetup, supplyReadoutCalculation, stateMolecularBeamForceSetup, supplyMolecularBeamForceCalculation, deriveMolecularBeamReduction, deriveReadoutResult, stateObservationSetup, supplyObservationCalculation, deriveObservationResult, stateMomentSetup, supplyMomentCalculation, retainNuclearMomentFormula, deriveMomentResult, stateRepresentationSetup, deriveRepresentationResult, stateMolecularHighFieldSetup, supplyMolecularInteractionCalculation, deriveMolecularMomentPrecision, stateReportedPrecision, stateTentativeShiftAssessment, statePrecisionAssessment, stateLineShapeScope, stateMethodScope, derivePrecisionResult, stateDirectComparison, stateAlternativeInterpretation, stateUnresolvedComparison, stateModelComparison, deriveDiscussionResult, composeCompleteConclusion

Route identifiers (6)

resonantTransitionDynamics, beamRefocusingReadout, calibratedObservation, isotopeMomentInference, precisionAndMethodScope, qualifiedDiscussion

Route kinds (6)

larmorAndDrivenTransition, gradientRefocusingAndIntensityMinimum, alignedCalibratedFieldScan, crossMoleculeAssignmentAndMomentExtraction, precisionLineShapeAndMethodLimits, openComparisonWithHyperfineTheory

R

Checked source-route details

This ledger is generated from the elaborated Lean route records. It lists direct predecessors, ordered inference steps, and exported claims. The independent fidelity audit checks every field; this ledger does not replace the physical semantics or certify every explanatory diagram.

resonantTransitionDynamics

Logical kind: larmorAndDrivenTransition.

Required predecessor routes: none.

Ordered inference steps: stateDynamicsSetup, supplyDynamicsCalculation, retainResonanceFormula, deriveNormalizedTransitionProbability, deriveOscillatingSignedMomentAmbiguity, deriveDynamicsResult.

Exported conclusions: dynamicsFormula, dynamicsProbability, dynamicsSignAmbiguity, dynamicsResult.

beamRefocusingReadout

Logical kind: gradientRefocusingAndIntensityMinimum.

Required predecessor routes: resonantTransitionDynamics.

Ordered inference steps: stateReadoutSetup, supplyReadoutCalculation, stateMolecularBeamForceSetup, supplyMolecularBeamForceCalculation, deriveMolecularBeamReduction, deriveReadoutResult.

Exported conclusions: forceReduction, readoutResult.

calibratedObservation

Logical kind: alignedCalibratedFieldScan.

Required predecessor routes: beamRefocusingReadout.

Ordered inference steps: stateObservationSetup, supplyObservationCalculation, deriveObservationResult.

Exported conclusions: observationResult.

isotopeMomentInference

Logical kind: crossMoleculeAssignmentAndMomentExtraction.

Required predecessor routes: calibratedObservation.

Ordered inference steps: stateMomentSetup, supplyMomentCalculation, retainNuclearMomentFormula, deriveMomentResult, stateRepresentationSetup, deriveRepresentationResult.

Exported conclusions: momentFormula, momentResult, representationResult.

precisionAndMethodScope

Logical kind: precisionLineShapeAndMethodLimits.

Required predecessor routes: isotopeMomentInference.

Ordered inference steps: stateMolecularHighFieldSetup, supplyMolecularInteractionCalculation, deriveMolecularMomentPrecision, stateReportedPrecision, stateTentativeShiftAssessment, statePrecisionAssessment, stateLineShapeScope, stateMethodScope, derivePrecisionResult.

Exported conclusions: molecularPrecision, precisionResult.

qualifiedDiscussion

Logical kind: openComparisonWithHyperfineTheory.

Required predecessor routes: precisionAndMethodScope.

Ordered inference steps: stateDirectComparison, stateAlternativeInterpretation, stateUnresolvedComparison, stateModelComparison, deriveDiscussionResult, composeCompleteConclusion.

Exported conclusions: discussionResult, completeConclusion.