Mathematics · proofs · software

Special Functions · Lean source

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

CoupledOperatorAudit.lean29 lines

Original source pathlean/CoupledOperatorAudit.lean

Skip source text

1 import CoupledOperator
2 
3 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.autonomous_iff_scalar_functional
4 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.nodePolynomial_differentiable
5 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.nodePolynomial_zero
6 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.nodePolynomial_values
7 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.autonomous_scalar_fibers
8 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.autonomous_row_sum_zero
9 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.nonzero_row_first_ne_zero
10 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.autonomous_scale_products
11 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.autonomous_ordered_rows
12 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.ordered_rows_field_zero
13 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.ordered_rows_autonomous
14 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.zero_row_autonomous
15 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.autonomous_iff_zero_or_ordered
16 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.autonomous_nonzero_classification
17 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.autonomous_projected_field_zero
18 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.no_nonzero_autonomous_if_rows_differ
19 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.autonomous_matrix_det_zero
20 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.no_invertible_constant_decoupling
21 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.local_projection_analytic
22 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.local_field_analytic
23 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.local_field_respects_component_germs
24 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.germ_autonomous_iff_scalar_functional
25 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.entire_field_differentiable
26 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.germ_autonomous_implies_entire
27 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.germ_autonomous_iff_entire
28 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.germ_autonomous_nonzero_classification
29 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.no_invertible_constant_germ_decoupling

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: 6b4cd5578f5ebaceb20d704ac7acc29b90fc5360f53bda5a46ebd1c5d18573f0

Original source on GitHub

Back to Special Functions