Mathematics · proofs · software

Special Functions · Lean source

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

CoupledUpperGrowthAudit.lean36 lines

Original source pathlean/CoupledUpperGrowthAudit.lean

Skip source text

1 import CoupledUpperGrowth
2 
3 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.full_radius_upper_from_deriv
4 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_axis_full_upper
5 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_axis_at_one_le_two
6 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.upperRadius_ge_one
7 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.upperRadius_child
8 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.upperSeed_ge_one
9 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_axis_upper_ladder
10 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.upperLogSeed_recurrence
11 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.upperSeed_log_le
12 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.scaleDelay_positive
13 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.scaleDelay_bounds
14 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.upperCorrection_positive
15 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.upperCorrection_rows
16 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.exp_one_lt_three
17 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.exists_upper_seed_index
18 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.upper_seed_exp_radius
19 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_axis_upper_log_seed
20 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.log_upper_from_full
21 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_axis_log_full_upper
22 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.upperSeedBudget_positive
23 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.upperPowerConstant_positive
24 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.upper_power_seed
25 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.exp_sub_scaleDelay
26 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_axis_log_delayed_upper
27 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.exp_weight_shift
28 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_log_delay_induction
29 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.upper_power_step
30 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coupled_upper_log_power
31 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_upper_log_power
32 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.upperSeedIndex_spec
33 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonicalUpperCoefficient_positive
34 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_upper_growth_ratio
35 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_two_sided_growth_ratio
36 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_upper_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: 6ecf165aa171a96f4bd8d7ed1f8bb1e9bd4d81dca3d4711e4946f7005be398be

Original source on GitHub

Back to Special Functions