AXLE_v5_1.lean
✓aspect_ratio_encodes_invariants
✓closurePoints_stationary
✓closurePoints_unbounded
✓crystal_aspect_ratio
✓crystal_base_perimeter
✓g6_equals_schumann
✓levelToOrdinal_strictMono
⚠mahlo_levels_exist
✓nextLevel_layer_count_gt
✓noiseTolerance
✓ordinalNextLevel_is_closure_point
✓ordinalNextLevel_level_gt
✓ordinal_regeneration_step
✓ordinal_regeneration_unbounded
✓regeneration_hierarchy_mahlo
✓regeneration_step
✓regeneration_unbounded
✓stabilityRadius_eq
✓sup_lt_of_regular
✓sup_strictMono_isLimit
AXLE_v6.lean
✓aspect_ratio_encodes_invariants
✓closurePoints_stationary
✓closurePoints_unbounded
✓collective_threshold_grows_with_agents
⚠collective_threshold_grows_with_circuits
✓crystal_aspect_ratio
✓crystal_base_perimeter
✓det_M_equals_64
⚠dm3_euler_preservation
⚠dm3_volume_invariant
✓effective_threshold_increases
✓effective_threshold_one
✓effective_threshold_zero
✓g64_equals_tau_sixth
✓g64_equals_two_sixth
✓g64_is_kether_orthogon
✓g6_equals_schumann
✓g6_equals_tau5_plus_one
✓g6_is_33
✓g6_is_minimum_monster
⚠g6_lattice_invariant
✓g6_less_than_g64
⚠g6_symmetry_preservation
✓g7_greater_than_g6
✓g7_value
⚠gronwall_contraction_below_stability_radius
✓gtct_effective_threshold_after_circuit
⚠gtct_return_stable_within_radius
⚠gtct_t1
✓levelToOrdinal_strictMono
✓mahlo_levels_exist
✓nextLevel_layer_count_gt
⚠noiseTolerance
✓ordinalNextLevel_is_closure_point
✓ordinalNextLevel_level_gt
✓ordinal_regeneration_step
✓ordinal_regeneration_unbounded
✓regeneration_hierarchy_mahlo
⚠regeneration_hierarchy_mahlo_unconditional
⚠regeneration_loop_invariant
✓regeneration_step
✓regeneration_unbounded
✓separation_step1
✓separation_step2_euler_characteristic
⚠separation_theorem
✓stabilityRadius_eq
✓stability_radius_from_gronwall
✓sup_lt_of_regular
✓sup_strictMono_isLimit
✓tau_embodiment
✓tau_is_two
AutophagyDm3.lean
✓V_at_one
✓V_critical_at_one
✓V_double_root
✓V_factored
✓V_second_deriv_at_one
✓V_second_deriv_ne_zero
✓basin_asymmetry
✓contactCoeff_ne_zero
✓contactCoeff_neg
✓contactForm_nondeg_full
⚠dΦ_at_threshold
✓dΦ_pos
✓gronwall_radius
✓gronwall_radius_lt_one
✓gronwall_radius_pos
⚠limitCycle_exists_auto
✓mu_canonical
✓mu_dm3
✓mu_dm3_neg
✓whitneyFold_from_kinase_data
AutophagyDm3_v2.lean
✓V_at_one
✓V_critical_at_one
✓V_double_root
✓V_factored
✓V_is_morse_at_one
✓V_second_deriv_at_one
✓V_second_deriv_ne_zero
✓basin_asymmetry
✓contactCoeff_ne_zero
✓contactCoeff_neg
✓contactForm_nondeg_scalar
⚠contactForm_orientation
✓dm3_basin_compact
✓dm3_basin_nonempty
✓dΦ_at_threshold
✓dΦ_pos
✓gronwall_radius
✓gronwall_radius_lt_one
✓gronwall_radius_pos
⚠limitCycle_exists_auto
✓mu_canonical
✓mu_dm3
✓mu_dm3_neg
⚠omega_limit_nonempty
⚠whitneyFold_conditional
DiscreteDM3.lean
✓M_collatz_iff_E_collatz
✓collatz_converges
✓collatz_operatorDecomposition
✓entropy_monotone
Dm3Comp.lean
⚠PNP_operatorDecomposition
Dm3GoldbachToy.lean
✓E_goldbach_iff_attractor
✓M_goldbach_iff_E_goldbach
✓entropy_monotone
✓goldbach_operatorDecomposition
✓goldbach_toy_converges
✓iterate_goldbachStep_n
✓iterate_to_attractor
Dm3NSToy.lean
✓E_ns_iff_attractor
✓M_ns_iff_E_ns
✓energy_bounded
✓entropy_monotone
✓iterate_nsStep_energy
✓iterate_to_attractor
✓ns_operatorDecomposition
✓ns_toy_converges
Dm3RHToy.lean
✓C_rh_abs_decreases
✓C_rh_neg
✓C_rh_pos
✓C_rh_zero
✓E_rh_iff_attractor
✓M_rh_iff_E_rh
✓entropy_monotone
✓iterate_rhStep_natAbs
✓iterate_to_attractor
✓rh_operatorDecomposition
✓rh_toy_converges
Examples.lean
✓f1_antitone
Main_v6.lean
✓aspect_ratio_encodes_invariants
✓closurePoints_stationary
✓closurePoints_unbounded
✓collective_threshold_grows_with_agents
⚠collective_threshold_grows_with_circuits
✓crystal_aspect_ratio
✓crystal_base_perimeter
✓det_M_equals_64
⚠dm3_euler_preservation
⚠dm3_volume_invariant
✓effective_threshold_increases
✓effective_threshold_one
✓effective_threshold_zero
✓g64_equals_tau_sixth
✓g64_equals_two_sixth
✓g64_is_kether_orthogon
✓g6_equals_schumann
✓g6_equals_tau5_plus_one
✓g6_is_33
✓g6_is_minimum_monster
⚠g6_lattice_invariant
✓g6_less_than_g64
⚠g6_symmetry_preservation
✓g7_greater_than_g6
✓g7_value
⚠gronwall_contraction_below_stability_radius
✓gtct_effective_threshold_after_circuit
⚠gtct_return_stable_within_radius
⚠gtct_t1
✓levelToOrdinal_strictMono
✓mahlo_levels_exist
✓nextLevel_layer_count_gt
⚠noiseTolerance
✓ordinalNextLevel_is_closure_point
✓ordinalNextLevel_level_gt
✓ordinal_regeneration_step
✓ordinal_regeneration_unbounded
✓regeneration_hierarchy_mahlo
⚠regeneration_hierarchy_mahlo_unconditional
⚠regeneration_loop_invariant
✓regeneration_step
✓regeneration_unbounded
✓separation_step1
✓separation_step2_euler_characteristic
⚠separation_theorem
✓stabilityRadius_eq
✓stability_radius_from_gronwall
✓sup_lt_of_regular
✓sup_strictMono_isLimit
✓tau_embodiment
✓tau_is_two
Monotonicity.lean
✓S_negative
✓f_schumann_antitone_in_h
✓f_schumann_monotone_in_κ
MultiChamber.lean
✓coupled_eigenvalue_decreases
✓dm3_curvature_lowers_coupled_modes
✓perturbation_term_nonneg
✓wall_offset_sensitivity
NonCommutativity_v4.lean
✓commuting_instance
✓exists_order_dependent
✓foldMap_not_odd
✓nonCommutativity_instance
✓nonCommutativity_nondegenerate
✓not_forall_order_dependent
✓thm_5_3_is_exactly_existential
TribonacciMeasure.lean
✓tribonacci_succ3
✓weight_pos
✓weight_strictAnti
TribonacciRatioConvergence.lean
⚠LinearRecurrence.tendsto_succ_div_of_dominant_simple_root
⚠alpha_beta_ne_real
⚠alpha_modulus_eq
⚠alpha_modulus_lt_one
⚠alpha_ne_beta
⚠binet_coeffs_conj_symmetric
⚠eta_cubic
✓eta_inv_eq
⚠eta_mem_Ioo
⚠eta_ne_alpha
⚠eta_ne_beta
✓eta_ne_zero
⚠eta_pos
⚠exists_binet_coeffs
⚠geom_alpha_isSol
⚠geom_beta_isSol
⚠geom_eta_isSol
⚠tendsto_trib_succ_div_trib_atTop
⚠tribCharPoly_factor
⚠tribRec_charPoly_eq
⚠trib_closed_form
⚠trib_geom_basis
✓trib_quotient_discrim_eq
✓trib_quotient_discrim_neg
✓trib_quotient_no_real_root
⚠triboM_eigen_eq
⚠triboM_eigenvector_pos
TripleChamber.lean
✓bessel_ratio_def
✓bessel_ratio_in_tribonacci_interval
✓canonical_coupling_ladder
✓triple_chamber_strictAnti_in_κ
✓triple_coupled_eigenvalue_decreases
✓triple_degenerate_at_zero_coupling
✓triple_dm3_curvature_lowers_all_modes
✓triple_mode_splitting_brackets
✓triple_perturbation_nonneg
TwinPrime_dm3.lean
✓criticalGap_antitone
✓criticalGap_pos
✓fold_fires_of_le_sq
✓gap_ladder
✓gap_ladder_descends
✓prime_flow_lyapunov_stable
⚠prime_gap_rh_bound
✓twin_prime_dm3
✓twin_prime_is_minimum_fold
✓twin_prime_poincare_recurrence
⚠zhang_bounded_gap
✓zhang_fold_operator
finite.lean
✓affine_line_ne_top
✓finite_kakeya_thickened_positive_measure
✓finite_segments_measure_zero
✓segment_measure_zero
✓span_singleton_lt_top
✓thickened_segment_pos_measure
gronwall_proof.lean
⚠gronwall_contraction_below_stability_radius
Autophagy/AutophagyDm3_v2.lean
✓V_at_one
✓V_critical_at_one
✓V_double_root
✓V_factored
✓V_is_morse_at_one
✓V_second_deriv_at_one
✓V_second_deriv_ne_zero
✓basin_asymmetry
✓contactCoeff_ne_zero
✓contactCoeff_neg
✓contactForm_nondeg_scalar
⚠contactForm_orientation
✓dm3_basin_compact
✓dm3_basin_nonempty
✓dΦ_at_threshold
✓dΦ_pos
✓gronwall_radius
✓gronwall_radius_lt_one
✓gronwall_radius_pos
⚠limitCycle_exists_auto
✓mu_canonical
✓mu_dm3
✓mu_dm3_neg
⚠omega_limit_nonempty
⚠whitneyFold_conditional
BioPhysics/MultiAgentTogt.lean
⚠T10_Lipschitz_lt_one
✓T11_subthreshold
✓T12_superthreshold
✓T13_branch_sanity
✓T14_reduction_factor
✓T15_circadian_anchor
✓T16_immune_zero_fp
✓T17_dm3_product
✓T18_contraction_compose
✓T1_threshold_interior
✓T2_subthreshold_contracts
✓T3_boundary_Lipschitz
✓T4_six_iterate_bound
✓T5_six_iterate_coarse
✓T6a_Tstar_pos
✓T6b_mumax_neg
✓T6c_tau_pos
✓T7_C_well_typed
✓T8_C_contracts_toward_mean
✓T9_clip_bound
CatGT/1finite.lean
⚠finite_kakeya_thickened_positive_measure
✓finite_segments_measure_zero
⚠segment_measure_zero
✓thickened_segment_pos_measure
CatGT/AXLE.lean
⚠closurePoints_stationary_regular
⚠collatz_conjecture_via_dm3_gqm
⚠crystal_lockin
⚠d6_lockin
⚠embedding_intertwining
⚠g6_unconditional_closure
CatGT/AXLE8.lean
⚠closurePoints_stationary_regular
⚠collatz_conjecture_via_dm3_gqm
⚠crystal_lockin
⚠d6_lockin
⚠embedding_intertwining
⚠g6_unconditional_closure
CatGT/CatGT_Main.lean
✓catgt_dm3_transport
✓criticalRadius_antitone
✓criticalRadius_pos
✓dnls_norm_conservation_ideal
⚠ensemble_scaling
✓helical_selectivity
✓ipr_between_zero_and_one
✓reeb_orbit_is_integral
✓selectivityFactor_eq
CatGT/Criticality_Principle.lean
✓collatz_c3_critical
⚠double_root_at_q_one
✓double_root_at_q_one_shifted
⚠double_root_deriv_zero
✓double_root_factored
✓fold_factorization_c3
✓kakeya_3d_critical
✓navier_stokes_3d_critical
✓ns_three_entropies_compatible
✓pentanacci_5_supercritical
✓ricci_3d_critical
✓tetranacci_4_supercritical
✓tribonacci_3_critical
CatGT/D6.lean
✓P12_identity
⚠d6_lockin
⚠orthogonalStepping_preserved
CatGT/DustyPlasma.lean
✓coherence_bridge_identity
✓fast_rate_exceeds_sweetparker_at_threshold
✓lundquist_pos
✓mhd_fold_operator_formal
✓operator_order_plasma
✓plasma_contactomorphism
✓plasma_r_star_antitone
✓plasma_r_star_pos
✓plasmoid_growth_pos
✓plasmoid_threshold_pos
✓reconnection_rate_bounded
⚠reconnection_rate_saturation
✓sweetparker_rate_antitone
✓sweetparker_rate_pos
CatGT/Finite.lean
✓affine_line_ne_top
⚠finite_kakeya_thickened_positive_measure
✓finite_segments_measure_zero
✓segment_measure_zero
✓span_singleton_ne_top
✓thickened_segment_pos_measure
✓unitSegment_zero
CatGT/G6.lean
⚠crystal_lockin
✓crystal_order_six
✓weight_positive
CatGT/Gronwall.lean
⚠gronwall_contraction_below_stability_radius
CatGT/MahloClosure.lean
⚠club_filter_intersection_nonempty
⚠crystal_saturation_lifts_to_transfinite
⚠g6_unconditional_closure
✓omega_omega_is_limit
CatGT/Main.lean
✓aspect_ratio_encodes_invariants
✓closurePoints_stationary
✓closurePoints_unbounded
✓crystal_aspect_ratio
✓crystal_base_perimeter
✓g6_equals_schumann
✓levelToOrdinal_strictMono
⚠mahlo_levels_exist
✓nextLevel_layer_count_gt
✓noiseTolerance
✓ordinalNextLevel_is_closure_point
✓ordinalNextLevel_level_gt
✓ordinal_regeneration_step
✓ordinal_regeneration_unbounded
✓regeneration_hierarchy_mahlo
✓regeneration_step
✓regeneration_unbounded
✓stabilityRadius_eq
✓sup_lt_of_regular
✓sup_strictMono_isLimit
CatGT/Main_v2.lean
✓aspect_ratio_encodes_invariants
✓crystal_aspect_ratio
✓crystal_base_perimeter
✓g6_equals_schumann
✓nextLevel_layer_count_gt
✓noiseTolerance
✓regeneration_step
✓regeneration_unbounded
✓stabilityRadius_eq
CatGT/Main_v3.lean
✓aspect_ratio_encodes_invariants
✓crystal_aspect_ratio
✓crystal_base_perimeter
✓firstFixedPointAbove_gt
✓fixedPoints_unbounded
✓g6_equals_schumann
✓levelToOrdinal_monotone
✓nextLevel_layer_count_gt
✓noiseTolerance
✓ordinalNextLevel_level_gt
✓ordinal_regeneration_step
✓ordinal_regeneration_unbounded
✓regeneration_step
✓regeneration_unbounded
✓stabilityRadius_eq
CatGT/Main_v3_corrected.lean
✓aspect_ratio_encodes_invariants
✓closurePoints_unbounded
✓crystal_aspect_ratio
✓crystal_base_perimeter
✓g6_equals_schumann
⚠levelToOrdinal_strictMono
✓nextLevel_layer_count_gt
✓noiseTolerance
✓ordinalNextLevel_is_closure_point
✓ordinalNextLevel_level_gt
✓ordinal_regeneration_step
✓ordinal_regeneration_unbounded
✓regeneration_step
✓regeneration_unbounded
✓stabilityRadius_eq
CatGT/Main_v4.lean
✓aspect_ratio_encodes_invariants
⚠closurePoints_stationary
✓closurePoints_unbounded
✓crystal_aspect_ratio
✓crystal_base_perimeter
✓g6_equals_schumann
✓levelToOrdinal_strictMono
⚠mahlo_levels_exist
✓nextLevel_layer_count_gt
✓noiseTolerance
✓ordinalNextLevel_is_closure_point
✓ordinalNextLevel_level_gt
✓ordinal_regeneration_step
✓ordinal_regeneration_unbounded
✓regeneration_hierarchy_mahlo
✓regeneration_step
✓regeneration_unbounded
✓stabilityRadius_eq
CatGT/Main_v5.lean
✓aspect_ratio_encodes_invariants
✓closurePoints_stationary
✓closurePoints_unbounded
✓crystal_aspect_ratio
✓crystal_base_perimeter
✓g6_equals_schumann
✓levelToOrdinal_strictMono
⚠mahlo_levels_exist
✓nextLevel_layer_count_gt
✓noiseTolerance
✓ordinalNextLevel_is_closure_point
✓ordinalNextLevel_level_gt
✓ordinal_regeneration_step
✓ordinal_regeneration_unbounded
✓regeneration_hierarchy_mahlo
✓regeneration_step
✓regeneration_unbounded
✓stabilityRadius_eq
✓sup_lt_of_regular
✓sup_strictMono_isLimit
CatGT/axle_togt_canonical.lean
✓collective_threshold_grows_with_agents
⚠collective_threshold_grows_with_circuits
✓det_M_equals_64
✓effective_threshold_increases
✓effective_threshold_one
✓effective_threshold_zero
✓g64_equals_tau_sixth
✓g64_equals_two_sixth
✓g64_is_kether_orthogon
✓g6_is_33
✓g6_is_minimum_monster
✓g6_less_than_g64
✓g7_greater_than_g6
✓g7_value
✓graphene_tau_matches_canonical
⚠tau_embodiment_threshold
✓tau_is_two
CatGT/dm3_Criticality_gtct.lean
⚠collatz_c3_critical
⚠double_root_at_q_one
⚠fold_factorization_c3
⚠hexagonal_eigenmode_crystal_saturated
⚠navier_stokes_3d_critical
⚠ricci_3d_critical
CatGT/dm³Criticality.lean
⚠criticality_vs_supercritical_ladder
⚠pentanacci_5_strong_supercritical
⚠tetranacci_4_mild_supercritical
⚠tribonacci_3_critical
CatGT/dm³_Operator_Formalization.lean
✓dm3_fixed_point
CatGT/fitribonacci.lean
⚠dm3_lockin
✓net_height_decrease
✓no_alternative_cycle
✓no_escape_to_infinity
✓valTwo_after_K
CatGT/gronwall_contraction_below_stability_radius.lean
✓gronwall_contraction_below_stability_radius
CatGT/gronwall_proof.lean
⚠gronwall_contraction_below_stability_radius
CatGT/gtct_t1.lean
⚠gtct_t1
CatGT/main_v7.lean
✓closurePoints_stationary
✓closurePoints_unbounded
⚠dm3_euler_preservation
⚠dm3_volume_invariant
⚠g6_lattice_invariant
⚠g6_symmetry_preservation
⚠gronwall_contraction_below_stability_radius
⚠gtct_t1
✓nextLevel_layer_count_gt
✓noiseTolerance
⚠regeneration_loop_invariant
⚠separation_theorem
✓stabilityRadius_eq
✓sup_lt_of_regular
✓sup_strictMono_isLimit
CatGT/regeneration_loop_invariant.lean
⚠regeneration_loop_invariant
CatGT/separation_theorem.lean
⚠separation_theorem
DNLS/FoldEvents.lean
⚠G_iter_thirty_three
✓G_iter_threshold
✓G_iter_zero_eq_min
✓G_le_threshold
✓G_monotone
✓g6_hex_lockin
✓g6_hex_lockin_in_orbit
✓stability_at_threshold
DNLS/TribonacciDNLS.lean
⚠tribonacci_rec
✓w_antitone
✓w_pos
✓w_strictAnti
✓w_tendsto_zero
EMMEs/PolarVortex.lean
✓a7_prevents_collapse
✓collatz_contraction_neg
✓collatz_triad_is_cycle
✓collatz_triad_size
✓collatz_vortex_parallel_precise
✓exterior_flows_inward
✓g6_condition_holds
✓g6_factors
✓interior_flows_outward
✓limit_cycle_is_fixed_point
✓moat_is_invariant
✓moat_nonempty
✓pole_is_fixed_point
✓pole_is_unstable
✓spatial_separation
✓three_layer_uniqueness_up_to_iso
✓vortex_hexagon_decoupled
✓vortex_inside_stability_ball
✓vortex_lyapunov_stable
✓vortex_not_at_pole
✓vortex_pv_is_barrier
EMMEs/SaturnRing.lean
✓cassini_gap_width
✓dual_resonance_consistency
✓dual_resonance_stability
✓hex_six_factors
✓hex_sixfold
✓monster_threshold_eq
✓ring_lyapunov_nonneg
✓ring_lyapunov_zero_iff
✓ring_satisfies_all_dm3_axioms
✓ring_transverse_stable_neg
✓stability_condition
✓stability_product
FruitFly/MultiOrbitBioSwarm.lean
✓Tstar_pos
✓alpha_03_contractive
⚠bio_pitchfork
✓collective_fixed_point
✓lipschitz_at_alpha_03
✓lipschitz_at_threshold
✓lipschitz_contraction
✓lipschitz_lb
✓mu_max_neg
✓six_iterate_bound
✓six_iterate_bound_pos
✓swarm_contraction
✓tau_eq_abs_mu
⚠tau_pos
✓threshold_lt_one
✓threshold_pos
GTCT/AXLE.lean
⚠closurePoints_stationary_regular
⚠collatz_conjecture_via_dm3_gqm
⚠crystal_lockin
⚠d6_lockin
⚠embedding_intertwining
⚠g6_unconditional_closure
GTCT/AXLE8.lean
⚠closurePoints_stationary_regular
⚠collatz_conjecture_via_dm3_gqm
⚠crystal_lockin
⚠d6_lockin
⚠embedding_intertwining
⚠g6_unconditional_closure
GTCT/Criticality_Principle.lean
⚠collatz_c3_critical
⚠double_root_at_q_one
⚠fold_factorization_c3
⚠kakeya_3d_critical
⚠navier_stokes_3d_critical
⚠ns_three_entropies_compatible
⚠pentanacci_5_supercritical
⚠ricci_3d_critical
⚠tetranacci_4_supercritical
⚠tribonacci_3_critical
GTCT/dm3_Criticality_gtct.lean
⚠collatz_c3_critical
⚠double_root_at_q_one
⚠fold_factorization_c3
⚠hexagonal_eigenmode_crystal_saturated
⚠navier_stokes_3d_critical
⚠ricci_3d_critical
GTCT/dm³ Criticality/dm³Criticality.lean
⚠criticality_vs_supercritical_ladder
⚠pentanacci_5_strong_supercritical
⚠tetranacci_4_mild_supercritical
⚠tribonacci_3_critical
Intelligence/SwarmSimulator.lean
✓T10_Ln_decreasing
✓T11_composition_contraction
⚠T12_state_space_dim
✓T1_contraction
✓T2_unique_fixedpoint
✓T3_global_convergence
✓T4_L_positive
✓T5_L_lt_one
✓T6_stabilise_decreases
✓T7_coordinate_decreases
✓T8_diffuse_increasing
✓T9_system_inv_strict
Multi-Orbit-Theory/MultiOrbitTogt.lean
✓T10_B3_collapse_def
✓T11_composition_preserves
✓T12_cycle_typed
✓T13_embodiment_shrink
✓T14_boundary_params_pos
✓T15_U1_commutative
⚠T16_finite_index
✓T1_invariant_constant
✓T2_system_inv_strict
✓T3a_U1_le_left
✓T3b_U1_le_right
✓T4_U2_preserves
✓T5_U3_synthesis
✓T6_R1_symmetric
✓T7_R2_increases
✓T8_R2_unbounded
✓T9_B2_decidable
NASA/MoonBase/AXLE_lean_files/AutophagyDm3_v2.lean
✓V_at_one
✓V_critical_at_one
✓V_double_root
✓V_factored
✓V_second_deriv_at_one
✓V_second_deriv_ne_zero
✓basin_asymmetry
✓contactCoeff_ne_zero
✓contactCoeff_neg
✓contactForm_nondeg_full
⚠dΦ_at_threshold
✓dΦ_pos
✓gronwall_radius
✓gronwall_radius_lt_one
✓gronwall_radius_pos
⚠limitCycle_exists_auto
✓mu_canonical
✓mu_dm3
⚠mu_dm3_neg
✓whitneyFold_from_kinase_data
NASA/MoonBase/AXLE_lean_files/Chain_updated.lean
✓GChain.iter_add
✓g33_stability_index
✓gronwall_outer
✓iter_consecutive_dist
✓poincare_collatz_contracting
✓r_star_lt_one
✓r_star_pos
✓spiral_return_exists
NASA/MoonBase/AXLE_lean_files/G6Crystal.lean
✓arnold_tongue_A4_coupling
✓aspect_ratio_encoded
✓aspect_ratio_eq
✓aspect_ratio_scale_invariant
✓base_side_metres
✓colony_depth1_cells
⚠colony_depth2_cells
✓dm3_Tstar_pos
✓dm3_epsilon0
✓dm3_mumax_neg
✓dm3_noise_tol_lt_one
✓dm3_noise_tolerance
✓dm3_tau_eq_abs_mumax
✓dm3_tau_pos
✓epsilon0_gravity_independent
✓epsilon0_lt_one
✓epsilon0_pos
✓g6_within_16pct
✓g6_within_2pct_of_f4
✓g_mars_lt_earth
✓g_moon_lt_earth
✓growth_factor_gt_one
✓height_metres
✓hex_beats_square
✓hex_embedding_real
✓hex_improvement_gt_115
✓hexagrid_collapse_resistance_superior
✓layer_height_cubits
✓lunar_crystal_taller
✓mars_height_within_troposphere
✓nasa_payload_mono
✓noise_tol_covers_g6_error
✓payload_ratio_phase_1_2
✓schumann_n4_sqrt
✓stability_band_width
NASA/MoonBase/AXLE_lean_files/Main_v6.lean
✓aspect_ratio_encodes_invariants
✓closurePoints_stationary
✓closurePoints_unbounded
✓collective_threshold_grows_with_agents
⚠collective_threshold_grows_with_circuits
✓crystal_aspect_ratio
✓crystal_base_perimeter
✓det_M_equals_64
✓dm3_euler_preservation
✓dm3_volume_invariant
✓effective_threshold_increases
✓effective_threshold_one
✓effective_threshold_zero
✓g64_equals_tau_sixth
✓g64_equals_two_sixth
✓g64_is_kether_orthogon
✓g6_equals_schumann
✓g6_equals_tau5_plus_one
✓g6_is_33
✓g6_is_minimum_monster
✓g6_lattice_invariant
✓g6_less_than_g64
✓g6_symmetry_preservation
✓g7_greater_than_g6
✓g7_value
✓gronwall_contraction_below_stability_radius
✓gtct_effective_threshold_after_circuit
⚠gtct_return_stable_within_radius
✓gtct_t1
✓levelToOrdinal_strictMono
✓mahlo_levels_exist
✓nextLevel_layer_count_gt
⚠noiseTolerance
✓ordinalNextLevel_is_closure_point
✓ordinalNextLevel_level_gt
✓ordinal_regeneration_step
✓ordinal_regeneration_unbounded
✓regeneration_hierarchy_mahlo
✓regeneration_hierarchy_mahlo_unconditional
✓regeneration_loop_invariant
✓regeneration_step
✓regeneration_unbounded
✓separation_step1
✓separation_step2_euler_characteristic
✓separation_theorem
✓stabilityRadius_eq
✓stability_radius_from_gronwall
✓sup_lt_of_regular
✓sup_strictMono_isLimit
✓tau_embodiment
✓tau_is_two
NASA/MoonBase/AXLE_lean_files/MultiAgentTogt.lean
⚠T10_Lipschitz_lt_one
✓T11_subthreshold
✓T12_superthreshold
✓T13_branch_sanity
✓T14_reduction_factor
✓T15_circadian_anchor
✓T16_immune_zero_fp
✓T17_dm3_product
✓T18_contraction_compose
✓T1_threshold_interior
✓T2_subthreshold_contracts
✓T3_boundary_Lipschitz
✓T4_six_iterate_bound
✓T5_six_iterate_coarse
✓T6a_Tstar_pos
✓T6b_mumax_neg
✓T6c_tau_pos
✓T7_C_well_typed
✓T8_C_contracts_toward_mean
✓T9_clip_bound
NASA/MoonBase/AXLE_lean_files/MultiOrbitBioSwarm.lean
✓Tstar_pos
✓alpha_03_contractive
⚠bio_pitchfork
✓collective_fixed_point
✓lipschitz_at_alpha_03
✓lipschitz_at_threshold
✓lipschitz_contraction
✓lipschitz_lb
✓mu_max_neg
✓six_iterate_bound
✓six_iterate_bound_pos
✓swarm_contraction
✓tau_eq_abs_mu
⚠tau_pos
✓threshold_lt_one
✓threshold_pos
NASA/MoonBase/AXLE_lean_files/NASAGaps.lean
✓FN_A_104L_neighbor_traversal
✓FN_A_104L_reachability
✓FN_C_101L_ring_count
✓FN_H_101L_isoperimetric
✓FN_H_102L_phase02_cluster
✓FN_L_101L_hex_interfaces
✓FN_L_101L_unique_interface
✓FN_M_302L_hex_path_exists
✓FN_P_101L_schumann_proximity
✓FN_P_402L_noise_tolerance
✓FN_T_201L_payload_monotone
✓FN_T_201L_stage_gated
✓FN_T_202L_payload_ratio
✓FN_U_103L_expand_models_ISRU
✓FN_U_103L_six_layers
✓nasa_gap_closure_summary
NASA/MoonBase/AXLE_lean_files/PrincipiaVol1.lean
✓Phi_pos
✓V_at_one
✓V_critical_at_one
⚠V_factored
✓V_second_deriv_at_one
✓V_second_deriv_ne_zero
✓aspect_ratio_encodes_invariants
⚠basin_asymmetry
⚠closurePoints_stationary
✓closurePoints_unbounded
⚠contactCoeff_ne_zero
✓contactCoeff_neg
✓crystal_aspect_ratio
⚠dPhi_at_threshold
✓dPhi_pos
⚠g6_equals_schumann
✓gronwall_contraction_below_stability_radius
✓gronwall_radius
✓gronwall_radius_lt_one
✓gronwall_radius_pos
✓mu_canonical
⚠mu_dm3_neg
✓nextLevel_layer_count_gt
⚠noiseTolerance
✓ordinalNextLevel_is_closure_point
✓ordinal_regeneration_unbounded
⚠regeneration_hierarchy_mahlo
✓regeneration_unbounded
⚠separation_theorem
✓sup_lt_of_regular
✓sup_strictMono_isLimit
NASA/MoonBase/AXLE_lean_files/TribonacciDNLS.lean
⚠tribonacci_rec
✓w_antitone
✓w_pos
✓w_strictAnti
✓w_tendsto_zero
NASA/MoonBase/AXLE_lean_files/VolumeTwo.lean
✓Theorem_15_2_integrability
✓alternating_vanishes_beyond_dim
✓eigenvalue_at_zero
✓eigenvalue_limit
✓eigenvalue_neg_pos_z
✓embodimentThreshold_pos
✓entropy_lyapunov_duality
✓epsilon_zero_waddington
✓integrability_on_contact_distribution
✓integrability_on_full_contact_manifold
✓thm_A_contact_realization_fold
✓thm_B_threshold_equivalence
✓thm_C_singularity_bijection
✓toyModel_epsilon0
✓toyModel_tau
✓vol2_contact_Theorem_3_3
NASA/MoonBase/NASAGaps.lean
✓FN_A_104L_neighbor_traversal
✓FN_A_104L_reachability
✓FN_C_101L_ring_count
✓FN_H_101L_isoperimetric
✓FN_H_102L_phase02_cluster
✓FN_L_101L_hex_interfaces
✓FN_L_101L_unique_interface
✓FN_M_302L_hex_path_exists
✓FN_P_101L_schumann_proximity
✓FN_P_402L_noise_tolerance
✓FN_T_201L_payload_monotone
✓FN_T_201L_stage_gated
✓FN_T_202L_payload_ratio
✓FN_U_103L_expand_models_ISRU
✓FN_U_103L_six_layers
✓nasa_gap_closure_summary
Papers/AutophagyDm3.lean
✓V_at_one
✓V_critical_at_one
✓V_double_root
✓V_factored
✓V_second_deriv_at_one
✓V_second_deriv_ne_zero
✓basin_asymmetry
✓contactCoeff_ne_zero
✓contactCoeff_neg
✓contactForm_nondeg_full
⚠dΦ_at_threshold
✓dΦ_pos
✓gronwall_radius
✓gronwall_radius_lt_one
✓gronwall_radius_pos
⚠limitCycle_exists_auto
✓mu_canonical
✓mu_dm3
✓mu_dm3_neg
✓whitneyFold_from_kinase_data
PrincipiaOrthogona1/PrincipiaVol1.lean
✓Phi_pos
✓V_at_one
✓V_critical_at_one
⚠V_factored
✓V_second_deriv_at_one
✓V_second_deriv_ne_zero
✓aspect_ratio_encodes_invariants
⚠basin_asymmetry
⚠closurePoints_stationary
✓closurePoints_unbounded
✓commuting_instance
⚠contactCoeff_ne_zero
✓contactCoeff_neg
✓crystal_aspect_ratio
⚠dPhi_at_threshold
✓dPhi_pos
✓exists_order_dependent
✓foldMap_not_odd
⚠g6_equals_schumann
✓gronwall_contraction_below_stability_radius
✓gronwall_radius
✓gronwall_radius_lt_one
✓gronwall_radius_pos
✓mu_canonical
⚠mu_dm3_neg
✓nextLevel_layer_count_gt
⚠noiseTolerance
✓nonCommutativity_instance
✓nonCommutativity_nondegenerate
✓not_forall_order_dependent
✓ordinalNextLevel_is_closure_point
✓ordinal_regeneration_unbounded
⚠regeneration_hierarchy_mahlo
✓regeneration_unbounded
⚠separation_theorem
✓sup_lt_of_regular
✓sup_strictMono_isLimit
✓thm_5_3_is_exactly_existential
PrincipiaOrthogona1/Theorem53NonCommutativity.lean
✓commuting_instance
✓exists_order_dependent
✓foldMap_not_odd
✓nonCommutativity_instance
✓nonCommutativity_nondegenerate
✓not_forall_order_dependent
✓thm_5_3_is_exactly_existential
PrincipiaOrthogona_v2/VolumeTwo.lean
✓Theorem_15_2_integrability
✓alternating_vanishes_beyond_dim
✓eigenvalue_at_zero
✓eigenvalue_limit
✓eigenvalue_neg_pos_z
✓embodimentThreshold_pos
✓entropy_lyapunov_duality
✓epsilon_zero_waddington
✓integrability_on_contact_distribution
✓integrability_on_full_contact_manifold
✓thm_A_contact_realization_fold
✓thm_B_threshold_equivalence
✓thm_C_singularity_bijection
✓toyModel_epsilon0
✓toyModel_tau
✓vol2_contact_Theorem_3_3
SWARM/SwarmSimulator.lean
✓T10_Ln_decreasing
✓T11_composition_contraction
⚠T12_state_space_dim
✓T1_contraction
✓T2_unique_fixedpoint
✓T3_global_convergence
✓T4_L_positive
✓T5_L_lt_one
✓T6_stabilise_decreases
✓T7_coordinate_decreases
✓T8_diffuse_increasing
✓T9_system_inv_strict
WaveNumber6/Wavenumber6.lean
✓P6_identity_ZMod
✓Tstar_over_pi_eq_tau
✓Tstar_pos
✓V3_root_at_1
✓W3_deriv_zero_at_1
✓W3_double_root
✓W3_factored
✓W3_root_at_neg2
✓W3_zero_at_1
✓c_star_is_3
✓companion_char_poly
✓companion_det
✓companion_trace
✓dominant_root_bounds
✓dominant_root_gt_phi
✓eleven_prime
✓g33_factorization
✓g33_pos
✓g6_minimal
✓g_series_order
✓hexagonal_period
✓mu_max_neg
⚠six_first_even_multiple_of_3
✓six_is_monster
✓tau_eq_abs_mu
✓tau_pos
✓three_prime
✓tribonacci_above_golden_ratio
✓tribonacci_partition_bounds
✓tribonacci_partition_lb
✓tribonacci_partition_ub
✓tribonacci_poly_at_1
✓tribonacci_poly_at_1839
✓tribonacci_poly_at_1840
✓tribonacci_poly_at_2
✓tribonacci_root_in_bracket
✓wavenumber_derivation
✓wavenumber_is_minimal_even_triple
✓wavenumber_not_4
✓wavenumber_not_8
✓wavenumber_unique_depth3
a.PolyLaminin/AutophagyDm3.lean
✓V_at_one
✓V_critical_at_one
✓V_double_root
✓V_factored
✓V_second_deriv_at_one
✓V_second_deriv_ne_zero
✓basin_asymmetry
✓contactCoeff_ne_zero
✓contactCoeff_neg
✓contactForm_nondeg_full
⚠dΦ_at_threshold
✓dΦ_pos
✓gronwall_radius
✓gronwall_radius_lt_one
✓gronwall_radius_pos
⚠limitCycle_exists_auto
✓mu_canonical
✓mu_dm3
✓mu_dm3_neg
✓whitneyFold_from_kinase_data
a.PolyLaminin/AutophagyDm3_v2.lean
✓V_at_one
✓V_critical_at_one
✓V_double_root
✓V_factored
✓V_second_deriv_at_one
✓V_second_deriv_ne_zero
✓basin_asymmetry
✓contactCoeff_ne_zero
✓contactCoeff_neg
✓contactForm_nondeg_full
⚠dΦ_at_threshold
✓dΦ_pos
✓gronwall_radius
✓gronwall_radius_lt_one
✓gronwall_radius_pos
⚠limitCycle_exists_auto
✓mu_canonical
✓mu_dm3
⚠mu_dm3_neg
✓whitneyFold_from_kinase_data
dm3-dual-cavity/dm3-dual-cavity/TripleChamber.lean
✓bessel_ratio_def
✓bessel_ratio_in_tribonacci_interval
✓canonical_coupling_ladder
✓triple_chamber_strictAnti_in_κ
✓triple_coupled_eigenvalue_decreases
✓triple_degenerate_at_zero_coupling
✓triple_dm3_curvature_lowers_all_modes
✓triple_mode_splitting_brackets
✓triple_perturbation_nonneg
lean/1finite.lean
⚠finite_kakeya_thickened_positive_measure
✓finite_segments_measure_zero
⚠segment_measure_zero
✓thickened_segment_pos_measure
lean/AXLE.lean
⚠closurePoints_stationary_regular
⚠collatz_conjecture_via_dm3_gqm
⚠crystal_lockin
⚠d6_lockin
⚠embedding_intertwining
⚠g6_unconditional_closure
lean/AXLE_V8.lean
✓closurePoints_stationary
✓closurePoints_stationary_regular
✓closurePoints_unbounded
⚠crystal_lockin
⚠dm3_euler_preservation
⚠dm3_volume_invariant
✓mahlo_closure
✓noiseTolerance
✓regeneration_loop_invariant
✓stabilityRadius_eq
✓sup_lt_of_regular
✓sup_strictMono_isLimit
lean/AXLE_v8.1.lean
⚠closurePoints_stationary_regular
⚠collatz_conjecture_via_dm3_gqm
⚠crystal_lockin
⚠d6_lockin
⚠g6_unconditional_closure
lean/ContactHopf.lean
⚠contactHopf_bifurcation
✓erroneous_root_is_exp
✓gammaStar_eq_two_mul_old
⚠gammaStar_is_root
✓gammaStar_ne_zero
✓gammaStar_pos
✓linearization_discrepancy
✓linearization_erroneous_expansion
lean/Crystal/G6.lean
⚠crystal_lockin
✓crystal_order_six
✓weight_positive
lean/Dm3Arithmetic.lean
✓flowAux_ode
✓flow_equilibrium_at_one
⚠flow_ode
⚠flow_zero
✓r_star_lt_one
✓r_star_mem_Ioo
✓r_star_pos
✓z₀_neg
lean/Dm3Arithmetic_fixed.lean
✓flowAux_ode
✓flow_equilibrium_at_one
⚠flow_ode
⚠flow_zero
✓r_star_lt_one
✓r_star_mem_Ioo
✓r_star_pos
✓z₀_neg
lean/ExistenceWellPosedness.lean
⚠Phi_contracts
⚠Phi_iterates_converge
⚠Phi_wellPosed
✓compression_contracts
✓compression_strict
✓names
lean/Finite.lean
✓affine_line_ne_top
⚠finite_kakeya_thickened_positive_measure
✓finite_segments_measure_zero
✓segment_measure_zero
✓span_singleton_ne_top
✓thickened_segment_pos_measure
✓unitSegment_zero
lean/FiniteBranching.lean
⚠analytic_zeros_isolated
⚠discrete_closed_in_compact_finite
⚠finiteBranching
lean/Gronwall.lean
⚠gronwall_contraction_below_stability_radius
lean/GronwallExtention.lean
⚠return_map_contraction
lean/Invariant75.lean
✓cos_three_pi_div_two
✓gerono_fails_conditionD
✓gerono_not_injOn
✓gerono_pi_div_two
✓gerono_self_intersects
✓gerono_three_pi_div_two
✓invariant_7_5_injective
lean/Main.lean
✓aspect_ratio_encodes_invariants
✓closurePoints_stationary
✓closurePoints_unbounded
✓crystal_aspect_ratio
✓crystal_base_perimeter
✓g6_equals_schumann
✓levelToOrdinal_strictMono
⚠mahlo_levels_exist
✓nextLevel_layer_count_gt
✓noiseTolerance
✓ordinalNextLevel_is_closure_point
✓ordinalNextLevel_level_gt
✓ordinal_regeneration_step
✓ordinal_regeneration_unbounded
✓regeneration_hierarchy_mahlo
✓regeneration_step
✓regeneration_unbounded
✓stabilityRadius_eq
✓sup_lt_of_regular
✓sup_strictMono_isLimit
lean/Main_v2.lean
✓aspect_ratio_encodes_invariants
✓crystal_aspect_ratio
✓crystal_base_perimeter
✓g6_equals_schumann
✓nextLevel_layer_count_gt
✓noiseTolerance
✓regeneration_step
✓regeneration_unbounded
✓stabilityRadius_eq
lean/Main_v3_corrected.lean
✓aspect_ratio_encodes_invariants
✓closurePoints_unbounded
✓crystal_aspect_ratio
✓crystal_base_perimeter
✓g6_equals_schumann
⚠levelToOrdinal_strictMono
✓nextLevel_layer_count_gt
✓noiseTolerance
✓ordinalNextLevel_is_closure_point
✓ordinalNextLevel_level_gt
✓ordinal_regeneration_step
✓ordinal_regeneration_unbounded
✓regeneration_step
✓regeneration_unbounded
✓stabilityRadius_eq
lean/Main_v4.lean
✓aspect_ratio_encodes_invariants
⚠closurePoints_stationary
✓closurePoints_unbounded
✓crystal_aspect_ratio
✓crystal_base_perimeter
✓g6_equals_schumann
✓levelToOrdinal_strictMono
⚠mahlo_levels_exist
✓nextLevel_layer_count_gt
✓noiseTolerance
✓ordinalNextLevel_is_closure_point
✓ordinalNextLevel_level_gt
✓ordinal_regeneration_step
✓ordinal_regeneration_unbounded
✓regeneration_hierarchy_mahlo
✓regeneration_step
✓regeneration_unbounded
✓stabilityRadius_eq
lean/Main_v5.lean
✓aspect_ratio_encodes_invariants
✓closurePoints_stationary
✓closurePoints_unbounded
✓crystal_aspect_ratio
✓crystal_base_perimeter
✓g6_equals_schumann
✓levelToOrdinal_strictMono
⚠mahlo_levels_exist
✓nextLevel_layer_count_gt
✓noiseTolerance
✓ordinalNextLevel_is_closure_point
✓ordinalNextLevel_level_gt
✓ordinal_regeneration_step
✓ordinal_regeneration_unbounded
✓regeneration_hierarchy_mahlo
✓regeneration_step
✓regeneration_unbounded
✓stabilityRadius_eq
✓sup_lt_of_regular
✓sup_strictMono_isLimit
lean/NonCommutativity_instance.lean
✓nonCommutativity_instance
lean/Ordinal/MahloClosure.lean
⚠club_filter_intersection_nonempty
⚠crystal_saturation_lifts_to_transfinite
⚠g6_unconditional_closure
✓omega_omega_is_limit
lean/Symmetry/D6.lean
✓P6_identity
⚠d6_lockin
⚠orthogonalStepping_preserved
lean/discreteDm3.lean
✓collatz_converges
lean/dm3_euler_preservation.lean
⚠dm3_euler_preservation
lean/dm3_volume_invariant.lean
⚠dm3_volume_invariant
lean/f35/Dm3Arithmetic.lean
✓flowAux_ode
✓flow_equilibrium_at_one
⚠flow_ode
⚠flow_zero
✓r_star_lt_one
✓r_star_mem_Ioo
✓r_star_pos
✓z₀_neg
lean/finite_v1.lean
✓finite_kakeya_thickened_positive_measure
✓finite_segments_measure_zero
✓segment_measure_zero
✓thickened_segment_pos_measure
lean/fitribonacci.lean
⚠dm3_lockin
✓net_height_decrease
✓no_alternative_cycle
✓no_escape_to_infinity
✓valTwo_after_K
lean/gronwall_contraction_below_stability_radius.lean
✓gronwall_contraction_below_stability_radius
lean/gtct_t1.lean
⚠gtct_t1
lean/lean/Crystal/G6.lean
⚠crystal_lockin
✓crystal_order_six
✓weight_positive
lean/main_v7.lean
✓closurePoints_stationary
✓closurePoints_unbounded
⚠dm3_euler_preservation
⚠dm3_volume_invariant
⚠g6_lattice_invariant
⚠g6_symmetry_preservation
⚠gronwall_contraction_below_stability_radius
⚠gtct_t1
✓nextLevel_layer_count_gt
✓noiseTolerance
⚠regeneration_loop_invariant
⚠separation_theorem
✓stabilityRadius_eq
✓sup_lt_of_regular
✓sup_strictMono_isLimit
lean/regeneration_loop_invariant.lean
⚠regeneration_loop_invariant
lean/separation_theorem.lean
⚠separation_theorem