Lean / HoTT Export Plan
Purpose
This plan identifies which claims can be moved toward formal proof assistants.
Export Classes & Status
| Class | Meaning | Realized State |
|---|---|---|
| Lean Definition | definitional object | 41 Formal Lean 4 Definitions (Compiler-Closed) |
| Lean Machine Proof | theorem declaration proven without sorry | 35 Machine-Verified Lean 4 Theorem Declarations |
| HoTT / Type Theory Target | identity/type/equivalence structure | Active Research Target |
| Simulation Target | numerical lattice surrogate | Simulation Atlas Solvers ( |
| Review-Only | conceptual or historical relation | SFR Review Portal & Public Dossier |
Realized Lean 4 Proof Modules (Fabrica.*)
Across the 11 canonical Lean modules, the current formal theorem set comprises 35 machine-verified theorem declarations (0 sorry, 0 admit, 0 quarantined source axioms):
| Module | Carrier Object | Key Verified Theorems | Lean Status |
|---|---|---|---|
Fabrica.KPField | Non-Local Krauss–Pasev Operators | thm_kp_kernel_symmetry, thm_kp_generator_symmetry, thm_kp_resolvent_bound, thm_kp_deficiency_indices_nullity, thm_kp_cayley_transform_unitary, thm_kp_selfadjoint_domain_closure | CURRENT LEAN THEOREM SET: 6/6 MACHINE-VERIFIED |
Fabrica.InvariantEngineering | Morphisms & Lawful Evolution | thm_invariant_identity, thm_invariant_composition, thm_invariant_invertible | CURRENT LEAN THEOREM SET: 3/3 MACHINE-VERIFIED |
Fabrica.ObserverKnot | Observer Projectors | thm_obs_idempotent_composition, thm_obs_identity_projector, thm_obs_product_absorption | CURRENT LEAN THEOREM SET: 3/3 MACHINE-VERIFIED |
Fabrica.TraceReciprocity | Trace Pairings | thm_trace_involution, thm_trace_dual_symmetry, thm_trace_dual_reflexive | CURRENT LEAN THEOREM SET: 3/3 MACHINE-VERIFIED |
Fabrica.FFE | Constrained Variational Euler-Lagrange | thm_ffe_variational_stationarity, thm_finite_ffe_kkt_zero_nullity, thm_ffe_homogeneous_triviality, thm_ffe_multiplier_superposition | CURRENT LEAN THEOREM SET: 4/4 MACHINE-VERIFIED |
Fabrica.FQFT | Resolvent & Operator Identities | thm_resolvent_two_sided_inverse, thm_first_resolvent_identity_algebraic, thm_shifted_operator_difference, thm_first_resolvent_identity_exact | CURRENT LEAN THEOREM SET: 4/4 MACHINE-VERIFIED |
Fabrica.PGP | Gauge Groupoid Actions | thm_pgp_gauge_identity, thm_pgp_gauge_composition, thm_pgp_gauge_orbit_invariance | CURRENT LEAN THEOREM SET: 3/3 MACHINE-VERIFIED |
Fabrica.ObserverMonad | Epistemic Monads | thm_monad_left_identity, thm_monad_right_identity, thm_monad_associativity | CURRENT LEAN THEOREM SET: 3/3 MACHINE-VERIFIED |
Fabrica.Fabricon | Relational Couplings | thm_fabricon_reflexive_coupling, thm_fabricon_conjugate_involution, thm_fabricon_coupling_symmetry | CURRENT LEAN THEOREM SET: 3/3 MACHINE-VERIFIED |
Fabrica.Realica | Infinite Stabilization | thm_stabilization_fixed_point_idempotence, thm_stabilization_state_convergence, thm_realica_partition_conservation | CURRENT LEAN THEOREM SET: 3/3 MACHINE-VERIFIED |
Fabrica (Root) | Master Soundness Certificate | FabricaDeductiveSoundnessCertificate (Master certificate structure) | FORMAL CORPUS: COMPILER-CLOSED |
See the Lean 4 Formalization Roadmap for complete proof scripts and dependency DAGs.