import PhysicsLogic.Logic.Route /-! # Lorenz 1963 Source Map Auxiliary provenance, paper order, and epistemic classification for the proposition-valued formalization in `PhysicsLogic.Papers.Lorenz1963`. -/ set_option autoImplicit false namespace PhysicsLogic.Papers.Lorenz1963 open PhysicsLogic.Logic inductive Atom where | centralNonperiodicSetup | centralStabilityCalculations | centralTrajectoryUnstable | noncentralNonperiodicSetup | noncentralLimitCalculation | noncentralTrajectoryNotUniformlyStable | finitePrecisionSetup | trajectoryDeterminismRealization | finitePrecisionDivergenceCalculation | pointPredictionReliabilityBridge | sharedFinitePrecisionPredictabilityLimit | numericalMethodSetup | numericalMethodCalculations | numericalMethodScope | threeModeReductionSetup | threeModeReductionCalculation | boundedThreeModeModelWithLimitedScope | numericalEvidenceSetup | returnMapEvidenceCalculation | qualifiedNonperiodicEvidence | atmosphericApplicationConditional | atmosphericScopeQualifications | qualifiedAtmosphericForecastConclusion deriving DecidableEq, Repr inductive ClaimId where | centralSetup | centralCalculations | centralInstability | noncentralSetup | noncentralCalculation | noncentralInstability | predictionSetup | trajectoryDeterminism | divergenceCalculation | predictionBridge | predictionLimit | methodSetup | methodCalculations | methodResult | reductionSetup | reductionCalculation | reductionResult | evidenceSetup | evidenceCalculation | evidenceResult | atmosphereConditional | atmosphereQualifications | atmosphereResult deriving DecidableEq, Repr inductive StepId where | stateCentralSetup | supplyCentralCalculations | deriveCentralInstability | stateNoncentralSetup | supplyNoncentralCalculation | deriveNoncentralInstability | statePredictionSetup | supplyTrajectoryDeterminism | supplyDivergenceCalculation | supplyPredictionBridge | derivePredictionLimit | stateMethodSetup | supplyMethodCalculations | deriveMethodResult | stateReductionSetup | supplyReductionCalculation | deriveReductionResult | stateEvidenceSetup | supplyEvidenceCalculation | deriveEvidenceResult | stateAtmosphericConditional | stateAtmosphericQualifications | deriveAtmosphericResult deriving DecidableEq, Repr inductive RouteId where | centralNonperiodicInstability | noncentralNonuniformInstability | finitePrecisionPrediction | finiteNumericalMethod | threeModeConvectionReduction | qualifiedNumericalEvidence | atmosphericForecastScope deriving DecidableEq, Repr inductive RouteKind where | stableLimitExclusion | uniformStabilityExclusion | deterministicFiniteResolutionDivergence | boundedFiniteMemoryComputation | severeHydrodynamicTruncation | expandingReturnMapEvidence | conditionalAtmosphericExtrapolation deriving DecidableEq, Repr def originalPaper (page : Nat) (description : String) (relation : SourceRelation := .directStatement) : SourceRef := { work := "E. N. Lorenz, Deterministic Nonperiodic Flow, Journal of the Atmospheric Sciences 20 (1963) 130-141" locator := "journal p. " ++ toString page ++ ": " ++ description relation := relation } def paperClaim (id : ClaimId) (atom : Atom) (role : ClaimRole) (sources : List SourceRef) : Claim ClaimId Atom := { id := id, formula := .atom atom, role := role, sources := sources } def claims : List (Claim ClaimId Atom) := [ paperClaim .centralSetup .centralNonperiodicSetup .setupPremise [originalPaper 132 "define central, stable, quasi-periodic, and nonperiodic trajectories"], paperClaim .centralCalculations .centralStabilityCalculations .intermediate [originalPaper 133 "a trajectory with a stable limiting trajectory is quasi-periodic, and a central trajectory is its own limiting trajectory" .reconstructedStep], paperClaim .centralInstability .centralTrajectoryUnstable .mainConclusion [originalPaper 133 "a central trajectory which is not quasi-periodic is unstable"], paperClaim .noncentralSetup .noncentralNonperiodicSetup .setupPremise [originalPaper 133 "consider a noncentral nonperiodic trajectory and uniform stability"], paperClaim .noncentralCalculation .noncentralLimitCalculation .intermediate [originalPaper 133 "uniform stability supplies a stable limiting trajectory" .reconstructedStep], paperClaim .noncentralInstability .noncentralTrajectoryNotUniformlyStable .mainConclusion [originalPaper 133 "a nonperiodic noncentral trajectory is not uniformly stable"], paperClaim .predictionSetup .finitePrecisionSetup .setupPremise [originalPaper 133 "two states indistinguishable at finite observational accuracy evolve under deterministic equations"], paperClaim .trajectoryDeterminism .trajectoryDeterminismRealization .intermediate [originalPaper 132 "one unique trajectory passes through each phase-space point, specialized to the selected reference state and time" .reconstructedStep], paperClaim .divergenceCalculation .finitePrecisionDivergenceCalculation .intermediate [originalPaper 133 "arbitrarily close initial states may eventually differ by an appreciable amount" .reconstructedStep], paperClaim .predictionBridge .pointPredictionReliabilityBridge .intermediate [originalPaper 133 "a reliable distant point forecast from the finite specification would exclude such separated continuations" .reconstructedStep], paperClaim .predictionLimit .sharedFinitePrecisionPredictabilityLimit .mainConclusion [originalPaper 133 "acceptable prediction of a distant instantaneous state may be impossible despite deterministic evolution"], paperClaim .methodSetup .numericalMethodSetup .setupPremise [originalPaper 134 "integrate the dissipative finite system with finite-state digital memory, a deterministic update, and selected step"], paperClaim .methodCalculations .numericalMethodCalculations .intermediate [originalPaper 134 "derive the small-step boundedness condition, then eventual recurrence in finite memory; reject centered differences for nonunique continuation" .reconstructedStep], paperClaim .methodResult .numericalMethodScope .mainConclusion [originalPaper 134 "the bounded finite numerical sequence is eventually periodic, without making the represented flow periodic"], paperClaim .reductionSetup .threeModeReductionSetup .setupPremise [originalPaper 134 "state Saltzman's stream-function and temperature equations (17)-(18), the Rayleigh number (21), and critical value (22)", originalPaper 135 "truncate to the stream-function mode and two distinct temperature modes of equations (23)-(24)"], paperClaim .reductionCalculation .threeModeReductionCalculation .intermediate [originalPaper 135 "derive equations (25)-(27), b=4/(1+a^2), the full Jacobian (29), phase-volume law (30), divergence (31), and conduction polynomial (32)" .reconstructedStep, originalPaper 136 "retain both convective equilibria, characteristic polynomial (33), and instability threshold sigma(sigma+b+3)/(sigma-b-1) in equation (34)" .reconstructedStep], paperClaim .reductionResult .boundedThreeModeModelWithLimitedScope .mainConclusion [originalPaper 135 "phase-volume shrinkage need not collapse to a point; the original Fourier modes identify X, Y, and Z physically", originalPaper 136 "the model is physically recognizable near onset but strong-convection resemblance is not expected"], paperClaim .evidenceSetup .numericalEvidenceSetup .setupPremise [originalPaper 136 "choose sigma=10, a^2=1/2, b=8/3, r=28 above 470/19, step .01, and initial state (0,1,0)"], paperClaim .evidenceCalculation .returnMapEvidenceCalculation .intermediate [originalPaper 138 "calculate irregular transitions, successive Z maxima, and an expanding empirical two-branch return relation" .reconstructedStep, originalPaper 139 "idealize the empirical map by equation (35), retain its undefined midpoint, opposite slopes, two preimages, and all printed periodic cycles" .reconstructedStep, originalPaper 140 "apply the exact exponential phase-volume evolution (37) with sigma+b+1=41/3 and circuit duration 7/10" .reconstructedStep], paperClaim .evidenceResult .qualifiedNonperiodicEvidence .mainConclusion [originalPaper 140 "finite numerical evidence strongly supports unstable nonperiodic flow but is not mathematical proof"], paperClaim .atmosphereConditional .atmosphericApplicationConditional .intermediate [originalPaper 140 "if the atmosphere satisfies the finite deterministic nonperiodic premises, finite observational error obstructs sufficiently distant point forecasts"], paperClaim .atmosphereQualifications .atmosphericScopeQualifications .setupPremise [originalPaper 141 "atmospheric finiteness, determinism, nonperiodicity, analogue recurrence, and the practical horizon are left unsettled"], paperClaim .atmosphereResult .qualifiedAtmosphericForecastConclusion .mainConclusion [originalPaper 141 "the very-long-range forecast conclusion is conditional and its timescale may range from days to centuries"] ] def rawSteps : List (ArgumentStep StepId ClaimId) := [ { id := .stateCentralSetup, premises := [], conclusion := .centralSetup, inference := .introduce, justification := .paperDerivation }, { id := .supplyCentralCalculations, premises := [], conclusion := .centralCalculations, inference := .computation, justification := .paperDerivation }, { id := .deriveCentralInstability, premises := [.centralSetup, .centralCalculations], conclusion := .centralInstability, inference := .logicalComposition, justification := .paperDerivation }, { id := .stateNoncentralSetup, premises := [], conclusion := .noncentralSetup, inference := .introduce, justification := .paperDerivation }, { id := .supplyNoncentralCalculation, premises := [], conclusion := .noncentralCalculation, inference := .computation, justification := .paperDerivation }, { id := .deriveNoncentralInstability, premises := [.noncentralSetup, .noncentralCalculation], conclusion := .noncentralInstability, inference := .logicalComposition, justification := .paperDerivation }, { id := .statePredictionSetup, premises := [], conclusion := .predictionSetup, inference := .introduce, justification := .physicalPrinciple }, { id := .supplyTrajectoryDeterminism, premises := [], conclusion := .trajectoryDeterminism, inference := .introduce, justification := .importedResult }, { id := .supplyDivergenceCalculation, premises := [], conclusion := .divergenceCalculation, inference := .computation, justification := .paperDerivation }, { id := .supplyPredictionBridge, premises := [], conclusion := .predictionBridge, inference := .introduce, justification := .interpretiveInference }, { id := .derivePredictionLimit, premises := [.predictionSetup, .trajectoryDeterminism, .divergenceCalculation, .predictionBridge], conclusion := .predictionLimit, inference := .logicalComposition, justification := .paperDerivation }, { id := .stateMethodSetup, premises := [], conclusion := .methodSetup, inference := .introduce, justification := .paperDerivation }, { id := .supplyMethodCalculations, premises := [], conclusion := .methodCalculations, inference := .computation, justification := .paperDerivation }, { id := .deriveMethodResult, premises := [.methodSetup, .methodCalculations], conclusion := .methodResult, inference := .logicalComposition, justification := .paperDerivation }, { id := .stateReductionSetup, premises := [], conclusion := .reductionSetup, inference := .introduce, justification := .controlledApproximation }, { id := .supplyReductionCalculation, premises := [], conclusion := .reductionCalculation, inference := .computation, justification := .paperDerivation }, { id := .deriveReductionResult, premises := [.reductionSetup, .reductionCalculation], conclusion := .reductionResult, inference := .logicalComposition, justification := .controlledApproximation }, { id := .stateEvidenceSetup, premises := [], conclusion := .evidenceSetup, inference := .introduce, justification := .paperDerivation }, { id := .supplyEvidenceCalculation, premises := [], conclusion := .evidenceCalculation, inference := .computation, justification := .paperDerivation }, { id := .deriveEvidenceResult, premises := [.evidenceSetup, .evidenceCalculation], conclusion := .evidenceResult, inference := .logicalComposition, justification := .interpretiveInference }, { id := .stateAtmosphericConditional, premises := [], conclusion := .atmosphereConditional, inference := .introduce, justification := .interpretiveInference }, { id := .stateAtmosphericQualifications, premises := [], conclusion := .atmosphereQualifications, inference := .introduce, justification := .openObligation }, { id := .deriveAtmosphericResult, premises := [.atmosphereConditional, .atmosphereQualifications], conclusion := .atmosphereResult, inference := .logicalComposition, justification := .interpretiveInference } ] def stepSources : StepId → List SourceRef | .stateCentralSetup => [originalPaper 132 "state the central nonperiodic trajectory setup"] | .supplyCentralCalculations => [originalPaper 133 "compose the stable-limit and quasi-periodicity lemmas" .reconstructedStep] | .deriveCentralInstability => [originalPaper 133 "contradict nonperiodicity with quasi-periodicity"] | .stateNoncentralSetup => [originalPaper 133 "state the noncentral nonperiodic case"] | .supplyNoncentralCalculation => [originalPaper 133 "obtain a stable limiting trajectory from uniform stability" .reconstructedStep] | .deriveNoncentralInstability => [originalPaper 133 "exclude uniform stability"] | .statePredictionSetup => [originalPaper 133 "make observationally indistinguishable initial states explicit"] | .supplyTrajectoryDeterminism => [originalPaper 132 "specialize Lorenz's trajectory uniqueness to the selected reference state and time" .reconstructedStep] | .supplyDivergenceCalculation => [originalPaper 133 "supply the appreciable later separation" .reconstructedStep] | .supplyPredictionBridge => [originalPaper 133 "state the finite-resolution reliability criterion" .reconstructedStep] | .derivePredictionLimit => [originalPaper 133 "retain determinism while excluding the selected forecast"] | .stateMethodSetup => [originalPaper 134 "state the digital integration setup"] | .supplyMethodCalculations => [originalPaper 134 "derive recurrence, boundedness, and scheme scope" .reconstructedStep] | .deriveMethodResult => [originalPaper 134 "combine the numerical-method conclusions"] | .stateReductionSetup => [originalPaper 135 "state the severe Fourier truncation"] | .supplyReductionCalculation => [originalPaper 135 "derive the three ordinary differential equations" .reconstructedStep] | .deriveReductionResult => [originalPaper 136 "retain the near-onset scope limitation"] | .stateEvidenceSetup => [originalPaper 136 "state parameters, step, initial state, and run"] | .supplyEvidenceCalculation => [originalPaper 138 "construct and inspect the return relation" .reconstructedStep] | .deriveEvidenceResult => [originalPaper 140 "mark the conclusion as strong evidence, not proof"] | .stateAtmosphericConditional => [originalPaper 140 "state the conditional atmospheric implication"] | .stateAtmosphericQualifications => [originalPaper 141 "retain unresolved atmospheric premises and horizon"] | .deriveAtmosphericResult => [originalPaper 141 "form the qualified forecasting conclusion"] def steps : List (ArgumentStep StepId ClaimId) := rawSteps.map fun step => { step with sources := stepSources step.id } def centralRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .centralNonperiodicInstability, kind := .stableLimitExclusion, dependsOn := [], steps := [.stateCentralSetup, .supplyCentralCalculations, .deriveCentralInstability], outputs := [.centralInstability] } def noncentralRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .noncentralNonuniformInstability, kind := .uniformStabilityExclusion, dependsOn := [], steps := [.stateNoncentralSetup, .supplyNoncentralCalculation, .deriveNoncentralInstability], outputs := [.noncentralInstability] } def predictionRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .finitePrecisionPrediction, kind := .deterministicFiniteResolutionDivergence, dependsOn := [], steps := [.statePredictionSetup, .supplyTrajectoryDeterminism, .supplyDivergenceCalculation, .supplyPredictionBridge, .derivePredictionLimit], outputs := [.predictionLimit] } def methodRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .finiteNumericalMethod, kind := .boundedFiniteMemoryComputation, dependsOn := [], steps := [.stateMethodSetup, .supplyMethodCalculations, .deriveMethodResult], outputs := [.methodResult] } def reductionRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .threeModeConvectionReduction, kind := .severeHydrodynamicTruncation, dependsOn := [], steps := [.stateReductionSetup, .supplyReductionCalculation, .deriveReductionResult], outputs := [.reductionResult] } def evidenceRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .qualifiedNumericalEvidence, kind := .expandingReturnMapEvidence, dependsOn := [], steps := [.stateEvidenceSetup, .supplyEvidenceCalculation, .deriveEvidenceResult], outputs := [.evidenceResult] } def atmosphereRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .atmosphericForecastScope, kind := .conditionalAtmosphericExtrapolation, dependsOn := [], steps := [.stateAtmosphericConditional, .stateAtmosphericQualifications, .deriveAtmosphericResult], outputs := [.atmosphereResult] } def routes : List (ArgumentRoute RouteId RouteKind StepId ClaimId) := [centralRoute, noncentralRoute, predictionRoute, methodRoute, reductionRoute, evidenceRoute, atmosphereRoute] def argument : PaperArgument ClaimId StepId Atom := { title := "Lorenz deterministic nonperiodic flow", sources := [originalPaper 130 "complete original paper, journal pp. 130-141"], claims := claims, steps := steps, mainConclusion := .atmosphereResult } def routedArgument : RoutedArgument ClaimId StepId Atom RouteId RouteKind := { argument := argument, routes := routes } theorem argument_wellFormed : argument.wellFormed = true := by rfl theorem argument_auditable : argument.auditable = true := by rfl theorem routes_wellFormed : routedArgument.wellFormed = true := by rfl theorem routes_have_exact_predecessor_graph : centralRoute.dependsOn = [] ∧ noncentralRoute.dependsOn = [] ∧ predictionRoute.dependsOn = [] ∧ methodRoute.dependsOn = [] ∧ reductionRoute.dependsOn = [] ∧ evidenceRoute.dependsOn = [] ∧ atmosphereRoute.dependsOn = [] := by constructor · rfl constructor · rfl constructor · rfl constructor · rfl constructor · rfl constructor <;> rfl theorem routes_have_exact_dependency_closure : routedArgument.routeDependencyIds centralRoute = [] ∧ routedArgument.routeDependencyIds noncentralRoute = [] ∧ routedArgument.routeDependencyIds predictionRoute = [] ∧ routedArgument.routeDependencyIds methodRoute = [] ∧ routedArgument.routeDependencyIds reductionRoute = [] ∧ routedArgument.routeDependencyIds evidenceRoute = [] ∧ routedArgument.routeDependencyIds atmosphereRoute = [] := by constructor · rfl constructor · rfl constructor · rfl constructor · rfl constructor · rfl constructor <;> rfl -- The implication-shaped calculation and bridge atoms are source contracts. -- Result steps below apply those contracts to the selected setup atoms. theorem local_inputs_and_contracts_are_independent_hypotheses : argument.stepRule? .stateCentralSetup = some ([], .centralSetup) ∧ argument.stepRule? .supplyCentralCalculations = some ([], .centralCalculations) ∧ argument.stepRule? .stateNoncentralSetup = some ([], .noncentralSetup) ∧ argument.stepRule? .supplyNoncentralCalculation = some ([], .noncentralCalculation) ∧ argument.stepRule? .statePredictionSetup = some ([], .predictionSetup) ∧ argument.stepRule? .supplyTrajectoryDeterminism = some ([], .trajectoryDeterminism) ∧ argument.stepRule? .supplyDivergenceCalculation = some ([], .divergenceCalculation) ∧ argument.stepRule? .supplyPredictionBridge = some ([], .predictionBridge) ∧ argument.stepRule? .stateMethodSetup = some ([], .methodSetup) ∧ argument.stepRule? .supplyMethodCalculations = some ([], .methodCalculations) ∧ argument.stepRule? .stateReductionSetup = some ([], .reductionSetup) ∧ argument.stepRule? .supplyReductionCalculation = some ([], .reductionCalculation) ∧ argument.stepRule? .stateEvidenceSetup = some ([], .evidenceSetup) ∧ argument.stepRule? .supplyEvidenceCalculation = some ([], .evidenceCalculation) ∧ argument.stepRule? .stateAtmosphericConditional = some ([], .atmosphereConditional) ∧ argument.stepRule? .stateAtmosphericQualifications = some ([], .atmosphereQualifications) := by constructor · rfl constructor · rfl constructor · rfl constructor · rfl constructor · rfl constructor · rfl constructor · rfl constructor · rfl constructor · rfl constructor · rfl constructor · rfl constructor · rfl constructor · rfl constructor · rfl constructor <;> rfl theorem result_steps_apply_selected_inputs_and_contracts : argument.stepRule? .deriveCentralInstability = some ([.centralSetup, .centralCalculations], .centralInstability) ∧ argument.stepRule? .deriveNoncentralInstability = some ([.noncentralSetup, .noncentralCalculation], .noncentralInstability) ∧ argument.stepRule? .derivePredictionLimit = some ([.predictionSetup, .trajectoryDeterminism, .divergenceCalculation, .predictionBridge], .predictionLimit) ∧ argument.stepRule? .deriveMethodResult = some ([.methodSetup, .methodCalculations], .methodResult) ∧ argument.stepRule? .deriveReductionResult = some ([.reductionSetup, .reductionCalculation], .reductionResult) ∧ argument.stepRule? .deriveEvidenceResult = some ([.evidenceSetup, .evidenceCalculation], .evidenceResult) ∧ argument.stepRule? .deriveAtmosphericResult = some ([.atmosphereConditional, .atmosphereQualifications], .atmosphereResult) := by constructor · rfl constructor · rfl constructor · rfl constructor · rfl constructor · rfl constructor <;> rfl theorem numerical_evidence_is_not_classified_as_mathematical_proof : argument.ClaimReliesOnJustification .evidenceResult .interpretiveInference := by decide theorem atmospheric_unknowns_are_explicit_open_obligations : argument.ClaimReliesOnJustification .atmosphereQualifications .openObligation := by decide end PhysicsLogic.Papers.Lorenz1963