Formal reconstruction - exact projection, force-memory relation, canonical statistical interpretation, collective variables, thermal after-effect, and transport
Transport, Collective Motion, and Brownian Motion
Mori's complete 1965 logical route, with exact identities, controlled approximations, physical postulates, and open comparisons kept distinct
Definitions, structures, and assumptions
Structures, classes, and inductive alternatives
- structureProof-free ordinary constraint for one selected exact memory reduction. It retains the physical indices shared by independent derivations but no proof that the exact route applies and no exact-reduction output.
- structureThe selected exact history-dependent reduction phenomenon.
- structureProof-free source constraint for one paper-local exact memory derivation. It retains the ordinary exact-memory constraint and derivation vocabulary but no proof that the derivation obtains and no exact-reduction output.
- structureThe selected-variable equation obtained on the reduced side.
- structureThe full-dynamics side of one selected exact reduction.
- structureThe retained memory and residual-force content of the exact equation.
- structure
- structure
- inductive
- structure
- structure
- structureProof-free data selecting one exact memory-kernel reduction.
- structure
- structure
- structure
- structure
- structure
- inductive
- inductive
- inductive
- structure
- inductive
- structure
- structureA selected claim must depend on exactly these source-map steps.
- structureA selected claim must retain exactly these epistemic statuses.
- structureA selected route must name exactly these immediate predecessor routes.
- structure
- structure
- inductive
- structure
- inductiveSource-native derivation selected from Mori's exact projection argument.
- structure
- structurePhysical data and proposition-valued relations used by Mori's paper.
- structure
- structureA finite scalar-component readout of equation (3.10). The four complex slots retain the derivative, frequency action, causal memory contribution, and orthogonal force, so a named memory-kernel result cannot stand in for the printed value-level equation.
- structure
- structureA hydrodynamic reduction may retain a conserved slow mode in a local equation without identifying that local equation with the exact memory equation. This finite model blocks an accidental upgrade from controlled reduction to exact prediction identity.
- structure
- structureThe ordinary-force correlation and Mori's projected damping kernel are not interchangeable. In this finite model the ordinary correlation has the slow tail, while only the distinct projected kernel evolved by the complement propagator avoids the plateau cancellation.
- structure
- structure
- structure
- inductive
- inductive
- inductive
- structure
- structure
- structure
- structureProof-free semantics for one selected response problem. The two time arguments of `responseDependsOnAt` and `responseKernelSupportsAt` are, respectively, the source time and response time.
- structure
- structure
Definitions and domain choices
- definition
- definition
- definition
- definitionOrdinary finite-cutoff convergence is separate from Abel regularization.
- definition
- definitionA finite-time residual bound, not a statement that nearby trajectories exist.
- definition
- definitionThe operator order is kernel followed on the right by the carrier.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- 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 field window and an error per unit field, not an exact finite-field law. The radius belongs to the selected ensemble, coupling, observable, and tolerance.
- definitionThe finite physical ensemble is inhabited and normalized; the response may vanish. A response coefficient is a derivative, not a finite-field difference.
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe first-order prediction uses the same unperturbed ensemble as the exact preparation.
- definition
- definition
- definitionThe finite canonical weights define a genuine probability mass function, not an independent law supplied by a physical assumption.
- definition
- definitionA static conjugate field changes the energy, and therefore the normalized populations.
- definition
- definition
- definition
- definitionA centered probability law realizing the matrix, not an assigned covariance alone.
- definition
- definition
- definition
- definition
- definitionStationarity is needed on the observed force, not on every ambient coordinate.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe entire observed past and the current state give the same predictions of all L1 queries.
- definitionExact closure is a property of the selected observation, not of all hidden coordinates.
- definitionA genuine fluctuating observable, in addition to valid conditional prediction.
- definition
- definition
- definition
- definitionSource-sensitive explanation of the selected exact memory reduction.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe exact selected model with both premise layers needed to interpret the exact and localized equations. No reduction, correlation, localization, or equation output is assumed.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionSource-sensitive structural semantics for the exact reduction. It retains the ordinary exact-memory constraint and phenomenon, while satisfaction additionally requires a realized typed paper derivation.
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe nonvacuous derivational-reduction result. Besides the universal bridge, it requires one actual selected realization, supported exact memory behavior, and exhibited reduced equation.
- definitionOne source-sensitive exact memory-kernel derivational reduction.
- definitionThe actual exact-reduction setup carried by one proof-free model. This is model-native rather than implication-valued: the selected system, environment, variables, dynamics, construction, exact regime, and exact scope really satisfy the premises needed before an exact memory calculation can be used.
- definitionThe actual short-memory setup carried by one proof-free model. The exact reduction is retained separately in the complete result below; this predicate records the additional local-regime validity and time-scale separation that license a localized-memory calculation.
- definitionThe realized exact reduction and force-memory relation at one model.
- definitionThe realized short-memory localization at one model.
- definitionThe complete realized exact-plus-local memory-kernel result at one proof-free model. It conjoins the independently meaningful exact and local outputs and contains no implication-valued calculation contract.
- definitionThe direct exact memory phenomenon, without setup or implication-valued calculation contracts.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe shared physical indices constraining the selected exact route.
- definitionThe exact selected model indices retained by the explained phenomenon.
- definitionThe exact model and typed paper derivation selected as source constraint.
- definitionThe selected reduced equation and variables.
- definitionThe selected full-dynamics description on the exact-reduction side.
- definitionThe selected memory kernel and residual force retained in the reduction.
- definition
- definition
- definition
- definition
- definitionDerivational-reduction semantics for the exact memory-kernel stage. Realization retains the full-dynamics setup, micro support retains the performed reduction and memory/force calculations, and macro exhibition is the actual exact reduced equation. The later short-memory approximation is absent.
- 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
- definitionEvery claim in the supplied identifier list holds.
- definitionA source-mapped step is semantically sound when the interpreted premises imply the interpreted conclusion. Physical principles and imported calculations therefore remain explicit hypotheses of paper-specific certificates rather than acquiring truth from their source-map labels. A reductio hypothesis is different: it introduces a temporary assumption into a subargument and therefore is not required to hold globally. Its later uses remain ordinary premise-sensitive steps, and discharging it into a negated conclusion remains an ordinary semantic obligation.
- definitionEvery step in the supplied identifier list is semantically sound.
- definition
- definition
- definition
- definition
- definition
- definitionThe formula declared for a claim identifier, when that claim is present.
- definition
- definitionEvery source-mapped step whose justification contributes to the claim through declared premise-to-conclusion steps.
- definitionAll justification statuses contributed by the exact source-mapped origins of a claim. This records epistemic provenance; it does not assert any paper claim or discharge any physical assumption.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe declared argument step with the requested identifier, when present.
- definition
- definitionThe premise list and conclusion attached to a declared step identifier.
- definition
- definition
- definition
- definition
- definitionThe complete Lean-side fidelity certificate. The first conjunct is computed from source-map data; the second is supplied by checked route semantics; the third requires each declared independence boundary to have a countermodel.
- definition
- definition
- definition
- definition
- definitionA typed countermodel matrix avoids string-keyed audit rows. Each index selects one proposition-valued separation obligation.
- definition
- definitionEvery route actually declared in the source map has a semantic certificate under the paper-local interpretation.
- definition
- definition
- definitionOne countermodel row retains a weaker proposition while rejecting a stronger upgrade. This is a proposition, not a structure carrying proof fields.
- definition
- definition
- definitionIndependent dependency and epistemic ledgers must review the same actual source claims, including every public conclusion and the selected paper conclusion. Empty, duplicated, nonexistent, or one-sided entries are invalid.
- definitionEvery actually declared source route must have exactly one independently reviewed predecessor row. Correct rows for a selected subset are insufficient.
- definitionThe declared main conclusion must be exposed by at least one public route output, rather than existing only as an unexported source-map claim.
- definition
- definition
- definitionTwo finite lists describe the same dependency set. Duplicate expected entries are rejected so a ledger cannot pass by repeating a label.
- definitionEvery paper-level, claim-level, and step-level source reference is present and has a nonempty work and locator. PaperArgument.auditable separately checks that every claim and step carries at least one source.
- definitionA source reference is usable for review only when both the work and its locator are nonempty.
- definitionStatic fidelity checks that can be evaluated from a paper's source map alone. They do not assert the truth of any physical premise.
- definitionEvery declared output of a named source route holds under the semantic interpretation. This is the proof obligation discharged by paper-specific Lean theorems.
- definition
- definitionA route is fully certified only when both its individual steps and its declared outputs are semantically checked.
- definitionEvery source-mapped inference step in a named route is semantically sound.
- definitionEvery route named in the supplied identifier list is semantically certified.
- definition
- definition
- definition
- definition
- definition
- definitionThe source-mapped route with the requested identifier, when present.
- definition
- definitionThe public semantic interface inherited from predecessor routes. Descendants receive only declared route outputs, not every internal intermediate claim. Outputs still carrying a temporary reductio origin are excluded.
- definitionAll direct and inherited route dependencies. The route-order check separately ensures that the declared graph is acyclic and topologically ordered.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe first-order expression (4.6)-(4.7), not an exact normalized nonequilibrium law.
- definition
- definition
- definition
- definition
- definition
- definitionThe finite initial-value characterization of the two source exponentials.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionTwo nonzero but identical selected observables violate equation (2.17).
- definition
- definition
- definition
- definitionThe residual coordinate is the initial momentum, with unit equilibrium variance.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe complete result already contains the certified hydrodynamic branch. This compatibility endpoint keeps the older explicit setup-plus-result projection available to downstream audits without reducing the enlarged paper result.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionOriginal journal p. 431, equation (3.8): the damping matrix is the orthogonal-force correlation multiplied by the inverse selected-variable covariance matrix.
- definitionOriginal journal p. 431, equation (3.11): the random force stays orthogonal to the selected-variable subspace.
- definitionOriginal journal p. 431, equation (3.10): the selected-variable column obeys the exact generalized Langevin equation componentwise.
- definitionOriginal journal p. 430, equation (3.3): the non-secular force is the complement-propagated vertical force. Equation (3.4)'s construction of that propagator remains the separate complement-propagator premise of the route.
- definitionOriginal journal p. 431, equation (3.12): the random-force two-time correlation is the damping matrix times the selected-variable covariance.
- definitionThe source's central exact-memory formulas retained together. This bundle keeps the propagated force, damping definition, causal equation, orthogonality, and fluctuation-dissipation relation visible at value level.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionRaw source premises constituting Mori's exact-memory derivation.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionEquations (3.13)-(3.20) distinguish the correlation of the ordinary force from the damping kernel built from Mori's orthogonal force. The former retains the slow secular tail and develops the plateau-value cancellation; the latter uses the complement propagator and excludes that tail. This is a paper-local physical argument, not a generic memory-kernel theorem.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe selected matrix equation has a nonempty, nonsingular covariance domain.
- definitionEquations (2.13) and (2.17) require a genuine selected covariance inverse.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionComponent of the frequency-matrix action on Mori's selected-variable column. The finite component set is selected data; the matrix multiplication is not hidden inside the opaque equation token.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionComponent of the causal memory convolution in equation (3.10). Its causal limits and kernel action are literal; the formula below separately records the imported interval-integrability premise needed to use this value.
- definitionIntegrand of the causal memory convolution in equation (3.10).
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionEquation (3.17) retains the rotating carrier and the positive Abel regulator.
- definition
- definitionThe source's exp(-i Omega s), characterized by its actual linear dynamics.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- 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 bridge principle derives a macro behavior from any realizing microdescription that supports it.
- definition
- definition
- definition
- definitionThe selected response kernel has no support from a later source time.
- definitionFor the selected problem, dependence holds exactly when stimulus and response occur and the response kernel connects their times.
- definitionThe represented response kernel has one occurring source-response pair.
- definitionEvery declared dependence has a source no later than its response.
- definitionThe selected response relation is physically inhabited by an occurring stimulus, an occurring response, and a dependence between them.
- definitionA nonvacuous retarded response: all response dependence is past-supported and at least one occurring stimulus-response pair realizes that dependence.
- 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
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
Source mappings and interpretation choices
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- 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
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- 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
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- 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
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- 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
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- definition
- definition
- checked statement
- definition
- definition
- definition
- definition
- definition
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- 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
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- structure
- definition
- instance
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- constructor
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- checked statement
- checked statement
- checked statement
- recursor
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- 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
- 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
- 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
- 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
- checked statement
- definition
- checked statement
- definition
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- checked statement
- definition
- definition
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- checked statement
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- definition
- checked statement
- definition
- definition
- checked statement
- checked statement
- definition
- definition
- checked statement
- definition
- definition
- definition
- definition
- checked statement
- definition
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
Checked statements: parameters, hypotheses, and interpretation
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe amplitude can be arbitrarily small while the conjugate coupling grows. Each model still has zero derivative at zero. The finite bias remains fixed.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementFinite classical specialization of (4.5)-(4.7): orthogonality gives an error small compared with the preparation field on a model-dependent window. This is neither exact cancellation nor a time-uniform estimate.
- checked statementThe residual observable is the existing projected force, evaluated on the same sampled initial state. Its centeredness and cross moment follow from the equilibrium covariance and matrix orthogonality, not response assumptions.
- checked statementThe finite classical part of (4.5)-(4.7). The same force observable is evaluated in the normalized prepared ensemble at every field amplitude.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked 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 (3.10) for a unit-frequency equilibrium oscillator retaining its position.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementNaming a force-correlation result does not retain equation (3.10)'s componentwise exact-memory equality. The source route must project the complete formula package from the checked correlation result.
- checked statement
- checked statement
- checked statement
- checked statement
- checked 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 completed force-correlation route retains equations (3.3), (3.8), (3.10), (3.11), and (3.12), rather than only an opaque memory-kernel label.
- checked statement
- checked statementThe exact projection result keeps the propagated-force equation, the literal causal generalized Langevin equation, and random-force orthogonality.
- checked statement
- checked statementAdding Mori's hydrodynamic branch to the complete paper logic does not erase the short-memory qualification. The selected local equation remains an approximation both in the local calculation and in the paper's final scope assessment.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementMori's exact projection route gives a derivational bridge from the selected full dynamics to the reduced memory equation. This claim does not use or establish the subsequent local-in-time approximation.
- checked statement
- checked statement
- checked statement
- checked statementMori's selected-variable, Hilbert-space, and projection premises realize the shared exact setup without assuming the later short-memory limit.
- checked statement
- checked statement
- checked statement
- checked statementMori's exact projection, force-correlation, and controlled short-memory routes realize the direct shared result rather than only implication-valued calculation contracts. Primary-source anchors: journal pp. 429-431 for the exact projected equation and force-memory identity, and pp. 431-433 for the qualified local approximation.
- checked statement
- checked statement
- checked statement
- checked statementOriginal pp. 428-431: projection geometry, orthogonal propagation, the exact generalized Langevin equation, and the orthogonal-force correlation make the shared exact memory route applicable directly from their source calculations.
- checked statementMori's source calculations realize exact memory-kernel derivational reduction before an `EstablishedForceCorrelation` or shared established endpoint is packaged. The local-in-time approximation is not used.
- checked statementMori's raw projection inputs realize the source-sensitive exact-memory derivational reduction without identifying this orthogonal-subspace route with Zwanzig's solvable-bath elimination. Primary-source anchors: original paper OCR lines 201-205 and 327-340 for the projection construction, lines 394-475 for orthogonal propagation, the exact memory equation, and the force-correlation relation.
- checked statementMori's projection and orthogonal-force calculations source-sensitively explain the selected exact memory-kernel phenomenon before any completed endpoint.
- checked statement
- checked statementRoute-level plateau composition keeps the ordinary-force result explicit after its own calculation step and applies only the remaining projected calculation.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementRoute-level composition of Mori's projection derivation. The intermediate geometry and orthogonal-dynamics results stay explicit so source coverage can consume the exact conclusions named by the route rather than recomputing them.
- checked statement
- checked statementRoute-level response comparison keeps the already checked response difference explicit before applying the controlled normal-limit calculation.
- checked statementRoute-level canonical-product composition consumes the already checked scalar-product result before applying the independent path interpretation.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementRoute-level thermal composition consumes the checked density, projected-flux, and after-effect results before applying the independent causality contract.
- checked statementRoute-level transport composition retains the checked projected-flux, ordered- limit, and identification results before applying the dilute-gas reduction.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- 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
- 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
- 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
- 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
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
External mathematical declarations
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
This edition is derived only from Mori1965.lean, Mori1965/SourceMap.lean, and Mori1965/Coverage.lean. Equations (3.3), (3.8), and (3.10)-(3.12) are proposition-valued formulas over a nonempty selected-component domain, complex values, an actual derivative, finite matrix sums, and a causal interval integral; differentiability and interval-integrability are explicit premises, while analytic evaluation and operator construction remain theorem premises. The force-correlation route now exports that complete formula package through retainExactMemoryFormulaPackage only after recovering the checked correlation result. Established results retain physical setups and outputs, never implication-valued proof payload. Coverage recovers each selected input from a checked ClaimsHold map; route certificates establish availability only. The prose below reports that formal logic; it does not replace it.
The paper has one root and sixteen dependent routes
The exact projection reduction is the only independent physical route. Force correlation and canonical scalar-product selection depend on it. Plateau resolution and short-memory localization are sibling children of force correlation. Everything later consumes certified outputs rather than restating them as assumptions.
The policy audit checks all fifteen established-result families and the three shared-adapter entry points. Calculation and assessment contracts stay visible in the source graph, but downstream physics receives the direct outputs they establish. Final projection, plateau, canonical-scalar-product, thermal, response, and transport steps consume their checked intermediate outputs rather than replaying the upstream calculations.
routes_have_exact_predecessor_graph and local_and_plateau_routes_are_siblings_after_force_correlation.Projection geometry and complementary evolution produce an exact memory equation
The setup retains a closed system, variables with invariant parts removed, no time-dependent external force, and at most a uniform magnetic field. It separately specifies the dynamical-variable Hilbert space, scalar-product properties, Hermitian Liouville dynamics, and the relevant projection.
with f(t) complement-propagated and (f(t), A*) = 0.
EquationThreeThreeOrthogonalForceFormulaAt, EquationThreeTenExactGeneralizedLangevinFormulaAt, EquationThreeElevenForceOrthogonalityFormulaAt, pp. 430-431(1)The source route first checks geometry and orthogonal dynamics as separate results, then composes them through projection_intermediate_results_establish_reduction. The final step does not rerun the calculations that already produced those intermediate outputs. exact_projection_reduction_retains_equations_three_three_ten_and_eleven checks that the established projection result still carries the propagated-force formula, literal causal equation, and orthogonality relation instead of only the equation token.
A second independent calculation establishes the generalized second fluctuation-dissipation relation:
and (f(t1), f(t2)*) = phi(t1-t2) (A, A*).
EquationThreeEightDampingKernelFormulaAt, EquationThreeTwelveFluctuationDissipationFormulaAt, established_force_correlation_retains_core_exact_memory_formulas, p. 431(2)force_correlation_route_exposes_core_exact_memory_formula_package checks that the route exports the complete exactMemoryFormulaPackage through the separate exactMemoryFormula claim, and named_force_correlation_result_does_not_supply_equation_three_ten_formula blocks replacing equation (3.10)'s derivative-frequency-memory-force equality by a result label.
SelectedCovarianceInverseAt now requires the actual two-sided covariance inverse in equations (2.13) and (2.17). The independent FiniteProjection model computes the Gram matrix, projector, complement, and vertical force. gram_inverse_makes_the_projection_idempotent and gram_inverse_makes_the_vertical_force_orthogonal check the operations themselves.
A'(t) + integral0t A(s) ds = f(t).
oscillator_satisfies_the_exact_memory_equation - projected_force_realizes_shared_residual_covariancePlateau resolution and local damping answer different questions
The ordinary force correlation contains the long cancellation tail. The projected damping kernel uses complementary propagation and excludes it. This is the content of complement_propagator_separates_damping_kernel_from_plateau_correlation and plateau_resolution_retains_distinct_correlation_roles.
The local equation instead requires finite kernel decay, slower macroscopic relaxation, and explicit time-scale separation. It follows from separated_time_scales_yield_qualified_local_langevin_approximation without taking the plateau conclusion as a premise.
The computed oscillator provides a sharper control: full_evolution_does_not_preserve_force_orthogonality rejects the wrong propagator, and exact_projection_does_not_imply_decaying_memory proves that its exact damping kernel does not tend to zero. An exact memory identity is not a short-memory hypothesis.
Countermodel boundary
identifying_ordinary_and_projected_correlations_breaks_plateau_resolution retains distinct ordinary/projected secular tails and complement/plateau residuals, rejecting one-kernel collapse. hydrodynamic_reduction_does_not_identify_exact_and_local_equations instantiates an inhabited conserved slow mode at zero wave number and positive observation time while the exact memory and local damping weights remain distinct.
The rotating coefficient and finite-history error are separate objects
Equations (3.15)-(3.17), pp. 431-433, compare a slowly relaxing rotating history with its local coefficient. FreeCarrierDynamics gives the carrier its actual generator; slow relaxation does not mean small oscillation frequency. The coefficient uses the source's positive-regulator prescription.
The finite-memory equation requires integrability on [0,t].
U(s) = exp(-i Omega s); C(t) = integral_0^t K(s) U(s) ds.
Gamma = lim_{epsilon -> 0+} integral_0^infinity exp(-epsilon s) K(s) U(s) ds.
The matrix order K(s) U(s) is retained; Gamma can be complex.
For K(s)=exp(-s)/100 and Omega=1: Gamma=(1-i)/200, not 1/100.
exponential_memory_has_the_finite_rotating_coefficient computes the finite coefficient, and the_exponential_family_realizes_moris_abel_prescription independently checks the regulated limit. The shared memory identity retains both finite-time errors. Its primitive version integrates the kernel before taking norms, preserving oscillatory cancellation.
For the scalar rotating channel: g(s)=U(-s)A(t-s), P'=K U, P(0)=0.
||M(t)-Gamma A(t)|| <= endpointError ||A(0)|| + rate integratedError.
Each bound is an explicit input on [0,t]; rate controls g', not Omega.
primitive_errors_in_the_rotating_frame_control_the_actual_memory proves this scalar bound with explicit regularity and error inputs. a_rotating_exponential_memory_has_an_inhabited_localization_readout supplies an actual nonzero shared readout. These regular-channel diagnostics do not construct the full microscopic Mori ensemble or establish global trajectory closeness.
C(2 pi n)=0 for every natural n.
The Abel coefficient alone does not give C(t) -> Gamma.
the_abel_coefficient_does_not_supply_finite_cutoff_convergence proves the missing implication is false. Neither the Abel limit nor the exact projection equation supplies a numerical localization budget by itself.
The canonical scalar product carries a statistical selection argument
Mori chooses the canonical Kubo scalar product so that the orthogonal force has zero mean in the linearized constrained ensemble. Neglecting that force then describes the most-probable linear path. canonical_zero_mean_requirement_selects_most_probable_linear_path also retains the distinction from the symmetrized quantum correlator and records that almost-all-initial-ensemble typicality is proposed but not established.
With definite time-reversal parities and magnetic-field reversal, canonical_projection_and_reversal_symmetry_establish_reciprocity retains projection invariance, the frequency-matrix parity structure, force-correlation reversal, Onsager reciprocity, kinetic dispersion relations, wave-vector orthogonality, and the zero-field even/odd classification.
One initial ensemble determines the entire force process
Original pp. 433-434, equations (4.1a), (4.2), and (4.4)-(4.7), ground this finite classical realization. The quantum Kubo scalar product in (4.1b) is not identified with a classical joint probability law. the_classical_force_readout_is_the_dual_of_orthogonal_evolution retains the complementary observable propagator rather than substituting full microscopic evolution.
f(t)=U_perp(t)V; F(t,z)=f(t)^T z.
E_mu[F(t)F(s)^T]=f(t)^T C f(s).
Every joint force law is the pushforward of one initial z.
classical_initial_sampling_realizes_the_source_force_correlation turns the source matrix into an actual ensemble integral. source_orthogonality_is_an_actual_classical_zero_cross_moment needs no Gaussian or independence assumption. The first-order preparation expression retains the source's epistemic scope:
Source orthogonality gives m_j^(1)(t)=0.
This is a linear-order mean, not an exact nonequilibrium law or a typicality theorem.
classical_orthogonality_removes_the_force_mean_at_linear_order proves this cancellation, without asserting an exact normalized nonequilibrium law. The concrete oscillator also satisfies its actual memory equation for every initial sample, with its derivative and finite integral checked.
q(0)=q0; q'(t)=p0-integral_0^t q(s) ds; F(t)=p0.
Unit Gaussian preparation: E[F]=0, E[F^2]=1; F(t) and F(s) are not independent.
Fixing (q0,p0) gives a Dirac joint force law.
Four-phase law: same covariance, but P(F=0)=1/2 instead of 0.
the_canonical_oscillator_has_an_actual_nonzero_residual_process and the_canonical_oscillator_force_has_stationary_gaussian_joint_laws realize genuine noise statistics. Nevertheless, stationary_projected_noise_does_not_require_ambient_covariance_preservation rejects a stronger ambient invariance premise. Zero mean does not remove fluctuations. The noncanonical four-phase control retains orthogonality but not statistical independence, and the_same_projected_covariance_can_give_different_joint_force_laws rejects reconstruction of full laws from covariance alone.
Which state is sufficient for prediction?
Original pp. 437-438, equation (5.1), concern a collective composition law on a selected time scale and evolution along the most-probable path. That criterion is not identified with a probabilistic Markov theorem. The shared MarkovOn instead compares actual conditional predictions:
H_t=sigma(X_s: s in D, s<=t); C_t=sigma(X_t).
For every measurable g with g(X_u) in L1(mu), and t<=u in D:
E_mu[g(X_u)|H_t]=E_mu[g(X_u)|C_t] almost surely.
Nonvacuous prediction additionally requires an L2 observed query of strictly positive variance.
the_full_phase_state_has_nonvacuous_markov_predictions proves this property for the actual full oscillator state. The position-only process does not have it; this is a statement under the normalized Gaussian law, not an inference from two isolated microscopic points.
q(0)=q0; q(pi/2)=p0; q(pi)=-q0.
E[q(pi)|H_(pi/2)]=-q0; E[q(pi)|q(pi/2)]=0 almost surely.
Var(q0)=1: position alone is not Markov; the full (q,p) state is Markov.
q'(t)=p(t) does not close position alone.
Complementary F(t)=p0 is Markov while the position memory kernel K(t)=1 does not decay.
restoring_momentum_restores_markov_prediction_but_position_alone_fails and a_local_position_equation_does_not_make_position_a_markov_state keep the selected state explicit. the_projected_force_is_markov_while_the_position_memory_does_not_decay distinguishes the force process from the position process. These are finite classical boundary realizations, not a universal classification of Mori's collective variables.
Good collective variables are selected by a dynamical criterion
separated_relaxation_selects_good_collective_variables encodes the semigroup/time-scale equivalence, the conserved long-wavelength class, weak-exchange modes, microscopic equation-of-motion modes, and failure diagnostics for incomplete variable sets.
conserved_slow_variables_realize_hydrodynamic_reduction, mori_hydrodynamic_reduction_retains_a_conserved_slow_variable, and hydrodynamic_setup_establishes_scoped_slow_mode_reduction realize the shared hydrodynamic interface without upgrading the local approximation. spin_oscillator_and_fluid_examples_test_collective_variable_selection keeps Mori's spin-wave, harmonic-coordinate, sound, plasma, and bad-set tests paper-local.
Projected density history yields an exact retarded thermal after-effect law
The time-dependent nonequilibrium ensemble and the local-equilibrium ensemble are distinct selected objects. The first is decomposed into projected and orthogonal parts. Complementary evolution gives an exact history retaining the initial deviation. The thermodynamic forces pair with projected conjugate fluxes orthogonal to the relevant variables.
implies an exact retarded thermal after-effect equation with initial memory and fluctuation correlation retained.
projected_density_and_flux_calculations_establish_thermal_after_effect and established_thermal_after_effect_realizes_retarded_response, pp. 441-445(3)The latter theorem exposes an actual RetardedResponseAt, so the shared response-causality import is used semantically rather than decoratively.
Two extra-premise routes lead from exact fluctuations to macroscopic transport
finite_kernel_memory_yields_exact_aged_fluctuation_law removes the initial memory in the aged limit but retains the fluctuation term. onsager_regression_and_low_frequency_steps_yield_transport_law reaches a phenomenological law only after adding the regression postulate, neglecting fluctuations, and assuming low frequency relative to kernel decay.
local_equilibrium_contraction_yields_average_final_stage_transport uses a different route: a local-equilibrium initial condition, relevant projection as contraction, and a typicality premise. two_transport_routes_retain_distinct_extra_premises prevents their identification.
projected_flux_and_propagator_distinguish_thermal_from_mechanical_response retains both differences: projected versus unprojected flux and complement versus full propagation. Conditional agreement occurs only under an ordered normal-system limit and excludes named plasma, phonon, and magnon cases. ordered_limit_agreement_does_not_supply_finite_wavevector_equality blocks a stronger conclusion.
projected_flux_and_ordered_limits_establish_transport_coefficients retains the explicit projected-flux formulas, ordered limits, conductivity/diffusion/viscosity identifications, hydrodynamic equations, nonlinear qualification, molecular expressions, and dilute-gas Boltzmann and Enskog-Chapman reduction. bare_flux_does_not_inherit_projected_collision_invariant_orthogonality protects the key projected-flux role.
The shared framework remains deliberately narrower than Mori's paper
MemoryKernelReductionContext shares only the independently repeated Mori-Zwanzig pattern: exact reduced equation, eliminated-sector memory, residual-force relation, and qualified localization. Its established records remain output-led, but mori_projection_setup_realizes_shared_selected_exact_memory_setup projects Mori's source setup directly. mori_source_inputs_make_shared_exact_memory_route_applicable then applies projection geometry, orthogonal dynamics, exact-equation, and force-correlation calculations in source order. mori_source_inputs_realize_exact_memory_derivational_reduction realizes the ordinary derivational reduction, while mori_source_inputs_realize_source_exact_memory_derivational_reduction retains Mori's typed orthogonal-projection provenance; both precede any completed force-correlation or shared endpoint. mori_source_inputs_realize_structural_exact_memory_kernel_explanation independently necessitates the exact selected memory phenomenon without using the later short-memory route. The older mori_force_correlation_realizes_shared_nonvacuous_exact_reduction, mori_exact_reduction_realizes_derivational_reduction, and mori_local_result_realizes_shared_nonvacuous_reduction retain the direct-output audit path.
mori_setups_realize_shared_selected_memory_kernel_setup limits theory/model/world grounding to projection and local-approximation premises. No exact equation, force-correlation, localization, or local-equation output is supplied by grounding.
Mori's canonical ensemble, time reversal, plateau mechanism, thermal conjugate fluxes, response comparison, and transport coefficients remain local. The paper is not forced into the existing shared mechanical-response transport component because its thermodynamic force is a state function that evolves with the system.
The final scope keeps Mori's comparison with Zwanzig unresolved. scope_distinguishes_exact_reduction_from_local_and_transport_claims, complete_mori_1965_logic, complete_result_and_hydrodynamic_setup_establish_full_scoped_logic, and full_scoped_logic_retains_hydrodynamic_reduction_and_approximate_status preserve the complete result and its qualifications.
The twenty-four inhabited fidelity boundaries are physical rather than label-based. In addition to the source equation, response, transport, and typicality controls, they check actual full/complement propagation, nondecaying oscillator memory, and duplicated observables whose inverse-named matrix cannot produce a projector. The shared finite covariance operation is used by projected_force_realizes_shared_residual_covariance; the full complex and infinite-dimensional mathematics is not replaced by this finite test sector.
Machine-checked semantic ledger
argument_wellFormed, argument_auditable, routes_wellFormed, every_source_claim_has_semantics, and route_semantic_realization_is_exhaustive establish structural and semantic coverage.
Primary semantic theorems
projection_and_orthogonal_evolution_derive_exact_generalized_langevin_equation projection_intermediate_results_establish_reduction exact_projection_reduction_retains_equations_three_three_ten_and_eleven random_force_correlation_establishes_memory_kernel_relation established_force_correlation_retains_core_exact_memory_formulas complement_propagator_separates_damping_kernel_from_plateau_correlation plateau_intermediate_results_establish_resolution plateau_resolution_retains_distinct_correlation_roles separated_time_scales_yield_qualified_local_langevin_approximation canonical_zero_mean_requirement_selects_most_probable_linear_path scalar_product_result_and_path_interpretation_establish_canonical_result canonical_projection_and_reversal_symmetry_establish_reciprocity separated_relaxation_selects_good_collective_variables conserved_slow_variables_realize_hydrodynamic_reduction mori_hydrodynamic_reduction_retains_a_conserved_slow_variable hydrodynamic_setup_establishes_scoped_slow_mode_reduction spin_oscillator_and_fluid_examples_test_collective_variable_selection projected_density_and_flux_calculations_establish_thermal_after_effect thermal_intermediate_results_and_causality_establish_after_effect established_thermal_after_effect_realizes_retarded_response finite_kernel_memory_yields_exact_aged_fluctuation_law onsager_regression_and_low_frequency_steps_yield_transport_law local_equilibrium_contraction_yields_average_final_stage_transport two_transport_routes_retain_distinct_extra_premises projected_flux_and_propagator_distinguish_thermal_from_mechanical_response response_difference_and_normal_limit_establish_comparison projected_flux_and_ordered_limits_establish_transport_coefficients transport_intermediate_results_and_dilute_gas_establish_chain scope_distinguishes_exact_reduction_from_local_and_transport_claims complete_mori_1965_logic complete_result_and_hydrodynamic_setup_establish_full_scoped_logic full_scoped_logic_retains_hydrodynamic_reduction_and_approximate_status
Shared memory-kernel adapter
memory_kernel_model_retains_mori_semantics mori_setups_realize_shared_selected_memory_kernel_setup mori_projection_setup_realizes_shared_selected_exact_memory_setup mori_source_inputs_make_shared_exact_memory_route_applicable mori_source_inputs_realize_exact_memory_derivational_reduction mori_source_inputs_realize_source_exact_memory_derivational_reduction mori_source_inputs_realize_structural_exact_memory_kernel_explanation mori_force_correlation_realizes_shared_nonvacuous_exact_reduction mori_routes_make_shared_exact_route_applicable mori_routes_establish_shared_exact_memory_kernel_reduction mori_exact_reduction_realizes_derivational_reduction mori_routes_make_shared_local_route_applicable mori_local_result_realizes_shared_nonvacuous_reduction mori_routes_establish_shared_memory_kernel_reduction mori_routes_exhibit_nonvacuous_shared_memory_kernel_reduction memory_kernel_model_inputs_establish_theory_model_grounding mori_routes_establish_grounded_shared_reduction grounded_mori_reduction_transfers_every_shared_claim
Countermodels
vacuous_projection_calculations_do_not_establish_projection_reduction identifying_ordinary_and_projected_correlations_breaks_plateau_resolution hydrodynamic_reduction_does_not_identify_exact_and_local_equations ordered_limit_agreement_does_not_supply_finite_wavevector_equality exact_aged_law_does_not_supply_phenomenological_law_without_extra_steps bare_flux_does_not_inherit_projected_collision_invariant_orthogonality proposed_most_probable_path_typicality_is_not_established_typicality named_force_correlation_result_does_not_supply_equation_three_ten_formula
Coverage theorems
projection_reduction_route_is_semantically_realized force_correlation_route_is_semantically_realized plateau_resolution_route_is_semantically_realized short_memory_approximation_route_is_semantically_realized canonical_scalar_product_route_is_semantically_realized time_reversal_consequences_route_is_semantically_realized good_collective_variables_route_is_semantically_realized hydrodynamic_slow_mode_route_is_semantically_realized collective_examples_route_is_semantically_realized thermal_after_effect_route_is_semantically_realized aged_fluctuation_law_route_is_semantically_realized regression_transport_route_is_semantically_realized nonequilibrium_transport_route_is_semantically_realized mechanical_response_comparison_route_is_semantically_realized transport_coefficient_chain_route_is_semantically_realized scope_qualification_route_is_semantically_realized complete_assessment_route_is_semantically_realized
Source-map audits
force_correlation_route_exposes_core_exact_memory_formula_package routes_have_exact_predecessor_graph calculation_contracts_are_independent_hypotheses normal_limit_setup_is_an_independent_hypothesis local_and_plateau_routes_are_siblings_after_force_correlation dependent_routes_consume_certified_predecessor_outputs thermal_calculation_results_consume_selected_inputs intermediate_result_steps_do_not_replay_upstream_calculations local_result_retains_controlled_approximation regression_result_retains_postulate_and_controlled_approximation nonequilibrium_result_retains_physical_and_interpretive_inputs response_comparison_retains_ordered_limit_approximation scope_result_retains_open_comparison complete_result_retains_controlled_approximation hydrodynamic_reduction_retains_controlled_approximation complete_result_relies_on_every_substantive_route
Atoms and claim identifiers (72 each)
projectionSetup projectionGeometryCalculation projectionGeometryResult orthogonalDynamicsCalculation orthogonalDynamicsResult exactEquationCalculation projectionResult correlationSetup correlationCalculation correlationResult exactMemoryFormulaPackage exactMemoryFormula plateauSetup ordinaryCorrelationCalculation ordinaryCorrelationResult projectedPlateauCalculation plateauResult localSetup localCalculation localResult scalarProductSetup scalarProductCalculation scalarProductResult pathInterpretation canonicalScalarProductResult timeReversalSetup timeReversalCalculation timeReversalResult goodVariableSetup goodVariableCalculation goodVariableResult hydrodynamicSetup hydrodynamicReduction examplesSetup examplesCalculation examplesResult thermalSetup densityHistoryCalculation densityHistoryResult conjugateFluxCalculation conjugateFluxResult afterEffectCalculation afterEffectResult causalityCalculation thermalResult agedSetup agedCalculation agedResult regressionSetup regressionCalculation regressionResult nonequilibriumSetup nonequilibriumCalculation nonequilibriumResult responseComparisonSetup responseDifferenceCalculation responseDifferenceResult normalLimitSetup normalLimitCalculation responseComparisonResult transportSetup fluxExpressionCalculation fluxExpressionResult coefficientLimitCalculation coefficientLimitResult transportIdentificationCalculation transportIdentificationResult diluteGasCalculation transportResult scopeSetup scopeAssessment scopeResult completeResult
Step identifiers (72)
stateProjectionSetup supplyProjectionGeometryCalculation deriveProjectionGeometryResult supplyOrthogonalDynamicsCalculation deriveOrthogonalDynamicsResult supplyExactEquationCalculation deriveProjectionResult stateCorrelationSetup supplyCorrelationCalculation deriveCorrelationResult retainExactMemoryFormulaPackage statePlateauSetup supplyOrdinaryCorrelationCalculation deriveOrdinaryCorrelationResult supplyProjectedPlateauCalculation derivePlateauResult stateLocalSetup supplyLocalCalculation deriveLocalResult stateScalarProductSetup supplyScalarProductCalculation deriveScalarProductResult supplyPathInterpretation deriveCanonicalScalarProductResult stateTimeReversalSetup supplyTimeReversalCalculation deriveTimeReversalResult stateGoodVariableSetup supplyGoodVariableCalculation deriveGoodVariableResult stateHydrodynamicSetup deriveHydrodynamicReduction stateExamplesSetup supplyExamplesCalculation deriveExamplesResult stateThermalSetup supplyDensityHistoryCalculation deriveDensityHistoryResult supplyConjugateFluxCalculation deriveConjugateFluxResult supplyAfterEffectCalculation deriveAfterEffectResult supplyCausalityCalculation deriveThermalResult stateAgedSetup supplyAgedCalculation deriveAgedResult stateRegressionSetup supplyRegressionCalculation deriveRegressionResult stateNonequilibriumSetup supplyNonequilibriumCalculation deriveNonequilibriumResult stateResponseComparisonSetup supplyResponseDifferenceCalculation deriveResponseDifferenceResult stateNormalLimitSetup supplyNormalLimitCalculation deriveResponseComparisonResult stateTransportSetup supplyFluxExpressionCalculation deriveFluxExpressionResult supplyCoefficientLimitCalculation deriveCoefficientLimitResult supplyTransportIdentificationCalculation deriveTransportIdentificationResult supplyDiluteGasCalculation deriveTransportResult stateScopeSetup supplyScopeAssessment deriveScopeResult assembleCompleteResult
Route identifiers and kinds (17 each)
projectionReduction forceCorrelation plateauResolution shortMemoryApproximation canonicalScalarProduct timeReversalConsequences goodCollectiveVariables hydrodynamicSlowModes collectiveExamples thermalAfterEffect agedFluctuationLaw regressionTransport nonequilibriumTransport mechanicalResponseComparison transportCoefficientChain scopeQualification completeAssessment
orthogonalProjectionIdentity fluctuationDissipationRelation complementPropagatorPlateauResolution separatedTimeScaleApproximation canonicalMostProbablePath parityFieldReversalReciprocity deterministicCollectiveVariableCriterion conservedSlowModeReduction spinOscillatorFluidApplications projectedThermalAfterEffect exactAgedFluctuationEquation regressionPostulateTransportLimit localEquilibriumContraction projectedVersusMechanicalResponse orderedLimitTransportCoefficients exactApproximateAndOpenScope completePaperSynthesis
Current checked semantic identifiers
These complete lists follow current Lean declaration order. Historical and selected explanatory lists elsewhere retain their separate scope.
Primary semantic theorems (148)
projection_and_orthogonal_evolution_derive_exact_generalized_langevin_equation, projection_intermediate_results_establish_reduction, random_force_correlation_establishes_memory_kernel_relation, exact_projection_reduction_retains_equations_three_three_ten_and_eleven, established_force_correlation_retains_core_exact_memory_formulas, complement_propagator_separates_damping_kernel_from_plateau_correlation, plateau_intermediate_results_establish_resolution, plateau_resolution_retains_distinct_correlation_roles, separated_time_scales_yield_qualified_local_langevin_approximation, canonical_zero_mean_requirement_selects_most_probable_linear_path, scalar_product_result_and_path_interpretation_establish_canonical_result, canonical_projection_and_reversal_symmetry_establish_reciprocity, separated_relaxation_selects_good_collective_variables, conserved_slow_variables_realize_hydrodynamic_reduction, mori_hydrodynamic_reduction_retains_a_conserved_slow_variable, spin_oscillator_and_fluid_examples_test_collective_variable_selection, projected_density_and_flux_calculations_establish_thermal_after_effect, thermal_intermediate_results_and_causality_establish_after_effect, established_thermal_after_effect_realizes_retarded_response, finite_kernel_memory_yields_exact_aged_fluctuation_law, onsager_regression_and_low_frequency_steps_yield_transport_law, local_equilibrium_contraction_yields_average_final_stage_transport, two_transport_routes_retain_distinct_extra_premises, projected_flux_and_propagator_distinguish_thermal_from_mechanical_response, response_difference_and_normal_limit_establish_comparison, projected_flux_and_ordered_limits_establish_transport_coefficients, transport_intermediate_results_and_dilute_gas_establish_chain, hydrodynamic_setup_establishes_scoped_slow_mode_reduction, scope_distinguishes_exact_reduction_from_local_and_transport_claims, complete_mori_1965_logic, complete_result_and_hydrodynamic_setup_establish_full_scoped_logic, full_scoped_logic_retains_hydrodynamic_reduction_and_approximate_status, memory_kernel_model_retains_mori_semantics, mori_setups_realize_shared_selected_memory_kernel_setup, mori_projection_setup_realizes_shared_selected_exact_memory_setup, mori_source_inputs_make_shared_exact_memory_route_applicable, mori_source_inputs_realize_exact_memory_derivational_reduction, mori_source_inputs_realize_source_exact_memory_derivational_reduction, mori_source_inputs_realize_structural_exact_memory_kernel_explanation, mori_force_correlation_realizes_shared_nonvacuous_exact_reduction, mori_routes_make_shared_exact_route_applicable, mori_routes_establish_shared_exact_memory_kernel_reduction, mori_exact_reduction_realizes_derivational_reduction, mori_routes_make_shared_local_route_applicable, mori_local_result_realizes_shared_nonvacuous_reduction, mori_routes_establish_shared_memory_kernel_reduction, mori_routes_exhibit_nonvacuous_shared_memory_kernel_reduction, memory_kernel_model_inputs_establish_theory_model_grounding, mori_routes_establish_grounded_shared_reduction, grounded_mori_reduction_transfers_every_shared_claim, named_force_correlation_result_does_not_supply_equation_three_ten_formula, vacuous_projection_calculations_do_not_establish_projection_reduction, identifying_ordinary_and_projected_correlations_breaks_plateau_resolution, hydrodynamic_reduction_does_not_identify_exact_and_local_equations, ordered_limit_agreement_does_not_supply_finite_wavevector_equality, exact_aged_law_does_not_supply_phenomenological_law_without_extra_steps, bare_flux_does_not_inherit_projected_collision_invariant_orthogonality, proposed_most_probable_path_typicality_is_not_established_typicality, gram_inverse_fixes_the_selected_variables, gram_inverse_makes_the_projection_idempotent, gram_inverse_makes_the_vertical_force_orthogonal, oscillator_projection, oscillator_complement, oscillator_vertical_force, oscillator_projected_force, oscillator_ordinary_force, oscillator_projection_domain, oscillator_propagators_solve_the_source_generators, oscillator_projected_correlation, oscillator_damping_kernel, oscillator_ordinary_correlation, oscillator_has_nonvacuous_projected_force, oscillator_variable_components, oscillator_satisfies_the_exact_memory_equation, oscillator_realizes_exact_memory, projected_force_realizes_shared_residual_covariance, full_evolution_cannot_replace_complement_evolution, full_evolution_does_not_preserve_force_orthogonality, exact_projection_does_not_imply_decaying_memory, duplicated_variables_have_no_identity_gram_inverse, an_inverse_named_matrix_does_not_make_a_projection, carrier_and_coefficient_control_give_a_nonvacuous_memory_readout, the_local_equation_retains_the_rotating_history_and_coefficient_errors, the_scalar_carrier_solves_the_actual_free_rotation, the_scalar_carrier_has_unit_modulus, positive_decay_keeps_the_rotating_denominator_nonzero, exponential_memory_has_the_finite_rotating_coefficient, exponential_memory_has_an_exact_finite_time_coefficient_error, the_abel_regulator_and_carrier_keep_their_distinct_exponents, the_regulated_exponential_memory_has_its_computed_damping, the_exponential_family_realizes_moris_abel_prescription, a_pure_rotating_history_has_zero_carrier_adjusted_variation, a_pure_carrier_does_not_require_low_oscillation_frequency, a_rotating_exponential_memory_has_an_inhabited_localization_readout, a_positive_oscillation_changes_the_complex_damping, the_high_frequency_control_has_a_frequency_shift, opposite_carrier_times_are_actual_inverses, the_rotating_profile_restores_the_actual_memory_integrand, the_rotating_profile_starts_at_the_current_state, the_rotating_profile_endpoint_retains_the_initial_state_norm, primitive_errors_in_the_rotating_frame_control_the_actual_memory, a_nondecaying_memory_still_has_a_nonzero_abel_coefficient, the_finite_coefficient_returns_to_zero_after_each_full_rotation, the_abel_coefficient_does_not_supply_finite_cutoff_convergence, the_classical_force_readout_is_the_dual_of_orthogonal_evolution, the_same_initial_sample_evaluates_the_actual_projected_force, the_shared_matrix_is_the_original_projected_correlation, classical_initial_sampling_realizes_the_source_force_correlation, source_orthogonality_is_an_actual_classical_zero_cross_moment, classical_orthogonality_removes_the_force_mean_at_linear_order, the_oscillator_projected_force_is_the_same_initial_momentum, the_same_initial_sample_satisfies_the_exact_oscillator_memory_equation, the_oscillator_readout_covariance_is_stationary, the_canonical_oscillator_has_an_actual_nonzero_residual_process, the_canonical_oscillator_force_has_stationary_gaussian_joint_laws, stationary_projected_noise_does_not_require_ambient_covariance_preservation, the_canonical_projected_noise_is_not_resampled_independently, zero_ensemble_force_mean_does_not_remove_the_actual_fluctuations, the_four_phase_ensemble_retains_the_same_projected_force_moments, the_oscillator_selected_observable_is_its_initial_position, classical_force_orthogonality_does_not_imply_initial_statistical_independence, the_same_projected_covariance_can_give_different_joint_force_laws, the_phase_state_uses_the_actual_full_oscillator_rotation, the_phase_state_has_measurable_observations, the_position_process_is_the_actual_first_phase_coordinate, the_position_observation_is_measurable, the_full_phase_state_recovers_the_actual_initial_state, the_full_phase_state_has_exact_measurable_state_closure, the_gaussian_full_phase_state_has_the_actual_markov_property, the_three_position_observations_retain_both_initial_coordinates, the_full_phase_state_has_nonvacuous_markov_predictions, equal_current_positions_do_not_determine_the_later_position, the_position_process_is_not_markov_under_actual_gaussian_sampling, restoring_momentum_restores_markov_prediction_but_position_alone_fails, the_actual_position_derivative_is_the_unretained_momentum, a_local_position_equation_does_not_make_position_a_markov_state, the_projected_force_is_markov_while_the_position_memory_does_not_decay, the_actual_projected_force_ensemble_composes_with_closed_state_prediction, the_prepared_force_has_a_normalized_canonical_response, force_orthogonality_gives_the_actual_zero_linear_preparation_derivative, sampled_projection_derives_the_zero_linear_preparation_force, orthogonality_controls_the_prepared_force_on_a_local_field_window, the_canonical_preparation_has_centered_orthogonal_observables, the_same_canonical_preparation_has_nonzero_nonlinear_residual_mean, a_zero_linear_force_response_does_not_make_finite_preparation_exact, arbitrarily_small_fields_retain_a_finite_bias_when_the_coupling_is_unbounded, every_rescaled_preparation_has_zero_linear_response_and_local_control, zero_linear_response_does_not_supply_a_coupling_independent_field_cutoff
Coverage theorems (19)
every_source_claim_has_semantics, projection_reduction_route_is_semantically_realized, force_correlation_route_is_semantically_realized, plateau_resolution_route_is_semantically_realized, short_memory_approximation_route_is_semantically_realized, canonical_scalar_product_route_is_semantically_realized, time_reversal_consequences_route_is_semantically_realized, good_collective_variables_route_is_semantically_realized, hydrodynamic_slow_mode_route_is_semantically_realized, collective_examples_route_is_semantically_realized, thermal_after_effect_route_is_semantically_realized, aged_fluctuation_law_route_is_semantically_realized, regression_transport_route_is_semantically_realized, nonequilibrium_transport_route_is_semantically_realized, mechanical_response_comparison_route_is_semantically_realized, transport_coefficient_chain_route_is_semantically_realized, scope_qualification_route_is_semantically_realized, complete_assessment_route_is_semantically_realized, route_semantic_realization_is_exhaustive
Source-map audit theorems (19)
argument_wellFormed, argument_auditable, routes_wellFormed, force_correlation_route_exposes_core_exact_memory_formula_package, routes_have_exact_predecessor_graph, calculation_contracts_are_independent_hypotheses, normal_limit_setup_is_an_independent_hypothesis, local_and_plateau_routes_are_siblings_after_force_correlation, dependent_routes_consume_certified_predecessor_outputs, thermal_calculation_results_consume_selected_inputs, intermediate_result_steps_do_not_replay_upstream_calculations, local_result_retains_controlled_approximation, regression_result_retains_postulate_and_controlled_approximation, nonequilibrium_result_retains_physical_and_interpretive_inputs, response_comparison_retains_ordered_limit_approximation, scope_result_retains_open_comparison, complete_result_retains_controlled_approximation, hydrodynamic_reduction_retains_controlled_approximation, complete_result_relies_on_every_substantive_route
Semantic atoms (72)
projectionSetup, projectionGeometryCalculation, projectionGeometryResult, orthogonalDynamicsCalculation, orthogonalDynamicsResult, exactEquationCalculation, projectionResult, correlationSetup, correlationCalculation, correlationResult, exactMemoryFormulaPackage, plateauSetup, ordinaryCorrelationCalculation, ordinaryCorrelationResult, projectedPlateauCalculation, plateauResult, localSetup, localCalculation, localResult, scalarProductSetup, scalarProductCalculation, scalarProductResult, pathInterpretation, canonicalScalarProductResult, timeReversalSetup, timeReversalCalculation, timeReversalResult, goodVariableSetup, goodVariableCalculation, goodVariableResult, hydrodynamicSetup, hydrodynamicReduction, examplesSetup, examplesCalculation, examplesResult, thermalSetup, densityHistoryCalculation, densityHistoryResult, conjugateFluxCalculation, conjugateFluxResult, afterEffectCalculation, afterEffectResult, causalityCalculation, thermalResult, agedSetup, agedCalculation, agedResult, regressionSetup, regressionCalculation, regressionResult, nonequilibriumSetup, nonequilibriumCalculation, nonequilibriumResult, responseComparisonSetup, responseDifferenceCalculation, responseDifferenceResult, normalLimitSetup, normalLimitCalculation, responseComparisonResult, transportSetup, fluxExpressionCalculation, fluxExpressionResult, coefficientLimitCalculation, coefficientLimitResult, transportIdentificationCalculation, transportIdentificationResult, diluteGasCalculation, transportResult, scopeSetup, scopeAssessment, scopeResult, completeResult
Claim identifiers (72)
projectionSetup, projectionGeometryCalculation, projectionGeometryResult, orthogonalDynamicsCalculation, orthogonalDynamicsResult, exactEquationCalculation, projectionResult, correlationSetup, correlationCalculation, correlationResult, exactMemoryFormula, plateauSetup, ordinaryCorrelationCalculation, ordinaryCorrelationResult, projectedPlateauCalculation, plateauResult, localSetup, localCalculation, localResult, scalarProductSetup, scalarProductCalculation, scalarProductResult, pathInterpretation, canonicalScalarProductResult, timeReversalSetup, timeReversalCalculation, timeReversalResult, goodVariableSetup, goodVariableCalculation, goodVariableResult, hydrodynamicSetup, hydrodynamicReduction, examplesSetup, examplesCalculation, examplesResult, thermalSetup, densityHistoryCalculation, densityHistoryResult, conjugateFluxCalculation, conjugateFluxResult, afterEffectCalculation, afterEffectResult, causalityCalculation, thermalResult, agedSetup, agedCalculation, agedResult, regressionSetup, regressionCalculation, regressionResult, nonequilibriumSetup, nonequilibriumCalculation, nonequilibriumResult, responseComparisonSetup, responseDifferenceCalculation, responseDifferenceResult, normalLimitSetup, normalLimitCalculation, responseComparisonResult, transportSetup, fluxExpressionCalculation, fluxExpressionResult, coefficientLimitCalculation, coefficientLimitResult, transportIdentificationCalculation, transportIdentificationResult, diluteGasCalculation, transportResult, scopeSetup, scopeAssessment, scopeResult, completeResult
Step identifiers (72)
stateProjectionSetup, supplyProjectionGeometryCalculation, deriveProjectionGeometryResult, supplyOrthogonalDynamicsCalculation, deriveOrthogonalDynamicsResult, supplyExactEquationCalculation, deriveProjectionResult, stateCorrelationSetup, supplyCorrelationCalculation, deriveCorrelationResult, retainExactMemoryFormulaPackage, statePlateauSetup, supplyOrdinaryCorrelationCalculation, deriveOrdinaryCorrelationResult, supplyProjectedPlateauCalculation, derivePlateauResult, stateLocalSetup, supplyLocalCalculation, deriveLocalResult, stateScalarProductSetup, supplyScalarProductCalculation, deriveScalarProductResult, supplyPathInterpretation, deriveCanonicalScalarProductResult, stateTimeReversalSetup, supplyTimeReversalCalculation, deriveTimeReversalResult, stateGoodVariableSetup, supplyGoodVariableCalculation, deriveGoodVariableResult, stateHydrodynamicSetup, deriveHydrodynamicReduction, stateExamplesSetup, supplyExamplesCalculation, deriveExamplesResult, stateThermalSetup, supplyDensityHistoryCalculation, deriveDensityHistoryResult, supplyConjugateFluxCalculation, deriveConjugateFluxResult, supplyAfterEffectCalculation, deriveAfterEffectResult, supplyCausalityCalculation, deriveThermalResult, stateAgedSetup, supplyAgedCalculation, deriveAgedResult, stateRegressionSetup, supplyRegressionCalculation, deriveRegressionResult, stateNonequilibriumSetup, supplyNonequilibriumCalculation, deriveNonequilibriumResult, stateResponseComparisonSetup, supplyResponseDifferenceCalculation, deriveResponseDifferenceResult, stateNormalLimitSetup, supplyNormalLimitCalculation, deriveResponseComparisonResult, stateTransportSetup, supplyFluxExpressionCalculation, deriveFluxExpressionResult, supplyCoefficientLimitCalculation, deriveCoefficientLimitResult, supplyTransportIdentificationCalculation, deriveTransportIdentificationResult, supplyDiluteGasCalculation, deriveTransportResult, stateScopeSetup, supplyScopeAssessment, deriveScopeResult, assembleCompleteResult
Route identifiers (17)
projectionReduction, forceCorrelation, plateauResolution, shortMemoryApproximation, canonicalScalarProduct, timeReversalConsequences, goodCollectiveVariables, hydrodynamicSlowModes, collectiveExamples, thermalAfterEffect, agedFluctuationLaw, regressionTransport, nonequilibriumTransport, mechanicalResponseComparison, transportCoefficientChain, scopeQualification, completeAssessment
Route kinds (17)
orthogonalProjectionIdentity, fluctuationDissipationRelation, complementPropagatorPlateauResolution, separatedTimeScaleApproximation, canonicalMostProbablePath, parityFieldReversalReciprocity, deterministicCollectiveVariableCriterion, conservedSlowModeReduction, spinOscillatorFluidApplications, projectedThermalAfterEffect, exactAgedFluctuationEquation, regressionPostulateTransportLimit, localEquilibriumContraction, projectedVersusMechanicalResponse, orderedLimitTransportCoefficients, exactApproximateAndOpenScope, completePaperSynthesis
Normalized preparation and its linear boundary
orthogonality_controls_the_prepared_force_on_a_local_field_window derives a genuine local statement: for every positive tolerance, there is a positive radius with |<force(t)>_h| <= tolerance*|h| throughout that field window. The model, observable, and time are fixed before selecting the radius.
Local control does not give a common cutoff across arbitrary coupling strengths. Every rescaled three-state preparation retains zero derivative and local control, but choosing h=radius/2 and s=2*log(2)/radius for coupling s*A preserves bias 1/7. The fidelity matrix rejects a coupling-independent absolute-error bound of 1/14. This is a diagnostic of an unsupported inference, not an additional claim attributed to Mori.
The shared scaling theorem transports a valid radius to radius/|s| and its error per unit field to tolerance*|s|. No numerical cutoff, quadratic remainder constant, time-uniform estimate, or thermodynamic-limit control is supplied.
Mori's pp. 433-434, equations (4.5)-(4.7), expand a normalized prepared ensemble. The finite classical library model changes the energy to E-h*A and derives d<B>/dh = beta*Cov(A,B) from the changing partition sum.
sampled_projection_derives_the_zero_linear_preparation_force uses the existing projected force on the same initial sample. Specified equilibrium moments and actual matrix orthogonality derive its zero preparation derivative. The derivative is not supplied as a premise.
A separate positive three-state preparation has centered orthogonal observables A=(-1,0,1) and B=(1,-2,1). Its zero linear response coexists with <B>=1/7 at h=log(2). This diagnoses an invalid finite-field extrapolation; it is not a microscopic force or typical-path construction.
The quantum canonical product, continuum limits, and most-probable-path interpretation remain separate. Existing source routes are unchanged.
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.
projectionReduction
Logical kind: orthogonalProjectionIdentity.
Required predecessor routes: none.
Ordered inference steps: stateProjectionSetup, supplyProjectionGeometryCalculation, deriveProjectionGeometryResult, supplyOrthogonalDynamicsCalculation, deriveOrthogonalDynamicsResult, supplyExactEquationCalculation, deriveProjectionResult.
Exported conclusions: projectionResult.
forceCorrelation
Logical kind: fluctuationDissipationRelation.
Required predecessor routes: projectionReduction.
Ordered inference steps: stateCorrelationSetup, supplyCorrelationCalculation, deriveCorrelationResult, retainExactMemoryFormulaPackage.
Exported conclusions: exactMemoryFormula, correlationResult.
plateauResolution
Logical kind: complementPropagatorPlateauResolution.
Required predecessor routes: forceCorrelation.
Ordered inference steps: statePlateauSetup, supplyOrdinaryCorrelationCalculation, deriveOrdinaryCorrelationResult, supplyProjectedPlateauCalculation, derivePlateauResult.
Exported conclusions: plateauResult.
shortMemoryApproximation
Logical kind: separatedTimeScaleApproximation.
Required predecessor routes: forceCorrelation.
Ordered inference steps: stateLocalSetup, supplyLocalCalculation, deriveLocalResult.
Exported conclusions: localResult.
canonicalScalarProduct
Logical kind: canonicalMostProbablePath.
Required predecessor routes: projectionReduction.
Ordered inference steps: stateScalarProductSetup, supplyScalarProductCalculation, deriveScalarProductResult, supplyPathInterpretation, deriveCanonicalScalarProductResult.
Exported conclusions: canonicalScalarProductResult.
timeReversalConsequences
Logical kind: parityFieldReversalReciprocity.
Required predecessor routes: canonicalScalarProduct, forceCorrelation.
Ordered inference steps: stateTimeReversalSetup, supplyTimeReversalCalculation, deriveTimeReversalResult.
Exported conclusions: timeReversalResult.
goodCollectiveVariables
Logical kind: deterministicCollectiveVariableCriterion.
Required predecessor routes: shortMemoryApproximation.
Ordered inference steps: stateGoodVariableSetup, supplyGoodVariableCalculation, deriveGoodVariableResult.
Exported conclusions: goodVariableResult.
hydrodynamicSlowModes
Logical kind: conservedSlowModeReduction.
Required predecessor routes: goodCollectiveVariables.
Ordered inference steps: stateHydrodynamicSetup, deriveHydrodynamicReduction.
Exported conclusions: hydrodynamicReduction.
collectiveExamples
Logical kind: spinOscillatorFluidApplications.
Required predecessor routes: goodCollectiveVariables, timeReversalConsequences.
Ordered inference steps: stateExamplesSetup, supplyExamplesCalculation, deriveExamplesResult.
Exported conclusions: examplesResult.
thermalAfterEffect
Logical kind: projectedThermalAfterEffect.
Required predecessor routes: canonicalScalarProduct, forceCorrelation.
Ordered inference steps: stateThermalSetup, supplyDensityHistoryCalculation, deriveDensityHistoryResult, supplyConjugateFluxCalculation, deriveConjugateFluxResult, supplyAfterEffectCalculation, deriveAfterEffectResult, supplyCausalityCalculation, deriveThermalResult.
Exported conclusions: thermalResult.
agedFluctuationLaw
Logical kind: exactAgedFluctuationEquation.
Required predecessor routes: thermalAfterEffect.
Ordered inference steps: stateAgedSetup, supplyAgedCalculation, deriveAgedResult.
Exported conclusions: agedResult.
regressionTransport
Logical kind: regressionPostulateTransportLimit.
Required predecessor routes: agedFluctuationLaw.
Ordered inference steps: stateRegressionSetup, supplyRegressionCalculation, deriveRegressionResult.
Exported conclusions: regressionResult.
nonequilibriumTransport
Logical kind: localEquilibriumContraction.
Required predecessor routes: thermalAfterEffect, goodCollectiveVariables.
Ordered inference steps: stateNonequilibriumSetup, supplyNonequilibriumCalculation, deriveNonequilibriumResult.
Exported conclusions: nonequilibriumResult.
mechanicalResponseComparison
Logical kind: projectedVersusMechanicalResponse.
Required predecessor routes: thermalAfterEffect.
Ordered inference steps: stateResponseComparisonSetup, supplyResponseDifferenceCalculation, deriveResponseDifferenceResult, stateNormalLimitSetup, supplyNormalLimitCalculation, deriveResponseComparisonResult.
Exported conclusions: responseComparisonResult.
transportCoefficientChain
Logical kind: orderedLimitTransportCoefficients.
Required predecessor routes: thermalAfterEffect, goodCollectiveVariables.
Ordered inference steps: stateTransportSetup, supplyFluxExpressionCalculation, deriveFluxExpressionResult, supplyCoefficientLimitCalculation, deriveCoefficientLimitResult, supplyTransportIdentificationCalculation, deriveTransportIdentificationResult, supplyDiluteGasCalculation, deriveTransportResult.
Exported conclusions: transportResult.
scopeQualification
Logical kind: exactApproximateAndOpenScope.
Required predecessor routes: projectionReduction, canonicalScalarProduct, forceCorrelation, plateauResolution, shortMemoryApproximation, timeReversalConsequences, goodCollectiveVariables, hydrodynamicSlowModes, collectiveExamples, thermalAfterEffect, agedFluctuationLaw, regressionTransport, nonequilibriumTransport, mechanicalResponseComparison, transportCoefficientChain.
Ordered inference steps: stateScopeSetup, supplyScopeAssessment, deriveScopeResult.
Exported conclusions: scopeResult.
completeAssessment
Logical kind: completePaperSynthesis.
Required predecessor routes: projectionReduction, canonicalScalarProduct, forceCorrelation, plateauResolution, shortMemoryApproximation, timeReversalConsequences, goodCollectiveVariables, hydrodynamicSlowModes, collectiveExamples, thermalAfterEffect, agedFluctuationLaw, regressionTransport, nonequilibriumTransport, mechanicalResponseComparison, transportCoefficientChain, scopeQualification.
Ordered inference steps: assembleCompleteResult.
Exported conclusions: completeResult.