Formal reconstruction · entropy-production positivity, thermodynamic insufficiency, chemical detailed balance, microscopic reversibility, ensemble regression, correlation symmetry, anisotropic heat reciprocity, principal heat axes, conditional spiral flow, intermediate-time validity, dissipation potentials, variational principles, stationary flow, magnetic field reversal, Coriolis rotation, and deferred general transport
Reciprocal Relations in Irreversible Processes. I.
Why positivity is not reciprocity, how equilibrium fluctuations produce the anisotropic heat result, and where the proof's regime and scope boundaries lie
Definitions, structures, and assumptions
Structures, classes, and inductive alternatives
- structure
- structureProof-free transport data fixed before the regression and correlation route establishes reciprocity. The kinetic-coefficient family is selected here, but no equality between its entries is stored in the constraint.
- structure
- structureThe selected parity-sensitive coefficient relation. The structure records the objects occurring in the phenomenon but carries no proof of reciprocity.
- structureThe physical transformation selected by one microscopic-reversal argument. The source and target fields remain explicit because ordinary time reversal at zero field and simultaneous time/field reversal at nonzero field are different realizations of the same relation.
- structureValue-bearing boundary data for distinguishing reversal at a fixed nonzero field from simultaneous microscopic and field reversal. The trajectory weights and the selected cross-coefficients are kept separately: microscopic reversal is a premise for the transport route, not the coefficient result.
- structureThe exact selected reciprocal-transport calculation is data-only. It stores all values and relation families consumed by the route, but no proof of selection, setup, regression, correlation reversal, or reciprocity.
- inductiveThe exact shared content of the Onsager and Casimir transport routes.
- structureShared semantics for the selected fluctuation-regression route. The selected transport data remain concrete context data so that a paper adapter can build the exact proof-free model and the semantics can reject substitutions.
- structureThe process and field pair within which reciprocity is explained.
- structurePaper-local interpretation of a selected reciprocal-transport calculation. Theory use and representation of a physical situation are independent bridges; neither is stored in the calculation.
- structureThe theory using the selected transport calculation remains distinct.
- structureThe represented transport situation remains distinct from model and theory.
- inductive
- 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
- structureSelected real-valued content of Physical Review pp. 412-413 equations (3.7)-(3.10). The readout keeps Onsager's three chemical forms, ideal-solution free energy, near-equilibrium force approximation, and six transition rates local to the chemical-triangle analogy.
- structure
- structure
- structureSelected real-valued content of Onsager's simple rotationally symmetric crystal calculation on Physical Review pp. 415-417. The readout keeps the printed fluctuation moments, thermodynamic forces, heat fluxes, regression drifts, delayed correlations, and reversal symmetry local to this paper.
- inductiveThe paper-local route producing Onsager's selected reciprocal relation.
- inductive
- inductive
- structure
- structure
- inductive
- inductive
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- inductive
- structure
- structure
- structurePhysical transformation and observable data need neither a selected vacuum family nor a variational principle.
- structureLaw symmetry and admissible state action, without interpretation, vacuum selection, or variational claims.
- structure
Definitions and domain choices
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe two scale comparisons use the same stated relative tolerance.
- definitionA stated relative bound; its numerical adequacy for regression is a separate input.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionBalance against the trajectory in the simultaneously reversed field.
- definitionThe selected Onsager-Casimir coefficient relation at the reversed field.
- definitionA genuinely nonzero field, its unchanged copy, and its reversed value.
- definitionBalance against a reversed trajectory while the field is held fixed.
- definitionThe corresponding parity-sensitive relation with the field held fixed.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe complete parity- and field-reversed coefficient relation.
- definitionThe shared reversible setup realizes a physical symmetry of the selected microscopic process and exhibits the actual source-to-reversed-field action. The two field endpoints are admissible in the same selected field-pair scope.
- definitionThe regression law is used only in its retained intermediate window.
- definitionThe universal result at the retained off-diagonal variable pair.
- definitionThe selected cross-variable setup stated directly on one calculation model, without a context-owned exact-selection certificate.
- definitionThe boundary readout retains the exact selected process, field pair, variables, parity, and coefficient entries of one calculation model. Its field-paired trajectory balance is equivalent to the model's microscopic reversal relation at that pair.
- definitionThe complete reciprocal-transport argument as a direct proposition on one physical model. It retains the actual reversible setup, scoped regression assumption, realized correlation and coefficient outputs, and selected off-diagonal relation, but neither implication-valued calculation contracts nor a context-owned exact-selection certificate.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe proof-free selected data constrained by the complete route.
- definitionThe exact paper-local derivation selected for this reciprocity route.
- definitionThe proof-free universal relation and selected off-diagonal instance.
- definitionThe exact field-paired reversal transformation retained by this model.
- definitionThe exact process and field pair used by the explanation.
- definitionPhysical-symmetry semantics for the selected microscopic reversal. The transformation maps the source field to its retained reversal, and its law-invariance and physical-transformation predicates retain respectively the microscopic-reversal and field-admissibility relations of the transport model. No regression or coefficient relation is built into this context, and no selected-family, descriptive, or variational classification is supplied.
- definition
- definition
- definitionThe retained transport pair is genuinely cross-variable.
- definition
- definition
- definitionThe explained transport output: the complete field-reversed law together with its retained cross-variable instance. The latter prevents diagonal identity from masquerading as the physical reciprocity phenomenon.
- definition
- definition
- definition
- definition
- definition
- definitionA source-sensitive structural explanation of reciprocal transport.
- definitionThe complete regression route structurally explains reciprocity.
- definitionThe universal result specialized to the retained off-diagonal pair.
- definitionExact equality with the context-owned model, together with the separate claim that its selected field lies in the paper-admissible field family.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe unique transport model fixed by the context-owned process and field value together with every route-used relation family.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- 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
- 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
- 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
- definitionEquations (3.4), (3.8), and footnote 9: displacements and variations conserve total amount. The forces describe this constrained variation, not three independent unconstrained partial derivatives.
- definitionEquation (3.9) is a first-order expansion at the reference state. It is not an unspecified binary comparison or an exact equality at finite displacement.
- definition
- definitionEquation (3.10) uses the stationary reference in (3.3) and the linearized forces from (3.9). Exact logarithmic forces leave an approximation error.
- definitionThe logarithms and RT denominators in equations (3.7)-(3.10) use positive amounts, positive equilibrium amounts, and positive temperature and gas constant.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe coefficient map in (3.10), with destination-first rate subscripts.
- definition
- definition
- definition
- definition
- definitionEquation (3.7): the ideal-solution free energy is Z_min plus RT times the three amount-weighted logarithms relative to equilibrium.
- definition
- definition
- definitionThe exact monomolecular amount-rate map in equation (3.2).
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA finite-component realization of the local temperature-weighted pairing. The physical temperature domain is positive; no extremum is stored.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThis readout satisfies the fluctuation, force, flux, regression, and opposite-sign correlation formulas with a nonzero spiral coefficient, but it violates the reversal correlation symmetry. It shows why equation (4.10) is not decorative in the route to equation (4.11).
- definitionPhysical Review p. 417, equation (4.8): after selecting alpha-one initially, the conditional average alpha-two displacement over the small lag is the spiral drift term.
- definitionPhysical Review p. 418, equation (4.11): the spiral coefficient vanishes.
- definitionPhysical Review p. 416, equation (4.5): the selected thermodynamic forces are proportional to the two energy-displacement moments with the same factor C.
- definitionPhysical Review p. 416, equation (4.4): the two transverse energy moments have the preceding zero means, equal mean squares, and vanishing equal-time cross moment.
- definitionPhysical Review p. 417, equations (4.9a-b): regression gives opposite-sign delayed cross correlations for the two transverse moment orderings.
- definitionPhysical Review p. 417, equation (4.7): multiplying the fluxes by the crystal volume gives the regression drifts of the two energy moments with the printed signs.
- definitionPhysical Review p. 416, equation (4.6): the longitudinal coefficient and allowed antisymmetric spiral coefficient determine the two heat fluxes.
- definitionPhysical Review p. 417, equation (4.10): microscopic reversibility makes the two delayed cross-correlation orderings equal for every lag.
- definitionPhysical Review p. 415, equation (4.3): alpha-one and alpha-two are the first spatial moments of the selected local energy density over the crystal volume. The volume integral remains imported mathematics through the selected operator.
- definitionThe paper uses a positive temperature, crystal volume, fluctuation stiffness, nonzero mean-square displacement, and positive small time increment in the equations-(4.8)-(4.11) comparison.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionPositive nearby amounts (1+s, 2-s, 1) about a detailed-balanced reference (1,2,1). The rate convention is the paper's destination-first convention.
- definition
- 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 remaining calculation inputs identify inverse matrices and actual integrals; they do not supply a potential-gradient or variational conclusion.
- definition
- definition
- definition
- definition
- definition
- definitionThe equations-(4.3)-(4.10) readout is tied to Onsager's selected anisotropic crystal, energy-fluctuation distribution, observed lag, cross correlation, and antisymmetric heat coefficient. The final iff is an explicit representation bridge from the real-valued omega-three formula to the paper's abstract coefficient-vanishing predicate.
- definition
- definition
- definition
- definition
- definition
- definitionEquation (5.12) restricts every trial flow; it does not assert a maximum.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe p. 409 ellipsoid argument is retained as an explicit calculation rather than hidden inside the reciprocal-coefficient theorem. Reciprocity supplies the premise; the geometric consequence says that every principal-axis temperature gradient gives parallel heat flow.
- definition
- definition
- definition
- definition
- definition
- definitionAt equilibrium, every admissible motion has an admissible reverse occurring equally often. This is Onsager's statistical use of reversible dynamics on Physical Review pp. 411 and 417, not a production-sign relation.
- definitionThe chemical route binds equations (3.7)-(3.10) to the selected mass-action triangle before the near-equilibrium reciprocity conclusion.
- definitionOnsager's cross coefficients compare two distinct indexed thermodynamic forces, as in the `L₁₂ = L₂₁` relation on Physical Review p. 419.
- definition
- definition
- definitionThe possible spiral flow is conditional: it concerns the low-symmetry planar crystals for which a nonzero antisymmetric coefficient is allowed. The paper reports a sensitive null search; it does not infer reciprocity from that null result.
- definition
- definitionEquations (6.1), (6.3), and (6.7), with the actual additional obstacle restriction and fixed prescribed normal flux. The common temperature and resistance functionals remain frozen throughout this comparison.
- definition
- definition
- definition
- definition
- definition
- definitionVelocity reversal is represented as an involution on complete motions.
- definitionGreen's identity and strictly positive dissipation are the remaining inputs for (5.11). Nonnegative entropy production alone does not give uniqueness.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionIsolation defines a family of admissible flows, not a claim that the separately selected open-boundary steady flow is also isolated.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe exact raw Onsager route retained by the source-sensitive explanation.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionEquations (5.1)-(5.3), with actual spatial fields and their analytic domains.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionOnsager's paper-local interpretation distinguishes the exact selected heat-conduction calculation from the linear irreversible theory using it and from the anisotropic equilibrium crystal represented by it. Primary-source anchors: sections 3-4 for the selected energy-fluctuation process, regression, and microscopic reversal; equations (4.14)-(4.16) for the variables and kinetic coefficients; section 7 for field reversal.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionEquation (5.10) is retained only at the selected constitutive flow.
- 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
- 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
- definition
- definition
- definition
Selected instances and coercions
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
Source mappings and interpretation choices
- checked statement
- inductive
- definition
- instance
- 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
- 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
- definition
- definition
- constructor
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- 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
- definition
- constructor
- definition
- checked statement
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- 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
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- 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
- 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
- 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
- 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
- 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
- definition
- constructor
- definition
- checked statement
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- definition
- definition
- checked statement
- definition
- definition
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- definition
- inductive
- definition
- instance
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- 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
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- inductive
- definition
- instance
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- structure
- definition
- instance
- checked statementRaw paper-local inputs construct every Onsager Part I route in source order.
- definition
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- constructor
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- checked statement
- recursor
- definition
- checked statement
- checked statementNo completed route certificate is needed to cover a route identifier.
- checked statement
- checked statement
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- 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
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- 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
- definition
- definition
- checked statement
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- checked statement
- definition
- checked statement
- definition
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- definition
- definition
- checked statement
- definition
- checked statement
- checked statement
- checked statement
- definition
- checked statement
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
Checked statements: parameters, hypotheses, and interpretation
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe unrestricted derivative contains RT times the change in total amount.
- checked statement
- checked statement
- checked statementThe three printed rate equations conserve total chemical amount.
- checked statement
- checked statement
- checked statementConstrained variations determine force differences, not absolute forces.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe source package retains equations (3.7)-(3.10) as value formulas.
- checked statement
- checked statement
- checked statementA quantitative consequence of the ideal logarithm, not an error estimate stated in the paper: the small parameter before (3.9) is displacement/reference.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementEquation (5.1) uses X = -grad(T)/T, not the unnormalized temperature gradient.
- checked statementThe inverse-temperature gradient in (5.9) retains both powers of temperature.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementEquations (4.9a-b) give opposite-sign cross correlations, while equation (4.10) identifies them under microscopic reversal. Positivity of the selected correlation scale then forces the printed equation (4.11), omega-three = 0.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementAbsolute smallness is not uniform relative smallness as the reference amount varies. This tests the scalar force formula, not a full kinetic history.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe source variation is correct on fixed-number directions, but it is not the derivative along a direction that adds chemical amount.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementOnsager Part I, section 7: the Righi-Leduc/Hall-shaped cross coefficients are reciprocal only after reversing the nonzero magnetic field together with the microscopic motion. Ordinary same-field reversal and reciprocity both fail.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked 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 linearization calculation exposes the printed chemical formulas.
- checked statement
- checked statement
- checked statement
- checked statementThe fluctuation route retains the printed equations (4.3)-(4.10) as a paper-local formula output before the abstract reciprocal-coefficient result is used downstream.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementOnsager's zero-field heat-fluctuation route realizes the source-sensitive explanation while retaining its regression, correlation, and coefficient calculation premises.
- checked statementOnsager's fluctuation-regression and heat-coefficient calculations realize a structural explanation of the universal zero-field relation and its retained cross-force instance. No established or direct terminal transport result is used as a premise.
- checked statement
- checked statementThe paper's selected equilibrium crystal and fluctuation ensemble supply the theory/model and model/world bridges. Grounding also consumes the selected reversible near-equilibrium setup, but no regression, correlation, or coefficient output.
- checked statement
- checked statement
- checked statement
- checked statementPhysical Review pp. 417-419 realizes the direct shared route: two distinct energy-displacement variables undergo macroscopic average regression, their two-time correlation is reversal symmetric, and the resulting off-diagonal heat coefficient is reciprocal at zero field.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe selected zero-field motion reversal is a physical symmetry before the independent regression and coefficient calculations are used. This is the Onsager realization of the shared microscopic field-reversal projection.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- 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
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- 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
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- 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
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- recursor
- constructor
- constructor
- recursor
- recursor
- constructor
- constructor
- recursor
- constructor
- constructor
- recursor
- constructor
- recursor
- constructor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- constructor
- recursor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
External mathematical declarations
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
Every statement below comes only from Onsager1931.lean, SourceMap.lean, and Coverage.lean. Entropy-production, detailed-balance, linearization, principal-axis, dissipation-potential, variational, stationary-flow, magnetic, Coriolis, and scope calculations remain independent proposition-valued contracts until substantive result steps apply them. ChemicalTriangleFormulaReadout separately retains equations (3.7)–(3.10) as a selected value bundle with logarithms, approximation relations, and all six rates; a checked theorem shows that its three rate equations conserve total displacement. The fluctuation branch separately retains a represented real-valued readout for equations (4.3)–(4.10), including energy-moment, force, flux, drift, and delayed-correlation formulas; its checked theorem derives equation (4.11). Route certificates establish predecessor availability only; dissipation, stationary, magnetic, and Part-I setup packages are reconstructed from exact ClaimsHold predecessor atoms plus separately source-mapped local inputs. Isolated-boundary zero exchange is also its own source claim. The spiral null search remains a separate evidence proposition.
The paper contains three independent foundations and six dependent developments
Thermodynamic insufficiency, the chemical kinetic analogy, the fluctuation-regression proof, and the controlled approximation route begin independently. The heat result feeds a paper-local principal-axis and spiral-evidence assessment and the dissipation route. Dissipation feeds stationary flow; heat reciprocity and dissipation together feed the nonreversible qualifications. The final scope route recovers the checked heat-reciprocity and crystal-assessment atoms while preserving the announced general theorem as deferred.
| Transition | Status | Retained boundary |
|---|---|---|
| Entropy production to positivity bound | thermodynamic calculation | Positivity does not determine reciprocal coefficients. |
| Chemical equilibrium to pairwise balance | microscopic calculation | Equilibrium alone does not exclude a stationary cycle. |
| Detailed balance to chemical reciprocity | near-equilibrium linearization | The free-energy forces are linearized only near equilibrium. |
| Fluctuation to macroscopic decay | physical regression assumption | Only the ensemble average obeys the heat law; individual paths need not. |
| Reversal and correlations to heat reciprocity | supplied calculations | Regression, correlation symmetry, coefficient identification, and comparison are all required. |
| Heat reciprocity to principal axes and spiral test | calculation plus limited evidence | Parallel principal-axis flow is derived; a sensitive null spiral search does not prove reciprocity. |
| Macroscopic heat law near zero time | controlled asymptotic regime | Microscopic lag and the zero-time crossing are excluded. |
| Reciprocity to variational principles | explicit potential and variation | Boundary isolation and vanishing entropy exchange are separate inputs. |
| Zero-field reciprocity to magnetic transport | qualified reversal | Ordinary same-field reciprocity fails; simultaneous field reversal is different. |
| Heat result to general transport | deferred generalization | Part I announces but does not prove the general theorem. |
Thermodynamic positivity constrains coupled transport without supplying reciprocity
The coupled-transport setup selects irreversible processes governed by a phenomenological linear law and identifies two cross coefficients. A supplied entropy-production calculation yields positivity and the corresponding thermodynamic bound. A separate insufficiency assessment says that thermodynamics alone does not determine reciprocity.
⇒ positive entropy production and its thermodynamic bound, but not reciprocity determined by thermodynamics alone.
thermodynamics_constrains_but_does_not_supply_reciprocity; Physical Review pp. 405, 407
(1)
This is an obstruction result, not the proof of reciprocity. The formal countermodel even supplies a positive numerical inequality while two test coefficients remain nonreciprocal.
The chemical triangle is a separate detailed-balance analogy
Three molecular forms undergo positive-rate mass-action transitions, possess an equilibrium, and come with three specified reverse-transition pairs. Microscopic reversibility means that trajectory reversal is involutive and every admissible motion has an admissible reverse occurring equally often.
The detailed-balance calculation uses that microscopic premise to balance all three reverse pairs and exclude a cyclic stationary current. A second calculation then uses near-equilibrium free-energy linearization to put the chemical rate law in phenomenological form and make its cross coefficients reciprocal. SelectedChemicalTriangleFormulaAt keeps the selected process attached to the printed equations before that conclusion is exported.
xi = ni − ni0, δZ = −XAδxA − XBδxB − XCδxC,
Xi = −RT log(ni/ni0) ≈ −RT xi/ni0,
(ẋA, ẋB, ẋC) = the printed six-rate linear combinations of (XA, XB, XC), ẋA + ẋB + ẋC = 0.
source_formula_retains_equations_three_seven_through_three_ten · equation_three_ten_conserves_total_displacement_rate; Physical Review pp. 412–413, equations (3.7)–(3.10)
(2a)
⇒ pairwise detailed balance for all three transition pairs, no cyclic stationary current, equations (3.7)–(3.10) and a linear phenomenological chemical law, and reciprocal chemical cross coefficients.
chemical_linearization_retains_equations_three_seven_through_three_ten · microscopic_reversibility_and_linearization_yield_chemical_reciprocity; pp. 410–413
(2)
An explicit six-transition countermodel shows why equilibrium plus a stationary cycle does not imply pairwise detailed balance. The reverse-pair equality is a substantive consequence of microscopic reversibility, not another name for equilibrium. a_named_chemical_rate_law_does_not_supply_equations_three_seven_through_three_ten separately blocks replacing the value bundle by a label.
The anisotropic heat proof combines microscopic reversal with an independent ensemble-regression principle
The selected anisotropic crystal is isolated and at statistical equilibrium, but not literally motionless: it has energy-distribution fluctuations. The history of the selected distribution is irrelevant to its regression. The setup explicitly states that not every microscopic realization obeys the macroscopic heat law, while heat-conduction trajectories obey microscopic reversibility.
Microscopic reversibility supplies a concrete witness: reversing the selected admissible trajectory gives another admissible trajectory, the reversal is involutive, and direct and reverse motions occur equally often at equilibrium. This does not yet yield a transport coefficient equality.
The missing bridge is RegressionAssumption: conditional on the fluctuation setup, the ensemble-average regression of the selected distribution obeys the macroscopic heat law. The represented formula readout keeps equations (4.3)–(4.10) local to the paper: the energy-displacement moments, equal transverse fluctuation variances, force and flux laws, volume-weighted regression drifts, the conditional delayed displacement, the opposite-sign cross correlations, and the equality of those correlations under microscopic reversal. The checked arithmetic theorem compares the last two formulas and forces equation (4.11), ω₃ = 0. A separate represented-zero bridge connects that real-valued conclusion to the abstract antisymmetric-coefficient predicate before reciprocal heat coefficients are retained.
mu_0 is normalized and stationary; the centered observables are square-integrable.
R Phi_0(t,x) = Phi_0(-t,Rx); R_*mu_0 = mu_0; a_i(Rx) = a_i(x).
With reversal-fixed zero field, C_ij(0,t) = C_ji(0,t).
the_actual_stationary_reversible_heat_ensemble_has_symmetric_correlations; the two displayed cross-correlation functions are these actual integrals, not independent readouts. Microscopic realization is an explicit input; heat regression is not inferred from symmetry.
(3c)
⟨α₁⟩ = ⟨α₂⟩ = 0, ⟨α₁²⟩ = ⟨α₂²⟩ = a², ⟨α₁α₂⟩ = 0,
−TX₁ = TCα₁, −TX₂ = TCα₂,
J₁ = −λ₁Cα₁ − ω₃Cα₂, J₂ = ω₃Cα₁ − λ₁Cα₂,
dα₁/dt = −λ₁VCα₁ − ω₃VCα₂, dα₂/dt = ω₃VCα₁ − λ₁VCα₂,
α₂(Δt, α₁′) = ω₃VCα₁′Δt,
⟨α₁(t)α₂(t+Δt)⟩ = ω₃VCa²Δt, ⟨α₂(t)α₁(t+Δt)⟩ = −ω₃VCa²Δt,
microscopic reversal ⇒ ⟨α₁(t)α₂(t+τ)⟩ = ⟨α₂(t)α₁(t+τ)⟩
⇒ ω₃ = 0.
equations_four_nine_and_four_ten_force_equation_four_eleven · heat_fluctuation_source_formula_forces_selected_coefficient_vanishes; pp. 415–418, equations (4.3)–(4.11)
(3)
⇒ the antisymmetric heat coefficient vanishes and the anisotropic heat coefficients satisfy Lᵢⱼ = Lⱼᵢ.
fluctuation_regression_and_correlation_symmetry_yield_heat_reciprocity; pp. 414–420, equations (4.9)–(4.10)
(3a)
The result retains all of its distinctions: equilibrium fluctuations exist; equilibrium is not literally motionless; average regression obeys the heat law; every microscopic realization need not; reverse motions occur equally often; correlation symmetry holds; the represented equations (4.3)–(4.10) remain visible; the antisymmetric coefficient vanishes; and heat reciprocity follows.
Reciprocity has a crystal-geometric consequence, while the spiral search is only evidence
The p. 409 branch is not collapsed into the coefficient equation. A named principal-axis calculation consumes reciprocal heat coefficients and yields a nonempty family of ellipsoid-determined, orthogonal principal heat axes, with parallel heat flow whenever the temperature gradient is along one of those axes.
⇒ at least one principal heat axis, conducting properties determined by the ellipsoid, orthogonal principal heat axes, and heat flow parallel to every principal-axis temperature gradient.
reciprocal_heat_coefficients_retain_principal_axes_and_limited_spiral_evidence; p. 409, equations (2.5)–(2.7)
(3b)
A separate low-symmetry planar setup keeps the alternative conditional: if its allowed antisymmetric coefficient is nonzero, heat flow has a fixed angle to the temperature gradient and a centrally heated circular plate would show spiral flow. Soret and Voigt's sensitive failure to observe that motion is encoded as SpiralNullEvidence. It is inherited by the assessment but never used as a converse proof of reciprocal coefficients.
Microscopic reversibility and null evidence have different limits
The countermodel equations_four_three_through_four_nine_do_not_supply_reversal_symmetry_or_zero satisfies the energy-moment, fluctuation, force, flux, drift, and opposite-sign correlation formulas with nonzero ω₃ while falsifying equation (4.10); reversal symmetry is genuinely needed for equation (4.11). The countermodel microscopic_reversibility_without_regression_bridge_does_not_yield_reciprocity makes the missing regression inference explicit. A third countermodel separates ensemble-average regression from pathwise regression. The countermodel sensitive_null_spiral_search_does_not_establish_reciprocity blocks the converse from a sensitive negative spiral search to reciprocal coefficients.
The regression law belongs to an intermediate-time, large-body asymptotic regime
The approximation setup places the observation interval well above the microscopic lag and well below the macroscopic relaxation time. The crystal is large compared with the mean free path. The average fluctuation grows toward equilibrium for negative time and decays for positive time.
⇒ acceleration lag negligible in the macroscopic regime, conduction valid macroscopically but not in the microscopic-lag regime, and the conduction law not applied through zero time, with negative-time growth and positive-time decay retained.
intermediate_time_and_large_body_conditions_control_regression; pp. 418–419
(4)
Hence 0<tau and tau_micro<tau<T.
the_intermediate_time_contract_retains_actual_lag_separation; the formula lag equals the selected physical clock. A chosen relative tolerance does not by itself justify regression.
(4a)
The apparent zero-time discontinuity is therefore not repaired by declaring the macroscopic equation exact at all scales. The formal result removes that extrapolation. A dedicated countermodel confirms that validity in the macroscopic regime need not extend through microscopic lag.
Reciprocal resistance supports a dissipation potential only through explicit calculations and boundary data
The dissipation setup now uses actual spatial temperature, resistance, conductivity, and heat-flow fields. Inverse-matrix and integral-representation calculations are explicit inputs. Reciprocal conductivity gives reciprocal resistance; the temperature-weighted bilinear pairing defines a quadratic dissipation functional. The potential gradient and variational maximum are derived, not supplied as named conclusions.
B(J,K)=integral_V J(x)^T R(x) K(x)/T(x) dV; Phi(J)=B(J,J)/2.
s(J)=integral_V J dot grad(1/T) dV.
Ssystem(J)=integral_V -div(J)/T dV; Sboundary(J)=integral_boundary J_n/T dA.
Green input: Ssystem(J)+Sboundary(J)=s(J) for every admissible flow.
HeatDissipationReadout; pp. 420-422, equations (5.1)-(5.9). Derivatives are actual coordinate derivatives; differentiability, integrability, and the continuum integral representations remain explicit inputs.
(5a)
At fixed temperature, entropy supply is linear in the varied flow, while dissipation is quadratic. The constitutive physical flow makes their values satisfy equation (5.10). Onsager's p. 422 warning is essential: this is not an identity to substitute for every varied flow before applying equation (5.11).
B(u,v)=B(v,u); constitutive flow J_* satisfies s(v)=B(v,J_*) for every v.
F(J_*+v)=F(J_*)-Phi(v).
Phi(v)>=0 for all v gives a maximum; Phi(v)>0 for every nonzero v gives uniqueness.
reciprocity_and_the_constitutive_equation_give_the_exact_variation_gap; the desired maximum is not a variational-calculation input.
(5b)
Constructed control: T=2, R=[[2,1],[1,2]], X=(4,5), J_*=(1,2).
s(J_*)=7; Phi(J_*)=7/2; s(2J_*)=14; Phi(2J_*)=14.
F(J_*)=7/2 > F(2J_*)=0, while Phi(2J_*)>Phi(J_*).
a_constitutive_entropy_identity_does_not_hold_for_all_trials; substituting s=2*Phi before variation changes the extremum. Maximizing F does not maximize unconstrained entropy supply.
(5c)
Phi(x,y)=(x^2+y^2)/2 is strictly positive away from zero; s(x,y)=x-y.
Its constitutive flow is not a maximum: F(1,-1)=1 > F(1,0)=1/2.
Semidefinite control: Phi(x,y)=x^2/2, s(x,y)=x; (1,0) and (1,1) are distinct maxima.
A resistance tensor and its transpose have the same quadratic dissipation but can give different forces.
positive_dissipation_and_a_constitutive_flow_do_not_supply_a_variational_maximum and a_positive_dissipating_physical_flow_need_not_have_a_unique_maximum. The semidefinite case tests nonnegativity alone, not the full invertible-conductivity setup. These finite matrices are controls, not fitted crystals.
(5d)
Phi changes from 7/2 to 7/4; s changes from 7 to 7/2.
the_temperature_weight_in_both_physical_functionals_is_not_optional; the same constitutive flow does not fix temperature-independent numerical functionals.
(5e)
⇒ reciprocal resistance coefficients, a quadratic potential with force as gradient, twice-dissipation/entropy-production identity at the physical flow, unique prescribed-temperature maximum, derived zero isolated-boundary entropy exchange, and isolated entropy-minus-dissipation maximum.
reciprocal_resistance_yields_dissipation_variational_principles; pp. 420–423, equations (5.3)–(5.13)
(5)
Isolation means vanishing normal heat flux for the physical and every admissible trial flow in that boundary family. Lean derives zero boundary entropy exchange from the actual integral, then specializes the maximum. The source graph records these as deductions from isolation, not independent zero-exchange or maximum assumptions. This family is separate from the selected open-boundary steady flow; a nonzero stationary dissipating flow is not also asserted to be isolated.
Divergence-free stationary heat flow obeys two differently constrained extremum principles
The stationary route consumes the derived variational maximum and adds actual zero divergence. Green balance turns its functional into boundary entropy exchange minus dissipation. The remaining source inputs specify the constrained trial's power identity, vanishing obstacle normal flux, and prescribed boundary profile; they do not assume the desired entropy bound or least-dissipation inequality.
Power constraints: Sboundary(J_*)=2*Phi(J_*) and Sboundary(J)=2*Phi(J).
F(J)<=F(J_*) then gives Sboundary(J)<=Sboundary(J_*).
The obstacle trial also satisfies J dot n_obstacle=0, using the same frozen T and R functional.
stationary_power_constraints_turn_the_variational_maximum_into_an_entropy_bound; equations (6.1)-(6.5). Stationarity alone does not replace the trial power constraint.
(6a)
With both flows stationary, Sboundary(J)=Sboundary(J_*), so Phi(J_*)<=Phi(J).
integral_boundary g dA=0 is only compatibility, not equality of boundary profiles.
prescribed_normal_flux_gives_least_dissipation_among_stationary_trials; (6.6)-(6.7). The p. 424 compatibility integral is unnumbered; equation (6.7) prescribes J_n.
(6b)
⇒ prescribed-temperature stationary maximum, entropy production not increased by the obstacle, and prescribed-flux least dissipation.
stationary_flow_obeys_obstacle_and_prescribed_flux_principles; pp. 423–425, equations (6.2)–(6.7)
(6)
The theorem retains the different boundary and constraint conditions. An independent finite-component client uses temperature five, a different reciprocal tensor and selected current, and a second nonsymmetric system. It derives a unique maximum in the first case and rejects that conclusion in the second despite strictly positive dissipation. This tests reuse of the functional logic, not a complete continuum heat conductor. The variational API remains paper-local until a second independent primary paper needs it.
Magnetic field reversal and Coriolis rotation require separate departures from the ordinary result
The magnetic setup includes the zero-field heat reciprocity and dissipation results, then adds a magnetic field for heat and electric conduction together with the Righi–Leduc and Hall transverse responses. The ordinary-failure calculation denies ordinary time-reversal invariance, same-field reciprocity, and least dissipation for the magnetic heat system.
A different supplied calculation reverses the magnetic field together with all velocities and establishes modified reversal invariance.
⇒ ordinary same-field reversal, reciprocity, and least dissipation fail, while modified field reversal remains invariant.
magnetic_field_requires_modified_reversal; pp. 425–426
(7)
The rotating-frame system is distinct. It selects viscous flow in a rotating frame with a Coriolis force. Its calculation denies ordinary rotational reversal and the ordinary least-dissipation principle in that frame.
⇒ ordinary rotation reversal fails and least dissipation is not valid in the rotating frame.
coriolis_rotation_qualifies_ordinary_reversal_and_dissipation; pp. 425–426
(8)
magnetic_and_coriolis_results_form_nonreversible_qualification joins the two already checked intermediate results into the final conjunction. It does not treat Coriolis rotation as magnetic-field reversal or rebuild the result from raw inputs after the source graph has selected the intermediate outputs. Two countermodels separately block extension of zero-field reciprocity to same-field magnetic reciprocity and extension of inertial-frame Stokes variation to a rotating frame.
Part I proves anisotropic heat reciprocity and explicitly defers the general transport theorem
The final route uses heat-reciprocity and crystal-assessment certificates only for availability, then recovers both exact result atoms from ClaimsHold. Its explicit scope setup says that Part I treats the anisotropic crystal, establishes heat reciprocity together with the principal-axis and limited spiral-evidence branch, announces a general transport theorem, and defers that development to Part II.
⇒ anisotropic heat conduction is treated and reciprocal, the crystal assessment is retained, the general transport theorem is announced and deferred, and that general theorem is not proved in Part I.
part_i_proves_heat_conduction_and_defers_general_transport; pp. 407, 423
(9)
This qualified statement is the source map's declared main conclusion. Its audits preserve the heat derivation, the crystal assessment with limited null evidence, and the genuinely deferred generalization. A formal countermodel prevents the anisotropic heat result from being relabeled as the general transport theorem.
Symmetry Role Scope
The microscopic-reversal adapter retains physical field reversal, admissibility, and the selected coefficient readout.
No selected vacuum family, descriptive classification, variational symmetry, or conservation predicate is filled in; regression and reciprocity retain their separate inputs.
onsager_heat_setup_realizes_microscopic_field_reversal_physical_symmetry
Concept guide
Thermodynamic positivity
Positive entropy production and its bound for the selected linear force–flux system, insufficient by themselves for reciprocity.
CoupledTransportResultChemical detailed balance
Pairwise reverse-transition balance and absence of a cyclic equilibrium current, derived from microscopic reversibility.
ChemicalDetailedBalanceCalculationMicroscopic reversibility
Involutive trajectory reversal with admissible direct and reverse motions occurring equally often at equilibrium.
MicroscopicReversibilityEnsemble regression assumption
The physical bridge asserting that the ensemble-average decay of the selected fluctuation follows the macroscopic heat law.
RegressionAssumptionCorrelation symmetry
The supplied two-time symmetry calculation used with coefficient identification to eliminate the antisymmetric heat term.
CorrelationSymmetryCalculationAnisotropic heat reciprocity
The paper-local result that the antisymmetric coefficient vanishes and the heat-transport coefficients are reciprocal.
FluctuationReciprocityResultPrincipal axes and spiral evidence
Ellipsoid-determined orthogonal heat axes and parallel principal-axis flow, kept distinct from the conditional low-symmetry spiral prediction and sensitive null search.
EstablishedCrystalSpiralAssessmentIntermediate regression regime
Observation after microscopic lag but before macroscopic relaxation, in a body large relative to mean free path.
RegressionApproximationResultDissipation potential
The reciprocal-resistance quadratic potential, its gradient relation, entropy-production identity, and boundary-dependent variations.
DissipationVariationalResultStationary-flow extrema
Qualified prescribed-temperature, obstacle, and prescribed-flux results for divergence-free heat flow.
StationaryFlowResultMagnetic modified reversal
Failure of ordinary same-field reciprocity and restoration of a modified operation when field and velocities reverse together.
MagneticQualificationResultCoriolis qualification
The separate rotating-frame failure of ordinary reversal and least dissipation for viscous flow.
CoriolisQualificationResultQualified Part-I scope
Anisotropic heat reciprocity proved; the announced general transport theorem deferred and not proved in Part I.
QualifiedPartIConclusionShared reciprocal transport
The grounded zero-field, even-parity reusable transport model realized through the paper-local heat route and explicit coefficient bridge.
reciprocalTransportModelAtComplete route inventory, blocked shortcuts, and provenance
The source map declares nine routes, forty-nine claims, and forty-nine sourced steps. Coverage interprets every atom, semantically realizes every route, and proves exhaustive realization. Implication-valued source contracts stay independent until result steps apply them; every nonempty step recovers its exact checked atoms from ClaimsHold, while route certificates establish predecessor availability only. The qualified Part-I conclusion is the declared main conclusion.
| Route | Direct dependencies | Declared output | Profile |
|---|---|---|---|
| Thermodynamic scope | — | Positivity with thermodynamic insufficiency | independent root |
| Chemical detailed-balance analogy | — | Detailed balance and reciprocal chemical coefficients | independent near-equilibrium analogy |
| Fluctuation reciprocity | — | Equations (4.3)–(4.10) and reciprocal anisotropic heat coefficients | independent regression root |
| Crystal spiral assessment | Fluctuation reciprocity | Principal-axis consequence with conditional spiral prediction and null evidence | paper-local calculation and evidence |
| Regression approximation scope | — | Macroscopic validity and microscopic exclusions | controlled asymptotic regime |
| Dissipation variational principle | Fluctuation reciprocity | Dissipation potential and two boundary variations | explicit calculation chain |
| Stationary flow | Dissipation variation | Qualified stationary extremum principles | stationary specialization |
| Magnetic and rotating exceptions | Fluctuation reciprocity; dissipation variation | Separate magnetic and Coriolis qualifications | nonreversible limitations |
| Part-I scope | Fluctuation reciprocity; crystal spiral assessment | Heat theorem and crystal assessment retained, general theorem deferred | qualified main conclusion |
Thermodynamic scope · thermodynamic_scope_route_is_semantically_realized
Chemical analogy · chemical_detailed_balance_analogy_route_is_semantically_realized
Fluctuation proof · fluctuation_reciprocity_route_is_semantically_realized
Crystal assessment · crystal_spiral_assessment_route_is_semantically_realized
ClaimsHold before certifying their qualified conjunction.Approximation scope · regression_approximation_scope_route_is_semantically_realized
Dissipation variation · dissipation_variational_principle_route_is_semantically_realized
Stationary flow · stationary_flow_route_is_semantically_realized
Nonreversible systems · magnetic_and_rotating_exceptions_route_is_semantically_realized
Part-I scope · part_i_scope_route_is_semantically_realized
ClaimsHold, then certifies the setup and assessment that restrict the proof and defer the general theorem.All forty-nine source-mapped claims
| Claim group | Source anchor | Status |
|---|---|---|
| Coupled setup, positivity calculation, thermodynamic assessment, and constrained result | pp. 405, 407 | Physical setup, calculation, obstruction |
| Chemical setup, reversal, near-equilibrium scope, two calculations, and detailed-balance result | pp. 410–413, equations (3.7)–(3.10) | Principle, controlled approximation, paper derivations |
| Fluctuation setup, regression assumption, correlation calculation, coefficient identification, reciprocity calculation, equations (4.3)–(4.10) source formula, and heat result | pp. 411, 414–420, equations (4.3)–(4.11) | Physical premises, represented formulas, and paper derivations |
| Crystal spiral setup, null evidence, principal-axis calculation, and qualified assessment | p. 409, equations (2.5)–(2.8) | Conditional prediction, evidence, and paper derivation |
| Approximation setup, calculation, and result | pp. 418–419 | Controlled asymptotic approximation |
| Dissipation local setup, reconstructed setup, potential and variational calculations, isolated boundary, zero exchange, specialization, and variational result | pp. 420–423, equations (5.3)–(5.13) | Physical premises and paper derivations |
| Stationary local setup, reconstructed setup, calculation, and result | pp. 423–425, equations (6.2)–(6.7) | Physical specialization and paper derivation |
| Magnetic local setup, reconstructed setup, ordinary failure, modified reversal, magnetic result, Coriolis setup and calculation, Coriolis result, combined qualification | pp. 425–426 | Two distinct nonreversible assessments |
| Part-I local scope, reconstructed scope setup, deferred assessment, and qualified conclusion | pp. 407, 423 | Proved heat result plus deferred generalization |
Ten formally blocked shortcuts
The finite witnesses retain the relevant physical data. A two-channel transport matrix has nonnegative entropy production for every force pair despite unequal cross coefficients; a three-state chemical cycle keeps positive populations, six positive rates, and all three stationarity equations while violating reverse-pair balance. The other witnesses retain the ensemble mean and individual rates, a bounded intermediate-time window, magnetic and Coriolis cross coefficients, distinct heat and general-transport pairs, the missing regression identification, a finite spiral-detection threshold, and a positive chemical formula domain that still fails the printed free-energy relation.
| Available fact | Conclusion not supplied | Lean witness |
|---|---|---|
| Positive entropy production | Reciprocal coefficients | positive_entropy_production_does_not_imply_reciprocity |
| Equilibrium and a stationary cycle | Pairwise detailed balance | equilibrium_and_stationary_cycle_do_not_imply_detailed_balance |
| Ensemble-average regression | Every path follows the macroscopic law | ensemble_average_regression_does_not_imply_pathwise_regression |
| Macroscopic validity | Validity through microscopic lag | macroscopic_validity_does_not_extend_through_microscopic_lag |
| Zero-field reciprocity | Same-field magnetic reciprocity | zero_field_reciprocity_does_not_imply_magnetic_same_field_reciprocity |
| Inertial-frame Stokes principle | Ordinary rotating-frame reversal or least dissipation | inertial_stokes_principle_does_not_extend_to_rotating_frame |
| Anisotropic heat theorem | General transport theorem in Part I | anisotropic_heat_result_does_not_prove_general_transport_theorem |
| Microscopic reversibility | Macroscopic reciprocity without regression | microscopic_reversibility_without_regression_bridge_does_not_yield_reciprocity |
| Equations (4.3)–(4.9) without reversal symmetry | Equation (4.11), ω₃ = 0 | equations_four_three_through_four_nine_do_not_supply_reversal_symmetry_or_zero |
| Sensitive null spiral search | Reciprocal heat coefficients | sensitive_null_spiral_search_does_not_establish_reciprocity |
Ten provenance, source-formula, and status audits
fluctuation_route_exposes_source_formula keeps the represented equations (4.3)–(4.10) visible as a fluctuation-route output. heat_reciprocity_retains_physical_regression_assumption and heat_reciprocity_records_regression_assumption_origin preserve the physical regression premise and its exact source step. crystal_spiral_result_retains_limited_evidence_status keeps the null search evidential, and qualified_conclusion_retains_crystal_spiral_assessment keeps that assessment in the final scope statement. approximation_result_retains_controlled_status preserves the asymptotic qualification. dissipation_result_records_isolated_boundary_specialization records both isolation and specialization. nonreversible_result_records_separate_magnetic_and_coriolis_origins keeps the two exceptions distinct. qualified_conclusion_retains_deferred_generalization and qualified_conclusion_retains_heat_reciprocity_derivation preserve the other sides of the final scope statement.
Shared-framework audit
reciprocal_transport_model_retains_paper_semantics verifies the exact zero-field model. onsager_heat_inputs_make_shared_reciprocal_route_applicable requires the additional regime, reversal, and coefficient bridges. onsager_heat_calculations_realize_structural_reciprocity_explanation realizes the ordinary route-bounded explanation, while onsager_heat_calculations_realize_source_structural_reciprocity_explanation retains the distinct token zeroFieldHeatFluctuationRegressionAndCorrelationSymmetry and the same raw paper premises. onsager_heat_setup_realizes_microscopic_field_reversal_physical_symmetry separately projects the reversal-fixed setup without assuming regression or reciprocity. onsager_heat_model_inputs_establish_theory_model_grounding grounds the model in linear irreversible thermodynamics and the selected anisotropic crystal only after receiving the selected fluctuation setup, near-equilibrium condition, and fixed zero field. The grounded theorem then combines that output-independent grounding with the direct technical result and transfers every shared claim.
Machine-checked audit boundary
argument_wellFormed, argument_auditable, routes_wellFormed, and routes_have_exact_predecessor_graph certify source structure. The six independent-input guards, downstream_setup_packages_reconstruct_predecessors_and_local_inputs, and the early and late result-step guards preserve the source-contract/application boundary. Coverage policy additionally rejects certificate extraction and ignored premise maps, checks each route's selected ClaimsHold atoms and paper-local bridge, requires the equation-(3.7)–(3.10) chemical formula output, and requires the equation-(4.3)–(4.10) fluctuation formula output. every_source_claim_has_semantics covers all forty-nine claims, and route_semantic_realization_is_exhaustive covers all nine routes. No paper calculation is hidden as a global axiom: every imported or reconstructed result remains a theorem parameter.
Lean-encoded bibliographic record
L. Onsager, Reciprocal Relations in Irreversible Processes. I., Physical Review 37 (1931), 405–426.
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 (131)
the_finite_pairing_retains_the_resistance_and_temperaturethe_finite_entropy_supply_is_the_actual_force_flux_pairingthe_actual_dissipation_is_quadraticthe_actual_functional_variation_retains_both_resistance_ordersthe_dissipation_directional_derivative_uses_the_symmetric_partreciprocal_constitutive_forces_are_actual_dissipation_derivativesreciprocal_resistance_gives_the_actual_potential_gradientthe_entropy_identity_holds_at_the_constitutive_flowreciprocity_and_the_constitutive_equation_give_the_exact_variation_gapnonnegative_dissipation_makes_the_constitutive_flow_a_maximumstrict_dissipation_also_gives_uniquenessstrict_dissipation_is_nonnegativean_active_constitutive_flow_has_a_nonvacuous_variational_maximumthe_physical_entropy_identity_is_not_an_identity_in_varied_flowsubstituting_the_physical_identity_before_variation_loses_the_maximumthe_coupled_resistance_has_an_actual_temperature_weighted_pairingthe_coupled_dissipation_and_entropy_supply_are_computedthe_coupled_resistance_is_reciprocal_and_strictly_dissipativethe_selected_coupled_flow_satisfies_the_actual_constitutive_equationthe_computed_coupled_flow_has_a_nonvacuous_unique_maximuma_constitutive_entropy_identity_does_not_hold_for_all_trialsreplacing_the_linear_entropy_supply_by_twice_dissipation_changes_the_extremumthe_variational_maximum_is_not_an_unconstrained_entropy_maximumthe_nonsymmetric_resistance_and_its_entropy_are_actual_functionsthe_nonsymmetric_resistance_is_strictly_dissipativethe_nonsymmetric_physical_flow_satisfies_its_constitutive_equationpositive_dissipation_and_a_constitutive_flow_do_not_supply_reciprocitypositive_dissipation_and_a_constitutive_flow_do_not_supply_a_variational_maximumthe_degenerate_resistance_has_a_real_undamped_directionthe_degenerate_source_is_reciprocal_nonnegative_and_constitutivenonnegative_dissipation_does_not_supply_strict_dissipationa_positive_dissipating_physical_flow_need_not_have_a_unique_maximumtransposing_the_resistance_preserves_dissipation_but_changes_the_forcethe_temperature_weight_in_both_physical_functionals_is_not_optionalthe_inverse_temperature_gradient_has_its_actual_derivativethe_constitutive_relation_uses_onsagers_normalized_temperature_forceinverse_reciprocal_conductivity_has_reciprocal_resistancethe_actual_spatial_resistance_pairing_inherits_reciprocitythe_pointwise_heat_law_identifies_the_actual_entropy_forcezero_normal_heat_flux_has_zero_boundary_entropy_exchangezero_divergence_has_zero_system_entropy_rateequal_prescribed_boundary_flux_has_equal_entropy_exchangethe_isolated_variation_keeps_the_boundary_constraintstationary_flow_turns_the_actual_functional_into_boundary_entropy_minus_dissipationthe_stationary_power_identity_holds_at_the_constitutive_flowstationary_power_constraints_turn_the_variational_maximum_into_an_entropy_boundprescribed_normal_flux_gives_least_dissipation_among_stationary_trialsthe_logarithmic_force_has_the_printed_first_order_expansionequation_three_nine_is_the_calibrated_logarithmic_forcethe_logarithmic_force_error_is_quadratic_in_relative_displacementrelative_displacement_controls_relative_force_errora_relative_displacement_cutoff_gives_a_uniform_force_error_tolerancelinearized_forces_reproduce_the_mass_action_displacement_ratessource_formula_retains_equations_three_seven_through_three_tenequation_three_ten_conserves_total_displacement_ratesource_formulas_use_the_actual_mass_action_ratesactual_free_energy_derivative_includes_the_number_changefixed_number_variations_remove_the_common_chemical_potentialthe_logarithmic_derivative_formula_is_exact_iff_total_variation_vanishesequation_three_eight_retains_the_conserved_displacementsource_chemical_variation_is_the_actual_constrained_derivativeforces_agree_on_conserved_variations_iff_they_differ_by_a_common_shifta_common_force_shift_preserves_equation_three_eightequations_four_nine_and_four_ten_force_equation_four_elevenequations_four_three_through_four_nine_do_not_supply_reversal_symmetry_or_zerothe_actual_heat_ensemble_realizes_nonvacuous_correlation_reversalthe_actual_stationary_reversible_heat_ensemble_has_symmetric_correlationsreciprocal_transport_model_retains_paper_semanticsthe_intermediate_time_contract_retains_actual_lag_separationheat_fluctuation_source_formula_forces_selected_coefficient_vanishesthermodynamics_constrains_but_does_not_supply_reciprocitychemical_linearization_retains_equations_three_seven_through_three_tenmicroscopic_reversibility_and_linearization_yield_chemical_reciprocitycorrelation_calculation_derives_the_actual_heat_correlation_symmetryfluctuation_reciprocity_result_exposes_heat_reciprocitymicroscopic_reversibility_supplies_equal_frequency_reverse_motionfluctuation_regression_and_correlation_symmetry_yield_heat_reciprocityfluctuation_calculation_retains_equations_four_three_through_four_tenfluctuation_reciprocity_result_retains_distinct_cross_force_pairreciprocal_heat_coefficients_retain_principal_axes_and_limited_spiral_evidencefluctuation_setup_realizes_shared_reciprocal_setuponsager_heat_inputs_make_shared_reciprocal_route_applicableonsager_heat_calculations_realize_structural_reciprocity_explanationonsager_heat_calculations_realize_source_structural_reciprocity_explanationonsager_heat_route_establishes_shared_reciprocal_transportonsager_heat_route_realizes_nonvacuous_reciprocal_transportonsager_heat_setup_realizes_microscopic_field_reversal_physical_symmetryonsager_heat_route_realizes_shared_reciprocal_transportonsager_heat_route_realizes_ordinary_zero_field_reciprocityonsager_heat_route_realizes_selected_cross_force_reciprocityonsager_heat_route_realizes_every_shared_reciprocal_transport_claimonsager_heat_model_inputs_establish_theory_model_groundingonsager_heat_route_establishes_theory_model_grounded_reciprocal_transportonsager_heat_route_transfers_every_shared_reciprocal_transport_claimintermediate_time_and_large_body_conditions_control_regressionmacroscopic_conduction_validity_realizes_regime_semanticsan_isolated_boundary_has_actual_zero_entropy_exchangethe_isolated_boundary_setup_supplies_the_trial_flow_restrictionsource_resistance_and_spatial_calculations_give_actual_variational_inputsreciprocal_resistance_yields_dissipation_variational_principlesstationary_flow_obeys_obstacle_and_prescribed_flux_principlesmagnetic_field_requires_modified_reversalcoriolis_rotation_qualifies_ordinary_reversal_and_dissipationmagnetic_field_reversal_and_coriolis_rotation_require_separate_qualificationsmagnetic_and_coriolis_results_form_nonreversible_qualificationpart_i_proves_heat_conduction_and_defers_general_transportpositive_entropy_production_does_not_imply_reciprocityequilibrium_and_stationary_cycle_do_not_imply_detailed_balanceensemble_average_regression_does_not_imply_pathwise_regressionmacroscopic_validity_does_not_extend_through_microscopic_lagzero_field_reciprocity_does_not_imply_magnetic_same_field_reciprocityinertial_stokes_principle_does_not_extend_to_rotating_frameanisotropic_heat_result_does_not_prove_general_transport_theoremmicroscopic_reversibility_without_regression_bridge_does_not_yield_reciprocitysensitive_null_spiral_search_does_not_establish_reciprocitya_named_chemical_rate_law_does_not_supply_equations_three_seven_through_three_tenthe_positive_chemical_reference_realizes_the_constrained_source_formulaschanging_total_amount_is_not_the_fixed_number_variationconstrained_variations_do_not_select_the_absolute_logarithmic_forcesthe_displaced_family_has_positive_source_datathe_displaced_family_keeps_a_detailed_balanced_referencethe_source_rate_law_reproduces_the_actual_displaced_kineticssubstituting_exact_forces_leaves_a_computed_rate_residualthe_exact_force_substitution_error_is_strict_at_positive_displacementthe_exact_force_substitution_still_agrees_to_first_orderarbitrarily_small_displacements_do_not_make_the_linearized_substitution_exactabsolute_displacement_does_not_control_the_force_error_uniformlyonsager_realizes_shared_field_reversal_boundaryheat_reciprocity_retains_regression_and_correlation_inputsvariational_principle_retains_reciprocity_and_explicit_calculationsgeneral_transport_conclusion_retains_deferred_status
Coverage theorems (13)
every_source_claim_has_semanticsthermodynamic_scope_route_is_semantically_realizedchemical_detailed_balance_analogy_route_is_semantically_realizedfluctuation_reciprocity_route_is_semantically_realizedfluctuation_route_exposes_source_formulacrystal_spiral_assessment_route_is_semantically_realizedregression_approximation_scope_route_is_semantically_realizeddissipation_variational_principle_route_is_semantically_realizedstationary_flow_route_is_semantically_realizedmagnetic_and_rotating_exceptions_route_is_semantically_realizedpart_i_scope_route_is_semantically_realizedall_routes_are_semantically_realizableroute_semantic_realization_is_exhaustive
Source-map audit theorems (26)
argument_wellFormedargument_auditableroutes_wellFormedroutes_have_exact_predecessor_graphapproximation_scope_is_local_to_its_regime_inputspart_i_scope_depends_on_certified_heat_reciprocity_and_crystal_assessmentthermodynamic_and_chemical_inputs_are_independent_hypothesesfluctuation_inputs_are_independent_hypothesescrystal_and_approximation_inputs_are_independent_hypothesesdissipation_variational_inputs_retain_derived_boundary_conditionsstationary_and_exception_inputs_are_independent_hypothesesscope_inputs_are_independent_hypothesesdownstream_setup_packages_reconstruct_predecessors_and_local_inputsearly_result_steps_apply_selected_inputs_and_contractslate_result_steps_apply_selected_inputs_and_contractsdependent_routes_consume_certified_predecessor_outputsheat_reciprocity_retains_physical_regression_assumptionfluctuation_route_exposes_source_formulaheat_reciprocity_records_regression_assumption_origincrystal_spiral_result_retains_limited_evidence_statusapproximation_result_retains_controlled_statusdissipation_result_records_isolated_boundary_specializationnonreversible_result_records_separate_magnetic_and_coriolis_originsqualified_conclusion_retains_deferred_generalizationqualified_conclusion_retains_heat_reciprocity_derivationqualified_conclusion_retains_crystal_spiral_assessment
Semantic atoms (49)
coupledTransportSetupthermodynamicPositivityCalculationthermodynamicInsufficiencyAssessmentcoupledTransportResultchemicalTriangleSetupchemicalMicroscopicReversibilitychemicalNearEquilibriumchemicalDetailedBalanceCalculationchemicalLinearizationCalculationchemicalDetailedBalanceResultfluctuationRegressionSetupregressionAssumptioncorrelationSymmetryCalculationcoefficientIdentificationheatReciprocityCalculationheatFluctuationSourceFormulafluctuationReciprocityResultcrystalSpiralSetupspiralNullEvidenceprincipalAxisCalculationcrystalSpiralResultregressionApproximationSetupregressionApproximationCalculationregressionApproximationResultdissipationLocalSetupdissipationSetupdissipationPotentialCalculationvariationalCalculationisolatedBoundarySetupisolatedZeroExchangeisolatedVariationalSpecializationdissipationVariationalResultstationaryFlowLocalSetupstationaryFlowSetupstationaryFlowCalculationstationaryFlowResultmagneticSystemLocalSetupmagneticSystemSetupmagneticOrdinaryFailureCalculationmagneticModifiedReversalCalculationmagneticQualificationResultcoriolisSystemSetupcoriolisQualificationCalculationcoriolisQualificationResultnonreversibleQualificationResultpartIScopeLocalSetuppartIScopeSetuppartIScopeAssessmentqualifiedPartIConclusion
Claim identifiers (49)
transportSetuppositivityCalculationthermodynamicAssessmenttransportResultchemicalSetupchemicalReversibilitychemicalNearEquilibriumbalanceCalculationlinearizationCalculationchemicalResultfluctuationSetupregressionAssumptioncorrelationCalculationcoefficientIdentificationreciprocityCalculationfluctuationSourceFormulafluctuationResultcrystalSpiralSetupspiralNullEvidenceprincipalAxisCalculationcrystalSpiralResultapproximationSetupapproximationCalculationapproximationResultdissipationLocalSetupdissipationSetuppotentialCalculationvariationalCalculationisolatedBoundarySetupisolatedZeroExchangeisolatedSpecializationdissipationResultstationaryLocalSetupstationarySetupstationaryCalculationstationaryResultmagneticLocalSetupmagneticSetupmagneticFailureCalculationmagneticModifiedCalculationmagneticResultcoriolisSetupcoriolisCalculationcoriolisResultnonreversibleResultscopeLocalSetupscopeSetupscopeAssessmentqualifiedConclusion
Step identifiers (49)
stateTransportSetupsupplyPositivityCalculationstateThermodynamicAssessmentderiveTransportResultstateChemicalSetupstateChemicalReversibilitystateChemicalNearEquilibriumsupplyBalanceCalculationsupplyLinearizationCalculationderiveChemicalResultstateFluctuationSetupstateRegressionAssumptionsupplyCorrelationCalculationstateCoefficientIdentificationsupplyReciprocityCalculationretainFluctuationSourceFormuladeriveFluctuationResultstateCrystalSpiralSetupstateSpiralNullEvidencecalculatePrincipalAxisConsequencederiveCrystalSpiralResultstateApproximationSetupsupplyApproximationCalculationderiveApproximationResultstateDissipationLocalSetupstateDissipationSetupsupplyPotentialCalculationsupplyVariationalCalculationstateIsolatedBoundarySetupstateIsolatedZeroExchangesupplyIsolatedSpecializationderiveDissipationResultstateStationaryLocalSetupstateStationarySetupsupplyStationaryCalculationderiveStationaryResultstateMagneticLocalSetupstateMagneticSetupsupplyMagneticFailureCalculationsupplyMagneticModifiedCalculationderiveMagneticResultstateCoriolisSetupsupplyCoriolisCalculationderiveCoriolisResultderiveNonreversibleResultstateScopeLocalSetupstateScopeSetupstateScopeAssessmentderiveQualifiedConclusion
Route identifiers (9)
thermodynamicScopechemicalDetailedBalanceAnalogyfluctuationReciprocitycrystalSpiralAssessmentregressionApproximationScopedissipationVariationalPrinciplestationaryFlowmagneticAndRotatingExceptionspartIScope
Route kinds (9)
thermodynamicInsufficiencychemicalKineticAnalogyfluctuationRegressionProofprincipalAxisAndNullEvidencecontrolledMacroscopicApproximationdissipationPotentialstationarySpecializationnonreversibleLimitationdeferredGeneralization
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.
thermodynamicScope
Logical kind: thermodynamicInsufficiency.
Required predecessor routes: none.
Ordered inference steps: stateTransportSetup, supplyPositivityCalculation, stateThermodynamicAssessment, deriveTransportResult.
Exported conclusions: transportResult.
chemicalDetailedBalanceAnalogy
Logical kind: chemicalKineticAnalogy.
Required predecessor routes: none.
Ordered inference steps: stateChemicalSetup, stateChemicalReversibility, stateChemicalNearEquilibrium, supplyBalanceCalculation, supplyLinearizationCalculation, deriveChemicalResult.
Exported conclusions: chemicalResult.
fluctuationReciprocity
Logical kind: fluctuationRegressionProof.
Required predecessor routes: none.
Ordered inference steps: stateFluctuationSetup, stateRegressionAssumption, supplyCorrelationCalculation, stateCoefficientIdentification, supplyReciprocityCalculation, retainFluctuationSourceFormula, deriveFluctuationResult.
Exported conclusions: fluctuationSourceFormula, fluctuationResult.
crystalSpiralAssessment
Logical kind: principalAxisAndNullEvidence.
Required predecessor routes: fluctuationReciprocity.
Ordered inference steps: stateCrystalSpiralSetup, stateSpiralNullEvidence, calculatePrincipalAxisConsequence, deriveCrystalSpiralResult.
Exported conclusions: crystalSpiralResult.
regressionApproximationScope
Logical kind: controlledMacroscopicApproximation.
Required predecessor routes: none.
Ordered inference steps: stateApproximationSetup, supplyApproximationCalculation, deriveApproximationResult.
Exported conclusions: approximationResult.
dissipationVariationalPrinciple
Logical kind: dissipationPotential.
Required predecessor routes: fluctuationReciprocity.
Ordered inference steps: stateDissipationLocalSetup, stateDissipationSetup, supplyPotentialCalculation, supplyVariationalCalculation, stateIsolatedBoundarySetup, stateIsolatedZeroExchange, supplyIsolatedSpecialization, deriveDissipationResult.
Exported conclusions: dissipationResult.
stationaryFlow
Logical kind: stationarySpecialization.
Required predecessor routes: dissipationVariationalPrinciple.
Ordered inference steps: stateStationaryLocalSetup, stateStationarySetup, supplyStationaryCalculation, deriveStationaryResult.
Exported conclusions: stationaryResult.
magneticAndRotatingExceptions
Logical kind: nonreversibleLimitation.
Required predecessor routes: fluctuationReciprocity, dissipationVariationalPrinciple.
Ordered inference steps: stateMagneticLocalSetup, stateMagneticSetup, supplyMagneticFailureCalculation, supplyMagneticModifiedCalculation, deriveMagneticResult, stateCoriolisSetup, supplyCoriolisCalculation, deriveCoriolisResult, deriveNonreversibleResult.
Exported conclusions: nonreversibleResult.
partIScope
Logical kind: deferredGeneralization.
Required predecessor routes: fluctuationReciprocity, crystalSpiralAssessment.
Ordered inference steps: stateScopeLocalSetup, stateScopeSetup, stateScopeAssessment, deriveQualifiedConclusion.
Exported conclusions: qualifiedConclusion.