import PhysicsLogic.Papers.HughesRobinsonBeltranLopez1960 import PhysicsLogic.Papers.HughesRobinsonBeltranLopez1960.SourceMap import PhysicsLogic.Logic.Semantics /-! # Semantic Coverage for Hughes-Robinson-Beltran-Lopez 1960 -/ set_option autoImplicit false namespace PhysicsLogic.Papers.HughesRobinsonBeltranLopez1960 open PhysicsLogic.Logic structure SemanticContext (T : HughesTypes) where framework : HughesFramework T namespace SemanticContext variable {T : HughesTypes} def interpretAtom (context : SemanticContext T) : Atom -> Prop | .selectedP2ModelSetup => context.framework.SelectedP2ModelSetup | .atomicP2EnergyFormula => context.framework.SelectedAtomicP2EnergyFormulaAt | .atomicScanSetup => context.framework.AtomicScanSetup | .atomicNullObservation => context.framework.AtomicNullObservation | .atomicBoundCalculation => context.framework.AtomicBoundCalculation | .establishedAtomicBound => context.framework.EstablishedAtomicBound | .printedAtomicReadout => context.framework.PrintedAtomicReadoutAt | .oxygenComparisonAssessment => context.framework.OxygenComparisonAssessment | .printedOxygenReadout => context.framework.PrintedOxygenReadoutAt | .nuclearScanSetup => context.framework.NuclearScanSetup | .nuclearLineObservation => context.framework.NuclearLineObservation | .nuclearLineSignatureCalculation => context.framework.NuclearLineSignatureCalculation | .excludedTripletOrBroadening => context.framework.tripletOrBroadeningExcludedAboveAt context.framework.p2GalacticAnisotropyModel context.framework.lithiumTransition context.framework.lithiumExcessWidthLimit context.framework.selectedRegime | .nuclearBoundCalculation => context.framework.NuclearBoundCalculation | .establishedNuclearBound => context.framework.EstablishedNuclearBound | .printedNuclearReadout => context.framework.PrintedNuclearReadoutAt | .nuclearBoundStronger => context.framework.StrictNuclearSensitivityImprovement | .selectedModelExclusionBridge => context.framework.SelectedModelExclusionBridge | .boundedSelectedModelRelation => context.framework.boundedVersionOfAt context.framework.boundedSelectedAnisotropyModel context.framework.p2GalacticAnisotropyModel context.framework.nuclearAnisotropyBound context.framework.selectedRegime | .scopeQualifications => Not (context.framework.exactMassIsotropyEstablishedAt context.framework.selectedRegime) /\ Not (context.framework.otherAngularDependenceTestedAt context.framework.selectedRegime) /\ Not (context.framework.arbitraryPreferredDirectionTestedAt context.framework.selectedRegime) /\ context.framework.improvedSensitivityProposedAt context.framework.lithiumTransition context.framework.selectedRegime | .scopedAnisotropyAssessment => context.framework.EstablishedScopedAnisotropyAssessment | .assessmentSupportBridge => context.framework.ScopedAssessmentSupportsBoundedModel | .boundedModelSupport => context.framework.toEvidenceSupportContext.SupportsModel context.framework.combinedNullEvidence context.framework.boundedSelectedAnisotropyModel context.framework.selectedRegime def interpretFormula (context : SemanticContext T) (formula : Formula Atom) : Prop := formula.eval context.interpretAtom def interpretedClaims (context : SemanticContext T) : List (ClaimId × Prop) := claims.map fun claim => (claim.id, context.interpretFormula claim.formula) theorem every_source_claim_has_semantics (context : SemanticContext T) : context.interpretedClaims.length = claims.length := by simp [interpretedClaims] private theorem atomClaim (context : SemanticContext T) (id : ClaimId) (atom : Atom) (lookup : argument.claimFormula? id = some (.atom atom)) (holds : context.interpretAtom atom) : argument.ClaimHolds context.interpretAtom id := PaperArgument.claimHolds_of_formula argument context.interpretAtom id (.atom atom) lookup holds private theorem certifyPremiseFreeStep (context : SemanticContext T) (id : StepId) (conclusion : ClaimId) (lookup : argument.stepRule? id = some ([], conclusion)) (holds : argument.ClaimHolds context.interpretAtom conclusion) : argument.StepSound context.interpretAtom id := PaperArgument.stepSound_of_conclusion_lookup argument context.interpretAtom id conclusion (by decide) lookup holds private theorem atomOfPremise (context : SemanticContext T) (premiseIds : List ClaimId) (premises : argument.ClaimsHold context.interpretAtom premiseIds) (id : ClaimId) (atom : Atom) (membership : id ∈ premiseIds) (formulaLookup : argument.claimFormula? id = some (.atom atom)) : context.interpretAtom atom := PaperArgument.formula_eval_of_claimHolds argument context.interpretAtom id (.atom atom) formulaLookup (premises id membership) private theorem certifyPremiseAwareStep (context : SemanticContext T) (id : StepId) (premises : List ClaimId) (conclusion : ClaimId) (lookup : argument.stepRule? id = some (premises, conclusion)) (rule : argument.ClaimsHold context.interpretAtom premises -> argument.ClaimHolds context.interpretAtom conclusion) : argument.StepSound context.interpretAtom id := PaperArgument.stepSound_of_rule_lookup argument context.interpretAtom id premises conclusion (by decide) lookup rule private theorem certifyRoute (context : SemanticContext T) (id : RouteId) (route : ArgumentRoute RouteId RouteKind StepId ClaimId) (lookup : routedArgument.route? id = some route) (dependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom (routedArgument.routeDependencyIds route)) (stepsSound : argument.StepsSound context.interpretAtom route.steps) (derivable : RoutedArgument.stepsDerivableFrom argument (routedArgument.routeDependencyClaims route) route.steps = true) (noReductio : RoutedArgument.stepsContainNoReductio argument route.steps = true) (outputs : route.outputs.all (RoutedArgument.claimsAfterSteps argument (routedArgument.routeDependencyClaims route) route.steps).contains = true) : routedArgument.RouteSemanticallyCertified context.interpretAtom id := RoutedArgument.routeSemanticallyCertified_of_certified_dependencies routedArgument context.interpretAtom id route lookup (by decide) dependencies stepsSound derivable noReductio outputs theorem selected_model_route_is_semantically_realized (context : SemanticContext T) (model : context.framework.SelectedP2ModelSetup) (formula : context.framework.SelectedAtomicP2EnergyFormulaAt) : routedArgument.RouteSemanticallyCertified context.interpretAtom .selectedModel := by have modelClaim := atomClaim context .modelSetup .selectedP2ModelSetup (by rfl) model have formulaClaim := atomClaim context .atomicEnergyFormula .atomicP2EnergyFormula (by rfl) formula have stepsSound : argument.StepsSound context.interpretAtom selectedModelRoute.steps := by change argument.StepsSound context.interpretAtom [.stateModelSetup, .stateAtomicP2EnergyFormula] intro stepId stepMem simp at stepMem rcases stepMem with rfl | rfl · exact certifyPremiseFreeStep context .stateModelSetup .modelSetup (by decide) modelClaim · exact certifyPremiseFreeStep context .stateAtomicP2EnergyFormula .atomicEnergyFormula (by decide) formulaClaim have dependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom (routedArgument.routeDependencyIds selectedModelRoute) := by change routedArgument.RoutesSemanticallyCertified context.interpretAtom [] intro routeId routeMem simp at routeMem exact certifyRoute context .selectedModel selectedModelRoute (by rfl) dependencies stepsSound (by decide) (by decide) (by decide) theorem atomic_bound_route_is_semantically_realized (context : SemanticContext T) (dependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom (routedArgument.routeDependencyIds atomicBoundRoute)) (setup : context.framework.AtomicScanSetup) (observation : context.framework.AtomicNullObservation) (calculation : context.framework.AtomicBoundCalculation) : routedArgument.RouteSemanticallyCertified context.interpretAtom .atomicBound := by have setupClaim := atomClaim context .atomicSetup .atomicScanSetup (by rfl) setup have observationClaim := atomClaim context .atomicNull .atomicNullObservation (by rfl) observation have calculationClaim := atomClaim context .atomicCalculation .atomicBoundCalculation (by rfl) calculation have stepsSound : argument.StepsSound context.interpretAtom atomicBoundRoute.steps := by change argument.StepsSound context.interpretAtom [.stateAtomicSetup, .recordAtomicNull, .supplyAtomicCalculation, .deriveAtomicBound, .retainPrintedAtomicReadout] intro stepId stepMem simp at stepMem rcases stepMem with rfl | rfl | rfl | rfl | rfl · exact certifyPremiseFreeStep context .stateAtomicSetup .atomicSetup (by decide) setupClaim · exact certifyPremiseFreeStep context .recordAtomicNull .atomicNull (by decide) observationClaim · exact certifyPremiseFreeStep context .supplyAtomicCalculation .atomicCalculation (by decide) calculationClaim · apply certifyPremiseAwareStep context .deriveAtomicBound [.modelSetup, .atomicEnergyFormula, .atomicSetup, .atomicNull, .atomicCalculation] .atomicBound (by decide) intro premises have modelFromPremises := atomOfPremise context [.modelSetup, .atomicEnergyFormula, .atomicSetup, .atomicNull, .atomicCalculation] premises .modelSetup .selectedP2ModelSetup (by simp) (by rfl) have formulaFromPremises := atomOfPremise context [.modelSetup, .atomicEnergyFormula, .atomicSetup, .atomicNull, .atomicCalculation] premises .atomicEnergyFormula .atomicP2EnergyFormula (by simp) (by rfl) have setupFromPremises := atomOfPremise context [.modelSetup, .atomicEnergyFormula, .atomicSetup, .atomicNull, .atomicCalculation] premises .atomicSetup .atomicScanSetup (by simp) (by rfl) have observationFromPremises := atomOfPremise context [.modelSetup, .atomicEnergyFormula, .atomicSetup, .atomicNull, .atomicCalculation] premises .atomicNull .atomicNullObservation (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.modelSetup, .atomicEnergyFormula, .atomicSetup, .atomicNull, .atomicCalculation] premises .atomicCalculation .atomicBoundCalculation (by simp) (by rfl) exact atomClaim context .atomicBound .establishedAtomicBound (by rfl) (context.framework.atomic_scan_and_model_calculation_establish_bound modelFromPremises formulaFromPremises setupFromPremises observationFromPremises calculationFromPremises) · apply certifyPremiseAwareStep context .retainPrintedAtomicReadout [.atomicBound] .atomicReadout (by decide) intro premises have atomicFromPremises := atomOfPremise context [.atomicBound] premises .atomicBound .establishedAtomicBound (by simp) (by rfl) exact atomClaim context .atomicReadout .printedAtomicReadout (by rfl) (context.framework |>.established_atomic_bound_retains_printed_atomic_readout atomicFromPremises) exact certifyRoute context .atomicBound atomicBoundRoute (by rfl) dependencies stepsSound (by decide) (by decide) (by decide) theorem oxygen_comparison_route_is_semantically_realized (context : SemanticContext T) (dependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom (routedArgument.routeDependencyIds oxygenComparisonRoute)) (assessment : context.framework.OxygenComparisonAssessment) : routedArgument.RouteSemanticallyCertified context.interpretAtom .oxygenComparison := by have assessmentClaim := atomClaim context .oxygenAssessment .oxygenComparisonAssessment (by rfl) assessment have stepsSound : argument.StepsSound context.interpretAtom oxygenComparisonRoute.steps := by change argument.StepsSound context.interpretAtom [.recordOxygenComparison, .retainPrintedOxygenReadout] intro stepId stepMem simp at stepMem rcases stepMem with rfl | rfl · exact certifyPremiseFreeStep context .recordOxygenComparison .oxygenAssessment (by decide) assessmentClaim · apply certifyPremiseAwareStep context .retainPrintedOxygenReadout [.oxygenAssessment] .oxygenReadout (by decide) intro premises have oxygenFromPremises := atomOfPremise context [.oxygenAssessment] premises .oxygenAssessment .oxygenComparisonAssessment (by simp) (by rfl) exact atomClaim context .oxygenReadout .printedOxygenReadout (by rfl) (context.framework.oxygen_comparison_retains_printed_oxygen_readout oxygenFromPremises) exact certifyRoute context .oxygenComparison oxygenComparisonRoute (by rfl) dependencies stepsSound (by decide) (by decide) (by decide) theorem nuclear_bound_route_is_semantically_realized (context : SemanticContext T) (dependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom (routedArgument.routeDependencyIds nuclearBoundRoute)) (setup : context.framework.NuclearScanSetup) (observation : context.framework.NuclearLineObservation) (signatureCalculation : context.framework.NuclearLineSignatureCalculation) (calculation : context.framework.NuclearBoundCalculation) : routedArgument.RouteSemanticallyCertified context.interpretAtom .nuclearBound := by have setupClaim := atomClaim context .nuclearSetup .nuclearScanSetup (by rfl) setup have observationClaim := atomClaim context .nuclearObservation .nuclearLineObservation (by rfl) observation have signatureCalculationClaim := atomClaim context .nuclearSignatureCalculation .nuclearLineSignatureCalculation (by rfl) signatureCalculation have calculationClaim := atomClaim context .nuclearCalculation .nuclearBoundCalculation (by rfl) calculation have stepsSound : argument.StepsSound context.interpretAtom nuclearBoundRoute.steps := by change argument.StepsSound context.interpretAtom [.stateNuclearSetup, .recordNuclearLine, .supplyNuclearSignatureCalculation, .deriveSignatureExclusion, .supplyNuclearCalculation, .deriveNuclearBound, .retainPrintedNuclearReadout] intro stepId stepMem simp at stepMem rcases stepMem with rfl | rfl | rfl | rfl | rfl | rfl | rfl · exact certifyPremiseFreeStep context .stateNuclearSetup .nuclearSetup (by decide) setupClaim · exact certifyPremiseFreeStep context .recordNuclearLine .nuclearObservation (by decide) observationClaim · exact certifyPremiseFreeStep context .supplyNuclearSignatureCalculation .nuclearSignatureCalculation (by decide) signatureCalculationClaim · apply certifyPremiseAwareStep context .deriveSignatureExclusion [.modelSetup, .nuclearSetup, .nuclearObservation, .nuclearSignatureCalculation] .signatureExclusion (by decide) intro premises have modelFromPremises := atomOfPremise context [.modelSetup, .nuclearSetup, .nuclearObservation, .nuclearSignatureCalculation] premises .modelSetup .selectedP2ModelSetup (by simp) (by rfl) have setupFromPremises := atomOfPremise context [.modelSetup, .nuclearSetup, .nuclearObservation, .nuclearSignatureCalculation] premises .nuclearSetup .nuclearScanSetup (by simp) (by rfl) have observationFromPremises := atomOfPremise context [.modelSetup, .nuclearSetup, .nuclearObservation, .nuclearSignatureCalculation] premises .nuclearObservation .nuclearLineObservation (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.modelSetup, .nuclearSetup, .nuclearObservation, .nuclearSignatureCalculation] premises .nuclearSignatureCalculation .nuclearLineSignatureCalculation (by simp) (by rfl) exact atomClaim context .signatureExclusion .excludedTripletOrBroadening (by rfl) (context.framework |>.single_lithium_line_and_width_limit_exclude_predicted_signature modelFromPremises setupFromPremises observationFromPremises calculationFromPremises) · exact certifyPremiseFreeStep context .supplyNuclearCalculation .nuclearCalculation (by decide) calculationClaim · apply certifyPremiseAwareStep context .deriveNuclearBound [.modelSetup, .nuclearSetup, .nuclearObservation, .signatureExclusion, .nuclearCalculation] .nuclearBound (by decide) intro premises have modelFromPremises := atomOfPremise context [.modelSetup, .nuclearSetup, .nuclearObservation, .signatureExclusion, .nuclearCalculation] premises .modelSetup .selectedP2ModelSetup (by simp) (by rfl) have setupFromPremises := atomOfPremise context [.modelSetup, .nuclearSetup, .nuclearObservation, .signatureExclusion, .nuclearCalculation] premises .nuclearSetup .nuclearScanSetup (by simp) (by rfl) have observationFromPremises := atomOfPremise context [.modelSetup, .nuclearSetup, .nuclearObservation, .signatureExclusion, .nuclearCalculation] premises .nuclearObservation .nuclearLineObservation (by simp) (by rfl) have signatureFromPremises := atomOfPremise context [.modelSetup, .nuclearSetup, .nuclearObservation, .signatureExclusion, .nuclearCalculation] premises .signatureExclusion .excludedTripletOrBroadening (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.modelSetup, .nuclearSetup, .nuclearObservation, .signatureExclusion, .nuclearCalculation] premises .nuclearCalculation .nuclearBoundCalculation (by simp) (by rfl) exact atomClaim context .nuclearBound .establishedNuclearBound (by rfl) (context.framework |>.excluded_signature_and_model_calculation_establish_bound modelFromPremises setupFromPremises observationFromPremises signatureFromPremises calculationFromPremises) · apply certifyPremiseAwareStep context .retainPrintedNuclearReadout [.nuclearBound] .nuclearReadout (by decide) intro premises have nuclearFromPremises := atomOfPremise context [.nuclearBound] premises .nuclearBound .establishedNuclearBound (by simp) (by rfl) exact atomClaim context .nuclearReadout .printedNuclearReadout (by rfl) (context.framework |>.established_nuclear_bound_retains_printed_nuclear_readout nuclearFromPremises) exact certifyRoute context .nuclearBound nuclearBoundRoute (by rfl) dependencies stepsSound (by decide) (by decide) (by decide) theorem scoped_assessment_route_is_semantically_realized (context : SemanticContext T) (dependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom (routedArgument.routeDependencyIds scopedAssessmentRoute)) (stronger : context.framework.StrictNuclearSensitivityImprovement) (exclusion : context.framework.SelectedModelExclusionBridge) (boundedModel : context.framework.boundedVersionOfAt context.framework.boundedSelectedAnisotropyModel context.framework.p2GalacticAnisotropyModel context.framework.nuclearAnisotropyBound context.framework.selectedRegime) (notExact : Not (context.framework.exactMassIsotropyEstablishedAt context.framework.selectedRegime)) (otherDependenceOpen : Not (context.framework.otherAngularDependenceTestedAt context.framework.selectedRegime)) (otherDirectionsOpen : Not (context.framework.arbitraryPreferredDirectionTestedAt context.framework.selectedRegime)) (improvement : context.framework.improvedSensitivityProposedAt context.framework.lithiumTransition context.framework.selectedRegime) : routedArgument.RouteSemanticallyCertified context.interpretAtom .scopedAssessment := by have strongerClaim := atomClaim context .strongerBound .nuclearBoundStronger (by rfl) stronger have exclusionClaim := atomClaim context .exclusionBridge .selectedModelExclusionBridge (by rfl) exclusion have boundedModelClaim := atomClaim context .boundedModelRelation .boundedSelectedModelRelation (by rfl) boundedModel have scopeClaim := atomClaim context .scope .scopeQualifications (by rfl) ⟨notExact, otherDependenceOpen, otherDirectionsOpen, improvement⟩ have stepsSound : argument.StepsSound context.interpretAtom scopedAssessmentRoute.steps := by change argument.StepsSound context.interpretAtom [.compareBounds, .stateExclusionBridge, .identifyBoundedModel, .retainScope, .deriveScopedAssessment] intro stepId stepMem simp at stepMem rcases stepMem with rfl | rfl | rfl | rfl | rfl · exact certifyPremiseFreeStep context .compareBounds .strongerBound (by decide) strongerClaim · exact certifyPremiseFreeStep context .stateExclusionBridge .exclusionBridge (by decide) exclusionClaim · exact certifyPremiseFreeStep context .identifyBoundedModel .boundedModelRelation (by decide) boundedModelClaim · exact certifyPremiseFreeStep context .retainScope .scope (by decide) scopeClaim · apply certifyPremiseAwareStep context .deriveScopedAssessment [.atomicBound, .oxygenAssessment, .nuclearBound, .strongerBound, .exclusionBridge, .boundedModelRelation, .scope] .scopedAssessment (by decide) intro premises have atomicFromPremises := atomOfPremise context [.atomicBound, .oxygenAssessment, .nuclearBound, .strongerBound, .exclusionBridge, .boundedModelRelation, .scope] premises .atomicBound .establishedAtomicBound (by simp) (by rfl) have oxygenFromPremises := atomOfPremise context [.atomicBound, .oxygenAssessment, .nuclearBound, .strongerBound, .exclusionBridge, .boundedModelRelation, .scope] premises .oxygenAssessment .oxygenComparisonAssessment (by simp) (by rfl) have nuclearFromPremises := atomOfPremise context [.atomicBound, .oxygenAssessment, .nuclearBound, .strongerBound, .exclusionBridge, .boundedModelRelation, .scope] premises .nuclearBound .establishedNuclearBound (by simp) (by rfl) have strongerFromPremises := atomOfPremise context [.atomicBound, .oxygenAssessment, .nuclearBound, .strongerBound, .exclusionBridge, .boundedModelRelation, .scope] premises .strongerBound .nuclearBoundStronger (by simp) (by rfl) have exclusionFromPremises := atomOfPremise context [.atomicBound, .oxygenAssessment, .nuclearBound, .strongerBound, .exclusionBridge, .boundedModelRelation, .scope] premises .exclusionBridge .selectedModelExclusionBridge (by simp) (by rfl) have boundedFromPremises := atomOfPremise context [.atomicBound, .oxygenAssessment, .nuclearBound, .strongerBound, .exclusionBridge, .boundedModelRelation, .scope] premises .boundedModelRelation .boundedSelectedModelRelation (by simp) (by rfl) have scopeFromPremises := atomOfPremise context [.atomicBound, .oxygenAssessment, .nuclearBound, .strongerBound, .exclusionBridge, .boundedModelRelation, .scope] premises .scope .scopeQualifications (by simp) (by rfl) rcases scopeFromPremises with ⟨notExactFromPremises, otherDependenceFromPremises, otherDirectionsFromPremises, improvementFromPremises⟩ exact atomClaim context .scopedAssessment .scopedAnisotropyAssessment (by rfl) (context.framework |>.independent_bounds_establish_scoped_anisotropy_assessment atomicFromPremises oxygenFromPremises nuclearFromPremises strongerFromPremises exclusionFromPremises boundedFromPremises notExactFromPremises otherDependenceFromPremises otherDirectionsFromPremises improvementFromPremises) exact certifyRoute context .scopedAssessment scopedAssessmentRoute (by rfl) dependencies stepsSound (by decide) (by decide) (by decide) theorem evidence_support_route_is_semantically_realized (context : SemanticContext T) (dependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom (routedArgument.routeDependencyIds evidenceSupportRoute)) (accessible : context.framework.evidenceAccessibleAt context.framework.combinedNullEvidence context.framework.selectedRegime) (obtained : context.framework.evidenceObtainedAt context.framework.combinedNullEvidence context.framework.selectedRegime) (bridge : context.framework.ScopedAssessmentSupportsBoundedModel) : routedArgument.RouteSemanticallyCertified context.interpretAtom .evidenceSupport := by have bridgeClaim := atomClaim context .supportBridge .assessmentSupportBridge (by rfl) bridge have stepsSound : argument.StepsSound context.interpretAtom evidenceSupportRoute.steps := by change argument.StepsSound context.interpretAtom [.stateSupportBridge, .deriveModelSupport] intro stepId stepMem simp at stepMem rcases stepMem with rfl | rfl · exact certifyPremiseFreeStep context .stateSupportBridge .supportBridge (by decide) bridgeClaim · apply certifyPremiseAwareStep context .deriveModelSupport [.scopedAssessment, .supportBridge] .modelSupport (by decide) intro premises have assessmentFromPremises := atomOfPremise context [.scopedAssessment, .supportBridge] premises .scopedAssessment .scopedAnisotropyAssessment (by simp) (by rfl) have bridgeFromPremises := atomOfPremise context [.scopedAssessment, .supportBridge] premises .supportBridge .assessmentSupportBridge (by simp) (by rfl) exact atomClaim context .modelSupport .boundedModelSupport (by rfl) (context.framework |>.scoped_assessment_realizes_model_support_only_through_bridge assessmentFromPremises accessible obtained bridgeFromPremises) exact certifyRoute context .evidenceSupport evidenceSupportRoute (by rfl) dependencies stepsSound (by decide) (by decide) (by decide) theorem all_routes_are_semantically_realizable (context : SemanticContext T) (model : context.framework.SelectedP2ModelSetup) (formula : context.framework.SelectedAtomicP2EnergyFormulaAt) (atomicSetup : context.framework.AtomicScanSetup) (atomicObservation : context.framework.AtomicNullObservation) (atomicCalculation : context.framework.AtomicBoundCalculation) (oxygen : context.framework.OxygenComparisonAssessment) (nuclearSetup : context.framework.NuclearScanSetup) (nuclearObservation : context.framework.NuclearLineObservation) (nuclearSignatureCalculation : context.framework.NuclearLineSignatureCalculation) (nuclearCalculation : context.framework.NuclearBoundCalculation) (stronger : context.framework.StrictNuclearSensitivityImprovement) (exclusion : context.framework.SelectedModelExclusionBridge) (boundedModel : context.framework.boundedVersionOfAt context.framework.boundedSelectedAnisotropyModel context.framework.p2GalacticAnisotropyModel context.framework.nuclearAnisotropyBound context.framework.selectedRegime) (notExact : Not (context.framework.exactMassIsotropyEstablishedAt context.framework.selectedRegime)) (otherDependenceOpen : Not (context.framework.otherAngularDependenceTestedAt context.framework.selectedRegime)) (otherDirectionsOpen : Not (context.framework.arbitraryPreferredDirectionTestedAt context.framework.selectedRegime)) (improvement : context.framework.improvedSensitivityProposedAt context.framework.lithiumTransition context.framework.selectedRegime) (accessible : context.framework.evidenceAccessibleAt context.framework.combinedNullEvidence context.framework.selectedRegime) (obtained : context.framework.evidenceObtainedAt context.framework.combinedNullEvidence context.framework.selectedRegime) (supportBridge : context.framework.ScopedAssessmentSupportsBoundedModel) : routedArgument.RoutesSemanticallyCertified context.interpretAtom routedArgument.routeIds := by have modelCertificate := selected_model_route_is_semantically_realized context model formula have atomicDependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom (routedArgument.routeDependencyIds atomicBoundRoute) := by change routedArgument.RoutesSemanticallyCertified context.interpretAtom [.selectedModel] intro routeId routeMem simp at routeMem rcases routeMem with rfl exact modelCertificate have atomicCertificate := atomic_bound_route_is_semantically_realized context atomicDependencies atomicSetup atomicObservation atomicCalculation have oxygenDependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom (routedArgument.routeDependencyIds oxygenComparisonRoute) := by change routedArgument.RoutesSemanticallyCertified context.interpretAtom [.selectedModel] intro routeId routeMem simp at routeMem rcases routeMem with rfl exact modelCertificate have oxygenCertificate := oxygen_comparison_route_is_semantically_realized context oxygenDependencies oxygen have nuclearDependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom (routedArgument.routeDependencyIds nuclearBoundRoute) := by change routedArgument.RoutesSemanticallyCertified context.interpretAtom [.selectedModel] intro routeId routeMem simp at routeMem rcases routeMem with rfl exact modelCertificate have nuclearCertificate := nuclear_bound_route_is_semantically_realized context nuclearDependencies nuclearSetup nuclearObservation nuclearSignatureCalculation nuclearCalculation have assessmentDependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom (routedArgument.routeDependencyIds scopedAssessmentRoute) := by change routedArgument.RoutesSemanticallyCertified context.interpretAtom [.atomicBound, .oxygenComparison, .nuclearBound, .selectedModel] intro routeId routeMem simp at routeMem rcases routeMem with rfl | rfl | rfl | rfl · exact atomicCertificate · exact oxygenCertificate · exact nuclearCertificate · exact modelCertificate have assessmentCertificate := scoped_assessment_route_is_semantically_realized context assessmentDependencies stronger exclusion boundedModel notExact otherDependenceOpen otherDirectionsOpen improvement have evidenceDependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom (routedArgument.routeDependencyIds evidenceSupportRoute) := by change routedArgument.RoutesSemanticallyCertified context.interpretAtom [.scopedAssessment, .atomicBound, .oxygenComparison, .nuclearBound, .selectedModel] intro routeId routeMem simp at routeMem rcases routeMem with rfl | rfl | rfl | rfl | rfl · exact assessmentCertificate · exact atomicCertificate · exact oxygenCertificate · exact nuclearCertificate · exact modelCertificate have evidenceCertificate := evidence_support_route_is_semantically_realized context evidenceDependencies accessible obtained supportBridge change routedArgument.RoutesSemanticallyCertified context.interpretAtom [.selectedModel, .atomicBound, .oxygenComparison, .nuclearBound, .scopedAssessment, .evidenceSupport] intro routeId routeMem simp at routeMem rcases routeMem with rfl | rfl | rfl | rfl | rfl | rfl · exact modelCertificate · exact atomicCertificate · exact oxygenCertificate · exact nuclearCertificate · exact assessmentCertificate · exact evidenceCertificate theorem route_semantic_realization_is_exhaustive (context : SemanticContext T) (model : context.framework.SelectedP2ModelSetup) (formula : context.framework.SelectedAtomicP2EnergyFormulaAt) (atomicSetup : context.framework.AtomicScanSetup) (atomicObservation : context.framework.AtomicNullObservation) (atomicCalculation : context.framework.AtomicBoundCalculation) (oxygen : context.framework.OxygenComparisonAssessment) (nuclearSetup : context.framework.NuclearScanSetup) (nuclearObservation : context.framework.NuclearLineObservation) (nuclearSignatureCalculation : context.framework.NuclearLineSignatureCalculation) (nuclearCalculation : context.framework.NuclearBoundCalculation) (stronger : context.framework.StrictNuclearSensitivityImprovement) (exclusion : context.framework.SelectedModelExclusionBridge) (boundedModel : context.framework.boundedVersionOfAt context.framework.boundedSelectedAnisotropyModel context.framework.p2GalacticAnisotropyModel context.framework.nuclearAnisotropyBound context.framework.selectedRegime) (notExact : Not (context.framework.exactMassIsotropyEstablishedAt context.framework.selectedRegime)) (otherDependenceOpen : Not (context.framework.otherAngularDependenceTestedAt context.framework.selectedRegime)) (otherDirectionsOpen : Not (context.framework.arbitraryPreferredDirectionTestedAt context.framework.selectedRegime)) (improvement : context.framework.improvedSensitivityProposedAt context.framework.lithiumTransition context.framework.selectedRegime) (accessible : context.framework.evidenceAccessibleAt context.framework.combinedNullEvidence context.framework.selectedRegime) (obtained : context.framework.evidenceObtainedAt context.framework.combinedNullEvidence context.framework.selectedRegime) (supportBridge : context.framework.ScopedAssessmentSupportsBoundedModel) : routedArgument.RoutesSemanticallyCertified context.interpretAtom routedArgument.routeIds := all_routes_are_semantically_realizable context model formula atomicSetup atomicObservation atomicCalculation oxygen nuclearSetup nuclearObservation nuclearSignatureCalculation nuclearCalculation stronger exclusion boundedModel notExact otherDependenceOpen otherDirectionsOpen improvement accessible obtained supportBridge end SemanticContext end PhysicsLogic.Papers.HughesRobinsonBeltranLopez1960