Mathematics · proofs · software

Special Functions · Lean source

CoupledNormalizationAudit.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)

CoupledNormalizationAudit.lean32 lines

Original source pathlean/CoupledNormalizationAudit.lean

Skip source text

1 import CoupledNormalization
2 
3 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.oddFactorial_ne_zero
4 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.oddFactorial_zero
5 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.oddFactorial_succ
6 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.binomial_factorial_product
7 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.binomial_factorial_quotient
8 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.rational_derivatives_zero
9 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.rational_derivatives_succ
10 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.rational_derivatives_solution
11 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.derivative_solution_unique
12 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.derivativeRow_factorialScale
13 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.factorial_scaled_coefficients_solution
14 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.rational_derivatives_factorial
15 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.derivativeNext_congr
16 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.derivative_array_eq
17 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.derivative_array_length
18 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.derivative_array_entry
19 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.derivative_component_factorial
20 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.derivative_component_normalized
21 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.derivative_normalized_cast
22 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.ordinary_array_eq
23 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.ordinary_array_length
24 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.ordinary_array_entry
25 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.derivative_polynomial_eq
26 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.array_polynomial_eq
27 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.array_polynomial_cast
28 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.derivative_polynomial_cast
29 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.derivative_endpoint_enclosure
30 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.array_endpoint_enclosure
31 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.rational_derivatives_one
32 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.derivative_normalization_first

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: ae5eb111ac8335a186618a20171734e385322ccef7aa0b71985cc83ed523a3af

Original source on GitHub

Back to Special Functions