Mathematics · proofs · software

Special Functions · Lean source

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

CoupledGuardedMajorantAudit.lean32 lines

Original source pathlean/CoupledGuardedMajorantAudit.lean

Skip source text

1 import CoupledGuardedMajorant
2 
3 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.ladder_terminal
4 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.ladder_terminal_small
5 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.ladder_adequate
6 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.ladder_fold_eq
7 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.build_ladder_ok
8 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.build_ladder_of_trace
9 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.build_ladder_ok_iff
10 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.build_ladder_not_bits
11 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.build_ladder_exists_of_adequate
12 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.guarded_fold_not_steps
13 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.guarded_fold_ok_iff
14 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.guarded_fold_bits_iff
15 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_success
16 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_small
17 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_zero
18 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_no_steps
19 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_disk_bound
20 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_endpoint_enclosure
21 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_step_failure
22 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_bit_failure
23 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.size_fits_iff
24 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.checked_invalid_scales
25 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.checked_negative_radius
26 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.checked_zero_before_resources
27 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.checked_invalid_steps
28 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.checked_invalid_bits
29 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.checked_valid_inputs
30 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.checked_small_seed_unchecked
31 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.checked_success_core
32 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.checked_endpoint_enclosure

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: 66312a82efcb43fe59998181bd3c872c33956b221fca5a47c61bfa1db980ddf8

Original source on GitHub

Back to Special Functions