Deterministic Nonperiodic Flow

The source map does not arrange the paper as one chain ending in a weather theorem. Every route is an independent root. The two stability arguments concern an abstract finite phase flow; the predictability route concerns finite observational resolution; the numerical-method route concerns a digital sequence; the reduction route concerns a three-mode model; the evidence route concerns one finite run; and the atmospheric route states a conditional implication together with open qualifications.

The first route concerns a central trajectory: one that is its own limiting trajectory. If that limit were stable, the stable-limit calculation would make the original trajectory quasi-periodic. The paper's nonperiodicity bridge excludes quasi-periodicity, so stability leads to contradiction.

The noncentral case is weaker and carefully worded. Uniform stability would supply some limiting trajectory and make that limit stable. The same stable-limit calculation would again imply quasi-periodicity, contradicting nonperiodicity. What is excluded is uniform stability, not every possible local notion of stability.

Choose two admissible initial states compatible at the input resolution. Both evolve under the same deterministic finite model to the selected time. The divergence calculation supplies final states whose separation exceeds the prediction resolution.

A separate reliability bridge states that a reliable point prediction from the finite specification would exclude such separated continuations. Lean then checks the contradiction while retaining deterministic evolution.

The selected numerical run has finite state memory, uses a deterministic forward update, and adopts a sufficiently small time step in the numerical regime. A dissipative-step calculation bounds the run. Finitely many machine states plus deterministic updating then force eventual repetition.

The route also records a scheme-specific negative result: the centered-difference scheme does not determine a unique future in the selected setup. The forward scheme and the centered scheme must not be treated as logically interchangeable.

Eventual periodicity here is a finite-state fact about the stored numerical sequence. The source claim explicitly refuses to infer periodicity of the represented continuum flow.

Saltzman's two-dimensional convection equations are truncated to three specific Fourier amplitudes, not three unspecified variables. The formalization retains the dimensional vorticity and temperature equations, identifies the selected reduced-state amplitudes, and keeps the original Rayleigh controls and dimensionless rescaling.

The stream function retains its X sin(pi a x/H) sin(pi z/H) mode. Temperature retains both the Y cos(pi a x/H) sin(pi z/H) current-difference mode and the distinct -Z sin(2 pi z/H) vertical-profile distortion, together with their original normalization factors. Omitting the second temperature mode fails a checked physical countermodel. At the selected geometry a^2=1/2, Lean derives Rc=27 pi^4/4.

Both the no-convection and steady-convection characteristic polynomials are encoded. At sigma=10 and b=8/3, the instability threshold is exactly 470/19, below the selected r=28; the two nonzero equilibria are (+/-6 sqrt(2), +/-6 sqrt(2), 27). The exact phase-volume law gives V(t+7/10)=exp(-287/30)V(t). Lean proves this volume contraction, but a checked witness simultaneously has growing trajectory separation: volume loss does not mean convergence to a point.

The scope bridge says that the model physically represents convection near onset, while fidelity to the original hydrodynamics in the strong-convection regime is not established.

The countermodels a_three_mode_truncation_does_not_establish_strong_convection_fidelity and equations_twenty_five_to_twenty_seven_do_not_supply_strong_convection_fidelity fix this boundary in the formal development. The value-level witness keeps the p. 136 parameters and initial state, satisfies all three ODEs, and retains three modes with a required fourth mode and nonzero omitted amplitude; strong-convection fidelity is therefore still false.

The numerical evidence route chooses σ = 10, r = 28, a² = 1/2, b = 8/3, time step 0.01, and a model-member initial state (0, 1, 0). NumericalValueSetup stores these as real-valued equalities; they and the calculated trajectory form the setup, not conclusions of the earlier truncation route.

The finite calculation observes irregular transitions, calculates successive maxima and an empirical return relation, and finds the selected trajectories unstable. The exactly analyzable equation-(35) map is an explicitly idealized surrogate for that finite evidence, not an identification with the empirical flow.

Lean checks the fixed point 2/3, the cycle 2/5 -> 4/5 -> 2/5, both printed length-three cycles 2/7 -> 4/7 -> 6/7 -> 2/7 and 2/9 -> 4/9 -> 8/9 -> 2/9, and the terminating sequence 1/4 -> 1/2 -> undefined. The distinct values 1/3 and 2/3 both map to 2/3. Checked countermodels reject an invented midpoint continuation, injectivity, and an incorrect reflected branch even when the left branch is correct.

finite_numerical_evidence_does_not_prove_continuum_nonperiodicity is the corresponding formal countermodel: it keeps 6000 integration steps, multiple return maxima, and return-slope magnitude greater than one while a periodic continuum continuation remains possible. The stronger exact_surrogate_and_finite_evidence_do_not_prove_flow_nonperiodicity preserves that failure even after adding the exact idealized return map. The source-map theorem numerical_evidence_is_not_classified_as_mathematical_proof verifies that the route retains its interpretive status.

The atmospheric route is not downstream of the reduced-model route in the formal graph. It states a conditional: if the atmosphere admits the required finite-dimensional deterministic nonperiodic description and observational error is inevitable, then the selected sufficiently distant point forecast is unreliable.

The paper-local qualifications simultaneously state that atmospheric finite dimensionality, determinism, and nonperiodicity have not been established, that no analogue recurrence has been established, and that no forecast horizon has been identified. The source map describes the possible timescale as ranging from days to centuries.

The countermodels finite_model_instability_does_not_establish_atmospheric_applicability and instability_does_not_identify_an_exact_forecast_horizon keep positive initial resolution and larger final separation while atmospheric validation is absent, the transfer residual is nonzero, and the horizon interval is nondegenerate. They block the two most tempting upgrades. atmospheric_unknowns_are_explicit_open_obligations confirms their status in the source graph.

Only the nearby-state divergence route enters the reusable framework. The adapter preserves the selected finite hydrodynamic system, reference and comparison states, time, input and prediction resolutions, regime validity, deterministic classification, trajectory relation, later separation, and reliability predicate. finite_model_setup_and_determinism_realize_shared_selected_setup combines the observationally indistinguishable-state setup with the explicit forward-uniqueness realization before any divergence output is used. The paper constructs the output-led endpoint directly from the later separated trajectories, unique reference evolution, and point-prediction failure.

The selected model is grounded in the theory of finite deterministic hydrodynamics and the world of the selected finite-flow model only from the complete nearby-state setup and explicit trajectory-uniqueness realization. Grounding consumes no separated final states or prediction-failure output. Lorenz's paper-local finite-precision setup is exactly the shared nearby-state setup, so the divergence and reliability adapters consume it directly. The later calculation yields the direct output-led endpoint, after which every shared claim transfers to theory and world semantics.