import PhysicsLogic.Papers.HastingsKoma2006
import PhysicsLogic.Papers.HastingsKoma2006.SourceMap
import PhysicsLogic.Logic.Semantics

/-!
# Semantic Coverage for Hastings-Koma 2006

Every source-map atom is interpreted through the paper-local lattice,
propagation, spectral-filtering, clustering, self-similarity, model, and
finite-degeneracy semantics. Every named route has a checked semantic
realization theorem.
-/

set_option autoImplicit false

namespace PhysicsLogic.Papers.HastingsKoma2006

open PhysicsLogic.Logic

structure SemanticContext where
  framework : PaperFramework

namespace SemanticContext

def interpretAtom (context : SemanticContext) : Atom → Prop
  | .powerLawSetup =>
      context.framework.PowerLawPropagationSetup
  | .powerLawSupportChain =>
      context.framework.SupportChainCalculation
  | .powerLawCalculation =>
      context.framework.PowerLawPropagationCalculation
  | .powerLawInterpretation =>
      context.framework.PowerLawPropagationInterpretation
  | .powerLawPropagation =>
      context.framework.EstablishedPowerLawPropagation
  | .exponentialSetup =>
      context.framework.ExponentialPropagationSetup
  | .exponentialSupportChain =>
      context.framework.SupportChainCalculation
  | .exponentialCalculation =>
      context.framework.ExponentialPropagationCalculation
  | .propagationInterpretation =>
      context.framework.PropagationInterpretation
  | .exponentialPropagation =>
      context.framework.EstablishedExponentialPropagation
  | .filteringSetup =>
      context.framework.SpectralFilteringSetup
  | .spectralDecomposition =>
      context.framework.groundStateSpectralDecompositionCalculated
        context.framework.selectedGroundState
          context.framework.selectedGroundSector
            context.framework.selectedHamiltonian
  | .gaussianFilterLemma =>
      context.framework.gaussianFrequencyFilterLemmaCalculated
        context.framework.selectedGap
  | .filteringCalculation =>
      context.framework.SpectralFilteringCalculation
  | .spectralFiltering =>
      context.framework.EstablishedSpectralFiltering
  | .bosonicSetup =>
      context.framework.BosonicClusteringSetup
  | .realTimeIntegral =>
      context.framework.finitePropagationControlsRealTimeIntegral
        context.framework.selectedPropagationBound
          context.framework.selectedGap
            context.framework.selectedCorrelationBound
  | .decayOptimization =>
      context.framework.decayParameterOptimized
        context.framework.selectedGap
          context.framework.selectedPropagationBound
            context.framework.selectedCorrelationBound
  | .finiteVolumeSetup =>
      context.framework.FiniteVolumeThermodynamicSetup
  | .finiteVolumeTransfer =>
      context.framework.FiniteVolumeThermodynamicTransfer
  | .thermodynamicTransfer =>
      context.framework.EstablishedFiniteVolumeThermodynamicClustering
  | .bosonicCalculation =>
      context.framework.BosonicClusteringCalculation
  | .bosonicClustering =>
      context.framework.BosonicCorrectedClusteringResult
  | .fermionicSetup =>
      context.framework.FermionicClusteringSetup
  | .fermionicRealTimeIntegral =>
      context.framework.finitePropagationControlsRealTimeIntegral
        context.framework.selectedPropagationBound
          context.framework.selectedGap
            context.framework.selectedCorrelationBound
  | .fermionicDecayOptimization =>
      context.framework.decayParameterOptimized
        context.framework.selectedGap
          context.framework.selectedPropagationBound
            context.framework.selectedCorrelationBound
  | .fermionicCalculation =>
      context.framework.FermionicClusteringCalculation
  | .projectionIdentity =>
      context.framework.normalizedGroundAverageProjectionIdentity
        context.framework.selectedGroundProjection
          context.framework.sourceObservable
            context.framework.targetObservable
  | .fermionicBridge =>
      context.framework.FermionicProjectionIdentityBridge
  | .fermionicDecay =>
      context.framework.EstablishedFermionicCorrelationDecay
  | .selfSimilaritySetup =>
      context.framework.SelfSimilaritySetup
  | .selfSimilarityMatrix =>
      context.framework.SelfSimilarityMatrixCalculation
  | .selfSimilarityBridge =>
      context.framework.SelfSimilarityDecayBridge
  | .selfSimilarityStrengthening =>
      context.framework.EstablishedSelfSimilarityStrengthening
  | .uOneSetup =>
      context.framework.UOneModelSetup
  | .importedUOneDecay =>
      context.framework.ImportedUOneDecayCalculation
  | .translationSelfSimilarity =>
      context.framework.TranslationSelfSimilarityCalculation
  | .uOneUpgradeCalculation =>
      context.framework.UOneExponentialUpgradeCalculation
  | .uOneModelUpgrade =>
      context.framework.EstablishedUOneModelUpgrade
  | .infiniteDegeneracySetup =>
      context.framework.InfiniteDegeneracyExtensionSetup
  | .infiniteDegeneracyMatrix =>
      context.framework.InfiniteDegeneracyMatrixCalculation
  | .infiniteDegeneracyCalculation =>
      context.framework.InfiniteDegeneracyExtensionCalculation
  | .infiniteDegeneracyExtension =>
      context.framework.EstablishedInfiniteDegeneracyExtension
  | .paperScope =>
      context.framework.PaperScopeAssessment
  | .completeScopedResult =>
      context.framework.CompleteScopedResult

def interpretFormula
    (context : SemanticContext) (formula : Formula Atom) : Prop :=
  formula.eval context.interpretAtom

def interpretedClaims
    (context : SemanticContext) : List (ClaimId × Prop) :=
  claims.map fun claim =>
    (claim.id, context.interpretFormula claim.formula)

theorem every_source_claim_has_semantics
    (context : SemanticContext) :
    context.interpretedClaims.length = claims.length := by
  simp [interpretedClaims]

/--
The source-map bosonic-clustering atom retains Hastings-Koma's printed
corrected-correlation bound in addition to the generic shared endpoint.
-/
theorem bosonic_clustering_atom_retains_printed_bound
    (context : SemanticContext)
    (clustering : context.interpretAtom .bosonicClustering) :
    context.framework.CorrectedBosonicClusteringFormulaAt := by
  change context.framework.BosonicCorrectedClusteringResult at clustering
  exact
    context.framework
      |>.bosonic_clustering_result_retains_printed_bound clustering

theorem bosonic_clustering_atom_retains_shared_correlation_decay
    (context : SemanticContext)
    (clustering : context.interpretAtom .bosonicClustering) :
    context.framework.correctedBosonicClusteringFormulaReadout
      |>.CorrectedCorrelationDecayAt := by
  change context.framework.BosonicCorrectedClusteringResult at clustering
  exact
    context.framework
      |>.bosonic_clustering_result_retains_shared_correlation_decay clustering

private theorem atomClaim
    (context : SemanticContext)
    (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)
    (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 certifyPremiseFreeAtomStep
    (context : SemanticContext)
    (id : StepId) (conclusion : ClaimId) (atom : Atom)
    (stepLookup : argument.stepRule? id = some ([], conclusion))
    (formulaLookup :
      argument.claimFormula? conclusion = some (.atom atom))
    (holds : context.interpretAtom atom) :
    argument.StepSound context.interpretAtom id :=
  certifyPremiseFreeStep context id conclusion stepLookup
    (atomClaim context conclusion atom formulaLookup holds)

private theorem atomOfPremise
    (context : SemanticContext)
    {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)
    (id : StepId) (premiseIds : List ClaimId)
    (conclusion : ClaimId) (atom : Atom)
    (stepLookup :
      argument.stepRule? id = some (premiseIds, conclusion))
    (formulaLookup :
      argument.claimFormula? conclusion = some (.atom atom))
    (derive :
      argument.ClaimsHold context.interpretAtom premiseIds →
        context.interpretAtom atom) :
    argument.StepSound context.interpretAtom id :=
  PaperArgument.stepSound_of_rule_lookup
    argument context.interpretAtom id premiseIds conclusion
      (by decide) stepLookup (fun premises =>
        atomClaim context conclusion atom formulaLookup (derive premises))

private theorem certifyIndependentRoute
    (context : SemanticContext)
    (id : RouteId)
    (route : ArgumentRoute RouteId RouteKind StepId ClaimId)
    (lookup : routedArgument.route? id = some route)
    (noDependencies : route.dependsOn = [])
    (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 := by
  apply
    RoutedArgument.routeSemanticallyCertified_of_sound_nonreductio_steps
      routedArgument context.interpretAtom id route lookup
  · rw [
      routedArgument.routeDependencyClaims_eq_nil_of_dependsOn_eq_nil
        route noDependencies]
    intro claim claimMem
    simp at claimMem
  · exact stepsSound
  · exact derivable
  · exact noReductio
  · exact outputs

private theorem certifyDependentRoute
    (context : SemanticContext)
    (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 power_law_propagation_route_is_semantically_realized
    (context : SemanticContext)
    (setup : context.framework.PowerLawPropagationSetup)
    (supportChain : context.framework.SupportChainCalculation)
    (calculation : context.framework.PowerLawPropagationCalculation)
    (interpretation : context.framework.PowerLawPropagationInterpretation) :
    routedArgument.RouteSemanticallyCertified
      context.interpretAtom .powerLawPropagation := by
  apply certifyIndependentRoute context .powerLawPropagation
    powerLawRoute (by rfl) (by rfl)
  · intro stepId stepMem
    simp [powerLawRoute] at stepMem
    rcases stepMem with rfl | rfl | rfl | rfl | rfl
    · exact certifyPremiseFreeAtomStep context .statePowerLawSetup
        .powerLawSetup .powerLawSetup (by decide) (by rfl) setup
    · exact certifyPremiseFreeAtomStep context .supplyPowerLawSupportChain
        .powerLawSupportChain .powerLawSupportChain
          (by decide) (by rfl) supportChain
    · exact certifyPremiseFreeAtomStep context .supplyPowerLawCalculation
        .powerLawCalculation .powerLawCalculation
          (by decide) (by rfl) calculation
    · exact certifyPremiseFreeAtomStep context .supplyPowerLawInterpretation
        .powerLawInterpretation .powerLawInterpretation
          (by decide) (by rfl) interpretation
    · apply certifyPremiseAwareStep context .derivePowerLawPropagation
        [.powerLawSetup, .powerLawSupportChain,
          .powerLawCalculation, .powerLawInterpretation]
        .powerLawPropagation .powerLawPropagation (by decide) (by rfl)
      intro premises
      have selectedSetup :=
        atomOfPremise context premises .powerLawSetup .powerLawSetup
          (by simp) (by rfl)
      have selectedSupportChain :=
        atomOfPremise context premises .powerLawSupportChain
          .powerLawSupportChain (by simp) (by rfl)
      have selectedCalculation :=
        atomOfPremise context premises .powerLawCalculation
          .powerLawCalculation (by simp) (by rfl)
      have selectedInterpretation :=
        atomOfPremise context premises .powerLawInterpretation
          .powerLawInterpretation (by simp) (by rfl)
      exact
        context.framework
          |>.support_chain_iteration_establishes_power_law_propagation
            selectedSetup selectedSupportChain selectedCalculation
              selectedInterpretation
  · rfl
  · rfl
  · rfl

theorem exponential_propagation_route_is_semantically_realized
    (context : SemanticContext)
    (setup : context.framework.ExponentialPropagationSetup)
    (supportChain : context.framework.SupportChainCalculation)
    (calculation : context.framework.ExponentialPropagationCalculation)
    (interpretation : context.framework.PropagationInterpretation) :
    routedArgument.RouteSemanticallyCertified
      context.interpretAtom .exponentialPropagation := by
  apply certifyIndependentRoute context .exponentialPropagation
    exponentialRoute (by rfl) (by rfl)
  · intro stepId stepMem
    simp [exponentialRoute] at stepMem
    rcases stepMem with rfl | rfl | rfl | rfl | rfl
    · exact certifyPremiseFreeAtomStep context .stateExponentialSetup
        .exponentialSetup .exponentialSetup (by decide) (by rfl) setup
    · exact certifyPremiseFreeAtomStep context
        .supplyExponentialSupportChain .exponentialSupportChain
        .exponentialSupportChain (by decide) (by rfl) supportChain
    · exact certifyPremiseFreeAtomStep context .supplyExponentialCalculation
        .exponentialCalculation .exponentialCalculation
          (by decide) (by rfl) calculation
    · exact certifyPremiseFreeAtomStep context
        .supplyPropagationInterpretation .propagationInterpretation
        .propagationInterpretation (by decide) (by rfl) interpretation
    · apply certifyPremiseAwareStep context .deriveExponentialPropagation
        [.exponentialSetup, .exponentialSupportChain,
          .exponentialCalculation, .propagationInterpretation]
        .exponentialPropagation .exponentialPropagation (by decide) (by rfl)
      intro premises
      have selectedSetup :=
        atomOfPremise context premises .exponentialSetup .exponentialSetup
          (by simp) (by rfl)
      have selectedSupportChain :=
        atomOfPremise context premises .exponentialSupportChain
          .exponentialSupportChain (by simp) (by rfl)
      have selectedCalculation :=
        atomOfPremise context premises .exponentialCalculation
          .exponentialCalculation (by simp) (by rfl)
      have selectedInterpretation :=
        atomOfPremise context premises .propagationInterpretation
          .propagationInterpretation (by simp) (by rfl)
      exact
        context.framework
          |>.support_chain_iteration_establishes_exponential_propagation
            selectedSetup selectedSupportChain selectedCalculation
              selectedInterpretation
  · rfl
  · rfl
  · rfl

theorem spectral_filtering_route_is_semantically_realized
    (context : SemanticContext)
    (setup : context.framework.SpectralFilteringSetup)
    (spectral :
      context.framework.groundStateSpectralDecompositionCalculated
        context.framework.selectedGroundState
          context.framework.selectedGroundSector
            context.framework.selectedHamiltonian)
    (filterLemma :
      context.framework.gaussianFrequencyFilterLemmaCalculated
        context.framework.selectedGap)
    (calculation : context.framework.SpectralFilteringCalculation) :
    routedArgument.RouteSemanticallyCertified
      context.interpretAtom .spectralFiltering := by
  apply certifyIndependentRoute context .spectralFiltering
    filteringRoute (by rfl) (by rfl)
  · intro stepId stepMem
    simp [filteringRoute] at stepMem
    rcases stepMem with rfl | rfl | rfl | rfl | rfl
    · exact certifyPremiseFreeAtomStep context .stateFilteringSetup
        .filteringSetup .filteringSetup (by decide) (by rfl) setup
    · exact certifyPremiseFreeAtomStep context .supplySpectralDecomposition
        .spectralDecomposition .spectralDecomposition
          (by decide) (by rfl) spectral
    · exact certifyPremiseFreeAtomStep context .supplyGaussianFilterLemma
        .gaussianFilterLemma .gaussianFilterLemma
          (by decide) (by rfl) filterLemma
    · exact certifyPremiseFreeAtomStep context .supplyFilteringCalculation
        .filteringCalculation .filteringCalculation
          (by decide) (by rfl) calculation
    · apply certifyPremiseAwareStep context .deriveSpectralFiltering
        [.filteringSetup, .spectralDecomposition,
          .gaussianFilterLemma, .filteringCalculation]
        .spectralFiltering .spectralFiltering (by decide) (by rfl)
      intro premises
      have selectedSetup :=
        atomOfPremise context premises .filteringSetup .filteringSetup
          (by simp) (by rfl)
      have selectedSpectral :=
        atomOfPremise context premises .spectralDecomposition
          .spectralDecomposition (by simp) (by rfl)
      have selectedFilterLemma :=
        atomOfPremise context premises .gaussianFilterLemma
          .gaussianFilterLemma (by simp) (by rfl)
      have selectedCalculation :=
        atomOfPremise context premises .filteringCalculation
          .filteringCalculation (by simp) (by rfl)
      exact
        context.framework
          |>.gaussian_filter_separates_excited_and_ground_sector_terms
            selectedSetup selectedSpectral selectedFilterLemma
              selectedCalculation
  · rfl
  · rfl
  · rfl

theorem bosonic_corrected_clustering_route_is_semantically_realized
    (context : SemanticContext)
    (dependencies :
      routedArgument.RoutesSemanticallyCertified context.interpretAtom
        (routedArgument.routeDependencyIds bosonicRoute))
    (setup : context.framework.BosonicClusteringSetup)
    (integral :
      context.framework.finitePropagationControlsRealTimeIntegral
        context.framework.selectedPropagationBound
          context.framework.selectedGap
            context.framework.selectedCorrelationBound)
    (optimization :
      context.framework.decayParameterOptimized
        context.framework.selectedGap
          context.framework.selectedPropagationBound
            context.framework.selectedCorrelationBound)
    (finiteSetup :
      context.framework.FiniteVolumeThermodynamicSetup)
    (transfer :
      context.framework.FiniteVolumeThermodynamicTransfer)
    (calculation : context.framework.BosonicClusteringCalculation) :
    routedArgument.RouteSemanticallyCertified
      context.interpretAtom .bosonicCorrectedClustering := by
  apply certifyDependentRoute context .bosonicCorrectedClustering
    bosonicRoute (by rfl) dependencies
  · intro stepId stepMem
    simp [bosonicRoute] at stepMem
    rcases stepMem with
      rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl
    · exact certifyPremiseFreeAtomStep context .stateBosonicSetup
        .bosonicSetup .bosonicSetup (by decide) (by rfl) setup
    · exact certifyPremiseFreeAtomStep context .supplyRealTimeIntegral
        .realTimeIntegral .realTimeIntegral (by decide) (by rfl) integral
    · exact certifyPremiseFreeAtomStep context .supplyDecayOptimization
        .decayOptimization .decayOptimization
          (by decide) (by rfl) optimization
    · exact certifyPremiseFreeAtomStep context .stateFiniteVolumeSetup
        .finiteVolumeSetup .finiteVolumeSetup
          (by decide) (by rfl) finiteSetup
    · exact certifyPremiseFreeAtomStep context .supplyFiniteVolumeTransfer
        .finiteVolumeTransfer .finiteVolumeTransfer
          (by decide) (by rfl) transfer
    · apply certifyPremiseAwareStep context .transferThermodynamicLimit
        [.finiteVolumeSetup, .finiteVolumeTransfer]
        .thermodynamicTransfer .thermodynamicTransfer (by decide) (by rfl)
      intro premises
      have selectedSetup :=
        atomOfPremise context premises .finiteVolumeSetup
          .finiteVolumeSetup (by simp) (by rfl)
      have selectedTransfer :=
        atomOfPremise context premises .finiteVolumeTransfer
          .finiteVolumeTransfer (by simp) (by rfl)
      exact
        context.framework
          |>.uniform_finite_volume_bounds_transfer_bosonic_clustering
            selectedSetup selectedTransfer
    · exact certifyPremiseFreeAtomStep context .supplyBosonicCalculation
        .bosonicCalculation .bosonicCalculation
          (by decide) (by rfl) calculation
    · apply certifyPremiseAwareStep context .deriveBosonicClustering
        [.bosonicSetup, .realTimeIntegral, .decayOptimization,
          .thermodynamicTransfer, .bosonicCalculation]
        .bosonicClustering .bosonicClustering (by decide) (by rfl)
      intro premises
      have selectedSetup :=
        atomOfPremise context premises .bosonicSetup .bosonicSetup
          (by simp) (by rfl)
      have selectedIntegral :=
        atomOfPremise context premises .realTimeIntegral .realTimeIntegral
          (by simp) (by rfl)
      have selectedOptimization :=
        atomOfPremise context premises .decayOptimization .decayOptimization
          (by simp) (by rfl)
      have selectedThermodynamic :=
        atomOfPremise context premises .thermodynamicTransfer
          .thermodynamicTransfer (by simp) (by rfl)
      have selectedCalculation :=
        atomOfPremise context premises .bosonicCalculation
          .bosonicCalculation (by simp) (by rfl)
      exact
        context.framework
          |>.gap_filter_and_real_time_bound_establish_bosonic_clustering_with_formula
            selectedSetup selectedIntegral selectedOptimization
              selectedThermodynamic selectedCalculation
  · rfl
  · rfl
  · rfl

theorem fermionic_correlation_decay_route_is_semantically_realized
    (context : SemanticContext)
    (dependencies :
      routedArgument.RoutesSemanticallyCertified context.interpretAtom
        (routedArgument.routeDependencyIds fermionicRoute))
    (setup : context.framework.FermionicClusteringSetup)
    (integral :
      context.framework.finitePropagationControlsRealTimeIntegral
        context.framework.selectedPropagationBound
          context.framework.selectedGap
            context.framework.selectedCorrelationBound)
    (optimization :
      context.framework.decayParameterOptimized
        context.framework.selectedGap
          context.framework.selectedPropagationBound
            context.framework.selectedCorrelationBound)
    (calculation : context.framework.FermionicClusteringCalculation)
    (identity :
      context.framework.normalizedGroundAverageProjectionIdentity
        context.framework.selectedGroundProjection
          context.framework.sourceObservable
            context.framework.targetObservable)
    (bridge : context.framework.FermionicProjectionIdentityBridge) :
    routedArgument.RouteSemanticallyCertified
      context.interpretAtom .fermionicCorrelationDecay := by
  apply certifyDependentRoute context .fermionicCorrelationDecay
    fermionicRoute (by rfl) dependencies
  · intro stepId stepMem
    simp [fermionicRoute] at stepMem
    rcases stepMem with
      rfl | rfl | rfl | rfl | rfl | rfl | rfl
    · exact certifyPremiseFreeAtomStep context .stateFermionicSetup
        .fermionicSetup .fermionicSetup (by decide) (by rfl) setup
    · exact certifyPremiseFreeAtomStep context
        .supplyFermionicRealTimeIntegral .fermionicRealTimeIntegral
        .fermionicRealTimeIntegral (by decide) (by rfl) integral
    · exact certifyPremiseFreeAtomStep context
        .supplyFermionicDecayOptimization .fermionicDecayOptimization
        .fermionicDecayOptimization (by decide) (by rfl) optimization
    · exact certifyPremiseFreeAtomStep context .supplyFermionicCalculation
        .fermionicCalculation .fermionicCalculation
          (by decide) (by rfl) calculation
    · exact certifyPremiseFreeAtomStep context .supplyProjectionIdentity
        .projectionIdentity .projectionIdentity (by decide) (by rfl) identity
    · exact certifyPremiseFreeAtomStep context .supplyFermionicBridge
        .fermionicBridge .fermionicBridge (by decide) (by rfl) bridge
    · apply certifyPremiseAwareStep context .deriveFermionicDecay
        [.fermionicSetup, .fermionicRealTimeIntegral,
          .fermionicDecayOptimization, .fermionicCalculation,
          .projectionIdentity, .fermionicBridge]
        .fermionicDecay .fermionicDecay (by decide) (by rfl)
      intro premises
      have selectedSetup :=
        atomOfPremise context premises .fermionicSetup .fermionicSetup
          (by simp) (by rfl)
      have selectedIntegral :=
        atomOfPremise context premises .fermionicRealTimeIntegral
          .fermionicRealTimeIntegral (by simp) (by rfl)
      have selectedOptimization :=
        atomOfPremise context premises .fermionicDecayOptimization
          .fermionicDecayOptimization (by simp) (by rfl)
      have selectedCalculation :=
        atomOfPremise context premises .fermionicCalculation
          .fermionicCalculation (by simp) (by rfl)
      have selectedIdentity :=
        atomOfPremise context premises .projectionIdentity
          .projectionIdentity (by simp) (by rfl)
      have selectedBridge :=
        atomOfPremise context premises .fermionicBridge .fermionicBridge
          (by simp) (by rfl)
      exact
        context.framework
          |>.anticommutator_route_and_projection_identity_yield_fermion_decay
            selectedSetup selectedIntegral selectedOptimization
              selectedCalculation selectedIdentity selectedBridge
  · rfl
  · rfl
  · rfl

theorem self_similarity_strengthening_route_is_semantically_realized
    (context : SemanticContext)
    (dependencies :
      routedArgument.RoutesSemanticallyCertified context.interpretAtom
        (routedArgument.routeDependencyIds selfSimilarityRoute))
    (setup : context.framework.SelfSimilaritySetup)
    (matrix : context.framework.SelfSimilarityMatrixCalculation)
    (bridge : context.framework.SelfSimilarityDecayBridge) :
    routedArgument.RouteSemanticallyCertified
      context.interpretAtom .selfSimilarityStrengthening := by
  apply certifyDependentRoute context .selfSimilarityStrengthening
    selfSimilarityRoute (by rfl) dependencies
  · intro stepId stepMem
    simp [selfSimilarityRoute] at stepMem
    rcases stepMem with rfl | rfl | rfl | rfl
    · exact certifyPremiseFreeAtomStep context .stateSelfSimilaritySetup
        .selfSimilaritySetup .selfSimilaritySetup
          (by decide) (by rfl) setup
    · exact certifyPremiseFreeAtomStep context .supplySelfSimilarityMatrix
        .selfSimilarityMatrix .selfSimilarityMatrix
          (by decide) (by rfl) matrix
    · exact certifyPremiseFreeAtomStep context .supplySelfSimilarityBridge
        .selfSimilarityBridge .selfSimilarityBridge
          (by decide) (by rfl) bridge
    · apply certifyPremiseAwareStep context
        .deriveSelfSimilarityStrengthening
        [.selfSimilaritySetup, .selfSimilarityMatrix,
          .selfSimilarityBridge]
        .selfSimilarityStrengthening .selfSimilarityStrengthening
          (by decide) (by rfl)
      intro premises
      have selectedSetup :=
        atomOfPremise context premises .selfSimilaritySetup
          .selfSimilaritySetup (by simp) (by rfl)
      have selectedMatrix :=
        atomOfPremise context premises .selfSimilarityMatrix
          .selfSimilarityMatrix (by simp) (by rfl)
      have selectedBridge :=
        atomOfPremise context premises .selfSimilarityBridge
          .selfSimilarityBridge (by simp) (by rfl)
      exact
        context.framework
          |>.self_similarity_removes_the_ground_sector_correction
            selectedSetup selectedMatrix selectedBridge
  · rfl
  · rfl
  · rfl

theorem uone_model_upgrade_route_is_semantically_realized
    (context : SemanticContext)
    (dependencies :
      routedArgument.RoutesSemanticallyCertified context.interpretAtom
        (routedArgument.routeDependencyIds uOneRoute))
    (setup : context.framework.UOneModelSetup)
    (prior : context.framework.ImportedUOneDecayCalculation)
    (translation :
      context.framework.TranslationSelfSimilarityCalculation)
    (upgrade : context.framework.UOneExponentialUpgradeCalculation) :
    routedArgument.RouteSemanticallyCertified
      context.interpretAtom .uOneModelUpgrade := by
  apply certifyDependentRoute context .uOneModelUpgrade
    uOneRoute (by rfl) dependencies
  · intro stepId stepMem
    simp [uOneRoute] at stepMem
    rcases stepMem with rfl | rfl | rfl | rfl | rfl
    · exact certifyPremiseFreeAtomStep context .stateUOneSetup
        .uOneSetup .uOneSetup (by decide) (by rfl) setup
    · exact certifyPremiseFreeAtomStep context .supplyImportedUOneDecay
        .importedUOneDecay .importedUOneDecay
          (by decide) (by rfl) prior
    · exact certifyPremiseFreeAtomStep context
        .supplyTranslationSelfSimilarity .translationSelfSimilarity
        .translationSelfSimilarity (by decide) (by rfl) translation
    · exact certifyPremiseFreeAtomStep context
        .supplyUOneUpgradeCalculation .uOneUpgradeCalculation
        .uOneUpgradeCalculation (by decide) (by rfl) upgrade
    · apply certifyPremiseAwareStep context .deriveUOneModelUpgrade
        [.uOneSetup, .importedUOneDecay,
          .translationSelfSimilarity, .bosonicClustering,
          .uOneUpgradeCalculation]
        .uOneModelUpgrade .uOneModelUpgrade (by decide) (by rfl)
      intro premises
      have selectedSetup :=
        atomOfPremise context premises .uOneSetup .uOneSetup
          (by simp) (by rfl)
      have selectedPrior :=
        atomOfPremise context premises .importedUOneDecay
          .importedUOneDecay (by simp) (by rfl)
      have selectedTranslation :=
        atomOfPremise context premises .translationSelfSimilarity
          .translationSelfSimilarity (by simp) (by rfl)
      have selectedClustering :=
        atomOfPremise context premises .bosonicClustering
          .bosonicClustering (by simp) (by rfl)
      have selectedUpgrade :=
        atomOfPremise context premises .uOneUpgradeCalculation
          .uOneUpgradeCalculation (by simp) (by rfl)
      exact
        context.framework
          |>.imported_uone_decay_and_translation_upgrade_model_correlations
            selectedSetup selectedPrior selectedTranslation
              selectedClustering.1 selectedUpgrade
  · rfl
  · rfl
  · rfl

theorem infinite_degeneracy_extension_route_is_semantically_realized
    (context : SemanticContext)
    (dependencies :
      routedArgument.RoutesSemanticallyCertified context.interpretAtom
        (routedArgument.routeDependencyIds infiniteDegeneracyRoute))
    (setup : context.framework.InfiniteDegeneracyExtensionSetup)
    (matrix : context.framework.InfiniteDegeneracyMatrixCalculation)
    (extension :
      context.framework.InfiniteDegeneracyExtensionCalculation) :
    routedArgument.RouteSemanticallyCertified
      context.interpretAtom .infiniteDegeneracyExtension := by
  apply certifyDependentRoute context .infiniteDegeneracyExtension
    infiniteDegeneracyRoute (by rfl) dependencies
  · intro stepId stepMem
    simp [infiniteDegeneracyRoute] at stepMem
    rcases stepMem with rfl | rfl | rfl | rfl
    · exact certifyPremiseFreeAtomStep context
        .stateInfiniteDegeneracySetup .infiniteDegeneracySetup
        .infiniteDegeneracySetup (by decide) (by rfl) setup
    · exact certifyPremiseFreeAtomStep context
        .supplyInfiniteDegeneracyMatrix .infiniteDegeneracyMatrix
        .infiniteDegeneracyMatrix (by decide) (by rfl) matrix
    · exact certifyPremiseFreeAtomStep context
        .supplyInfiniteDegeneracyCalculation .infiniteDegeneracyCalculation
        .infiniteDegeneracyCalculation (by decide) (by rfl) extension
    · apply certifyPremiseAwareStep context
        .deriveInfiniteDegeneracyExtension
        [.infiniteDegeneracySetup, .infiniteDegeneracyMatrix,
          .infiniteDegeneracyCalculation]
        .infiniteDegeneracyExtension .infiniteDegeneracyExtension
          (by decide) (by rfl)
      intro premises
      have selectedSetup :=
        atomOfPremise context premises .infiniteDegeneracySetup
          .infiniteDegeneracySetup (by simp) (by rfl)
      have selectedMatrix :=
        atomOfPremise context premises .infiniteDegeneracyMatrix
          .infiniteDegeneracyMatrix (by simp) (by rfl)
      have selectedExtension :=
        atomOfPremise context premises .infiniteDegeneracyCalculation
          .infiniteDegeneracyCalculation (by simp) (by rfl)
      exact
        context.framework
          |>.controlled_finite_volume_degeneracy_extends_clustering
            selectedSetup selectedMatrix selectedExtension
  · rfl
  · rfl
  · rfl

theorem complete_scoped_result_route_is_semantically_realized
    (context : SemanticContext)
    (dependencies :
      routedArgument.RoutesSemanticallyCertified context.interpretAtom
        (routedArgument.routeDependencyIds completeRoute))
    (scope : context.framework.PaperScopeAssessment) :
    routedArgument.RouteSemanticallyCertified
      context.interpretAtom .completeScopedResult := by
  apply certifyDependentRoute context .completeScopedResult
    completeRoute (by rfl) dependencies
  · intro stepId stepMem
    simp [completeRoute] at stepMem
    rcases stepMem with rfl | rfl
    · exact certifyPremiseFreeAtomStep context .recordPaperScope
        .paperScope .paperScope (by decide) (by rfl) scope
    · apply certifyPremiseAwareStep context .assembleCompleteResult
        [.powerLawPropagation, .exponentialPropagation,
          .spectralFiltering, .bosonicClustering, .fermionicDecay,
          .selfSimilarityStrengthening, .uOneModelUpgrade,
          .infiniteDegeneracyExtension, .paperScope]
        .completeResult .completeScopedResult (by decide) (by rfl)
      intro premises
      have selectedPower :=
        atomOfPremise context premises .powerLawPropagation
          .powerLawPropagation (by simp) (by rfl)
      have selectedExponential :=
        atomOfPremise context premises .exponentialPropagation
          .exponentialPropagation (by simp) (by rfl)
      have selectedFiltering :=
        atomOfPremise context premises .spectralFiltering
          .spectralFiltering (by simp) (by rfl)
      have selectedBosonic :=
        atomOfPremise context premises .bosonicClustering
          .bosonicClustering (by simp) (by rfl)
      have selectedFermionic :=
        atomOfPremise context premises .fermionicDecay
          .fermionicDecay (by simp) (by rfl)
      have selectedSelfSimilarity :=
        atomOfPremise context premises .selfSimilarityStrengthening
          .selfSimilarityStrengthening (by simp) (by rfl)
      have selectedUOne :=
        atomOfPremise context premises .uOneModelUpgrade
          .uOneModelUpgrade (by simp) (by rfl)
      have selectedInfiniteDegeneracy :=
        atomOfPremise context premises .infiniteDegeneracyExtension
          .infiniteDegeneracyExtension (by simp) (by rfl)
      have selectedScope :=
        atomOfPremise context premises .paperScope .paperScope
          (by simp) (by rfl)
      exact
        context.framework
          |>.independent_routes_establish_complete_scoped_result
            selectedPower selectedExponential selectedFiltering
              selectedBosonic.1 selectedFermionic selectedSelfSimilarity
                selectedUOne selectedInfiniteDegeneracy selectedScope
  · rfl
  · rfl
  · rfl

theorem route_semantic_realization_is_exhaustive
    (context : SemanticContext)
    (power :
      routedArgument.RouteSemanticallyCertified
        context.interpretAtom .powerLawPropagation)
    (exponential :
      routedArgument.RouteSemanticallyCertified
        context.interpretAtom .exponentialPropagation)
    (filtering :
      routedArgument.RouteSemanticallyCertified
        context.interpretAtom .spectralFiltering)
    (bosonic :
      routedArgument.RouteSemanticallyCertified
        context.interpretAtom .bosonicCorrectedClustering)
    (fermionic :
      routedArgument.RouteSemanticallyCertified
        context.interpretAtom .fermionicCorrelationDecay)
    (selfSimilarity :
      routedArgument.RouteSemanticallyCertified
        context.interpretAtom .selfSimilarityStrengthening)
    (uOne :
      routedArgument.RouteSemanticallyCertified
        context.interpretAtom .uOneModelUpgrade)
    (infiniteDegeneracy :
      routedArgument.RouteSemanticallyCertified
        context.interpretAtom .infiniteDegeneracyExtension)
    (complete :
      routedArgument.RouteSemanticallyCertified
        context.interpretAtom .completeScopedResult) :
    ∀ routeId,
      routeId ∈ routedArgument.routeIds →
        routedArgument.RouteSemanticallyCertified
          context.interpretAtom routeId := by
  intro routeId routeMem
  change routeId ∈
    [.powerLawPropagation, .exponentialPropagation,
      .spectralFiltering, .bosonicCorrectedClustering,
      .fermionicCorrelationDecay, .selfSimilarityStrengthening,
      .uOneModelUpgrade, .infiniteDegeneracyExtension,
      .completeScopedResult] at routeMem
  simp at routeMem
  rcases routeMem with
    rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl
  · exact power
  · exact exponential
  · exact filtering
  · exact bosonic
  · exact fermionic
  · exact selfSimilarity
  · exact uOne
  · exact infiniteDegeneracy
  · exact complete

theorem actual_ground_sector_inputs_realize_source_filtering_route
    (context : SemanticContext) (localSystem : context.framework.LocalQuantumSystemSetup)
    (ground : context.framework.groundData.AdmissibleAt context.framework.selectedInteraction
      context.framework.selectedGroundState context.framework.selectedGap)
    (separation : context.framework.ObservableSeparationSetup)
    (spectral : context.framework.groundStateSpectralDecompositionCalculated
      context.framework.selectedGroundState context.framework.selectedGroundSector context.framework.selectedHamiltonian)
    (filterLemma : context.framework.gaussianFrequencyFilterLemmaCalculated context.framework.selectedGap)
    (calculation : context.framework.SpectralFilteringCalculation) :
    routedArgument.RouteSemanticallyCertified context.interpretAtom .spectralFiltering :=
  context.spectral_filtering_route_is_semantically_realized
    ⟨context.framework.actual_ground_sector_realizes_uniform_gap_setup localSystem ground, separation⟩
    spectral filterLemma calculation

theorem actual_weak_star_inputs_realize_source_bosonic_route
    (context : SemanticContext)
    (dependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom
      (routedArgument.routeDependencyIds bosonicRoute))
    (setup : context.framework.BosonicClusteringSetup)
    (integral : context.framework.finitePropagationControlsRealTimeIntegral
      context.framework.selectedPropagationBound context.framework.selectedGap context.framework.selectedCorrelationBound)
    (optimization : context.framework.decayParameterOptimized context.framework.selectedGap
      context.framework.selectedPropagationBound context.framework.selectedCorrelationBound)
    (finiteSetup : context.framework.FiniteVolumeThermodynamicSetup)
    (calculation : context.framework.BosonicClusteringCalculation) :
    routedArgument.RouteSemanticallyCertified context.interpretAtom .bosonicCorrectedClustering :=
  context.bosonic_corrected_clustering_route_is_semantically_realized dependencies setup integral optimization
    finiteSetup context.framework.actual_weak_star_semantics_supply_finite_volume_transfer calculation

theorem actual_ground_average_inputs_realize_source_fermionic_route
    (context : SemanticContext)
    (dependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom
      (routedArgument.routeDependencyIds fermionicRoute))
    (setup : context.framework.FermionicClusteringSetup)
    (integral : context.framework.finitePropagationControlsRealTimeIntegral
      context.framework.selectedPropagationBound context.framework.selectedGap context.framework.selectedCorrelationBound)
    (optimization : context.framework.decayParameterOptimized context.framework.selectedGap
      context.framework.selectedPropagationBound context.framework.selectedCorrelationBound)
    (calculation : context.framework.FermionicClusteringCalculation)
    (average : context.framework.groundData.AverageWeakStarLimitAt) :
    routedArgument.RouteSemanticallyCertified context.interpretAtom .fermionicCorrelationDecay :=
  context.fermionic_correlation_decay_route_is_semantically_realized dependencies setup integral optimization calculation
    (context.framework.actual_ground_average_supplies_projection_identity average)
    context.framework.actual_ground_average_correction_derives_fermionic_bridge

theorem bosonic_clustering_atom_retains_actual_ground_sector
    (context : SemanticContext) (clustering : context.interpretAtom .bosonicClustering) :
    context.framework.groundData.AdmissibleAt context.framework.selectedInteraction
      context.framework.selectedGroundState context.framework.selectedGap :=
  context.framework.uniform_gap_setup_retains_actual_ground_sector clustering.1.1.2.1.1.1

local instance (context : SemanticContext) : CStarAlgebra context.framework.operatorModel.Operator :=
  context.framework.operatorModel.operatorAlgebra

open PhysicsLogic.Framework in
theorem bosonic_clustering_atom_realizes_finite_hamiltonian_dynamics
    (context : SemanticContext) (clustering : context.interpretAtom .bosonicClustering)
    (volume : Lattice) (admissible : context.framework.groundData.admissibleVolume volume) :
    ∃ dynamics : QuantumGroundSector.HamiltonianDynamics
        (context.framework.groundData.finiteSector volume).StateSpace,
      dynamics.hamiltonian =
        (context.framework.groundData.finiteSector volume).hamiltonianOperator.toPMap ⊤ ∧
      dynamics.RealTimeGeneratorAt ∧
      ∀ (time : Real) (observable : context.framework.operatorModel.Operator),
        observable ∈ context.framework.operatorModel.localAlgebra
          (context.framework.groundData.finiteSites volume) →
        context.framework.groundData.restriction volume
          (QuantumCommutator.finiteVolumeHeisenberg
            (context.framework.operatorModel.finiteVolumeHamiltonian context.framework.selectedInteraction
              (context.framework.groundData.finiteSites volume)) time observable) =
          (dynamics.unitaryAt time : QuantumGroundSector.Operator
            (context.framework.groundData.finiteSector volume).StateSpace) *
          context.framework.groundData.restriction volume observable *
          star (dynamics.unitaryAt time : QuantumGroundSector.Operator
            (context.framework.groundData.finiteSector volume).StateSpace) := by
  have ground := context.bosonic_clustering_atom_retains_actual_ground_sector clustering
  refine ⟨(context.framework.groundData.finiteSector volume).hamiltonianDynamics
    (ground.2.2.1 volume admissible).1, rfl, ?_⟩
  exact context.framework.groundData.ground_bands_realize_finite_hamiltonian_dynamics
    context.framework.selectedInteraction ground.2.2.1 ground.2.1 volume admissible

theorem fermionic_decay_atom_retains_distinct_state_bounds
    (context : SemanticContext) (decay : context.interpretAtom .fermionicDecay) :
    context.framework.fermionicCorrectedCorrelationBoundCalculated
        context.framework.selectedGroundState context.framework.selectedGroundProjection
        context.framework.sourceObservable context.framework.targetObservable
        context.framework.sourceRegion context.framework.targetRegion context.framework.selectedGap
        context.framework.selectedPropagationBound context.framework.selectedCorrelationBound ∧
      context.framework.FermionicGroundAverageCorrectedBoundAt
        context.framework.sourceObservable context.framework.targetObservable
        context.framework.sourceRegion context.framework.targetRegion context.framework.selectedCorrelationBound ∧
      context.framework.groundData.averageLimit.NormalizedPositiveAt ∧
      context.framework.fermionicUnsubtractedCorrelationDecays
        context.framework.selectedGroundAverageState context.framework.sourceObservable context.framework.targetObservable
        context.framework.sourceRegion context.framework.targetRegion context.framework.selectedCorrelationBound := by
  rcases decay with ⟨setup, _correction, vectorBound, averageBound, identity, raw⟩
  have ground := context.framework.uniform_gap_setup_retains_actual_ground_sector setup.2.1.1.1
  exact ⟨vectorBound, averageBound,
    context.framework.groundData.average_limit_is_normalized_positive ground.1.1 ground.1.2.1
      ground.2.2.1 identity.2.1, raw⟩

end SemanticContext

end PhysicsLogic.Papers.HastingsKoma2006