Mathematics · proofs · software

Special Functions · Lean source

CoupledFormalAudit.lean

Selected results recorded Coverage and evidence

Compiler/replay evidence is reported for a subset or bounded block. No whole-work coverage is implied.

This viewer reads the retained source; it does not run Lean or assign new claim mappings.

Local imports (1)

CoupledFormalAudit.lean31 lines

Original source pathlean/CoupledFormalAudit.lean

Skip source text

1 import CoupledFormal
2 
3 #print axioms Komorebi.SpecialFunctions.Coupled.positive_pair_recovery
4 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.defect_factor
5 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.defect_eq_zero_iff
6 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.positive_square_injective
7 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.seven_jet_injective
8 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coefficients_solution
9 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.nextCoefficient_congr
10 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coefficient_solution_unique
11 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coefficient_solution_exists_unique
12 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coefficients_zero
13 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coefficients_one
14 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coefficients_two
15 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coefficients_three
16 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.nextCoefficient_positive
17 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coefficients_positive
18 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.nextCoefficient_le_geometric
19 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coefficients_le_geometric
20 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.odd_series_norm_bound
21 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.odd_series_norm_summable
22 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.odd_series_summable
23 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coefficient_series_absolutely_convergent
24 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.odd_series_tail_bound
25 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.sameJet_of_coefficients_eq
26 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.parameters_of_jet_through_degree_seven
27 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.parameters_of_formal_pair_eq
28 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.workedScales_positive
29 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.workedScales_defect
30 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.workedScales_recoverable
31 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.boundary_collision

Back to source controls

Original file and source record

This copy matches the recorded source file. Its publication here does not change the work’s review status.

SHA-256: f6d92e0dec5458142cbbf0b2b717b5233f2330b59ef58e89c8be10361f24f437

Original source on GitHub

Back to Special Functions