Examples and distinctions
Constructed examples of this model; each answer includes the Lean statement.
Selected argument
Return to conclusion
Back
Meaning dependencies
Inference and proof references
Complete project specification
Exact root statement (dynamics 1).UniqueForwardEvolutionAt (Real.log 4) 0 ∧
¬PhysicsLogic.Paradigm.Dynamics.FiniteInformation.HasUniformForecastAt (dynamics 1) ForecastFromIntervals.compatible
(fun forecast actual => dist forecast actual ≤ 1 / 2) (Set.Icc (-(1 / 4)) (1 / 4)) (Real.log 4)
Compare two arguments
Compare their definitions and hypotheses. Shared declarations may be instantiated
differently; differences do not establish equivalence or implication.
Compared statement
No comparison 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.
Earlier extraction
Clear comparison
No earlier extraction selected.
Notes and questions
Export notebook
Merge notebook
Import merges local entries without overwriting them.
All declarations in the selected argument
Find a declaration
Definitions, structures, and assumptions
Enable JavaScript to open the Lean code panel.
Structures, classes, and inductive alternatives
PhysicsLogic.Paradigm.Dynamics.Dynamics structure
Definitions and domain choices
PhysicsLogic.Paradigm.Dynamics.Dynamics.ForwardDeterministic definition PhysicsLogic.Paradigm.Dynamics.Dynamics.ForwardTotal definition PhysicsLogic.Paradigm.Dynamics.Dynamics.HasForwardEvolutionAt definition PhysicsLogic.Paradigm.Dynamics.Dynamics.TotalDeterministicEvolution definition PhysicsLogic.Paradigm.Dynamics.Dynamics.UniqueForwardEvolutionAt definition PhysicsLogic.Paradigm.Dynamics.Dynamics.evolves definition PhysicsLogic.Paradigm.Dynamics.FiniteInformation.HasUniformForecastAt definition PhysicsLogic.Paradigm.Dynamics.FiniteInformation.PossibleOutcomeAt definition PhysicsLogic.Paradigm.Dynamics.FiniteInformation.UniformForecastAt definition PhysicsLogicConsumer.ClassicalDynamics.ForecastFromIntervals.compatible definition PhysicsLogicConsumer.ClassicalDynamics.ForecastFromIntervals.thresholdDynamics definition PhysicsLogicConsumer.ClassicalDynamics.ForecastFromIntervals.thresholdStep definition PhysicsLogicConsumer.ClassicalDynamics.dynamics definition PhysicsLogicConsumer.ClassicalDynamics.flow definition PhysicsLogicConsumer.ClassicalDynamics.reliable definition
Checked statements: parameters, hypotheses, and interpretation
PhysicsLogic.Paradigm.Dynamics.total_deterministic_evolution_iff_unique_successors checked statement PhysicsLogicConsumer.ClassicalDynamics.ForecastFromIntervals.continuous_dependence_at_each_fixed_time checked statement PhysicsLogicConsumer.ClassicalDynamics.ForecastFromIntervals.empty_information_does_not_count_as_a_successful_forecast checked statement PhysicsLogicConsumer.ClassicalDynamics.ForecastFromIntervals.exact_initial_information_allows_an_exact_forecast checked statement PhysicsLogicConsumer.ClassicalDynamics.ForecastFromIntervals.no_initial_radius_controls_all_future_times checked statement PhysicsLogicConsumer.ClassicalDynamics.ForecastFromIntervals.nominal_failure_does_not_exclude_another_accurate_forecast checked statement PhysicsLogicConsumer.ClassicalDynamics.ForecastFromIntervals.unique_evolution_can_exclude_every_uniform_half_unit_forecast checked statement PhysicsLogicConsumer.ClassicalDynamics.ForecastFromIntervals.unique_threshold_evolution_does_not_supply_continuous_dependence checked statement
Constructors, projections, and other meaning dependencies
PhysicsLogic.Paradigm.Dynamics.Dynamics.mk constructor
External mathematical declarations
And external type boundary Continuous external type boundary ContinuousAt external type boundary Dist.dist external type boundary DivInvMonoid.toDiv external type boundary EmptyCollection.emptyCollection external type boundary Eq external type boundary Exists external type boundary HDiv.hDiv external type boundary HMul.hMul external type boundary HSub.hSub external type boundary Iff external type boundary LE.le external type boundary LT.lt external type boundary Membership.mem external type boundary Nat external type boundary Nat.instAtLeastTwoHAddOfNat external type boundary Nat.instNeZeroSucc external type boundary Nat.iterate external type boundary Neg.neg external type boundary Not external type boundary OfNat.ofNat external type boundary One.toOfNat1 external type boundary PseudoMetricSpace.toDist external type boundary PseudoMetricSpace.toUniformSpace external type boundary Real external type boundary Real.decidableEq external type boundary Real.exp external type boundary Real.instAddGroup external type boundary Real.instDivInvMonoid external type boundary Real.instLE external type boundary Real.instLT external type boundary Real.instMul external type boundary Real.instNatCast external type boundary Real.instNeg external type boundary Real.instOne external type boundary Real.instPreorder external type boundary Real.instSub external type boundary Real.instZero external type boundary Real.lattice external type boundary Real.log external type boundary Real.pseudoMetricSpace external type boundary Set external type boundary Set.Icc external type boundary Set.instEmptyCollection external type boundary Set.instMembership external type boundary Set.instSingletonSet external type boundary Singleton.singleton external type boundary UniformSpace.toTopologicalSpace external type boundary Zero.toOfNat0 external type boundary abs external type boundary instHDiv external type boundary instHMul external type boundary instHSub external type boundary instOfNatAtLeastTwo external type boundary instOfNatNat external type boundary ite external type boundary
Source motivation: Lorenz 1963, p. 133, distinguishes uniqueness, continuity, boundedness and long-time stability; Miller 1964, pp. 255-256, distinguishes a true trajectory from error-induced changes of the calculated phase point. The interval examples, factor-two metric obstruction and discontinuous threshold map are our diagnostics, not numerical results attributed to those papers. TotalDeterministicEvolution means only existence and uniqueness. The earlier WellPosedForwardEvolution name survives as deprecated compatibility, not a claim of continuous dependence.
Characterizations of the physical model