IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness

declarations in this module (1168)

• structure PRCRatioCharacter L38
• def costFromCharacter L57
• theorem costFromCharacter_toRat L61
• def doubledTraceValue L68
• def nativeCostDoubledTrace L73
• theorem doubledTraceValue_congr L77
• def PRCDoubledTraceDAlembert L87
• theorem nativeCostDoubledTrace_dAlembert_of_native_hypotheses L93
• structure PRCDoubledTraceHypotheses L106
• theorem nativeCostDoubledTrace_hypotheses_of_native_cost_hypotheses L118
• def PRCCharacterTraceMatchesCost L141
• theorem PRCCharacterTraceMatchesCost_of_cost_crossEq L148
• theorem cost_crossEq_of_PRCCharacterTraceMatchesCost L162
• def PRCNativeCostCharacterTraceLiftTarget L177
• def PRCDoubledTraceCoherentRootTarget L186
• def zeroSpikeDoubledTrace L205
• theorem zeroSpikeDoubledTrace_zero L208
• theorem zeroSpikeDoubledTrace_nonzero L212
• theorem zeroSpikeDoubledTrace_hypotheses L217
• theorem zeroSpikeDoubledTrace_no_ratio_character_trace L288
• theorem PRCDoubledTraceCoherentRootTarget_refuted L314
• def PRCDoubledTraceZeroCalibrated L323
• theorem zeroSpikeDoubledTrace_not_zero_calibrated L326
• def PRCDoubledTraceZeroCalibratedCoherentRootTarget L335
• def traceRootDenominator L348
• theorem traceRootDenominator_toRat L351
• def traceRootCandidate L361
• theorem traceRootCandidate_zero L372
• theorem traceRootCandidate_toRat_of_nonzero L376
• def PRCDoubledTraceLinearRootCandidateWorks L387
• def PRCDoubledTraceZeroCalibratedLinearRootTarget L397
• theorem PRCDoubledTraceZeroCalibratedCoherentRootTarget_of_linear_root L403
• theorem PRCNativeCostCharacterTraceLiftTarget_of_doubled_trace_coherent_root L410
• def PRCNativeCostCharacterFactorizationTarget L421
• theorem PRCNativeCostCharacterTraceLiftTarget_of_factorization L429
• theorem PRCNativeCostCharacterFactorizationTarget_of_trace_lift L436
• theorem PRCNativeCostCharacterFactorizationTarget_of_doubled_trace_coherent_root L443
• theorem PRCNativeCostCharacterFactorizationTarget_iff_trace_lift L449
• def PRCNativeCostCharacterRigidityTarget L459
• def orbitDirection L467
• def primeDirection L474
• def PRCCharacterPrimeDirectionCalibrated L480
• def PRCTwoCalibrationForcesPrimeCalibrationTarget L490
• def PRCPrimeCalibrationPropagationTarget L499
• theorem onRatioOrbit_congr L506
• theorem jcost_eq_forces_same_or_reciprocal L512
• theorem primeDirection_toRat_ne_zero L546
• theorem primeDirection_toRat L557
• theorem twoOrbit_primeOrbit L563
• def threeOrbit L586
• theorem threeOrbit_toNat L589
• theorem threeOrbit_primeOrbit L594
• theorem threeOrbit_ne_twoOrbit L616
• theorem orbitDirection_toRat L623
• theorem primeDirection_not_crossEq_recip L629
• theorem orbitDirection_nonunit_not_crossEq_recip L662
• theorem orbit_succ_ne_zero L696
• theorem orbitDirection_succ_crossEq_add_one L701
• def orbitPositionTrace L722
• theorem orbitPositionTrace_add_extends_left L726
• theorem orbitPositionTrace_add_extends_right L739
• theorem orbitPositionTrace_extends_of_toNat_le L745
• theorem orbitPositionTrace_comparable L756
• def PRCPrimeAxisTraceConnected L767
• theorem PRCPrimeAxisTraceConnected_proved L774
• def PRCCharacterGlobalCostOrientation L785
• def PRCPrimeCalibrationForcesGlobalOrientationTarget L794
• def PRCCharacterPrimeOrientationCoherent L802
• def twoPrimeDirection L810
• theorem twoPrimeDirection_toRat L813
• def PRCCharacterTwoPrimeBranchControlsPrimes L822
• def PRCCharacterPrimeIdentityIffTwoPrimeIdentity L835
• def PRCCharacterPrimeIdentityForcesTwoPrimeIdentity L845
• def PRCCharacterTwoPrimeReciprocalExcludesPrimeIdentity L853
• def PRCCharacterTwoPrimeReciprocalExcludesPrimeIdentityWitness L863
• def PRCCharacterTwoPrimeReciprocalIdentityPrimeMixed L874
• def PRCCharacterTwoPrimeReciprocalIdentityNonTwoPrimeMixed L883
• def PRCCharacterTwoAdicAxisTwist L894
• def PRCTwoAdicAxisTwistRatioCharacter L905
• def ratioOrbitOfRat L913

… and 1088 more