IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.UniversalFoundation

   1/-
   2  PrimitiveRecognitionCalculus/UniversalFoundation.lean
   3
   4  Round-trip source:
   5    δ/PRC_Universal_Foundation_Execution_Plan_20260526.html
   6
   7  Spec anchor:
   8    Build Order step 15: compose arithmetic, structural surfaces, cost, logic,
   9    real completion, recognizer, and admissible inevitability.
  10
  11  This file declares the final PRC universal-foundation certificate after pass
  12  320. The final theorem keeps the repaired/refuted native-cost ledger explicit
  13  instead of pretending the refuted unsigned routes were proved.
  14-/
  15
  16import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Kernel
  17import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness
  18
  19namespace IndisputableMonolith
  20namespace Foundation
  21namespace PrimitiveRecognitionCalculus
  22
  23/-- Historical target ledger carried by the conditional top-level certificate.
  24Positive entries point to proved repaired interfaces; negative entries point to
  25the exact refutations for routes that cannot force the final surface. -/
  26structure PRCUniversalFoundationOpenTargets : Prop where
  27  zero_calibrated_native_cost_uniqueness_refuted :
  28    ¬ PRCJCost.PRCZeroCalibratedNativeCostUniquenessTarget
  29  zero_calibrated_native_cost_character_factorization :
  30    PRCJCost.PRCZeroCalibratedNativeCostCharacterFactorizationTarget
  31  zero_calibrated_native_cost_signed_admissible_factorization_refuted :
  32    ¬ PRCJCost.PRCZeroCalibratedNativeCostSignedAdmissibleCharacterFactorizationTarget
  33  zero_calibration_signed_unit_refuted :
  34    ¬ PRCJCost.PRCZeroCalibrationForcesNativeCostSignedUnitCalibrationTarget
  35  zero_calibrated_prime_signed_strengthened_native_cost_uniqueness :
  36    PRCJCost.PRCZeroCalibratedPrimeSignedStrengthenedNativeCostUniquenessTarget
  37  native_cost_signed_admissible_character_rigidity :
  38    PRCJCost.PRCNativeCostSignedAdmissibleCharacterRigidityTarget
  39  old_native_cost_character_rigidity_refuted :
  40    ¬ PRCJCost.PRCNativeCostCharacterRigidityTarget
  41  old_native_cost_sharpened_refuted :
  42    ¬ PRCJCost.PRCNativeCostUniquenessSharpenedTarget
  43  two_to_prime_calibration_refuted :
  44    ¬ PRCJCost.PRCTwoCalibrationForcesPrimeCalibrationTarget
  45  prime_calibration_propagation_refuted :
  46    ¬ PRCJCost.PRCPrimeCalibrationPropagationTarget
  47  prime_global_orientation_refuted :
  48    ¬ PRCJCost.PRCPrimeCalibrationForcesGlobalOrientationTarget
  49  coherent_prime_orientation :
  50    {χ : RatioOrbit → RatioOrbit} →
  51      PRCJCost.PRCCharacterPrimeOrientationCoherent χ →
  52        PRCJCost.PRCCharacterTwoPrimeBranchControlsPrimes χ
  53  two_prime_branch_controls_primes :
  54    {χ : RatioOrbit → RatioOrbit} →
  55      PRCJCost.PRCCharacterPrimeLocalOrientation χ →
  56        PRCJCost.PRCCharacterTwoPrimeBranchControlsPrimes χ →
  57          PRCJCost.PRCCharacterPrimeOrientationCoherent χ
  58  prime_identity_iff_two_prime_identity :
  59    {χ : RatioOrbit → RatioOrbit} →
  60      PRCJCost.PRCCharacterPrimeLocalOrientation χ →
  61        PRCJCost.PRCCharacterTwoPrimeBranchControlsPrimes χ →
  62          PRCJCost.PRCCharacterPrimeIdentityIffTwoPrimeIdentity χ
  63  prime_identity_forces_two_prime_identity :
  64    {χ : RatioOrbit → RatioOrbit} →
  65      PRCJCost.PRCCharacterPrimeIdentityIffTwoPrimeIdentity χ →
  66        PRCJCost.PRCCharacterPrimeIdentityForcesTwoPrimeIdentity χ
  67  two_prime_reciprocal_excludes_prime_identity :
  68    {χ : RatioOrbit → RatioOrbit} →
  69      PRCJCost.PRCCharacterPrimeLocalOrientation χ →
  70        (PRCJCost.PRCCharacterPrimeIdentityForcesTwoPrimeIdentity χ ↔
  71          PRCJCost.PRCCharacterTwoPrimeReciprocalExcludesPrimeIdentity χ)
  72  two_prime_reciprocal_excludes_prime_identity_witness :
  73    {χ : RatioOrbit → RatioOrbit} →
  74      (PRCJCost.PRCCharacterTwoPrimeReciprocalExcludesPrimeIdentity χ ↔
  75        PRCJCost.PRCCharacterTwoPrimeReciprocalExcludesPrimeIdentityWitness χ)
  76  two_prime_reciprocal_identity_prime_mixed :
  77    {χ : RatioOrbit → RatioOrbit} →
  78      (PRCJCost.PRCCharacterTwoPrimeReciprocalIdentityPrimeMixed χ ↔
  79        PRCJCost.PRCCharacterTwoPrimeReciprocalIdentityNonTwoPrimeMixed χ)
  80  two_prime_reciprocal_identity_non_two_prime_mixed :
  81    {χ : RatioOrbit → RatioOrbit} →
  82      PRCJCost.PRCRatioCharacter χ →
  83        (PRCJCost.PRCCharacterTwoPrimeReciprocalIdentityNonTwoPrimeMixed χ ↔
  84          PRCJCost.PRCCharacterTwoPrimeReciprocalIdentityNonTwoCompositeDefect χ)
  85  two_prime_reciprocal_identity_non_two_composite_defect :
  86    {χ : RatioOrbit → RatioOrbit} →
  87      (PRCJCost.PRCCharacterTwoPrimeReciprocalIdentityNonTwoCompositeDefect χ ↔
  88        PRCJCost.PRCCharacterTwoPrimeReciprocalIdentityNonTwoCompositeCostDefect χ)
  89  two_prime_reciprocal_identity_non_two_composite_cost_defect :
  90    {χ : RatioOrbit → RatioOrbit} →
  91      PRCJCost.PRCCharacterTwoPrimeReciprocalIdentityNonTwoCompositeCostDefect χ →
  92        PRCJCost.PRCCharacterTwoPrimeReciprocalIdentityNonTwoCompositeDefect χ
  93  two_prime_mixed_composite_cost_consistency_target_refuted :
  94    ¬ PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget
  95  prime_pair_product_cost_consistency_target_refuted :
  96    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget
  97  two_prime_reciprocal_forces_prime_reciprocal :
  98    {χ : RatioOrbit → RatioOrbit} →
  99      PRCJCost.PRCCharacterPrimeReciprocalWitnessGlobalizes χ →
 100        PRCJCost.PRCCharacterTwoPrimeReciprocalForcesPrimeReciprocal χ
 101  two_prime_reciprocal_trace_connected :
 102    {χ : RatioOrbit → RatioOrbit} →
 103      (PRCJCost.PRCCharacterTwoPrimeReciprocalRespectsTraceConnected χ ↔
 104        PRCJCost.PRCCharacterTwoPrimeReciprocalForcesPrimeReciprocal χ)
 105  two_prime_identity_trace_connected :
 106    {χ : RatioOrbit → RatioOrbit} →
 107      PRCJCost.PRCCharacterPrimeIdentityRespectsTraceConnected χ →
 108        PRCJCost.PRCCharacterTwoPrimeIdentityRespectsTraceConnected χ
 109  no_mixed_prime_orientation :
 110    {χ : RatioOrbit → RatioOrbit} →
 111      (PRCJCost.PRCCharacterNoMixedPrimeWitnesses χ ↔
 112        PRCJCost.PRCCharacterNoMixedPrimeOrientation χ)
 113  mixed_prime_witnesses :
 114    {χ : RatioOrbit → RatioOrbit} →
 115      (PRCJCost.PRCCharacterMixedPrimeWitnesses χ ↔
 116        PRCJCost.PRCCharacterMixedPrimePairWitnesses χ)
 117  mixed_prime_pair_witnesses :
 118    {χ : RatioOrbit → RatioOrbit} →
 119      (PRCJCost.PRCCharacterMixedPrimePairWitnesses χ ↔
 120        PRCJCost.PRCCharacterSamePrimeMixedPairWitnesses χ ∨
 121          PRCJCost.PRCCharacterDistinctPrimeMixedPairWitnesses χ)
 122  same_prime_mixed_pair_witnesses :
 123    {χ : RatioOrbit → RatioOrbit} →
 124      ¬ PRCJCost.PRCCharacterSamePrimeMixedPairWitnesses χ
 125  distinct_prime_mixed_pair_witnesses :
 126    {χ : RatioOrbit → RatioOrbit} →
 127      PRCJCost.PRCCharacterPrimeIdentityBranchUniform χ →
 128        ¬ PRCJCost.PRCCharacterDistinctPrimeMixedPairWitnesses χ
 129  prime_identity_witness_excludes_reciprocal :
 130    {χ : RatioOrbit → RatioOrbit} →
 131      (PRCJCost.PRCCharacterPrimeIdentityWitnessExcludesReciprocal χ ↔
 132        PRCJCost.PRCCharacterNoMixedPrimeOrientation χ)
 133  prime_reciprocal_witness_globalizes :
 134    {χ : RatioOrbit → RatioOrbit} →
 135      PRCJCost.PRCCharacterPrimeLocalOrientation χ →
 136        PRCJCost.PRCCharacterNoMixedPrimeOrientation χ →
 137          PRCJCost.PRCCharacterPrimeReciprocalWitnessGlobalizes χ
 138  prime_reciprocal_forces_two_prime_reciprocal :
 139    {χ : RatioOrbit → RatioOrbit} →
 140      PRCJCost.PRCCharacterPrimeReciprocalWitnessGlobalizes χ →
 141        PRCJCost.PRCCharacterPrimeReciprocalForcesTwoPrimeReciprocal χ
 142  prime_reciprocal_witness_globalizes_split :
 143    {χ : RatioOrbit → RatioOrbit} →
 144      (PRCJCost.PRCCharacterPrimeReciprocalWitnessGlobalizes χ ↔
 145        PRCJCost.PRCCharacterPrimeReciprocalWitnessGlobalizesSplit χ)
 146  prime_reciprocal_forces_two_from_reciprocal_twist_identity_forces_two :
 147    ∀ χ : RatioOrbit → RatioOrbit,
 148      PRCJCost.PRCCharacterPrimeIdentityForcesTwoPrimeIdentity
 149          (PRCJCost.PRCCharacterReciprocalTwist χ) →
 150        PRCJCost.PRCCharacterPrimeReciprocalForcesTwoPrimeReciprocal χ
 151  prime_identity_forces_two_from_reciprocal_twist_reciprocal_forces_two :
 152    ∀ χ : RatioOrbit → RatioOrbit,
 153      PRCJCost.PRCCharacterPrimeReciprocalForcesTwoPrimeReciprocal
 154          (PRCJCost.PRCCharacterReciprocalTwist χ) →
 155        PRCJCost.PRCCharacterPrimeIdentityForcesTwoPrimeIdentity χ
 156  prime_identity_trace_coherence :
 157    {χ : RatioOrbit → RatioOrbit} →
 158      (PRCJCost.PRCCharacterPrimeIdentityBranchUniform χ ↔
 159        PRCJCost.PRCCharacterPrimeIdentityTraceCoherent χ)
 160  prime_identity_branch_uniform :
 161    {χ : RatioOrbit → RatioOrbit} →
 162      (PRCJCost.PRCCharacterPrimeIdentityBranchUniform χ ↔
 163        PRCJCost.PRCCharacterPrimeIdentityIffTwoPrimeIdentity χ)
 164  prime_axis_trace_connected :
 165    ∀ p : DistinctionNat, ∀ hp : DistinctionNat.primeOrbit p,
 166      ∀ r : DistinctionNat, ∀ hr : DistinctionNat.primeOrbit r,
 167        PRCJCost.PRCPrimeAxisTraceConnected p hp r hr
 168  prime_identity_respects_trace_connected :
 169    {χ : RatioOrbit → RatioOrbit} →
 170      (PRCJCost.PRCCharacterPrimeIdentityRespectsCanonicalAddTrace χ ↔
 171        PRCJCost.PRCCharacterPrimeIdentityRespectsTraceConnected χ)
 172  prime_identity_respects_common_trace_extension :
 173    {χ : RatioOrbit → RatioOrbit} →
 174      (PRCJCost.PRCCharacterPrimeIdentityRespectsCanonicalAddTrace χ ↔
 175        PRCJCost.PRCCharacterPrimeIdentityRespectsCommonTraceExtension χ)
 176  prime_identity_respects_canonical_add_trace :
 177    {χ : RatioOrbit → RatioOrbit} →
 178      (PRCJCost.PRCCharacterPrimeIdentityBranchUniform χ ↔
 179        PRCJCost.PRCCharacterPrimeIdentityRespectsCanonicalAddTrace χ)
 180  prime_identity_respects_comparable_trace :
 181    {χ : RatioOrbit → RatioOrbit} →
 182      (PRCJCost.PRCCharacterPrimeIdentityRespectsComparableTrace χ ↔
 183        PRCJCost.PRCCharacterPrimeIdentityTraceCoherent χ)
 184  prime_identity_trace_coherence_target_refuted :
 185    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget
 186  prime_identity_branch_uniformity_target_refuted :
 187    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget
 188  prime_identity_trace_transport_target_refuted :
 189    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceTransportTarget
 190  prime_identity_common_trace_extension_target_refuted :
 191    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCommonTraceExtensionTarget
 192  prime_identity_canonical_add_trace_target_refuted :
 193    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCanonicalAddTraceTarget
 194  prime_identity_comparable_trace_target_refuted :
 195    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityComparableTraceTarget
 196  orbit_successor_identity_target_refuted :
 197    ¬ PRCJCost.PRCPrimeCalibrationForcesOrbitSuccessorIdentityTarget
 198  orbit_successor_transport_target_refuted :
 199    ¬ PRCJCost.PRCPrimeCalibrationForcesOrbitSuccessorTransportTarget
 200  prime_floor_successor_transport_target_refuted :
 201    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget
 202  prime_identity_witness_globalizes_nonunit_target_refuted :
 203    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityWitnessGlobalizesNonunitTarget
 204  prime_floor_identity_extends_successor_step_target_refuted :
 205    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentityExtendsSuccessorStepTarget
 206  prime_floor_identity_contracts_successor_step_target_refuted :
 207    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentityContractsSuccessorStepTarget
 208  prime_floor_identity_successor_step_pair_target_refuted :
 209    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget
 210  prime_floor_nonunit_local_orientation_target_refuted :
 211    ¬ PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitLocalOrientationTarget
 212  prime_floor_nonunit_product_local_orientation_target_refuted :
 213    ¬ PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitProductLocalOrientationTarget
 214  prime_floor_nonunit_orbit_orientation_coherent_target_refuted :
 215    ¬ PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget
 216  prime_floor_no_mixed_nonunit_orbit_orientation_target_refuted :
 217    ¬ PRCJCost.PRCPrimeCalibrationForcesNoMixedNonunitOrbitOrientationTarget
 218  prime_floor_nonunit_identity_branch_transport_target_refuted :
 219    ¬ PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityBranchTransportTarget
 220  prime_floor_nonunit_identity_witness_globalizes_target_refuted :
 221    ¬ PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget
 222  prime_floor_nonunit_identity_witness_excludes_reciprocal_target_refuted :
 223    ¬ PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessExcludesReciprocalTarget
 224  prime_floor_nonunit_no_mixed_witnesses_target_refuted :
 225    ¬ PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesTarget
 226  prime_floor_no_mixed_prime_witnesses_target_refuted :
 227    ¬ PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget
 228  prime_floor_mixed_prime_witness_character :
 229    PRCJCost.PRCPrimeCalibratedMixedPrimeWitnessesCharacter
 230  prime_floor_mixed_prime_pair_witness_character :
 231    PRCJCost.PRCPrimeCalibratedMixedPrimePairWitnessCharacter
 232  prime_floor_same_prime_mixed_pair_witness_character_refuted :
 233    ¬ PRCJCost.PRCPrimeCalibratedSamePrimeMixedPairWitnessCharacter
 234  prime_floor_distinct_prime_mixed_pair_witness_character :
 235    PRCJCost.PRCPrimeCalibratedDistinctPrimeMixedPairWitnessCharacter
 236  prime_floor_prime_identity_witness_excludes_reciprocal_target_refuted :
 237    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityWitnessExcludesReciprocalTarget
 238  prime_floor_prime_reciprocal_witness_globalizes_target_refuted :
 239    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget
 240  prime_floor_prime_reciprocal_forces_two_prime_reciprocal_target_refuted :
 241    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalForcesTwoPrimeReciprocalTarget
 242  prime_floor_prime_reciprocal_witness_globalizes_split_target_refuted :
 243    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesSplitTarget
 244  prime_floor_prime_witnesses_control_nonunit_target :
 245    PRCJCost.PRCPrimeCalibrationForcesPrimeWitnessesControlNonunitWitnessesTarget
 246  prime_floor_mixed_nonunit_witnesses_reflect_prime_target :
 247    PRCJCost.PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesTarget
 248  prime_floor_mixed_nonunit_identity_witness_reflects_prime_target :
 249    PRCJCost.PRCPrimeCalibrationForcesMixedNonunitIdentityWitnessReflectsPrimeWitnessTarget
 250  prime_floor_mixed_nonunit_reciprocal_witness_reflects_prime_target :
 251    PRCJCost.PRCPrimeCalibrationForcesMixedNonunitReciprocalWitnessReflectsPrimeWitnessTarget
 252  prime_floor_mixed_nonunit_witnesses_reflect_prime_split_target :
 253    PRCJCost.PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesSplitTarget
 254  prime_floor_nonunit_no_mixed_witnesses_split_target_refuted :
 255    ¬ PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesSplitTarget
 256  prime_floor_nonunit_identity_witness_local_exclusion_target_refuted :
 257    ¬ PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessLocalExclusionTarget
 258  prime_floor_nonunit_reciprocal_branch_transport_target_refuted :
 259    ¬ PRCJCost.PRCPrimeCalibrationForcesNonunitReciprocalBranchTransportTarget
 260  prime_floor_nonunit_branch_transport_pair_target_refuted :
 261    ¬ PRCJCost.PRCPrimeCalibrationForcesNonunitBranchTransportPairTarget
 262  prime_floor_nonunit_identity_comparable_trace_target_refuted :
 263    ¬ PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget
 264  prime_floor_nonunit_branch_agreement_target_refuted :
 265    ¬ PRCJCost.PRCPrimeCalibrationForcesNonunitBranchAgreementTarget
 266  prime_floor_nonunit_orbit_orientation_local_branch_agreement_target_refuted :
 267    ¬ PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalBranchAgreementTarget
 268  prime_floor_nonunit_orbit_orientation_local_identity_transport_target_refuted :
 269    ¬ PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalIdentityTransportTarget
 270  prime_floor_nonunit_orbit_orientation_local_comparable_trace_target_refuted :
 271    ¬ PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalComparableTraceTarget
 272  prime_floor_nonunit_orbit_orientation_local_no_mixed_target_refuted :
 273    ¬ PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalNoMixedTarget
 274  prime_floor_nonunit_orbit_orientation_local_product_no_mixed_target_refuted :
 275    ¬ PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalProductNoMixedTarget
 276  prime_floor_no_mixed_nonunit_from_product_no_mixed :
 277    PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget →
 278      PRCJCost.PRCPrimeCalibrationForcesNoMixedNonunitOrbitOrientationTarget
 279  prime_floor_product_no_mixed_from_no_mixed_nonunit :
 280    PRCJCost.PRCPrimeCalibrationForcesNoMixedNonunitOrbitOrientationTarget →
 281      PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget
 282  prime_floor_product_no_mixed_iff_no_mixed_nonunit :
 283    PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget ↔
 284      PRCJCost.PRCPrimeCalibrationForcesNoMixedNonunitOrbitOrientationTarget
 285  prime_floor_product_no_mixed_from_identity_branch_transport :
 286    PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityBranchTransportTarget →
 287      PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget
 288  prime_floor_nonunit_identity_branch_transport_from_comparable_trace :
 289    PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget →
 290      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityBranchTransportTarget
 291  prime_floor_nonunit_coherent_from_product_no_mixed :
 292    PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget →
 293      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget
 294  prime_floor_product_no_mixed_iff_nonunit_coherent :
 295    PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget ↔
 296      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget
 297  prime_floor_nonunit_identity_branch_transport_from_product_no_mixed :
 298    PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget →
 299      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityBranchTransportTarget
 300  prime_floor_product_no_mixed_iff_identity_branch_transport :
 301    PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget ↔
 302      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityBranchTransportTarget
 303  prime_floor_identity_witness_globalizes_from_identity_branch_transport :
 304    PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityBranchTransportTarget →
 305      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget
 306  prime_floor_identity_branch_transport_from_identity_witness_globalizes :
 307    PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget →
 308      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityBranchTransportTarget
 309  prime_floor_identity_witness_globalizes_iff_identity_branch_transport :
 310    PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget ↔
 311      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityBranchTransportTarget
 312  prime_floor_identity_witness_globalizes_from_product_no_mixed :
 313    PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget →
 314      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget
 315  prime_floor_product_no_mixed_from_identity_witness_globalizes :
 316    PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget →
 317      PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget
 318  prime_floor_product_no_mixed_iff_identity_witness_globalizes :
 319    PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget ↔
 320      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget
 321  prime_floor_nonunit_coherent_from_identity_witness_globalizes :
 322    PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget →
 323      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget
 324  prime_floor_identity_witness_globalizes_from_nonunit_coherent :
 325    PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget →
 326      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget
 327  prime_floor_nonunit_coherent_iff_identity_witness_globalizes :
 328    PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget ↔
 329      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget
 330  prime_floor_identity_witness_excludes_reciprocal_from_no_mixed :
 331    PRCJCost.PRCPrimeCalibrationForcesNoMixedNonunitOrbitOrientationTarget →
 332      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessExcludesReciprocalTarget
 333  prime_floor_no_mixed_from_identity_witness_excludes_reciprocal :
 334    PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessExcludesReciprocalTarget →
 335      PRCJCost.PRCPrimeCalibrationForcesNoMixedNonunitOrbitOrientationTarget
 336  prime_floor_identity_witness_excludes_reciprocal_iff_no_mixed :
 337    PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessExcludesReciprocalTarget ↔
 338      PRCJCost.PRCPrimeCalibrationForcesNoMixedNonunitOrbitOrientationTarget
 339  prime_floor_no_mixed_witnesses_from_identity_witness_excludes_reciprocal :
 340    PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessExcludesReciprocalTarget →
 341      PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesTarget
 342  prime_floor_identity_witness_excludes_reciprocal_from_no_mixed_witnesses :
 343    PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesTarget →
 344      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessExcludesReciprocalTarget
 345  prime_floor_no_mixed_witnesses_iff_identity_witness_excludes_reciprocal :
 346    PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesTarget ↔
 347      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessExcludesReciprocalTarget
 348  prime_floor_no_mixed_prime_witnesses_from_no_mixed_prime_orientation :
 349    PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget →
 350      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget
 351  prime_floor_no_mixed_prime_orientation_from_no_mixed_prime_witnesses :
 352    PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget →
 353      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget
 354  prime_floor_no_mixed_prime_witnesses_iff_no_mixed_prime_orientation :
 355    PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget ↔
 356      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget
 357  prime_floor_prime_identity_witness_excludes_reciprocal_from_no_mixed_prime_orientation :
 358    PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget →
 359      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityWitnessExcludesReciprocalTarget
 360  prime_floor_no_mixed_prime_orientation_from_identity_witness_excludes_reciprocal :
 361    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityWitnessExcludesReciprocalTarget →
 362      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget
 363  prime_floor_prime_identity_witness_excludes_reciprocal_iff_no_mixed_prime_orientation :
 364    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityWitnessExcludesReciprocalTarget ↔
 365      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget
 366  prime_floor_no_mixed_prime_witnesses_from_identity_witness_excludes_reciprocal :
 367    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityWitnessExcludesReciprocalTarget →
 368      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget
 369  prime_floor_prime_identity_witness_excludes_reciprocal_from_no_mixed_prime_witnesses :
 370    PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget →
 371      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityWitnessExcludesReciprocalTarget
 372  prime_floor_no_mixed_prime_witnesses_iff_identity_witness_excludes_reciprocal :
 373    PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget ↔
 374      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityWitnessExcludesReciprocalTarget
 375  prime_floor_no_mixed_prime_witnesses_iff_not_mixed_prime_witnesses :
 376    ∀ χ : RatioOrbit → RatioOrbit,
 377      PRCJCost.PRCCharacterNoMixedPrimeWitnesses χ ↔
 378        ¬ PRCJCost.PRCCharacterMixedPrimeWitnesses χ
 379  prime_floor_mixed_prime_pair_witnesses_from_mixed_prime_witnesses :
 380    ∀ χ : RatioOrbit → RatioOrbit,
 381      PRCJCost.PRCCharacterMixedPrimeWitnesses χ →
 382        PRCJCost.PRCCharacterMixedPrimePairWitnesses χ
 383  prime_floor_mixed_prime_witnesses_from_pair_witnesses :
 384    ∀ χ : RatioOrbit → RatioOrbit,
 385      PRCJCost.PRCCharacterMixedPrimePairWitnesses χ →
 386        PRCJCost.PRCCharacterMixedPrimeWitnesses χ
 387  prime_floor_mixed_prime_witnesses_iff_pair_witnesses :
 388    ∀ χ : RatioOrbit → RatioOrbit,
 389      PRCJCost.PRCCharacterMixedPrimeWitnesses χ ↔
 390        PRCJCost.PRCCharacterMixedPrimePairWitnesses χ
 391  prime_floor_no_mixed_prime_witnesses_iff_not_mixed_prime_pair_witnesses :
 392    ∀ χ : RatioOrbit → RatioOrbit,
 393      PRCJCost.PRCCharacterNoMixedPrimeWitnesses χ ↔
 394        ¬ PRCJCost.PRCCharacterMixedPrimePairWitnesses χ
 395  prime_floor_mixed_prime_pair_witnesses_same_or_distinct :
 396    ∀ χ : RatioOrbit → RatioOrbit,
 397      PRCJCost.PRCCharacterMixedPrimePairWitnesses χ →
 398        PRCJCost.PRCCharacterSamePrimeMixedPairWitnesses χ ∨
 399          PRCJCost.PRCCharacterDistinctPrimeMixedPairWitnesses χ
 400  prime_floor_mixed_prime_pair_witnesses_from_same_or_distinct :
 401    ∀ χ : RatioOrbit → RatioOrbit,
 402      PRCJCost.PRCCharacterSamePrimeMixedPairWitnesses χ ∨
 403        PRCJCost.PRCCharacterDistinctPrimeMixedPairWitnesses χ →
 404          PRCJCost.PRCCharacterMixedPrimePairWitnesses χ
 405  prime_floor_mixed_prime_pair_witnesses_iff_same_or_distinct :
 406    ∀ χ : RatioOrbit → RatioOrbit,
 407      PRCJCost.PRCCharacterMixedPrimePairWitnesses χ ↔
 408        PRCJCost.PRCCharacterSamePrimeMixedPairWitnesses χ ∨
 409          PRCJCost.PRCCharacterDistinctPrimeMixedPairWitnesses χ
 410  prime_floor_no_mixed_prime_witnesses_iff_no_same_and_no_distinct_pair :
 411    ∀ χ : RatioOrbit → RatioOrbit,
 412      PRCJCost.PRCCharacterNoMixedPrimeWitnesses χ ↔
 413        ¬ PRCJCost.PRCCharacterSamePrimeMixedPairWitnesses χ ∧
 414          ¬ PRCJCost.PRCCharacterDistinctPrimeMixedPairWitnesses χ
 415  prime_floor_same_prime_mixed_pair_witnesses_absurd :
 416    ∀ χ : RatioOrbit → RatioOrbit,
 417      ¬ PRCJCost.PRCCharacterSamePrimeMixedPairWitnesses χ
 418  prime_floor_no_mixed_prime_witnesses_iff_not_distinct_prime_pair :
 419    ∀ χ : RatioOrbit → RatioOrbit,
 420      PRCJCost.PRCCharacterNoMixedPrimeWitnesses χ ↔
 421        ¬ PRCJCost.PRCCharacterDistinctPrimeMixedPairWitnesses χ
 422  prime_floor_distinct_prime_mixed_pair_witnesses_absurd_from_branch_uniform :
 423    ∀ χ : RatioOrbit → RatioOrbit,
 424      PRCJCost.PRCCharacterPrimeIdentityBranchUniform χ →
 425        ¬ PRCJCost.PRCCharacterDistinctPrimeMixedPairWitnesses χ
 426  prime_floor_prime_identity_branch_uniform_from_local_no_distinct_prime_pair :
 427    ∀ χ : RatioOrbit → RatioOrbit,
 428      PRCJCost.PRCCharacterPrimeLocalOrientation χ →
 429        ¬ PRCJCost.PRCCharacterDistinctPrimeMixedPairWitnesses χ →
 430          PRCJCost.PRCCharacterPrimeIdentityBranchUniform χ
 431  prime_floor_prime_identity_branch_uniform_iff_no_distinct_prime_pair_of_local :
 432    ∀ χ : RatioOrbit → RatioOrbit,
 433      PRCJCost.PRCCharacterPrimeLocalOrientation χ →
 434        (PRCJCost.PRCCharacterPrimeIdentityBranchUniform χ ↔
 435          ¬ PRCJCost.PRCCharacterDistinctPrimeMixedPairWitnesses χ)
 436  prime_floor_prime_identity_branch_uniform_from_identity_iff_two :
 437    ∀ χ : RatioOrbit → RatioOrbit,
 438      PRCJCost.PRCCharacterPrimeIdentityIffTwoPrimeIdentity χ →
 439        PRCJCost.PRCCharacterPrimeIdentityBranchUniform χ
 440  prime_floor_prime_identity_iff_two_from_branch_uniform :
 441    ∀ χ : RatioOrbit → RatioOrbit,
 442      PRCJCost.PRCCharacterPrimeIdentityBranchUniform χ →
 443        PRCJCost.PRCCharacterPrimeIdentityIffTwoPrimeIdentity χ
 444  prime_floor_prime_identity_branch_uniform_iff_identity_iff_two :
 445    ∀ χ : RatioOrbit → RatioOrbit,
 446      PRCJCost.PRCCharacterPrimeIdentityBranchUniform χ ↔
 447        PRCJCost.PRCCharacterPrimeIdentityIffTwoPrimeIdentity χ
 448  prime_floor_prime_reciprocal_witness_globalizes_from_no_mixed_prime_orientation :
 449    PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget →
 450      PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget
 451  prime_floor_no_mixed_prime_orientation_from_reciprocal_witness_globalizes :
 452    PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget →
 453      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget
 454  prime_floor_prime_reciprocal_witness_globalizes_iff_no_mixed_prime_orientation :
 455    PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget ↔
 456      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget
 457  prime_floor_prime_reciprocal_witness_globalizes_iff_identity_witness_excludes_reciprocal :
 458    PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget ↔
 459      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityWitnessExcludesReciprocalTarget
 460  prime_floor_prime_reciprocal_forces_two_from_reciprocal_witness_globalizes :
 461    PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget →
 462      PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalForcesTwoPrimeReciprocalTarget
 463  prime_floor_two_prime_reciprocal_forces_from_reciprocal_witness_globalizes :
 464    PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget →
 465      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget
 466  prime_floor_prime_reciprocal_witness_globalizes_split_from_reciprocal_witness_globalizes :
 467    PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget →
 468      PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesSplitTarget
 469  prime_floor_prime_reciprocal_witness_globalizes_from_split :
 470    PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesSplitTarget →
 471      PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget
 472  prime_floor_prime_reciprocal_witness_globalizes_iff_split :
 473    PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget ↔
 474      PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesSplitTarget
 475  prime_floor_prime_reciprocal_forces_two_from_identity_forces_two :
 476    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget →
 477      PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalForcesTwoPrimeReciprocalTarget
 478  prime_floor_prime_identity_forces_two_from_reciprocal_forces_two :
 479    PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalForcesTwoPrimeReciprocalTarget →
 480      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget
 481  prime_floor_prime_reciprocal_forces_two_iff_identity_forces_two :
 482    PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalForcesTwoPrimeReciprocalTarget ↔
 483      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget
 484  prime_floor_two_prime_reciprocal_excludes_identity_witness_from_excludes :
 485    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget →
 486      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget
 487  prime_floor_two_prime_reciprocal_excludes_from_identity_witness_excludes :
 488    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget →
 489      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget
 490  prime_floor_two_prime_reciprocal_excludes_iff_identity_witness_excludes :
 491    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget ↔
 492      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget
 493  prime_floor_prime_identity_forces_two_from_two_prime_reciprocal_excludes_identity_witness :
 494    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget →
 495      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget
 496  prime_floor_two_prime_reciprocal_excludes_identity_witness_from_identity_forces_two :
 497    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget →
 498      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget
 499  prime_floor_prime_identity_forces_two_iff_two_prime_reciprocal_excludes_identity_witness :
 500    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget ↔
 501      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget
 502  prime_floor_two_prime_reciprocal_excludes_identity_witness_from_no_mixed_character :
 503    ¬ PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityPrimeMixedCharacter →
 504      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget
 505  prime_floor_no_mixed_character_from_two_prime_reciprocal_excludes_identity_witness :
 506    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget →
 507      ¬ PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityPrimeMixedCharacter
 508  prime_floor_two_prime_reciprocal_excludes_identity_witness_iff_no_mixed_character :
 509    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget ↔
 510      ¬ PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityPrimeMixedCharacter
 511  prime_floor_non_two_mixed_character_from_mixed_character :
 512    PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityPrimeMixedCharacter →
 513      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter
 514  prime_floor_mixed_character_from_non_two_mixed_character :
 515    PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter →
 516      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityPrimeMixedCharacter
 517  prime_floor_mixed_character_iff_non_two_mixed_character :
 518    PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityPrimeMixedCharacter ↔
 519      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter
 520  prime_floor_two_prime_reciprocal_excludes_identity_witness_iff_no_non_two_mixed_character :
 521    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget ↔
 522      ¬ PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter
 523  prime_floor_composite_defect_character_from_non_two_mixed_character :
 524    PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter →
 525      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter
 526  prime_floor_non_two_mixed_character_from_composite_defect_character :
 527    PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter →
 528      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter
 529  prime_floor_non_two_mixed_character_iff_composite_defect_character :
 530    PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter ↔
 531      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter
 532  prime_floor_two_prime_reciprocal_excludes_identity_witness_iff_no_composite_defect_character :
 533    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget ↔
 534      ¬ PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter
 535  prime_floor_composite_cost_defect_character_from_composite_defect_character :
 536    PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter →
 537      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter
 538  prime_floor_composite_defect_character_from_composite_cost_defect_character :
 539    PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter →
 540      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter
 541  prime_floor_composite_defect_character_iff_composite_cost_defect_character :
 542    PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter ↔
 543      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter
 544  prime_floor_two_prime_reciprocal_excludes_identity_witness_iff_no_composite_cost_defect_character :
 545    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget ↔
 546      ¬ PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter
 547  prime_floor_two_prime_mixed_composite_cost_consistency_from_no_cost_defect :
 548    ¬ PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter →
 549      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget
 550  prime_floor_no_cost_defect_from_two_prime_mixed_composite_cost_consistency :
 551    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget →
 552      ¬ PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter
 553  prime_floor_two_prime_mixed_composite_cost_consistency_iff_no_cost_defect :
 554    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget ↔
 555      ¬ PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter
 556  prime_floor_two_prime_reciprocal_excludes_identity_witness_iff_mixed_composite_cost_consistency :
 557    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget ↔
 558      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget
 559  prime_floor_two_prime_reciprocal_excludes_identity_witness_from_mixed_composite_cost_consistency_direct :
 560    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget →
 561      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget
 562  prime_floor_two_prime_mixed_composite_cost_consistency_from_prime_pair_product_cost_consistency :
 563    PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget →
 564      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget
 565  prime_floor_prime_pair_product_cost_consistency_from_prime_calibration_propagation :
 566    PRCJCost.PRCPrimeCalibrationPropagationTarget →
 567      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget
 568  prime_floor_prime_pair_product_cost_consistency_from_coherent_prime_orientation :
 569    PRCJCost.PRCPrimeCalibrationForcesCoherentPrimeOrientationTarget →
 570      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget
 571  prime_floor_coherent_prime_orientation_from_prime_pair_product_cost_consistency :
 572    PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget →
 573      PRCJCost.PRCPrimeCalibrationForcesCoherentPrimeOrientationTarget
 574  prime_floor_prime_pair_product_cost_consistency_iff_coherent_prime_orientation :
 575    PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget ↔
 576      PRCJCost.PRCPrimeCalibrationForcesCoherentPrimeOrientationTarget
 577  prime_floor_prime_pair_product_cost_consistency_from_no_mixed_prime_witnesses :
 578    PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget →
 579      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget
 580  prime_floor_no_mixed_prime_witnesses_from_prime_pair_product_cost_consistency :
 581    PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget →
 582      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget
 583  prime_floor_prime_pair_product_cost_consistency_iff_no_mixed_prime_witnesses :
 584    PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget ↔
 585      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget
 586  prime_floor_no_mixed_prime_witness_character_absurd_from_no_mixed_prime_witnesses :
 587    PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget →
 588      ¬ PRCJCost.PRCPrimeCalibratedMixedPrimeWitnessesCharacter
 589  prime_floor_no_mixed_prime_witnesses_from_no_mixed_prime_witness_character :
 590    ¬ PRCJCost.PRCPrimeCalibratedMixedPrimeWitnessesCharacter →
 591      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget
 592  prime_floor_no_mixed_prime_witnesses_iff_no_mixed_prime_witness_character :
 593    PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget ↔
 594      ¬ PRCJCost.PRCPrimeCalibratedMixedPrimeWitnessesCharacter
 595  prime_floor_prime_pair_product_cost_consistency_iff_no_mixed_prime_witness_character :
 596    PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget ↔
 597      ¬ PRCJCost.PRCPrimeCalibratedMixedPrimeWitnessesCharacter
 598  prime_floor_no_mixed_prime_witnesses_not_from_mixed_prime_witness_character :
 599    PRCJCost.PRCPrimeCalibratedMixedPrimeWitnessesCharacter →
 600      ¬ PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget
 601  prime_floor_mixed_prime_witness_character_from_not_no_mixed_prime_witnesses :
 602    ¬ PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget →
 603      PRCJCost.PRCPrimeCalibratedMixedPrimeWitnessesCharacter
 604  prime_floor_no_mixed_prime_witnesses_not_iff_mixed_prime_witness_character :
 605    ¬ PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget ↔
 606      PRCJCost.PRCPrimeCalibratedMixedPrimeWitnessesCharacter
 607  prime_floor_prime_pair_product_cost_consistency_not_from_mixed_prime_witness_character :
 608    PRCJCost.PRCPrimeCalibratedMixedPrimeWitnessesCharacter →
 609      ¬ PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget
 610  prime_floor_mixed_prime_witness_character_from_not_prime_pair_product_cost_consistency :
 611    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget →
 612      PRCJCost.PRCPrimeCalibratedMixedPrimeWitnessesCharacter
 613  prime_floor_prime_pair_product_cost_consistency_not_iff_mixed_prime_witness_character :
 614    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget ↔
 615      PRCJCost.PRCPrimeCalibratedMixedPrimeWitnessesCharacter
 616  prime_floor_mixed_prime_pair_witness_character_from_mixed_prime_witness_character :
 617    PRCJCost.PRCPrimeCalibratedMixedPrimeWitnessesCharacter →
 618      PRCJCost.PRCPrimeCalibratedMixedPrimePairWitnessCharacter
 619  prime_floor_mixed_prime_witness_character_from_pair_witness_character :
 620    PRCJCost.PRCPrimeCalibratedMixedPrimePairWitnessCharacter →
 621      PRCJCost.PRCPrimeCalibratedMixedPrimeWitnessesCharacter
 622  prime_floor_mixed_prime_witness_character_iff_pair_witness_character :
 623    PRCJCost.PRCPrimeCalibratedMixedPrimeWitnessesCharacter ↔
 624      PRCJCost.PRCPrimeCalibratedMixedPrimePairWitnessCharacter
 625  prime_floor_no_mixed_prime_witnesses_iff_no_mixed_prime_pair_witness_character :
 626    PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget ↔
 627      ¬ PRCJCost.PRCPrimeCalibratedMixedPrimePairWitnessCharacter
 628  prime_floor_no_mixed_prime_witnesses_not_iff_mixed_prime_pair_witness_character :
 629    ¬ PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget ↔
 630      PRCJCost.PRCPrimeCalibratedMixedPrimePairWitnessCharacter
 631  prime_floor_prime_pair_product_cost_consistency_iff_no_mixed_prime_pair_witness_character :
 632    PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget ↔
 633      ¬ PRCJCost.PRCPrimeCalibratedMixedPrimePairWitnessCharacter
 634  prime_floor_prime_pair_product_cost_consistency_not_iff_mixed_prime_pair_witness_character :
 635    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget ↔
 636      PRCJCost.PRCPrimeCalibratedMixedPrimePairWitnessCharacter
 637  prime_floor_mixed_prime_pair_witness_character_same_or_distinct :
 638    PRCJCost.PRCPrimeCalibratedMixedPrimePairWitnessCharacter →
 639      PRCJCost.PRCPrimeCalibratedSamePrimeMixedPairWitnessCharacter ∨
 640        PRCJCost.PRCPrimeCalibratedDistinctPrimeMixedPairWitnessCharacter
 641  prime_floor_mixed_prime_pair_witness_character_from_same_or_distinct :
 642    PRCJCost.PRCPrimeCalibratedSamePrimeMixedPairWitnessCharacter ∨
 643      PRCJCost.PRCPrimeCalibratedDistinctPrimeMixedPairWitnessCharacter →
 644        PRCJCost.PRCPrimeCalibratedMixedPrimePairWitnessCharacter
 645  prime_floor_mixed_prime_pair_witness_character_iff_same_or_distinct :
 646    PRCJCost.PRCPrimeCalibratedMixedPrimePairWitnessCharacter ↔
 647      PRCJCost.PRCPrimeCalibratedSamePrimeMixedPairWitnessCharacter ∨
 648        PRCJCost.PRCPrimeCalibratedDistinctPrimeMixedPairWitnessCharacter
 649  prime_floor_no_mixed_prime_witnesses_iff_no_same_and_no_distinct_pair_witness_character :
 650    PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget ↔
 651      ¬ PRCJCost.PRCPrimeCalibratedSamePrimeMixedPairWitnessCharacter ∧
 652        ¬ PRCJCost.PRCPrimeCalibratedDistinctPrimeMixedPairWitnessCharacter
 653  prime_floor_no_mixed_prime_witnesses_not_iff_same_or_distinct_pair_witness_character :
 654    ¬ PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget ↔
 655      PRCJCost.PRCPrimeCalibratedSamePrimeMixedPairWitnessCharacter ∨
 656        PRCJCost.PRCPrimeCalibratedDistinctPrimeMixedPairWitnessCharacter
 657  prime_floor_prime_pair_product_cost_consistency_iff_no_same_and_no_distinct_pair_witness_character :
 658    PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget ↔
 659      ¬ PRCJCost.PRCPrimeCalibratedSamePrimeMixedPairWitnessCharacter ∧
 660        ¬ PRCJCost.PRCPrimeCalibratedDistinctPrimeMixedPairWitnessCharacter
 661  prime_floor_prime_pair_product_cost_consistency_not_iff_same_or_distinct_pair_witness_character :
 662    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget ↔
 663      PRCJCost.PRCPrimeCalibratedSamePrimeMixedPairWitnessCharacter ∨
 664        PRCJCost.PRCPrimeCalibratedDistinctPrimeMixedPairWitnessCharacter
 665  prime_floor_same_prime_mixed_pair_witness_character_absurd :
 666    ¬ PRCJCost.PRCPrimeCalibratedSamePrimeMixedPairWitnessCharacter
 667  prime_floor_no_mixed_prime_witnesses_iff_no_distinct_prime_pair_witness_character :
 668    PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget ↔
 669      ¬ PRCJCost.PRCPrimeCalibratedDistinctPrimeMixedPairWitnessCharacter
 670  prime_floor_no_mixed_prime_witnesses_not_iff_distinct_prime_pair_witness_character :
 671    ¬ PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget ↔
 672      PRCJCost.PRCPrimeCalibratedDistinctPrimeMixedPairWitnessCharacter
 673  prime_floor_prime_pair_product_cost_consistency_iff_no_distinct_prime_pair_witness_character :
 674    PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget ↔
 675      ¬ PRCJCost.PRCPrimeCalibratedDistinctPrimeMixedPairWitnessCharacter
 676  prime_floor_prime_pair_product_cost_consistency_not_iff_distinct_prime_pair_witness_character :
 677    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget ↔
 678      PRCJCost.PRCPrimeCalibratedDistinctPrimeMixedPairWitnessCharacter
 679  prime_floor_prime_identity_branch_uniformity_from_no_distinct_prime_pair_witness_character :
 680    ¬ PRCJCost.PRCPrimeCalibratedDistinctPrimeMixedPairWitnessCharacter →
 681      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget
 682  prime_floor_no_distinct_prime_pair_witness_character_from_prime_identity_branch_uniformity :
 683    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget →
 684      ¬ PRCJCost.PRCPrimeCalibratedDistinctPrimeMixedPairWitnessCharacter
 685  prime_floor_prime_identity_branch_uniformity_iff_no_distinct_prime_pair_witness_character :
 686    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget ↔
 687      ¬ PRCJCost.PRCPrimeCalibratedDistinctPrimeMixedPairWitnessCharacter
 688  prime_floor_prime_identity_branch_uniformity_not_iff_distinct_prime_pair_witness_character :
 689    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget ↔
 690      PRCJCost.PRCPrimeCalibratedDistinctPrimeMixedPairWitnessCharacter
 691  prime_floor_prime_pair_product_cost_consistency_iff_prime_identity_branch_uniformity :
 692    PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget ↔
 693      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget
 694  prime_floor_prime_identity_branch_uniformity_from_identity_iff_two :
 695    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityIffTwoPrimeIdentityTarget →
 696      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget
 697  prime_floor_prime_identity_iff_two_from_branch_uniformity :
 698    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget →
 699      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityIffTwoPrimeIdentityTarget
 700  prime_floor_prime_identity_branch_uniformity_iff_identity_iff_two :
 701    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget ↔
 702      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityIffTwoPrimeIdentityTarget
 703  prime_floor_prime_identity_branch_uniformity_iff_identity_forces_two :
 704    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget ↔
 705      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget
 706  prime_floor_prime_pair_product_cost_consistency_iff_prime_identity_forces_two :
 707    PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget ↔
 708      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget
 709  prime_floor_prime_identity_forces_two_not_iff_distinct_prime_pair_witness_character :
 710    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget ↔
 711      PRCJCost.PRCPrimeCalibratedDistinctPrimeMixedPairWitnessCharacter
 712  prime_floor_prime_identity_forces_two_iff_no_two_prime_mixed_character :
 713    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget ↔
 714      ¬ PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityPrimeMixedCharacter
 715  prime_floor_prime_identity_forces_two_iff_no_non_two_mixed_character :
 716    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget ↔
 717      ¬ PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter
 718  prime_floor_non_two_mixed_character_from_two_adic_axis_twist :
 719    PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter →
 720      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter
 721  prime_floor_prime_calibration_from_two_adic_axis_twist :
 722    ∀ χ : RatioOrbit → RatioOrbit,
 723      PRCJCost.PRCCharacterTwoAdicAxisTwist χ →
 724        PRCJCost.PRCCharacterPrimeDirectionCalibrated χ
 725  prime_floor_calibrated_two_adic_axis_twist_from_ratio_character_axis_twist :
 726    PRCJCost.PRCTwoAdicAxisTwistRatioCharacter →
 727      PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter
 728  prime_floor_ratio_character_axis_twist_from_calibrated_two_adic_axis_twist :
 729    PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter →
 730      PRCJCost.PRCTwoAdicAxisTwistRatioCharacter
 731  prime_floor_calibrated_two_adic_axis_twist_iff_ratio_character_axis_twist :
 732    PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter ↔
 733      PRCJCost.PRCTwoAdicAxisTwistRatioCharacter
 734  prime_floor_ratio_character_axis_twist_absurd_from_no_calibrated_twist :
 735    ¬ PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter →
 736      ¬ PRCJCost.PRCTwoAdicAxisTwistRatioCharacter
 737  prime_floor_two_adic_axis_twist_absurd_from_no_non_two_mixed :
 738    ¬ PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter →
 739      ¬ PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter
 740  prime_floor_two_adic_axis_twist_absurd_from_mixed_composite_cost_consistency :
 741    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget →
 742      ¬ PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter
 743  prime_floor_two_adic_axis_twist_absurd_from_prime_identity_forces_two :
 744    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget →
 745      ¬ PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter
 746  prime_floor_two_adic_axis_twist_absurd_from_prime_pair_product_cost_consistency :
 747    PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget →
 748      ¬ PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter
 749  prime_floor_mixed_composite_cost_consistency_not_from_two_adic_axis_twist :
 750    PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter →
 751      ¬ PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget
 752  prime_floor_prime_identity_forces_two_not_from_two_adic_axis_twist :
 753    PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter →
 754      ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget
 755  prime_floor_prime_pair_product_cost_consistency_not_from_two_adic_axis_twist :
 756    PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter →
 757      ¬ PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget
 758  prime_floor_ratio_character_axis_twist_absurd_from_mixed_composite_cost_consistency :
 759    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget →
 760      ¬ PRCJCost.PRCTwoAdicAxisTwistRatioCharacter
 761  prime_floor_ratio_character_axis_twist_absurd_from_prime_identity_forces_two :
 762    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget →
 763      ¬ PRCJCost.PRCTwoAdicAxisTwistRatioCharacter
 764  prime_floor_ratio_character_axis_twist_absurd_from_prime_pair_product_cost_consistency :
 765    PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget →
 766      ¬ PRCJCost.PRCTwoAdicAxisTwistRatioCharacter
 767  prime_floor_mixed_composite_cost_consistency_not_from_ratio_character_axis_twist :
 768    PRCJCost.PRCTwoAdicAxisTwistRatioCharacter →
 769      ¬ PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget
 770  prime_floor_prime_identity_forces_two_not_from_ratio_character_axis_twist :
 771    PRCJCost.PRCTwoAdicAxisTwistRatioCharacter →
 772      ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget
 773  prime_floor_prime_pair_product_cost_consistency_not_from_ratio_character_axis_twist :
 774    PRCJCost.PRCTwoAdicAxisTwistRatioCharacter →
 775      ¬ PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget
 776  prime_floor_two_three_mixed_not_composite :
 777    ¬ RatioOrbit.crossEq PRCJCost.twoThreePrimeMixedDirection
 778      PRCJCost.twoThreePrimeCompositeDirection
 779  prime_floor_two_three_mixed_not_composite_recip :
 780    ¬ RatioOrbit.crossEq PRCJCost.twoThreePrimeMixedDirection
 781      (RatioOrbit.recip PRCJCost.twoThreePrimeCompositeDirection)
 782  prime_floor_two_adic_axis_twist_two_three_mixed_image :
 783    ∀ χ : RatioOrbit → RatioOrbit,
 784      PRCJCost.PRCRatioCharacter χ →
 785        PRCJCost.PRCCharacterTwoAdicAxisTwist χ →
 786          RatioOrbit.crossEq (χ PRCJCost.twoThreePrimeCompositeDirection)
 787            PRCJCost.twoThreePrimeMixedDirection
 788  prime_floor_two_adic_axis_twist_two_three_local_orientation_absurd :
 789    ∀ χ : RatioOrbit → RatioOrbit,
 790      PRCJCost.PRCRatioCharacter χ →
 791        PRCJCost.PRCCharacterTwoAdicAxisTwist χ →
 792          ¬ PRCJCost.PRCCharacterTwoThreeCompositeLocalOrientation χ
 793  prime_floor_ratio_character_axis_twist_forces_two_three_local_orientation_failure :
 794    PRCJCost.PRCTwoAdicAxisTwistRatioCharacter →
 795      ∃ χ : RatioOrbit → RatioOrbit,
 796        PRCJCost.PRCRatioCharacter χ ∧
 797          PRCJCost.PRCCharacterTwoAdicAxisTwist χ ∧
 798            ¬ PRCJCost.PRCCharacterTwoThreeCompositeLocalOrientation χ
 799  prime_floor_two_three_failure_character_from_ratio_character_axis_twist :
 800    PRCJCost.PRCTwoAdicAxisTwistRatioCharacter →
 801      PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter
 802  prime_floor_ratio_character_axis_twist_from_two_three_failure_character :
 803    PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter →
 804      PRCJCost.PRCTwoAdicAxisTwistRatioCharacter
 805  prime_floor_two_three_failure_character_iff_ratio_character_axis_twist :
 806    PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter ↔
 807      PRCJCost.PRCTwoAdicAxisTwistRatioCharacter
 808  prime_floor_two_three_failure_character_iff_calibrated_two_adic_axis_twist :
 809    PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter ↔
 810      PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter
 811  prime_floor_two_three_local_orientation_target_from_no_ratio_character_axis_twist :
 812    ¬ PRCJCost.PRCTwoAdicAxisTwistRatioCharacter →
 813      PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget
 814  prime_floor_ratio_character_axis_twist_absurd_from_two_three_local_orientation_target :
 815    PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget →
 816      ¬ PRCJCost.PRCTwoAdicAxisTwistRatioCharacter
 817  prime_floor_two_three_local_orientation_target_iff_no_ratio_character_axis_twist :
 818    PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget ↔
 819      ¬ PRCJCost.PRCTwoAdicAxisTwistRatioCharacter
 820  prime_floor_two_three_failure_character_absurd_from_two_three_local_orientation_target :
 821    PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget →
 822      ¬ PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter
 823  prime_floor_two_three_local_orientation_target_iff_no_failure_character :
 824    PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget ↔
 825      ¬ PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter
 826  prime_floor_two_three_local_orientation_target_iff_no_calibrated_two_adic_axis_twist :
 827    PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget ↔
 828      ¬ PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter
 829  prime_floor_calibrated_two_adic_axis_twist_absurd_from_two_three_local_orientation_target :
 830    PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget →
 831      ¬ PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter
 832  prime_floor_two_three_local_orientation_target_from_no_failure_character :
 833    ¬ PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter →
 834      PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget
 835  prime_floor_two_three_local_fork_certificate :
 836    PRCJCost.PRCTwoThreeCompositeLocalForkCertificate
 837  prime_floor_calibrated_two_adic_axis_twist_from_two_three_failure_character :
 838    PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter →
 839      PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter
 840  prime_floor_non_two_mixed_character_from_two_three_failure_character :
 841    PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter →
 842      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter
 843  prime_floor_composite_defect_character_from_two_three_failure_character :
 844    PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter →
 845      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter
 846  prime_floor_composite_cost_defect_character_from_two_three_failure_character :
 847    PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter →
 848      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter
 849  prime_floor_mixed_composite_cost_consistency_not_from_two_three_failure_character :
 850    PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter →
 851      ¬ PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget
 852  prime_floor_prime_identity_forces_two_not_from_two_three_failure_character :
 853    PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter →
 854      ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget
 855  prime_floor_prime_pair_product_cost_consistency_not_from_two_three_failure_character :
 856    PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter →
 857      ¬ PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget
 858  prime_floor_two_three_failure_character_absurd_from_no_calibrated_two_adic_axis_twist :
 859    ¬ PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter →
 860      ¬ PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter
 861  prime_floor_two_three_failure_character_absurd_from_no_non_two_mixed_character :
 862    ¬ PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter →
 863      ¬ PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter
 864  prime_floor_two_three_failure_character_absurd_from_no_non_two_composite_defect_character :
 865    ¬ PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter →
 866      ¬ PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter
 867  prime_floor_two_three_failure_character_absurd_from_no_non_two_composite_cost_defect_character :
 868    ¬ PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter →
 869      ¬ PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter
 870  prime_floor_two_three_local_orientation_target_from_no_calibrated_two_adic_axis_twist :
 871    ¬ PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter →
 872      PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget
 873  prime_floor_two_three_local_orientation_target_from_no_non_two_mixed_character :
 874    ¬ PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter →
 875      PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget
 876  prime_floor_two_three_local_orientation_target_from_no_non_two_composite_defect_character :
 877    ¬ PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter →
 878      PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget
 879  prime_floor_two_three_local_orientation_target_from_no_non_two_composite_cost_defect_character :
 880    ¬ PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter →
 881      PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget
 882  prime_floor_two_three_local_orientation_target_from_mixed_composite_cost_consistency :
 883    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget →
 884      PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget
 885  prime_floor_two_three_local_orientation_target_from_prime_identity_forces_two :
 886    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget →
 887      PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget
 888  prime_floor_two_three_local_orientation_target_from_prime_pair_product_cost_consistency :
 889    PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget →
 890      PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget
 891  prime_floor_two_three_failure_character_absurd_from_mixed_composite_cost_consistency :
 892    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget →
 893      ¬ PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter
 894  prime_floor_two_three_failure_character_absurd_from_prime_identity_forces_two :
 895    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget →
 896      ¬ PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter
 897  prime_floor_two_three_failure_character_absurd_from_prime_pair_product_cost_consistency :
 898    PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget →
 899      ¬ PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter
 900  prime_floor_ratio_character_axis_twist_absurd_from_prime_identity_branch_uniformity :
 901    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget →
 902      ¬ PRCJCost.PRCTwoAdicAxisTwistRatioCharacter
 903  prime_floor_two_three_failure_character_absurd_from_prime_identity_branch_uniformity :
 904    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget →
 905      ¬ PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter
 906  prime_floor_two_three_local_orientation_target_from_prime_identity_branch_uniformity :
 907    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget →
 908      PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget
 909  prime_floor_prime_identity_forces_two_iff_no_non_two_composite_defect_character :
 910    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget ↔
 911      ¬ PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter
 912  prime_floor_prime_identity_forces_two_iff_no_non_two_composite_cost_defect_character :
 913    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget ↔
 914      ¬ PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter
 915  prime_floor_prime_identity_forces_two_not_iff_non_two_composite_cost_defect_character :
 916    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget ↔
 917      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter
 918  prime_floor_prime_identity_forces_two_iff_mixed_composite_cost_consistency :
 919    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget ↔
 920      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget
 921  prime_floor_prime_pair_product_cost_consistency_iff_mixed_composite_cost_consistency :
 922    PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget ↔
 923      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget
 924  prime_floor_two_prime_mixed_composite_cost_consistency_iff_no_non_two_mixed_character :
 925    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget ↔
 926      ¬ PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter
 927  prime_floor_two_prime_mixed_composite_cost_consistency_not_iff_non_two_mixed_character :
 928    ¬ PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget ↔
 929      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter
 930  prime_floor_two_prime_mixed_composite_cost_consistency_not_iff_non_two_composite_cost_defect_character :
 931    ¬ PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget ↔
 932      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter
 933  prime_floor_two_prime_reciprocal_excludes_identity_witness_from_prime_pair_product_cost_consistency :
 934    PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget →
 935      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget
 936  prime_floor_prime_reciprocal_witness_globalizes_split_from_two_prime_reciprocal_forces :
 937    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget →
 938      PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesSplitTarget
 939  prime_floor_two_prime_reciprocal_forces_from_split :
 940    PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesSplitTarget →
 941      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget
 942  prime_floor_prime_reciprocal_witness_globalizes_split_iff_two_prime_reciprocal_forces :
 943    PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesSplitTarget ↔
 944      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget
 945  prime_identity_trace_coherence_from_no_mixed_prime_orientation :
 946    PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget →
 947      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget
 948  prime_no_mixed_prime_orientation_iff_trace_coherence :
 949    PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget ↔
 950      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget
 951  prime_no_mixed_prime_orientation_from_branch_uniformity :
 952    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget →
 953      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget
 954  prime_identity_branch_uniformity_from_no_mixed_prime_orientation :
 955    PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget →
 956      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget
 957  prime_identity_branch_uniformity_iff_no_mixed_prime_orientation :
 958    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget ↔
 959      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget
 960  prime_no_mixed_prime_witnesses_iff_trace_coherence :
 961    PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget ↔
 962      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget
 963  coherent_prime_orientation_from_no_mixed_prime_witnesses :
 964    PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget →
 965      PRCJCost.PRCPrimeCalibrationForcesCoherentPrimeOrientationTarget
 966  no_mixed_prime_witnesses_from_coherent_prime_orientation :
 967    PRCJCost.PRCPrimeCalibrationForcesCoherentPrimeOrientationTarget →
 968      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget
 969  no_mixed_prime_witnesses_iff_coherent_prime_orientation :
 970    PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget ↔
 971      PRCJCost.PRCPrimeCalibrationForcesCoherentPrimeOrientationTarget
 972  two_prime_branch_controls_target_refuted :
 973    ¬ PRCJCost.PRCPrimeCalibrationForcesTwoPrimeBranchControlsPrimesTarget
 974  two_prime_branch_controls_from_coherent_prime_orientation :
 975    PRCJCost.PRCPrimeCalibrationForcesCoherentPrimeOrientationTarget →
 976      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeBranchControlsPrimesTarget
 977  coherent_prime_orientation_from_two_prime_branch_controls :
 978    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeBranchControlsPrimesTarget →
 979      PRCJCost.PRCPrimeCalibrationForcesCoherentPrimeOrientationTarget
 980  coherent_prime_orientation_iff_two_prime_branch_controls :
 981    PRCJCost.PRCPrimeCalibrationForcesCoherentPrimeOrientationTarget ↔
 982      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeBranchControlsPrimesTarget
 983  prime_identity_iff_two_prime_identity_target_refuted :
 984    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityIffTwoPrimeIdentityTarget
 985  prime_identity_forces_two_prime_identity_target_refuted :
 986    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget
 987  two_prime_reciprocal_excludes_prime_identity_target_refuted :
 988    ¬ PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget
 989  two_prime_reciprocal_excludes_prime_identity_witness_target_refuted :
 990    ¬ PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget
 991  two_prime_reciprocal_identity_prime_mixed_character :
 992    PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityPrimeMixedCharacter
 993  two_prime_reciprocal_identity_non_two_prime_mixed_character :
 994    PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter
 995  two_prime_reciprocal_identity_non_two_composite_defect_character :
 996    PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter
 997  two_prime_reciprocal_identity_non_two_composite_cost_defect_character :
 998    PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter
 999  calibrated_two_prime_mixed_composite_cost_consistency_target_refuted :
1000    ¬ PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget
1001  calibrated_prime_pair_product_cost_consistency_target_refuted :
1002    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget
1003  two_prime_reciprocal_forces_prime_reciprocal_target_refuted :
1004    ¬ PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget
1005  two_prime_reciprocal_trace_connected_target_refuted :
1006    ¬ PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget
1007  two_prime_identity_trace_connected_target_refuted :
1008    ¬ PRCJCost.PRCPrimeCalibrationForcesTwoPrimeIdentityTraceConnectedTarget
1009  prime_identity_iff_two_from_two_prime_branch_controls :
1010    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeBranchControlsPrimesTarget →
1011      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityIffTwoPrimeIdentityTarget
1012  two_prime_branch_controls_from_prime_identity_iff_two :
1013    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityIffTwoPrimeIdentityTarget →
1014      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeBranchControlsPrimesTarget
1015  two_prime_branch_controls_iff_prime_identity_iff_two :
1016    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeBranchControlsPrimesTarget ↔
1017      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityIffTwoPrimeIdentityTarget
1018  prime_identity_forces_two_from_identity_iff_two_target :
1019    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityIffTwoPrimeIdentityTarget →
1020      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget
1021  prime_identity_iff_two_from_identity_forces_two_target :
1022    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget →
1023      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityIffTwoPrimeIdentityTarget
1024  prime_identity_iff_two_iff_identity_forces_two :
1025    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityIffTwoPrimeIdentityTarget ↔
1026      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget
1027  two_prime_reciprocal_excludes_from_identity_forces_two_target :
1028    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget →
1029      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget
1030  prime_identity_forces_two_from_two_prime_reciprocal_excludes_target :
1031    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget →
1032      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget
1033  prime_identity_forces_two_target_iff_two_prime_reciprocal_excludes :
1034    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget ↔
1035      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget
1036  two_prime_reciprocal_excludes_from_two_prime_reciprocal_forces_target :
1037    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget →
1038      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget
1039  two_prime_reciprocal_forces_from_two_prime_reciprocal_excludes_target :
1040    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget →
1041      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget
1042  two_prime_reciprocal_excludes_target_iff_two_prime_reciprocal_forces :
1043    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget ↔
1044      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget
1045  two_prime_reciprocal_forces_from_identity_forces_two_target :
1046    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget →
1047      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget
1048  prime_identity_forces_two_from_two_prime_reciprocal_forces_target :
1049    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget →
1050      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget
1051  two_prime_reciprocal_forces_target_iff_identity_forces_two :
1052    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget ↔
1053      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget
1054  two_prime_reciprocal_forces_from_trace_connected_target :
1055    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget →
1056      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget
1057  two_prime_reciprocal_trace_connected_from_forces_target :
1058    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget →
1059      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget
1060  two_prime_reciprocal_trace_connected_target_iff_forces :
1061    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget ↔
1062      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget
1063  two_prime_reciprocal_trace_connected_from_identity_trace_connected_target :
1064    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeIdentityTraceConnectedTarget →
1065      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget
1066  two_prime_identity_trace_connected_from_reciprocal_trace_connected_target :
1067    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget →
1068      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeIdentityTraceConnectedTarget
1069  two_prime_reciprocal_trace_connected_target_iff_identity_trace_connected :
1070    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget ↔
1071      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeIdentityTraceConnectedTarget
1072  two_prime_identity_trace_connected_from_prime_identity_trace_transport_target :
1073    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceTransportTarget →
1074      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeIdentityTraceConnectedTarget
1075  prime_identity_trace_transport_from_two_prime_identity_trace_connected_target :
1076    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeIdentityTraceConnectedTarget →
1077      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceTransportTarget
1078  two_prime_identity_trace_connected_target_iff_prime_identity_trace_transport :
1079    PRCJCost.PRCPrimeCalibrationForcesTwoPrimeIdentityTraceConnectedTarget ↔
1080      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceTransportTarget
1081  prime_identity_canonical_add_trace_from_common_trace_target :
1082    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCommonTraceExtensionTarget →
1083      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCanonicalAddTraceTarget
1084  prime_identity_common_trace_from_canonical_add_trace_target :
1085    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCanonicalAddTraceTarget →
1086      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCommonTraceExtensionTarget
1087  prime_identity_canonical_add_trace_target_iff_common_trace :
1088    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCanonicalAddTraceTarget ↔
1089      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCommonTraceExtensionTarget
1090  prime_identity_canonical_add_trace_from_trace_transport_target :
1091    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceTransportTarget →
1092      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCanonicalAddTraceTarget
1093  prime_identity_trace_transport_from_canonical_add_trace_target :
1094    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCanonicalAddTraceTarget →
1095      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceTransportTarget
1096  prime_identity_canonical_add_trace_target_iff_trace_transport :
1097    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCanonicalAddTraceTarget ↔
1098      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceTransportTarget
1099  prime_identity_branch_uniformity_from_trace_coherence_target :
1100    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget →
1101      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget
1102  prime_identity_trace_coherence_from_branch_uniformity_target :
1103    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget →
1104      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget
1105  prime_identity_branch_uniformity_target_iff_trace_coherence :
1106    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget ↔
1107      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget
1108  prime_identity_canonical_add_trace_from_branch_uniformity_target :
1109    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget →
1110      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCanonicalAddTraceTarget
1111  prime_identity_branch_uniformity_from_canonical_add_trace_target :
1112    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCanonicalAddTraceTarget →
1113      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget
1114  prime_identity_branch_uniformity_target_iff_canonical_add_trace :
1115    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget ↔
1116      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCanonicalAddTraceTarget
1117  prime_identity_comparable_trace_from_trace_coherence :
1118    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget →
1119      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityComparableTraceTarget
1120  prime_identity_trace_coherence_from_comparable_trace :
1121    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityComparableTraceTarget →
1122      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget
1123  prime_identity_trace_coherence_iff_comparable_trace :
1124    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget ↔
1125      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityComparableTraceTarget
1126  prime_identity_comparable_trace_from_nonunit_identity_comparable :
1127    PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget →
1128      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityComparableTraceTarget
1129  nonunit_identity_comparable_trace_from_prime_identity_comparable :
1130    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityComparableTraceTarget →
1131      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget
1132  prime_identity_comparable_trace_iff_nonunit_identity_comparable :
1133    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityComparableTraceTarget ↔
1134      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget
1135  prime_identity_comparable_trace_iff_prime_floor_successor_transport :
1136    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityComparableTraceTarget ↔
1137      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget
1138  prime_identity_common_trace_from_trace_coherence :
1139    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget →
1140      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCommonTraceExtensionTarget
1141  prime_identity_trace_coherence_from_common_trace :
1142    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCommonTraceExtensionTarget →
1143      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget
1144  prime_identity_trace_coherence_iff_common_trace :
1145    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget ↔
1146      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCommonTraceExtensionTarget
1147  prime_identity_trace_transport_from_trace_coherence :
1148    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget →
1149      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceTransportTarget
1150  prime_identity_trace_coherence_iff_trace_transport :
1151    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget ↔
1152      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceTransportTarget
1153  prime_floor_no_mixed_prime_witnesses_from_nonunit_no_mixed_witnesses :
1154    PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesTarget →
1155      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget
1156  prime_floor_nonunit_no_mixed_witnesses_split_from_nonunit_no_mixed_witnesses :
1157    PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesTarget →
1158      PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesSplitTarget
1159  prime_floor_nonunit_no_mixed_witnesses_from_split :
1160    PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesSplitTarget →
1161      PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesTarget
1162  prime_floor_nonunit_no_mixed_witnesses_iff_split :
1163    PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesTarget ↔
1164      PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesSplitTarget
1165  prime_floor_prime_witnesses_control_from_mixed_reflects :
1166    PRCJCost.PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesTarget →
1167      PRCJCost.PRCPrimeCalibrationForcesPrimeWitnessesControlNonunitWitnessesTarget
1168  prime_floor_mixed_reflects_from_prime_witnesses_control :
1169    PRCJCost.PRCPrimeCalibrationForcesPrimeWitnessesControlNonunitWitnessesTarget →
1170      PRCJCost.PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesTarget
1171  prime_floor_prime_witnesses_control_iff_mixed_reflects :
1172    PRCJCost.PRCPrimeCalibrationForcesPrimeWitnessesControlNonunitWitnessesTarget ↔
1173      PRCJCost.PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesTarget
1174  prime_floor_mixed_reflection_split_from_reflects :
1175    PRCJCost.PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesTarget →
1176      PRCJCost.PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesSplitTarget
1177  prime_floor_mixed_reflection_from_split :
1178    PRCJCost.PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesSplitTarget →
1179      PRCJCost.PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesTarget
1180  prime_floor_mixed_reflection_iff_split :
1181    PRCJCost.PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesTarget ↔
1182      PRCJCost.PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesSplitTarget
1183  prime_floor_mixed_identity_reflects_prime_proved :
1184    PRCJCost.PRCPrimeCalibrationForcesMixedNonunitIdentityWitnessReflectsPrimeWitnessTarget
1185  prime_floor_mixed_reciprocal_reflects_prime_proved :
1186    PRCJCost.PRCPrimeCalibrationForcesMixedNonunitReciprocalWitnessReflectsPrimeWitnessTarget
1187  prime_floor_mixed_reflection_split_proved :
1188    PRCJCost.PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesSplitTarget
1189  prime_floor_mixed_reflection_proved :
1190    PRCJCost.PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesTarget
1191  prime_floor_prime_witnesses_control_nonunit_proved :
1192    PRCJCost.PRCPrimeCalibrationForcesPrimeWitnessesControlNonunitWitnessesTarget
1193  prime_floor_nonunit_no_mixed_split_from_no_mixed_prime_witnesses :
1194    PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget →
1195      PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesSplitTarget
1196  prime_floor_nonunit_no_mixed_from_no_mixed_prime_witnesses :
1197    PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget →
1198      PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesTarget
1199  prime_floor_nonunit_no_mixed_iff_no_mixed_prime_witnesses :
1200    PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesTarget ↔
1201      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget
1202  prime_floor_identity_witness_globalizes_from_local_exclusion :
1203    PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessLocalExclusionTarget →
1204      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget
1205  prime_floor_identity_witness_local_exclusion_from_globalizes :
1206    PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget →
1207      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessLocalExclusionTarget
1208  prime_floor_identity_witness_globalizes_iff_local_exclusion :
1209    PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget ↔
1210      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessLocalExclusionTarget
1211  prime_floor_nonunit_identity_comparable_trace_from_product_no_mixed :
1212    PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget →
1213      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget
1214  prime_floor_nonunit_identity_branch_transport_iff_comparable_trace :
1215    PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityBranchTransportTarget ↔
1216      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget
1217  prime_floor_product_no_mixed_iff_identity_comparable_trace :
1218    PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget ↔
1219      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget
1220  prime_floor_product_local_orientation_from_identity_comparable_trace :
1221    PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget →
1222      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitProductLocalOrientationTarget
1223  prime_floor_nonunit_local_orientation_from_identity_comparable_trace :
1224    PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget →
1225      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitLocalOrientationTarget
1226  prime_floor_nonunit_local_comparable_trace_from_identity_comparable_trace :
1227    PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget →
1228      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalComparableTraceTarget
1229  prime_floor_nonunit_identity_comparable_trace_from_local_comparable_trace :
1230    PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalComparableTraceTarget →
1231      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget
1232  prime_floor_nonunit_local_comparable_trace_iff_identity_comparable_trace :
1233    PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalComparableTraceTarget ↔
1234      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget
1235  prime_floor_nonunit_branch_agreement_from_transport_pair :
1236    PRCJCost.PRCPrimeCalibrationForcesNonunitBranchTransportPairTarget →
1237      PRCJCost.PRCPrimeCalibrationForcesNonunitBranchAgreementTarget
1238  prime_floor_nonunit_identity_branch_transport_from_branch_agreement :
1239    PRCJCost.PRCPrimeCalibrationForcesNonunitBranchAgreementTarget →
1240      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityBranchTransportTarget
1241  prime_floor_nonunit_reciprocal_branch_transport_from_branch_agreement :
1242    PRCJCost.PRCPrimeCalibrationForcesNonunitBranchAgreementTarget →
1243      PRCJCost.PRCPrimeCalibrationForcesNonunitReciprocalBranchTransportTarget
1244  prime_floor_nonunit_branch_transport_pair_from_branch_agreement :
1245    PRCJCost.PRCPrimeCalibrationForcesNonunitBranchAgreementTarget →
1246      PRCJCost.PRCPrimeCalibrationForcesNonunitBranchTransportPairTarget
1247  prime_floor_nonunit_branch_agreement_iff_transport_pair :
1248    PRCJCost.PRCPrimeCalibrationForcesNonunitBranchAgreementTarget ↔
1249      PRCJCost.PRCPrimeCalibrationForcesNonunitBranchTransportPairTarget
1250  prime_floor_nonunit_branch_agreement_from_local_identity_transport :
1251    PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalIdentityTransportTarget →
1252      PRCJCost.PRCPrimeCalibrationForcesNonunitBranchAgreementTarget
1253  prime_floor_nonunit_local_identity_transport_from_local_branch_agreement :
1254    PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalBranchAgreementTarget →
1255      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalIdentityTransportTarget
1256  prime_floor_nonunit_local_branch_agreement_from_local_identity_transport :
1257    PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalIdentityTransportTarget →
1258      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalBranchAgreementTarget
1259  prime_floor_nonunit_local_branch_agreement_iff_local_identity_transport :
1260    PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalBranchAgreementTarget ↔
1261      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalIdentityTransportTarget
1262  prime_floor_nonunit_local_comparable_trace_from_local_identity_transport :
1263    PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalIdentityTransportTarget →
1264      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalComparableTraceTarget
1265  prime_floor_nonunit_local_identity_transport_from_local_comparable_trace :
1266    PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalComparableTraceTarget →
1267      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalIdentityTransportTarget
1268  prime_floor_nonunit_local_identity_transport_iff_local_comparable_trace :
1269    PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalIdentityTransportTarget ↔
1270      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalComparableTraceTarget
1271  prime_floor_nonunit_branch_agreement_from_coherent :
1272    PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget →
1273      PRCJCost.PRCPrimeCalibrationForcesNonunitBranchAgreementTarget
1274  prime_floor_nonunit_local_branch_agreement_from_coherent :
1275    PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget →
1276      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalBranchAgreementTarget
1277  prime_floor_nonunit_coherent_from_local_branch_agreement :
1278    PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalBranchAgreementTarget →
1279      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget
1280  prime_floor_nonunit_orbit_orientation_coherent_iff_local_branch_agreement :
1281    PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget ↔
1282      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalBranchAgreementTarget
1283  prime_floor_nonunit_identity_comparable_trace_iff_successor_transport :
1284    PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget ↔
1285      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget
1286  prime_floor_identity_extends_successor_step_from_successor_transport :
1287    PRCJCost.PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget →
1288      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentityExtendsSuccessorStepTarget
1289  prime_floor_identity_contracts_successor_step_from_successor_transport :
1290    PRCJCost.PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget →
1291      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentityContractsSuccessorStepTarget
1292  prime_floor_identity_successor_step_pair_from_successor_transport :
1293    PRCJCost.PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget →
1294      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget
1295  prime_floor_successor_transport_from_successor_step_pair :
1296    PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget →
1297      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget
1298  prime_floor_successor_transport_iff_successor_step_pair :
1299    PRCJCost.PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget ↔
1300      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget
1301  prime_identity_witness_globalizes_nonunit_from_successor_transport :
1302    PRCJCost.PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget →
1303      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityWitnessGlobalizesNonunitTarget
1304  prime_floor_successor_transport_from_prime_identity_witness_globalizes :
1305    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityWitnessGlobalizesNonunitTarget →
1306      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget
1307  prime_floor_successor_transport_iff_prime_identity_witness_globalizes :
1308    PRCJCost.PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget ↔
1309      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityWitnessGlobalizesNonunitTarget
1310  prime_identity_witness_globalizes_nonunit_from_no_mixed_prime_witnesses :
1311    PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget →
1312      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityWitnessGlobalizesNonunitTarget
1313  no_mixed_prime_witnesses_from_prime_identity_witness_globalizes :
1314    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityWitnessGlobalizesNonunitTarget →
1315      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget
1316  prime_identity_witness_globalizes_nonunit_iff_no_mixed_prime_witnesses :
1317    PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityWitnessGlobalizesNonunitTarget ↔
1318      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget
1319  prime_floor_identity_successor_step_pair_from_identity_comparable_trace :
1320    PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget →
1321      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget
1322  prime_floor_nonunit_identity_comparable_trace_from_successor_step_pair :
1323    PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget →
1324      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget
1325  prime_floor_nonunit_identity_comparable_trace_iff_successor_step_pair :
1326    PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget ↔
1327      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget
1328  prime_floor_product_no_mixed_from_successor_step_pair :
1329    PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget →
1330      PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget
1331  prime_floor_identity_successor_step_pair_from_product_no_mixed :
1332    PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget →
1333      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget
1334  prime_floor_product_no_mixed_iff_successor_step_pair :
1335    PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget ↔
1336      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget
1337  prime_floor_nonunit_coherent_from_successor_step_pair :
1338    PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget →
1339      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget
1340  prime_floor_identity_successor_step_pair_from_nonunit_coherent :
1341    PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget →
1342      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget
1343  prime_floor_nonunit_coherent_iff_successor_step_pair :
1344    PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget ↔
1345      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget
1346  prime_floor_successor_transport_local_adjacent_target_refuted :
1347    ¬ PRCJCost.PRCPrimeFloorSuccessorTransportLocalAdjacentTarget
1348  prime_floor_successor_transport_local_adjacent_iff_local_successor_transport :
1349    PRCJCost.PRCPrimeFloorSuccessorTransportLocalAdjacentTarget ↔
1350      (PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitLocalOrientationTarget ∧
1351        PRCJCost.PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget)
1352  prime_floor_successor_transport_local_adjacent_iff_nonunit_coherent :
1353    PRCJCost.PRCPrimeFloorSuccessorTransportLocalAdjacentTarget ↔
1354      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget
1355  prime_floor_nonunit_orbit_orientation_coherent_iff_local_no_mixed :
1356    PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget ↔
1357      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalNoMixedTarget
1358  prime_floor_nonunit_orbit_orientation_coherent_sharpened_target_refuted :
1359    ¬ PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentSharpenedTarget
1360  prime_floor_nonunit_orbit_orientation_coherent_iff_sharpened :
1361    PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget ↔
1362      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentSharpenedTarget
1363  prime_floor_product_local_orientation_sharpened_target_refuted :
1364    ¬ PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitProductLocalOrientationSharpenedTarget
1365  prime_floor_no_adjacent_mixed_orientation_target_refuted :
1366    ¬ PRCJCost.PRCPrimeCalibrationForcesPrimeFloorNoAdjacentMixedOrientationTarget
1367  prime_floor_successor_transport_sharpened_refuted :
1368    ¬ PRCJCost.PRCPrimeFloorSuccessorTransportSharpenedTarget
1369  prime_to_coherent_orientation_refuted :
1370    ¬ PRCJCost.PRCPrimeCalibrationForcesCoherentPrimeOrientationTarget
1371  coherent_prime_orientation_propagation_refuted :
1372    ¬ PRCJCost.PRCCoherentPrimeOrientationPropagatesToGlobalTarget
1373  admissible_prime_orientation_coherent :
1374    PRCJCost.PRCAdmissibleCharacterPrimeOrientationCoherentTarget
1375  admissible_signed_unit_calibration_refuted :
1376    ¬ PRCJCost.PRCAdmissibleCharacterSignedUnitCalibratedTarget
1377  signed_coherent_prime_orientation_propagation :
1378    PRCJCost.PRCSignedCoherentPrimeOrientationPropagatesToGlobalTarget
1379  prime_propagation_sharpened_refuted :
1380    ¬ PRCJCost.PRCPrimeCalibrationPropagationSharpenedTarget
1381  native_cost_rigidity_sharpened_refuted :
1382    ¬ PRCJCost.PRCNativeCostCharacterRigiditySharpenedTarget
1383  external_foundation_parsing_schema :
1384    ∀ (ExternalFoundation : Type)
1385      (FaithfulParse : ExternalFoundation → FormalSystem → Prop),
1386      ExternalFoundationParsingTarget ExternalFoundation FaithfulParse =
1387        ExternalFoundationParsingTarget ExternalFoundation FaithfulParse
1388
1389/-- Top-level conditional certificate: all built PRC surfaces compose, with the
1390repaired/refuted native-cost ledger exposed by name. -/
1391structure PRCUniversalFoundationConditionalCertificate : Prop where
1392  kernel : KernelFirstPassCertificate
1393  real_complete_ordered_field :
1394    PRCRealCompleteOrderedFieldPromotedCertificate
1395  trace_logic : TraceLogicCertificate
1396  formal_system : FormalSystemCertificate
1397  inevitability : PRCInevitabilityCertificate
1398  recognizer_bridge : PRCRecognizerBridgeCertificate
1399  native_cost_blocker : PRCJCost.PRCNativeCostUniquenessBlockerCertificate
1400  open_targets : PRCUniversalFoundationOpenTargets
1401  no_project_local_axioms_audit :
1402    StrengthTag.classicalExtension = StrengthTag.classicalExtension
1403
1404/-- Final PRC universal-foundation certificate. The certificate closes the
1405top-level theorem by carrying the built PRC surfaces together with the exact
1406native-cost ledger: the repaired signed/prime/zero-calibrated uniqueness route
1407is proved, while the weaker unsigned routes are recorded as refuted targets. -/
1408structure PRCUniversalFoundationCertificate : Prop where
1409  delta_kernel : KernelFirstPassCertificate
1410  real_complete_ordered_field :
1411    PRCRealCompleteOrderedFieldPromotedCertificate
1412  trace_logic : TraceLogicCertificate
1413  formal_system : FormalSystemCertificate
1414  inevitability : PRCInevitabilityCertificate
1415  recognizer_bridge : PRCRecognizerBridgeCertificate
1416  native_cost_blocker : PRCJCost.PRCNativeCostUniquenessBlockerCertificate
1417  repaired_refuted_native_cost_ledger : PRCUniversalFoundationOpenTargets
1418  conditional_certificate : PRCUniversalFoundationConditionalCertificate
1419  no_project_local_axioms_audit :
1420    StrengthTag.classicalExtension = StrengthTag.classicalExtension
1421
1422theorem prc_universal_foundation_conditional_certificate :
1423    PRCUniversalFoundationConditionalCertificate where
1424  kernel := kernel_first_pass_certificate
1425  real_complete_ordered_field :=
1426    prc_real_complete_ordered_field_promoted_certificate
1427  trace_logic := trace_logic_certificate
1428  formal_system := formal_system_certificate
1429  inevitability := prc_inevitability_certificate
1430  recognizer_bridge := prc_recognizer_bridge_certificate
1431  native_cost_blocker := PRCJCost.prc_native_cost_uniqueness_blocker_certificate
1432  open_targets := {
1433    zero_calibrated_native_cost_uniqueness_refuted :=
1434      PRCJCost.PRCZeroCalibratedNativeCostUniquenessTarget_refuted
1435    zero_calibrated_native_cost_character_factorization :=
1436      PRCJCost.PRCZeroCalibratedNativeCostCharacterFactorizationTarget_proved
1437    zero_calibrated_native_cost_signed_admissible_factorization_refuted :=
1438      PRCJCost.PRCZeroCalibratedNativeCostSignedAdmissibleCharacterFactorizationTarget_refuted
1439    zero_calibration_signed_unit_refuted :=
1440      PRCJCost.PRCZeroCalibrationForcesNativeCostSignedUnitCalibrationTarget_refuted
1441    zero_calibrated_prime_signed_strengthened_native_cost_uniqueness :=
1442      PRCJCost.PRCZeroCalibratedPrimeSignedStrengthenedNativeCostUniquenessTarget_proved
1443    native_cost_signed_admissible_character_rigidity :=
1444      PRCJCost.PRCNativeCostSignedAdmissibleCharacterRigidityTarget_proved
1445    old_native_cost_character_rigidity_refuted :=
1446      PRCJCost.PRCNativeCostCharacterRigidityTarget_refuted
1447    old_native_cost_sharpened_refuted :=
1448      PRCJCost.PRCNativeCostUniquenessSharpenedTarget_refuted
1449    two_to_prime_calibration_refuted :=
1450      PRCJCost.PRCTwoCalibrationForcesPrimeCalibrationTarget_refuted
1451    prime_calibration_propagation_refuted :=
1452      PRCJCost.PRCPrimeCalibrationPropagationTarget_refuted
1453    prime_global_orientation_refuted :=
1454      PRCJCost.PRCPrimeCalibrationForcesGlobalOrientationTarget_refuted
1455    coherent_prime_orientation :=
1456      PRCJCost.PRCCharacterTwoPrimeBranchControlsPrimes_of_coherent
1457    two_prime_branch_controls_primes :=
1458      PRCJCost.PRCCharacterPrimeOrientationCoherent_of_local_two_prime_branch_controls
1459    prime_identity_iff_two_prime_identity :=
1460      PRCJCost.PRCCharacterPrimeIdentityIffTwoPrimeIdentity_of_local_two_prime_branch_controls
1461    prime_identity_forces_two_prime_identity :=
1462      PRCJCost.PRCCharacterPrimeIdentityForcesTwoPrimeIdentity_of_identity_iff_two
1463    two_prime_reciprocal_excludes_prime_identity :=
1464      PRCJCost.PRCCharacterPrimeIdentityForcesTwoPrimeIdentity_iff_two_prime_reciprocal_excludes
1465    two_prime_reciprocal_excludes_prime_identity_witness :=
1466      PRCJCost.PRCCharacterTwoPrimeReciprocalExcludesPrimeIdentity_iff_witness
1467    two_prime_reciprocal_identity_prime_mixed :=
1468      PRCJCost.PRCCharacterTwoPrimeReciprocalIdentityPrimeMixed_iff_non_two
1469    two_prime_reciprocal_identity_non_two_prime_mixed :=
1470      PRCJCost.PRCCharacterTwoPrimeReciprocalIdentityNonTwoPrimeMixed_iff_composite_defect_of_character
1471    two_prime_reciprocal_identity_non_two_composite_defect :=
1472      PRCJCost.PRCCharacterTwoPrimeReciprocalIdentityNonTwoCompositeDefect_iff_cost_defect
1473    two_prime_reciprocal_identity_non_two_composite_cost_defect :=
1474      PRCJCost.PRCCharacterTwoPrimeReciprocalIdentityNonTwoCompositeDefect_of_cost_defect
1475    two_prime_mixed_composite_cost_consistency_target_refuted :=
1476      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_refuted
1477    prime_pair_product_cost_consistency_target_refuted :=
1478      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_refuted
1479    two_prime_reciprocal_forces_prime_reciprocal :=
1480      PRCJCost.PRCCharacterTwoPrimeReciprocalForcesPrimeReciprocal_of_reciprocal_witness_globalizes
1481    two_prime_reciprocal_trace_connected :=
1482      PRCJCost.PRCCharacterTwoPrimeReciprocalRespectsTraceConnected_iff_forces
1483    two_prime_identity_trace_connected :=
1484      PRCJCost.PRCCharacterTwoPrimeIdentityRespectsTraceConnected_of_prime_identity_trace_connected
1485    no_mixed_prime_orientation :=
1486      PRCJCost.PRCCharacterNoMixedPrimeWitnesses_iff_no_mixed_prime_orientation
1487    mixed_prime_witnesses :=
1488      PRCJCost.PRCCharacterMixedPrimeWitnesses_iff_pair_witnesses
1489    mixed_prime_pair_witnesses :=
1490      PRCJCost.PRCCharacterMixedPrimePairWitnesses_iff_same_or_distinct
1491    same_prime_mixed_pair_witnesses :=
1492      PRCJCost.PRCCharacterSamePrimeMixedPairWitnesses_absurd
1493    distinct_prime_mixed_pair_witnesses :=
1494      PRCJCost.PRCCharacterDistinctPrimeMixedPairWitnesses_absurd_of_branch_uniform
1495    prime_identity_witness_excludes_reciprocal :=
1496      PRCJCost.PRCCharacterPrimeIdentityWitnessExcludesReciprocal_iff_no_mixed_prime_orientation
1497    prime_reciprocal_witness_globalizes :=
1498      PRCJCost.PRCCharacterPrimeReciprocalWitnessGlobalizes_of_local_no_mixed_prime_orientation
1499    prime_reciprocal_forces_two_prime_reciprocal :=
1500      PRCJCost.PRCCharacterPrimeReciprocalForcesTwoPrimeReciprocal_of_reciprocal_witness_globalizes
1501    prime_reciprocal_witness_globalizes_split :=
1502      PRCJCost.PRCCharacterPrimeReciprocalWitnessGlobalizes_iff_split
1503    prime_reciprocal_forces_two_from_reciprocal_twist_identity_forces_two := by
1504      intro χ
1505      exact PRCJCost.PRCCharacterPrimeReciprocalForcesTwoPrimeReciprocal_of_reciprocal_twist_identity_forces_two
1506    prime_identity_forces_two_from_reciprocal_twist_reciprocal_forces_two := by
1507      intro χ
1508      exact PRCJCost.PRCCharacterPrimeIdentityForcesTwoPrimeIdentity_of_reciprocal_twist_reciprocal_forces_two
1509    prime_identity_trace_coherence :=
1510      PRCJCost.PRCCharacterPrimeIdentityBranchUniform_iff_trace_coherence
1511    prime_identity_branch_uniform :=
1512      PRCJCost.PRCCharacterPrimeIdentityBranchUniform_iff_identity_iff_two
1513    prime_axis_trace_connected := PRCJCost.PRCPrimeAxisTraceConnected_proved
1514    prime_identity_respects_trace_connected :=
1515      PRCJCost.PRCCharacterPrimeIdentityRespectsCanonicalAddTrace_iff_trace_connected
1516    prime_identity_respects_common_trace_extension :=
1517      PRCJCost.PRCCharacterPrimeIdentityRespectsCanonicalAddTrace_iff_common_trace_extension
1518    prime_identity_respects_canonical_add_trace :=
1519      PRCJCost.PRCCharacterPrimeIdentityBranchUniform_iff_canonical_add_trace
1520    prime_identity_respects_comparable_trace :=
1521      PRCJCost.PRCCharacterPrimeIdentityRespectsComparableTrace_iff_trace_coherence
1522    prime_identity_trace_coherence_target_refuted :=
1523      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget_refuted
1524    prime_identity_branch_uniformity_target_refuted :=
1525      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_refuted
1526    prime_identity_trace_transport_target_refuted :=
1527      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceTransportTarget_refuted
1528    prime_identity_common_trace_extension_target_refuted :=
1529      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCommonTraceExtensionTarget_refuted
1530    prime_identity_canonical_add_trace_target_refuted :=
1531      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCanonicalAddTraceTarget_refuted
1532    prime_identity_comparable_trace_target_refuted :=
1533      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityComparableTraceTarget_refuted
1534    orbit_successor_identity_target_refuted :=
1535      PRCJCost.PRCPrimeCalibrationForcesOrbitSuccessorIdentityTarget_refuted
1536    orbit_successor_transport_target_refuted :=
1537      PRCJCost.PRCPrimeCalibrationForcesOrbitSuccessorTransportTarget_refuted
1538    prime_floor_successor_transport_target_refuted :=
1539      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget_refuted
1540    prime_identity_witness_globalizes_nonunit_target_refuted :=
1541      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityWitnessGlobalizesNonunitTarget_refuted
1542    prime_floor_identity_extends_successor_step_target_refuted :=
1543      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentityExtendsSuccessorStepTarget_refuted
1544    prime_floor_identity_contracts_successor_step_target_refuted :=
1545      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentityContractsSuccessorStepTarget_refuted
1546    prime_floor_identity_successor_step_pair_target_refuted :=
1547      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget_refuted
1548    prime_floor_nonunit_local_orientation_target_refuted :=
1549      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitLocalOrientationTarget_refuted
1550    prime_floor_nonunit_product_local_orientation_target_refuted :=
1551      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitProductLocalOrientationTarget_refuted
1552    prime_floor_nonunit_orbit_orientation_coherent_target_refuted :=
1553      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget_refuted
1554    prime_floor_no_mixed_nonunit_orbit_orientation_target_refuted :=
1555      PRCJCost.PRCPrimeCalibrationForcesNoMixedNonunitOrbitOrientationTarget_refuted
1556    prime_floor_nonunit_identity_branch_transport_target_refuted :=
1557      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityBranchTransportTarget_refuted
1558    prime_floor_nonunit_identity_witness_globalizes_target_refuted :=
1559      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget_refuted
1560    prime_floor_nonunit_identity_witness_excludes_reciprocal_target_refuted :=
1561      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessExcludesReciprocalTarget_refuted
1562    prime_floor_nonunit_no_mixed_witnesses_target_refuted :=
1563      PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesTarget_refuted
1564    prime_floor_no_mixed_prime_witnesses_target_refuted :=
1565      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_refuted
1566    prime_floor_mixed_prime_witness_character :=
1567      PRCJCost.PRCPrimeCalibratedMixedPrimeWitnessesCharacter_of_pair_witness_character
1568        (PRCJCost.PRCPrimeCalibratedMixedPrimePairWitnessCharacter_of_distinct
1569          (PRCJCost.PRCPrimeCalibratedDistinctPrimeMixedPairWitnessCharacter_of_non_two_mixed
1570            (PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter_of_two_adic_axis_twist
1571              (PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter_of_ratio_character_axis_twist
1572                PRCJCost.PRCTwoAdicAxisTwistRatioCharacter_constructed))))
1573    prime_floor_mixed_prime_pair_witness_character :=
1574      PRCJCost.PRCPrimeCalibratedMixedPrimePairWitnessCharacter_of_distinct
1575        (PRCJCost.PRCPrimeCalibratedDistinctPrimeMixedPairWitnessCharacter_of_non_two_mixed
1576          (PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter_of_two_adic_axis_twist
1577            (PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter_of_ratio_character_axis_twist
1578              PRCJCost.PRCTwoAdicAxisTwistRatioCharacter_constructed)))
1579    prime_floor_same_prime_mixed_pair_witness_character_refuted :=
1580      PRCJCost.PRCPrimeCalibratedSamePrimeMixedPairWitnessCharacter_absurd
1581    prime_floor_distinct_prime_mixed_pair_witness_character :=
1582      PRCJCost.PRCPrimeCalibratedDistinctPrimeMixedPairWitnessCharacter_of_non_two_mixed
1583        (PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter_of_two_adic_axis_twist
1584          (PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter_of_ratio_character_axis_twist
1585            PRCJCost.PRCTwoAdicAxisTwistRatioCharacter_constructed))
1586    prime_floor_prime_identity_witness_excludes_reciprocal_target_refuted :=
1587      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityWitnessExcludesReciprocalTarget_refuted
1588    prime_floor_prime_reciprocal_witness_globalizes_target_refuted :=
1589      PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget_refuted
1590    prime_floor_prime_reciprocal_forces_two_prime_reciprocal_target_refuted :=
1591      PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalForcesTwoPrimeReciprocalTarget_refuted
1592    prime_floor_prime_reciprocal_witness_globalizes_split_target_refuted :=
1593      PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesSplitTarget_refuted
1594    prime_floor_prime_witnesses_control_nonunit_target :=
1595      PRCJCost.PRCPrimeCalibrationForcesPrimeWitnessesControlNonunitWitnessesTarget_proved
1596    prime_floor_mixed_nonunit_witnesses_reflect_prime_target :=
1597      PRCJCost.PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesTarget_proved
1598    prime_floor_mixed_nonunit_identity_witness_reflects_prime_target :=
1599      PRCJCost.PRCPrimeCalibrationForcesMixedNonunitIdentityWitnessReflectsPrimeWitnessTarget_proved
1600    prime_floor_mixed_nonunit_reciprocal_witness_reflects_prime_target :=
1601      PRCJCost.PRCPrimeCalibrationForcesMixedNonunitReciprocalWitnessReflectsPrimeWitnessTarget_proved
1602    prime_floor_mixed_nonunit_witnesses_reflect_prime_split_target :=
1603      PRCJCost.PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesSplitTarget_proved
1604    prime_floor_nonunit_no_mixed_witnesses_split_target_refuted :=
1605      PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesSplitTarget_refuted
1606    prime_floor_nonunit_identity_witness_local_exclusion_target_refuted :=
1607      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessLocalExclusionTarget_refuted
1608    prime_floor_nonunit_reciprocal_branch_transport_target_refuted :=
1609      PRCJCost.PRCPrimeCalibrationForcesNonunitReciprocalBranchTransportTarget_refuted
1610    prime_floor_nonunit_branch_transport_pair_target_refuted :=
1611      PRCJCost.PRCPrimeCalibrationForcesNonunitBranchTransportPairTarget_refuted
1612    prime_floor_nonunit_identity_comparable_trace_target_refuted :=
1613      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget_refuted
1614    prime_floor_nonunit_branch_agreement_target_refuted :=
1615      PRCJCost.PRCPrimeCalibrationForcesNonunitBranchAgreementTarget_refuted
1616    prime_floor_nonunit_orbit_orientation_local_branch_agreement_target_refuted :=
1617      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalBranchAgreementTarget_refuted
1618    prime_floor_nonunit_orbit_orientation_local_identity_transport_target_refuted :=
1619      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalIdentityTransportTarget_refuted
1620    prime_floor_nonunit_orbit_orientation_local_comparable_trace_target_refuted :=
1621      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalComparableTraceTarget_refuted
1622    prime_floor_nonunit_orbit_orientation_local_no_mixed_target_refuted :=
1623      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalNoMixedTarget_refuted
1624    prime_floor_nonunit_orbit_orientation_local_product_no_mixed_target_refuted :=
1625      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalProductNoMixedTarget_refuted
1626    prime_floor_no_mixed_nonunit_from_product_no_mixed :=
1627      PRCJCost.PRCPrimeCalibrationForcesNoMixedNonunitOrbitOrientationTarget_of_product_no_mixed
1628    prime_floor_product_no_mixed_from_no_mixed_nonunit :=
1629      PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_of_no_mixed_nonunit
1630    prime_floor_product_no_mixed_iff_no_mixed_nonunit :=
1631      PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_iff_no_mixed_nonunit
1632    prime_floor_product_no_mixed_from_identity_branch_transport :=
1633      PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_of_identity_branch_transport
1634    prime_floor_nonunit_identity_branch_transport_from_comparable_trace :=
1635      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityBranchTransportTarget_of_comparable_trace
1636    prime_floor_nonunit_coherent_from_product_no_mixed :=
1637      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget_of_product_no_mixed
1638    prime_floor_product_no_mixed_iff_nonunit_coherent :=
1639      PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_iff_nonunit_coherent
1640    prime_floor_nonunit_identity_branch_transport_from_product_no_mixed :=
1641      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityBranchTransportTarget_of_product_no_mixed
1642    prime_floor_product_no_mixed_iff_identity_branch_transport :=
1643      PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_iff_identity_branch_transport
1644    prime_floor_identity_witness_globalizes_from_identity_branch_transport :=
1645      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget_of_identity_branch_transport
1646    prime_floor_identity_branch_transport_from_identity_witness_globalizes :=
1647      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityBranchTransportTarget_of_identity_witness_globalizes
1648    prime_floor_identity_witness_globalizes_iff_identity_branch_transport :=
1649      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget_iff_identity_branch_transport
1650    prime_floor_identity_witness_globalizes_from_product_no_mixed :=
1651      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget_of_product_no_mixed
1652    prime_floor_product_no_mixed_from_identity_witness_globalizes :=
1653      PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_of_identity_witness_globalizes
1654    prime_floor_product_no_mixed_iff_identity_witness_globalizes :=
1655      PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_iff_identity_witness_globalizes
1656    prime_floor_nonunit_coherent_from_identity_witness_globalizes :=
1657      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget_of_identity_witness_globalizes
1658    prime_floor_identity_witness_globalizes_from_nonunit_coherent :=
1659      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget_of_nonunit_coherent
1660    prime_floor_nonunit_coherent_iff_identity_witness_globalizes :=
1661      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget_iff_identity_witness_globalizes
1662    prime_floor_identity_witness_excludes_reciprocal_from_no_mixed :=
1663      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessExcludesReciprocalTarget_of_no_mixed
1664    prime_floor_no_mixed_from_identity_witness_excludes_reciprocal :=
1665      PRCJCost.PRCPrimeCalibrationForcesNoMixedNonunitOrbitOrientationTarget_of_identity_witness_excludes
1666    prime_floor_identity_witness_excludes_reciprocal_iff_no_mixed :=
1667      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessExcludesReciprocalTarget_iff_no_mixed
1668    prime_floor_no_mixed_witnesses_from_identity_witness_excludes_reciprocal :=
1669      PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesTarget_of_identity_witness_excludes
1670    prime_floor_identity_witness_excludes_reciprocal_from_no_mixed_witnesses :=
1671      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessExcludesReciprocalTarget_of_no_mixed_witnesses
1672    prime_floor_no_mixed_witnesses_iff_identity_witness_excludes_reciprocal :=
1673      PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesTarget_iff_identity_witness_excludes
1674    prime_floor_no_mixed_prime_witnesses_from_no_mixed_prime_orientation :=
1675      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_of_no_mixed_prime_orientation
1676    prime_floor_no_mixed_prime_orientation_from_no_mixed_prime_witnesses :=
1677      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget_of_no_mixed_prime_witnesses
1678    prime_floor_no_mixed_prime_witnesses_iff_no_mixed_prime_orientation :=
1679      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_iff_no_mixed_prime_orientation
1680    prime_floor_prime_identity_witness_excludes_reciprocal_from_no_mixed_prime_orientation :=
1681      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityWitnessExcludesReciprocalTarget_of_no_mixed_prime_orientation
1682    prime_floor_no_mixed_prime_orientation_from_identity_witness_excludes_reciprocal :=
1683      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget_of_identity_witness_excludes_reciprocal
1684    prime_floor_prime_identity_witness_excludes_reciprocal_iff_no_mixed_prime_orientation :=
1685      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityWitnessExcludesReciprocalTarget_iff_no_mixed_prime_orientation
1686    prime_floor_no_mixed_prime_witnesses_from_identity_witness_excludes_reciprocal :=
1687      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_of_identity_witness_excludes_reciprocal
1688    prime_floor_prime_identity_witness_excludes_reciprocal_from_no_mixed_prime_witnesses :=
1689      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityWitnessExcludesReciprocalTarget_of_no_mixed_prime_witnesses
1690    prime_floor_no_mixed_prime_witnesses_iff_identity_witness_excludes_reciprocal :=
1691      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_iff_identity_witness_excludes_reciprocal
1692    prime_floor_no_mixed_prime_witnesses_iff_not_mixed_prime_witnesses :=
1693      fun χ => PRCJCost.PRCCharacterNoMixedPrimeWitnesses_iff_not_mixed_prime_witnesses
1694    prime_floor_mixed_prime_pair_witnesses_from_mixed_prime_witnesses :=
1695      fun χ => PRCJCost.PRCCharacterMixedPrimePairWitnesses_of_mixed_prime_witnesses
1696    prime_floor_mixed_prime_witnesses_from_pair_witnesses :=
1697      fun χ => PRCJCost.PRCCharacterMixedPrimeWitnesses_of_pair_witnesses
1698    prime_floor_mixed_prime_witnesses_iff_pair_witnesses :=
1699      fun χ => PRCJCost.PRCCharacterMixedPrimeWitnesses_iff_pair_witnesses
1700    prime_floor_no_mixed_prime_witnesses_iff_not_mixed_prime_pair_witnesses :=
1701      fun χ => PRCJCost.PRCCharacterNoMixedPrimeWitnesses_iff_not_mixed_prime_pair_witnesses
1702    prime_floor_mixed_prime_pair_witnesses_same_or_distinct :=
1703      fun χ => PRCJCost.PRCCharacterMixedPrimePairWitnesses_same_or_distinct
1704    prime_floor_mixed_prime_pair_witnesses_from_same_or_distinct :=
1705      fun χ => PRCJCost.PRCCharacterMixedPrimePairWitnesses_of_same_or_distinct
1706    prime_floor_mixed_prime_pair_witnesses_iff_same_or_distinct :=
1707      fun χ => PRCJCost.PRCCharacterMixedPrimePairWitnesses_iff_same_or_distinct
1708    prime_floor_no_mixed_prime_witnesses_iff_no_same_and_no_distinct_pair :=
1709      fun χ => PRCJCost.PRCCharacterNoMixedPrimeWitnesses_iff_no_same_and_no_distinct_pair
1710    prime_floor_same_prime_mixed_pair_witnesses_absurd :=
1711      fun χ => PRCJCost.PRCCharacterSamePrimeMixedPairWitnesses_absurd
1712    prime_floor_no_mixed_prime_witnesses_iff_not_distinct_prime_pair :=
1713      fun χ => PRCJCost.PRCCharacterNoMixedPrimeWitnesses_iff_not_distinct_prime_pair
1714    prime_floor_distinct_prime_mixed_pair_witnesses_absurd_from_branch_uniform :=
1715      fun χ => PRCJCost.PRCCharacterDistinctPrimeMixedPairWitnesses_absurd_of_branch_uniform
1716    prime_floor_prime_identity_branch_uniform_from_local_no_distinct_prime_pair :=
1717      fun χ => PRCJCost.PRCCharacterPrimeIdentityBranchUniform_of_local_no_distinct_prime_pair
1718    prime_floor_prime_identity_branch_uniform_iff_no_distinct_prime_pair_of_local :=
1719      fun χ => PRCJCost.PRCCharacterPrimeIdentityBranchUniform_iff_no_distinct_prime_pair_of_local
1720    prime_floor_prime_identity_branch_uniform_from_identity_iff_two :=
1721      fun χ => PRCJCost.PRCCharacterPrimeIdentityBranchUniform_of_identity_iff_two
1722    prime_floor_prime_identity_iff_two_from_branch_uniform :=
1723      fun χ => PRCJCost.PRCCharacterPrimeIdentityIffTwoPrimeIdentity_of_branch_uniform
1724    prime_floor_prime_identity_branch_uniform_iff_identity_iff_two :=
1725      fun χ => PRCJCost.PRCCharacterPrimeIdentityBranchUniform_iff_identity_iff_two
1726    prime_floor_prime_reciprocal_witness_globalizes_from_no_mixed_prime_orientation :=
1727      PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget_of_no_mixed_prime_orientation
1728    prime_floor_no_mixed_prime_orientation_from_reciprocal_witness_globalizes :=
1729      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget_of_reciprocal_witness_globalizes
1730    prime_floor_prime_reciprocal_witness_globalizes_iff_no_mixed_prime_orientation :=
1731      PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget_iff_no_mixed_prime_orientation
1732    prime_floor_prime_reciprocal_witness_globalizes_iff_identity_witness_excludes_reciprocal :=
1733      PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget_iff_identity_witness_excludes_reciprocal
1734    prime_floor_prime_reciprocal_forces_two_from_reciprocal_witness_globalizes :=
1735      PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalForcesTwoPrimeReciprocalTarget_of_reciprocal_witness_globalizes
1736    prime_floor_two_prime_reciprocal_forces_from_reciprocal_witness_globalizes :=
1737      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget_of_reciprocal_witness_globalizes
1738    prime_floor_prime_reciprocal_witness_globalizes_split_from_reciprocal_witness_globalizes :=
1739      PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesSplitTarget_of_reciprocal_witness_globalizes
1740    prime_floor_prime_reciprocal_witness_globalizes_from_split :=
1741      PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget_of_split
1742    prime_floor_prime_reciprocal_witness_globalizes_iff_split :=
1743      PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget_iff_split
1744    prime_floor_prime_reciprocal_forces_two_from_identity_forces_two :=
1745      PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalForcesTwoPrimeReciprocalTarget_of_identity_forces_two
1746    prime_floor_prime_identity_forces_two_from_reciprocal_forces_two :=
1747      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_of_prime_reciprocal_forces_two
1748    prime_floor_prime_reciprocal_forces_two_iff_identity_forces_two :=
1749      PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalForcesTwoPrimeReciprocalTarget_iff_identity_forces_two
1750    prime_floor_two_prime_reciprocal_excludes_identity_witness_from_excludes :=
1751      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_of_two_prime_reciprocal_excludes
1752    prime_floor_two_prime_reciprocal_excludes_from_identity_witness_excludes :=
1753      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget_of_witness
1754    prime_floor_two_prime_reciprocal_excludes_iff_identity_witness_excludes :=
1755      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget_iff_witness
1756    prime_floor_prime_identity_forces_two_from_two_prime_reciprocal_excludes_identity_witness :=
1757      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_of_two_prime_reciprocal_excludes_witness
1758    prime_floor_two_prime_reciprocal_excludes_identity_witness_from_identity_forces_two :=
1759      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_of_identity_forces_two
1760    prime_floor_prime_identity_forces_two_iff_two_prime_reciprocal_excludes_identity_witness :=
1761      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_iff_two_prime_reciprocal_excludes_witness
1762    prime_floor_two_prime_reciprocal_excludes_identity_witness_from_no_mixed_character :=
1763      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_of_no_mixed_character
1764    prime_floor_no_mixed_character_from_two_prime_reciprocal_excludes_identity_witness :=
1765      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityPrimeMixedCharacter_absurd_of_witness_excludes
1766    prime_floor_two_prime_reciprocal_excludes_identity_witness_iff_no_mixed_character :=
1767      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_mixed_character
1768    prime_floor_non_two_mixed_character_from_mixed_character :=
1769      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter_of_mixed
1770    prime_floor_mixed_character_from_non_two_mixed_character :=
1771      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityPrimeMixedCharacter_of_non_two_mixed
1772    prime_floor_mixed_character_iff_non_two_mixed_character :=
1773      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityPrimeMixedCharacter_iff_non_two
1774    prime_floor_two_prime_reciprocal_excludes_identity_witness_iff_no_non_two_mixed_character :=
1775      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_non_two_mixed_character
1776    prime_floor_composite_defect_character_from_non_two_mixed_character :=
1777      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter_of_non_two_mixed
1778    prime_floor_non_two_mixed_character_from_composite_defect_character :=
1779      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter_of_composite_defect
1780    prime_floor_non_two_mixed_character_iff_composite_defect_character :=
1781      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter_iff_composite_defect
1782    prime_floor_two_prime_reciprocal_excludes_identity_witness_iff_no_composite_defect_character :=
1783      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_composite_defect_character
1784    prime_floor_composite_cost_defect_character_from_composite_defect_character :=
1785      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter_of_composite_defect
1786    prime_floor_composite_defect_character_from_composite_cost_defect_character :=
1787      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter_of_cost_defect
1788    prime_floor_composite_defect_character_iff_composite_cost_defect_character :=
1789      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter_iff_cost_defect
1790    prime_floor_two_prime_reciprocal_excludes_identity_witness_iff_no_composite_cost_defect_character :=
1791      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_composite_cost_defect_character
1792    prime_floor_two_prime_mixed_composite_cost_consistency_from_no_cost_defect :=
1793      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_of_no_composite_cost_defect
1794    prime_floor_no_cost_defect_from_two_prime_mixed_composite_cost_consistency :=
1795      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter_absurd_of_mixed_composite_consistency
1796    prime_floor_two_prime_mixed_composite_cost_consistency_iff_no_cost_defect :=
1797      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_iff_no_composite_cost_defect_character
1798    prime_floor_two_prime_reciprocal_excludes_identity_witness_iff_mixed_composite_cost_consistency :=
1799      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_mixed_composite_cost_consistency
1800    prime_floor_two_prime_reciprocal_excludes_identity_witness_from_mixed_composite_cost_consistency_direct :=
1801      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_of_mixed_composite_cost_consistency_direct
1802    prime_floor_two_prime_mixed_composite_cost_consistency_from_prime_pair_product_cost_consistency :=
1803      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_of_prime_pair_product_cost_consistency
1804    prime_floor_prime_pair_product_cost_consistency_from_prime_calibration_propagation :=
1805      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_of_prime_calibration_propagation
1806    prime_floor_prime_pair_product_cost_consistency_from_coherent_prime_orientation :=
1807      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_of_coherent_prime_orientation
1808    prime_floor_coherent_prime_orientation_from_prime_pair_product_cost_consistency :=
1809      PRCJCost.PRCPrimeCalibrationForcesCoherentPrimeOrientationTarget_of_prime_pair_product_cost_consistency
1810    prime_floor_prime_pair_product_cost_consistency_iff_coherent_prime_orientation :=
1811      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_iff_coherent_prime_orientation
1812    prime_floor_prime_pair_product_cost_consistency_from_no_mixed_prime_witnesses :=
1813      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_of_no_mixed_prime_witnesses
1814    prime_floor_no_mixed_prime_witnesses_from_prime_pair_product_cost_consistency :=
1815      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_of_prime_pair_product_cost_consistency
1816    prime_floor_prime_pair_product_cost_consistency_iff_no_mixed_prime_witnesses :=
1817      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_iff_no_mixed_prime_witnesses
1818    prime_floor_no_mixed_prime_witness_character_absurd_from_no_mixed_prime_witnesses :=
1819      PRCJCost.PRCPrimeCalibratedMixedPrimeWitnessesCharacter_absurd_of_no_mixed_prime_witnesses
1820    prime_floor_no_mixed_prime_witnesses_from_no_mixed_prime_witness_character :=
1821      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_of_no_mixed_prime_witness_character
1822    prime_floor_no_mixed_prime_witnesses_iff_no_mixed_prime_witness_character :=
1823      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_iff_no_mixed_prime_witness_character
1824    prime_floor_prime_pair_product_cost_consistency_iff_no_mixed_prime_witness_character :=
1825      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_iff_no_mixed_prime_witness_character
1826    prime_floor_no_mixed_prime_witnesses_not_from_mixed_prime_witness_character :=
1827      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_not_of_mixed_prime_witness_character
1828    prime_floor_mixed_prime_witness_character_from_not_no_mixed_prime_witnesses :=
1829      PRCJCost.PRCPrimeCalibratedMixedPrimeWitnessesCharacter_of_not_no_mixed_prime_witnesses
1830    prime_floor_no_mixed_prime_witnesses_not_iff_mixed_prime_witness_character :=
1831      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_not_iff_mixed_prime_witness_character
1832    prime_floor_prime_pair_product_cost_consistency_not_from_mixed_prime_witness_character :=
1833      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_not_of_mixed_prime_witness_character
1834    prime_floor_mixed_prime_witness_character_from_not_prime_pair_product_cost_consistency :=
1835      PRCJCost.PRCPrimeCalibratedMixedPrimeWitnessesCharacter_of_not_prime_pair_product_cost_consistency
1836    prime_floor_prime_pair_product_cost_consistency_not_iff_mixed_prime_witness_character :=
1837      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_not_iff_mixed_prime_witness_character
1838    prime_floor_mixed_prime_pair_witness_character_from_mixed_prime_witness_character :=
1839      PRCJCost.PRCPrimeCalibratedMixedPrimePairWitnessCharacter_of_mixed_prime_witness_character
1840    prime_floor_mixed_prime_witness_character_from_pair_witness_character :=
1841      PRCJCost.PRCPrimeCalibratedMixedPrimeWitnessesCharacter_of_pair_witness_character
1842    prime_floor_mixed_prime_witness_character_iff_pair_witness_character :=
1843      PRCJCost.PRCPrimeCalibratedMixedPrimeWitnessesCharacter_iff_pair_witness_character
1844    prime_floor_no_mixed_prime_witnesses_iff_no_mixed_prime_pair_witness_character :=
1845      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_iff_no_mixed_prime_pair_witness_character
1846    prime_floor_no_mixed_prime_witnesses_not_iff_mixed_prime_pair_witness_character :=
1847      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_not_iff_mixed_prime_pair_witness_character
1848    prime_floor_prime_pair_product_cost_consistency_iff_no_mixed_prime_pair_witness_character :=
1849      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_iff_no_mixed_prime_pair_witness_character
1850    prime_floor_prime_pair_product_cost_consistency_not_iff_mixed_prime_pair_witness_character :=
1851      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_not_iff_mixed_prime_pair_witness_character
1852    prime_floor_mixed_prime_pair_witness_character_same_or_distinct :=
1853      PRCJCost.PRCPrimeCalibratedMixedPrimePairWitnessCharacter_same_or_distinct
1854    prime_floor_mixed_prime_pair_witness_character_from_same_or_distinct :=
1855      PRCJCost.PRCPrimeCalibratedMixedPrimePairWitnessCharacter_of_same_or_distinct
1856    prime_floor_mixed_prime_pair_witness_character_iff_same_or_distinct :=
1857      PRCJCost.PRCPrimeCalibratedMixedPrimePairWitnessCharacter_iff_same_or_distinct
1858    prime_floor_no_mixed_prime_witnesses_iff_no_same_and_no_distinct_pair_witness_character :=
1859      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_iff_no_same_and_no_distinct_pair_witness_character
1860    prime_floor_no_mixed_prime_witnesses_not_iff_same_or_distinct_pair_witness_character :=
1861      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_not_iff_same_or_distinct_pair_witness_character
1862    prime_floor_prime_pair_product_cost_consistency_iff_no_same_and_no_distinct_pair_witness_character :=
1863      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_iff_no_same_and_no_distinct_pair_witness_character
1864    prime_floor_prime_pair_product_cost_consistency_not_iff_same_or_distinct_pair_witness_character :=
1865      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_not_iff_same_or_distinct_pair_witness_character
1866    prime_floor_same_prime_mixed_pair_witness_character_absurd :=
1867      PRCJCost.PRCPrimeCalibratedSamePrimeMixedPairWitnessCharacter_absurd
1868    prime_floor_no_mixed_prime_witnesses_iff_no_distinct_prime_pair_witness_character :=
1869      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_iff_no_distinct_prime_pair_witness_character
1870    prime_floor_no_mixed_prime_witnesses_not_iff_distinct_prime_pair_witness_character :=
1871      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_not_iff_distinct_prime_pair_witness_character
1872    prime_floor_prime_pair_product_cost_consistency_iff_no_distinct_prime_pair_witness_character :=
1873      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_iff_no_distinct_prime_pair_witness_character
1874    prime_floor_prime_pair_product_cost_consistency_not_iff_distinct_prime_pair_witness_character :=
1875      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_not_iff_distinct_prime_pair_witness_character
1876    prime_floor_prime_identity_branch_uniformity_from_no_distinct_prime_pair_witness_character :=
1877      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_of_no_distinct_prime_pair_witness_character
1878    prime_floor_no_distinct_prime_pair_witness_character_from_prime_identity_branch_uniformity :=
1879      PRCJCost.PRCPrimeCalibrationForcesNoDistinctPrimePairWitnessCharacter_of_prime_identity_branch_uniformity
1880    prime_floor_prime_identity_branch_uniformity_iff_no_distinct_prime_pair_witness_character :=
1881      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_iff_no_distinct_prime_pair_witness_character
1882    prime_floor_prime_identity_branch_uniformity_not_iff_distinct_prime_pair_witness_character :=
1883      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_not_iff_distinct_prime_pair_witness_character
1884    prime_floor_prime_pair_product_cost_consistency_iff_prime_identity_branch_uniformity :=
1885      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_iff_prime_identity_branch_uniformity
1886    prime_floor_prime_identity_branch_uniformity_from_identity_iff_two :=
1887      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_of_identity_iff_two
1888    prime_floor_prime_identity_iff_two_from_branch_uniformity :=
1889      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityIffTwoPrimeIdentityTarget_of_branch_uniformity
1890    prime_floor_prime_identity_branch_uniformity_iff_identity_iff_two :=
1891      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_iff_identity_iff_two
1892    prime_floor_prime_identity_branch_uniformity_iff_identity_forces_two :=
1893      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_iff_identity_forces_two
1894    prime_floor_prime_pair_product_cost_consistency_iff_prime_identity_forces_two :=
1895      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_iff_prime_identity_forces_two
1896    prime_floor_prime_identity_forces_two_not_iff_distinct_prime_pair_witness_character :=
1897      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_not_iff_distinct_prime_pair_witness_character
1898    prime_floor_prime_identity_forces_two_iff_no_two_prime_mixed_character :=
1899      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_iff_no_two_prime_mixed_character
1900    prime_floor_prime_identity_forces_two_iff_no_non_two_mixed_character :=
1901      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_iff_no_non_two_mixed_character
1902    prime_floor_non_two_mixed_character_from_two_adic_axis_twist :=
1903      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter_of_two_adic_axis_twist
1904    prime_floor_prime_calibration_from_two_adic_axis_twist := by
1905      intro χ htwist
1906      exact PRCJCost.PRCCharacterPrimeDirectionCalibrated_of_two_adic_axis_twist htwist
1907    prime_floor_calibrated_two_adic_axis_twist_from_ratio_character_axis_twist :=
1908      PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter_of_ratio_character_axis_twist
1909    prime_floor_ratio_character_axis_twist_from_calibrated_two_adic_axis_twist :=
1910      PRCJCost.PRCTwoAdicAxisTwistRatioCharacter_of_calibrated_two_adic_axis_twist
1911    prime_floor_calibrated_two_adic_axis_twist_iff_ratio_character_axis_twist :=
1912      PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter_iff_ratio_character_axis_twist
1913    prime_floor_ratio_character_axis_twist_absurd_from_no_calibrated_twist :=
1914      PRCJCost.PRCTwoAdicAxisTwistRatioCharacter_absurd_of_no_calibrated_twist
1915    prime_floor_two_adic_axis_twist_absurd_from_no_non_two_mixed :=
1916      PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter_absurd_of_no_non_two_mixed
1917    prime_floor_two_adic_axis_twist_absurd_from_mixed_composite_cost_consistency :=
1918      PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter_absurd_of_mixed_composite_cost_consistency
1919    prime_floor_two_adic_axis_twist_absurd_from_prime_identity_forces_two :=
1920      PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter_absurd_of_prime_identity_forces_two
1921    prime_floor_two_adic_axis_twist_absurd_from_prime_pair_product_cost_consistency :=
1922      PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter_absurd_of_prime_pair_product_cost_consistency
1923    prime_floor_mixed_composite_cost_consistency_not_from_two_adic_axis_twist :=
1924      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_not_of_two_adic_axis_twist
1925    prime_floor_prime_identity_forces_two_not_from_two_adic_axis_twist :=
1926      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_not_of_two_adic_axis_twist
1927    prime_floor_prime_pair_product_cost_consistency_not_from_two_adic_axis_twist :=
1928      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_not_of_two_adic_axis_twist
1929    prime_floor_ratio_character_axis_twist_absurd_from_mixed_composite_cost_consistency :=
1930      PRCJCost.PRCTwoAdicAxisTwistRatioCharacter_absurd_of_mixed_composite_cost_consistency
1931    prime_floor_ratio_character_axis_twist_absurd_from_prime_identity_forces_two :=
1932      PRCJCost.PRCTwoAdicAxisTwistRatioCharacter_absurd_of_prime_identity_forces_two
1933    prime_floor_ratio_character_axis_twist_absurd_from_prime_pair_product_cost_consistency :=
1934      PRCJCost.PRCTwoAdicAxisTwistRatioCharacter_absurd_of_prime_pair_product_cost_consistency
1935    prime_floor_mixed_composite_cost_consistency_not_from_ratio_character_axis_twist :=
1936      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_not_of_ratio_character_axis_twist
1937    prime_floor_prime_identity_forces_two_not_from_ratio_character_axis_twist :=
1938      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_not_of_ratio_character_axis_twist
1939    prime_floor_prime_pair_product_cost_consistency_not_from_ratio_character_axis_twist :=
1940      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_not_of_ratio_character_axis_twist
1941    prime_floor_two_three_mixed_not_composite :=
1942      PRCJCost.twoThreePrimeMixedDirection_not_crossEq_composite
1943    prime_floor_two_three_mixed_not_composite_recip :=
1944      PRCJCost.twoThreePrimeMixedDirection_not_crossEq_composite_recip
1945    prime_floor_two_adic_axis_twist_two_three_mixed_image := by
1946      intro χ hχ htwist
1947      exact PRCJCost.PRCCharacterTwoAdicAxisTwist_two_three_mixed_image hχ htwist
1948    prime_floor_two_adic_axis_twist_two_three_local_orientation_absurd := by
1949      intro χ hχ htwist
1950      exact
1951        PRCJCost.PRCCharacterTwoAdicAxisTwist_two_three_local_orientation_absurd
1952          hχ htwist
1953    prime_floor_ratio_character_axis_twist_forces_two_three_local_orientation_failure :=
1954      PRCJCost.PRCTwoAdicAxisTwistRatioCharacter_forces_two_three_local_orientation_failure
1955    prime_floor_two_three_failure_character_from_ratio_character_axis_twist :=
1956      PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter_of_ratio_character_axis_twist
1957    prime_floor_ratio_character_axis_twist_from_two_three_failure_character :=
1958      PRCJCost.PRCTwoAdicAxisTwistRatioCharacter_of_two_three_local_orientation_failure_character
1959    prime_floor_two_three_failure_character_iff_ratio_character_axis_twist :=
1960      PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter_iff_ratio_character_axis_twist
1961    prime_floor_two_three_failure_character_iff_calibrated_two_adic_axis_twist :=
1962      PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter_iff_calibrated_two_adic_axis_twist
1963    prime_floor_two_three_local_orientation_target_from_no_ratio_character_axis_twist :=
1964      PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_of_no_ratio_character_axis_twist
1965    prime_floor_ratio_character_axis_twist_absurd_from_two_three_local_orientation_target :=
1966      PRCJCost.PRCTwoAdicAxisTwistRatioCharacter_absurd_of_two_three_local_orientation_target
1967    prime_floor_two_three_local_orientation_target_iff_no_ratio_character_axis_twist :=
1968      PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_iff_no_ratio_character_axis_twist
1969    prime_floor_two_three_failure_character_absurd_from_two_three_local_orientation_target :=
1970      PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter_absurd_of_two_three_local_orientation_target
1971    prime_floor_two_three_local_orientation_target_iff_no_failure_character :=
1972      PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_iff_no_failure_character
1973    prime_floor_two_three_local_orientation_target_iff_no_calibrated_two_adic_axis_twist :=
1974      PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_iff_no_calibrated_two_adic_axis_twist
1975    prime_floor_calibrated_two_adic_axis_twist_absurd_from_two_three_local_orientation_target :=
1976      PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter_absurd_of_two_three_local_orientation_target
1977    prime_floor_two_three_local_orientation_target_from_no_failure_character :=
1978      PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_of_no_failure_character
1979    prime_floor_two_three_local_fork_certificate :=
1980      PRCJCost.prcTwoThreeCompositeLocalForkCertificate
1981    prime_floor_calibrated_two_adic_axis_twist_from_two_three_failure_character :=
1982      PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter_of_two_three_local_orientation_failure_character
1983    prime_floor_non_two_mixed_character_from_two_three_failure_character :=
1984      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter_of_two_three_local_orientation_failure_character
1985    prime_floor_composite_defect_character_from_two_three_failure_character :=
1986      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter_of_two_three_local_orientation_failure_character
1987    prime_floor_composite_cost_defect_character_from_two_three_failure_character :=
1988      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter_of_two_three_local_orientation_failure_character
1989    prime_floor_mixed_composite_cost_consistency_not_from_two_three_failure_character :=
1990      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_not_of_two_three_local_orientation_failure_character
1991    prime_floor_prime_identity_forces_two_not_from_two_three_failure_character :=
1992      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_not_of_two_three_local_orientation_failure_character
1993    prime_floor_prime_pair_product_cost_consistency_not_from_two_three_failure_character :=
1994      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_not_of_two_three_local_orientation_failure_character
1995    prime_floor_two_three_failure_character_absurd_from_no_calibrated_two_adic_axis_twist :=
1996      PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter_absurd_of_no_calibrated_two_adic_axis_twist
1997    prime_floor_two_three_failure_character_absurd_from_no_non_two_mixed_character :=
1998      PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter_absurd_of_no_non_two_mixed_character
1999    prime_floor_two_three_failure_character_absurd_from_no_non_two_composite_defect_character :=
2000      PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter_absurd_of_no_non_two_composite_defect_character
2001    prime_floor_two_three_failure_character_absurd_from_no_non_two_composite_cost_defect_character :=
2002      PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter_absurd_of_no_non_two_composite_cost_defect_character
2003    prime_floor_two_three_local_orientation_target_from_no_calibrated_two_adic_axis_twist :=
2004      PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_of_no_calibrated_two_adic_axis_twist
2005    prime_floor_two_three_local_orientation_target_from_no_non_two_mixed_character :=
2006      PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_of_no_non_two_mixed_character
2007    prime_floor_two_three_local_orientation_target_from_no_non_two_composite_defect_character :=
2008      PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_of_no_non_two_composite_defect_character
2009    prime_floor_two_three_local_orientation_target_from_no_non_two_composite_cost_defect_character :=
2010      PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_of_no_non_two_composite_cost_defect_character
2011    prime_floor_two_three_local_orientation_target_from_mixed_composite_cost_consistency :=
2012      PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_of_mixed_composite_cost_consistency
2013    prime_floor_two_three_local_orientation_target_from_prime_identity_forces_two :=
2014      PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_of_prime_identity_forces_two
2015    prime_floor_two_three_local_orientation_target_from_prime_pair_product_cost_consistency :=
2016      PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_of_prime_pair_product_cost_consistency
2017    prime_floor_two_three_failure_character_absurd_from_mixed_composite_cost_consistency :=
2018      PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter_absurd_of_mixed_composite_cost_consistency
2019    prime_floor_two_three_failure_character_absurd_from_prime_identity_forces_two :=
2020      PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter_absurd_of_prime_identity_forces_two
2021    prime_floor_two_three_failure_character_absurd_from_prime_pair_product_cost_consistency :=
2022      PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter_absurd_of_prime_pair_product_cost_consistency
2023    prime_floor_ratio_character_axis_twist_absurd_from_prime_identity_branch_uniformity :=
2024      PRCJCost.PRCTwoAdicAxisTwistRatioCharacter_absurd_of_prime_identity_branch_uniformity
2025    prime_floor_two_three_failure_character_absurd_from_prime_identity_branch_uniformity :=
2026      PRCJCost.PRCTwoThreeCompositeLocalOrientationFailureCharacter_absurd_of_prime_identity_branch_uniformity
2027    prime_floor_two_three_local_orientation_target_from_prime_identity_branch_uniformity :=
2028      PRCJCost.PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_of_prime_identity_branch_uniformity
2029    prime_floor_prime_identity_forces_two_iff_no_non_two_composite_defect_character :=
2030      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_iff_no_non_two_composite_defect_character
2031    prime_floor_prime_identity_forces_two_iff_no_non_two_composite_cost_defect_character :=
2032      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_iff_no_non_two_composite_cost_defect_character
2033    prime_floor_prime_identity_forces_two_not_iff_non_two_composite_cost_defect_character :=
2034      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_not_iff_non_two_composite_cost_defect_character
2035    prime_floor_prime_identity_forces_two_iff_mixed_composite_cost_consistency :=
2036      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_iff_mixed_composite_cost_consistency
2037    prime_floor_prime_pair_product_cost_consistency_iff_mixed_composite_cost_consistency :=
2038      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_iff_mixed_composite_cost_consistency
2039    prime_floor_two_prime_mixed_composite_cost_consistency_iff_no_non_two_mixed_character :=
2040      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_iff_no_non_two_mixed_character
2041    prime_floor_two_prime_mixed_composite_cost_consistency_not_iff_non_two_mixed_character :=
2042      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_not_iff_non_two_mixed_character
2043    prime_floor_two_prime_mixed_composite_cost_consistency_not_iff_non_two_composite_cost_defect_character :=
2044      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_not_iff_non_two_composite_cost_defect_character
2045    prime_floor_two_prime_reciprocal_excludes_identity_witness_from_prime_pair_product_cost_consistency :=
2046      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_of_prime_pair_product_cost_consistency
2047    prime_floor_prime_reciprocal_witness_globalizes_split_from_two_prime_reciprocal_forces :=
2048      PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesSplitTarget_of_two_prime_reciprocal_forces
2049    prime_floor_two_prime_reciprocal_forces_from_split :=
2050      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget_of_split
2051    prime_floor_prime_reciprocal_witness_globalizes_split_iff_two_prime_reciprocal_forces :=
2052      PRCJCost.PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesSplitTarget_iff_two_prime_reciprocal_forces
2053    prime_identity_trace_coherence_from_no_mixed_prime_orientation :=
2054      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget_of_no_mixed_prime_orientation
2055    prime_no_mixed_prime_orientation_iff_trace_coherence :=
2056      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget_iff_trace_coherence
2057    prime_no_mixed_prime_orientation_from_branch_uniformity :=
2058      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget_of_branch_uniformity
2059    prime_identity_branch_uniformity_from_no_mixed_prime_orientation :=
2060      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_of_no_mixed_prime_orientation
2061    prime_identity_branch_uniformity_iff_no_mixed_prime_orientation :=
2062      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_iff_no_mixed_prime_orientation
2063    prime_no_mixed_prime_witnesses_iff_trace_coherence :=
2064      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_iff_trace_coherence
2065    coherent_prime_orientation_from_no_mixed_prime_witnesses :=
2066      PRCJCost.PRCPrimeCalibrationForcesCoherentPrimeOrientationTarget_of_no_mixed_prime_witnesses
2067    no_mixed_prime_witnesses_from_coherent_prime_orientation :=
2068      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_of_coherent_prime_orientation
2069    no_mixed_prime_witnesses_iff_coherent_prime_orientation :=
2070      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_iff_coherent_prime_orientation
2071    two_prime_branch_controls_target_refuted :=
2072      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeBranchControlsPrimesTarget_refuted
2073    two_prime_branch_controls_from_coherent_prime_orientation :=
2074      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeBranchControlsPrimesTarget_of_coherent_prime_orientation
2075    coherent_prime_orientation_from_two_prime_branch_controls :=
2076      PRCJCost.PRCPrimeCalibrationForcesCoherentPrimeOrientationTarget_of_two_prime_branch_controls
2077    coherent_prime_orientation_iff_two_prime_branch_controls :=
2078      PRCJCost.PRCPrimeCalibrationForcesCoherentPrimeOrientationTarget_iff_two_prime_branch_controls
2079    prime_identity_iff_two_prime_identity_target_refuted :=
2080      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityIffTwoPrimeIdentityTarget_refuted
2081    prime_identity_forces_two_prime_identity_target_refuted :=
2082      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_refuted
2083    two_prime_reciprocal_excludes_prime_identity_target_refuted :=
2084      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget_refuted
2085    two_prime_reciprocal_excludes_prime_identity_witness_target_refuted :=
2086      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_refuted
2087    two_prime_reciprocal_identity_prime_mixed_character :=
2088      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityPrimeMixedCharacter_of_non_two_mixed
2089        (PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter_of_two_adic_axis_twist
2090          (PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter_of_ratio_character_axis_twist
2091            PRCJCost.PRCTwoAdicAxisTwistRatioCharacter_constructed))
2092    two_prime_reciprocal_identity_non_two_prime_mixed_character :=
2093      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter_of_two_adic_axis_twist
2094        (PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter_of_ratio_character_axis_twist
2095          PRCJCost.PRCTwoAdicAxisTwistRatioCharacter_constructed)
2096    two_prime_reciprocal_identity_non_two_composite_defect_character :=
2097      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter_of_non_two_mixed
2098        (PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter_of_two_adic_axis_twist
2099          (PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter_of_ratio_character_axis_twist
2100            PRCJCost.PRCTwoAdicAxisTwistRatioCharacter_constructed))
2101    two_prime_reciprocal_identity_non_two_composite_cost_defect_character :=
2102      PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter_of_composite_defect
2103        (PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter_of_non_two_mixed
2104          (PRCJCost.PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter_of_two_adic_axis_twist
2105            (PRCJCost.PRCPrimeCalibratedTwoAdicAxisTwistCharacter_of_ratio_character_axis_twist
2106              PRCJCost.PRCTwoAdicAxisTwistRatioCharacter_constructed)))
2107    calibrated_two_prime_mixed_composite_cost_consistency_target_refuted :=
2108      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_refuted
2109    calibrated_prime_pair_product_cost_consistency_target_refuted :=
2110      PRCJCost.PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_refuted
2111    two_prime_reciprocal_forces_prime_reciprocal_target_refuted :=
2112      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget_refuted
2113    two_prime_reciprocal_trace_connected_target_refuted :=
2114      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget_refuted
2115    two_prime_identity_trace_connected_target_refuted :=
2116      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeIdentityTraceConnectedTarget_refuted
2117    prime_identity_iff_two_from_two_prime_branch_controls :=
2118      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityIffTwoPrimeIdentityTarget_of_two_prime_branch_controls
2119    two_prime_branch_controls_from_prime_identity_iff_two :=
2120      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeBranchControlsPrimesTarget_of_prime_identity_iff_two
2121    two_prime_branch_controls_iff_prime_identity_iff_two :=
2122      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeBranchControlsPrimesTarget_iff_prime_identity_iff_two
2123    prime_identity_forces_two_from_identity_iff_two_target :=
2124      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_of_identity_iff_two
2125    prime_identity_iff_two_from_identity_forces_two_target :=
2126      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityIffTwoPrimeIdentityTarget_of_identity_forces_two
2127    prime_identity_iff_two_iff_identity_forces_two :=
2128      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityIffTwoPrimeIdentityTarget_iff_identity_forces_two
2129    two_prime_reciprocal_excludes_from_identity_forces_two_target :=
2130      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget_of_identity_forces_two
2131    prime_identity_forces_two_from_two_prime_reciprocal_excludes_target :=
2132      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_of_two_prime_reciprocal_excludes
2133    prime_identity_forces_two_target_iff_two_prime_reciprocal_excludes :=
2134      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_iff_two_prime_reciprocal_excludes
2135    two_prime_reciprocal_excludes_from_two_prime_reciprocal_forces_target :=
2136      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget_of_two_prime_reciprocal_forces
2137    two_prime_reciprocal_forces_from_two_prime_reciprocal_excludes_target :=
2138      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget_of_two_prime_reciprocal_excludes
2139    two_prime_reciprocal_excludes_target_iff_two_prime_reciprocal_forces :=
2140      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget_iff_two_prime_reciprocal_forces
2141    two_prime_reciprocal_forces_from_identity_forces_two_target :=
2142      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget_of_identity_forces_two
2143    prime_identity_forces_two_from_two_prime_reciprocal_forces_target :=
2144      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_of_two_prime_reciprocal_forces
2145    two_prime_reciprocal_forces_target_iff_identity_forces_two :=
2146      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget_iff_identity_forces_two
2147    two_prime_reciprocal_forces_from_trace_connected_target :=
2148      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget_of_trace_connected
2149    two_prime_reciprocal_trace_connected_from_forces_target :=
2150      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget_of_forces
2151    two_prime_reciprocal_trace_connected_target_iff_forces :=
2152      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget_iff_forces
2153    two_prime_reciprocal_trace_connected_from_identity_trace_connected_target :=
2154      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget_of_identity_trace_connected
2155    two_prime_identity_trace_connected_from_reciprocal_trace_connected_target :=
2156      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeIdentityTraceConnectedTarget_of_reciprocal_trace_connected
2157    two_prime_reciprocal_trace_connected_target_iff_identity_trace_connected :=
2158      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget_iff_identity_trace_connected
2159    two_prime_identity_trace_connected_from_prime_identity_trace_transport_target :=
2160      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeIdentityTraceConnectedTarget_of_prime_identity_trace_transport
2161    prime_identity_trace_transport_from_two_prime_identity_trace_connected_target :=
2162      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceTransportTarget_of_two_prime_identity_trace_connected
2163    two_prime_identity_trace_connected_target_iff_prime_identity_trace_transport :=
2164      PRCJCost.PRCPrimeCalibrationForcesTwoPrimeIdentityTraceConnectedTarget_iff_prime_identity_trace_transport
2165    prime_identity_canonical_add_trace_from_common_trace_target :=
2166      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCanonicalAddTraceTarget_of_common_trace_extension
2167    prime_identity_common_trace_from_canonical_add_trace_target :=
2168      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCommonTraceExtensionTarget_of_canonical_add_trace
2169    prime_identity_canonical_add_trace_target_iff_common_trace :=
2170      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCanonicalAddTraceTarget_iff_common_trace_extension
2171    prime_identity_canonical_add_trace_from_trace_transport_target :=
2172      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCanonicalAddTraceTarget_of_trace_transport
2173    prime_identity_trace_transport_from_canonical_add_trace_target :=
2174      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceTransportTarget_of_canonical_add_trace
2175    prime_identity_canonical_add_trace_target_iff_trace_transport :=
2176      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCanonicalAddTraceTarget_iff_trace_transport
2177    prime_identity_branch_uniformity_from_trace_coherence_target :=
2178      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_of_trace_coherence
2179    prime_identity_trace_coherence_from_branch_uniformity_target :=
2180      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget_of_branch_uniformity
2181    prime_identity_branch_uniformity_target_iff_trace_coherence :=
2182      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_iff_trace_coherence
2183    prime_identity_canonical_add_trace_from_branch_uniformity_target :=
2184      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCanonicalAddTraceTarget_of_branch_uniformity
2185    prime_identity_branch_uniformity_from_canonical_add_trace_target :=
2186      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_of_canonical_add_trace
2187    prime_identity_branch_uniformity_target_iff_canonical_add_trace :=
2188      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_iff_canonical_add_trace
2189    prime_identity_comparable_trace_from_trace_coherence :=
2190      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityComparableTraceTarget_of_trace_coherence
2191    prime_identity_trace_coherence_from_comparable_trace :=
2192      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget_of_comparable_trace
2193    prime_identity_trace_coherence_iff_comparable_trace :=
2194      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget_iff_comparable_trace
2195    prime_identity_comparable_trace_from_nonunit_identity_comparable :=
2196      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityComparableTraceTarget_of_nonunit_identity_comparable_trace
2197    nonunit_identity_comparable_trace_from_prime_identity_comparable :=
2198      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget_of_prime_identity_comparable_trace
2199    prime_identity_comparable_trace_iff_nonunit_identity_comparable :=
2200      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityComparableTraceTarget_iff_nonunit_identity_comparable_trace
2201    prime_identity_comparable_trace_iff_prime_floor_successor_transport :=
2202      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityComparableTraceTarget_iff_prime_floor_successor_transport
2203    prime_identity_common_trace_from_trace_coherence :=
2204      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityCommonTraceExtensionTarget_of_trace_coherence
2205    prime_identity_trace_coherence_from_common_trace :=
2206      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget_of_common_trace_extension
2207    prime_identity_trace_coherence_iff_common_trace :=
2208      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget_iff_common_trace_extension
2209    prime_identity_trace_transport_from_trace_coherence :=
2210      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceTransportTarget_of_trace_coherence
2211    prime_identity_trace_coherence_iff_trace_transport :=
2212      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget_iff_trace_transport
2213    prime_floor_no_mixed_prime_witnesses_from_nonunit_no_mixed_witnesses :=
2214      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_of_nonunit_no_mixed_witnesses
2215    prime_floor_nonunit_no_mixed_witnesses_split_from_nonunit_no_mixed_witnesses :=
2216      PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesSplitTarget_of_nonunit_no_mixed_witnesses
2217    prime_floor_nonunit_no_mixed_witnesses_from_split :=
2218      PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesTarget_of_split
2219    prime_floor_nonunit_no_mixed_witnesses_iff_split :=
2220      PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesTarget_iff_split
2221    prime_floor_prime_witnesses_control_from_mixed_reflects :=
2222      PRCJCost.PRCPrimeCalibrationForcesPrimeWitnessesControlNonunitWitnessesTarget_of_mixed_reflects
2223    prime_floor_mixed_reflects_from_prime_witnesses_control :=
2224      PRCJCost.PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesTarget_of_prime_control
2225    prime_floor_prime_witnesses_control_iff_mixed_reflects :=
2226      PRCJCost.PRCPrimeCalibrationForcesPrimeWitnessesControlNonunitWitnessesTarget_iff_mixed_reflects
2227    prime_floor_mixed_reflection_split_from_reflects :=
2228      PRCJCost.PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesSplitTarget_of_reflects
2229    prime_floor_mixed_reflection_from_split :=
2230      PRCJCost.PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesTarget_of_split
2231    prime_floor_mixed_reflection_iff_split :=
2232      PRCJCost.PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesTarget_iff_split
2233    prime_floor_mixed_identity_reflects_prime_proved :=
2234      PRCJCost.PRCPrimeCalibrationForcesMixedNonunitIdentityWitnessReflectsPrimeWitnessTarget_proved
2235    prime_floor_mixed_reciprocal_reflects_prime_proved :=
2236      PRCJCost.PRCPrimeCalibrationForcesMixedNonunitReciprocalWitnessReflectsPrimeWitnessTarget_proved
2237    prime_floor_mixed_reflection_split_proved :=
2238      PRCJCost.PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesSplitTarget_proved
2239    prime_floor_mixed_reflection_proved :=
2240      PRCJCost.PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesTarget_proved
2241    prime_floor_prime_witnesses_control_nonunit_proved :=
2242      PRCJCost.PRCPrimeCalibrationForcesPrimeWitnessesControlNonunitWitnessesTarget_proved
2243    prime_floor_nonunit_no_mixed_split_from_no_mixed_prime_witnesses :=
2244      PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesSplitTarget_of_no_mixed_prime_witnesses
2245    prime_floor_nonunit_no_mixed_from_no_mixed_prime_witnesses :=
2246      PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesTarget_of_no_mixed_prime_witnesses
2247    prime_floor_nonunit_no_mixed_iff_no_mixed_prime_witnesses :=
2248      PRCJCost.PRCPrimeCalibrationForcesNonunitNoMixedWitnessesTarget_iff_no_mixed_prime_witnesses
2249    prime_floor_identity_witness_globalizes_from_local_exclusion :=
2250      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget_of_local_exclusion
2251    prime_floor_identity_witness_local_exclusion_from_globalizes :=
2252      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessLocalExclusionTarget_of_identity_witness_globalizes
2253    prime_floor_identity_witness_globalizes_iff_local_exclusion :=
2254      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget_iff_local_exclusion
2255    prime_floor_nonunit_identity_comparable_trace_from_product_no_mixed :=
2256      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget_of_product_no_mixed
2257    prime_floor_nonunit_identity_branch_transport_iff_comparable_trace :=
2258      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityBranchTransportTarget_iff_comparable_trace
2259    prime_floor_product_no_mixed_iff_identity_comparable_trace :=
2260      PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_iff_identity_comparable_trace
2261    prime_floor_product_local_orientation_from_identity_comparable_trace :=
2262      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitProductLocalOrientationTarget_of_identity_comparable_trace
2263    prime_floor_nonunit_local_orientation_from_identity_comparable_trace :=
2264      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitLocalOrientationTarget_of_identity_comparable_trace
2265    prime_floor_nonunit_local_comparable_trace_from_identity_comparable_trace :=
2266      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalComparableTraceTarget_of_identity_comparable_trace
2267    prime_floor_nonunit_identity_comparable_trace_from_local_comparable_trace :=
2268      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget_of_local_comparable_trace
2269    prime_floor_nonunit_local_comparable_trace_iff_identity_comparable_trace :=
2270      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalComparableTraceTarget_iff_identity_comparable_trace
2271    prime_floor_nonunit_branch_agreement_from_transport_pair :=
2272      PRCJCost.PRCPrimeCalibrationForcesNonunitBranchAgreementTarget_of_transport_pair
2273    prime_floor_nonunit_identity_branch_transport_from_branch_agreement :=
2274      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityBranchTransportTarget_of_branch_agreement
2275    prime_floor_nonunit_reciprocal_branch_transport_from_branch_agreement :=
2276      PRCJCost.PRCPrimeCalibrationForcesNonunitReciprocalBranchTransportTarget_of_branch_agreement
2277    prime_floor_nonunit_branch_transport_pair_from_branch_agreement :=
2278      PRCJCost.PRCPrimeCalibrationForcesNonunitBranchTransportPairTarget_of_branch_agreement
2279    prime_floor_nonunit_branch_agreement_iff_transport_pair :=
2280      PRCJCost.PRCPrimeCalibrationForcesNonunitBranchAgreementTarget_iff_transport_pair
2281    prime_floor_nonunit_branch_agreement_from_local_identity_transport :=
2282      PRCJCost.PRCPrimeCalibrationForcesNonunitBranchAgreementTarget_of_local_identity_transport
2283    prime_floor_nonunit_local_identity_transport_from_local_branch_agreement :=
2284      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalIdentityTransportTarget_of_local_branch_agreement
2285    prime_floor_nonunit_local_branch_agreement_from_local_identity_transport :=
2286      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalBranchAgreementTarget_of_local_identity_transport
2287    prime_floor_nonunit_local_branch_agreement_iff_local_identity_transport :=
2288      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalBranchAgreementTarget_iff_local_identity_transport
2289    prime_floor_nonunit_local_comparable_trace_from_local_identity_transport :=
2290      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalComparableTraceTarget_of_local_identity_transport
2291    prime_floor_nonunit_local_identity_transport_from_local_comparable_trace :=
2292      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalIdentityTransportTarget_of_local_comparable_trace
2293    prime_floor_nonunit_local_identity_transport_iff_local_comparable_trace :=
2294      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalIdentityTransportTarget_iff_local_comparable_trace
2295    prime_floor_nonunit_branch_agreement_from_coherent :=
2296      PRCJCost.PRCPrimeCalibrationForcesNonunitBranchAgreementTarget_of_coherent
2297    prime_floor_nonunit_local_branch_agreement_from_coherent :=
2298      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalBranchAgreementTarget_of_coherent
2299    prime_floor_nonunit_coherent_from_local_branch_agreement :=
2300      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget_of_local_branch_agreement
2301    prime_floor_nonunit_orbit_orientation_coherent_iff_local_branch_agreement :=
2302      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget_iff_local_branch_agreement
2303    prime_floor_nonunit_identity_comparable_trace_iff_successor_transport :=
2304      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget_iff_prime_floor_successor_transport
2305    prime_floor_identity_extends_successor_step_from_successor_transport :=
2306      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentityExtendsSuccessorStepTarget_of_successor_transport
2307    prime_floor_identity_contracts_successor_step_from_successor_transport :=
2308      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentityContractsSuccessorStepTarget_of_successor_transport
2309    prime_floor_identity_successor_step_pair_from_successor_transport :=
2310      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget_of_successor_transport
2311    prime_floor_successor_transport_from_successor_step_pair :=
2312      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget_of_successor_step_pair
2313    prime_floor_successor_transport_iff_successor_step_pair :=
2314      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget_iff_successor_step_pair
2315    prime_identity_witness_globalizes_nonunit_from_successor_transport :=
2316      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityWitnessGlobalizesNonunitTarget_of_prime_floor_successor_transport
2317    prime_floor_successor_transport_from_prime_identity_witness_globalizes :=
2318      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget_of_prime_identity_witness_globalizes
2319    prime_floor_successor_transport_iff_prime_identity_witness_globalizes :=
2320      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget_iff_prime_identity_witness_globalizes
2321    prime_identity_witness_globalizes_nonunit_from_no_mixed_prime_witnesses :=
2322      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityWitnessGlobalizesNonunitTarget_of_no_mixed_prime_witnesses
2323    no_mixed_prime_witnesses_from_prime_identity_witness_globalizes :=
2324      PRCJCost.PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_of_prime_identity_witness_globalizes
2325    prime_identity_witness_globalizes_nonunit_iff_no_mixed_prime_witnesses :=
2326      PRCJCost.PRCPrimeCalibrationForcesPrimeIdentityWitnessGlobalizesNonunitTarget_iff_no_mixed_prime_witnesses
2327    prime_floor_identity_successor_step_pair_from_identity_comparable_trace :=
2328      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget_of_identity_comparable_trace
2329    prime_floor_nonunit_identity_comparable_trace_from_successor_step_pair :=
2330      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget_of_successor_step_pair
2331    prime_floor_nonunit_identity_comparable_trace_iff_successor_step_pair :=
2332      PRCJCost.PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget_iff_successor_step_pair
2333    prime_floor_product_no_mixed_from_successor_step_pair :=
2334      PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_of_successor_step_pair
2335    prime_floor_identity_successor_step_pair_from_product_no_mixed :=
2336      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget_of_product_no_mixed
2337    prime_floor_product_no_mixed_iff_successor_step_pair :=
2338      PRCJCost.PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_iff_successor_step_pair
2339    prime_floor_nonunit_coherent_from_successor_step_pair :=
2340      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget_of_successor_step_pair
2341    prime_floor_identity_successor_step_pair_from_nonunit_coherent :=
2342      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget_of_nonunit_coherent
2343    prime_floor_nonunit_coherent_iff_successor_step_pair :=
2344      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget_iff_successor_step_pair
2345    prime_floor_successor_transport_local_adjacent_target_refuted :=
2346      PRCJCost.PRCPrimeFloorSuccessorTransportLocalAdjacentTarget_refuted
2347    prime_floor_successor_transport_local_adjacent_iff_local_successor_transport :=
2348      PRCJCost.PRCPrimeFloorSuccessorTransportLocalAdjacentTarget_iff_local_successor_transport
2349    prime_floor_successor_transport_local_adjacent_iff_nonunit_coherent :=
2350      PRCJCost.PRCPrimeFloorSuccessorTransportLocalAdjacentTarget_iff_nonunit_coherent
2351    prime_floor_nonunit_orbit_orientation_coherent_iff_local_no_mixed :=
2352      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget_iff_local_no_mixed
2353    prime_floor_nonunit_orbit_orientation_coherent_sharpened_target_refuted :=
2354      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentSharpenedTarget_refuted
2355    prime_floor_nonunit_orbit_orientation_coherent_iff_sharpened :=
2356      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget_iff_sharpened
2357    prime_floor_product_local_orientation_sharpened_target_refuted :=
2358      PRCJCost.PRCPrimeCalibrationForcesNonunitOrbitProductLocalOrientationSharpenedTarget_refuted
2359    prime_floor_no_adjacent_mixed_orientation_target_refuted :=
2360      PRCJCost.PRCPrimeCalibrationForcesPrimeFloorNoAdjacentMixedOrientationTarget_refuted
2361    prime_floor_successor_transport_sharpened_refuted :=
2362      PRCJCost.PRCPrimeFloorSuccessorTransportSharpenedTarget_refuted
2363    prime_to_coherent_orientation_refuted :=
2364      PRCJCost.PRCPrimeCalibrationForcesCoherentPrimeOrientationTarget_refuted
2365    coherent_prime_orientation_propagation_refuted :=
2366      PRCJCost.PRCCoherentPrimeOrientationPropagatesToGlobalTarget_refuted
2367    admissible_prime_orientation_coherent :=
2368      PRCJCost.PRCAdmissibleCharacterPrimeOrientationCoherentTarget_proved
2369    admissible_signed_unit_calibration_refuted :=
2370      PRCJCost.PRCAdmissibleCharacterSignedUnitCalibratedTarget_refuted
2371    signed_coherent_prime_orientation_propagation :=
2372      PRCJCost.PRCSignedCoherentPrimeOrientationPropagatesToGlobalTarget_proved
2373    prime_propagation_sharpened_refuted :=
2374      PRCJCost.PRCPrimeCalibrationPropagationSharpenedTarget_refuted
2375    native_cost_rigidity_sharpened_refuted :=
2376      PRCJCost.PRCNativeCostCharacterRigiditySharpenedTarget_refuted
2377    external_foundation_parsing_schema := by
2378      intro ExternalFoundation FaithfulParse
2379      rfl
2380  }
2381  no_project_local_axioms_audit := rfl
2382
2383theorem prc_universal_foundation :
2384    PRCUniversalFoundationCertificate where
2385  delta_kernel :=
2386    prc_universal_foundation_conditional_certificate.kernel
2387  real_complete_ordered_field :=
2388    prc_universal_foundation_conditional_certificate.real_complete_ordered_field
2389  trace_logic :=
2390    prc_universal_foundation_conditional_certificate.trace_logic
2391  formal_system :=
2392    prc_universal_foundation_conditional_certificate.formal_system
2393  inevitability :=
2394    prc_universal_foundation_conditional_certificate.inevitability
2395  recognizer_bridge :=
2396    prc_universal_foundation_conditional_certificate.recognizer_bridge
2397  native_cost_blocker :=
2398    prc_universal_foundation_conditional_certificate.native_cost_blocker
2399  repaired_refuted_native_cost_ledger :=
2400    prc_universal_foundation_conditional_certificate.open_targets
2401  conditional_certificate :=
2402    prc_universal_foundation_conditional_certificate
2403  no_project_local_axioms_audit :=
2404    prc_universal_foundation_conditional_certificate.no_project_local_axioms_audit
2405
2406end PrimitiveRecognitionCalculus
2407end Foundation
2408end IndisputableMonolith
2409