Proof forgery via mismatched structure projections

Type confusion in Lean FRO Lean 4 before 4.32.2 and in 4.33.0-rc1 allows attackers to forge proofs via in-process metaprograms. The kernel accepts projection expressions whose named structure does not match the projected value's type, and environment::add_inductive in src/kernel/inductive.cpp fails to type-check nested inductive applications replaced by auxiliary types, letting parametric arguments escape checking. Reachability requires running a metaprogram in the Lean process, such as during a build or through a malicious Lake dependency, after which ordinary checked addDecl can register ill-typed declarations and derive False without axioms.