Mathematics · proofs · software

Special Functions · Lean source

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

CoupledLowerGrowthAudit.lean18 lines

Original source pathlean/CoupledLowerGrowthAudit.lean

Skip source text

1 import CoupledLowerGrowth
2 
3 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.maxScale_positive
4 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.lowerShift_positive
5 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.lowerDescent_positive
6 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.lowerPowerConstant_positive
7 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.shifted_child_radius
8 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.child_radius_descent
9 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_radius_descent_induction
10 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.lower_power_seed
11 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.lower_power_step
12 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coupled_lower_log_power
13 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.normalizedCharacteristicVector_le_one
14 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_lower_log_power
15 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.lower_log_power_ratio
16 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonicalLowerCoefficient_positive
17 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_lower_growth_ratio
18 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_lower_norm_power

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: 76b48f9a4aac1d6e996c1b7deabf17cf77821a72f461046f59e9c4e5e84cd2e7

Original source on GitHub

Back to Special Functions