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

152
Proved
7
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

PROVED

coefficient_support_truncation_eq

Coefficient support truncation

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

PROVED

coefficient_tail_error_bound

Coefficient tail error bound

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

PROVED

activation_weighted_error_le_frobenius

Activation ≤ Frobenius

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

PROVED

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

PROVED

activation_error_zero_on_data_subspace

Zero error on data subspace

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

PROVED

linear_gauge_foldable_between_layers

Linear gauge foldable between layers

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

PROVED

gap_preserved_under_perturbation

Gate 3 gap preservation

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

PROVED

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

PROVED

two_layer_error_bound

Two-layer error recurrence

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

PROVED

finite_stack_error_bound

Finite-stack error recurrence

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

PROVED

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

PROVED

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

PROVED

shared_basis_layer_frobenius_bound

Shared-basis per-layer bound

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

PROVED

shared_basis_stack_error_additive

Shared-basis stack error (additive)

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

PROVED

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

PROVED

mode_one_total_energy

Mode-1 unfolding energy

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

PROVED

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

bias_decomposition

STEADY STATE · LeanMining/SteadyState/BiasGenDecoupling.lean:92

PROVED

gen_decomposition

STEADY STATE · LeanMining/SteadyState/BiasGenDecoupling.lean:100

PROVED

classK_decoupled_iff_kappa_split

STEADY STATE · LeanMining/SteadyState/BiasGenDecoupling.lean:119

PROVED

classK_realised_of_kappa_gen_zero

STEADY STATE · LeanMining/SteadyState/BiasGenDecoupling.lean:129

PROVED

equal_readouts_collapses

STEADY STATE · LeanMining/SteadyState/BiasGenDecoupling.lean:142

PROVED

falsifier_negates_decoupling

STEADY STATE · LeanMining/SteadyState/BiasGenDecoupling.lean:165

PROVED

decoupled_at_zero_gen_iff_kappa_gen_zero

STEADY STATE · LeanMining/SteadyState/BiasGenDecoupling.lean:176

PROVED

inverse_source_under_decoupled

STEADY STATE · LeanMining/SteadyState/BiasGenDecoupling.lean:197

PROVED

cross_readout_response_ratio

STEADY STATE · LeanMining/SteadyState/BiasGenDecoupling.lean:239

PROVED

cross_readout_budget_at_bias_saturation

STEADY STATE · LeanMining/SteadyState/BiasGenDecoupling.lean:261

PROVED

cross_corpus_budget_violated_when_kappa_ratio_exceeds_headroom

STEADY STATE · LeanMining/SteadyState/BiasGenDecoupling.lean:279

PROVED

prod_one_add_le_pow_one_add_max

STEADY STATE · LeanMining/SteadyState/DepthCompositionInflation.lean:85

PROVED

composed_inflation_bound

STEADY STATE · LeanMining/SteadyState/DepthCompositionInflation.lean:106

PROVED

kills_iff_pow_exceeds

STEADY STATE · LeanMining/SteadyState/DepthCompositionInflation.lean:125

PROVED

per_layer_budget_clears_composed

STEADY STATE · LeanMining/SteadyState/DepthCompositionInflation.lean:155

PROVED

pythagoras_decomposition

STEADY STATE · LeanMining/SteadyState/EckartYoungResidual.lean:55

PROVED

residual_sq_le_norm_sq

STEADY STATE · LeanMining/SteadyState/EckartYoungResidual.lean:62

PROVED

residual_sq_ge_of_projected_short

STEADY STATE · LeanMining/SteadyState/EckartYoungResidual.lean:74

PROVED

residual_eq_norm_of_kernel

STEADY STATE · LeanMining/SteadyState/EckartYoungResidual.lean:85

PROVED

kill_iff_witness

STEADY STATE · LeanMining/SteadyState/EckartYoungResidual.lean:95

PROVED

family_residual_lower_bound

STEADY STATE · LeanMining/SteadyState/EckartYoungResidual.lean:114

PROVED

shrunk_zero_implies_kappa_zero

STEADY STATE · LeanMining/SteadyState/HaarConcentration.lean:53

PROVED

shrunk_mono_in_eps

STEADY STATE · LeanMining/SteadyState/HaarConcentration.lean:66

PROVED

source_coupling_bounded_of_shrunk

STEADY STATE · LeanMining/SteadyState/HaarConcentration.lean:87

PROVED

not_shrunk_iff_witness

STEADY STATE · LeanMining/SteadyState/HaarConcentration.lean:99

PROVED

shrunk_comp_right

STEADY STATE · LeanMining/SteadyState/HaarConcentration.lean:111

PROVED

sourceEffect_eq_readout_transport_source

STEADY STATE · LeanMining/SteadyState/LayerFlowSteerability.lean:48

PROVED

readoutNullSource_effect_eq_baseline

STEADY STATE · LeanMining/SteadyState/LayerFlowSteerability.lean:55

PROVED

not_crossesSteeringThreshold_of_effect_lt

STEADY STATE · LeanMining/SteadyState/LayerFlowSteerability.lean:64

PROVED

crossesSteeringThreshold_of_threshold_le_effect

STEADY STATE · LeanMining/SteadyState/LayerFlowSteerability.lean:74

PROVED

inverseSource_exists_of_witness

STEADY STATE · LeanMining/SteadyState/LayerFlowSteerability.lean:97

PROVED

inverseSource_crosses_threshold_of_target_ge

STEADY STATE · LeanMining/SteadyState/LayerFlowSteerability.lean:105

PROVED

not_beatsNullBy_of_candidate_lt_null_plus_margin

STEADY STATE · LeanMining/SteadyState/LayerFlowSteerability.lean:131

PROVED

beatsNullBy_of_null_plus_margin_le_candidate

STEADY STATE · LeanMining/SteadyState/LayerFlowSteerability.lean:141

PROVED

selectivityRatio_pos

STEADY STATE · LeanMining/SteadyState/SelectivityCap.lean:35

PROVED

selectivityRatio_mono_in_alpha

STEADY STATE · LeanMining/SteadyState/SelectivityCap.lean:47

PROVED

selectivityRatio_gt_cap_iff

STEADY STATE · LeanMining/SteadyState/SelectivityCap.lean:58

PROVED

no_jointly_feasible_of_coherence_violates_selectivity

STEADY STATE · LeanMining/SteadyState/SelectivityCap.lean:82

PROVED

not_jointlyFeasible_of_excess

STEADY STATE · LeanMining/SteadyState/SelectivityCap.lean:91

PROVED

jointlyFeasible_of_coherent_subcap

STEADY STATE · LeanMining/SteadyState/SelectivityCap.lean:105

PROVED

entropy_nonneg

STEADY STATE · LeanMining/SteadyState/SoftmaxEntropySlack.lean:79

PROVED

entropy_le_log_card

STEADY STATE · LeanMining/SteadyState/SoftmaxEntropySlack.lean:100

PROVED

perplexity_ge_one

STEADY STATE · LeanMining/SteadyState/SoftmaxEntropySlack.lean:133

PROVED

perplexity_le_card

STEADY STATE · LeanMining/SteadyState/SoftmaxEntropySlack.lean:142

PROVED

entropy_uniform

STEADY STATE · LeanMining/SteadyState/SoftmaxEntropySlack.lean:162

PROVED

perplexity_uniform

STEADY STATE · LeanMining/SteadyState/SoftmaxEntropySlack.lean:175

PROVED

entropy_delta

STEADY STATE · LeanMining/SteadyState/SoftmaxEntropySlack.lean:182

PROVED

perplexity_delta

STEADY STATE · LeanMining/SteadyState/SoftmaxEntropySlack.lean:198

PROVED

attentionSlackRatio_ge_one

STEADY STATE · LeanMining/SteadyState/SoftmaxEntropySlack.lean:206

PROVED

attentionSlackRatio_le_card

STEADY STATE · LeanMining/SteadyState/SoftmaxEntropySlack.lean:217

PROVED

attentionSlackRatio_uniform_eq_one

STEADY STATE · LeanMining/SteadyState/SoftmaxEntropySlack.lean:230

PROVED

attentionSlackRatio_delta_eq_card

STEADY STATE · LeanMining/SteadyState/SoftmaxEntropySlack.lean:238

PROVED

noGenerationWitness_blocksTransport

STEADY STATE · LeanMining/SteadyState/SteerabilityPostmortemRouting.lean:73

PROVED

noGenerationWitness_blocksInverseSource

STEADY STATE · LeanMining/SteadyState/SteerabilityPostmortemRouting.lean:80

PROVED

biasGenDecoupled_blocksFixedReadoutSteering

STEADY STATE · LeanMining/SteadyState/SteerabilityPostmortemRouting.lean:87

PROVED

linearRegimeFailure_blocksKappaInterpretation

STEADY STATE · LeanMining/SteadyState/SteerabilityPostmortemRouting.lean:98

PROVED

readoutTrapHalt_isMethodologyNotMechanism

STEADY STATE · LeanMining/SteadyState/SteerabilityPostmortemRouting.lean:108

PROVED

reopenRequiresTrapCleanGenerationWitness

STEADY STATE · LeanMining/SteadyState/SteerabilityPostmortemRouting.lean:116

PROVED

bestScore_le_of_subset

STEADY STATE · LeanMining/SteadyState/SubsetFamilyClosure.lean:46

PROVED

no_subset_member_beats_superset

STEADY STATE · LeanMining/SteadyState/SubsetFamilyClosure.lean:58

PROVED

bestScore_attained

STEADY STATE · LeanMining/SteadyState/SubsetFamilyClosure.lean:73

PROVED

strict_loss_iff_excluded_witness

STEADY STATE · LeanMining/SteadyState/SubsetFamilyClosure.lean:86

PROVED

toy_sourceEffect_linear_decomposition

STEADY STATE · LeanMining/SteadyState/ToyLayerFlow.lean:73

PROVED

toy_baselineEffect

STEADY STATE · LeanMining/SteadyState/ToyLayerFlow.lean:82

PROVED

toy_readoutNull_iff_kappa_zero

STEADY STATE · LeanMining/SteadyState/ToyLayerFlow.lean:89

PROVED

toy_crossesSteeringThreshold_iff

STEADY STATE · LeanMining/SteadyState/ToyLayerFlow.lean:111

PROVED

toy_inverseSourceWitness_linear

STEADY STATE · LeanMining/SteadyState/ToyLayerFlow.lean:124

PROVED

toy_beatsNullBy_iff

STEADY STATE · LeanMining/SteadyState/ToyLayerFlow.lean:137

PROVED

toy_outputPresence_eq_zero_of_zero_readout

STEADY STATE · LeanMining/SteadyState/ToyLayerFlow.lean:161

PROVED

toy_outputGated_of_zero_readout

STEADY STATE · LeanMining/SteadyState/ToyLayerFlow.lean:169

PROVED

error_le_geom_sum

Discrete Grönwall — geom-sum form

G 10 · LeanMining/VerifiedNeuralCompilation/RWKVStability.lean:39

PROVED

error_le_geom_closed

Discrete Grönwall — closed form δ/(1−γ)

G 10 · LeanMining/VerifiedNeuralCompilation/RWKVStability.lean:60

PROVED

affine_error_le_geom_sum

Affine perturbation — geom-sum

G 10 · LeanMining/VerifiedNeuralCompilation/RWKVStability.lean:87

PROVED

affine_error_le_closed

Affine perturbation — closed form

G 10 · LeanMining/VerifiedNeuralCompilation/RWKVStability.lean:129

PROVED

affine_error_le_closed_per_channel

Per-channel closed-form envelope

G 10 · LeanMining/VerifiedNeuralCompilation/RWKVStability.lean:152

PROVED

affine_error_le_closed_per_channel_sup

Sup-δ certification (Lean-faithful)

G 10 · LeanMining/VerifiedNeuralCompilation/RWKVStability.lean:174

PROVED

affine_error_linf_le_per_channel_envelope

L∞ channel aggregator

G 10 · LeanMining/VerifiedNeuralCompilation/RWKVStability.lean:192

PROVED

affine_error_l2_le_per_channel_envelope

L2 channel aggregator

G 10 · LeanMining/VerifiedNeuralCompilation/RWKVStability.lean:221

PROVED

affine_state_bound_geom_sum

Affine state bound — geom-sum

G 10 · LeanMining/VerifiedNeuralCompilation/RWKVStability.lean:262

PROVED

affine_state_bound_closed

Affine state bound — closed form

G 10 · LeanMining/VerifiedNeuralCompilation/RWKVStability.lean:295

PROVED

quotient_lipschitz

WKV readout quotient Lipschitz

G 10 · LeanMining/VerifiedNeuralCompilation/RWKVStability.lean:327

PROVED

combine_assoc

Scan-monoid associativity (parallel ≡ sequential)

G 10 · LeanMining/VerifiedNeuralCompilation/RWKVStability.lean:392

PROVED

block_error_le_geom_sum

Blockwise stability — geom-sum

G 10 · LeanMining/VerifiedNeuralCompilation/RWKVStability.lean:412

PROVED

block_error_le_closed

Blockwise stability — closed form

G 10 · LeanMining/VerifiedNeuralCompilation/RWKVStability.lean:426

PROVED

attention_output_split

Hybrid attention split linearity

G 10.5 · LeanMining/VerifiedNeuralCompilation/RWKVStability.lean:438

PROVED

hybrid_output_error_bound

Hybrid reconstruction Frobenius bound

G 10.5 · LeanMining/VerifiedNeuralCompilation/RWKVStability.lean:451

PROVED

sparse_smooth_mass_decomposition

Row-stochastic mass split (top-k + complement)

G 10.5 · LeanMining/VerifiedNeuralCompilation/RWKVStability.lean:495

PROVED

not_lowBudgetSmoothClosurePass_of_gate_failure

Low-budget smooth-closure kill (gate failure)

G 10 · LeanMining/VerifiedNeuralCompilation/RWKVStability.lean:534

PROVED

lowBudgetGlobalG10_kill_certificate_of_smooth_gate_failure

Low-budget global G_10 kill cert (smooth gate)

G 10 · LeanMining/VerifiedNeuralCompilation/RWKVStability.lean:540

PROVED

lowBudgetGlobalG10_kill_certificate_of_routing_gate_failure

Low-budget global G_10 kill cert (routing gate)

G 10 · LeanMining/VerifiedNeuralCompilation/RWKVStability.lean:554

PROVED

Source + reproduction