PhysicsLogic · Paper-first edition Lean-extracted article 030

Formal reconstruction · Statistical mechanics and linear response

Irreversibility and Generalized Noise

The logical anatomy of perturbative dissipation, spontaneous equilibrium fluctuations, the quantum noise–resistance relation, its classical limit, and Brownian, electromagnetic, and acoustic specializations

Original work encoded in Lean: H. B. Callen and T. A. Welton Edition: human-readable logical reconstruction
Formal object PhysicsLogic.Papers.CallenWelton1951
Physical result The same equilibrium spectral construction governs the real dissipative response to a weak periodic force and the spontaneous generalized-force noise, yielding a quantum noise–dissipation relation with zero-point contribution and a classical/Nyquist limit at high temperature or low frequency
Argument architecture 7 routes · 24 semantic claims · 3 applications · 2 independent spectral calculations · 1 checked equation-(4.8)-(4.11) formula output · 1 inhabited classical limit · 1 two-system interpretation · 1 open future program · 45 formal physical countermodels

Definitions, structures, and assumptions

Structures, classes, and inductive alternatives

  • structureTyped equilibrium and dissipative structure used by the complete shared calculation. The calculated noise-value map is excluded because it belongs to the explained phenomenon rather than the constraining setup.
  • structureThe selected noise-dissipation calculation is proof-free data. It retains its physical indices and the exact proposition-valued relations and value maps used by the shared route.
  • inductiveThe exact shared claims established by the Nyquist, Callen-Welton, and Kubo routes. Circuit elements, quantum operators, correlation functions, and conductivity tensors remain paper-local.
  • structure
  • inductive
  • inductive
  • inductive
  • inductive
  • inductive
  • inductive
  • inductive
  • structure
  • structurePaper-local interpretation of the selected noise-dissipation calculation. Theory use and representation of a physical equilibrium system are independent bridges.
  • structureProof-free source constraint for one paper-local derivation of an equilibrium noise/dissipation relation. It stores the exact selected calculation, a typed derivation token, and the proposition-valued interpretation of that token, but no proof that the derivation obtains and no noise-relation output.
  • structureThe containing theory remains distinct from the selected calculation.
  • structureThe represented equilibrium system remains distinct from the calculation and the theory using it.
  • structureThe represented, convention-indexed, frequency-resolved noise relation. It does not identify the selected value with an observed record or erase the paper-local spectrum or correlation convention.
  • structureA density and its reference measure are inseparable. This data can describe discrete lines, a gap density, or an angular-frequency density; physical reconstruction, convergence, and coordinate conventions are separate propositions, with no FDT conclusion stored as a proof field.
  • structureThe base measure counts states or supplies their density of states; it is not the canonical probability law. No normalization or temperature assumption is stored as a proof field.
  • structureFrequencies may have different spectral fibres and measures, but not different Hamiltonians, temperatures, or observables. The measures still need a physical spectral-resolution interpretation supplied by the paper.
  • structureA selected spectral slice, not a product measure restricted to a possibly null energy surface. The source supplies its spectral-resolution meaning. The two matrix-element functions can describe different observables, so their ordered cross spectrum need not be real or positive.
  • 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
  • inductiveCallen-Welton's common quantum spectral-sum derivation.
  • inductive
  • inductive
  • structure
  • structure
  • structure
  • structureEquations (4.8)-(4.11) retain actual spectral integrals, distinct quantum and classical readouts, and a quantitative passband comparison.
  • structureSections V-VII retain distinct Brownian, electric-radiation, and acoustic quantities rather than identifying three named applications.
  • structureSections II-IV distinguish Boltzmann-related upward/downward transitions, their sum and difference, and the quantum versus classical force spectra.
  • structureSection VIII describes a distinct source and dissipative partner, actual coherence/energy changes, and a proposed rather than completed broad theory.
  • structureThe dense-spectrum/golden-rule interpretation is an external physical input. These are calculated rates and densities from the same canonical transition slice, not asserted final force-noise or resistance values.
  • structure
  • structureA real measure replaces an arbitrary integral-valued function. A source-continuum representation is separate from finite spectral controls.
  • structure
  • structure
  • structure

Definitions and domain choices

  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe declared frequency sector contains an actual frequency. This keeps all frequency-scoped readout and equality propositions from becoming vacuous.
  • definition
  • definition
  • definition
  • definitionThe paper-local noise calculation must retain the convention under which its selected value is a spectrum or correlation. The generic framework does not identify one-sided, positive-frequency, ordered, or symmetrized conventions.
  • definition
  • definition
  • definition
  • definition
  • definitionThe direct, nonvacuous noise-dissipation result. The setup contains an actual frequency in the selected sector, while the calculations, represented readouts, selected convention, and quantitative relation hold directly over the whole sector. No implication-valued route bridge is stored here.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe selected equilibrium-dissipative constraint as typed data.
  • definitionExact proof-free source constraint selected by a model and derivation.
  • definitionThe selected represented noise relation whose structure is explained.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionInterpret a declared shared claim directly at the selected calculation. This model-level semantics is independent of any later theory or world bridge.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionAll three calculation flags can be true while the declared frequency sector is empty. The strengthened shared route rejects this vacuous case.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionSource-sensitive structural explanation by one typed paper derivation.
  • definitionThe complete selected route structurally explains its noise relation.
  • definition
  • definition
  • definitionThe selected model is exactly the proof-free calculation data declared by the paper-local adapter.
  • definitionThe complete exact pre-output boundary used for theory/model/world grounding. It fixes the context-owned calculation and requires the inhabited equilibrium linear-dissipative setup, but no calculation, readout, convention, or noise-dissipation relation.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionSource-sensitive structural semantics for one typed paper derivation. The source constraint must carry the exact selected calculation and realized derivation token; the physical constraint and explained phenomenon remain the ones fixed by the existing shared route.
  • definitionStructural-explanation semantics for the complete equilibrium noise-dissipation route. A candidate satisfies the typed constraint only when the exact selected setup, all three calculations, the physical readouts, the noise-value convention, and the frequency-scoped relation bridge are applicable. Numerical equality or a dissipative label alone is insufficient.
  • definitionInterpret the selected spectral calculation without identifying it with its containing theory or represented physical equilibrium system.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionA physical resolution reconstructs both ordered state-pair integrals on every measurable sub-band of its declared window. The contract contains no relaxation spectrum or thermal-factor equality.
  • definitionThis convention is appropriate for an energy-gap density. With gap hbar*omega it must not be silently replaced by Lebesgue measure in omega.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionIntegrability is not inferred from a totalized integral or a named partition value. A zero or divergent partition does not describe equilibrium.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionMatrix elements of [H,A] in the same energy representation.
  • definitionEnergy-basis matrix elements of exp(iHt/hbar) A exp(-iHt/hbar). The identification of the energy basis with a physical Hamiltonian is a separate spectral-representation input, not an inferred spectral theorem.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionA real two-level Gibbs ensemble. The finite realization tests spectral logic only; it is not a dense-spectrum golden-rule or continuum model.
  • definition
  • definitionAn ordinary integrable density represents the correlation measure with respect to energy-gap volume. It cannot represent a nonzero spectral atom.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionA band selects state pairs by their energy difference. This is not a restriction to a potentially null constant-energy surface. The interpretation of the basis measure and matrix kernels is still a physical source input.
  • definition
  • definition
  • definitionKeep individual state pairs as spectral labels before any regrouping by frequency. The reference measure will carry the state-pair multiplicities.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionHermiticity is needed for positive self-noise, not for the algebraic cross-spectrum relation between distinct observables.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionFull imaginary-time canonical response. This includes invariant weight; it is not automatically the source's invariant-subtracted relaxation.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe contribution p_i A(t_first)_ij B(t_second)_ji uses both Heisenberg evolutions from the same energy function.
  • definitionThe nonzero-gap canonical relaxation coefficient. This totalized quotient does not represent an invariant zero-frequency contribution.
  • definitionReversing the transition and exchanging the observables is the opposite ordered spectral line of the same system, with the same transition measure.
  • definition
  • definition
  • definition
  • definition
  • definitionThe imaginary-time canonical kernel, before the invariant contribution is subtracted in Kubo (3.11). Its zero-gap value is an actual integral.
  • definitionThe static value is only a scalar continuation. Application to a complete zero-frequency spectral measure needs its own invariant-sector argument.
  • 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
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionRaw source premises for the Callen-Welton derivation. The two independently calculated spectral sums and their comparison are retained as route contracts.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • 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 printed generalized-Nyquist readout is attached to the selected temperature, frequency, dissipation, generalized-force noise, and positive-frequency integral used by the paper's relation route.
  • definition
  • definitionSections II-III are consumed as separate predecessors. The remaining inputs identify actual measured spectra, their angular-frequency measure and finite readout, and the oscillator energy expression. No finished FDT or classical equality is supplied here.
  • definitionEquations (4.4)-(4.7) use a density per energy gap. Its reference measure must reconstruct the same two state-pair sums and must not be silently replaced by d-omega: the source's separate force-noise readout retains the hbar Jacobian and the Q-dot squared-frequency factor.
  • definitionEquations (2.1)-(2.3), (3.1), and (4.1)-(4.7) use the same H_0 and Q. This ties the common spectral energy and both kernels to those physical data, without assuming the later relation between resistance and force noise.
  • definition
  • definitionSelected value-level equations (4.8)-(4.11) and their distinct Boltzmann/difference/sum source calculation.
  • definitionThe exact quantum relation has no classical-regime restriction. The selected classical comparison is retained only under its own small-gap condition, independently of the full-band integral error estimate.
  • definitionThe selected spectral data have the same physical readouts as the integrated formula. This identification contains no response/noise equality.
  • definitionCanonical matrix data and oscillator/reference readouts precede the comparison of absorbed power with spontaneous force fluctuations.
  • definition
  • definitionCallen and Welton begin with an extensive thermodynamic coordinate and its conjugate intensive generalized force. This is paper-local structure: the shared noise-dissipation route needs only the resulting generalized force.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • 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 response premise identifies a measured resistance with the real impedance of the same driven canonical system. Its power correspondence is the physical golden-rule/linear-response input, not the noise conclusion.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionSection III supplies the independent coordinate-fluctuation calculation: the force readout uses the same impedance, the velocity square, and the energy-to-angular-frequency Jacobian. It does not assume a noise/R ratio.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionCallen and Welton's interpretation distinguishes the generalized quantum spectral calculation from the perturbative theory using it and from the zero-force equilibrium system whose spontaneous generalized-force noise is represented. Primary-source anchors: sections II-III for perturbative dissipation and equilibrium fluctuations; section IV for their generalized relation.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionA named generalized relation can coexist with a false oscillator factor.
  • definition
  • definition
  • definition
  • definition
  • definitionThe measured mean square is the integral of the independently calculated force spectrum. The classical number is a reference-model integral, not an asserted equality with the quantum observation.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionA finite spectral control with an actual Dirac measure; it does not realize the dense-spectrum continuum representation of the source.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionSections II-IV, especially (2.8) and (4.3)-(4.5). The spectral weights are obtained from one canonical ensemble and one Hermitian coordinate. The legacy `upward` slot denotes the suppressed upper-state population term; it is the emission weight, not the lower-population absorption weight. Spectral resolution and convergence remain explicit physical inputs.
  • definition
  • definitionThe high-temperature comparison is separate from the exact quantum relation. No quantum force-noise equality is assumed in this input.
  • definition
  • definitionThe original (4.6)-(4.7) retain their distinct response and force-noise prefactors. In (4.6) it is pi*omega, not pi*omega/hbar. The Q-dot conversion accounts for the hbar*omega^2 factor in the positive-frequency force noise.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionFinite readouts test the formula and its conditional classical clause; they are not asserted to realize the original continuum density.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • 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 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
  • 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

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
  • constructor
  • definition
  • checked statement
  • definition
  • 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
  • definition
  • definition
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • recursor
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • 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
  • 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
  • definition
  • definition
  • 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
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • inductive
  • definition
  • instance
  • constructor
  • definition
  • checked statement
  • definition
  • 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
  • definition
  • definition
  • 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
  • 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
  • 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
  • definition
  • definition
  • definition
  • definition
  • definition
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • definition
  • checked statement
  • definition
  • definition
  • instance
  • checked statement
  • checked statement
  • instance
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • checked statement
  • checked statement
  • definition
  • inductive
  • definition
  • instance
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • recursor
  • definition
  • 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
  • definition
  • definition
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • recursor
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • structure
  • definition
  • instance
  • checked statement
  • checked statement
  • checked statement
  • definition
  • definition
  • checked statement
  • checked statement
  • definition
  • checked statement
  • checked statementThe checked generalized-relation atom retains the selected equations (4.8)-(4.11) package before the source map projects it as a distinct output.
  • definition
  • definition
  • definition
  • checked statement
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • checked statement
  • definition
  • checked statement
  • definition
  • definition
  • checked statement
  • recursor
  • definition
  • checked statement
  • checked statement
  • inductive
  • definition
  • instance
  • definition
  • 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
  • definition
  • definition
  • 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
  • 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
  • checked statement
  • checked statement
  • definition
  • checked statement
  • checked statement
  • definition
  • checked statement
  • checked statement
  • checked statement
  • definition
  • checked statement
  • definition
  • definition
  • 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
  • definition
  • checked statement
  • checked statement
  • definition
  • definition
  • definition
  • definition
  • definition
  • checked statement
  • definition
  • definition
  • checked statement
  • checked statement
  • definition
  • definition
  • definition
  • 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 statementCalling an observable a generalized force does not recover the extensive thermodynamic coordinate to which Callen and Welton make it conjugate.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementCallen and Welton's complete perturbative-dissipation, equilibrium- fluctuation, convention, and quantum relation route structurally explains its represented generalized-force noise relation. The projection preserves the positive-frequency mean-square convention and is neither a causal nor an experimental-observation claim.
  • checked statement
  • checked statementCallen-Welton 1951, p. 37, Eqs. (4.8)-(4.11): the represented spontaneous generalized-force fluctuation is related to the dissipative resistance over an inhabited positive-frequency sector. The selected mean-square convention and quantum oscillator factor remain explicit paper-local semantics.
  • checked statementCallen and Welton's raw spectral-sum route realizes a source-sensitive structural explanation without consuming the packaged generalized relation.
  • checked statementCallen-Welton 1951, pp. 35-37: the perturbative dissipation calculation, zero-force equilibrium fluctuation calculation, and common-spectral-sum relation directly realize the shared structural explanation. The packaged generalized relation is reconstructed from these source stages rather than accepted as a theorem premise.
  • checked statement
  • checked statement
  • checked statement
  • checked 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 is the full coordinate-transition sum in a positive energy band, not the force-noise variance: the impedance and Q-dot conversion remain separate calculations. The thermal factor stays inside the band integral.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementThe actual relation route retains the original Boltzmann transition ratio, distinct spectral sum and difference, zero point, and classical scope.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementA corollary using the shared canonical kernel. The 1951 source still uses its positive-frequency transition calculation, not a static or imaginary-time derivation of the force-noise readout.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementThe shared result retains Callen and Welton's positive-frequency mean-square generalized-force spectrum. This convention is distinct from the zero-point factor, which their paper separately includes in the quantum prediction. Primary-source anchor: Physical Review p. 37, equations (4.8)-(4.9).
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked 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 noise relation follows by comparing separately identified response and fluctuation integrals, without assuming the relation being derived.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement

Axioms and trust boundaries

  • axiom / trust boundary
  • axiom / trust boundary
  • axiom / trust boundary
  • axiom / trust boundary

Constructors, projections, and other meaning dependencies

  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • 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
  • recursor
  • constructor
  • constructor
  • recursor
  • recursor
  • constructor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • constructor
  • recursor
  • 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

Every physical statement, dependency, equation-level relation, and epistemic qualifier in this edition is taken only from CallenWelton1951.lean, SourceMap.lean, and Coverage.lean. The Lean module retains equations (4.8)–(4.11) through a value-level readout: the positive-frequency 2/π integral, the explicit oscillator factor ℏω/2 + ℏω/(exp(ℏω/kT) − 1), its high-temperature approximation to kT, and the resulting classical integral. The approximation remains a relation, not an exact equality. The source map projects this selected formula package only after the established generalized relation has been checked. Implication-shaped calculation contracts are independent hypotheses; only their result steps inherit the exact earlier outputs they consume.

01

Driven dissipation and zero-force equilibrium noise are calculated separately before their spectra are identified

The formal logic does not assume fluctuation–dissipation as a single primitive law. One route perturbs the system and extracts dissipative response. A second route removes the applied force and computes spontaneous equilibrium fluctuation. A third route compares their spectral sums and establishes the quantum relation and its classical limit. Brownian motion, electromagnetic vacuum noise, acoustic pressure, and the coherence interpretation are downstream applications, not premises of the generalized theorem.

Perturbative dissipation small periodic perturbation · dense levels · transition sums · Boltzmann weights · quadratic power · real impedance
Zero-force equilibrium fluctuation thermal equilibrium · no applied force · spontaneous response matrix sum · conversion to generalized-force noise
Generalized quantum noise–dissipation relation common spectral construct · oscillator mean energy · zero-point contribution · classical/Nyquist limit
Brownian specializationviscous friction · force noise · classical limit · high-frequency nonwhite scope
Vacuum-radiation specializationdipole resistance · field noise · isotropic density · zero point + Planck
Acoustic specializationsphere impedance · volume pressure · wall pressure · thermodynamic high-frequency form
Coherence interpretationisolated periodic source · dense-spectrum partner · fluctuation backreaction · lost motion/coherence · energy transfer · future theory
Figure 1. The seven source-mapped routes. Every application depends on the complete generalized relation. The paper’s declared main conclusion is the relation itself, not a conjunction of every application.
Epistemic ledger
TransitionStatusRetained qualification
Periodic perturbation to dissipationquantum transition calculationDense spectrum, matrix sums, Boltzmann weighting, and impedance identification are explicit.
Zero applied force to equilibrium noiseequilibrium matrix calculationSpontaneous fluctuation and response-to-force conversion are separately supplied.
Generalized relationspectral comparisonThe quantum equality is sector-wise; the classical form needs high temperature or low frequency.
Brownian applicationcontrolled frequency scopeClassical white noise is explicitly denied at high frequency.
Vacuum applicationradiation calculationBoth the zero-point and Planck pieces remain in the energy density.
Acoustic applicationcontrolled frequency scopeThe thermodynamic pressure expression is conditional on high frequency.
Coherence and irreversibilityinterpretation + open obligationThe two-system backreaction chain is retained; the broad theory of irreversible processes is future work.
02

A weak periodic perturbation turns transition probabilities into a real dissipative impedance

The general system is valid in the selected equilibrium regime. The chosen generalized force is conjugate to a selected extensive thermodynamic coordinate. A small periodic perturbation at a selected frequency belonging to the declared spectral sector then couples that force to its response, and the unperturbed Hamiltonian has densely distributed energy levels. These clauses form the dissipation setup.

The supplied perturbative calculation computes the transition matrix- element sum, applies Boltzmann weights, relates upward and downward transitions, and obtains power quadratic in the perturbation. It defines impedance from the force and response and identifies the dissipation value with the real part of that impedance. The system is then linear dissipative, and its dissipation value represents the physical dissipation at every selected frequency.

small periodic force–response perturbation + dense spectrum
→ transition sums + Boltzmann detailed weighting → quadratic dissipated power
→ impedance Z(ω) → represented dissipation D(ω) = real part of Z(ω). the driven linear-response route (1)
F=-i V0; U=F/Zimp; V(t)=Re(F exp(i omega t)); u(t)=Re(U exp(i omega t)).
V(t)=V0 sin(omega t); omega>0 and Zimp!=0.
P_cycle=integral_0^(2*pi/omega) V(t) u(t) dt / (2*pi/omega).
P_cycle=V0^2 Re(Zimp)/(2 |Zimp|^2). The actual period average derives (2.13); peak amplitude is not RMS amplitude. the_actual_period_average_derives_equation_two_thirteen
Gamma_abs=pi V0^2 C_forward/(2 hbar).
Gamma_emit=pi V0^2 C_backward/(2 hbar).
Gamma_emit=exp(-hbar*omega/(kT)) Gamma_abs.
P_abs=hbar*omega*(Gamma_abs-Gamma_emit)=pi V0^2 omega Cminus/2.
P_cycle=P_abs and V0!=0 imply Re(Zimp)=pi omega |Zimp|^2 Cminus. The dense-spectrum, golden-rule power correspondence remains a physical input; the coefficient comparison is checked. a_nonzero_drive_compares_quantum_absorption_with_actual_cycle_power
Force phasor i and velocity phasor 1 have zero average power, although |i|^2=1.
Force and velocity phasors both 1 have average power 1/2, not 1.
Dissipation uses the in-phase response and the peak-amplitude cycle coefficient. Actual periodic waves distinguish reactive impedance from dissipation and peak from RMS conventions. a_reactive_periodic_response_has_no_in_phase_dissipation
Two-level Gibbs weights are (2/3,1/3); hbar=kT=1; omega=log(2).
R0=3/(pi log(2)); choose Zimp=2R0 and V0=0.
P_cycle=P_abs=0, but N=36/pi^2 while (2/pi) Re(Zimp) E=18/pi^2. This finite canonical response control explains why extracting resistance requires a nonzero probe. It is not a continuum golden-rule realization. zero_drive_power_balance_does_not_determine_the_noise_resistance_relation
Perturbative dissipation theoremLean checked from supplied calculation

The setup and transition calculation establish every matrix-sum, weighting, power, impedance, linearity, and represented-dissipation clause. The setup separately projects the extensive coordinate and conjugate-force premise.

dissipation_setup_retains_extensive_coordinate_and_conjugate_force · quantum_transition_calculation_establishes_linear_dissipation · established_dissipation_retains_extensive_coordinate_and_conjugate_force · Physical Review pp. 34–36

generalized_force_label_does_not_supply_extensive_conjugacy blocks the name-only shortcut from a generalized-force label to Callen and Welton's extensive/intensive thermodynamic pairing.

Value-level countermodel boundary

The thermodynamic-force witness retains a selected generalized force, an explicit extensive-coordinate count, an extensive variation, and a work increment; the force can be selected while the coordinate and conjugacy equation are absent. The generalized-Nyquist formula witness separately retains positive frequency, temperature, reduced Planck and Boltzmann constants, and nonnegative dissipation while falsifying the oscillator factor. The blocked shortcuts are physical non-implications, not feature labels.

03

With the applied force removed, the same equilibrium system exhibits spontaneous generalized-force noise

The fluctuation setup retains the complete perturbative-dissipation result, places the system in thermal equilibrium at the selected temperature, removes the applied generalized force, and states that the chosen force is the system’s generalized force.

Its calculation establishes spontaneous equilibrium fluctuation, computes a response-fluctuation matrix sum, converts that response fluctuation through the impedance into force noise, and supplies a represented positive-frequency mean-square spectral value for every frequency in the selected sector.

established linear dissipation + thermal equilibrium + zero applied force
→ spontaneous response fluctuation → equilibrium matrix sum → represented generalized-force noise N(ω). an independent zero-force calculation, not the driven power result reused by name (2)
Qdot_ij=(i/hbar)(E_i-E_j) Q_ij is the derivative of Q_ij(t) at t=0.
Energy-diagonal entries have Qdot_ii=0.
At gap hbar*omega, each ordered Qdot spectrum equals omega^2 times its Q spectrum.
For a finite positive-gap integral: integral f(Delta) dDelta=hbar integral f(hbar*omega) domega. The velocity square and the change of reference measure are separate, checked factors in (3.1)-(3.6). velocity_squares_and_the_energy_gap_jacobian_give_the_original_noise_prefactor
Equilibrium fluctuation theoremLean checked from supplied matrix sum

The zero-force setup and calculation establish spontaneous fluctuation, response-noise conversion, and represented noise across the frequency sector.

zero_force_matrix_sum_establishes_spontaneous_force_noise · Physical Review p. 36
04

The generalized relation identifies the common spectral sum and keeps the zero-point term

The comparison calculation receives both complete results. Its value-level readout keeps the paper's printed oscillator factor rather than merely naming a quantum-noise function. At every positive selected frequency, the first term is the zero-point contribution and the second is the Planck occupation contribution. The same readout then records the positive-frequency resistance-times-energy integral for the mean-square generalized force.

F(ω,T) = ℏω/2 + ℏω/(exp(ℏω/kT) − 1)
⟨V2⟩ = (2/π) ∫0∞ R(ω) F(ω,T) dω
and the positive-frequency spectrum is (2/π) R(ω) F(ω,T). equations (4.8)–(4.9), retained as value-level propositions (3)
The readout uses an actual measure mu; pushforward by omega is Lebesgue measure on (0,infinity).
N_total=integral N(omega) domega; N_classical_total=integral (2/pi) R(omega) kT domega.
N, R*E, and R are integrable in the finite readout.
N_total=(2/pi) integral R(omega) E(omega) domega is derived from the pointwise relation. The main route retains the angular reference and finite measured integral, not an arbitrary integration function. canonical_source_calculations_derive_the_actual_spectral_formula

The pointwise theorem separate_power_and_noise_readouts_derive_the_quantum_relation needs no frequency-integral convergence assumption. Equations for a real mean-square readout are additional finite-domain conclusions. The later radiation discussion of an infinite zero-point contribution is not thereby reinterpreted as a finite observable. The final finite formula package retains both its physical readout domain and its positive-frequency scope.

The selected spectral realization now computes its populations and transition weights. HasCanonicalTransitionRepresentation binds the readout to a normalized ensemble, actual complex matrix elements, a common energy gap, and a convergent transition integral. Identifying that measure with the source's density-of-states integral remains an explicit spectral-representation input.

Z = integral exp(-beta E(s)) dmu(s).
p(s) = exp(-beta E(s))/Z; integral p(s) dmu(s) = 1.
Integrable Boltzmann weight; Z > 0; beta = 1/(kT) > 0. generalized_relation_retains_normalized_canonical_law; the base measure counts states or supplies their density
All frequency slices share E_n, beta, and Q_ij.
Q_ij(t) = exp(i(E_i-E_j)t/hbar) Q_ij.
The selected hbar and k match the generalized-Nyquist readout. OriginalFixedHamiltonianRepresentationAt and generalized_noise_line_has_the_original_hamiltonian_time_phase; the energy-basis interpretation remains explicit
Same H and p=(2/3,1/3), Q=sigma_x: F_positive=2/3, F_negative=1/3.
Replacing Q by 2Q only on the negative slice gives F_negative=4/3.
Its local thermal FDT still holds, but the original fixed-Q line matching fails. pointwise_thermal_fdt_does_not_fix_opposite_observable_lines; fixed data and physical spectral resolution are separate requirements
At the selected positive gap Delta=hbar*omega, C_full=K_beta(Delta) J!=0.
K_beta(Delta)=(1-exp(-beta Delta))/Delta; C_full=f at nonzero gap.
This shared-kernel corollary does not extend the force-noise formula to zero gap. positive_frequency_noise_retains_nonvacuous_canonical_response; a derived corollary, not an imaginary-time argument attributed to the 1951 source
E=(0,log(2)), beta=1, Q=sigma_x: the positive spectral atom has mass 2/3.
An ordinary integrable energy-gap density gives every singleton mass zero.
The finite line cannot itself realize the source's continuous density-of-states model. active_positive_line_is_not_an_ordinary_energy_density; no obstruction to a separately justified continuum or coarse-grained limit is asserted
For every measurable band B inside W: F_resolved(B)=F_canonical(B) and B_resolved(B)=B_canonical(B).
Canonical weights integrate p_i Q_ij Q_ji and p_j Q_ij Q_ji over E_j-E_i in B.
Both kernels are integrable; the resulting complex spectral measures agree on W.
The source J uses an energy-gap reference: dDelta=hbar*domega. OriginalCanonicalBandRepresentationAt and generalized_relation_reconstructs_both_coordinate_spectral_measures; reconstruction is an explicit source input, not a spectral-theorem proof
B lies in the positive energy window W.
Cplus_canonical(B) = 2 integral_{Delta in B} E_beta(Delta) f(Delta) dnu.
The energy factor stays inside the integral; the weighted integrand is integrable.
This is coordinate spectral weight, not the force-noise variance. generalized_coordinate_band_has_the_full_transition_sum; impedance, Q-dot, and Jacobian readouts remain separate
Fixed H, beta, Q=sigma_x: canonical total forward weight=1.
Replacing only the reference measure nu by 2nu gives total forward weight=2.
Every local nonzero-gap FDT survives; canonical band reconstruction fails. fixed_system_local_fdt_does_not_fix_spectral_multiplicity; a finite line control, not the continuous energy-density source model
Delta = E(final)-E(initial) = hbar omega > 0 almost everywhere.
J = integral p(initial)|Q_initial,final|^2 dnu.
r = exp(-beta Delta); Cminus = (1-r)J; Cplus = (1+r)J.
Hermiticity and integrability are explicit; J > 0 selects an active frequency. canonical_transitions_derive_original_detailed_balance_and_sums; (2.8), (4.3)-(4.5)
R = pi omega |Zimp|^2 Cminus.
N = |Zimp|^2 hbar omega^2 Cplus. HasOriginalMatrixElementReadouts; selected (4.6)-(4.7) readouts derived from cycle-power correspondence and the independent Q-dot spectrum
N = (2/pi) R E_beta(Delta).
E_beta(Delta) = Delta/2 + Delta/(exp(beta Delta)-1).
Classical comparison is separate, not exact at finite gap. original_matrix_element_readouts_derive_quantum_noise_relation; the quantum equality is derived, not assumed in these inputs
Two-level Gibbs probabilities: (2/3, 1/3); Delta = log(2).
For Q = sigma_x: Cplus = 1, but the symmetrized half-sum is 1/2.
This finite control is not a dense-spectrum golden-rule realization. full_transition_sum_is_not_the_symmetrized_half_sum; the convention distinction is an actual spectral counterexample

A second output keeps the approximation step distinct. In the high-temperature or low-frequency regime, the oscillator factor is related approximately to kT; only then does the classical generalized-Nyquist integral follow, and the electrical specialization recovers Nyquist’s result.

kT ≫ ℏω ⇒ F(ω,T) ∼ kT
⟨V2⟩classical = (2/π) kT ∫0∞ R(ω) dω
and the electrical specialization is Nyquist’s relation. equations (4.10)–(4.11); approximation, not the general quantum statement (4)
tau=kT>0; Delta=hbar*omega>0; E=tau plus a controlled quantum correction.
|E-tau| <= Delta/2.
Delta <= 2 epsilon tau and R>=0 imply |N-N_classical| <= epsilon N_classical. A conservative error estimate is derived from the exponential formula. It is not an exact classical equality or an error formula printed in the original paper. a_selected_small_quantum_gap_controls_the_classical_spectral_error
epsilon>=0; almost everywhere with R(omega)!=0, hbar*omega <= 2 epsilon kT.
Together with finite integrals, |N_total-N_classical_total| <= epsilon N_classical_total.
The exact quantum route does not require this classical regime. The whole response band must be controlled; one selected frequency is insufficient for the integrated comparison. generalized_relation_retains_the_controlled_integrated_classical_error
A finite bin with kT=1, hbar*omega=log(2), R=pi has N_total=3 log(2) and N_classical_total=2.
It satisfies the epsilon=1/2 comparison but these two values are unequal.
At kT=1/2 the quantum formula still holds, while the same selected classical criterion fails.
The bin uses a Dirac measure; it is not Lebesgue angular-frequency measure. The oscillator factor and both integrals are computed, rather than assigning unrelated quantum and classical values. a_controlled_classical_approximation_is_not_an_exact_quantum_equality
Two finite bins have kT=hbar=R=1 and frequencies log(2), 8 log(2).
The first bin satisfies the epsilon=1/2 small-gap condition.
The actual summed noise violates the epsilon=1/2 integrated classical bound. Both bins have finite, computed quantum spectra; the failure comes from the uncontrolled high-frequency contribution. one_low_selected_frequency_does_not_control_the_integrated_classical_error
On the actual positive angular-frequency continuum, take hbar=kT=R=1.
N(omega)=(2/pi) E(omega) satisfies the pointwise quantum relation.
This N is not integrable: the relation alone does not define a finite total force variance. A totalized Lean integral at a divergent spectrum is not treated as an observed zero variance. a_pointwise_quantum_relation_does_not_make_the_continuum_noise_integrable
Generalized quantum noise–dissipation theoremLean-checked spectral comparison

The established absorption and fluctuation predecessors are consumed to derive the quantum equality. The comparison input no longer supplies the final noise formula. The attached package retains the actual angular measure, finite equations (4.8)-(4.9), and the conditional error bounds interpreting (4.10)-(4.11).

common_spectral_sums_establish_generalized_quantum_noise_relation · Physical Review pp. 36–37
Printed formula retentionLean-checked projection and countermodel

The established generalized relation projects the selected formula package and therefore the printed equations. A finite countermodel keeps a named generalized-relation output true while falsifying the oscillator formula, so the name alone cannot discharge the source equations.

generalized_relation_retains_printed_equations_four_eight_through_four_eleven · named_generalized_relation_does_not_supply_printed_nyquist_formula

Response and classical-limit boundaries

These are constructed controls. Finite Gibbs slices and bins do not stand in for the source's dense-spectrum dynamics; the prescribed continuum readout tests integrability rather than a microscopic reservoir model.

Retained contentRejected inference
Canonical fluctuations and zero driven powerA determined noise-resistance relation without a nonzero probe
Nonzero reactive impedanceIts modulus is dissipative resistance
Actual sinusoidal cycle averagePeak and RMS power coefficients agree
Exact finite quantum formulaA selected classical regime is necessary
Controlled classical approximationQuantum and classical noise are exactly equal
Computed oscillator energy in that regimeExact equipartition at nonzero gap
Finite spectral-bin formulaThe reference is continuous angular Lebesgue measure
One small selected gapA bound on the integrated noise error
Exact continuum pointwise relationA finite total force variance
05

Viscous drag gives Brownian force noise, but the classical white spectrum has a frequency boundary

The Brownian system is valid and in equilibrium, with viscous drag characterized by a selected friction value. Its calculation identifies that friction with dissipation, calculates Brownian force noise, and recovers the classical Brownian relation under the same high-temperature or low-frequency condition.

generalized relation + viscous friction η → Brownian force-noise spectrum,
high T or low ω → classical Brownian relation,
high ω → classical white-noise spectrum is not valid. the controlled qualification is part of the theorem output (5)
Qualified Brownian-noise theoremcontrolled frequency scope

For every selected frequency, the theorem retains calculated Brownian noise, conditional classical recovery, and the high-frequency failure of the white-spectrum description.

viscous_drag_implies_qualified_brownian_force_noise · Physical Review p. 37
06

Dipole radiation resistance turns the generalized relation into vacuum electric-field fluctuations

The electromagnetic application selects a valid electric dipole that radiates in the equilibrium regime. Its calculation obtains the dipole radiation resistance, computes the vacuum electric-field fluctuation, identifies field noise with generalized-force noise, and constructs the isotropic field energy density.

generalized relation + radiating electric dipole → radiation resistance → vacuum electric-field noise
→ isotropic field energy density = zero-point contribution + Planck contribution. both pieces are retained by the formal result (6)
Vacuum-radiation theoremLean checked from impedance calculation

At every selected frequency, the theorem retains the field fluctuation, isotropic energy density, zero-point term, and Planck term. Radiation resistance and the field-to-force bridge remain explicit outputs of the underlying calculation.

radiation_resistance_yields_vacuum_field_and_planck_spectrum · Physical Review p. 38
07

Acoustic impedance yields distinct volume and wall pressure fluctuations

The acoustic system is a valid oscillating sphere radiating into a gas. Its calculation obtains acoustic radiation impedance, volume pressure fluctuation, agreement with a direct acoustic-mode calculation, wall radiation resistance, and wall pressure fluctuation. The wall variance is twice the volume variance; at high frequency, the volume pressure can also be expressed through the selected thermodynamic quantity.

generalized relation + acoustic radiation from a sphere
→ volume pressure noise = direct mode result,
wall pressure noise = 2 × volume pressure noise,
high ω → thermodynamic pressure expression. the factor two and the high-frequency condition are separate outputs (7)
Acoustic pressure-noise theoremcontrolled high-frequency scope

For every selected frequency, the theorem retains the volume calculation, direct-mode agreement, wall calculation, factor of two, and conditional thermodynamic expression.

acoustic_impedance_yields_volume_wall_and_thermodynamic_pressure_noise · Physical Review pp. 38–39
08

Loss of coherence is an interpretation of dissipation, while the broad irreversible theory remains future work

The interpretive route keeps two systems distinct. The source is initially isolated from the generalized dissipative system, has internal energy, is simple and periodic, and has internal coherence. It supplies the selected periodic force to the same dense-spectrum system already established by the generalized relation, and is later coupled to it. The supplied calculation says that equilibrium fluctuations of the dissipative system act back on the source, destroy periodic motion and coherence, transfer energy away, randomize the remaining source energy to equilibrium, and support the paper's macroscopic interpretation of dissipation as fluctuation-induced loss of coherence.

The separate future-theory assessment denies that the broad theory of irreversible processes is completed in the paper and affirms that it is proposed for later work. The packaged theorem retains the entire two-system chain and both scope clauses; a separate projection theorem exposes the initial source conditions, dense-spectrum partner, force supply, coupling, fluctuation backreaction, loss of motion and coherence, energy transfer, randomization, interpretation, and open future program.

isolated energetic periodic coherent source
+ selected force supplied to dense-spectrum dissipative system + later coupling
→ equilibrium fluctuations act back → periodic motion and coherence lost + energy transferred and randomized
→ dissipation interpreted as fluctuation-induced loss of coherence,
while general irreversible theory is not completed and is proposed for future work. interpretation plus explicit open obligation (8)
Coherence-interpretation and scope theoreminterpretation + future program

The generalized relation, coherent periodic-source setup, dense-spectrum coupling, interpretation calculation, and future assessment establish the scoped result; the projection theorem verifies that none of the two-system backreaction clauses disappears inside the package.

coherent_periodic_source_coupling_establishes_fluctuation_backreaction_interpretation · coherence_interpretation_does_not_complete_future_irreversibility_theory · complete_interpretation_retains_two_system_backreaction_and_open_scope · Physical Review pp. 39–40
09

The generalized relation realizes a reusable equilibrium noise–dissipation pattern

The module maps its general system, equilibrium regime, temperature, force, frequency sector, dissipation values, and noise values into a shared framework. The paper-local dissipation, fluctuation, and relation results serve as the three calculations required by that shared model. The selected driving frequency witnesses that the shared sector is nonempty.

Paper-local realization of shared equilibrium noise
Shared requirementCallen–Welton realization
Valid linear dissipative equilibrium systemPerturbative transition calculation and real impedance
Spontaneous generalized-force noiseZero-applied-force equilibrium fluctuation calculation
Represented dissipation and noise valuesSector-wise readout predicates from the two calculations
Selected noise conventionPositive-frequency mean-square generalized-force spectrum
Noise predicted from dissipationThe generalized quantum equality at every selected frequency

The established generalized relation directly realizes the shared output: inhabited setup, completed calculations, represented dissipation and noise readouts, the positive-frequency convention, and the sector-wide quantum relation. The implication-valued route remains separately reconstructible. Grounding identifies generalized quantum noise theory as the theory and the selected equilibrium generalized system as the represented world. The grounding uses only the dissipation setup, equilibrium, linearity, absence of applied force, generalized-force status, spontaneous fluctuation, and an inhabited selected sector, with no calculation or noise-dissipation output. Every shared claim then transfers both to theory entailment and to truth in that world.

Source-input structural explanationstaged pre-endpoint route

The perturbative dissipation calculation, zero-force equilibrium fluctuation calculation, and common-spectral-sum relation are executed in source order. The source-sensitive theorem retains the typed transitionAndEquilibriumSpectralSums derivation before the applicable shared route explains the represented positive-frequency force-noise relation.

callen_welton_raw_source_inputs_make_shared_noise_dissipation_route_applicable · callen_welton_source_inputs_realize_source_structural_noise_dissipation_explanation · Physical Review pp. 35–37
Grounded shared noise–dissipation theoremsemantic transport

The paper-local generalized relation establishes and grounds the shared result, retaining the positive-frequency mean-square force-spectrum convention, after which every shared claim transfers to theory and world predicates.

shared_relation_retains_positive_frequency_mean_square_force_spectrum · callen_welton_route_establishes_theory_model_grounded_noise_dissipation · grounded_callen_welton_relation_transfers_every_shared_claim
Reader aids and formal audit
A

Concept guide

Terms linked throughout the article resolve to these paper-local definitions and results.

Perturbative dissipation

Linear dissipative response obtained from weak periodic driving, transition sums, Boltzmann weighting, and the real part of impedance.

EstablishedPerturbativeDissipation

Generalized impedance

The force–response quantity whose real part represents the selected system’s dissipation value.

dissipationValueIsRealImpedancePartAt

Equilibrium force noise

Spontaneous generalized-force fluctuation calculated with no applied force and represented spectrally.

EstablishedEquilibriumFluctuation

Generalized noise–dissipation relation

The sector-wise equality of equilibrium noise with the quantum prediction from represented dissipation.

EstablishedGeneralizedNoiseDissipation

Zero-point contribution

The quantum mean-energy component retained in the general relation and in the vacuum field energy density.

zeroPointContributionIncludedAt

Classical/Nyquist limit

The high-temperature or low-frequency specialization equating noise to the classical dissipation prediction.

highTemperatureOrLowFrequencyAt

Qualified Brownian noise

Viscous-force noise with classical recovery in its limit and explicit failure of the classical white spectrum at high frequency.

BrownianApplicationCalculation

Vacuum electric-field noise

Dipole-radiation specialization producing an isotropic field energy density with zero-point and Planck terms.

VacuumRadiationCalculation

Planck contribution

The thermal-radiation term retained alongside the vacuum zero-point contribution.

vacuumEnergyDensityContainsPlanckTermAt

Acoustic pressure noise

Volume and rigid-wall pressure fluctuations obtained from acoustic radiation impedance.

AcousticApplicationCalculation

Wall factor of two

The result that the selected wall pressure variance is twice the volume pressure variance.

wallPressureIsTwiceVolumePressureAt

Fluctuation-induced loss of coherence

The two-system interpretation in which an initially isolated periodic source couples to the dense-spectrum dissipative system, receives equilibrium-fluctuation backreaction, loses motion and coherence, and transfers and randomizes energy.

CoherentPeriodicSourceSetup · SourceDissipativeCouplingSetup · CoherenceInterpretationCalculation

Future irreversible theory

The broader theory of linear irreversible processes proposed for later work and explicitly not completed here.

FutureTheoryAssessment

Shared equilibrium-noise model

The reusable pattern connecting represented dissipation, spontaneous equilibrium noise, and a calculation predicting noise from dissipation.

equilibriumNoiseDissipationModel
B

Route inventory and formal provenance

The source map declares seven routes and twenty-four semantic claims. Coverage interprets every atom through the paper-local generalized-noise framework and certifies every route from its explicit calculations. Local equilibrium, application, and source-coupling inputs remain local; certified dissipation or generalized-relation outputs are recombined with them only when the corresponding result theorem is applied.

Complete route inventory
RouteDirect dependenciesPrincipal outputsProfile
Perturbative dissipation—Linear response, impedance, represented dissipationquantum transition calculation
Equilibrium fluctuationDissipationSpontaneous represented force noisezero-force matrix calculation
Generalized relationEquilibrium fluctuationQuantum relation, selected equations (4.8)-(4.11) package, classical limit, shared resultspectral comparison
Brownian motionGeneralized relationForce noise, classical limit, high-frequency failurecontrolled scope
Vacuum radiationGeneralized relationField noise, isotropic density, zero-point and Planck termsradiation calculation
Acoustic pressureGeneralized relationVolume/wall noise, factor two, thermodynamic formcontrolled scope
Interpretation and scopeGeneralized relationDecoherence interpretation and future programinterpretive + open
Dissipation route · perturbative_dissipation_route_is_semantically_realized
Independently certifies the weak-driving setup, transition calculation, real impedance, linearity, and represented dissipation.
Fluctuation route · equilibrium_fluctuation_route_is_semantically_realized
Consumes dissipation and certifies thermal zero-force setup, spontaneous fluctuation, matrix sum, conversion, and represented noise.
Generalized route · generalized_noise_dissipation_route_is_semantically_realized
Recovers actual dissipation and fluctuation claims from the predecessor proofs, derives the quantum relation, and retains its measured finite-integral formula. The classical comparison is conditional and quantitative; source certificates establish availability, not physical content.
Brownian route · brownian_motion_route_is_semantically_realized
Consumes the complete relation chain and certifies the viscous specialization with its high-frequency qualification.
Vacuum route · vacuum_radiation_route_is_semantically_realized
Consumes the complete relation chain and certifies dipole radiation resistance, field noise, and both energy-density components.
Acoustic route · acoustic_pressure_route_is_semantically_realized
Consumes the complete relation chain and certifies volume and wall pressure noise, direct-mode agreement, factor two, and conditional thermodynamic expression.
Interpretation route · interpretation_scope_route_is_semantically_realized
Consumes the complete relation chain and certifies an initially isolated periodic source, force supply to the dense-spectrum partner, later coupling, fluctuation backreaction, lost motion and coherence, energy transfer and randomization, and the unfinished future program.

Exhaustive coverage and inherited status

all_routes_are_semantically_realizable constructs all seven certificates from raw paper-local inputs, while route_semantic_realization_is_exhaustive projects an arbitrary declared route. Source-map audits preserve the exact route graph, independent calculation contracts, local setup scope, the checked formula projection in relation_route_exposes_selected_nyquist_formula_package, and certified predecessor consumption. They also preserve controlled high-frequency scope in both Brownian and acoustic results, open-obligation status in the future-theory assessment, and interpretive rather than deductive status for the final two-system conclusion.

Lean-encoded bibliographic record

H. B. Callen and T. A. Welton, Irreversibility and Generalized Noise, Physical Review 83 (1951), 34–40. All page locators above are stored in SourceMap.lean.

Original source-valued quantum noise, applications, and scope

The earlier scalar readout fixture, distinct from the normalized two-level transition model above, sets hbar=k=T=1, omega=log(2), and resistance pi. Its upper/lower-population Boltzmann ratio is 1/2; the dissipative difference is C_-=1, the fluctuation sum is C_+=3, and C_+/C_-=3. The separate zero-point and Planck energies are log(2)/2 and log(2), giving oscillator energy 3log(2)/2, quantum force spectrum 3log(2), and classical prediction 2. The classical regime log(2)<1 is inhabited, but its bounded approximation is not an exact equality.

Viscous friction eta=3 produces distinct Brownian spectra 9log(2)/pi and 10log(2)/pi rather than high-frequency white noise. Electric dipole data e=2, c=2, omega=2 give radiation resistance 4/3 and isotropic density 3=1+2, with separate zero-point and Planck terms. Acoustic volume pressure 3/(2pi^2) and wall pressure 3/pi^2 differ by exactly two; the rigid wall has a velocity node and the independent adiabatic sound relation gives c^2=4.

The initially isolated source and dissipative system are distinct. Their later coupling erases source periodicity and coherence while respecting energy balance 10=2+8; zero completed and one proposed general irreversibility theory retain the original open scope. These reconstructed physical instances, the transition-sum control, the fixed-coordinate frequency control, and the atomic-density distinction are protected by 38 physically inhabited Callen-Welton boundaries.

TraceComplete Lean semantic identifier ledger

Reading note. The article above is the human exposition. This collapsed cross-reference records every public theorem and every constructor of the five paper-local source-map vocabularies. It introduces no additional claim; its purpose is to make semantic omissions mechanically detectable.

Primary semantic theorems (136)

the_thermal_occupation_is_positive_and_bounded_by_equipartitionthe_exact_quantum_energy_has_a_controlled_classical_errora_small_quantum_to_thermal_ratio_gives_a_relative_error_boundthe_energy_factor_is_the_existing_canonical_spectral_factorthe_cycle_mean_is_the_actual_in_phase_powercomplex_impedance_separates_dissipation_from_reactancecomplex_force_response_gives_the_original_peak_amplitude_coefficientthe_force_has_the_original_sinusoidal_time_dependencepositive_frequency_has_a_positive_periodthe_time_average_equals_the_phase_cycle_averagethe_actual_period_average_derives_equation_two_thirteenabsorption_and_emission_rates_have_the_actual_canonical_ratiorate_difference_and_energy_transfer_derive_quadratic_absorptiona_nonzero_drive_compares_quantum_absorption_with_actual_cycle_powerthe_original_matrix_prefactors_derive_quantum_force_noisecanonical_absorption_is_passive_even_when_a_selected_matrix_element_vanishesthe_heisenberg_coordinate_derivative_is_the_commutator_velocityenergy_diagonal_coordinate_entries_have_zero_velocitythe_two_velocity_matrix_elements_supply_the_squared_gapthe_velocity_transition_spectra_are_the_coordinate_spectra_times_frequency_squaredvelocity_squares_and_the_energy_gap_jacobian_give_the_original_noise_prefactora_positive_energy_gap_change_has_the_actual_planck_jacobianthe_spectral_relation_gives_the_finite_original_noise_integralthe_classical_reference_is_an_actual_resistance_integralthe_classical_reference_is_integrablethe_quantum_to_classical_spectral_error_is_controlled_in_the_response_banda_passband_classical_regime_controls_the_actual_integrated_noise_errorthe_angular_reference_integrates_actual_positive_frequenciesthe_calculated_pointwise_spectrum_also_represents_the_measured_spectral_integralthe_calculated_spectrum_and_actual_readout_derive_equations_four_eight_through_four_elevenequation_four_nine_makes_selected_oscillator_energy_positivethe_one_bin_formula_readout_has_actual_finite_integralsthe_one_bin_noise_is_the_calculated_quantum_spectrumoriginal_quantum_nyquist_formula_and_inhabited_classical_regime_are_consistentnamed_generalized_relation_does_not_supply_printed_nyquist_formulathe_two_level_response_has_positive_physical_parametersthe_two_level_response_compares_actual_cycle_power_and_absorbed_energythe_two_level_force_noise_is_computed_and_strictly_positivea_nonzero_canonical_probe_has_the_actual_quantum_noise_relationthe_unprobed_system_has_the_same_canonical_fluctuationszero_drive_power_balance_does_not_determine_the_noise_resistance_relationa_reactive_periodic_response_has_no_in_phase_dissipationpeak_amplitude_and_rms_amplitude_do_not_have_the_same_power_coefficientthe_finite_bin_uses_an_actual_measure_and_computed_quantum_formulathe_exact_quantum_formula_is_valid_outside_the_selected_classical_regimea_controlled_classical_approximation_is_not_an_exact_quantum_equalitythe_computed_oscillator_energy_is_not_exactly_classical_in_the_comparison_regimea_finite_spectral_bin_is_not_the_original_continuum_frequency_measurethe_two_frequency_bins_have_finite_actual_quantum_noisethe_two_bin_means_are_the_sums_of_their_actual_spectral_weightsone_low_selected_frequency_does_not_control_the_integrated_classical_errorthe_unfiltered_continuum_has_the_actual_angular_measure_and_pointwise_quantum_relationa_pointwise_quantum_relation_does_not_make_the_continuum_noise_integrablecanonical_transitions_derive_original_detailed_balance_and_sumsoriginal_matrix_element_readouts_derive_quantum_noise_relationcanonical_matrix_elements_and_classical_comparison_retain_original_scopeoriginal_boltzmann_difference_sum_zero_point_and_classical_scope_are_inhabitedoriginal_brownian_nonwhite_dipole_planck_and_double_wall_noise_are_inhabitedoriginal_distinct_source_loses_coherence_without_completing_irreversibility_theorydissipation_setup_retains_extensive_coordinate_and_conjugate_forcequantum_transition_calculation_establishes_linear_dissipationestablished_dissipation_retains_extensive_coordinate_and_conjugate_forcezero_force_matrix_sum_establishes_spontaneous_force_noiseestablished_dissipation_supplies_canonical_response_inputsestablished_fluctuation_supplies_the_coordinate_noise_readoutseparate_power_and_noise_readouts_derive_the_quantum_relationcanonical_dissipation_makes_the_measured_resistance_nonnegativethe_oscillator_readout_retains_the_selected_energy_and_zero_pointraw_source_readouts_and_canonical_power_derive_the_selected_spectral_balancecanonical_source_calculations_derive_the_actual_spectral_formulaa_selected_small_quantum_gap_controls_the_classical_spectral_errorcommon_spectral_sums_establish_generalized_quantum_noise_relationgeneralized_relation_retains_selected_nyquist_formula_packagegeneralized_relation_retains_printed_equations_four_eight_through_four_elevengeneralized_relation_exposes_the_actual_angular_frequency_integralgeneralized_relation_retains_the_finite_energy_to_frequency_jacobiangeneralized_relation_retains_the_controlled_integrated_classical_errorgeneralized_relation_retains_original_detailed_balance_and_quantum_noisegeneralized_relation_retains_actual_canonical_transition_noisegeneralized_relation_retains_normalized_canonical_lawpositive_frequency_noise_retains_nonvacuous_canonical_responsegeneralized_relation_retains_one_hamiltonian_and_coordinategeneralized_relation_reconstructs_both_coordinate_spectral_measuresgeneralized_coordinate_band_has_the_full_transition_sumactive_coordinate_band_has_nonzero_canonical_weightgeneralized_noise_line_has_the_original_hamiltonian_time_phaseviscous_drag_implies_qualified_brownian_force_noisebrownian_route_retains_original_friction_and_nonwhite_quantum_spectrumradiation_resistance_yields_vacuum_field_and_planck_spectrumvacuum_route_retains_original_dipole_resistance_and_split_energy_densityacoustic_impedance_yields_volume_wall_and_thermodynamic_pressure_noiseacoustic_route_retains_original_double_wall_noise_and_adiabatic_soundcoherent_periodic_source_coupling_establishes_fluctuation_backreaction_interpretationcoherence_interpretation_does_not_complete_future_irreversibility_theorycomplete_interpretation_retains_two_system_backreaction_and_open_scopecoherence_route_retains_original_two_system_transfer_and_open_programequilibrium_noise_dissipation_model_retains_exact_paper_semanticscallen_welton_inputs_make_shared_noise_dissipation_route_applicablecallen_welton_raw_source_inputs_make_shared_noise_dissipation_route_applicablecallen_welton_source_inputs_realize_structural_noise_dissipation_explanationcallen_welton_source_inputs_realize_source_structural_noise_dissipation_explanationcallen_welton_relation_realizes_shared_noise_dissipationcallen_welton_relation_realizes_structural_noise_dissipation_explanationcallen_welton_route_exhibits_nonvacuous_shared_noise_dissipationshared_relation_retains_positive_frequency_mean_square_force_spectrumcallen_welton_inputs_establish_theory_model_groundingcallen_welton_route_establishes_theory_model_grounded_noise_dissipationgrounded_callen_welton_relation_transfers_every_shared_claimgeneralized_force_label_does_not_supply_extensive_conjugacypositive_temperature_does_not_fix_the_boltzmann_transition_ratiodetailed_balance_does_not_supply_the_dissipative_transition_differencedissipative_transition_difference_does_not_supply_fluctuation_sumfluctuation_transition_sum_does_not_supply_boltzmann_detailed_balancecorrect_spectral_sums_do_not_supply_the_zero_point_energypositive_zero_point_energy_does_not_supply_the_planck_occupation_termpositive_planck_occupation_does_not_supply_the_zero_point_termpositive_resistance_does_not_supply_the_quantum_noise_spectrumexact_quantum_noise_does_not_imply_the_classical_noise_valuelow_frequency_regime_does_not_make_the_quantum_oscillator_exactly_classicalpositive_friction_does_not_supply_the_brownian_force_spectrumcorrect_low_frequency_brownian_noise_does_not_make_high_frequency_noise_whitebrownian_force_noise_does_not_supply_electric_dipole_radiation_resistancedipole_radiation_resistance_does_not_supply_electric_field_varianceelectric_field_variance_does_not_supply_the_isotropic_energy_densityvacuum_zero_point_density_does_not_supply_the_planck_densityvacuum_planck_density_does_not_supply_the_zero_point_densitypositive_volume_pressure_does_not_supply_the_doubled_wall_pressuredoubled_wall_pressure_does_not_supply_the_rigid_wall_velocity_nodea_rigid_wall_velocity_node_does_not_supply_the_adiabatic_sound_formuladistinct_source_and_dissipative_systems_do_not_imply_initial_isolationinitial_source_coherence_does_not_supply_later_system_couplinglater_system_coupling_does_not_supply_equilibrium_fluctuation_backreactionfluctuation_backreaction_does_not_by_itself_erase_source_coherenceloss_of_source_coherence_does_not_supply_the_energy_transfer_balancetransferred_source_energy_does_not_supply_a_positive_thermal_remaindera_proposed_future_irreversibility_program_is_not_a_completed_theory

Coverage theorems (11)

every_source_claim_has_semanticsgeneralized_relation_atom_retains_selected_nyquist_formula_packageperturbative_dissipation_route_is_semantically_realizedequilibrium_fluctuation_route_is_semantically_realizedgeneralized_noise_dissipation_route_is_semantically_realizedbrownian_motion_route_is_semantically_realizedvacuum_radiation_route_is_semantically_realizedacoustic_pressure_route_is_semantically_realizedinterpretation_scope_route_is_semantically_realizedall_routes_are_semantically_realizableroute_semantic_realization_is_exhaustive

Source-map audit theorems (14)

argument_wellFormedargument_auditableroutes_wellFormedroutes_have_exact_predecessor_graphcalculation_contracts_are_independent_hypotheseslocal_setup_and_scope_inputs_are_independent_hypothesescentral_result_steps_apply_selected_inputs_and_contractsrelation_route_exposes_selected_nyquist_formula_packageapplication_and_interpretation_results_apply_selected_inputsdependent_routes_consume_certified_predecessor_outputsbrownian_route_retains_controlled_high_frequency_scopeacoustic_route_retains_controlled_high_frequency_scopefuture_theory_retains_open_obligation_statusinterpretation_result_retains_interpretive_status

Semantic atoms (24)

dissipationSetupperturbativeDissipationCalculationestablishedDissipationequilibriumFluctuationSetupequilibriumFluctuationCalculationestablishedEquilibriumFluctuationgeneralizedRelationCalculationestablishedGeneralizedRelationgeneralizedNyquistFormulaPackagesharedNoiseDissipationbrownianSetupbrownianCalculationbrownianResultvacuumRadiationSetupvacuumRadiationCalculationvacuumRadiationResultacousticSetupacousticCalculationacousticResultcoherentSourcesourceDissipativeCouplingcoherenceInterpretationCalculationfutureTheoryAssessmentinterpretationAndScopeResult

Claim identifiers (24)

dissipationSetupdissipationCalculationdissipationResultfluctuationSetupfluctuationCalculationfluctuationResultrelationCalculationrelationResultrelationFormulasharedResultbrownianSetupbrownianCalculationbrownianResultvacuumSetupvacuumCalculationvacuumResultacousticSetupacousticCalculationacousticResultcoherentSourcecouplinginterpretationCalculationfutureAssessmentinterpretationResult

Step identifiers (24)

stateDissipationSetupsupplyDissipationCalculationderiveDissipationResultstateFluctuationSetupsupplyFluctuationCalculationderiveFluctuationResultsupplyRelationCalculationderiveRelationResultretainRelationFormulaPackagerealizeSharedResultstateBrownianSetupsupplyBrownianCalculationderiveBrownianResultstateVacuumSetupsupplyVacuumCalculationderiveVacuumResultstateAcousticSetupsupplyAcousticCalculationderiveAcousticResultstateCoherentSourcestateCouplingsupplyInterpretationCalculationstateFutureAssessmentderiveInterpretationResult

Route identifiers (7)

perturbativeDissipationequilibriumFluctuationgeneralizedNoiseDissipationbrownianMotionvacuumRadiationacousticPressureinterpretationScope

Route kinds (7)

quantumTransitionDissipationzeroForceEquilibriumFluctuationgeneralizedQuantumNyquistRelationviscousDragSpecializationdipoleRadiationSpecializationacousticRadiationSpecializationcoherenceInterpretationAndFutureProgram

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.

perturbativeDissipation

Logical kind: quantumTransitionDissipation.

Required predecessor routes: none.

Ordered inference steps: stateDissipationSetup, supplyDissipationCalculation, deriveDissipationResult.

Exported conclusions: dissipationResult.

equilibriumFluctuation

Logical kind: zeroForceEquilibriumFluctuation.

Required predecessor routes: perturbativeDissipation.

Ordered inference steps: stateFluctuationSetup, supplyFluctuationCalculation, deriveFluctuationResult.

Exported conclusions: fluctuationResult.

generalizedNoiseDissipation

Logical kind: generalizedQuantumNyquistRelation.

Required predecessor routes: equilibriumFluctuation.

Ordered inference steps: supplyRelationCalculation, deriveRelationResult, retainRelationFormulaPackage, realizeSharedResult.

Exported conclusions: relationFormula, relationResult, sharedResult.

brownianMotion

Logical kind: viscousDragSpecialization.

Required predecessor routes: generalizedNoiseDissipation.

Ordered inference steps: stateBrownianSetup, supplyBrownianCalculation, deriveBrownianResult.

Exported conclusions: brownianResult.

vacuumRadiation

Logical kind: dipoleRadiationSpecialization.

Required predecessor routes: generalizedNoiseDissipation.

Ordered inference steps: stateVacuumSetup, supplyVacuumCalculation, deriveVacuumResult.

Exported conclusions: vacuumResult.

acousticPressure

Logical kind: acousticRadiationSpecialization.

Required predecessor routes: generalizedNoiseDissipation.

Ordered inference steps: stateAcousticSetup, supplyAcousticCalculation, deriveAcousticResult.

Exported conclusions: acousticResult.

interpretationScope

Logical kind: coherenceInterpretationAndFutureProgram.

Required predecessor routes: generalizedNoiseDissipation.

Ordered inference steps: stateCoherentSource, stateCoupling, supplyInterpretationCalculation, stateFutureAssessment, deriveInterpretationResult.

Exported conclusions: interpretationResult.