Mathematics · proofs · software

Special Functions · Lean source

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

CoupledUniquenessAudit.lean18 lines

Original source pathlean/CoupledUniquenessAudit.lean

Skip source text

1 import CoupledUniqueness
2 
3 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.analytic_scale_at_zero
4 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.analytic_order_scale_ge
5 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.analytic_order_mul_ge_left
6 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.analytic_order_mul_ge_right
7 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.analytic_row_order_ge
8 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.derivative_difference_germ
9 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.analytic_pair_germ_unique
10 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.entire_solution_differentiable
11 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.entire_solution_unique
12 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.entire_solution_eq
13 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coupled_entire_exists_unique
14 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.analytic_solution_germ_eq
15 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.analytic_solution_hasSum
16 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.entire_solution_hasSum
17 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.entire_solution_odd
18 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coupled_F1_contract

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: 228af41b5b27418b3d4202df64b144c84affb9a4e05cdfbeb7a8d8e438823180

Original source on GitHub

Back to Special Functions