Mathematics · proofs · software

Special Functions · Lean source

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

CoupledScalarReductionAudit.lean45 lines

Original source pathlean/CoupledScalarReductionAudit.lean

Skip source text

1 import CoupledScalarReduction
2 
3 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.positive_pair_from_product_and_square_sum
4 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.equal_components_coefficients
5 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.equal_components_product
6 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.equal_components_square_sum
7 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.equal_components_unordered_rows
8 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.scalar_pair_solution
9 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.unordered_rows_scalar_representation
10 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.components_equal_iff_unordered_rows
11 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.components_equal_iff_scale_pair_set
12 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.characteristicExponent_eq_of_balance
13 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.scalar_characteristic_balance_iff
14 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.scalar_characteristic_order
15 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.characteristic_order_invariant
16 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.complex_sinh_hasDerivAt
17 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.sinh_half_derivative_identity
18 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.scaled_sinh_half_equation
19 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.halfScales_positive
20 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.halfScales_strict
21 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.scaled_sinh_half_solution
22 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.sqrt_two_complex_square
23 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_half_sinh
24 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.half_characteristic_order
25 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.half_radial_order
26 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.unequalScales_positive
27 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.unequalScales_strict
28 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.unequal_characteristic_order
29 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.unequal_radial_order
30 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.unequal_normalized_vector
31 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.unequal_type_proportions
32 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.unequal_components_different
33 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.unequal_coefficients_through_seven
34 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.unequal_row_sums
35 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.unequal_lower_constants
36 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.unequal_explicit_lower_growth
37 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.surface_cross_scale_contract
38 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.order_surface_realization
39 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.component_oddSum
40 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.component_coefficient_majorant
41 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.oddSum_truncation_eq_tail
42 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_complex_truncation_bound
43 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_four_term_remainder
44 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.unequal_degree_seven_polynomials
45 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.unequal_degree_seven_error

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: 53ed37138bafd35638304c2cb5c644930b5f4b7c403ee5705e3e9f26b6cfc536

Original source on GitHub

Back to Special Functions