PhysicsLogic / Mori 1965

One Robust Prediction Is Not Closed Evolution

Inspect the selected-behavior quantifier in reduction and emergence against actual oscillator dynamics.

Definitions and assumptions

Scope and physical limitations

The dimensionless unit-frequency oscillator rotates (q,p); a third full-state coordinate is unchanged and is not retained. The two-component observation is linked to the actual three-coordinate propagator. A behavior is a time and a future value, not a named atom. Macro exhibition means that this time/value pair is possible from one compatible initial state; robust realization requires the same future value from every compatible initial state. AutonomousEmergenceAt concerns this selected behavior. It does not quantify over every future behavior or assert Markov prediction. The positive comparison retains (q,p), with exact closed prediction despite the unrecoverable third coordinate. Position alone has robust predictions exactly when sin(t)=0, but even an arbitrary nonmeasurable function of its present value cannot predict its quarter-period value. These exact diagnostics supply no heat bath, damping approximation, universal emergence criterion.

Other arguments
Examples and distinctions

Constructed examples of this model; each answer includes the Lean statement.

Exact root statement

∀ (present : ℝ),
  AutonomousEmergenceAt (predictionRealization fun state => state 0) present (Real.pi, -present) ∧
    ¬MeasurableStateClosureOn position (Set.Ici 0)
Compare two arguments

Compare their definitions and hypotheses. Shared declarations may be instantiated differently; differences do not establish equivalence or implication.

No comparison argument selected.

Compare an earlier extraction

Compare the displayed specifications with an earlier JSON export. This compares text, not mathematical equivalence. Files stay in this browser.

No earlier extraction selected.

Notes and questions

Note for

Unsubmitted text stays in this tab when navigating declarations, but is not saved across reloads.

Import merges local entries without overwriting them.

All declarations in the selected argument

Definitions, structures, and assumptions

Structures, classes, and inductive alternatives

  • structure

Definitions and domain choices

  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition

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

Constructors, projections, and other meaning dependencies

  • 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