Lean Status

Formal verification, live

Every analytical kill on the ladder is paired with a Lean 4 theorem. Green = proved end-to-end. Violet = sorry placeholder. Red = killed (formal counterexample).

45
Proved
24
Sorry
5
Axiom
3
Killed (analytical)

Theorem grid

rank_mul_left_isUnit_det

Mathlib instantiation: unit-det preserves rank

G 0 · LeanMining/NeuralGeometry/CompressionLadder.lean:59

PROVED

invertible_gauge_preserves_rank_family

Free-orthogonal regauge invariant

G 0 · LeanMining/NeuralGeometry/CompressionLadder.lean:75

PROVED

effective_weight_gram_eq

G₃ algebraic bridge

G 3 · LeanMining/NeuralGeometry/CompressionLadder.lean:126

PROVED

same_precision_residual_not_free

Gate 1 byte-cost lower bound

GATE 1 · LeanMining/NeuralGeometry/CompressionLadder.lean:214

SORRY

coefficient_support_truncation_eq

Coefficient support truncation

GATE 1 · LeanMining/NeuralGeometry/CompressionLadder.lean:231

SORRY

coefficient_tail_error_bound

Coefficient tail error bound

GATE 1 · LeanMining/NeuralGeometry/CompressionLadder.lean:250

SORRY

activation_weighted_error_le_frobenius

Activation ≤ Frobenius

GATE 2 · LeanMining/NeuralGeometry/DeploymentCorrectness.lean:76

SORRY

activation_weighted_error_le_spectral

Activation ≤ spectral

GATE 2 · LeanMining/NeuralGeometry/DeploymentCorrectness.lean:119

SORRY

activation_error_depends_only_on_data_subspace

Activation depends only on data subspace

GATE 2 · LeanMining/NeuralGeometry/DeploymentCorrectness.lean:154

SORRY

activation_error_zero_on_data_subspace

Zero error on data subspace

GATE 2 · LeanMining/NeuralGeometry/DeploymentCorrectness.lean:175

SORRY

linear_gauge_foldable_between_layers

Linear gauge foldable between layers

G 0 · LeanMining/NeuralGeometry/DeploymentCorrectness.lean:205

SORRY

gap_preserved_under_perturbation

Gate 3 gap preservation

GATE 3 · LeanMining/NeuralGeometry/DeploymentCorrectness.lean:241

SORRY

topk_route_stability

Gate 3 top-k route stability

GATE 3 · LeanMining/NeuralGeometry/DeploymentCorrectness.lean:281

PROVED

route_flip_zero_above_margin

Gate 3 zero flip above margin

GATE 3 · LeanMining/NeuralGeometry/DeploymentCorrectness.lean:390

PROVED

single_layer_approx_error

Per-layer approximation

G 6 · LeanMining/NeuralGeometry/LayerStackDistillation.lean:101

SORRY

two_layer_error_bound

Two-layer error recurrence

G 5 · LeanMining/NeuralGeometry/LayerStackDistillation.lean:119

SORRY

finite_stack_error_bound

Finite-stack error recurrence

G 5 · LeanMining/NeuralGeometry/LayerStackDistillation.lean:162

SORRY

uniform_stack_error_bound

Uniform stack error bound

G 5 · LeanMining/NeuralGeometry/LayerStackDistillation.lean:191

PROVED

uniform_stack_error_bound_geometric

Uniform stack — geometric closed form

G 5 · LeanMining/NeuralGeometry/LayerStackDistillation.lean:216

PROVED

uniform_stack_geometric_closed_form

Uniform stack closed form

G 5 · LeanMining/NeuralGeometry/LayerStackDistillation.lean:279

PROVED

uniform_stack_error_upper_bound

Uniform stack upper bound

G 5 · LeanMining/NeuralGeometry/LayerStackDistillation.lean:299

PROVED

one_bit_compounding_exceeds_gate

1-bit compounding exceeds Gate 5

GATE 5 · LeanMining/NeuralGeometry/LayerStackDistillation.lean:323

PROVED

one_bit_kill_signal_corollary

1-bit kill corollary

GATE 5 · LeanMining/NeuralGeometry/LayerStackDistillation.lean:333

PROVED

key_projection_gauge_invariance

MoE key-proj gauge invariance

G 0 · LeanMining/NeuralGeometry/MoEGauge.lean:39

PROVED

attention_score_gauge_invariance

MoE attention score gauge invariance

G 0 · LeanMining/NeuralGeometry/MoEGauge.lean:59

PROVED

value_projection_gauge_invariance

MoE value-proj gauge invariance

G 0 · LeanMining/NeuralGeometry/MoEGauge.lean:71

PROVED

kq_space_gauge_invariance

K/Q-space gauge invariance

G 0 · LeanMining/NeuralGeometry/MoEGauge.lean:94

PROVED

post_rope_score_invariance

Post-RoPE score invariance

G 0 · LeanMining/NeuralGeometry/MoEGauge.lean:120

PROVED

exact_residual_recovery

MoE exact residual recovery

GATE 2 · LeanMining/NeuralGeometry/MoEGauge.lean:145

PROVED

attention_error_bound

MoE attention error bound

GATE 2 · LeanMining/NeuralGeometry/MoEGauge.lean:172

PROVED

top_k_optimal

Top-k optimal

GATE 3 · LeanMining/NeuralGeometry/MoEGauge.lean:385

PROVED

stack_iterate_approximation

Stack iterate approximation

G 5 · LeanMining/NeuralGeometry/StackCompression.lean:116

SORRY

recursive_shared_weight_exists

Recursive shared weight exists

G 5 · LeanMining/NeuralGeometry/StackCompression.lean:155

SORRY

contractive_shared_weight_bounded_error

Contractive shared weight bounded error

G 5 · LeanMining/NeuralGeometry/StackCompression.lean:184

SORRY

low_rank_bytes_closed_form

Bytes — low-rank closed form

GATE 1 · LeanMining/NeuralGeometry/StaticCompressionBudget.lean:89

PROVED

sign_scale_rank_bytes_closed_form

Bytes — sign+scale+rank closed form

GATE 1 · LeanMining/NeuralGeometry/StaticCompressionBudget.lean:95

PROVED

shared_codebook_saves_when_K_lt_experts

Bytes — shared codebook saves when K<E

GATE 1 · LeanMining/NeuralGeometry/StaticCompressionBudget.lean:111

PROVED

static_student_bytes_lt_dense

Bytes — static student < dense

GATE 1 · LeanMining/NeuralGeometry/StaticCompressionBudget.lean:147

PROVED

pareto_dominance_refl

Pareto reflexive

GATE 1 · LeanMining/NeuralGeometry/StaticCompressionBudget.lean:164

PROVED

pareto_dominance_transitive

Pareto transitive

GATE 1 · LeanMining/NeuralGeometry/StaticCompressionBudget.lean:170

PROVED

pareto_dominance_from_components

Pareto from components

GATE 1 · LeanMining/NeuralGeometry/StaticCompressionBudget.lean:185

PROVED

pareto_strict_implies_weak

Pareto strict ⇒ weak

GATE 1 · LeanMining/NeuralGeometry/StaticCompressionBudget.lean:202

PROVED

global_delta_bytes_lt_per_task

Global+δ packaging beats per-task

G 4 · LeanMining/NeuralGeometry/StaticCompressionBudget.lean:231

PROVED

global_delta_bytes_lt_per_task_with_overhead

Global+δ packaging (with overhead)

G 4 · LeanMining/NeuralGeometry/StaticCompressionBudget.lean:245

PROVED

static_student_no_runtime_choice

Static-student interface

G 3 · LeanMining/NeuralGeometry/StaticDistillation.lean:85

PROVED

static_distillation_activation_error_eq

Static distillation = activation error

GATE 2 · LeanMining/NeuralGeometry/StaticDistillation.lean:91

PROVED

static_distillation_frobenius_bound

Static distillation Frobenius bound

GATE 2 · LeanMining/NeuralGeometry/StaticDistillation.lean:104

PROVED

low_rank_factor_bytes

Low-rank factorization bytes

GATE 1 · LeanMining/NeuralGeometry/TensorFactorization.lean:66

SORRY

additive_residual_error_triangle

Residual triangle inequality

G 2 · LeanMining/NeuralGeometry/TensorFactorization.lean:150

PROVED

low_rank_residual_frobenius_bound

Low-rank residual Frobenius bound

G 2 · LeanMining/NeuralGeometry/TensorFactorization.lean:175

PROVED

tensor_factor_frobenius_to_activation

Frobenius → activation lift

GATE 2 · LeanMining/NeuralGeometry/TensorFactorization.lean:218

SORRY

shared_basis_layer_frobenius_bound

Shared-basis per-layer bound

G 6 · LeanMining/NeuralGeometry/TensorFactorization.lean:250

SORRY

shared_basis_stack_error_additive

Shared-basis stack error (additive)

G 6 · LeanMining/NeuralGeometry/TensorFactorization.lean:266

SORRY

shared_basis_stack_error_orthogonal

Shared-basis stack error (orthogonal √N)

G 6 · LeanMining/NeuralGeometry/TensorFactorization.lean:300

PROVED

shared_basis_compression_saves

Shared-basis cheaper than N dense

G 6 · LeanMining/NeuralGeometry/TensorFactorization.lean:323

PROVED

restricted_family_cannot_meet_target

Restricted-family lower bound

G 7 · LeanMining/NeuralGeometry/TensorFactorization.lean:353

PROVED

olmoe_joint_basis_no_low_distortion

OLMoE joint-basis no low distortion

G 7 · LeanMining/NeuralGeometry/TensorFactorization.lean:402

SORRY

mode_one_total_energy

Mode-1 unfolding energy

G 2 · LeanMining/NeuralGeometry/TensorFactorization.lean:468

SORRY

independent_layers_spectral_norm

Independent layers spectral norm

G 2 · LeanMining/NeuralGeometry/TensorFactorization.lean:490

SORRY

tucker_mode1_spectral_lower_bound

Tucker mode-1 lower bound

G 2 · LeanMining/NeuralGeometry/TensorFactorization.lean:519

SORRY

tucker_mode0_spectral_lower_bound

Tucker mode-0 lower bound

G 2 · LeanMining/NeuralGeometry/TensorFactorization.lean:537

SORRY

olmoe_tucker_layer_no_compression

OLMoE Tucker layer kill

G 2 · LeanMining/NeuralGeometry/TensorFactorization.lean:597

PROVED

olmoe_tucker_expert_no_compression

OLMoE Tucker expert kill

G 2 · LeanMining/NeuralGeometry/TensorFactorization.lean:618

PROVED

olmoe_hosvd_joint_no_compression

OLMoE HOSVD joint kill

G 2 · LeanMining/NeuralGeometry/TensorFactorization.lean:648

PROVED

olmoe_tucker_cross_mode_no_compression

OLMoE cross-mode kill

G 2 · LeanMining/NeuralGeometry/TensorFactorization.lean:700

PROVED

task_union_basis_contains_task_basis

Union basis ⊇ task basis

G 4 · LeanMining/NeuralGeometry/TensorFactorization.lean:736

PROVED

certified_distillation_bounds_all_static_inference

Certified distillation bound

GATE 2 · LeanMining/NeuralGeometry/TensorialDistillationError.lean:64

PROVED

frob_certificate_implies_distillation_certificate

Frob ⇒ distillation cert

GATE 2 · LeanMining/NeuralGeometry/TensorialDistillationError.lean:76

PROVED

rank_r_certificate_implies_distillation_certificate

Rank-r ⇒ distillation cert

GATE 2 · LeanMining/NeuralGeometry/TensorialDistillationError.lean:108

PROVED

Source + reproduction