import Lean.Elab.Command
import Lean.Util.CollectAxioms
import PhysicsLogicConsumer.StatMech
import PhysicsLogicConsumer.ClassicalDynamics
import PhysicsLogicConsumer.BellLocality
import PhysicsLogicConsumer.CosmicVariance
import PhysicsLogicConsumer.CosmologicalPosterior
import PhysicsLogicConsumer.GeodesicFocusing
import PhysicsLogicConsumer.CriticalCollapse
import PhysicsLogicConsumer.NuclearScattering
import PhysicsLogicConsumer.RadioactiveDecay
import PhysicsLogicConsumer.CondensedMatter
import PhysicsLogicConsumer.AMOSpectroscopy
import PhysicsLogicConsumer.QuantumInformation
import PhysicsLogicConsumer.PlasmaPhysics
import PhysicsLogicConsumer.BrownianMotion
import PhysicsLogicConsumer.Langevin1908
import PhysicsLogicConsumer.MomentIdentification
import PhysicsLogicConsumer.FluidCorrelations
import PhysicsLogicConsumer.ImpermeableLayer
import PhysicsLogicConsumer.ThermalNoise
import PhysicsLogicConsumer.ThermalProbeCompleteness
import PhysicsLogicConsumer.PeriodicSampling
import PhysicsLogicConsumer.RejectedMoves
import PhysicsLogicConsumer.Supersymmetry
import PhysicsLogicConsumer.CoarseGraining
import PhysicsLogicConsumer.ControlledApproximation
import PhysicsLogicConsumer.StellarHydrostatics
import PhysicsLogicConsumer.MeasurementRecords
import PhysicsLogicConsumer.Fluctuations
import PhysicsLogicConsumer.NebularCalibration
import PhysicsLogicConsumer.LocalInvariance
import PhysicsLogicConsumer.FrequencyReference
import PhysicsLogicConsumer.WorkSamplingTail
import PhysicsLogicConsumer.StatePositivity
import PhysicsLogicConsumer.UnitaryInfluence
import PhysicsLogicConsumer.CoordinateCurrents
import PhysicsLogicConsumer.LightConePropagation

open Lean Elab Command

private def forbiddenPhysicsDependency (name : Name) : Bool :=
  let parts := name.toString.splitOn "."
  parts.contains "PhysicsLogic" &&
    (parts.contains "Papers" || parts.contains "deprecated" || parts.contains "FourPhaseControl" ||
      parts.any (fun part => part.endsWith "Countermodels" || part.endsWith "Controls"))

namespace PhysicsLogicConsumer.DependencyAudit

abbrev ParentIndex := Std.HashMap Name (List Name)

/-- Match the pinned Lean/Util/CollectAxioms.lean (Leonardo de Moura, Microsoft,
Apache-2.0), including opaque values and inductive constructors.
ConstantInfo.getUsedConstantsAsSet has different recursor and quotient semantics. -/
def directDependencies (environment : Environment) (name : Name) : Array Name :=
  match environment.checked.get.find? name with
  | some (.axiomInfo value) => value.type.getUsedConstants
  | some (.defnInfo value) => value.type.getUsedConstants ++ value.value.getUsedConstants
  | some (.thmInfo value) => value.type.getUsedConstants ++ value.value.getUsedConstants
  | some (.opaqueInfo value) => value.type.getUsedConstants ++ value.value.getUsedConstants
  | some (.quotInfo _) => #[]
  | some (.ctorInfo value) => value.type.getUsedConstants
  | some (.recInfo value) => value.type.getUsedConstants
  | some (.inductInfo value) => value.type.getUsedConstants ++ value.ctors.toArray
  | none => #[]

def buildParentIndex (environment : Environment) (visited : NameSet) :
    Except String ParentIndex := Id.run do
  let mut parents : ParentIndex := {}
  for parent in visited.toList do
    for dependency in directDependencies environment parent do
      unless visited.contains dependency do
        return .error s!"Dependency index omitted {dependency}, used by {parent}"
      parents := parents.insert dependency (parent :: parents.getD dependency [])
  return .ok parents

/-- Reverse reachability is per target; no consumer inherits another consumer's uses. -/
def ancestors (parents : ParentIndex) (target : Name) : NameSet := Id.run do
  let mut visited : NameSet := {}
  let mut pending : Array Name := #[target]
  while !pending.isEmpty do
    let current := pending.back!
    pending := pending.pop
    unless visited.contains current do
      visited := visited.insert current
      for parent in parents.getD current [] do
        pending := pending.push parent
  return visited

def groupRequirements (requirements : Array (Name × Name)) :
    Except String (Std.HashMap Name (Array Name)) := Id.run do
  if requirements.isEmpty then return .error "External consumer has no required public API uses"
  let mut seen : Std.HashSet (Name × Name) := {}
  let mut groups : Std.HashMap Name (Array Name) := {}
  for (declaration, required) in requirements do
    if seen.contains (declaration, required) then
      return .error s!"Duplicate public API use: {declaration}, {required}"
    seen := seen.insert (declaration, required)
    groups := groups.insert required ((groups.getD required #[]).push declaration)
  return .ok groups

namespace Examples

def leftApi : Nat := 37
def rightApi : Nat := 41
def leftHelper : Nat := leftApi
def leftClient : Nat := leftHelper
def rightClient : Nat := rightApi
abbrev TypeApi := Nat
def typeClient : TypeApi := Nat.zero
opaque opaqueClient : Nat := leftHelper
theorem theoremClient : leftClient = 37 := rfl

inductive Tree where
  | leaf
  | branch : Tree -> Tree -> Tree

def treeClient : Tree := .branch .leaf .leaf

def treeSize : Tree -> Nat
  | .leaf => 1
  | .branch first second => treeSize first + treeSize second

end Examples

private def checkDependencyIndexExamples : CommandElabM Unit := do
  let environment ← getEnv
  let roots := #[``Examples.leftClient, ``Examples.rightClient, ``Examples.typeClient,
    ``Examples.opaqueClient, ``Examples.theoremClient, ``Examples.Tree,
    ``Examples.Tree.branch, ``Examples.Tree.rec, ``Examples.treeClient,
    ``Examples.treeSize, ``Quot, ``Quot.lift, ``Quot.ind, ``propext,
    ``Classical.choice, ``Quot.sound, `MissingDependencyExample]
  let targets := #[``Examples.leftApi, ``Examples.rightApi, ``Examples.leftHelper,
    ``Examples.TypeApi, ``Examples.Tree, ``Examples.Tree.branch, ``Examples.Tree.rec,
    ``Nat, ``Quot, ``Iff, ``propext, ``Classical.choice, ``Quot.sound,
    `MissingDependencyExample, `EntirelyUnreachable]
  let mut traversal : Lean.CollectAxioms.State := {}
  for root in roots do
    let (_, updated) := ((Lean.CollectAxioms.collect root).run environment).run traversal
    traversal := updated
  let parents ← match buildParentIndex environment traversal.visited with
    | .ok result => pure result
    | .error message => throwError message
  for root in roots do
    let (_, reference) := ((Lean.CollectAxioms.collect root).run environment).run {}
    for target in targets do
      unless (ancestors parents target).contains root == reference.visited.contains target do
        throwError "Dependency index disagrees with kernel collector: {root}, {target}"
  unless (ancestors parents ``Examples.leftApi).contains ``Examples.leftClient do
    throwError "Dependency index lost a transitive value dependency"
  if (ancestors parents ``Examples.leftApi).contains ``Examples.rightClient then
    throwError "Dependency index leaked one consumer's API use to another"
  let some typeInfo := environment.checked.get.find? ``Examples.typeClient
    | throwError "Missing type-only regression declaration"
  unless typeInfo.type.getUsedConstants.contains ``Examples.TypeApi do
    throwError "Type-only regression does not retain its named type"
  if (typeInfo.value?.getD (.sort .zero)).getUsedConstants.contains ``Examples.TypeApi then
    throwError "Type-only regression unexpectedly also mentions its API in the value"
  let missingEdgeDomain : NameSet := ({} : NameSet).insert ``Examples.leftClient
  match buildParentIndex environment missingEdgeDomain with
  | .error _ => pure ()
  | .ok _ => throwError "Dependency index accepted an unclosed traversal"
  let cycle : ParentIndex :=
    ({} : ParentIndex).insert `a [`b] |>.insert `b [`a, `c] |>.insert `d [`e]
  let reached := ancestors cycle `a
  unless reached.size == 3 && reached.contains `a && reached.contains `b &&
      reached.contains `c && !reached.contains `d && !reached.contains `e do
    throwError "Dependency index mishandled a cycle or disconnected component"
  match groupRequirements #[] with
  | .error _ => pure ()
  | .ok _ => throwError "Dependency audit accepted an empty public-use registry"
  match groupRequirements #[(`left, `api), (`left, `api)] with
  | .error _ => pure ()
  | .ok _ => throwError "Dependency audit accepted duplicate public-use evidence"
  match groupRequirements #[(`left, `api), (`right, `api)] with
  | .error message => throwError message
  | .ok groups =>
      unless groups.size == 1 && groups.getD `api #[] == #[`left, `right] do
        throwError "Dependency audit lost consumers sharing an API target"
  logInfo m!"Dependency-index differential examples passed: {roots.size * targets.size} comparisons."

elab "check_dependency_index_examples" : command => checkDependencyIndexExamples

check_dependency_index_examples

end PhysicsLogicConsumer.DependencyAudit

private def consumerUseOwnershipError (environment : Environment)
    (declaration required : Name) : Option String := Id.run do
  unless (environment.checked.get.find? declaration).isSome do
    return some s!"Missing checked consumer declaration {declaration}"
  unless (environment.checked.get.find? required).isSome do
    return some s!"Missing checked public API {required}"
  let some clientIndex := environment.getModuleIdxFor? declaration
    | return some s!"Consumer declaration has no imported owner: {declaration}"
  let clientModule := environment.allImportedModuleNames[clientIndex.toNat]!
  unless `PhysicsLogicConsumer |>.isPrefixOf clientModule do
    return some s!"Registered consumer belongs to a nonconsumer module: {declaration}"
  let some apiIndex := environment.getModuleIdxFor? required
    | return some s!"Public API has no imported owner: {required}"
  let apiModule := environment.allImportedModuleNames[apiIndex.toNat]!
  let publicScope := fun name : Name =>
    [`PhysicsLogic.Framework, `PhysicsLogic.Philosophy, `PhysicsLogic.Paradigm].any
      (fun scopeRoot => scopeRoot.isPrefixOf name)
  unless publicScope apiModule && publicScope required && !forbiddenPhysicsDependency required do
    return some s!"Registered API is not an ordinary public physics declaration: {required}"
  return none

private def requiredPublicUses : Array (Name × Name) := #[
  (``PhysicsLogicConsumer.RejectedMoves.actual_attempts_preserve_the_canonical_law,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.detailed_balance_realizes_nonvacuous_stationary_update),
  (``PhysicsLogicConsumer.RejectedMoves.the_retained_chain_is_stochastic_and_balanced,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.detailed_balance_realizes_nonvacuous_stationary_update),
  (``PhysicsLogicConsumer.RejectedMoves.deleting_rejections_changes_the_limit_even_when_both_chains_converge,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.positive_refresh_probability_gives_actual_distribution_convergence),
  (``PhysicsLogicConsumer.PeriodicSampling.UniformControl.law_comparison_iff_normalized_statewise_error,
    ``PhysicsLogic.Paradigm.ScaleAndRegime.controlled_approximation_iff_explicit_prediction_matches),
  (``PhysicsLogicConsumer.PeriodicSampling.UniformControl.the_library_certifies_eventual_control_on_every_gapped_band,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.every_iterate_is_a_normalized_probability_law),
  (``PhysicsLogicConsumer.PeriodicSampling.actual_balance_and_stationarity_hold_throughout_the_probability_interval,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.detailed_balance_realizes_nonvacuous_stationary_update),
  (``PhysicsLogicConsumer.PeriodicSampling.every_prepared_iterate_is_a_probability_distribution,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.every_iterate_is_a_normalized_probability_law),
  (``PhysicsLogicConsumer.PeriodicSampling.positive_switching_and_holding_restore_relaxation,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.an_absolutely_contracting_mode_has_zero_asymptotic_mean),
  (``PhysicsLogicConsumer.PeriodicSampling.a_negative_relaxation_mode_still_converges,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.a_calculated_mode_has_the_actual_iterated_mean),
  (``PhysicsLogicConsumer.ThermalNoise.CanonicalPreparation.the_independent_ensemble_has_actual_controlled_preparation_predictions,
    ``PhysicsLogic.Framework.FiniteCanonicalData.every_positive_tolerance_has_a_model_dependent_preparation_window),
  (``PhysicsLogicConsumer.ThermalNoise.CanonicalPreparation.the_independent_ensemble_has_actual_controlled_preparation_predictions,
    ``PhysicsLogic.Framework.FiniteCanonicalData.a_preparation_window_controls_actual_predictions),
  (``PhysicsLogicConsumer.ThermalNoise.CanonicalPreparation.tripling_the_coupling_transports_the_error_regime,
    ``PhysicsLogic.Framework.FiniteCanonicalData.a_coupling_rescaling_changes_both_the_window_and_error_per_field),
  (``PhysicsLogicConsumer.ThermalNoise.CanonicalPreparation.the_same_finite_bias_occurs_at_one_third_the_field,
    ``PhysicsLogic.Framework.FiniteCanonicalData.rescaling_the_coupling_rescales_the_actual_field),
  (``PhysicsLogicConsumer.ThermalNoise.CanonicalPreparation.the_library_derives_distinct_linear_responses_for_the_same_ensemble,
    ``PhysicsLogic.Framework.FiniteCanonicalData.normalized_canonical_preparation_realizes_the_field_response),
  (``PhysicsLogicConsumer.ThermalNoise.CanonicalPreparation.the_library_derives_distinct_linear_responses_for_the_same_ensemble,
    ``PhysicsLogic.Framework.FiniteCanonicalData.centered_orthogonality_removes_only_the_linear_preparation_response),
  (``PhysicsLogicConsumer.ThermalNoise.CanonicalPreparation.the_library_derives_distinct_linear_responses_for_the_same_ensemble,
    ``PhysicsLogic.Framework.FiniteCanonicalData.adding_a_constant_to_the_measured_observable_preserves_response),
  (``PhysicsLogicConsumer.ThermalNoise.CanonicalPreparation.the_library_derives_distinct_linear_responses_for_the_same_ensemble,
    ``PhysicsLogic.Framework.FiniteCanonicalData.zero_field_response_is_the_original_connected_correlation),
  (``PhysicsLogicConsumer.ThermalNoise.CanonicalPreparation.the_same_positive_preparation_has_a_nonlinear_residual_response,
    ``PhysicsLogic.Framework.FiniteCanonicalData.every_field_has_actual_normalized_positive_populations),
  (``PhysicsLogicConsumer.NuclearScattering.CrossSectionRecords.every_observed_momentum_has_actual_elastic_scattering,
    ``PhysicsLogic.Framework.ElasticSWave.real_effective_range_function_realizes_elastic_scattering),
  (``PhysicsLogicConsumer.NuclearScattering.CrossSectionRecords.the_complex_amplitude_supplies_a_calibrated_signed_readout,
    ``PhysicsLogic.Framework.ElasticSWave.inverse_amplitude_recovers_real_effective_range_function),
  (``PhysicsLogicConsumer.NuclearScattering.CrossSectionRecords.the_library_rejects_signed_length_determination_even_from_the_whole_curve,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.ambiguous_record_does_not_determine_a_value),
  (``PhysicsLogicConsumer.NuclearScattering.CrossSectionRecords.the_library_retains_magnitude_information_despite_the_sign_ambiguity,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.record_constraint_mono),
  (``PhysicsLogicConsumer.NuclearScattering.CrossSectionRecords.the_library_determines_the_signed_parameter_with_complex_amplitude_access,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.calibrated_decoder_determines_record_value),
  (``PhysicsLogicConsumer.NuclearScattering.CrossSectionRecords.the_library_preserves_the_magnitude_constraint_under_refined_access,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.finer_records_preserve_value_constraints),
  (``PhysicsLogicConsumer.NuclearScattering.CrossSectionRecords.rate_only_access_does_not_refine_amplitude_access,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.finer_records_preserve_determined_values),
  (``PhysicsLogicConsumer.CondensedMatter.DensityVariational.the_density_minimum_has_an_explicit_fixed_number_readback,
    ``PhysicsLogic.Framework.GroundDensityModel.nonvacuous_ground_density_iff_primitive_specification),
  (``PhysicsLogicConsumer.CondensedMatter.DensityVariational.candidate_functional_completeness_iff_zero_penalty,
    ``PhysicsLogic.Framework.GroundDensityModel.density_completeness_iff_domain_coverage_and_energy_agreement),
  (``PhysicsLogicConsumer.CondensedMatter.DensityVariational.self_completeness_holds_for_every_functional_penalty,
    ``PhysicsLogic.Framework.GroundDensityModel.self_density_completeness_iff_inhabited_selected_domain),
  (``PhysicsLogicConsumer.CondensedMatter.DensityVariational.the_selected_route_rejects_a_nonzero_functional_penalty,
    ``PhysicsLogic.Framework.DensityFunctionalContext.established_variational_principle_exposes_selected_semantics),
  (``PhysicsLogicConsumer.ClassicalDynamics.ForecastFromIntervals.unique_evolution_can_exclude_every_uniform_half_unit_forecast,
    ``PhysicsLogic.Framework.UniformPointForecast.separated_compatible_outcomes_exclude_uniform_forecasting),
  (``PhysicsLogicConsumer.ClassicalDynamics.ForecastFromIntervals.unique_evolution_can_exclude_every_uniform_half_unit_forecast,
    ``PhysicsLogic.Paradigm.Dynamics.FiniteInformation.incompatible_possible_outcomes_exclude_uniform_forecasting),
  (``PhysicsLogicConsumer.ClassicalDynamics.ForecastFromIntervals.empty_information_does_not_count_as_a_successful_forecast,
    ``PhysicsLogic.Paradigm.Dynamics.FiniteInformation.no_compatible_evolution_excludes_a_uniform_forecast),
  (``PhysicsLogicConsumer.ClassicalDynamics.ForecastFromIntervals.exact_initial_information_allows_an_exact_forecast,
    ``PhysicsLogic.Paradigm.Dynamics.FiniteInformation.exact_initial_information_and_unique_evolution_admit_an_exact_forecast),
  (``PhysicsLogicConsumer.ClassicalDynamics.ObservedHistoryReuse.the_framework_derives_paradigm_determinism_of_full_phase_data,
    ``PhysicsLogic.Framework.InitialEnsemblePrediction.measurable_closure_has_paradigm_observed_forward_uniqueness),
  (``PhysicsLogicConsumer.ClassicalDynamics.ObservedHistoryReuse.the_library_supplies_an_actual_unique_phase_successor,
    ``PhysicsLogic.Paradigm.Dynamics.ObservedHistory.determined_future_iff_observed_forward_uniqueness),
  (``PhysicsLogicConsumer.ClassicalDynamics.ObservedHistoryReuse.the_library_supplies_an_actual_unique_phase_successor,
    ``PhysicsLogic.Paradigm.Dynamics.ObservedHistory.determination_and_an_admitted_history_give_unique_observed_evolution),
  (``PhysicsLogicConsumer.ClassicalDynamics.ObservedHistoryReuse.the_library_detects_position_branching_without_phase_branching,
    ``PhysicsLogic.Paradigm.Dynamics.ObservedHistory.equal_present_and_distinct_futures_give_observed_branching),
  (``PhysicsLogicConsumer.ClassicalDynamics.ObservedHistoryReuse.the_library_preserves_closure_under_a_genuine_sector_restriction,
    ``PhysicsLogic.Paradigm.Dynamics.ObservedHistory.determination_restricts_to_admitted_histories),
  (``PhysicsLogicConsumer.ClassicalDynamics.ObservedHistoryReuse.the_library_rejects_existence_for_an_unrealized_selected_velocity,
    ``PhysicsLogic.Paradigm.Dynamics.ObservedHistory.no_admitted_present_history_excludes_observed_evolution),
  (``PhysicsLogicConsumer.CoordinateCurrents.library_derives_local_transport_balance,
    ``PhysicsLogic.Framework.CoordinateCurrent.nonvacuous_balance_of_vanishing_source),
  (``PhysicsLogicConsumer.CoordinateCurrents.library_restricts_the_same_transport_to_future,
    ``PhysicsLogic.Framework.CoordinateCurrent.nonvacuous_balance_restricts_to_inhabited_domain),
  (``PhysicsLogicConsumer.CoordinateCurrents.library_separates_uniform_production_from_conservation,
    ``PhysicsLogic.Framework.CoordinateCurrent.nonzero_source_excludes_local_balance),
  (``PhysicsLogicConsumer.CoordinateCurrents.library_subtracts_the_background_current,
    ``PhysicsLogic.Framework.CoordinateCurrent.regular_sub),
  (``PhysicsLogicConsumer.CoordinateCurrents.library_subtracts_the_background_current,
    ``PhysicsLogic.Framework.CoordinateCurrent.divergence_sub),
  (``PhysicsLogicConsumer.CoordinateCurrents.library_derives_pulse_balance,
    ``PhysicsLogic.Framework.CoordinateCurrent.nonvacuous_balance_of_local_balance),
  (``PhysicsLogicConsumer.ControlledApproximation.ArgumentScopeReuse.the_library_rejects_both_uniform_acceleration_claims,
    ``PhysicsLogic.Paradigm.ScaleAndRegime.ScopedArgumentContext.inconclusive_constraints_entail_neither_alternative),
  (``PhysicsLogicConsumer.NuclearScattering.ReadoutComparison.complex_amplitude_equivalence_preserves_the_effective_range_function,
    ``PhysicsLogic.Philosophy.Representation.empirical_equivalence_iff_readout_equivalence_of_separating_predictions),
  (``PhysicsLogicConsumer.NuclearScattering.ReadoutComparison.all_three_readouts_have_the_same_active_momentum_sector,
    ``PhysicsLogic.Philosophy.Representation.active_prediction_sector_iff_value_readout),
  (``PhysicsLogicConsumer.NuclearScattering.ReadoutComparison.a_nonnegative_branch_makes_cross_section_agreement_reflective,
    ``PhysicsLogic.Philosophy.Representation.empirical_equivalence_iff_readout_equivalence_of_separating_predictions),
  (``PhysicsLogicConsumer.NuclearScattering.ReadoutComparison.elastic_cross_section_equivalence_does_not_determine_complex_amplitudes,
    ``PhysicsLogic.Framework.ElasticSWave.real_effective_range_function_realizes_elastic_scattering),
  (``PhysicsLogicConsumer.ControlledApproximation.ArgumentScopeReuse.the_library_requires_distinct_retained_force_realizations,
    ``PhysicsLogic.Paradigm.ScaleAndRegime.ScopedArgumentContext.inconclusive_constraints_have_distinct_realizations),
  (``PhysicsLogicConsumer.ControlledApproximation.ArgumentScopeReuse.the_library_exhibits_an_out_of_scope_force_case,
    ``PhysicsLogic.Paradigm.ScaleAndRegime.ScopedArgumentContext.inconclusive_constraints_exhibit_a_case_outside_sound_scope),
  (``PhysicsLogicConsumer.ControlledApproximation.ArgumentScopeReuse.the_library_infers_positive_acceleration_after_calibration,
    ``PhysicsLogic.Paradigm.ScaleAndRegime.ScopedArgumentContext.sound_argument_establishes_its_conclusion),
  (``PhysicsLogicConsumer.StatMech.SamplingParadigmReuse.the_library_supplies_unique_evolution_of_actual_probability_laws,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.stochastic_evolution_is_total_deterministic_on_normalized_laws),
  (``PhysicsLogicConsumer.StatMech.SamplingParadigmReuse.the_library_supplies_actual_retained_successors,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.stochastic_rows_supply_actual_retained_successors),
  (``PhysicsLogicConsumer.StatMech.SamplingParadigmReuse.the_populated_row_separates_ensemble_and_retained_state_dynamics,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.actual_positive_branching_separates_distribution_and_state_evolution),
  (``PhysicsLogicConsumer.StatMech.SamplingParadigmReuse.the_stationary_probability_state_has_an_actual_unique_successor,
    ``PhysicsLogic.Paradigm.Dynamics.total_deterministic_evolution_is_unique_everywhere),
  (``PhysicsLogicConsumer.StatMech.SamplingParadigmReuse.the_library_preserves_the_meaning_of_retained_state_determinism,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.probabilistic_and_paradigm_determinism_agree_on_finite_stochastic_updates),
  (``PhysicsLogicConsumer.StatMech.SamplingParadigmReuse.unique_probability_evolution_does_not_select_an_individual_successor,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.unique_distribution_evolution_does_not_remove_actual_retained_branching),
  (``PhysicsLogicConsumer.StatMech.SamplingParadigmReuse.the_library_constructs_a_deterministic_larger_state_with_the_actual_joint_law,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.an_actual_stationary_joint_law_has_a_deterministic_one_step_realization),
  (``PhysicsLogicConsumer.StatMech.SamplingParadigmReuse.a_deterministic_one_step_realization_does_not_reproduce_the_next_markov_step,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.matching_one_step_statistics_does_not_supply_the_second_step_law),
  (``PhysicsLogicConsumer.StatMech.SamplingParadigmReuse.the_identity_retains_paradigm_forward_uniqueness,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.deterministic_point_mass_updates_have_paradigm_forward_uniqueness),
  (``PhysicsLogicConsumer.StatMech.SamplingJointReuse.the_faster_update_preserves_the_same_target,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.refresh_preserves_a_normalized_target),
  (``PhysicsLogicConsumer.StatMech.SamplingJointReuse.the_two_actual_joint_laws_have_the_same_marginals,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.a_stationary_update_has_the_actual_joint_law),
  (``PhysicsLogicConsumer.StatMech.SamplingJointReuse.the_library_computes_both_actual_adjacent_correlations,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.a_calculated_mode_determines_the_actual_lagged_product),
  (``PhysicsLogicConsumer.StatMech.SamplingJointReuse.the_actual_joint_laws_differ_despite_identical_equilibrium_marginals,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.different_lagged_products_require_different_actual_joint_laws),
  (``PhysicsLogicConsumer.StatMech.SamplingJointReuse.the_stochastic_update_is_not_a_function_of_the_retained_state,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.a_branching_row_excludes_deterministic_retained_state_evolution),
  (``PhysicsLogicConsumer.StatMech.SamplingJointReuse.the_identity_has_the_same_equilibrium_marginals_and_is_deterministic,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.a_stationary_update_has_the_actual_joint_law),
  (``PhysicsLogicConsumer.StatMech.RepeatedSampling.the_library_accepts_the_actual_refresh_update,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.refresh_preserves_a_normalized_target),
  (``PhysicsLogicConsumer.StatMech.RepeatedSampling.every_actual_run_is_a_probability_law,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.every_iterate_is_a_normalized_probability_law),
  (``PhysicsLogicConsumer.StatMech.RepeatedSampling.the_library_computes_every_finite_state_weight,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.every_refresh_iterate_has_the_actual_relaxation_factor),
  (``PhysicsLogicConsumer.StatMech.RepeatedSampling.the_library_derives_the_actual_distribution_limit,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.positive_refresh_probability_gives_actual_distribution_convergence),
  (``PhysicsLogicConsumer.StatMech.RepeatedSampling.the_library_transports_the_actual_observable_bias,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.a_calculated_mode_has_the_actual_iterated_mean),
  (``PhysicsLogicConsumer.StatMech.RepeatedSampling.the_library_composes_the_actual_update_order,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.composed_kernel_evolves_in_the_actual_update_order),
  (``PhysicsLogicConsumer.StatMech.RepeatedSampling.the_library_retains_the_common_target_under_an_ordered_sweep,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.composition_preserves_stochastic_rows),
  (``PhysicsLogicConsumer.StatMech.RepeatedSampling.the_library_retains_the_common_target_under_an_ordered_sweep,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.composition_preserves_a_common_stationary_law),
  (``PhysicsLogicConsumer.StatMech.RepeatedSampling.detailed_balance_reverses_the_schedule,
    ``PhysicsLogic.Framework.FiniteTransitionKernel.local_detailed_balance_pairs_opposite_update_orders),
  (``PhysicsLogicConsumer.AMOSpectroscopy.FrameTransport.the_library_reconstructs_the_actual_laboratory_generator,
    ``PhysicsLogic.Framework.CoherentTwoState.LinearPhaseFrame.transformed_generator_entry),
  (``PhysicsLogicConsumer.AMOSpectroscopy.FrameTransport.the_library_supplies_nonvacuous_frame_dynamics,
    ``PhysicsLogic.Framework.CoherentTwoState.LinearPhaseFrame.physical_pulse_from_entrance_has_nonvacuous_frame_dynamics),
  (``PhysicsLogicConsumer.AMOSpectroscopy.FrameTransport.the_library_solves_the_actual_laboratory_equation,
    ``PhysicsLogic.Framework.CoherentTwoState.LinearPhaseFrame.actual_phase_transformation_transports_schrodinger_dynamics),
  (``PhysicsLogicConsumer.AMOSpectroscopy.FrameTransport.the_library_retains_the_specified_entrance_state,
    ``PhysicsLogic.Framework.CoherentTwoState.LinearPhaseFrame.physical_pulse_attains_the_actual_entrance_state),
  (``PhysicsLogicConsumer.AMOSpectroscopy.FrameTransport.the_library_preserves_the_energy_basis_probabilities,
    ``PhysicsLogic.Framework.CoherentTwoState.LinearPhaseFrame.phase_transformation_preserves_each_energy_basis_probability),
  (``PhysicsLogicConsumer.AMOSpectroscopy.FrameTransport.the_laboratory_pulse_is_normalized,
    ``PhysicsLogic.Framework.CoherentTwoState.LinearPhaseFrame.phase_transformation_preserves_state_normalization),
  (``PhysicsLogicConsumer.AMOSpectroscopy.FrameTransport.the_detuned_laboratory_probability_keeps_the_actual_coupling,
    ``PhysicsLogic.Framework.CoherentTwoState.LinearPhaseFrame.component_phase_has_unit_norm),
  (``PhysicsLogicConsumer.MeasurementRecords.RateSeparation.the_library_refutes_every_compatible_reflection_symmetric_model,
    ``PhysicsLogic.Framework.RateRecordInference.a_separated_record_distinguishes_the_bound_physical_rates),
  (``PhysicsLogicConsumer.MeasurementRecords.RateSeparation.both_compatible_coefficients_break_reflection_symmetry,
    ``PhysicsLogic.Framework.RateRecordInference.a_separated_record_distinguishes_the_bound_physical_rates),
  (``PhysicsLogicConsumer.MeasurementRecords.RateSeparation.excluding_symmetry_does_not_identify_the_exact_odd_coefficient,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.ambiguous_record_does_not_determine_a_value),
  (``PhysicsLogicConsumer.MeasurementRecords.RateSeparation.the_public_api_certifies_the_separated_record,
    ``PhysicsLogic.Framework.RateRecordInference.a_separated_inhabited_record_excludes_equal_mean_rates),
  (``PhysicsLogicConsumer.MeasurementRecords.RateSeparation.the_library_bounds_the_physical_contrast_without_exact_calibration,
    ``PhysicsLogic.Framework.RateRecordInference.a_compatible_record_bounds_the_actual_mean_contrast),
  (``PhysicsLogicConsumer.MeasurementRecords.RateSeparation.the_public_api_rejects_angular_invariance,
    ``PhysicsLogic.Framework.RateRecordInference.a_separated_record_refutes_the_selected_observable_invariance),
  (``PhysicsLogicConsumer.MeasurementRecords.RateSeparation.the_record_and_the_physical_prediction_refute_law_invariance,
    ``PhysicsLogic.Framework.RateRecordInference.a_separated_record_refutes_the_selected_observable_invariance),
  (``PhysicsLogicConsumer.MeasurementRecords.RateSeparation.the_record_and_the_physical_prediction_refute_law_invariance,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.record_constraint_holds_on_compatible_configuration),
  (``PhysicsLogicConsumer.CosmologicalPosterior.SelectionReuse.the_public_api_realizes_both_selections,
    ``PhysicsLogic.Framework.StandardCandleSelection.admissible_detection_weights_realize_standardized_selection),
  (``PhysicsLogicConsumer.CosmologicalPosterior.SelectionReuse.the_library_computes_the_surviving_relative_shift,
    ``PhysicsLogic.Framework.StandardCandleSelection.two_realized_populations_retain_the_residual_contrast),
  (``PhysicsLogicConsumer.CosmologicalPosterior.SelectionReuse.two_bright_tails_do_not_certify_cancellation,
    ``PhysicsLogic.Framework.StandardCandleSelection.two_realized_populations_retain_the_residual_contrast),
  (``PhysicsLogicConsumer.CosmologicalPosterior.SelectionReuse.no_selection_shift_is_not_exact_absolute_calibration,
    ``PhysicsLogic.Framework.StandardCandleSelection.constant_residuals_have_no_selection_shift),
  (``PhysicsLogicConsumer.CosmologicalPosterior.SelectionReuse.no_selection_shift_is_not_exact_absolute_calibration,
    ``PhysicsLogic.Framework.StandardCandleSelection.a_positive_weighted_mean_preserves_an_additive_offset),
  (``PhysicsLogicConsumer.CosmologicalPosterior.SelectionReuse.no_selection_shift_is_not_exact_absolute_calibration,
    ``PhysicsLogic.Framework.StandardCandleSelection.standardization_removes_the_shape_term_but_retains_residual_scatter),
  (``PhysicsLogicConsumer.CosmologicalPosterior.the_library_identifies_physical_and_hubble_free_predictions,
    ``PhysicsLogic.Framework.StandardCandleCalibration.Calibration.hubble_free_prediction_is_the_same_apparent_magnitude),
  (``PhysicsLogicConsumer.CosmologicalPosterior.the_library_retains_relative_predictions_but_changes_hubble_scale,
    ``PhysicsLogic.Framework.StandardCandleCalibration.Calibration.positive_rescaling_preserves_hubble_free_distance),
  (``PhysicsLogicConsumer.CosmologicalPosterior.the_library_retains_relative_predictions_but_changes_hubble_scale,
    ``PhysicsLogic.Framework.StandardCandleCalibration.Calibration.positive_rescaling_preserves_the_fitted_intercept),
  (``PhysicsLogicConsumer.CosmologicalPosterior.the_library_retains_relative_predictions_but_changes_hubble_scale,
    ``PhysicsLogic.Framework.StandardCandleCalibration.Calibration.positive_rescaling_preserves_every_apparent_magnitude),
  (``PhysicsLogicConsumer.CosmologicalPosterior.the_library_breaks_the_freedom_when_absolute_calibration_is_fixed,
    ``PhysicsLogic.Framework.StandardCandleCalibration.Calibration.fixed_absolute_calibration_and_same_predictions_identify_the_hubble_scale),
  (``PhysicsLogicConsumer.CosmologicalPosterior.the_library_reconstructs_a_normalization_without_assuming_its_hubble_scale,
    ``PhysicsLogic.Framework.StandardCandleCalibration.Calibration.reconstruction_retains_the_fitted_apparent_magnitude),
  (``PhysicsLogicConsumer.CosmologicalPosterior.the_library_preserves_the_cosmological_law_under_nuisance_pushforward,
    ``PhysicsLogic.Framework.StandardCandlePosterior.NuisanceMarginalization.nuisance_only_pushforward_preserves_cosmological_marginal),
  (``PhysicsLogicConsumer.CriticalCollapse.the_library_derives_the_clients_actual_mass_limit,
    ``PhysicsLogic.Framework.CriticalThresholdMassCurve.controlled_relative_fit_forces_zero_threshold_mass),
  (``PhysicsLogicConsumer.CriticalCollapse.the_library_excludes_a_positive_mass_floor,
    ``PhysicsLogic.Framework.CriticalThresholdMassCurve.vanishing_mass_excludes_a_positive_mass_floor),
  (``PhysicsLogicConsumer.CriticalCollapse.the_library_certifies_the_nonvacuous_mass_family,
    ``PhysicsLogic.Framework.CriticalCollapseMassFamily.controlled_scaling_and_realization_give_nonvacuous_threshold_masses),
  (``PhysicsLogicConsumer.CriticalCollapse.the_library_supplies_arbitrarily_small_positive_horizon_masses,
    ``PhysicsLogic.Framework.CriticalCollapseMassFamily.physical_family_and_mass_limit_give_arbitrarily_small_black_holes),
  (``PhysicsLogicConsumer.CriticalCollapse.the_library_rejects_the_fixed_tolerance_zero_mass_inference,
    ``PhysicsLogic.Framework.CriticalThresholdMassCurve.positive_power_profile_tends_to_zero),
  (``PhysicsLogicConsumer.CosmologicalPosterior.the_library_normalizes_the_actual_joint_posterior,
    ``PhysicsLogic.Framework.StandardCandlePosterior.LikelihoodModel.the_posterior_has_total_mass_one_only_after_resolving_normalization),
  (``PhysicsLogicConsumer.CosmologicalPosterior.the_library_preserves_physical_support_under_likelihood_reweighting,
    ``PhysicsLogic.Framework.StandardCandlePosterior.LikelihoodModel.posterior_reweighting_preserves_prior_null_sets),
  (``PhysicsLogicConsumer.CosmologicalPosterior.the_library_normalizes_the_nuisance_marginal,
    ``PhysicsLogic.Framework.StandardCandlePosterior.NuisanceMarginalization.a_normalized_joint_posterior_gives_the_actual_physical_marginal),
  (``PhysicsLogicConsumer.CosmologicalPosterior.the_library_computes_the_marginal_acceleration_probability,
    ``PhysicsLogic.Framework.StandardCandlePosterior.NuisanceMarginalization.marginalization_retains_the_same_parameter_event),
  (``PhysicsLogicConsumer.CosmologicalPosterior.the_library_computes_the_marginal_acceleration_probability,
    ``PhysicsLogic.Framework.StandardCandlePosterior.LikelihoodModel.the_selected_posterior_event_is_the_normalized_likelihood_integral),
  (``PhysicsLogicConsumer.CosmologicalPosterior.the_library_certifies_nonvacuous_acceleration_evidence,
    ``PhysicsLogic.Framework.StandardCandlePosterior.NuisanceMarginalization.a_normalized_joint_acceleration_calculation_establishes_nonvacuous_evidence),
  (``PhysicsLogicConsumer.CosmologicalPosterior.the_library_preserves_the_same_q_event,
    ``PhysicsLogic.Framework.StandardCandlePosterior.the_deceleration_pushforward_retains_the_actual_acceleration_event),
  (``PhysicsLogicConsumer.CosmologicalPosterior.the_lambda_region_contains_at_least_the_acceleration_probability,
    ``PhysicsLogic.Framework.StandardCandlePosterior.the_same_physical_posterior_gives_no_more_acceleration_mass_than_positive_lambda_mass),
  (``PhysicsLogicConsumer.CosmologicalPosterior.the_library_uses_one_third_not_zero_for_a_flat_prior,
    ``PhysicsLogic.Framework.StandardCandlePosterior.the_flat_prior_uses_the_actual_one_third_acceleration_threshold),
  (``PhysicsLogicConsumer.CosmologicalPosterior.the_library_retains_the_boundary_mass_instead_of_silently_dropping_it,
    ``PhysicsLogic.Framework.StandardCandlePosterior.weak_acceleration_probability_retains_the_coasting_mass),
  (``PhysicsLogicConsumer.NebularCalibration.the_library_certifies_the_nonempty_positive_scale_comparison,
    ``PhysicsLogic.Framework.NebularRadialData.positive_calibration_realizes_nonvacuous_scale_comparison),
  (``PhysicsLogicConsumer.LocalInvariance.the_library_transfers_the_calibrated_response,
    ``PhysicsLogic.Paradigm.EquivalencePrinciples.local_lorentz_and_position_invariance_transfer_between_available_frames),
  (``PhysicsLogicConsumer.FrequencyReference.the_library_rejects_frequency_determination_from_a_ratio,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.ambiguous_record_does_not_determine_a_value),
  (``PhysicsLogicConsumer.FrequencyReference.the_library_recovers_frequency_with_independent_reference_access,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.calibrated_decoder_determines_record_value),
  (``PhysicsLogicConsumer.WorkSamplingTail.the_library_computes_each_observable_mean,
    ``PhysicsLogic.Framework.FiniteCanonicalData.finite_canonical_mean_is_the_actual_weighted_state_sum),
  (``PhysicsLogicConsumer.WorkSamplingTail.the_library_derives_the_exact_work_identity,
    ``PhysicsLogic.Framework.FiniteCanonicalData.actual_energy_change_reweights_the_canonical_probability),
  (``PhysicsLogicConsumer.WorkSamplingTail.the_library_derives_the_exact_work_identity,
    ``PhysicsLogic.Framework.FiniteCanonicalData.finite_partition_ratio_is_exponential_free_energy_difference),
  (``PhysicsLogicConsumer.StatePositivity.the_repaired_definition_rejects_the_distorted_functional,
    ``PhysicsLogic.Framework.QuantumGroundSector.ProjectedCorrelationFunctional.normalized_positive_iff_real_nonnegative),
  (``PhysicsLogicConsumer.StatePositivity.the_library_bounds_every_projection_probability,
    ``PhysicsLogic.Framework.QuantumGroundSector.ProjectedCorrelationFunctional.projection_expectation_is_real_probability),
  (``PhysicsLogicConsumer.StatePositivity.SharpMeasurement.individual_access_iff_two_positive_binary_measurements,
    ``PhysicsLogic.Philosophy.Observability.nonvacuous_availability_iff_inhabited_and_available),
  (``PhysicsLogicConsumer.UnitaryInfluence.the_library_preserves_the_prepared_state,
    ``PhysicsLogic.Framework.QuantumGroundSector.a_unitary_preserves_vector_state_normalization),
  (``PhysicsLogicConsumer.UnitaryInfluence.the_library_excludes_an_immediate_change,
    ``PhysicsLogic.Framework.QuantumCommutator.a_commuting_unitary_preserves_the_observable),
  (``PhysicsLogicConsumer.UnitaryInfluence.the_library_controls_the_actual_readout_change,
    ``PhysicsLogic.Framework.QuantumGroundSector.normalized_vector_intervention_bound),
  (``PhysicsLogicConsumer.NebularCalibration.the_library_exhibits_an_actual_compared_object,
    ``PhysicsLogic.Framework.NebularRadialData.nonvacuous_scale_comparison_exhibits_an_actual_object),
  (``PhysicsLogicConsumer.NebularCalibration.EvidenceComparison.every_positive_scale_supports_the_observed_radial_records,
    ``PhysicsLogic.Framework.NebularRadialData.reciprocal_distance_calibration_preserves_every_residual),
  (``PhysicsLogicConsumer.NebularCalibration.EvidenceComparison.radial_records_underdetermine_the_two_positive_scales,
    ``PhysicsLogic.Philosophy.Evidence.empirical_underdetermination_iff_explicit_obtained_support),
  (``PhysicsLogicConsumer.NebularCalibration.EvidenceComparison.the_library_excludes_underdetermination_after_the_anchor_is_obtained,
    ``PhysicsLogic.Philosophy.Evidence.discriminating_evidence_excludes_empirical_underdetermination),
  (``PhysicsLogicConsumer.NebularCalibration.the_library_preserves_each_actual_residual,
    ``PhysicsLogic.Framework.NebularRadialData.reciprocal_distance_calibration_preserves_every_residual),
  (``PhysicsLogicConsumer.NebularCalibration.the_library_preserves_the_loss_with_a_changed_coefficient,
    ``PhysicsLogic.Framework.NebularRadialData.a_nontrivial_positive_scale_changes_a_nonzero_coefficient),
  (``PhysicsLogicConsumer.NebularCalibration.the_library_preserves_the_loss_with_a_changed_coefficient,
    ``PhysicsLogic.Framework.NebularRadialData.reciprocal_distance_calibration_preserves_fixed_weight_loss),
  (``PhysicsLogicConsumer.NebularCalibration.the_library_preserves_corrected_data_under_paired_offsets,
    ``PhysicsLogic.Framework.NebularRadialData.paired_reference_offsets_preserve_corrected_velocities_and_residuals),
  (``PhysicsLogicConsumer.NebularCalibration.the_library_preserves_the_fixed_weight_loss_under_paired_offsets,
    ``PhysicsLogic.Framework.NebularRadialData.paired_reference_offsets_preserve_fixed_weight_loss),
  (``PhysicsLogicConsumer.NebularCalibration.an_unresolved_anchor_allows_unbounded_coefficients_with_the_same_loss,
    ``PhysicsLogic.Framework.NebularRadialData.positive_calibration_preserves_finite_positive_distances),
  (``PhysicsLogicConsumer.NebularCalibration.an_unresolved_anchor_allows_unbounded_coefficients_with_the_same_loss,
    ``PhysicsLogic.Framework.NebularRadialData.reciprocal_distance_calibration_preserves_fixed_weight_loss),
  (``PhysicsLogicConsumer.NebularCalibration.a_small_anchor_error_admits_distinct_coefficients_with_the_same_loss,
    ``PhysicsLogic.Framework.NebularRadialData.reciprocal_distance_calibration_preserves_fixed_weight_loss),
  (``PhysicsLogicConsumer.CondensedMatter.ScaleFlowReuse.the_library_derives_the_zero_large_scale_limit,
    ``PhysicsLogic.Framework.PositiveLogScaleTrajectory.future_continuation_and_a_negative_monotone_beta_force_zero),
  (``PhysicsLogicConsumer.CondensedMatter.ScaleFlowReuse.the_library_excludes_a_persistent_conducting_response,
    ``PhysicsLogic.Framework.PositiveLogScaleTrajectory.a_zero_limit_excludes_a_persistent_positive_response),
  (``PhysicsLogicConsumer.CondensedMatter.ScaleFlowReuse.the_library_certifies_the_floor_curve_at_every_scale,
    ``PhysicsLogic.Framework.PositiveLogScaleTrajectory.an_actual_beta_derivative_is_nonvacuous),
  (``PhysicsLogicConsumer.CondensedMatter.ScaleFlowReuse.the_library_rejects_an_independently_reassigned_floor_beta,
    ``PhysicsLogic.Framework.PositiveLogScaleTrajectory.the_beta_value_is_fixed_by_the_actual_derivative),
  (``PhysicsLogicConsumer.StatMech.FiniteWorkSamplingReuse.the_public_canonical_api_computes_the_actual_reference,
    ``PhysicsLogic.Framework.FiniteCanonicalData.finite_canonical_mean_is_the_actual_weighted_state_sum),
  (``PhysicsLogicConsumer.StatMech.FiniteWorkSamplingReuse.the_library_transfers_confidence_only_to_a_selected_quench_readout,
    ``PhysicsLogic.Philosophy.ProbabilityRoles.typical_state_has_typical_property_through_bridge),
  (``PhysicsLogicConsumer.StatMech.TypicalityReuse.the_library_exhibits_a_selected_thermal_sample,
    ``PhysicsLogic.Philosophy.ProbabilityRoles.nonvacuous_typical_property_exhibits_selected_state),
  (``PhysicsLogicConsumer.StatMech.TypicalityReuse.the_library_transfers_the_typical_property_only_to_a_selected_sample,
    ``PhysicsLogic.Philosophy.ProbabilityRoles.typical_state_has_typical_property_through_bridge),
  (``PhysicsLogicConsumer.StatMech.SimultaneousTypicality.the_selection_bridge_iff_no_selected_state_is_excluded,
    ``PhysicsLogic.Philosophy.ProbabilityRoles.typical_property_bridge_iff_selected_state_soundness),
  (``PhysicsLogicConsumer.StatMech.SimultaneousTypicality.sound_nonempty_selection_requires_a_state_outside_the_test_family,
    ``PhysicsLogic.Philosophy.ProbabilityRoles.sound_nonempty_selection_has_simultaneous_properties),
  (``PhysicsLogicConsumer.CondensedMatter.SelectedStateReuse.the_library_recovers_breaking_from_the_selected_minima,
    ``PhysicsLogic.Philosophy.Symmetry.selected_movement_and_physical_action_establish_spontaneous_breaking),
  (``PhysicsLogicConsumer.CondensedMatter.SelectedStateReuse.the_library_recovers_breaking_from_the_selected_minima,
    ``PhysicsLogic.Philosophy.Symmetry.moved_selected_breaking_implies_noninvariant_selected_breaking),
  (``PhysicsLogicConsumer.CondensedMatter.SelectedStateReuse.the_library_exhibits_the_other_selected_minimum,
    ``PhysicsLogic.Philosophy.Symmetry.spontaneous_breaking_requires_selected_state_and_preserved_family),
  (``PhysicsLogicConsumer.CondensedMatter.SelectedStateReuse.the_library_rejects_the_excited_high_temperature_configuration,
    ``PhysicsLogic.Philosophy.Symmetry.spontaneous_breaking_requires_selected_state_and_preserved_family),
  (``PhysicsLogicConsumer.MeasurementRecords.ReversalCalibration.the_public_measurement_api_certifies_the_calibrated_gravity_readout,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.calibrated_decoder_determines_record_value),
  (``PhysicsLogicConsumer.MeasurementRecords.ReversalCalibration.the_public_measurement_api_rejects_gravity_determination_from_uncorrected_records,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.ambiguous_record_does_not_determine_a_value),
  (``PhysicsLogicConsumer.ClassicalDynamics.QuadraticDirections.the_library_supplies_unique_quadratic_evolution,
    ``PhysicsLogic.Paradigm.Dynamics.total_deterministic_evolution_is_unique_everywhere),
  (``PhysicsLogicConsumer.ClassicalDynamics.QuadraticDirections.the_library_excludes_branching_of_this_nonlinear_orbit,
    ``PhysicsLogic.Paradigm.Dynamics.unique_forward_evolution_excludes_branching_at),
  (``PhysicsLogicConsumer.ClassicalDynamics.ModalReturn.the_library_transfers_the_actual_full_state_return_to_the_energy_observable,
    ``PhysicsLogic.Paradigm.EntropyAndIrreversibility.EvolutionReturnContext.exact_recurrence_is_near_recurrence_for_reflexive_neighborhood),
  (``PhysicsLogicConsumer.ClassicalDynamics.ModalReturn.the_library_certifies_full_return_in_rescaled_energy_units,
    ``PhysicsLogic.Paradigm.EntropyAndIrreversibility.EvolutionReturnContext.exact_recurrence_is_near_recurrence_for_reflexive_neighborhood),
  (``PhysicsLogicConsumer.NuclearScattering.LowEnergyExpansion.the_library_derives_the_actual_effective_range_expansion,
    ``PhysicsLogic.Framework.EffectiveRangeExpansion.quartic_control_establishes_nonvacuous_effective_range_expansion),
  (``PhysicsLogicConsumer.NuclearScattering.LowEnergyExpansion.the_source_truncation_has_a_computed_nonzero_remainder,
    ``PhysicsLogic.Framework.EffectiveRangeExpansion.nonvacuous_expansion_iff_control_and_actual_coefficients),
  (``PhysicsLogicConsumer.NuclearScattering.LowEnergyExpansion.the_library_identifies_the_unique_low_energy_coefficients,
    ``PhysicsLogic.Framework.EffectiveRangeExpansion.the_actual_effective_range_coefficients_are_unique),
  (``PhysicsLogicConsumer.NuclearScattering.LowEnergyExpansion.the_library_exhibits_a_positive_momentum_prediction,
    ``PhysicsLogic.Framework.EffectiveRangeExpansion.nonvacuous_expansion_has_a_matched_positive_momentum),
  (``PhysicsLogicConsumer.NuclearScattering.LowEnergyExpansion.the_library_composes_independent_phase_reconstruction_errors,
    ``PhysicsLogic.Framework.EffectiveRangeExpansion.independent_quartic_errors_compose_through_the_shared_paradigm),
  (``PhysicsLogicConsumer.NuclearScattering.LowEnergyExpansion.the_reconstructed_phase_has_the_same_first_two_coefficients,
    ``PhysicsLogic.Framework.EffectiveRangeExpansion.quartic_control_establishes_nonvacuous_effective_range_expansion),
  (``PhysicsLogicConsumer.NuclearScattering.LowEnergyExpansion.the_library_bounds_the_actual_threshold_amplitude,
    ``PhysicsLogic.Framework.ElasticSWave.controlled_phase_error_bounds_amplitude_error),
  (``PhysicsLogicConsumer.NuclearScattering.LowEnergyExpansion.the_controlled_phases_give_actual_elastic_scattering,
    ``PhysicsLogic.Framework.ElasticSWave.real_effective_range_function_realizes_elastic_scattering),
  (``PhysicsLogicConsumer.NuclearScattering.LowEnergyExpansion.same_effective_range_coefficients_do_not_fix_the_scattering_amplitude,
    ``PhysicsLogic.Framework.ElasticSWave.inverse_amplitude_recovers_real_effective_range_function),
  (``PhysicsLogicConsumer.NuclearScattering.LowEnergyExpansion.a_phase_error_tolerance_is_not_an_amplitude_error_tolerance,
    ``PhysicsLogic.Framework.ElasticSWave.real_effective_range_function_realizes_elastic_scattering),
  (``PhysicsLogicConsumer.StatMech.ExcitationResponseReuse.the_library_retains_the_bose_response_enhancement,
    ``PhysicsLogic.Framework.EquilibriumExcitationData.the_response_weight_retains_the_statistics),
  (``PhysicsLogicConsumer.StatMech.ExcitationResponseReuse.the_library_differentiates_each_actual_mode,
    ``PhysicsLogic.Framework.EquilibriumExcitationData.each_mode_has_the_actual_momentum_current_derivative),
  (``PhysicsLogicConsumer.StatMech.ExcitationResponseReuse.the_library_derives_the_clients_nonvacuous_current_response,
    ``PhysicsLogic.Framework.EquilibriumExcitationData.the_momentum_calculation_realizes_a_nonvacuous_response),
  (``PhysicsLogicConsumer.StatMech.ExcitationResponseReuse.the_library_exhibits_a_strictly_positive_current_derivative,
    ``PhysicsLogic.Framework.EquilibriumExcitationData.a_nonvacuous_response_has_a_nonzero_diagonal_derivative),
  (``PhysicsLogicConsumer.Fluctuations.the_library_reflects_both_current_bin_endpoints,
    ``PhysicsLogic.Framework.WeightedReversalEvents.Model.reversal_reflects_both_observation_window_endpoints),
  (``PhysicsLogicConsumer.Fluctuations.the_current_bin_bounds_the_actual_exponent_variation,
    ``PhysicsLogic.Framework.WeightedReversalEvents.membership_in_a_window_bounds_the_reference_error),
  (``PhysicsLogicConsumer.Fluctuations.the_library_derives_the_finite_resolution_logarithmic_estimate,
    ``PhysicsLogic.Framework.WeightedReversalEvents.Model.finite_resolution_inputs_derive_nonvacuous_logarithmic_estimate),
  (``PhysicsLogicConsumer.Fluctuations.the_library_realizes_a_controlled_current_approximation,
    ``PhysicsLogic.Framework.WeightedReversalEvents.Model.logarithmic_estimate_realizes_controlled_approximation),
  (``PhysicsLogicConsumer.Fluctuations.the_approximation_target_predicts_the_actual_log_ratio_not_the_reference,
    ``PhysicsLogic.Framework.WeightedReversalEvents.Model.logRatioApproximationContext),
  (``PhysicsLogicConsumer.Fluctuations.finite_resolution_does_not_supply_a_zero_error_current_estimate,
    ``PhysicsLogic.Framework.WeightedReversalEvents.Model.zero_logarithmic_error_recovers_the_exact_exponential),
  (``PhysicsLogicConsumer.Fluctuations.preparation_produces_the_actual_polynomial_correction,
    ``PhysicsLogic.Framework.WeightedReversalEvents.Model.event_ratio_cancels_the_common_normalizer),
  (``PhysicsLogicConsumer.Fluctuations.the_library_keeps_the_leading_bias_under_sublinear_preparation_error,
    ``PhysicsLogic.Framework.WeightedReversalEvents.sublinear_logarithmic_error_preserves_the_leading_rate),
  (``PhysicsLogicConsumer.Fluctuations.the_library_bounds_the_preparation_corrected_current_ratio,
    ``PhysicsLogic.Framework.WeightedReversalEvents.Model.bounded_reweighting_controls_actual_event_probabilities),
  (``PhysicsLogicConsumer.Fluctuations.nonuniform_preparation_preserves_the_aggregate_current_ratio,
    ``PhysicsLogic.Framework.WeightedReversalEvents.Model.a_positive_lower_comparison_retains_positive_weights),
  (``PhysicsLogicConsumer.Fluctuations.the_library_aggregates_the_actual_path_ratio,
    ``PhysicsLogic.Framework.WeightedReversalEvents.Model.constant_pair_ratios_give_the_exact_event_ratio),
  (``PhysicsLogicConsumer.Fluctuations.the_library_derives_nonvacuous_current_probabilities,
    ``PhysicsLogic.Framework.WeightedReversalEvents.Model.physical_weight_inputs_derive_nonvacuous_ratio_bounds),
  (``PhysicsLogicConsumer.Fluctuations.the_library_derives_actual_statistical_preference,
    ``PhysicsLogic.Framework.WeightedReversalEvents.Model.a_ratio_bound_above_one_gives_statistical_asymmetry),
  (``PhysicsLogicConsumer.Fluctuations.the_library_retains_the_reversed_observation,
    ``PhysicsLogic.Paradigm.FluctuationsAndArrow.WeightedReversalContext.statistical_asymmetry_retains_the_reverse_pair),
  (``PhysicsLogicConsumer.Fluctuations.the_library_distinguishes_the_two_current_events,
    ``PhysicsLogic.Paradigm.FluctuationsAndArrow.WeightedReversalContext.asymmetric_weights_distinguish_the_reversed_observations),
  (``PhysicsLogicConsumer.Fluctuations.the_library_retains_the_reverse_weighted_aggregation,
    ``PhysicsLogic.Framework.WeightedReversalEvents.Model.event_ratio_is_a_reverse_weighted_average_of_pair_ratios),
  (``PhysicsLogicConsumer.Fluctuations.the_unbiased_walk_retains_the_actual_reversal_pair,
    ``PhysicsLogic.Framework.WeightedReversalEvents.Model.physical_weight_inputs_derive_nonvacuous_aggregation),
  (``PhysicsLogicConsumer.Fluctuations.the_library_does_not_infer_bias_from_reversal_alone,
    ``PhysicsLogic.Framework.WeightedReversalEvents.Model.constant_pair_ratios_give_the_exact_event_ratio),
  (``PhysicsLogicConsumer.Fluctuations.the_library_recovers_the_monotone_history_ratio,
    ``PhysicsLogic.Framework.WeightedReversalEvents.Model.event_ratio_cancels_the_common_normalizer),
  (``PhysicsLogicConsumer.Fluctuations.the_library_derives_the_expected_per_step_logarithmic_bias,
    ``PhysicsLogic.Framework.WeightedReversalEvents.a_linear_exponent_and_uniform_correction_give_the_logarithmic_rate),
  (``PhysicsLogicConsumer.MeasurementRecords.the_library_derives_three_outcome_record_agreement,
    ``PhysicsLogic.Framework.CoherentRecordMeasurement.Process.comparison_inputs_derive_nonvacuous_record_result),
  (``PhysicsLogicConsumer.MeasurementRecords.FiniteRecordReduction.the_library_realizes_the_three_coordinate_record_reduction,
    ``PhysicsLogic.Framework.FiniteQuantumState.TwoBranchRecordState.normalized_populated_records_realize_reduction),
  (``PhysicsLogicConsumer.MeasurementRecords.FiniteRecordReduction.the_library_keeps_global_purity_and_actual_reduced_mixedness,
    ``PhysicsLogic.Framework.FiniteQuantumState.TwoBranchRecordState.distinguished_records_give_actual_mixedness),
  (``PhysicsLogicConsumer.MeasurementRecords.FiniteRecordReduction.the_library_retains_a_nonzero_imaginary_coherence,
    ``PhysicsLogic.Framework.FiniteQuantumState.TwoBranchRecordState.reduced_off_diagonal),
  (``PhysicsLogicConsumer.MeasurementRecords.FiniteRecordReduction.the_library_computes_the_independent_reduced_purity,
    ``PhysicsLogic.Framework.FiniteQuantumState.TwoBranchRecordState.actual_reduced_purity),
  (``PhysicsLogicConsumer.MeasurementRecords.the_library_preserves_actual_quantum_normalization,
    ``PhysicsLogic.Framework.CoherentRecordMeasurement.Process.calibration_preserves_normalization),
  (``PhysicsLogicConsumer.MeasurementRecords.the_library_preserves_the_imaginary_coefficient,
    ``PhysicsLogic.Framework.CoherentRecordMeasurement.Process.calibration_preserves_the_same_input_coefficients),
  (``PhysicsLogicConsumer.MeasurementRecords.the_library_excludes_a_single_outcome_state_after_communication,
    ``PhysicsLogic.Framework.CoherentRecordMeasurement.Process.two_supported_alternatives_exclude_certain_compared_outcome),
  (``PhysicsLogicConsumer.MeasurementRecords.the_library_recovers_the_value_from_a_pointer_record,
    ``PhysicsLogic.Framework.CoherentRecordMeasurement.Process.pointer_record_determines_the_correlated_value),
  (``PhysicsLogicConsumer.MeasurementRecords.the_library_does_not_turn_a_match_record_into_an_outcome,
    ``PhysicsLogic.Framework.CoherentRecordMeasurement.Process.correlation_record_does_not_determine_the_individual_value),
  (``PhysicsLogicConsumer.MeasurementRecords.the_library_rejects_temperature_determination_from_common_bias_agreement,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.ambiguous_record_does_not_determine_a_value),
  (``PhysicsLogicConsumer.MeasurementRecords.the_library_determines_temperature_with_the_reference,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.calibrated_decoder_determines_record_value),
  (``PhysicsLogicConsumer.MeasurementRecords.the_library_preserves_a_display_fact_under_refined_access,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.finer_records_preserve_determined_values),
  (``PhysicsLogicConsumer.MeasurementRecords.the_library_rejects_two_temperatures_for_the_same_reference_record,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.determined_record_value_is_unique),
  (``PhysicsLogicConsumer.MeasurementRecords.IntervalConstraints.the_library_recovers_positive_temperature_without_exact_identification,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.record_constraint_mono),
  (``PhysicsLogicConsumer.MeasurementRecords.ExactTemperatureInformation.record_constraint_iff_exact_interval,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.record_constraint_holds_on_compatible_configuration),
  (``PhysicsLogicConsumer.MeasurementRecords.ExactTemperatureInformation.exact_temperature_iff_lowest_possible_reading,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.record_determination_iff_equality_constraint),
  (``PhysicsLogicConsumer.MeasurementRecords.IntervalConstraints.the_library_recombines_lower_and_upper_temperature_constraints,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.record_constraints_combine),
  (``PhysicsLogicConsumer.MeasurementRecords.IntervalConstraints.the_library_applies_interval_only_to_a_compatible_configuration,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.record_constraint_holds_on_compatible_configuration),
  (``PhysicsLogicConsumer.MeasurementRecords.IntervalConstraints.the_library_preserves_interval_after_reference_access,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.finer_records_preserve_value_constraints),
  (``PhysicsLogicConsumer.MeasurementRecords.IntervalConstraints.the_library_derives_an_interval_from_a_calibrated_value,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.determined_record_constrains_every_property_of_its_value),
  (``PhysicsLogicConsumer.MeasurementRecords.IntervalConstraints.the_library_identifies_exact_temperature_as_an_equality_constraint,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.record_determination_iff_equality_constraint),
  (``PhysicsLogicConsumer.MeasurementRecords.EstimateAssignment.the_library_does_not_identify_the_recorded_center_with_physical_temperature,
    ``PhysicsLogic.Philosophy.OperationalValue.operational_value_contains_established_representation),
  (``PhysicsLogicConsumer.MeasurementRecords.ReferenceCorrection.representation_faithful_iff_decoder_correct,
    ``PhysicsLogic.Philosophy.MathematicsAndNature.faithful_representation_iff_nonempty_sound_assignments),
  (``PhysicsLogicConsumer.MeasurementRecords.ReferenceCorrection.one_correct_assignment_does_not_establish_sound_representation,
    ``PhysicsLogic.Philosophy.MathematicsAndNature.unfaithful_representation_refutes_faithfulness),
  (``PhysicsLogicConsumer.MeasurementRecords.ReferenceCorrection.one_correct_recorded_value_does_not_certify_global_soundness,
    ``PhysicsLogic.Philosophy.OperationalValue.recorded_measurement_contains_assigned_representation),
  (``PhysicsLogicConsumer.MeasurementRecords.RecordRefinement.reference_access_recovers_coarse_readout_but_not_conversely,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.records_refine_iff_coarse_record_decoder),
  (``PhysicsLogicConsumer.MeasurementRecords.RecordRefinement.identical_value_inferences_do_not_make_records_equivalent,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.determined_record_constrains_every_property_of_its_value),
  (``PhysicsLogicConsumer.MeasurementRecords.RecordRefinement.pointer_access_is_strictly_finer_than_match_only_access,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.records_refine_iff_coarse_record_decoder),
  (``PhysicsLogicConsumer.AMOSpectroscopy.ConventionalSinglePulse.the_library_preserves_the_cyclic_to_angular_frequency_conversion,
    ``PhysicsLogic.Framework.CoherentTwoState.pulse_solves_schrodinger),
  (``PhysicsLogicConsumer.AMOSpectroscopy.ConventionalSinglePulse.the_library_realizes_the_detuned_single_pulse,
    ``PhysicsLogic.Framework.CoherentTwoState.single_pulse_realizes_coherent_transition),
  (``PhysicsLogicConsumer.AMOSpectroscopy.ConventionalSinglePulse.a_second_pulse_is_not_the_conventional_single_region_response,
    ``PhysicsLogic.Framework.CoherentTwoState.pulse_free_pulse_transition_probability),
  (``PhysicsLogicConsumer.MeasurementRecords.TailOnlyLineWidth.the_library_rejects_width_identification_from_tail_records,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.ambiguous_record_does_not_determine_a_value),
  (``PhysicsLogicConsumer.MeasurementRecords.TailOnlyLineWidth.the_library_determines_width_with_a_calibrated_inner_probe,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.calibrated_decoder_determines_record_value),
  (``PhysicsLogicConsumer.MeasurementRecords.WeakLineIntensity.the_library_rejects_identification_at_insufficient_beam_intensity,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.ambiguous_record_does_not_determine_a_value),
  (``PhysicsLogicConsumer.MeasurementRecords.WeakLineIntensity.the_library_recovers_line_presence_when_beam_intensity_exceeds_the_error,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.calibrated_decoder_determines_record_value),
  (``PhysicsLogicConsumer.MeasurementRecords.MomentStandards.the_library_decodes_the_ratio_without_the_absolute_standard,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.calibrated_decoder_determines_record_value),
  (``PhysicsLogicConsumer.MeasurementRecords.MomentStandards.the_library_rejects_absolute_moment_identification_from_the_same_records,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.ambiguous_record_does_not_determine_a_value),
  (``PhysicsLogicConsumer.MeasurementRecords.MomentStandards.the_library_decodes_an_absolute_moment_when_the_standard_is_available,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.calibrated_decoder_determines_record_value),
  (``PhysicsLogicConsumer.StellarHydrostatics.the_library_exhibits_growing_enclosed_mass,
    ``PhysicsLogic.Framework.SphericalMassProfile.positive_source_and_mass_balance_give_mass_growth),
  (``PhysicsLogicConsumer.StellarHydrostatics.the_library_recovers_declining_density_from_actual_mass,
    ``PhysicsLogic.Framework.SphericalMassProfile.actual_mass_gradient_recovers_gravitational_source),
  (``PhysicsLogicConsumer.StellarHydrostatics.the_library_rejects_alternative_density_for_the_same_mass,
    ``PhysicsLogic.Framework.SphericalMassProfile.same_mass_profile_cannot_have_two_gravitational_sources),
  (``PhysicsLogicConsumer.StellarHydrostatics.the_library_excludes_spatially_constant_mass,
    ``PhysicsLogic.Framework.SphericalMassProfile.nonvacuous_mass_growth_excludes_constant_mass),
  (``PhysicsLogicConsumer.RadioactiveDecay.IsotopeMixture.component_has_the_actual_exponential_tail,
    ``PhysicsLogic.Framework.DecayTimeRecordLaw.exponential_survival_probability),
  (``PhysicsLogicConsumer.RadioactiveDecay.IsotopeMixture.each_component_has_actual_memoryless_decay_records,
    ``PhysicsLogic.Framework.DecayTimeRecordLaw.actual_exponential_records_exhibit_nonvacuous_future_decay),
  (``PhysicsLogicConsumer.RadioactiveDecay.IsotopeMixture.the_library_exhibits_both_actual_record_events,
    ``PhysicsLogic.Framework.DecayTimeRecordLaw.nonvacuous_decay_has_actual_surviving_and_decaying_records),
  (``PhysicsLogicConsumer.RadioactiveDecay.IsotopeMixture.the_library_conditions_the_actual_mixed_population,
    ``PhysicsLogic.Framework.DecayTimeRecordLaw.conditional_survival_is_the_actual_tail_ratio),
  (``PhysicsLogicConsumer.RadioactiveDecay.IsotopeMixture.the_library_rejects_every_constant_rate_for_the_mixture,
    ``PhysicsLogic.Framework.DecayTimeRecordLaw.positive_exponential_tail_realizes_actual_conditioning),
  (``PhysicsLogicConsumer.RadioactiveDecay.IsotopeMixture.the_library_rejects_every_constant_rate_for_the_mixture,
    ``PhysicsLogic.Framework.ExponentialMetastableSurvivalReadout.exponential_survival_and_conditional_consistency_imply_memorylessness),
  (``PhysicsLogicConsumer.RadioactiveDecay.IsotopeMixture.the_library_distinguishes_elapsed_escape_from_the_survival_drop,
    ``PhysicsLogic.Framework.DecayTimeRecordLaw.escape_probability_is_the_actual_survival_drop),
  (``PhysicsLogicConsumer.RadioactiveDecay.IsotopeMixture.the_library_normalizes_both_actual_conditional_outcomes,
    ``PhysicsLogic.Framework.DecayTimeRecordLaw.actual_conditioned_outcomes_are_normalized),
  (``PhysicsLogicConsumer.RadioactiveDecay.IsotopeMixture.the_library_assigns_no_escape_to_zero_elapsed_time,
    ``PhysicsLogic.Framework.DecayTimeRecordLaw.zero_elapsed_has_no_escape_event),
  (``PhysicsLogicConsumer.RadioactiveDecay.CoherentRevival.the_library_rejects_a_lifetime_interpretation_of_coherent_occupation,
    ``PhysicsLogic.Framework.DecayTimeRecordLaw.survival_probability_is_antitone),
  (``PhysicsLogicConsumer.StatMech.OrderedLimitReuse.the_library_rejects_interchanging_relaxation_and_vanishing_rate,
    ``PhysicsLogic.Paradigm.OrderedLimits.ObservableLimitFamily.actual_noncommutation_excludes_commutation),
  (``PhysicsLogicConsumer.StatMech.OrderedLimitReuse.the_library_rejects_assigning_zero_to_the_equilibrated_order,
    ``PhysicsLogic.Paradigm.OrderedLimits.ObservableLimitFamily.two_realizations_of_one_order_have_the_same_value),
  (``PhysicsLogicConsumer.StatMech.OrderedLimitReuse.the_library_rejects_an_empty_time_approach_for_the_same_population,
    ``PhysicsLogic.Paradigm.OrderedLimits.ObservableLimitFamily.a_realized_order_requires_both_nontrivial_approaches),
  (``PhysicsLogicConsumer.StatMech.ConditionalHistoryReuse.the_actual_conditional_noise_kernel_keeps_its_gaussian_law,
    ``PhysicsLogic.Framework.InitialEnsemblePrediction.an_independent_input_keeps_its_actual_law_after_conditioning),
  (``PhysicsLogicConsumer.StatMech.ConditionalHistoryReuse.the_library_predicts_fresh_thermal_noise_through_the_current_coarse_state,
    ``PhysicsLogic.Framework.InitialEnsemblePrediction.a_history_independent_input_predicts_through_the_retained_state),
  (``PhysicsLogicConsumer.StatMech.ConditionalHistoryReuse.the_conditional_query_integral_uses_the_actual_variance_two_noise,
    ``PhysicsLogic.Framework.InitialEnsemblePrediction.an_independent_input_gives_the_actual_conditional_query_integral),
  (``PhysicsLogicConsumer.StatMech.ConditionalHistoryReuse.the_correlated_observation_history_is_not_markov,
    ``PhysicsLogic.Framework.InitialEnsemblePrediction.a_past_known_fluctuating_residual_independent_of_the_present_is_not_markov),
  (``PhysicsLogicConsumer.StatMech.ConditionalHistoryReuse.the_correlated_observation_history_is_not_markov,
    ``PhysicsLogic.Framework.InitialEnsemblePrediction.a_measurable_query_of_an_earlier_state_is_known_from_the_past),
  (``PhysicsLogicConsumer.StatMech.ConditionalHistoryReuse.exact_static_coarse_predictions_do_not_supply_temporal_markov_prediction,
    ``PhysicsLogic.Framework.StatisticalCoarseGraining.Data.actual_probability_projection_realizes_nonvacuous_retained_predictions),
  (``PhysicsLogicConsumer.StatMech.StateSufficiencyReuse.the_actual_thermal_subsystem_is_markov_without_recovering_the_microstate,
    ``PhysicsLogic.Framework.InitialEnsemblePrediction.measurable_state_closure_gives_the_actual_markov_prediction_property),
  (``PhysicsLogicConsumer.StatMech.RealizerPrediction.selected_robust_prediction_iff_every_compatible_initial_state_agrees,
    ``PhysicsLogic.Paradigm.ReductionAndOntologyPositions.autonomous_emergence_iff_distinct_realizers_and_supported_behavior),
  (``PhysicsLogicConsumer.StatMech.RealizerPrediction.the_pair_prediction_is_both_derivationally_reduced_and_robust,
    ``PhysicsLogic.Paradigm.ReductionAndOntologyPositions.derivational_reduction_and_autonomous_emergence_are_compatible),
  (``PhysicsLogicConsumer.StatMech.RealizerPrediction.a_closed_pair_description_does_not_uniquely_recover_the_full_initial_state,
    ``PhysicsLogic.Paradigm.ReductionAndEmergence.multiple_realization_excludes_unique_micro_recovery),
  (``PhysicsLogicConsumer.StatMech.StateSufficiencyReuse.projecting_the_closed_thermal_subsystem_loses_markov_prediction,
    ``PhysicsLogic.Framework.InitialEnsemblePrediction.a_fluctuating_future_known_from_the_past_but_independent_of_the_present_is_not_markov),
  (``PhysicsLogicConsumer.StatMech.StateSufficiencyReuse.projecting_the_closed_thermal_subsystem_loses_markov_prediction,
    ``PhysicsLogic.Framework.InitialEnsemblePrediction.a_measurable_query_of_an_earlier_state_is_known_from_the_past),
  (``PhysicsLogicConsumer.StatMech.StateSufficiencyReuse.the_early_walk_pasts_are_generated_by_the_current_observation,
    ``PhysicsLogic.Framework.InitialEnsemblePrediction.current_information_is_part_of_the_actual_past),
  (``PhysicsLogicConsumer.StatMech.StateSufficiencyReuse.the_actual_three_time_random_walk_is_markov,
    ``PhysicsLogic.Framework.InitialEnsemblePrediction.measurable_observations_give_a_valid_past_information_algebra),
  (``PhysicsLogicConsumer.StatMech.StateSufficiencyReuse.the_random_walk_does_not_have_deterministic_state_closure,
    ``PhysicsLogic.Framework.InitialEnsemblePrediction.closed_current_states_cannot_have_different_selected_futures),
  (``PhysicsLogicConsumer.StatMech.InitialEnsembleReuse.the_actual_thermal_law_realizes_nonzero_correlated_force_channels,
    ``PhysicsLogic.Framework.FiniteResidualCovariance.LinearResidualModel.a_realized_initial_law_and_stationary_covariance_give_an_actual_noise_process),
  (``PhysicsLogicConsumer.StatMech.InitialEnsembleReuse.the_mixed_channels_have_stationary_gaussian_joint_laws,
    ``PhysicsLogic.Framework.FiniteResidualCovariance.LinearResidualModel.gaussian_initial_sampling_gives_jointly_gaussian_forces),
  (``PhysicsLogicConsumer.StatMech.InitialEnsembleReuse.the_mixed_channels_have_stationary_gaussian_joint_laws,
    ``PhysicsLogic.Framework.FiniteResidualCovariance.LinearResidualModel.gaussian_covariance_stationarity_preserves_every_joint_force_law),
  (``PhysicsLogicConsumer.StatMech.InitialEnsembleReuse.the_cross_channel_second_moment_is_an_actual_integral,
    ``PhysicsLogic.Framework.FiniteResidualCovariance.LinearResidualModel.the_force_second_moment_is_the_actual_two_time_matrix),
  (``PhysicsLogicConsumer.StatMech.InitialEnsembleReuse.independent_thermal_inputs_do_not_make_the_mixed_force_channels_independent,
    ``PhysicsLogic.Framework.FiniteResidualCovariance.LinearResidualModel.nonzero_actual_force_covariance_rejects_independent_resampling),
  (``PhysicsLogicConsumer.StatMech.InitialEnsembleReuse.a_joint_law_marginal_is_the_original_force_observation,
    ``PhysicsLogic.Framework.FiniteResidualCovariance.LinearResidualModel.the_joint_law_has_the_actual_force_marginal),
  (``PhysicsLogicConsumer.StatMech.InitialEnsembleReuse.relabeling_observation_times_keeps_the_same_underlying_ensemble,
    ``PhysicsLogic.Framework.FiniteResidualCovariance.LinearResidualModel.selecting_observation_times_preserves_the_actual_joint_law),
  (``PhysicsLogicConsumer.StatMech.InitialEnsembleReuse.fixing_the_full_initial_state_collapses_the_computed_joint_law,
    ``PhysicsLogic.Framework.FiniteResidualCovariance.LinearResidualModel.fixing_all_initial_data_gives_a_dirac_joint_force_law),
  (``PhysicsLogicConsumer.StatMech.InitialEnsembleReuse.a_fixed_sample_does_not_retain_the_ensemble_noise_variance,
    ``PhysicsLogic.Framework.FiniteResidualCovariance.LinearResidualModel.fixed_initial_data_do_not_have_nonzero_noise_variance),
  (``PhysicsLogicConsumer.StatMech.CausalMemoryReuse.the_library_identifies_the_actual_finite_coefficient,
    ``PhysicsLogic.Framework.CausalMemoryLocalization.a_kernel_primitive_is_the_actual_finite_coefficient),
  (``PhysicsLogicConsumer.StatMech.CausalMemoryReuse.the_library_bounds_the_actual_changing_history_memory,
    ``PhysicsLogic.Framework.CausalMemoryLocalization.a_slow_profile_and_primitive_budget_control_the_local_readout),
  (``PhysicsLogicConsumer.StatMech.CausalMemoryReuse.the_library_resolves_nonzero_memory_for_the_changing_history,
    ``PhysicsLogic.Framework.CausalMemoryLocalization.a_local_signal_above_the_error_resolves_actual_memory),
  (``PhysicsLogicConsumer.StatMech.CausalMemoryReuse.the_library_ignores_changes_only_in_the_future_history,
    ``PhysicsLogic.Framework.CausalMemoryLocalization.identical_past_histories_have_identical_memory),
  (``PhysicsLogicConsumer.StatMech.CausalMemoryReuse.the_public_operator_adapter_retains_noncommuting_order,
    ``PhysicsLogic.Framework.CausalMemoryLocalization.matrix_operator_composition_preserves_the_order),
  (``PhysicsLogicConsumer.StatMech.CausalMemoryReuse.a_nonzero_rectangular_kernel_can_cancel_a_nonzero_history,
    ``PhysicsLogic.Framework.CausalMemoryLocalization.matrixOperator),
  (``PhysicsLogicConsumer.ImpermeableLayer.library_retained_equation_is_exact,
    ``PhysicsLogic.Framework.BoundaryLayerFieldReduction.Data.full_and_retained_residuals_differ_by_actual_discarded_terms),
  (``PhysicsLogicConsumer.ImpermeableLayer.library_recognizes_actual_inner_viscous_balance,
    ``PhysicsLogic.Framework.BoundaryLayerFieldReduction.Data.primitive_balances_and_bounds_realize_nonvacuous_controlled_reduction),
  (``PhysicsLogicConsumer.ImpermeableLayer.deleting_time_acceleration_breaks_the_inner_balance,
    ``PhysicsLogic.Framework.BoundaryLayerFieldReduction.Data.retained_equation_keeps_the_actual_time_acceleration),
  (``PhysicsLogicConsumer.FluidCorrelations.RetardedResponseReuse.opposing_nonzero_past_forces_can_cancel_the_readout,
    ``PhysicsLogic.Framework.RetardedLinearResponse.integrable_force_histories_superpose_their_responses),
  (``PhysicsLogicConsumer.FluidCorrelations.RetardedResponseReuse.the_library_preserves_response_under_future_force_changes,
    ``PhysicsLogic.Framework.RetardedLinearResponse.past_equivalence_preserves_integrability_and_nonvacuous_response),
  (``PhysicsLogicConsumer.FluidCorrelations.RetardedResponseReuse.the_library_preserves_response_under_future_force_changes,
    ``PhysicsLogic.Framework.RetardedLinearResponse.almost_everywhere_past_agreement_preserves_the_causal_readout),
  (``PhysicsLogicConsumer.FluidCorrelations.RetardedResponseReuse.the_library_differentiates_the_actual_force_amplitude,
    ``PhysicsLogic.Framework.RetardedLinearResponse.the_convolution_coefficient_is_an_actual_probe_derivative),
  (``PhysicsLogicConsumer.FluidCorrelations.RetardedResponseReuse.the_library_identifies_a_nonzero_static_response,
    ``PhysicsLogic.Framework.RetardedLinearResponse.a_nonzero_integrable_kernel_integral_realizes_the_static_response),
  (``PhysicsLogicConsumer.FluidCorrelations.RetardedResponseReuse.the_library_derives_temporal_response_and_probe_detectability,
    ``PhysicsLogic.Framework.RetardedLinearResponse.a_nonvacuous_impulse_readout_realizes_retarded_response),
  (``PhysicsLogicConsumer.FluidCorrelations.RetardedResponseReuse.the_library_derives_temporal_response_and_probe_detectability,
    ``PhysicsLogic.Framework.RetardedLinearResponse.an_active_impulse_is_detectable_against_the_absent_probe),
  (``PhysicsLogicConsumer.FluidCorrelations.RetardedResponseReuse.the_library_differentiates_the_impulse_amplitude,
    ``PhysicsLogic.Framework.RetardedLinearResponse.the_impulse_response_coefficient_is_an_actual_amplitude_derivative),
  (``PhysicsLogicConsumer.FluidCorrelations.ViscosityTransportReuse.the_library_composes_the_two_viscosity_dependent_spectra,
    ``PhysicsLogic.Framework.ObservableScaleTransport.Data.exact_agreements_compose_on_an_inhabited_transformed_domain),
  (``PhysicsLogicConsumer.FluidCorrelations.ViscosityTransportReuse.the_library_retains_zero_residual_for_the_coupled_readout,
    ``PhysicsLogic.Framework.ObservableScaleTransport.Data.exact_agreement_has_zero_residual),
  (``PhysicsLogicConsumer.FluidCorrelations.ScaleTransportReuse.the_library_composes_the_actual_gaussian_spectrum,
    ``PhysicsLogic.Framework.ObservableScaleTransport.Data.exact_agreements_compose_on_an_inhabited_transformed_domain),
  (``PhysicsLogicConsumer.FluidCorrelations.ScaleTransportReuse.the_library_identifies_the_exact_comparison_as_zero_residual,
    ``PhysicsLogic.Framework.ObservableScaleTransport.Data.exact_agreement_has_zero_residual),
  (``PhysicsLogicConsumer.FluidCorrelations.ScaleTransportReuse.the_library_amplifies_the_intermediate_readout_error,
    ``PhysicsLogic.Framework.ObservableScaleTransport.Data.residual_bounds_compose_with_the_first_readout_amplification),
  (``PhysicsLogicConsumer.FluidCorrelations.ScaleTransportReuse.the_library_bounds_the_original_spectral_query,
    ``PhysicsLogic.Framework.ObservableScaleTransport.Data.composed_residual_controls_each_admissible_original_query),
  (``PhysicsLogicConsumer.CoarseGraining.MarkovDecimation.the_library_composes_two_actual_Ising_decimations,
    ``PhysicsLogic.Framework.ObservableScaleTransport.Data.exact_agreements_compose_on_an_inhabited_transformed_domain),
  (``PhysicsLogicConsumer.CoarseGraining.MarkovDecimation.LimitingRegime.the_library_excludes_interchanging_decimation_and_alignment,
    ``PhysicsLogic.Paradigm.OrderedLimits.ObservableLimitFamily.actual_noncommutation_excludes_commutation),
  (``PhysicsLogicConsumer.ControlledApproximation.the_library_accumulates_both_phase_errors,
    ``PhysicsLogic.Paradigm.ScaleAndRegime.controlled_approximations_compose_with_an_explicit_accuracy_rule),
  (``PhysicsLogicConsumer.NuclearScattering.ReadoutStability.a_constant_inverse_amplitude_shift_has_exact_uniform_phase_error,
    ``PhysicsLogic.Framework.ElasticSWave.controlled_phase_approximation_iff_nonempty_sector_and_uniform_error),
  (``PhysicsLogicConsumer.NuclearScattering.ReadoutStability.uniform_phase_control_and_unitarity_do_not_give_uniform_amplitude_control,
    ``PhysicsLogic.Framework.ElasticSWave.controlled_amplitude_approximation_iff_nonempty_sector_and_uniform_error),
  (``PhysicsLogicConsumer.NuclearScattering.ReadoutStability.a_positive_momentum_floor_restores_uniform_amplitude_convergence,
    ``PhysicsLogic.Framework.ElasticSWave.controlled_phase_error_bounds_amplitude_error),
  (``PhysicsLogicConsumer.NuclearScattering.ReadoutStability.every_fixed_positive_momentum_has_amplitude_convergence,
    ``PhysicsLogic.Framework.ElasticSWave.controlled_phase_error_bounds_amplitude_error),
  (``PhysicsLogicConsumer.NuclearScattering.ReadoutStability.large_phase_values_have_small_amplitude_separation,
    ``PhysicsLogic.Framework.ElasticSWave.phase_difference_gives_exact_amplitude_distance),
  (``PhysicsLogicConsumer.NuclearScattering.ReadoutStability.exact_unitarity_and_a_positive_momentum_floor_do_not_control_inverse_recovery,
    ``PhysicsLogic.Framework.ElasticSWave.controlled_amplitude_approximation_iff_nonempty_sector_and_uniform_error),
  (``PhysicsLogicConsumer.NuclearScattering.ReadoutStability.bounded_phase_values_on_a_fixed_band_allow_stable_inverse_recovery,
    ``PhysicsLogic.Framework.ElasticSWave.controlled_amplitude_approximation_recovers_the_phase),
  (``PhysicsLogicConsumer.NuclearScattering.the_real_phase_formula_supplies_both_unitarity_readouts,
    ``PhysicsLogic.Framework.ElasticSWave.nonvacuous_elastic_s_wave_iff_explicit_amplitude),
  (``PhysicsLogicConsumer.NuclearScattering.the_real_phase_formula_supplies_both_unitarity_readouts,
    ``PhysicsLogic.Framework.ElasticSWave.nonvacuous_elastic_s_wave_has_unitarity_and_optical_theorem),
  (``PhysicsLogicConsumer.NuclearScattering.zero_contact_is_unitary_but_outside_the_finite_inverse_range_chart,
    ``PhysicsLogic.Framework.ElasticSWave.denominator_ne_zero_of_positive_momentum),
  (``PhysicsLogicConsumer.NuclearScattering.the_bubble_amplitude_needs_the_source_s_matrix_normalization,
    ``PhysicsLogic.Framework.ElasticSWave.real_contact_amplitude_is_elastic_unitary),
  (``PhysicsLogicConsumer.ControlledApproximation.the_library_transfers_the_accumulated_error_to_amplitudes,
    ``PhysicsLogic.Framework.ElasticSWave.two_phase_approximations_give_a_combined_amplitude_error),
  (``PhysicsLogicConsumer.ControlledApproximation.the_composed_comparison_has_actual_unitary_amplitudes,
    ``PhysicsLogic.Framework.ElasticSWave.controlled_phase_approximation_contains_actual_elastic_scattering),
  (``PhysicsLogicConsumer.ControlledApproximation.an_active_single_momentum_inherits_the_bound,
    ``PhysicsLogic.Paradigm.ScaleAndRegime.controlled_approximation_restricts_to_an_active_sector),
  (``PhysicsLogicConsumer.ControlledApproximation.the_library_bounds_the_error_at_each_selected_positive_momentum,
    ``PhysicsLogic.Framework.ElasticSWave.controlled_phase_error_bounds_amplitude_error),
  (``PhysicsLogicConsumer.ControlledApproximation.positive_momentum_and_unitarity_do_not_bound_error_amplification,
    ``PhysicsLogic.Framework.ElasticSWave.real_effective_range_function_realizes_elastic_scattering),
  (``PhysicsLogicConsumer.CoarseGraining.the_library_normalizes_the_microscopic_star_law,
    ``PhysicsLogic.Framework.FiniteCanonicalData.finite_canonical_probability_law_is_normalized),
  (``PhysicsLogicConsumer.CoarseGraining.the_marginal_is_normalized,
    ``PhysicsLogic.Framework.FiniteCanonicalData.finite_canonical_probabilities_sum_to_one),
  (``PhysicsLogicConsumer.CoarseGraining.the_library_retains_every_outer_observable_law,
    ``PhysicsLogic.Framework.StatisticalCoarseGraining.Data.actual_probability_projection_realizes_nonvacuous_retained_predictions),
  (``PhysicsLogicConsumer.CoarseGraining.the_library_matches_the_computed_microscopic_pair_mean,
    ``PhysicsLogic.Framework.StatisticalCoarseGraining.Data.a_nonvacuous_integrable_retained_observable_has_the_microscopic_mean),
  (``PhysicsLogicConsumer.CoarseGraining.positive_probability_hidden_spins_cannot_be_reconstructed,
    ``PhysicsLogic.Framework.StatisticalCoarseGraining.Data.different_values_on_one_retained_fiber_obstruct_observable_reconstruction),
  (``PhysicsLogicConsumer.CoarseGraining.positive_probability_hidden_spins_cannot_be_reconstructed_almost_surely,
    ``PhysicsLogic.Framework.StatisticalCoarseGraining.Data.non_null_fiber_values_obstruct_almost_sure_observable_reconstruction),
  (``PhysicsLogicConsumer.CoarseGraining.a_null_fiber_disagreement_blocks_only_pointwise_recovery,
    ``PhysicsLogic.Framework.StatisticalCoarseGraining.Data.different_values_on_one_retained_fiber_obstruct_observable_reconstruction),
  (``PhysicsLogicConsumer.CoarseGraining.positive_probability_hidden_spins_cannot_be_reconstructed,
    ``PhysicsLogic.Framework.FiniteCanonicalData.finite_canonical_probability_is_positive),
  (``PhysicsLogicConsumer.CoarseGraining.two_step_reduction_preserves_the_actual_magnetization_law,
    ``PhysicsLogic.Framework.StatisticalCoarseGraining.Data.successive_eliminations_have_the_composed_retained_law),
  (``PhysicsLogicConsumer.CoarseGraining.invertible_rescaling_preserves_the_correctly_reexpressed_magnetization_law,
    ``PhysicsLogic.Framework.StatisticalCoarseGraining.Data.an_invertible_reexpression_preserves_the_reexpressed_observable_law),
  (``PhysicsLogicConsumer.CoarseGraining.the_exact_coarse_law_is_not_closed_in_the_pairwise_gibbs_family,
    ``PhysicsLogic.Framework.FiniteCanonicalData.finite_canonical_log_probability_is_energy_and_partition),
  (``PhysicsLogicConsumer.CoarseGraining.the_mapped_pmf_has_the_computed_marginal,
    ``PhysicsLogic.Framework.FiniteCanonicalData.finite_canonical_probability_is_positive),
  (``PhysicsLogicConsumer.StatMech.gibbs_pmf_toReal,
    ``PhysicsLogic.Framework.FiniteCanonicalData.finite_canonical_pmf_has_the_computed_probability),
  (``PhysicsLogicConsumer.Supersymmetry.library_derives_a_nonvacuous_normalizable_vacuum,
    ``PhysicsLogic.Framework.SupersymmetricOperator.ChargeEnergyData.actual_normalized_kernel_realizes_nonvacuous_unbroken_vacuum),
  (``PhysicsLogicConsumer.Supersymmetry.library_derives_a_nonvacuous_positive_energy_pair,
    ``PhysicsLogic.Framework.SupersymmetricOperator.GradedChargeData.actual_supersymmetry_algebra_derives_a_nonvacuous_positive_pair),
  (``PhysicsLogicConsumer.Supersymmetry.library_derives_a_nonvacuous_positive_energy_pair,
    ``PhysicsLogic.Framework.SupersymmetricOperator.GradedChargeData.actual_positive_energy_pair_has_the_source_charge_actions),
  (``PhysicsLogicConsumer.Supersymmetry.the_library_pairing_is_involutive_and_orthogonal,
    ``PhysicsLogic.Framework.SupersymmetricOperator.GradedChargeData.applying_the_normalized_positive_energy_partner_twice_recovers_the_state),
  (``PhysicsLogicConsumer.Supersymmetry.the_library_pairing_is_involutive_and_orthogonal,
    ``PhysicsLogic.Framework.SupersymmetricOperator.GradedChargeData.actual_opposite_grading_states_are_orthogonal),
  (``PhysicsLogicConsumer.Supersymmetry.an_energy_origin_shift_does_not_preserve_the_supersymmetric_zero_energy_criterion,
    ``PhysicsLogic.Framework.SupersymmetricOperator.ChargeEnergyData.changing_the_energy_origin_changes_the_actual_expectation),
  (``PhysicsLogicConsumer.Supersymmetry.invariant_vacuum_has_zero_anticommutator_expectation_for_every_operator,
    ``PhysicsLogic.Framework.SupersymmetricOperator.ChargeEnergyData.an_annihilated_state_has_zero_charge_anticommutator_expectation),
  (``PhysicsLogicConsumer.Supersymmetry.the_complete_basis_has_computed_energies_and_parities,
    ``PhysicsLogic.Framework.SupersymmetricOperator.GradedChargeData.actual_eigenstate_has_its_energy_expectation),
  (``PhysicsLogicConsumer.Supersymmetry.the_positive_only_system_has_no_normalizable_supersymmetric_state,
    ``PhysicsLogic.Framework.SupersymmetricOperator.ChargeEnergyData.zero_energy_iff_every_actual_charge_annihilates),
  (``PhysicsLogicConsumer.Supersymmetry.the_library_derives_positive_ground_energy_for_the_zero_index_broken_system,
    ``PhysicsLogic.Framework.SupersymmetricOperator.ChargeEnergyData.absence_of_a_supersymmetric_state_gives_positive_attained_ground_energy),
  (``PhysicsLogicConsumer.Supersymmetry.a_zero_computed_index_does_not_decide_whether_a_normalizable_vacuum_exists,
    ``PhysicsLogic.Framework.SupersymmetricOperator.ChargeEnergyData.actual_normalized_kernel_realizes_nonvacuous_unbroken_vacuum),
  (``PhysicsLogicConsumer.Supersymmetry.ScalarDifferential.the_gaussian_client_has_an_actual_normalizable_charge_zero_mode,
    ``PhysicsLogic.Framework.ScalarSupersymmetricZeroMode.Data.an_integrable_profile_is_an_actual_nonzero_normalizable_zero_mode),
  (``PhysicsLogicConsumer.Supersymmetry.ScalarDifferential.the_gaussian_client_positive_profile_is_obstructed,
    ``PhysicsLogic.Framework.ScalarSupersymmetricZeroMode.Data.a_nondecaying_positive_tail_excludes_normalizable_zero_modes),
  (``PhysicsLogicConsumer.Supersymmetry.ScalarDifferential.the_gaussian_client_kernel_dimensions_and_index_are_computed,
    ``PhysicsLogic.Framework.ScalarSupersymmetricZeroMode.Data.an_integrable_profile_has_exactly_one_normalizable_zero_mode),
  (``PhysicsLogicConsumer.Supersymmetry.ScalarDifferential.the_gaussian_client_kernel_dimensions_and_index_are_computed,
    ``PhysicsLogic.Framework.ScalarSupersymmetricZeroMode.Data.an_obstruction_has_no_normalizable_zero_modes),
  (``PhysicsLogicConsumer.Supersymmetry.ScalarDifferential.the_two_well_positive_profile_is_not_square_integrable,
    ``PhysicsLogic.Framework.ScalarSupersymmetricZeroMode.Data.a_nondecaying_positive_tail_excludes_normalizable_zero_modes),
  (``PhysicsLogicConsumer.Supersymmetry.ScalarDifferential.the_two_well_negative_profile_is_not_square_integrable,
    ``PhysicsLogic.Framework.ScalarSupersymmetricZeroMode.Data.a_nondecaying_negative_tail_excludes_normalizable_zero_modes),
  (``PhysicsLogicConsumer.Supersymmetry.ScalarDifferential.the_two_well_actual_normalizable_kernels_are_zero,
    ``PhysicsLogic.Framework.ScalarSupersymmetricZeroMode.Data.an_obstruction_makes_the_actual_normalizable_kernel_zero),
  (``PhysicsLogicConsumer.Supersymmetry.ScalarDifferential.the_zero_mode_equation_remembers_the_clients_planck_constant,
    ``PhysicsLogic.Framework.ScalarSupersymmetricZeroMode.Data.the_exponential_profile_solves_the_actual_zero_mode_equation),
  (``PhysicsLogicConsumer.Supersymmetry.ScalarDifferential.the_client_zero_mode_pair_is_annihilated_by_the_actual_charge,
    ``PhysicsLogic.Framework.ScalarSupersymmetricZeroMode.Data.two_actual_zero_mode_equations_annihilate_the_first_order_charge),
  (``PhysicsLogicConsumer.Supersymmetry.ScalarDifferential.the_actual_first_order_charge_remains_odd_for_both_clients,
    ``PhysicsLogic.Framework.ScalarSupersymmetricZeroMode.Data.the_actual_first_order_charge_reverses_the_grading),
  (``PhysicsLogicConsumer.Supersymmetry.ScalarDifferential.a_nonzero_formal_solution_does_not_supply_a_physical_normalizable_state,
    ``PhysicsLogic.Framework.ScalarSupersymmetricZeroMode.Data.a_nonintegrable_profile_excludes_every_nonzero_normalizable_solution),
  (``PhysicsLogicConsumer.CondensedMatter.MajoranaWire.independently_selected_ends_are_nonvacuous,
    ``PhysicsLogic.Framework.FermionicModeAlgebra.MajoranaPair.canonical_pair_is_nonvacuous),
  (``PhysicsLogicConsumer.CondensedMatter.MajoranaWire.actual_end_coupling_has_two_nonempty_parity_sectors,
    ``PhysicsLogic.Framework.FiniteMajoranaParity.Data.canonical_majorana_pair_realizes_nonvacuous_effective_parity),
  (``PhysicsLogicConsumer.CondensedMatter.MajoranaWire.finite_end_coupling_has_nonzero_exact_operator_residuals,
    ``PhysicsLogic.Framework.FermionicModeAlgebra.MajoranaPair.effective_pair_coupling_has_actual_majorana_residuals),
  (``PhysicsLogicConsumer.CondensedMatter.MajoranaWire.finite_coupling_is_parity_preserving_but_not_an_exact_zero_mode,
    ``PhysicsLogic.Framework.FermionicModeAlgebra.nonzero_effective_splitting_prevents_exact_majorana_zero_modes),
  (``PhysicsLogicConsumer.CondensedMatter.MajoranaWire.parity_preserving_perturbations_have_zero_opposite_sector_blocks,
    ``PhysicsLogic.Framework.FiniteMajoranaParity.Data.parity_preserving_perturbation_has_no_cross_sector_block),
  (``PhysicsLogicConsumer.CondensedMatter.MajoranaWire.independent_complex_spin_combination_is_an_actual_normalized_majorana,
    ``PhysicsLogic.Framework.FermionicModeAlgebra.Family.conjugate_nonzero_weights_realize_an_actual_majorana),
  (``PhysicsLogicConsumer.CondensedMatter.MajoranaWire.independent_complex_spin_combination_is_an_actual_normalized_majorana,
    ``PhysicsLogic.Framework.FermionicModeAlgebra.Family.actual_majorana_square_has_its_own_normalization),
  (``PhysicsLogicConsumer.CondensedMatter.MajoranaWire.an_imaginary_rephase_changes_literal_self_conjugacy_but_can_be_undone,
    ``PhysicsLogic.Framework.FermionicModeAlgebra.imaginary_rephasing_is_not_literal_self_conjugacy),
  (``PhysicsLogicConsumer.CondensedMatter.MajoranaWire.unit_coefficient_weight_does_not_replace_actual_conjugation,
    ``PhysicsLogic.Framework.FermionicModeAlgebra.Family.actual_self_conjugacy_iff_conjugate_coefficients),
  (``PhysicsLogicConsumer.CondensedMatter.MajoranaWire.unit_coefficient_weight_does_not_replace_actual_conjugation,
    ``PhysicsLogic.Framework.FermionicModeAlgebra.Family.nonzero_canonical_coefficient_gives_nonzero_operator),
  (``PhysicsLogicConsumer.StatMech.partition_pos,
    ``PhysicsLogic.Framework.FiniteCanonicalData.finite_partition_is_positive),
  (``PhysicsLogicConsumer.StatMech.gibbs_weight_pos,
    ``PhysicsLogic.Framework.FiniteCanonicalData.finite_canonical_probability_is_positive),
  (``PhysicsLogicConsumer.StatMech.gibbs_weights_sum_one,
    ``PhysicsLogic.Framework.FiniteCanonicalData.finite_canonical_probabilities_sum_to_one),
  (``PhysicsLogicConsumer.StatMech.DrivenProtocol.actual_protocol_is_gibbs_preserving,
    ``PhysicsLogic.Framework.FiniteDrivenWork.Data.actual_detailed_balance_steps_derive_gibbs_preserving_driving),
  (``PhysicsLogicConsumer.StatMech.DrivenProtocol.actual_three_event_protocol_realizes_forward_and_reverse_work,
    ``PhysicsLogic.Framework.FiniteDrivenWork.Data.actual_canonical_schedules_realize_nonvacuous_forward_reverse_work),
  (``PhysicsLogicConsumer.StatMech.DrivenProtocol.actual_three_event_exponential_average,
    ``PhysicsLogic.Framework.FiniteDrivenWork.Data.gibbs_preserving_steps_derive_the_actual_partition_ratio),
  (``PhysicsLogicConsumer.StatMech.DrivenProtocol.actual_three_event_mean_work_bound,
    ``PhysicsLogic.Framework.FiniteDrivenWork.Data.gibbs_preserving_driving_derives_mean_work_bound),
  (``PhysicsLogicConsumer.StatMech.DrivenProtocol.actual_free_energy_difference,
    ``PhysicsLogic.Framework.FiniteDrivenWork.Data.gibbs_preserving_driving_derives_exponential_work_identity),
  (``PhysicsLogicConsumer.StatMech.DrivenProtocol.actual_heat_exchange_retains_the_first_law,
    ``PhysicsLogic.Framework.FiniteDrivenWork.Data.path_work_and_heat_give_the_actual_endpoint_energy_change),
  (``PhysicsLogicConsumer.StatMech.DrivenProtocol.actual_forward_reverse_work_weights,
    ``PhysicsLogic.Framework.FiniteDrivenWork.Data.canonical_preparations_and_detailed_balance_derive_path_work_ratio),
  (``PhysicsLogicConsumer.StatMech.DrivenProtocol.reverse_experiment_prepared_from_the_actual_final_law_is_normalized,
    ``PhysicsLogic.Framework.FiniteDrivenWork.Data.stochastic_path_sum_is_the_initial_mass),
  (``PhysicsLogicConsumer.StatMech.DrivenProtocol.reverse_experiment_prepared_from_the_actual_final_law_is_normalized,
    ``PhysicsLogic.Framework.FiniteDrivenWork.Data.actual_terminal_marginal_is_a_normalized_probability_law),
  (``PhysicsLogicConsumer.StatMech.DrivenProtocol.actual_endpoint_entropy_retains_the_nonequilibrium_correction,
    ``PhysicsLogic.Framework.FiniteDrivenWork.Data.a_positive_weight_path_has_a_genuine_endpoint_entropy_domain),
  (``PhysicsLogicConsumer.StatMech.DrivenProtocol.actual_endpoint_entropy_retains_the_nonequilibrium_correction,
    ``PhysicsLogic.Framework.FiniteDrivenWork.Data.actual_endpoint_entropy_has_a_final_nonequilibrium_correction),
  (``PhysicsLogicConsumer.FluidCorrelations.BoundaryLayerReuse.library_recognizes_nonzero_local_diffusion,
    ``PhysicsLogic.Framework.BoundaryLayerFieldReduction.Data.primitive_balances_and_bounds_realize_nonvacuous_controlled_reduction),
  (``PhysicsLogicConsumer.FluidCorrelations.SuctionLayerReuse.the_library_recovers_the_exact_retained_suction_equation,
    ``PhysicsLogic.Framework.BoundaryLayerFieldReduction.Data.full_and_retained_residuals_differ_by_actual_discarded_terms),
  (``PhysicsLogicConsumer.FluidCorrelations.SuctionLayerReuse.the_library_retains_nonzero_viscous_suction_balance,
    ``PhysicsLogic.Framework.BoundaryLayerFieldReduction.Data.primitive_balances_and_bounds_realize_nonvacuous_controlled_reduction),
  (``PhysicsLogicConsumer.FluidCorrelations.BoundaryLayerReuse.library_computes_actual_discarded_term_residual,
    ``PhysicsLogic.Framework.BoundaryLayerFieldReduction.Data.full_and_retained_residuals_differ_by_actual_discarded_terms),
  (``PhysicsLogicConsumer.FluidCorrelations.BoundaryLayerReuse.library_retains_the_actual_unsteady_acceleration,
    ``PhysicsLogic.Framework.BoundaryLayerFieldReduction.Data.retained_equation_keeps_the_actual_time_acceleration),
  (``PhysicsLogicConsumer.FluidCorrelations.BoundaryLayerReuse.library_source_order_budget_retains_the_outer_calibration_error,
    ``PhysicsLogic.Framework.BoundaryLayerFieldReduction.Data.source_order_and_longitudinal_control_bound_the_retained_equation),
  (``PhysicsLogicConsumer.FluidCorrelations.BoundaryLayerReuse.library_keeps_curvature_pressure_variation_at_first_order,
    ``PhysicsLogic.Framework.BoundaryLayerFieldReduction.Data.source_normal_balance_bounds_pressure_variation_across_the_layer),
  (``PhysicsLogicConsumer.FluidCorrelations.BoundaryLayerReuse.library_vanishing_boundary_calibration_forces_vanishing_actual_residuals,
    ``PhysicsLogic.Framework.BoundaryLayerFieldReduction.vanishing_discarded_term_budgets_force_vanishing_residuals),
  (``PhysicsLogicConsumer.FluidCorrelations.BoundaryLayerReuse.library_recovers_the_outer_acceleration_form_under_its_actual_euler_input,
    ``PhysicsLogic.Framework.BoundaryLayerFieldReduction.Data.outer_euler_input_equates_the_two_retained_momentum_forms),
  (``PhysicsLogicConsumer.FluidCorrelations.ChannelWallReuse.library_retains_the_same_dynamic_viscosity_and_wall_gradient,
    ``PhysicsLogic.Framework.PlanarWallTraction.Data.actual_wall_traction_is_viscosity_times_the_one_sided_velocity_gradient),
  (``PhysicsLogicConsumer.FluidCorrelations.ChannelWallReuse.both_actual_wall_forces_are_nonvacuous,
    ``PhysicsLogic.Framework.PlanarWallTraction.Data.equal_face_loading_justifies_doubling),
  (``PhysicsLogicConsumer.FluidCorrelations.ChannelWallReuse.library_rejects_doubling_the_lower_wall_load,
    ``PhysicsLogic.Framework.PlanarWallTraction.Data.doubling_requires_the_same_force_on_the_other_face),
  (``PhysicsLogicConsumer.FluidCorrelations.ChannelWallReuse.library_distinguishes_one_wall_from_two_identical_walls,
    ``PhysicsLogic.Framework.PlanarWallTraction.Data.positive_drag_on_one_face_is_not_the_two_face_drag),
  (``PhysicsLogicConsumer.ClassicalDynamics.CanonicalReuse.actual_partial_derivative_vanishes_along_the_constraint_surface,
    ``PhysicsLogic.Framework.CanonicalConstraintAction.CanonicalPair.polynomial_partial_is_actual_derivative),
  (``PhysicsLogicConsumer.ClassicalDynamics.CanonicalReuse.actual_surface_has_local_first_order_constraint_representatives,
    ``PhysicsLogic.Framework.CanonicalConstraintAction.CanonicalPair.first_order_equality_is_value_and_partials),
  (``PhysicsLogicConsumer.ClassicalDynamics.CanonicalReuse.library_derives_first_class_bracket_closure,
    ``PhysicsLogic.Framework.CanonicalConstraintAction.Data.complete_constraints_close_first_class_brackets),
  (``PhysicsLogicConsumer.ClassicalDynamics.CanonicalReuse.library_retains_nonzero_canonical_generator_action,
    ``PhysicsLogic.Framework.CanonicalConstraintAction.Data.complete_first_class_constraints_realize_physical_closure),
  (``PhysicsLogicConsumer.ClassicalDynamics.CanonicalReuse.library_bracket_action_is_the_transformation_commutator,
    ``PhysicsLogic.Framework.CanonicalConstraintAction.Data.poisson_action_of_bracket_is_commutator),
  (``PhysicsLogicConsumer.ClassicalDynamics.CanonicalReuse.library_quadratic_extension_preserves_the_same_canonical_action,
    ``PhysicsLogic.Framework.CanonicalConstraintAction.Data.quadratic_constraint_terms_preserve_first_order_action),
  (``PhysicsLogicConsumer.ClassicalDynamics.CanonicalReuse.library_canonical_bracket_is_an_actual_coordinate_formula,
    ``PhysicsLogic.Framework.CanonicalConstraintAction.CanonicalPair.bracket_is_actual_canonical_coordinate_formula),
  (``PhysicsLogicConsumer.QuantumInformation.ReferenceReuse.library_recovers_the_normalized_reference_input,
    ``PhysicsLogic.Framework.CoherentQuantumRecovery.Experiment.coherent_recovery_restores_every_reference_input),
  (``PhysicsLogicConsumer.QuantumInformation.ReferenceReuse.library_restores_the_whole_reference_density,
    ``PhysicsLogic.Framework.CoherentQuantumRecovery.Model.recovery_with_reference_restores_joint_density),
  (``PhysicsLogicConsumer.QuantumInformation.ReferenceReuse.library_composes_recovery_with_reference_entanglement,
    ``PhysicsLogic.Framework.CoherentQuantumRecovery.Experiment.coherent_recovery_preserves_calibrated_reference_entanglement),
  (``PhysicsLogicConsumer.QuantumInformation.ReferenceReuse.recovered_reference_and_code_are_not_separable,
    ``PhysicsLogic.Framework.CoherentQuantumRecovery.Model.entanglement_preserving_recovery_retains_nonseparable_joint_density),
  (``PhysicsLogicConsumer.QuantumInformation.ReferenceReuse.library_preserves_every_joint_observable,
    ``PhysicsLogic.Framework.CoherentQuantumRecovery.Model.reference_recovery_preserves_all_joint_expectations),
  (``PhysicsLogicConsumer.QuantumInformation.ReferenceReuse.recorded_mixture_is_admissible,
    ``PhysicsLogic.Framework.CoherentQuantumRecovery.pure_density_is_density),
  (``PhysicsLogicConsumer.QuantumInformation.ReferenceReuse.logical_recorded_density_is_normalized,
    ``PhysicsLogic.Framework.FiniteQuantumState.ProductMixture.isDensity),
  (``PhysicsLogicConsumer.QuantumInformation.ReferenceReuse.initial_reference_state_is_not_separable,
    ``PhysicsLogic.Framework.FiniteQuantumState.positive_pptWitness_not_separable),
  (``PhysicsLogicConsumer.CosmicVariance.FieldReadoutReuse.finite_patch_fields_are_regular_centered_and_wick,
    ``PhysicsLogic.Framework.QuadraticFieldSampling.Readout.counting_observation_mass),
  (``PhysicsLogicConsumer.CosmicVariance.FieldReadoutReuse.actual_equal_area_patches_have_different_correlation_norms,
    ``PhysicsLogic.Framework.QuadraticFieldSampling.Readout.counting_diagonal_correlation_squared_mass),
  (``PhysicsLogicConsumer.CosmicVariance.FieldReadoutReuse.independent_finite_patch_is_nonvacuous,
    ``PhysicsLogic.Framework.QuadraticFieldSampling.Readout.counting_positive_diagonal_exhibits_nonvacuous_sampling),
  (``PhysicsLogicConsumer.CosmicVariance.FieldReadoutReuse.library_computes_each_patch_mean,
    ``PhysicsLogic.Framework.QuadraticFieldSampling.Readout.uniform_diagonal_correlation_determines_estimator_mean),
  (``PhysicsLogicConsumer.CosmicVariance.FieldReadoutReuse.library_computes_each_patch_variance,
    ``PhysicsLogic.Framework.QuadraticFieldSampling.Readout.wick_variance_is_the_squared_correlation_integral),
  (``PhysicsLogicConsumer.NuclearScattering.SquareWell.exterior_has_derivative,
    ``PhysicsLogic.Framework.NeutralBoundState.decaying_factor_has_derivative),
  (``PhysicsLogicConsumer.NuclearScattering.SquareWell.matched_wave_is_regular_nonzero_and_decaying,
    ``PhysicsLogic.Framework.NeutralBoundState.positive_inverse_length_gives_decay),
  (``PhysicsLogicConsumer.NuclearScattering.SquareWell.library_recognizes_the_matched_bound_mode,
    ``PhysicsLogic.Framework.NeutralBoundState.RadialMode.no_growing_component_realizes_bound_mode),
  (``PhysicsLogicConsumer.NuclearScattering.SquareWell.comparison_mode_is_the_exterior_not_the_regular_interior,
    ``PhysicsLogic.Framework.NeutralBoundState.RadialMode.nonvacuous_bound_mode_is_not_regular_at_origin),
  (``PhysicsLogicConsumer.NuclearScattering.SquareWell.library_computes_the_actual_exterior_radial_weight,
    ``PhysicsLogic.Framework.NeutralBoundState.RadialMode.bound_mode_exterior_weight_is_computed),
  (``PhysicsLogicConsumer.NuclearScattering.SquareWell.library_computes_the_actual_exterior_radial_weight,
    ``PhysicsLogic.Framework.NeutralBoundState.RadialMode.bound_mode_has_integrable_exterior_weight),
  (``PhysicsLogicConsumer.NuclearScattering.SquareWell.library_computes_the_actual_exterior_radial_weight,
    ``PhysicsLogic.Framework.NeutralBoundState.RadialMode.bound_mode_exterior_weight_is_positive),
  (``PhysicsLogicConsumer.NuclearScattering.ShapeRemainder.real_momentum_data_retain_elastic_unitarity,
    ``PhysicsLogic.Framework.ElasticSWave.s_matrix_is_outgoing_incoming_ratio),
  (``PhysicsLogicConsumer.NuclearScattering.ShapeRemainder.library_exposes_and_bounds_the_nonzero_range_error,
    ``PhysicsLogic.Framework.NeutralBoundState.range_extraction_error_is_scaled_binding_residual),
  (``PhysicsLogicConsumer.NuclearScattering.ShapeRemainder.library_exposes_and_bounds_the_nonzero_range_error,
    ``PhysicsLogic.Framework.NeutralBoundState.controlled_binding_residual_bounds_range_error),
  (``PhysicsLogicConsumer.ThermalNoise.FixedFrequencyFamily.library_nonzero_lines_retain_the_full_canonical_response,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.TransitionSlice.canonical_response_equals_relaxation_at_nonzero_gap),
  (``PhysicsLogicConsumer.ThermalNoise.StaticNumberObservable.library_zero_gap_canonical_response_is_nonvacuous,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.TransitionSlice.actual_ordered_weight_gives_nonvacuous_canonical_response),
  (``PhysicsLogicConsumer.ThermalNoise.StaticNumberObservable.library_zero_gap_response_retains_full_static_weight,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.TransitionSlice.canonical_response_at_zero_retains_invariant_weight),
  (``PhysicsLogicConsumer.ThermalNoise.StaticNumberObservable.library_zero_gap_symmetrized_identity_uses_the_full_response,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.TransitionSlice.symmetrized_spectrum_is_weighted_full_canonical_response),
  (``PhysicsLogicConsumer.ThermalNoise.StaticNumberObservable.library_isolation_removes_the_invariant_response,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.SpectralFamily.canonical_response_splits_zero_and_nonzero_gaps),
  (``PhysicsLogicConsumer.ThermalNoise.StaticNumberObservable.library_rejects_an_ordinary_density_for_the_static_atom,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.SpectralFamily.ordinary_energy_gap_density_has_no_atoms),
  (``PhysicsLogicConsumer.ThermalNoise.FixedFrequencyFamily.library_identifies_the_two_countably_additive_spectral_measures,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.BandResolution.reconstruction_identifies_full_spectral_measures),
  (``PhysicsLogicConsumer.ThermalNoise.FixedFrequencyFamily.library_derives_the_exact_thermal_relation_on_each_nonzero_band,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.BandResolution.canonical_band_noise_is_weighted_resolved_relaxation),
  (``PhysicsLogicConsumer.ThermalNoise.FixedFrequencyFamily.library_positive_band_has_nonzero_canonical_weight,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.BandResolution.nonvacuous_band_has_nonzero_canonical_weight),
  (``PhysicsLogicConsumer.ThermalNoise.FixedFrequencyFamily.positive_band_relaxation_is_not_weighted_at_one_nominal_frequency,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.BandResolution.band_fdt_keeps_the_energy_factor_inside_the_integral),
  (``PhysicsLogicConsumer.ThermalNoise.FixedFrequencyFamily.library_uses_one_normalized_state_for_all_four_lines,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.SpectralFamily.common_system_has_one_canonical_law),
  (``PhysicsLogicConsumer.ThermalNoise.FixedFrequencyFamily.library_derives_fdt_at_both_signs_and_two_gap_magnitudes,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.SpectralFamily.fixed_system_fluctuation_dissipation),
  (``PhysicsLogicConsumer.ThermalNoise.FixedFrequencyFamily.library_selects_all_four_lines_with_one_time_evolution,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.TransitionSlice.negative_fourier_kernel_selects_the_energy_gap),
  (``PhysicsLogicConsumer.ThermalNoise.FixedFrequencyFamily.library_preserves_nonzero_spectra_under_invariant_subtraction,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.TransitionSlice.nonzero_spectra_survive_invariant_subtraction),
  (``PhysicsLogicConsumer.ThermalNoise.library_normalizes_the_actual_state_law,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.CanonicalEnsemble.canonical_law_is_probability),
  (``PhysicsLogicConsumer.ThermalNoise.independent_two_transition_noise_is_nonvacuous,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.TransitionSlice.positive_self_noise_is_nonvacuous),
  (``PhysicsLogicConsumer.ThermalNoise.library_derives_balanced_forward_reverse_spectra,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.TransitionSlice.canonical_spectral_detailed_balance),
  (``PhysicsLogicConsumer.ThermalNoise.library_recovers_quantum_noise_from_relaxation,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.TransitionSlice.canonical_symmetrized_fluctuation_dissipation),
  (``PhysicsLogicConsumer.ThermalNoise.library_compares_noise_and_dissipation,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.TransitionSlice.active_self_noise_has_thermal_sum_difference_ratio),
  (``PhysicsLogicConsumer.ThermalNoise.ImpedanceReadout.library_fdt_derives_the_independent_force_noise_normalization,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.TransitionSlice.canonical_symmetrized_fluctuation_dissipation),
  (``PhysicsLogicConsumer.ThermalNoise.RetardedFilter.the_library_establishes_the_computed_nonvacuous_retarded_response,
    ``PhysicsLogic.Paradigm.ResponseCausality.ResponseCausalityContext.retarded_kernel_representation_with_witness_realizes_retarded_response),
  (``PhysicsLogicConsumer.ThermalNoise.RetardedFilter.the_library_excludes_a_future_source_for_the_actual_response,
    ``PhysicsLogic.Paradigm.ResponseCausality.ResponseCausalityContext.retarded_response_excludes_future_dependence),
  (``PhysicsLogicConsumer.ThermalNoise.OperatorEvolution.the_library_recovers_the_unevolved_operator,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.CanonicalEnsemble.heisenberg_matrix_at_zero),
  (``PhysicsLogicConsumer.ThermalNoise.OperatorEvolution.the_library_composes_the_same_actual_operator,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.CanonicalEnsemble.heisenberg_matrix_time_composition),
  (``PhysicsLogicConsumer.ThermalNoise.OperatorEvolution.the_library_normalizes_the_actual_matrix_density,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.CanonicalEnsemble.normalized_density_integrates_to_one),
  (``PhysicsLogicConsumer.ThermalNoise.CanonicalTrace.the_library_identifies_the_actual_hamiltonian_exponential,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.CanonicalOperatorCorrelation.Finite.the_matrix_exponential_has_its_actual_energy_action),
  (``PhysicsLogicConsumer.ThermalNoise.CanonicalTrace.the_library_identifies_the_actual_partition_trace,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.CanonicalOperatorCorrelation.Finite.the_matrix_gibbs_trace_is_the_partition),
  (``PhysicsLogicConsumer.ThermalNoise.CanonicalTrace.the_library_certifies_the_same_operator_representation,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.CanonicalOperatorCorrelation.Finite.actual_finite_matrices_realize_the_common_hamiltonian_representation),
  (``PhysicsLogicConsumer.ThermalNoise.CanonicalTrace.the_library_uses_the_actual_matrix_density_for_every_observable,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.CanonicalOperatorCorrelation.Finite.the_normalized_operator_trace_uses_the_actual_gibbs_density),
  (``PhysicsLogicConsumer.ThermalNoise.CanonicalTrace.the_library_derives_the_actual_imaginary_time_trace,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.CanonicalOperatorCorrelation.Finite.the_finite_thermal_trace_has_the_actual_full_spectral_kernel),
  (``PhysicsLogicConsumer.ThermalNoise.CanonicalTrace.the_library_supplies_the_actual_imaginary_time_interchange,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.CanonicalOperatorCorrelation.Finite.finite_matrices_supply_the_actual_imaginary_time_interchange),
  (``PhysicsLogicConsumer.ThermalNoise.CanonicalTrace.the_full_imaginary_time_trace_has_its_independently_computed_origin,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.CanonicalOperatorCorrelation.Finite.finite_pair_integrals_are_the_actual_double_sums),
  (``PhysicsLogicConsumer.ThermalNoise.CanonicalTrace.the_library_exhibits_nonvacuous_independent_operator_correlation,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.CanonicalOperatorCorrelation.Operators.represented_operators_and_trace_domains_derive_a_nonvacuous_correlation),
  (``PhysicsLogicConsumer.FluidCorrelations.independent_two_dimensional_mode_is_nonvacuous,
    ``PhysicsLogic.Framework.IncompressibleVelocityCorrelationContext.selected_setup_transversality_and_calculation_realize_nonvacuous_incompressible_correlation),
  (``PhysicsLogicConsumer.FluidCorrelations.library_extracts_the_actual_two_dimensional_contraction,
    ``PhysicsLogic.Framework.IncompressibleVelocityCorrelationContext.nonvacuous_fourier_correlation_annihilates_the_actual_wave_vector),
  (``PhysicsLogicConsumer.FluidCorrelations.a_transverse_negative_matrix_rejects_covariance_semantics,
    ``PhysicsLogic.Framework.IncompressibleVelocityCorrelationContext.nonvacuous_incompressible_velocity_correlation_has_positive_semidefinite_tensor),
  (``PhysicsLogicConsumer.FluidCorrelations.independent_radial_profile_is_nonvacuous,
    ``PhysicsLogic.Framework.IncompressibleVelocityCorrelationContext.selected_setup_transversality_and_calculation_realize_nonvacuous_incompressible_correlation),
  (``PhysicsLogicConsumer.FluidCorrelations.library_extracts_the_actual_radial_derivative,
    ``PhysicsLogic.Framework.IncompressibleVelocityCorrelationContext.nonvacuous_radial_correlation_has_an_actual_derivative),
  (``PhysicsLogicConsumer.StatMech.finite_quench_exponential_average,
    ``PhysicsLogic.Framework.ClassicalWorkEnsemble.finite_pmf_expectation),
  (``PhysicsLogicConsumer.StatMech.three_state_quench_separates_average_from_each_run,
    ``PhysicsLogic.Framework.ClassicalWorkEnsemble.exponential_identity_implies_mean_work_bound),
  (``PhysicsLogicConsumer.ClassicalDynamics.unstable_mode_is_nonvacuous_without_ontic_branching,
    ``PhysicsLogic.Framework.FinitePrecisionTrajectoryModel.finite_resolution_divergence_realizes_structural_prediction_failure),
  (``PhysicsLogicConsumer.ClassicalDynamics.unstable_mode_is_nonvacuous_without_ontic_branching,
    ``PhysicsLogic.Paradigm.Dynamics.unique_forward_evolution_excludes_branching_at),
  (``PhysicsLogicConsumer.BellLocality.bell_source_logic,
    ``PhysicsLogic.Framework.DeterministicLocalResponse.established_response_exhibits_nonvacuous_local_factorization),
  (``PhysicsLogicConsumer.BellLocality.bell_source_logic,
    ``PhysicsLogic.Framework.DeterministicLocalResponse.established_response_has_no_signalling_support),
  (``PhysicsLogicConsumer.BellLocality.Averaging.every_hidden_state_violates_pointwise_no_signalling,
    ``PhysicsLogic.Framework.DeterministicLocalResponse.deterministic_support_no_signalling_iff_remote_setting_independence),
  (``PhysicsLogicConsumer.BellLocality.Averaging.a_common_joint_law_does_not_identify_locality_of_the_response_model,
    ``PhysicsLogic.Framework.DeterministicLocalResponse.admits_local_factorization_iff_pointwise_no_signalling),
  (``PhysicsLogicConsumer.QuantumInformation.UnclassifiedOrbitReuse.the_library_retains_neutral_movement_without_classifying_it,
    ``PhysicsLogic.Philosophy.Symmetry.selected_law_movement_retains_unclassified_admissible_movement),
  (``PhysicsLogicConsumer.QuantumInformation.UnclassifiedOrbitReuse.the_library_confirms_both_density_interpretations,
    ``PhysicsLogic.Framework.CoherentQuantumRecovery.pure_density_is_density),
  (``PhysicsLogicConsumer.ClassicalDynamics.SymmetryRoleReuse.the_library_derives_mechanical_momentum_conservation_for_free_motion,
    ``PhysicsLogic.Philosophy.Symmetry.variational_symmetry_yields_conservation_only_through_bridge),
  (``PhysicsLogicConsumer.ClassicalDynamics.SymmetryRoleReuse.the_library_derives_the_weighted_conservation_law_for_damped_motion,
    ``PhysicsLogic.Philosophy.Symmetry.variational_symmetry_yields_conservation_only_through_bridge),
  (``PhysicsLogicConsumer.CosmicVariance.noise_free_cosmic_variance_is_nonvacuous,
    ``PhysicsLogic.Framework.PowerSpectrumSamplingVarianceCalculationModel.actual_positive_variance_gives_distinct_possible_estimates),
  (``PhysicsLogicConsumer.CosmicVariance.noise_free_cosmic_variance_is_nonvacuous,
    ``PhysicsLogic.Paradigm.CosmologicalInference.sampling_variation_excludes_exact_recovery_from_every_realization),
  (``PhysicsLogicConsumer.GeodesicFocusing.caustic_does_not_end_null_geodesics,
    ``PhysicsLogic.Framework.TransverseScale.positive_convergence_gives_finite_zero),
  (``PhysicsLogicConsumer.GeodesicFocusing.caustic_does_not_end_null_geodesics,
    ``PhysicsLogic.Framework.CongruenceFocusingContext.applicable_route_establishes_finite_parameter_focusing),
  (``PhysicsLogicConsumer.GeodesicFocusing.NormalAreaReuse.the_library_recognizes_the_actual_closed_spacelike_sphere,
    ``PhysicsLogic.Framework.NullSurfaceGeometry.NullSurfaceReadout.regular_normal_geometry_has_a_closed_spacelike_domain),
  (``PhysicsLogicConsumer.GeodesicFocusing.NormalAreaReuse.the_library_uses_the_same_actual_normal_in_the_area_derivative,
    ``PhysicsLogic.Framework.NullSurfaceGeometry.NullSurfaceReadout.the_area_profile_derivative_uses_its_actual_normal),
  (``PhysicsLogicConsumer.GeodesicFocusing.NormalAreaReuse.actual_focusing_and_closed_geometry_do_not_supply_shared_trapping,
    ``PhysicsLogic.Framework.NullSurfaceGeometry.NullSurfaceReadout.oriented_trapping_has_positive_convergence),
  (``PhysicsLogicConsumer.NuclearScattering.nuclear_truncation_is_orderwise_not_exactly_unitary,
    ``PhysicsLogic.Framework.ElasticSWave.real_contact_insertion_satisfies_linearized_unitarity),
  (``PhysicsLogicConsumer.NuclearScattering.LowEnergyData.unitary_limit_parameter_coordinates_preserve_predictions_not_variation,
    ``PhysicsLogic.Paradigm.RenormalizationGroup.all_scale_matching_and_active_target_establish_nonvacuous_scale_independent_predictions),
  (``PhysicsLogicConsumer.NuclearScattering.LowEnergyData.unitary_limit_parameter_coordinates_preserve_predictions_not_variation,
    ``PhysicsLogic.Framework.ElasticSWave.matched_contacts_recover_the_two_effective_range_terms),
  (``PhysicsLogicConsumer.NuclearScattering.RangeTruncation.the_single_insertion_has_a_small_relative_norm,
    ``PhysicsLogic.Framework.ElasticSWave.real_inverse_range_insertion_has_relative_bound),
  (``PhysicsLogicConsumer.NuclearScattering.RangeTruncation.a_physical_phase_remainder_needs_its_own_error_budget,
    ``PhysicsLogic.Framework.ElasticSWave.real_inverse_range_shift_has_relative_quadratic_error),
  (``PhysicsLogicConsumer.NuclearScattering.nuclear_truncation_is_orderwise_not_exactly_unitary,
    ``PhysicsLogic.Framework.ElasticSWave.nonzero_first_order_truncation_is_not_exactly_unitary),
  (``PhysicsLogicConsumer.NuclearScattering.LowEnergyData.resumming_derivative_contact_retains_exact_remainder,
    ``PhysicsLogic.Framework.ElasticSWave.contact_shift_has_exact_quadratic_remainder),
  (``PhysicsLogicConsumer.NuclearScattering.exactly_unitary_two_contact_resummations_need_not_be_scale_independent,
    ``PhysicsLogic.Framework.ElasticSWave.real_contact_amplitude_is_elastic_unitary),
  (``PhysicsLogicConsumer.CondensedMatter.opposite_chiralities_have_opposite_differential_hall_response,
    ``PhysicsLogic.Framework.DifferentialHallResponse.signed_density_and_streda_determine_hall_response),
  (``PhysicsLogicConsumer.CondensedMatter.DensityVariational.gauge_equivalence_laws_follow_from_the_actual_density_classification,
    ``PhysicsLogic.Philosophy.Determination.EquivalenceQualifiedDeterminationContext.classification_law_implies_equivalence_laws),
  (``PhysicsLogicConsumer.CondensedMatter.DensityVariational.the_library_makes_the_actual_density_route_applicable,
    ``PhysicsLogic.Framework.DensityFunctionalContext.setup_and_calculation_make_ground_density_route_applicable),
  (``PhysicsLogicConsumer.CondensedMatter.DensityVariational.the_library_establishes_the_actual_density_minimum,
    ``PhysicsLogic.Framework.DensityFunctionalContext.applicable_route_establishes_ground_density_variational_principle),
  (``PhysicsLogicConsumer.CondensedMatter.DensityVariational.the_library_retains_a_nonvacuous_density_minimum,
    ``PhysicsLogic.Framework.DensityFunctionalContext.established_variational_principle_exhibits_nonvacuous_ground_density_variational),
  (``PhysicsLogicConsumer.CondensedMatter.DensityVariational.the_library_bounds_every_actual_fixed_number_candidate,
    ``PhysicsLogic.Framework.DensityFunctionalContext.admissible_candidate_is_bounded_by_established_ground_density),
  (``PhysicsLogicConsumer.CondensedMatter.ThermalFermionReuse.both_ensembles_use_the_public_nonvacuous_gibbs_normalization,
    ``PhysicsLogic.Framework.FiniteCanonicalData.computed_finite_weights_realize_nonvacuous_canonical_normalization),
  (``PhysicsLogicConsumer.CondensedMatter.ThermalFermionReuse.the_public_mean_api_returns_one_grand_mean_particle,
    ``PhysicsLogic.Framework.FiniteCanonicalData.finite_canonical_mean_is_the_actual_weighted_state_sum),
  (``PhysicsLogicConsumer.CondensedMatter.ThermalFermionReuse.the_public_mean_api_returns_nonzero_grand_number_variance,
    ``PhysicsLogic.Framework.FiniteCanonicalData.finite_canonical_mean_is_the_actual_weighted_state_sum),
  (``PhysicsLogicConsumer.CondensedMatter.ThermalFermionReuse.the_public_mean_api_returns_zero_fixed_sector_number_variance,
    ``PhysicsLogic.Framework.FiniteCanonicalData.finite_canonical_mean_is_the_actual_weighted_state_sum),
  (``PhysicsLogicConsumer.CondensedMatter.ThermalFermionReuse.the_public_mean_api_returns_the_same_one_body_density_in_both_ensembles,
    ``PhysicsLogic.Framework.FiniteCanonicalData.finite_canonical_mean_is_the_actual_weighted_state_sum),
  (``PhysicsLogicConsumer.CondensedMatter.ThermalFermionReuse.the_public_log_weight_api_computes_the_entropy_from_actual_energy,
    ``PhysicsLogic.Framework.FiniteCanonicalData.finite_canonical_log_probability_is_energy_and_partition),
  (``PhysicsLogicConsumer.CondensedMatter.ThermalFermionReuse.the_public_log_weight_api_computes_the_entropy_from_actual_energy,
    ``PhysicsLogic.Framework.FiniteCanonicalData.finite_canonical_probabilities_sum_to_one),
  (``PhysicsLogicConsumer.CondensedMatter.zero_field_quantization_does_not_fix_finite_field_measurement,
    ``PhysicsLogic.Framework.DifferentialHallResponse.first_order_remainder_preserves_response),
  (``PhysicsLogicConsumer.CondensedMatter.filled_landau_levels_change_total_response,
    ``PhysicsLogic.Framework.DifferentialHallResponse.normalized_coefficient_gives_integer_response),
  (``PhysicsLogicConsumer.CondensedMatter.SpectralProbe.identical_spectral_gap_does_not_fix_hall_sign,
    ``PhysicsLogic.Framework.SpectralHallResponse.SpectralData.swapping_operators_reverses_response),
  (``PhysicsLogicConsumer.CondensedMatter.SpectralProbe.identical_spectral_gap_does_not_fix_hall_sign,
    ``PhysicsLogic.Framework.SpectralHallResponse.SpectralData.swapping_operators_preserves_nonvacuity),
  (``PhysicsLogicConsumer.CondensedMatter.SpectralProbe.rephasing_the_eigenvectors_preserves_the_response,
    ``PhysicsLogic.Framework.SpectralHallResponse.SpectralData.unitary_identification_preserves_response),
  (``PhysicsLogicConsumer.CondensedMatter.SpectralProbe.spectral_response_is_real,
    ``PhysicsLogic.Framework.SpectralHallResponse.SpectralData.summable_hermitian_response_is_real),
  (``PhysicsLogicConsumer.CondensedMatter.SpectralProbe.actual_torus_average_uses_the_reversed_bracket,
    ``PhysicsLogic.Framework.TwistCurvatureResponse.averaging_response_gives_oriented_curvature),
  (``PhysicsLogicConsumer.CondensedMatter.SpatialScreening.current_is_gauge_invariant,
    ``PhysicsLogic.Framework.SpatialCurrentResponse.ward_contraction_implies_gauge_invariance),
  (``PhysicsLogicConsumer.CondensedMatter.SpatialScreening.GaugeValues.ward_response_is_an_invariant_quantity,
    ``PhysicsLogic.Framework.SpatialCurrentResponse.ward_contraction_implies_gauge_invariance),
  (``PhysicsLogicConsumer.CondensedMatter.SpatialScreening.GaugeValues.physical_current_value_iff_the_field_is_transverse,
    ``PhysicsLogic.Philosophy.SymmetryAndGauge.invariant_quantity_is_representation_independent_at),
  (``PhysicsLogicConsumer.CondensedMatter.SpatialScreening.GaugeValues.every_transverse_field_has_one_attained_current,
    ``PhysicsLogic.Philosophy.SymmetryAndGauge.physical_value_at_iff_one_attained_value),
  (``PhysicsLogicConsumer.CondensedMatter.SpatialScreening.pure_gauge_modes_produce_no_current,
    ``PhysicsLogic.Framework.SpatialCurrentResponse.ward_contraction_implies_vanishing_pure_gauge_response),
  (``PhysicsLogicConsumer.CondensedMatter.SpatialScreening.nonaxis_aligned_probe_has_nonzero_london_response,
    ``PhysicsLogic.Framework.SpatialCurrentResponse.RadialFamily.transverse_setup_and_actual_limit_realize_london_response),
  (``PhysicsLogicConsumer.CondensedMatter.SpatialScreening.orthogonal_transverse_probe_has_different_london_stiffness,
    ``PhysicsLogic.Framework.SpatialCurrentResponse.RadialFamily.transverse_setup_and_actual_limit_realize_london_response),
  (``PhysicsLogicConsumer.CondensedMatter.SpatialScreening.actual_london_current_is_nonzero,
    ``PhysicsLogic.Framework.SpatialCurrentResponse.RadialFamily.nonvacuous_london_response_has_nonzero_limiting_current),
  (``PhysicsLogicConsumer.CondensedMatter.SpatialScreening.normal_current_opposes_the_probe,
    ``PhysicsLogic.Framework.SpatialCurrentResponse.response_pairing_real_multiple),
  (``PhysicsLogicConsumer.CondensedMatter.SpatialScreening.finite_wavevector_normal_response_does_not_supply_london_screening,
    ``PhysicsLogic.Framework.SpatialCurrentResponse.RadialFamily.vanishing_current_limit_excludes_london_response),
  (``PhysicsLogicConsumer.CondensedMatter.SpatialScreening.zero_value_at_zero_momentum_does_not_erase_the_london_limit,
    ``PhysicsLogic.Framework.SpatialCurrentResponse.RadialFamily.transverse_setup_and_actual_limit_realize_london_response),
  (``PhysicsLogicConsumer.AMOSpectroscopy.pulse_segment_solves_dynamics,
    ``PhysicsLogic.Framework.CoherentTwoState.pulse_solves_schrodinger),
  (``PhysicsLogicConsumer.AMOSpectroscopy.PhysicalPulseScale.the_library_evolves_the_calibrated_pulse,
    ``PhysicsLogic.Framework.CoherentTwoState.pulse_solves_schrodinger),
  (``PhysicsLogicConsumer.AMOSpectroscopy.PhysicalPulseScale.the_library_gives_a_coherent_physical_beam,
    ``PhysicsLogic.Framework.CoherentTwoState.pulse_free_pulse_realizes_coherent_transition),
  (``PhysicsLogicConsumer.AMOSpectroscopy.PhysicalPulseScale.equal_physical_areas_and_resonant_peaks_do_not_fix_the_frequency_response,
    ``PhysicsLogic.Framework.CoherentTwoState.pulse_free_pulse_transition_probability),
  (``PhysicsLogicConsumer.AMOSpectroscopy.positive_speed_has_physical_transit,
    ``PhysicsLogic.Framework.CoherentTwoState.pulse_free_pulse_realizes_coherent_transition),
  (``PhysicsLogicConsumer.AMOSpectroscopy.drive_free_evolution_is_visible_after_recombination,
    ``PhysicsLogic.Framework.CoherentTwoState.pulse_free_pulse_transition_probability),
  (``PhysicsLogicConsumer.AMOSpectroscopy.coherent_molecules_do_not_imply_complete_beam_inversion,
    ``PhysicsLogic.Framework.CoherentTwoState.nonvacuous_transition_has_normalized_final_state),
  (``PhysicsLogicConsumer.AMOSpectroscopy.coherent_molecules_do_not_imply_complete_beam_inversion,
    ``PhysicsLogic.Framework.CoherentTwoState.nonvacuous_transition_probability_is_admissible),
  (``PhysicsLogicConsumer.QuantumInformation.dephasing_recovery_is_nonvacuous,
    ``PhysicsLogic.Framework.CoherentQuantumRecovery.Model.supported_binary_calculations_give_coherent_recovery),
  (``PhysicsLogicConsumer.QuantumInformation.dephasing_recovery_restores_density,
    ``PhysicsLogic.Framework.CoherentQuantumRecovery.Experiment.coherent_recovery_restores_density),
  (``PhysicsLogicConsumer.QuantumInformation.dephasing_recovery_has_common_normalized_environment,
    ``PhysicsLogic.Framework.CoherentQuantumRecovery.Experiment.coherent_recovery_has_normalized_state_independent_environment),
  (``PhysicsLogicConsumer.QuantumInformation.dephasing_recovery_preserves_reference_coherences,
    ``PhysicsLogic.Framework.CoherentQuantumRecovery.Model.factorized_recovery_preserves_reference_coherences),
  (``PhysicsLogicConsumer.QuantumInformation.first_basis_repair_needs_the_complementary_stage,
    ``PhysicsLogic.Framework.CoherentQuantumRecovery.isometric_matrix_preserves_joint_norm),
  (``PhysicsLogicConsumer.PlasmaPhysics.self_consistent_phase_mixing_is_not_microscopic_decay,
    ``PhysicsLogic.Framework.ElectrostaticKinetic.free_streaming_preserves_velocity_modulus),
  (``PhysicsLogicConsumer.PlasmaPhysics.self_consistent_phase_mixing_is_not_microscopic_decay,
    ``PhysicsLogic.Framework.ElectrostaticKinetic.free_streaming_is_reversible),
  (``PhysicsLogicConsumer.PlasmaPhysics.mode_has_derivative,
    ``PhysicsLogic.Framework.ElectrostaticKinetic.free_streaming_amplitude_has_derivative),
  (``PhysicsLogicConsumer.PlasmaPhysics.fixed_ion_probe_has_actual_linearized_equation,
    ``PhysicsLogic.Framework.ElectrostaticKinetic.FourierKineticMode.kinetic_mode_iff_actual_linearized_equation),
  (``PhysicsLogicConsumer.PlasmaPhysics.neutral_pair_retains_actual_poisson_equation,
    ``PhysicsLogic.Framework.ElectrostaticKinetic.FinitePlasma.nonvacuous_vlasov_poisson_retains_actual_charge_density),
  (``PhysicsLogicConsumer.PhaseMixingRecovery.the_library_refocuses_the_velocity_mode,
    ``PhysicsLogic.Framework.ElectrostaticKinetic.velocity_reversal_and_forward_streaming_recover_reflected_initial),
  (``PhysicsLogicConsumer.ThermalProbeCompleteness.the_library_normalizes_the_reference_law,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.CanonicalEnsemble.canonical_law_is_probability),
  (``PhysicsLogicConsumer.ThermalProbeCompleteness.the_alternative_is_not_gibbs_at_any_temperature,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.CanonicalEnsemble.density_at_energy_difference),
  (``PhysicsLogicConsumer.ThermalProbeCompleteness.the_library_derives_reference_spectral_balance,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.TransitionSlice.canonical_spectral_detailed_balance),
  (``PhysicsLogicConsumer.ThermalProbeCompleteness.the_library_derives_reference_fluctuation_dissipation,
    ``PhysicsLogic.Framework.ThermalTransitionSpectrum.TransitionSlice.canonical_symmetrized_fluctuation_dissipation),
  (``PhysicsLogicConsumer.ThermalProbeCompleteness.the_library_excludes_exact_state_recovery_from_this_probe,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.ambiguous_record_does_not_determine_a_value),
  (``PhysicsLogicConsumer.ThermalProbeCompleteness.the_library_excludes_thermal_certification_from_this_probe,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.record_constraint_holds_on_compatible_configuration),
  (``PhysicsLogicConsumer.ThermalProbeCompleteness.DescriptiveScope.the_same_record_is_complete_for_populations_but_omits_coherence,
    ``PhysicsLogic.Philosophy.DescriptiveCompleteness.incompleteness_excludes_completeness),
  (``PhysicsLogicConsumer.ThermalProbeCompleteness.DescriptiveScope.empty_entry_scope_is_neither_complete_nor_incomplete,
    ``PhysicsLogic.Philosophy.DescriptiveCompleteness.not_complete_iff_empty_or_omitted),
  (``PhysicsLogicConsumer.ThermalProbeCompleteness.Calibration.the_library_cannot_recover_the_state_with_uncertain_relative_gains,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.ambiguous_record_does_not_determine_a_value),
  (``PhysicsLogicConsumer.ThermalProbeCompleteness.Calibration.the_library_cannot_certify_gibbs_with_uncertain_relative_gains,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.record_constraint_holds_on_compatible_configuration),
  (``PhysicsLogicConsumer.ThermalProbeCompleteness.CrossProbeScope.the_conditional_recovery_includes_an_actual_nonstationary_state,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.record_constraint_mono),
  (``PhysicsLogicConsumer.ThermalProbeCompleteness.CrossProbeScope.the_library_rejects_full_state_recovery_from_all_cross_records,
    ``PhysicsLogic.Philosophy.Measurement.RecordAccessContext.ambiguous_record_does_not_determine_a_value),
  (``PhysicsLogicConsumer.LightConePropagation.the_library_excludes_spacelike_light_signals,
    ``PhysicsLogic.Paradigm.CausalLocality.nonvacuous_propagation_and_causal_exclusion_forbid_spacelike_signals),
  (``PhysicsLogicConsumer.LightConePropagation.the_library_excludes_spacelike_signals_under_the_explicit_speed_bound,
    ``PhysicsLogic.Paradigm.CausalLocality.finite_propagation_and_causal_exclusion_forbid_spacelike_signals),
  (``PhysicsLogicConsumer.LightConePropagation.Redescription.same_event_iff_equal_decoded_coordinates,
    ``PhysicsLogic.Philosophy.Covariance.same_physical_situation_iff_equal_decoded_situations),
  (``PhysicsLogicConsumer.LightConePropagation.Redescription.a_passive_boost_describes_the_same_event_with_different_coordinates,
    ``PhysicsLogic.Philosophy.Covariance.interpreted_reexpression_represents_same_physical_situation),
  (``PhysicsLogicConsumer.BrownianMotion.independent_pair_has_additive_mean_square,
    ``PhysicsLogic.Framework.StochasticDisplacement.independent_centered_steps_give_linear_mean_square),
  (``PhysicsLogicConsumer.Langevin1908.Ensemble.the_library_retains_the_initial_displacement_cross_term,
    ``PhysicsLogic.Framework.StochasticDisplacement.mean_square_successor_retains_cross_moments),
  (``PhysicsLogicConsumer.Langevin1908.Ensemble.independence_supplies_a_distinct_sufficient_closure,
    ``PhysicsLogic.Framework.StochasticDisplacement.independent_centered_steps_have_zero_cross_moment),
  (``PhysicsLogicConsumer.Langevin1908.Ensemble.newton_averaging_and_two_closures_give_the_source_law,
    ``PhysicsLogic.Framework.StochasticDisplacement.mean_square_successor_retains_cross_moments),
  (``PhysicsLogicConsumer.Langevin1908.Ensemble.stationary_rate_and_zero_cross_moment_give_nonvacuous_source_spreading,
    ``PhysicsLogic.Framework.StochasticDisplacement.Observation.physical_positive_moment_realizes_nonvacuous_spreading),
  (``PhysicsLogicConsumer.Langevin1908.DynamicalDiagnostic.symmetric_displacement_does_not_remove_the_initial_position_cross_term,
    ``PhysicsLogic.Framework.StochasticDisplacement.mean_square_successor_retains_cross_moments),
  (``PhysicsLogicConsumer.MomentIdentification.the_library_certifies_real_spreading_for_both_laws,
    ``PhysicsLogic.Framework.StochasticDisplacement.Observation.physical_positive_moment_realizes_nonvacuous_spreading),
  (``PhysicsLogicConsumer.MomentIdentification.the_library_identifies_the_raw_moment_with_variance_and_rms,
    ``PhysicsLogic.Framework.StochasticDisplacement.Observation.zero_mean_identifies_raw_and_centered_second_moments),
  (``PhysicsLogicConsumer.MomentIdentification.the_library_identifies_the_raw_moment_with_variance_and_rms,
    ``PhysicsLogic.Framework.StochasticDisplacement.Observation.rms_squared_is_mean_square),
  (``PhysicsLogicConsumer.MomentIdentification.matching_first_two_moments_does_not_determine_the_law,
    ``PhysicsLogic.Philosophy.Determination.reduced_determination_is_injective_on_admissible_domain),
  (``PhysicsLogicConsumer.MomentIdentification.equal_linear_spreading_does_not_supply_the_quartic_diffusion_balance,
    ``PhysicsLogic.Framework.StochasticDisplacement.Observation.physical_positive_moment_realizes_nonvacuous_spreading),
  (``PhysicsLogicConsumer.BrownianMotion.repeated_steps_have_quadratic_mean_square,
    ``PhysicsLogic.Framework.StochasticDisplacement.mean_square_is_sum_of_actual_cross_moments),
  (``PhysicsLogicConsumer.BrownianMotion.both_second_observations_are_nonvacuous,
    ``PhysicsLogic.Framework.StochasticDisplacement.nonvacuous_process_spread_retains_actual_observation),
  (``PhysicsLogicConsumer.BrownianMotion.repeated_centered_steps_are_not_independent,
    ``PhysicsLogic.Framework.StochasticDisplacement.independent_centered_steps_have_zero_cross_moment),
  (``PhysicsLogicConsumer.BrownianMotion.relative_observation_has_unit_dispersion,
    ``PhysicsLogic.Framework.StochasticDisplacement.Observation.zero_mean_identifies_raw_and_centered_second_moments),
  (``PhysicsLogicConsumer.BrownianMotion.noiseless_finite_records_do_not_exactly_recover_the_ensemble_target,
    ``PhysicsLogic.Framework.StochasticDisplacement.Observation.rms_squared_is_mean_square),
  (``PhysicsLogicConsumer.BrownianMotion.all_diffusive_gaussian_prefixes_do_not_imply_independent_steps,
    ``PhysicsLogic.Framework.StochasticDisplacement.independent_centered_steps_have_zero_cross_moment),
  (``PhysicsLogicConsumer.BrownianMotion.all_diffusive_gaussian_prefixes_do_not_imply_independent_steps,
    ``PhysicsLogic.Framework.StochasticDisplacement.observed_prefix_retains_actual_moments),
  (``PhysicsLogicConsumer.StatMech.ReciprocityReuse.the_independent_three_coordinate_ensemble_realizes_nonvacuous_reciprocity,
    ``PhysicsLogic.Framework.ReciprocalTransport.EquilibriumCorrelation.Dynamics.a_reversible_fluctuating_equilibrium_has_nonvacuous_correlation_reversal),
  (``PhysicsLogicConsumer.StatMech.ReciprocityReuse.the_shared_reversal_law_excludes_a_nonzero_even_initial_slope,
    ``PhysicsLogic.Framework.ReciprocalTransport.EquilibriumCorrelation.Dynamics.a_differentiable_equal_parity_correlation_has_zero_initial_slope),
  (``PhysicsLogicConsumer.StatMech.ReciprocityReuse.a_variance_two_moment_fit_has_an_explicit_reciprocity_error_budget,
    ``PhysicsLogic.Framework.ReciprocalTransport.EquilibriumCorrelation.Dynamics.controlled_regression_errors_bound_the_actual_reciprocity_defect),
  (``PhysicsLogicConsumer.AMOSpectroscopy.GuidedTrapTransport.the_public_api_propagates_the_actual_normalized_trap_ensemble,
    ``PhysicsLogic.Framework.GuidedDensityTransport.Model.an_initially_normalized_nontrivial_born_law_has_nonvacuous_equivariance),
  (``PhysicsLogicConsumer.AMOSpectroscopy.GuidedTrapTransport.the_public_api_transports_actual_configuration_events,
    ``PhysicsLogic.Framework.GuidedDensityTransport.Model.transported_born_events_use_the_actual_configuration_preimage),
  (``PhysicsLogicConsumer.AMOSpectroscopy.GuidedTrapTransport.the_public_api_gives_normalized_detector_statistics,
    ``PhysicsLogic.Framework.GuidedDensityTransport.Model.a_measurable_record_of_an_equivariant_ensemble_has_normalized_born_statistics),
  (``PhysicsLogicConsumer.AMOSpectroscopy.GuidedTrapTransport.the_public_api_excludes_exact_equilibration_of_the_displaced_ensemble,
    ``PhysicsLogic.Framework.GuidedDensityTransport.Model.injective_transport_cannot_create_exact_equilibrium_from_nonequilibrium),
  (``PhysicsLogicConsumer.AMOSpectroscopy.CentralFieldSpectroscopy.an_s_orbital_has_two_states_and_no_fictitious_lower_partner,
    ``PhysicsLogic.Framework.SpinHalfCentralField.Doublet.s_orbital_occupation_counts_only_the_physical_two_states),
  (``PhysicsLogicConsumer.AMOSpectroscopy.CentralFieldSpectroscopy.the_atomic_p_doublet_has_a_nonzero_physical_spectrum,
    ``PhysicsLogic.Framework.SpinHalfCentralField.Doublet.nonzero_coupling_realizes_nonvacuous_doublet),
  (``PhysicsLogicConsumer.AMOSpectroscopy.CentralFieldSpectroscopy.the_same_interaction_formula_gives_opposite_level_orders,
    ``PhysicsLogic.Framework.SpinHalfCentralField.Doublet.higher_energy_formula),
  (``PhysicsLogicConsumer.AMOSpectroscopy.CentralFieldSpectroscopy.the_same_interaction_formula_gives_opposite_level_orders,
    ``PhysicsLogic.Framework.SpinHalfCentralField.Doublet.lower_energy_formula),
  (``PhysicsLogicConsumer.AMOSpectroscopy.CentralFieldSpectroscopy.a_nonzero_spin_orbit_splitting_does_not_select_nuclear_ordering,
    ``PhysicsLogic.Framework.SpinHalfCentralField.Doublet.higher_j_is_lower_iff_negative_coupling),
  (``PhysicsLogicConsumer.AMOSpectroscopy.CentralFieldSpectroscopy.chemical_potential_zero_selects_different_subshell_counts,
    ``PhysicsLogic.Framework.SpinHalfCentralField.Doublet.chemical_potential_in_nuclear_gap_fills_only_higher_j),
  (``PhysicsLogicConsumer.AMOSpectroscopy.CentralFieldSpectroscopy.chemical_potential_zero_selects_different_subshell_counts,
    ``PhysicsLogic.Framework.SpinHalfCentralField.Doublet.chemical_potential_in_reversed_gap_fills_only_lower_j),
  (``PhysicsLogicConsumer.AMOSpectroscopy.CentralFieldSpectroscopy.the_weighted_centroid_is_not_the_unweighted_level_midpoint,
    ``PhysicsLogic.Framework.SpinHalfCentralField.Doublet.degeneracy_weighted_energy_has_unchanged_centroid),
  (``PhysicsLogicConsumer.AMOSpectroscopy.CentralFieldSpectroscopy.a_common_energy_reference_shift_preserves_the_filled_subshell,
    ``PhysicsLogic.Framework.SpinHalfCentralField.Doublet.shifting_energy_and_chemical_potential_preserves_occupation),
  (``PhysicsLogicConsumer.CosmicVariance.ClosedUniverseDynamics.library_accepts_the_actual_coasting_fluid,
    ``PhysicsLogic.Framework.HomogeneousFluidHistory.field_equations_realize_nonvacuous_fluid_evolution),
  (``PhysicsLogicConsumer.CosmicVariance.ClosedUniverseDynamics.library_accepts_the_actual_coasting_fluid,
    ``PhysicsLogic.Framework.HomogeneousFluidHistory.constraint_on_open_domain_holds_near),
  (``PhysicsLogicConsumer.CosmicVariance.ClosedUniverseDynamics.library_derives_the_actual_density_decay_at_reference_time,
    ``PhysicsLogic.Framework.HomogeneousFluidHistory.field_equations_imply_energy_conservation),
  (``PhysicsLogicConsumer.CosmicVariance.ClosedUniverseDynamics.the_constraint_does_not_test_the_fluid_pressure,
    ``PhysicsLogic.Framework.HomogeneousFluidHistory.constraint_on_open_domain_holds_near),
  (``PhysicsLogicConsumer.CosmicVariance.ClosedUniverseDynamics.library_recovers_pressure_only_with_the_energy_and_motion_inputs,
    ``PhysicsLogic.Framework.HomogeneousFluidHistory.moving_constraint_and_conservation_imply_pressure_equation),
  (``PhysicsLogicConsumer.CosmicVariance.ClosedUniverseDynamics.library_recovers_pressure_only_with_the_energy_and_motion_inputs,
    ``PhysicsLogic.Framework.HomogeneousFluidHistory.differentiated_constraint_retains_rate_factor),
  (``PhysicsLogicConsumer.NuclearScattering.CoulombPhaseTransfer.Datum.the_library_realizes_the_actual_coulomb_relative_amplitude,
    ``PhysicsLogic.Framework.ElasticSWave.real_effective_range_function_realizes_elastic_scattering),
  (``PhysicsLogicConsumer.NuclearScattering.CoulombPhaseTransfer.Datum.the_library_transfers_the_converted_plot_error_to_the_nuclear_amplitude,
    ``PhysicsLogic.Framework.ElasticSWave.controlled_phase_error_bounds_amplitude_error),
  (``PhysicsLogicConsumer.NuclearScattering.CoulombPhaseTransfer.a_small_coulomb_plot_error_is_not_the_same_amplitude_error,
    ``PhysicsLogic.Framework.ElasticSWave.real_effective_range_function_realizes_elastic_scattering),
  (``PhysicsLogicConsumer.NuclearScattering.NeutralParameterComparison.the_library_transfers_inverse_length_and_effective_range_errors,
    ``PhysicsLogic.Framework.ElasticSWave.controlled_phase_error_bounds_amplitude_error),
  (``PhysicsLogicConsumer.NuclearScattering.NeutralParameterComparison.the_library_recognizes_both_parameterized_scattering_responses,
    ``PhysicsLogic.Framework.ElasticSWave.real_effective_range_function_realizes_elastic_scattering),
  (``PhysicsLogicConsumer.NuclearScattering.NeutralParameterComparison.opposite_inverse_lengths_can_have_identical_cross_sections,
    ``PhysicsLogic.Framework.ElasticSWave.inverse_amplitude_recovers_real_effective_range_function)
]

private def auditExternalConsumers (compareReference : Bool) : CommandElabM Unit := do
  unless forbiddenPhysicsDependency
      "PhysicsLogic.Framework.StandardCandlePosterior.Countermodels.LikelihoodModel.uninformedVacuumDirection".toName do
    throwError "External consumer audit failed to reject a posterior countermodel"
  unless forbiddenPhysicsDependency
      "PhysicsLogic.Framework.FiniteResidualCovariance.FourPhaseControl.law".toName do
    throwError "External consumer audit failed to reject the existing four-phase control fixture"
  unless forbiddenPhysicsDependency
      "PhysicsLogic.Framework.SupersymmetricOperator.GroundAttainmentCountermodels.charge".toName do
    throwError "External consumer audit failed to reject a suffixed countermodel namespace"
  if forbiddenPhysicsDependency
      "PhysicsLogic.Framework.SupersymmetricOperator.ChargeEnergyData.energy".toName then
    throwError "External consumer audit rejected an ordinary public operator API"
  if forbiddenPhysicsDependency
      "PhysicsLogic.Framework.FiniteResidualCovariance.InitialMoments".toName then
    throwError "External consumer audit rejected the public initial-moments API"
  let environment ← getEnv
  for moduleName in environment.allImportedModuleNames do
    if `PhysicsLogic.Papers |>.isPrefixOf moduleName then
      throwError "External consumer imported paper module {moduleName}"
    if moduleName.toString.startsWith "deprecated." then
      throwError "External consumer imported deprecated module {moduleName}"

  let groups ← match PhysicsLogicConsumer.DependencyAudit.groupRequirements requiredPublicUses with
    | .ok result => pure result
    | .error message => throwError message
  for (declaration, required) in requiredPublicUses do
    if let some message := consumerUseOwnershipError environment declaration required then
      throwError message
  let (firstClient, firstApi) := requiredPublicUses[0]!
  for (declaration, required) in #[(``Nat.zero, firstApi), (firstClient, ``Nat.zero),
      (`MissingConsumerDeclaration, firstApi), (firstClient, `MissingPublicApi)] do
    unless (consumerUseOwnershipError environment declaration required).isSome do
      throwError "Consumer ownership check accepted invalid use: {declaration}, {required}"

  let collectionStarted ← liftIO IO.monoMsNow
  let mut traversal : Lean.CollectAxioms.State := {}
  let mut declarationCount := 0
  let mut theoremCount := 0
  for (name, info) in environment.constants do
    let some moduleIndex := environment.getModuleIdxFor? name | continue
    let moduleName := environment.allImportedModuleNames[moduleIndex.toNat]!
    unless `PhysicsLogicConsumer |>.isPrefixOf moduleName do continue
    declarationCount := declarationCount + 1
    if let .thmInfo _ := info then theoremCount := theoremCount + 1
    let (_, updated) :=
      ((Lean.CollectAxioms.collect name).run environment).run traversal
    traversal := updated
  if theoremCount == 0 then throwError "External consumer has no checked theorems"
  for axiomName in traversal.axioms do
    unless axiomName == ``propext || axiomName == ``Classical.choice ||
        axiomName == ``Quot.sound do
      throwError "External consumer depends on nonfoundational axiom {axiomName}"
  for dependency in traversal.visited.toList do
    if forbiddenPhysicsDependency dependency then
      throwError "External consumer reused forbidden shortcut {dependency}"

  let collectionFinished ← liftIO IO.monoMsNow
  let parents ← match PhysicsLogicConsumer.DependencyAudit.buildParentIndex environment traversal.visited with
    | .ok result => pure result
    | .error message => throwError message
  let graphFinished ← liftIO IO.monoMsNow
  let mut referenceTargets : Array (Name × NameSet) := #[]
  for (required, declarations) in groups do
    let reached := PhysicsLogicConsumer.DependencyAudit.ancestors parents required
    for declaration in declarations do
      unless traversal.visited.contains declaration && reached.contains declaration do
        throwError "{declaration} does not actually use public API {required}"
    if compareReference then
      referenceTargets := referenceTargets.push (required, reached)
  let indexFinished ← liftIO IO.monoMsNow
  logInfo m!"External consumer dependency timings: shared trust {collectionFinished - collectionStarted} ms, \
    reverse graph {graphFinished - collectionFinished} ms, \
    indexed queries {indexFinished - graphFinished} ms; {traversal.visited.size} visited constants, \
    {groups.size} distinct public targets."
  if compareReference then
    let referenceStarted ← liftIO IO.monoMsNow
    let mut decisions := 0
    for (declaration, _) in requiredPublicUses do
      let (_, reference) :=
        ((Lean.CollectAxioms.collect declaration).run environment).run {}
      for (required, reached) in referenceTargets do
        unless reference.visited.contains required == reached.contains declaration do
          throwError "Indexed/reference dependency mismatch: {declaration}, {required}"
        decisions := decisions + 1
    let referenceFinished ← liftIO IO.monoMsNow
    logInfo m!"External consumer full reference comparison passed: {decisions} positive/negative decisions, \
      {requiredPublicUses.size} fresh kernel-collector closures in {referenceFinished - referenceStarted} ms."
  logInfo m!"External consumer audit passed: {declarationCount} declarations, \
    {theoremCount} theorems, {requiredPublicUses.size} public API uses, \
    {traversal.axioms.size} foundational axioms."

elab "audit_external_consumers" : command => auditExternalConsumers false
elab "audit_external_consumers_with_reference" : command => auditExternalConsumers true

audit_external_consumers