IndisputableMonolith.Cost.RealCharacterFactorization · Recognition explainer

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Cost.GaugeOrbitFromRealCharacter module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.RealTraceRoot module_import
IndisputableMonolith.Cost.TraceRationalExponent module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness module_import

declarations in this module (73)

theorem doubledTrace_dAlembert_of_rcl L35
theorem doubledTrace_dAlembert_of_native L57
def IsPosIntOrbit L69
def natOrbit L72
theorem natOrbit_toRat L74
def PRCNativeCostSignReversing L77
def PRCNativeCostMonotone L81
structure BaseSansTwo L86
structure SansAnchorHypotheses L104
theorem doubledTrace_dAlembert_of_sansAnchor L110
structure PRCRealRatioCharacter L122
def costFromRealCharacter L135
def exponentOfCharacter L138
def SansAnchorRealCharacterFactorizationTarget L144
abbrev SansAnchorRealCharacterFactorizationInput L154
def traceDisplay L160
theorem traceDisplay_one L164
theorem traceDisplay_recip L172
theorem traceDisplay_dAlembert L181
theorem traceDisplay_posInt_ge_two L192
theorem traceDisplay_two_ge_two L210
theorem traceDisplay_eq_of_crossEq L215
def rationalTrace L231
theorem rationalTrace_eq_traceDisplay L235
theorem rationalTrace_one L242
theorem rationalTrace_recip L253
theorem rationalTrace_dAlembert L266
theorem rationalTrace_neg L299
theorem rationalTrace_nat_ge_two L311
def linearExtraction L322
theorem linearExtraction_unit L326
theorem linearExtraction_multiplicative L338
theorem linearExtraction_recip_sum L416
def anchorRoot L454
def nontrivialCharacterValue L458
theorem anchorRoot_ge_one L462
theorem anchorRoot_add_inv L468
theorem anchorRoot_gt_one L474
theorem anchorRoot_ne_zero L486
theorem anchorRoot_sq_sub_one_ne_zero L491
theorem nontrivialCharacterValue_one L498
theorem nontrivialCharacterValue_mul L505
theorem nontrivialCharacterValue_recip_sum L515
theorem rationalTrace_nat_mono L527
theorem rationalTrace_two_pow_eq_two L550
theorem rationalTrace_nat_eq_two_of_two_eq_two L573
theorem rationalTrace_pos_eq_two_of_two_eq_two L593
def rationalSignCharacter L630
theorem rationalSignCharacter_one L633
theorem rationalSignCharacter_mul L636
theorem rationalSignCharacter_recip L661
theorem rationalSignCharacter_nonzero L670
theorem rationalSignCharacter_of_pos L676
def realCharacterCandidate L682
theorem nontrivialCharacterValue_nonzero L691
theorem nontrivialCharacterValue_recip L702
theorem nontrivialCharacterValue_trace L712
theorem nontrivialCharacterValue_two L723
theorem nontrivialCharacterValue_pow L746
theorem nontrivialCharacterValue_pos_on_nat L761
theorem exists_pow_trace_decrease L778
theorem nontrivialCharacterValue_nat_trace_mono L819
theorem nontrivialCharacterValue_principal_on_nat L836
theorem realCharacterCandidate_unit L868
theorem realCharacterCandidate_mul L877
theorem realCharacterCandidate_recip L890
theorem realCharacterCandidate_nonzero L903
theorem realCharacterCandidate_principal_on_pos_int L913
theorem realCharacterCandidate_is_character L925
theorem realCharacterCandidate_trace_of_pos L934
theorem realCharacterCandidate_cost_agrees L950
theorem realCharacterCandidate_small_traces_rational L962
theorem SansAnchorRealCharacterFactorizationTarget_proved L976