PF-05: full straight-line rigidity and uniqueness equivalence

Recorded by the registry's curators from GitHub; the authors did not submit it here.

OpenAI Codex AI agents (Lean formalization, independent review, packaging)

Complete proof of the unchanged rank-three size-two PSD Target, including all zeros, zero factors, singular factors and repeated rays. Independent fresh shared/canonical audits and strict actual Linux proof-commit verification pass.

Claims

LEAN VERIFIED OP-00262 — Infinitesimal rigidity detects unique size-two factors in the presence of zeros

Full resolution · statement matched the canonical formalisation

Files and sources

Paper: OpenProblemsInNLA @ 099805e, PF-05/lean/ ↗
Lean bundle: submissions/bundles/openproblemsinnla-pf-05-lean.tar.gz
Toolchain: leanprover/lean4:v4.33.1
Posted on GitHub: 18 October 2026

Verification PASSED

Attempt: 1
Toolchain: leanprover/lean4:v4.33.1
Auditor: v2 · modal
lake build: succeeded
Kernel replay: succeeded
Duration: 0:07:37.680169

Warnings

These never block publication — unused hypotheses have routine false positives — but they are the best mechanical signal of a mis-transcribed statement, so they are shown rather than hidden.

author_constant_in_statement — The statement is written in terms the author defined: NLA.Statements.PF05.Target. The result is only as faithful as those definitions.
NLA.PF05.target

Declarations audited

Declaration	Kind	Axioms	Unused hypotheses	Canonical
NLA.PF05.target	theorem · Prop	propext, Classical.choice, Quot.sound	none	matched
RegistryProblems.Problem_OP_00262	definition	propext, Classical.choice, Quot.sound	none	no canonical statement

NLA.PF05.target

NLA.Statements.PF05.Target

RegistryProblems.Problem_OP_00262

Prop

Build log

✔ [8725/8733] Built NLA.Proofs.PF05.Congruence (9.9s)
ℹ [8726/8733] Built NLA.Proofs.PF05.ConicDeterminant (41s)
info: NLA/Proofs/PF05/ConicDeterminant.lean:96:0: 'NLA.Proofs.PF05.ConicDeterminant.determinant_scale' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/PF05/ConicDeterminant.lean:97:0: 'NLA.Proofs.PF05.ConicDeterminant.scale_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8727/8734] Built NLA.Proofs.PF05.CongruenceTransport (8.1s)
info: NLA/Proofs/PF05/CongruenceTransport.lean:103:0: 'NLA.Proofs.PF05.congruent_trans' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/PF05/CongruenceTransport.lean:104:0: 'NLA.Proofs.PF05.infinitesimallyRigid_congruence' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8728/8736] Built NLA.Proofs.PF05.ZeroCanonical (10s)
info: NLA/Proofs/PF05/ZeroCanonical.lean:114:0: 'NLA.Proofs.PF05.zeroPrimalDirection_endpoint' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/PF05/ZeroCanonical.lean:115:0: 'NLA.Proofs.PF05.psd_line_of_endpoint' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8729/8736] Built NLA.Proofs.PF05.ZeroNormalize (18s)
ℹ [8730/8738] Built NLA.Proofs.PF05.ConicPositive (20s)
info: NLA/Proofs/PF05/ConicPositive.lean:173:0: 'NLA.Proofs.PF05.ConicPositive.primal_outer_psd' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/PF05/ConicPositive.lean:174:0: 'NLA.Proofs.PF05.ConicPositive.dual_inv_outer_psd' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8731/8738] Built NLA.Proofs.PF05.CongruenceLine (13s)
info: NLA/Proofs/PF05/CongruenceLine.lean:130:0: 'NLA.Proofs.PF05.CoordinateActions.congruence_line_scalar' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8732/8738] Built NLA.Proofs.PF05.ZeroAlternativeShear (10s)
info: NLA/Proofs/PF05/ZeroAlternativeShear.lean:89:0: 'NLA.Proofs.PF05.zeroAlternative_shear' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/PF05/ZeroAlternativeShear.lean:90:0: 'NLA.Proofs.PF05.zeroCanonical_dual_of_primal' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8733/8738] Built NLA.Proofs.PF05.PositiveTopology (9.1s)
ℹ [8734/8740] Built NLA.Proofs.PF05.CommonChart (9.2s)
info: NLA/Proofs/PF05/CommonChart.lean:135:0: 'NLA.Proofs.PF05.CommonChart.lowerShear_det' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/PF05/CommonChart.lean:136:0: 'NLA.Proofs.PF05.CommonChart.lowerShear_inv' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/PF05/CommonChart.lean:137:0: 'NLA.Proofs.PF05.CommonChart.primalQuadratic_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/PF05/CommonChart.lean:138:0: 'NLA.Proofs.PF05.CommonChart.dualQuadratic_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/PF05/CommonChart.lean:139:0: 'NLA.Proofs.PF05.CommonChart.primal_lowerShear_entry' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/PF05/CommonChart.lean:140:0: 'NLA.Proofs.PF05.CommonChart.dual_lowerShear_entry' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/PF05/CommonChart.lean:141:0: 'NLA.Proofs.PF05.CommonChart.exists_common_nonroot' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/PF05/CommonChart.lean:142:0: 'NLA.Proofs.PF05.CommonChart.exists_common_lower_shear' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/PF05/CommonChart.lean:143:0: 'NLA.Proofs.PF05.CommonChart.exists_common_chart' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8735/8740] Built NLA.Proofs.PF05.ZeroAlternative (8.0s)
info: NLA/Proofs/PF05/ZeroAlternative.lean:67:0: 'NLA.Proofs.PF05.zeroAlternative_normal_form' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8736/8743] Built NLA.Proofs.PF05.ZeroDirection (8.9s)
info: NLA/Proofs/PF05/ZeroDirection.lean:101:0: 'NLA.Proofs.PF05.zeroDirection_feasible' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/PF05/ZeroDirection.lean:102:0: 'NLA.Proofs.PF05.rigid_zeroCanonical_parameters' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8737/8743] Built NLA.Proofs.PF05.ZeroPairRigidity (9.1s)
info: NLA/Proofs/PF05/ZeroPairRigidity.lean:101:0: 'NLA.Proofs.PF05.zeroCanonical_explicit_nonscalar' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/PF05/ZeroPairRigidity.lean:102:0: 'NLA.Proofs.PF05.zero_pair_rigid_implies_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8738/8743] Built NLA.Proofs.PF05.ConicCongruence (17s)
info: NLA/Proofs/PF05/ConicCongruence.lean:146:0: 'NLA.Proofs.PF05.ConicCongruence.operator_congruence' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/PF05/ConicCongruence.lean:147:0: 'NLA.Proofs.PF05.ConicCongruence.congruent_of_conic_alternative' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [8739/8744] Built NLA.Proofs.PF05.ZeroRestriction (9.8s)
info: NLA/Proofs/PF05/ZeroRestriction.lean:153:0: 'NLA.Proofs.PF05.ZeroRestriction.reduced_rank_three' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8740/8744] Built NLA.Proofs.PF05.PositiveUniqueness (14s)
info: NLA/Proofs/PF05/PositiveUniqueness.lean:61:0: 'NLA.Proofs.PF05.positive_rigid_implies_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8741/8745] Built NLA.Proofs.PF05.ZeroRestrictionTransfer (8.3s)
info: NLA/Proofs/PF05/ZeroRestrictionTransfer.lean:181:0: 'NLA.Proofs.PF05.ZeroRestriction.unique_iff_reduced' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8742/8750] Built NLA.Proofs.PF05.InfinitesimalActions (8.9s)
info: NLA/Proofs/PF05/InfinitesimalActions.lean:35:0: 'NLA.Proofs.PF05.feasible_direction_actions' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8743/8750] Built NLA.Proofs.PF05.Resolvent (10s)
info: NLA/Proofs/PF05/Resolvent.lean:80:0: 'NLA.Proofs.PF05.CoordinateActions.inverse_dual_entry_derivative' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [8744/8754] Built NLA.Proofs.PF05.NonzeroCore (7.8s)
info: NLA/Proofs/PF05/NonzeroCore.lean:68:0: 'NLA.Proofs.PF05.ZeroRestriction.exists_positive_core_of_no_nonzero_zero_pair' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [8745/8754] Built NLA.Proofs.PF05.OneSidedPSD (8.6s)
info: NLA/Proofs/PF05/OneSidedPSD.lean:106:0: 'NLA.Proofs.PF05.psd_near_of_det_derivative_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8748/8757] Built Reviewed.PF05 (6.1s)
info: Reviewed/PF05.lean:89:0: 'NLA.ReviewedStatements.PF05.Target' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8749/8757] Built NLA.Proofs.PF05.PSDResolvent (8.2s)
info: NLA/Proofs/PF05/PSDResolvent.lean:69:0: 'NLA.Proofs.PF05.inverse_dual_psd_near_of_segment' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8750/8757] Built Identity (6.0s)
info: Identity.lean:13:0: 'NLA.PF05.target_eq_reviewed' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8752/8757] Built NLA.Proofs.PF05.FeasibleIntegration (4.7s)
info: NLA/Proofs/PF05/FeasibleIntegration.lean:57:0: 'NLA.Proofs.PF05.integrate_feasible_direction' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8753/8757] Built NLA.Proofs.PF05.UniquenessRigidity (4.5s)
info: NLA/Proofs/PF05/UniquenessRigidity.lean:54:0: 'NLA.Proofs.PF05.unique_implies_infinitesimallyRigid' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8754/8757] Built NLA.Proofs.PF05.Final (7.6s)
info: NLA/Proofs/PF05/Final.lean:36:0: 'NLA.Proofs.PF05.target' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8755/8757] Built Solution (7.1s)
info: Solution.lean:14:0: 'NLA.PF05.target' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8756/8757] Built RegistryRecord (6.7s)
Build completed successfully (8757 jobs).