Mathematics · proofs · software

Special Functions · Lean source

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

CoupledRescalingAudit.lean21 lines

Original source pathlean/CoupledRescalingAudit.lean

Skip source text

1 import CoupledRescaling
2 
3 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.denseOddComplex_odd
4 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.complex_odd_series_hasFPowerSeriesAt
5 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.complex_odd_coefficients_eq
6 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.rescaling_coefficient_identity
7 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.rescaling_forces_defect_zero
8 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.scalar_components_equal
9 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.scalarT_solution
10 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.reductionScale_positive_sq
11 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.reductionScale_surface
12 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.effective_scalar_scales
13 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.scalar_rescaled_solution
14 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.reductionRoot_positive_sq
15 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coupled_scalar_representation
16 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_component_rescaling
17 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.component_rescaling_iff_defect
18 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.component_rescaling_iff_surfaces
19 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.scalarT_unique
20 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.scalarT_symm
21 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.boundary_entire_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: 97104bd96fe19af8bb0d2e700940258cb084ae044ca0f47ab86d9264536f8b76

Original source on GitHub

Back to Special Functions