Blueprint Summary🔗

Overview

Total entries71completed: 57; deps incomplete: 11; sorries: 0; no proof: 2

Ready now2Entries with an actionable next formalization step.

Fully closed57Local code and prerequisite closure are both complete.

Actionable priorities2Entries ready now and already unlocking downstream work.

Missing informal coverage12Entries with Lean code but missing an informal statement or proof block.

Actionable priorities (2)

«def:nopertQ»(Definition)

Ready for statement work.

stage: statementstatement: ready to formalizedirect uses: 2downstream unlocks: 12
«thm:exists_solution_table»(Theorem)

Ready for statement work.

stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 6proof: not ready

Missing informal coverage (12)

«code:lem:XPgt0»(Theorem)
Associated lean decls (1)
- bp_XPgt0
«code:lem:sqrt5»(Theorem)
Associated lean decls (1)
- bp_norm_RM_sub_RM_le
«code:lem:RaRa»(Theorem)
Associated lean decls (4)
«thm:solution_global»(Theorem)
Associated lean decls (1)
- Noperthedron.Solution.valid_global_imp_no_rupert
«code:lem:sqrt2»(Theorem)
Associated lean decls (2)
- bp_norm_M_sub_lt
- bp_norm_X_sub_lt
«thm:global_rational»(Theorem)
Associated lean decls (1)
- RationalApprox.GlobalTheorem.rational_global
«code:lem:RxRy»(Theorem)
Associated lean decls (2)
- bp_lemma12
- bp_lemma12_lt_of_ne
«thm:nopertQ_approximate»(Theorem)
Associated lean decls (1)
- Noperthedron.KappaApprox.exact_κApprox_python
«code:lem:MPgtr»(Theorem)
Associated lean decls (1)
- bp_norm_M_apply_gt
«thm:local_rational»(Theorem)
Associated lean decls (1)
- RationalApprox.LocalTheorem.rational_local
«code:lem:RaRalpha»(Theorem)
Associated lean decls (5)
«thm:solution_local»(Theorem)
Associated lean decls (1)
- Noperthedron.Solution.valid_local_imp_no_rupert

Entry index (71)

Definitions8completed: 7; deps incomplete: 0; sorries: 0; no proof: 0

Lemmas33completed: 33; deps incomplete: 0; sorries: 0; no proof: 0

Theorems26completed: 14; deps incomplete: 10; sorries: 0; no proof: 2

Corollaries4completed: 3; deps incomplete: 1; sorries: 0; no proof: 0

Lean-only entries7

Informal-only entries3

Definition Index (8)

«def:eps-spanning»(Definition)
Associated lean decls (1)
- Local.Triangle.Spanning
«def:nopertQ»(Definition)
«def:noperthedron»(Definition)
Associated lean decls (1)
- Noperthedron.exactVertex
«def:ekspanning»(Definition)
Associated lean decls (1)
- Local.Triangle.κSpanning
«def:pointsymmetric»(Definition)
Associated lean decls (1)
- PointSym
«def:LMD»(Definition)
Associated lean decls (1)
- Local.LocallyMaximallyDistant
«def:spanp»(Definition)
Associated lean decls (1)
- Local.Spanp
«dfn:sin_cos_approx»(Definition)
Associated lean decls (2)
- RationalApprox.sinℚ
- RationalApprox.cosℚ

Theorem / Proposition / Lemma / Corollary Index (63)

«thm:pose_of_matrix_pose»(Theorem)
Associated lean decls (2)
- pose_of_matrix_pose
- converted_pose_rupert_iff
«lem:absscalar»(Lemma)
Associated lean decls (1)
- Local.abs_sub_inner_le
«code:lem:XPgt0»(Theorem)
Associated lean decls (1)
- bp_XPgt0
«lem:boundskappa4»(Corollary)
Associated lean decls (1)
- RationalApprox.bounds_kappa4
«code:lem:sqrt5»(Theorem)
Associated lean decls (1)
- bp_norm_RM_sub_RM_le
«lem:congruent»(Lemma)
Associated lean decls (1)
- Local.congruent_iff_sym_matrix_eq
«lem:ekspanningespanning»(Lemma)
Associated lean decls (1)
- RationalApprox.ek_spanning_imp_e_spanning
«lem:dist_le_kappa»(Lemma)
Associated lean decls (1)
- RationalApprox.norm_matrix_actual_approx_le_kappa
«code:lem:RaRa»(Theorem)
Associated lean decls (4)
«thm:solution_global»(Theorem)
Associated lean decls (1)
- Noperthedron.Solution.valid_global_imp_no_rupert
«code:lem:sqrt2»(Theorem)
Associated lean decls (2)
- bp_norm_M_sub_lt
- bp_norm_X_sub_lt
«lemma:nopert_verts_norm_le_one»(Lemma)
Associated lean decls (1)
- Noperthedron.exactVertex_norm_le_one
«thm:row_valid_imp_not_rupert_ix»(Theorem)
Associated lean decls (2)
- Noperthedron.Solution.Row.valid_imp_not_rupert_ix
- Noperthedron.Solution.valid_split_imp_no_rupert
«lem:scalarprodbars»(Lemma)
Associated lean decls (1)
- Local.abs_sub_inner_bars_le
«lem:XPgt0»(Lemma)
Associated lean decls (1)
- Bounding.XPgt0
«lem:langles»(Lemma)
Associated lean decls (1)
- Local.langles
«thm:row_valid_imp_not_rupert»(Corollary)
Associated lean decls (1)
- Noperthedron.Solution.Row.valid_imp_not_rupert
«lem:pythagoras»(Lemma)
Associated lean decls (1)
- Local.pythagoras
«lem:symmetries»(Lemma)
Associated lean decls (3)
«cor:rupert_tightening»(Corollary)
Associated lean decls (1)
- Noperthedron.Tightening.rupert_tightening
«thm:global_rational»(Theorem)
Associated lean decls (1)
- RationalApprox.GlobalTheorem.rational_global
c1_c2_c3_norms(Lemma)
Associated lean decls (3)
«thm:rupert_iff_rupert_set»(Theorem)
Associated lean decls (1)
- rupert_iff_rupert_set
«lem:LMD»(Lemma)
Associated lean decls (1)
- Local.inner_ge_implies_LMD
«code:lem:RxRy»(Theorem)
Associated lean decls (2)
- bp_lemma12
- bp_lemma12_lt_of_ne
«lem:kappa7»(Lemma)
Associated lean decls (2)
- RationalApprox.sinℚ_approx'
- RationalApprox.cosℚ_approx'
«corr:kappa1kappa»(Corollary)
Associated lean decls (17)
«thm:nopert_not_rupert_set»(Theorem)
Associated lean decls (1)
- Noperthedron.nopert_not_rupert_set
«lem:origintriangle»(Lemma)
Associated lean decls (1)
- Local.origin_in_triangle
«lem:n2»(Lemma)
Associated lean decls (1)
- GlobalTheorem.bounded_partials_control_difference2
«thm:no_nopert_matrix_pose»(Theorem)
Associated lean decls (1)
- Noperthedron.no_nopert_matrix_pose
«lem:RxRy»(Lemma)
Associated lean decls (2)
- Bounding.lemma12
- Bounding.lemma12_lt_of_ne
«lem:coss»(Lemma)
Associated lean decls (1)
- Local.coss
«thm:exists_solution_table»(Theorem)
«thm:no_nopert_rot_pose»(Theorem)
Associated lean decls (1)
- Noperthedron.no_nopert_rot_pose
«lem:hullscalarprod»(Lemma)
Associated lean decls (1)
- GlobalTheorem.hull_scalar_prod
«lem:leq1»(Lemma)
Associated lean decls (1)
- GlobalTheorem.rotation_third_partials_bounded
«thm:nopertQ_approximate»(Theorem)
Associated lean decls (1)
- Noperthedron.KappaApprox.exact_κApprox_python
«lem:sqrt5»(Lemma)
Associated lean decls (1)
- Bounding.norm_RM_sub_RM_le
«lem:sin27cos26»(Lemma)
Associated lean decls (2)
- RationalApprox.sinℚ_approx
- RationalApprox.cosℚ_approx
«lem:MPgtr»(Lemma)
Associated lean decls (1)
- Bounding.norm_M_apply_gt
«lem:RaRa»(Lemma)
Associated lean decls (4)
«thm:local»(Theorem)
Associated lean decls (1)
- Local.local_theorem
«thm:rupert_implies_rot_rupert»(Theorem)
Associated lean decls (1)
- rupert_implies_rot_rupert
«thm:polyhedron_radius_def»(Theorem)
«lem:inCirc»(Lemma)
Associated lean decls (1)
- Local.inCirc
«thm:global»(Theorem)
Associated lean decls (1)
- GlobalTheorem.global_theorem
«lem:sqrt2»(Lemma)
Associated lean decls (2)
- Bounding.norm_M_sub_lt
- Bounding.norm_X_sub_lt
«code:lem:MPgtr»(Theorem)
Associated lean decls (1)
- bp_norm_M_apply_gt
«thm:nopert_not_rupert»(Theorem)
Associated lean decls (1)
- Noperthedron.nopert_not_rupert
«thm:local_rational»(Theorem)
Associated lean decls (1)
- RationalApprox.LocalTheorem.rational_local
«lem:rotation_derivatives»(Lemma)
Associated lean decls (7)
«lem:boundskappa3»(Lemma)
Associated lean decls (1)
- RationalApprox.bounds_kappa3_X
«code:lem:RaRalpha»(Theorem)
Associated lean decls (5)
«thm:no_nopert_tight_pose»(Theorem)
Associated lean decls (1)
- Noperthedron.no_nopert_tight_pose
«lem:eps-spanning»(Lemma)
Associated lean decls (1)
- Local.vecX_spanning
«lem:A_le_deltamn»(Lemma)
Associated lean decls (1)
- RationalApprox.norm_le_delta_sqrt_dims
«lemma:nopert_point_symmetric»(Lemma)
Associated lean decls (1)
- Noperthedron.exactPoly_point_symmetric
«thm:no_nopert_pose»(Theorem)
Associated lean decls (1)
- Noperthedron.no_nopert_pose
«lem:RaRalpha»(Lemma)
Associated lean decls (8)
«lem:boundskappa»(Lemma)
Associated lean decls (15)
«thm:solution_local»(Theorem)
Associated lean decls (1)
- Noperthedron.Solution.valid_local_imp_no_rupert
«lem:A1AnB1Bn»(Lemma)
Associated lean decls (1)
- RationalApprox.norm_sub_le_prod

By parent groups (15)

Rational trigonometric approximations. (2)

«lem:sin27cos26»(Lemma)
Associated lean decls (2)
- RationalApprox.sinℚ_approx
- RationalApprox.cosℚ_approx
«lem:kappa7»(Lemma)
Associated lean decls (2)
- RationalApprox.sinℚ_approx'
- RationalApprox.cosℚ_approx'

Radius and norm control for noperthedron vertices. (2)

c1_c2_c3_norms(Lemma)
Associated lean decls (3)
«lemma:nopert_verts_norm_le_one»(Lemma)
Associated lean decls (1)
- Noperthedron.exactVertex_norm_le_one

Soundness of table rows and propagated non-Rupert certificates. (4)

«thm:solution_local»(Theorem)
Associated lean decls (1)
- Noperthedron.Solution.valid_local_imp_no_rupert
«thm:row_valid_imp_not_rupert»(Corollary)
Associated lean decls (1)
- Noperthedron.Solution.Row.valid_imp_not_rupert
«thm:row_valid_imp_not_rupert_ix»(Theorem)
Associated lean decls (2)
- Noperthedron.Solution.Row.valid_imp_not_rupert_ix
- Noperthedron.Solution.valid_split_imp_no_rupert
«thm:solution_global»(Theorem)
Associated lean decls (1)
- Noperthedron.Solution.valid_global_imp_no_rupert

Rotation and norm control inequalities. (2)

«lem:RaRalpha»(Lemma)
Associated lean decls (8)
«lem:RaRa»(Lemma)
Associated lean decls (4)

Perturbation bounds for projected points. (4)

«lem:sqrt2»(Lemma)
Associated lean decls (2)
- Bounding.norm_M_sub_lt
- Bounding.norm_X_sub_lt
«lem:MPgtr»(Lemma)
Associated lean decls (1)
- Bounding.norm_M_apply_gt
«lem:sqrt5»(Lemma)
Associated lean decls (1)
- Bounding.norm_RM_sub_RM_le
«lem:XPgt0»(Lemma)
Associated lean decls (1)
- Bounding.XPgt0

Reductions from general poses to certified subcases. (3)

«thm:no_nopert_pose»(Theorem)
Associated lean decls (1)
- Noperthedron.no_nopert_pose
«thm:no_nopert_rot_pose»(Theorem)
Associated lean decls (1)
- Noperthedron.no_nopert_rot_pose
«thm:no_nopert_matrix_pose»(Theorem)
Associated lean decls (1)
- Noperthedron.no_nopert_matrix_pose

Distance and local-maximality sector estimates. (3)

«lem:inCirc»(Lemma)
Associated lean decls (1)
- Local.inCirc
«lem:coss»(Lemma)
Associated lean decls (1)
- Local.coss
«lem:LMD»(Lemma)
Associated lean decls (1)
- Local.inner_ge_implies_LMD

Linear-algebra lemmas for local geometry. (5)

«lem:origintriangle»(Lemma)
Associated lean decls (1)
- Local.origin_in_triangle
«lem:pythagoras»(Lemma)
Associated lean decls (1)
- Local.pythagoras
«lem:langles»(Lemma)
Associated lean decls (1)
- Local.langles
«lem:scalarprodbars»(Lemma)
Associated lean decls (1)
- Local.abs_sub_inner_bars_le
«lem:absscalar»(Lemma)
Associated lean decls (1)
- Local.abs_sub_inner_le

Rupert-tightening reduction lemmas. (2)

«cor:rupert_tightening»(Corollary)
Associated lean decls (1)
- Noperthedron.Tightening.rupert_tightening
«lem:symmetries»(Lemma)
Associated lean decls (3)

Matrix approximation error bounds. (5)

«lem:A1AnB1Bn»(Lemma)
Associated lean decls (1)
- RationalApprox.norm_sub_le_prod
«lem:boundskappa»(Lemma)
Associated lean decls (15)
«lem:A_le_deltamn»(Lemma)
Associated lean decls (1)
- RationalApprox.norm_le_delta_sqrt_dims
«corr:kappa1kappa»(Corollary)
Associated lean decls (17)
«lem:dist_le_kappa»(Lemma)
Associated lean decls (1)
- RationalApprox.norm_matrix_actual_approx_le_kappa

Derivative bounds and approximation control for rotated projections. (3)

«lem:rotation_derivatives»(Lemma)
Associated lean decls (7)
«lem:leq1»(Lemma)
Associated lean decls (1)
- GlobalTheorem.rotation_third_partials_bounded
«lem:n2»(Lemma)
Associated lean decls (1)
- GlobalTheorem.bounded_partials_control_difference2

Certified rational approximations of the noperthedron vertices. (1)

«thm:nopertQ_approximate»(Theorem)
Associated lean decls (1)
- Noperthedron.KappaApprox.exact_κApprox_python

Local theorem approximation bounds. (3)

«lem:boundskappa3»(Lemma)
Associated lean decls (1)
- RationalApprox.bounds_kappa3_X
«lem:ekspanningespanning»(Lemma)
Associated lean decls (1)
- RationalApprox.ek_spanning_imp_e_spanning
«lem:boundskappa4»(Corollary)
Associated lean decls (1)
- RationalApprox.bounds_kappa4

Final non-Rupert conclusions for the noperthedron. (2)

«thm:nopert_not_rupert»(Theorem)
Associated lean decls (1)
- Noperthedron.nopert_not_rupert
«thm:nopert_not_rupert_set»(Theorem)
Associated lean decls (1)
- Noperthedron.nopert_not_rupert_set

Spanning criteria for projected triples. (1)

«lem:eps-spanning»(Lemma)
Associated lean decls (1)
- Local.vecX_spanning

Dependency insights

Statement-used entries8Entries reused in statement dependencies.

Proof-used entries54Entries reused in proof-only dependencies.

Tracked parent groups16Grouped health rollups for parents with more than one child entry.

Most used in statements (8)

«def:noperthedron»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 9
Associated lean decls (1)
- Noperthedron.exactVertex
«def:ekspanning»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 11
Associated lean decls (1)
- Local.Triangle.κSpanning
«dfn:sin_cos_approx»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 18
Associated lean decls (2)
- RationalApprox.sinℚ
- RationalApprox.cosℚ
«def:eps-spanning»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 13
Associated lean decls (1)
- Local.Triangle.Spanning
«def:spanp»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 13
Associated lean decls (1)
- Local.Spanp
«def:nopertQ»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 12
«def:LMD»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 12
Associated lean decls (1)
- Local.LocallyMaximallyDistant
«def:pointsymmetric»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
Associated lean decls (1)
- PointSym

Most used in proofs (54)

«lem:sqrt2»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 5statement uses: 0direct uses: 5downstream unlocks: 17
Associated lean decls (2)
- Bounding.norm_M_sub_lt
- Bounding.norm_X_sub_lt
«lem:A1AnB1Bn»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 16
Associated lean decls (1)
- RationalApprox.norm_sub_le_prod
«lem:RxRy»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 19
Associated lean decls (2)
- Bounding.lemma12
- Bounding.lemma12_lt_of_ne
«corr:kappa1kappa»(Corollary)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 14
Associated lean decls (17)
«lem:eps-spanning»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 12
Associated lean decls (1)
- Local.vecX_spanning
«lem:boundskappa3»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 11
Associated lean decls (1)
- RationalApprox.bounds_kappa3_X
«thm:nopertQ_approximate»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 10
Associated lean decls (1)
- Noperthedron.KappaApprox.exact_κApprox_python
«lem:sin27cos26»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 17
Associated lean decls (2)
- RationalApprox.sinℚ_approx
- RationalApprox.cosℚ_approx
«lem:A_le_deltamn»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 16
Associated lean decls (1)
- RationalApprox.norm_le_delta_sqrt_dims
«lem:kappa7»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 16
Associated lean decls (2)
- RationalApprox.sinℚ_approx'
- RationalApprox.cosℚ_approx'
Show all 44 more proof-used entries
- «lem:RaRalpha»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 15
  Associated lean decls (8)
- «lem:dist_le_kappa»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 15
  Associated lean decls (1)
  - RationalApprox.norm_matrix_actual_approx_le_kappa
- «lem:origintriangle»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 13
  Associated lean decls (1)
  - Local.origin_in_triangle
- «lem:scalarprodbars»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 13
  Associated lean decls (1)
  - Local.abs_sub_inner_bars_le
- «def:nopertQ»(Definition)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 12
- «lem:absscalar»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 12
  Associated lean decls (1)
  - Local.abs_sub_inner_le
- «lem:sqrt5»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 12
  Associated lean decls (1)
  - Bounding.norm_RM_sub_RM_le
- «lem:LMD»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
  Associated lean decls (1)
  - Local.inner_ge_implies_LMD
- «lem:MPgtr»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
  Associated lean decls (1)
  - Bounding.norm_M_apply_gt
- «lem:XPgt0»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
  Associated lean decls (1)
  - Bounding.XPgt0
- «lem:coss»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
  Associated lean decls (1)
  - Local.coss
- «lem:hullscalarprod»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
  Associated lean decls (1)
  - GlobalTheorem.hull_scalar_prod
- «lem:inCirc»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
  Associated lean decls (1)
  - Local.inCirc
- «lem:langles»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
  Associated lean decls (1)
  - Local.langles
- «lem:leq1»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
  Associated lean decls (1)
  - GlobalTheorem.rotation_third_partials_bounded
- «lem:n2»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
  Associated lean decls (1)
  - GlobalTheorem.bounded_partials_control_difference2
- «lem:pythagoras»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
  Associated lean decls (1)
  - Local.pythagoras
- «lem:rotation_derivatives»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
  Associated lean decls (7)
- «lem:boundskappa4»(Corollary)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
  Associated lean decls (1)
  - RationalApprox.bounds_kappa4
- «lem:boundskappa»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
  Associated lean decls (15)
- «lem:ekspanningespanning»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
  Associated lean decls (1)
  - RationalApprox.ek_spanning_imp_e_spanning
- «thm:global»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
  Associated lean decls (1)
  - GlobalTheorem.global_theorem
- «thm:local»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
  Associated lean decls (1)
  - Local.local_theorem
- c1_c2_c3_norms(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (3)
- «lem:congruent»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (1)
  - Local.congruent_iff_sym_matrix_eq
- «lemma:nopert_verts_norm_le_one»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (1)
  - Noperthedron.exactVertex_norm_le_one
- «thm:global_rational»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (1)
  - RationalApprox.GlobalTheorem.rational_global
- «thm:local_rational»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (1)
  - RationalApprox.LocalTheorem.rational_local
- «thm:solution_global»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 8
  Associated lean decls (1)
  - Noperthedron.Solution.valid_global_imp_no_rupert
- «thm:solution_local»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 8
  Associated lean decls (1)
  - Noperthedron.Solution.valid_local_imp_no_rupert
- «thm:row_valid_imp_not_rupert_ix»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 7
  Associated lean decls (2)
  - Noperthedron.Solution.Row.valid_imp_not_rupert_ix
  - Noperthedron.Solution.valid_split_imp_no_rupert
- «lem:symmetries»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (3)
- «thm:exists_solution_table»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 6
- «thm:row_valid_imp_not_rupert»(Corollary)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (1)
  - Noperthedron.Solution.Row.valid_imp_not_rupert
- «cor:rupert_tightening»(Corollary)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (1)
  - Noperthedron.Tightening.rupert_tightening
- «thm:no_nopert_tight_pose»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (1)
  - Noperthedron.no_nopert_tight_pose
- «thm:no_nopert_pose»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (1)
  - Noperthedron.no_nopert_pose
- «thm:pose_of_matrix_pose»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (2)
  - pose_of_matrix_pose
  - converted_pose_rupert_iff
- «lemma:nopert_point_symmetric»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - Noperthedron.exactPoly_point_symmetric
- «thm:no_nopert_rot_pose»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - Noperthedron.no_nopert_rot_pose
- «thm:rupert_implies_rot_rupert»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - rupert_implies_rot_rupert
- «thm:no_nopert_matrix_pose»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - Noperthedron.no_nopert_matrix_pose
- «thm:nopert_not_rupert_set»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - Noperthedron.nopert_not_rupert_set
- «thm:rupert_iff_rupert_set»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - rupert_iff_rupert_set

Group health (16)

Certified rational approximations of the noperthedron vertices.computational_rational_vertices

Grouped view over entries sharing the same parent.

total: 2closed: 0local-only: 1ready: 1blocked: 0incomplete Lean: 0unlock score: 22

Next: «def:nopertQ» stage: statementdownstream unlocks: 12
Linear-algebra lemmas for local geometry.local_linear_algebra

Grouped view over entries sharing the same parent.

total: 6closed: 6local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 73

Next: no ready child currently unlocks downstream work.
Matrix approximation error bounds.rational_matrix_error

Grouped view over entries sharing the same parent.

total: 5closed: 5local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 71

Next: no ready child currently unlocks downstream work.
Perturbation bounds for projected points.bounding_perturbation

Grouped view over entries sharing the same parent.

total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 51

Next: no ready child currently unlocks downstream work.
Rational trigonometric approximations.rational_trig_approx

Grouped view over entries sharing the same parent.

total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 51

Next: no ready child currently unlocks downstream work.
Distance and local-maximality sector estimates.local_distance_sector

Grouped view over entries sharing the same parent.

total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 45

Next: no ready child currently unlocks downstream work.
Local theorem approximation bounds.rational_local_approx

Grouped view over entries sharing the same parent.

total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 42

Next: no ready child currently unlocks downstream work.
Derivative bounds and approximation control for rotated projections.global_derivative_bounds

Grouped view over entries sharing the same parent.

total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 33

Next: no ready child currently unlocks downstream work.
Soundness of table rows and propagated non-Rupert certificates.computational_table_soundness

Grouped view over entries sharing the same parent.

total: 4closed: 0local-only: 4ready: 0blocked: 0incomplete Lean: 0unlock score: 29

Next: no ready child currently unlocks downstream work.
Spanning criteria for projected triples.local_spanning

Grouped view over entries sharing the same parent.

total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 25

Next: no ready child currently unlocks downstream work.
Show all 6 more groups
- Radius and norm control for noperthedron vertices.nopert_radius
  
  Grouped view over entries sharing the same parent.
  
  total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 18
  
  Next: no ready child currently unlocks downstream work.
- Rotation and norm control inequalities.bounding_rotation_norms
  
  Grouped view over entries sharing the same parent.
  
  total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 15
  
  Next: no ready child currently unlocks downstream work.
- Noperthedron construction and core definitions.nopert_construction
  
  Grouped view over entries sharing the same parent.
  
  total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 13
  
  Next: no ready child currently unlocks downstream work.
- Rupert-tightening reduction lemmas.nopert_rupert_tightening
  
  Grouped view over entries sharing the same parent.
  
  total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 11
  
  Next: no ready child currently unlocks downstream work.
- Reductions from general poses to certified subcases.main_pose_reductions
  
  Grouped view over entries sharing the same parent.
  
  total: 3closed: 0local-only: 3ready: 0blocked: 0incomplete Lean: 0unlock score: 9
  
  Next: no ready child currently unlocks downstream work.
- Final non-Rupert conclusions for the noperthedron.main_final_nonrupert
  
  Grouped view over entries sharing the same parent.
  
  total: 2closed: 0local-only: 2ready: 0blocked: 0incomplete Lean: 0unlock score: 1
  
  Next: no ready child currently unlocks downstream work.

Metadata

Owners in use2Distinct owners referenced by the current blueprint entries.

Tags in use6Distinct tags currently attached to blueprint entries.

Owner rollups (2)

David Renshawdavid

entries: 2actionable: 0quick wins: 0linked PRs: 0
Jason Reedjason

entries: 2actionable: 0quick wins: 0linked PRs: 0

Tag rollups (6)

tag: local

entries: 4actionable: 0quick wins: 0linked PRs: 0
tag: spanning

entries: 2actionable: 0quick wins: 0linked PRs: 0
tag: congruence

entries: 1actionable: 0quick wins: 0linked PRs: 0
tag: main-theorem

entries: 1actionable: 0quick wins: 0linked PRs: 0
tag: proof

entries: 1actionable: 0quick wins: 0linked PRs: 0
tag: setup

entries: 1actionable: 0quick wins: 0linked PRs: 0

Metadata audit

Missing owner67

Missing effort67

Untagged67

Missing owner (67)

c1_c2_c3_norms(Lemma)

Missing owner metadata.
Associated lean decls (3)
«code:lem:MPgtr»(Theorem)

Missing owner metadata.
Associated lean decls (1)
- bp_norm_M_apply_gt
«code:lem:RaRalpha»(Theorem)

Missing owner metadata.
Associated lean decls (5)
«code:lem:RaRa»(Theorem)

Missing owner metadata.
Associated lean decls (4)
«code:lem:RxRy»(Theorem)

Missing owner metadata.
Associated lean decls (2)
- bp_lemma12
- bp_lemma12_lt_of_ne
«code:lem:XPgt0»(Theorem)

Missing owner metadata.
Associated lean decls (1)
- bp_XPgt0
«code:lem:sqrt2»(Theorem)

Missing owner metadata.
Associated lean decls (2)
- bp_norm_M_sub_lt
- bp_norm_X_sub_lt
«code:lem:sqrt5»(Theorem)

Missing owner metadata.
Associated lean decls (1)
- bp_norm_RM_sub_RM_le
«cor:rupert_tightening»(Corollary)

Missing owner metadata.
Associated lean decls (1)
- Noperthedron.Tightening.rupert_tightening
«corr:kappa1kappa»(Corollary)

Missing owner metadata.
Associated lean decls (17)
Show all 57 more entries missing owner
- «def:LMD»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Local.LocallyMaximallyDistant
- «def:ekspanning»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Local.Triangle.κSpanning
- «def:nopertQ»(Definition)
  
  Missing owner metadata.
- «def:noperthedron»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Noperthedron.exactVertex
- «def:pointsymmetric»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - PointSym
- «def:spanp»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Local.Spanp
- «dfn:sin_cos_approx»(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - RationalApprox.sinℚ
  - RationalApprox.cosℚ
- «lem:A1AnB1Bn»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - RationalApprox.norm_sub_le_prod
- «lem:A_le_deltamn»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - RationalApprox.norm_le_delta_sqrt_dims
- «lem:LMD»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Local.inner_ge_implies_LMD
- «lem:MPgtr»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Bounding.norm_M_apply_gt
- «lem:RaRalpha»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (8)
- «lem:RaRa»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (4)
- «lem:RxRy»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - Bounding.lemma12
  - Bounding.lemma12_lt_of_ne
- «lem:XPgt0»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Bounding.XPgt0
- «lem:absscalar»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Local.abs_sub_inner_le
- «lem:boundskappa3»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - RationalApprox.bounds_kappa3_X
- «lem:boundskappa4»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (1)
  - RationalApprox.bounds_kappa4
- «lem:boundskappa»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (15)
- «lem:coss»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Local.coss
- «lem:dist_le_kappa»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - RationalApprox.norm_matrix_actual_approx_le_kappa
- «lem:ekspanningespanning»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - RationalApprox.ek_spanning_imp_e_spanning
- «lem:hullscalarprod»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - GlobalTheorem.hull_scalar_prod
- «lem:inCirc»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Local.inCirc
- «lem:kappa7»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - RationalApprox.sinℚ_approx'
  - RationalApprox.cosℚ_approx'
- «lem:langles»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Local.langles
- «lem:leq1»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - GlobalTheorem.rotation_third_partials_bounded
- «lem:n2»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - GlobalTheorem.bounded_partials_control_difference2
- «lem:origintriangle»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Local.origin_in_triangle
- «lem:pythagoras»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Local.pythagoras
- «lem:rotation_derivatives»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (7)
- «lem:scalarprodbars»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Local.abs_sub_inner_bars_le
- «lem:sin27cos26»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - RationalApprox.sinℚ_approx
  - RationalApprox.cosℚ_approx
- «lem:sqrt2»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - Bounding.norm_M_sub_lt
  - Bounding.norm_X_sub_lt
- «lem:sqrt5»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Bounding.norm_RM_sub_RM_le
- «lem:symmetries»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (3)
- «lemma:nopert_point_symmetric»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Noperthedron.exactPoly_point_symmetric
- «lemma:nopert_verts_norm_le_one»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Noperthedron.exactVertex_norm_le_one
- «thm:exists_solution_table»(Theorem)
  
  Missing owner metadata.
- «thm:global_rational»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - RationalApprox.GlobalTheorem.rational_global
- «thm:global»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - GlobalTheorem.global_theorem
- «thm:local_rational»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - RationalApprox.LocalTheorem.rational_local
- «thm:no_nopert_matrix_pose»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Noperthedron.no_nopert_matrix_pose
- «thm:no_nopert_pose»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Noperthedron.no_nopert_pose
- «thm:no_nopert_rot_pose»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Noperthedron.no_nopert_rot_pose
- «thm:no_nopert_tight_pose»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Noperthedron.no_nopert_tight_pose
- «thm:nopertQ_approximate»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Noperthedron.KappaApprox.exact_κApprox_python
- «thm:nopert_not_rupert_set»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Noperthedron.nopert_not_rupert_set
- «thm:nopert_not_rupert»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Noperthedron.nopert_not_rupert
- «thm:polyhedron_radius_def»(Theorem)
  
  Missing owner metadata.
- «thm:pose_of_matrix_pose»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - pose_of_matrix_pose
  - converted_pose_rupert_iff
- «thm:row_valid_imp_not_rupert_ix»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - Noperthedron.Solution.Row.valid_imp_not_rupert_ix
  - Noperthedron.Solution.valid_split_imp_no_rupert
- «thm:row_valid_imp_not_rupert»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Noperthedron.Solution.Row.valid_imp_not_rupert
- «thm:rupert_iff_rupert_set»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - rupert_iff_rupert_set
- «thm:rupert_implies_rot_rupert»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - rupert_implies_rot_rupert
- «thm:solution_global»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Noperthedron.Solution.valid_global_imp_no_rupert
- «thm:solution_local»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Noperthedron.Solution.valid_local_imp_no_rupert

Missing effort (67)

c1_c2_c3_norms(Lemma)

Missing effort metadata.
Associated lean decls (3)
«code:lem:MPgtr»(Theorem)

Missing effort metadata.
Associated lean decls (1)
- bp_norm_M_apply_gt
«code:lem:RaRalpha»(Theorem)

Missing effort metadata.
Associated lean decls (5)
«code:lem:RaRa»(Theorem)

Missing effort metadata.
Associated lean decls (4)
«code:lem:RxRy»(Theorem)

Missing effort metadata.
Associated lean decls (2)
- bp_lemma12
- bp_lemma12_lt_of_ne
«code:lem:XPgt0»(Theorem)

Missing effort metadata.
Associated lean decls (1)
- bp_XPgt0
«code:lem:sqrt2»(Theorem)

Missing effort metadata.
Associated lean decls (2)
- bp_norm_M_sub_lt
- bp_norm_X_sub_lt
«code:lem:sqrt5»(Theorem)

Missing effort metadata.
Associated lean decls (1)
- bp_norm_RM_sub_RM_le
«cor:rupert_tightening»(Corollary)

Missing effort metadata.
Associated lean decls (1)
- Noperthedron.Tightening.rupert_tightening
«corr:kappa1kappa»(Corollary)

Missing effort metadata.
Associated lean decls (17)
Show all 57 more entries missing effort
- «def:LMD»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Local.LocallyMaximallyDistant
- «def:ekspanning»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Local.Triangle.κSpanning
- «def:nopertQ»(Definition)
  
  Missing effort metadata.
- «def:noperthedron»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Noperthedron.exactVertex
- «def:pointsymmetric»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - PointSym
- «def:spanp»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Local.Spanp
- «dfn:sin_cos_approx»(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - RationalApprox.sinℚ
  - RationalApprox.cosℚ
- «lem:A1AnB1Bn»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - RationalApprox.norm_sub_le_prod
- «lem:A_le_deltamn»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - RationalApprox.norm_le_delta_sqrt_dims
- «lem:LMD»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Local.inner_ge_implies_LMD
- «lem:MPgtr»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Bounding.norm_M_apply_gt
- «lem:RaRalpha»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (8)
- «lem:RaRa»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (4)
- «lem:RxRy»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - Bounding.lemma12
  - Bounding.lemma12_lt_of_ne
- «lem:XPgt0»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Bounding.XPgt0
- «lem:absscalar»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Local.abs_sub_inner_le
- «lem:boundskappa3»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - RationalApprox.bounds_kappa3_X
- «lem:boundskappa4»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (1)
  - RationalApprox.bounds_kappa4
- «lem:boundskappa»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (15)
- «lem:coss»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Local.coss
- «lem:dist_le_kappa»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - RationalApprox.norm_matrix_actual_approx_le_kappa
- «lem:ekspanningespanning»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - RationalApprox.ek_spanning_imp_e_spanning
- «lem:hullscalarprod»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - GlobalTheorem.hull_scalar_prod
- «lem:inCirc»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Local.inCirc
- «lem:kappa7»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - RationalApprox.sinℚ_approx'
  - RationalApprox.cosℚ_approx'
- «lem:langles»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Local.langles
- «lem:leq1»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - GlobalTheorem.rotation_third_partials_bounded
- «lem:n2»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - GlobalTheorem.bounded_partials_control_difference2
- «lem:origintriangle»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Local.origin_in_triangle
- «lem:pythagoras»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Local.pythagoras
- «lem:rotation_derivatives»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (7)
- «lem:scalarprodbars»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Local.abs_sub_inner_bars_le
- «lem:sin27cos26»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - RationalApprox.sinℚ_approx
  - RationalApprox.cosℚ_approx
- «lem:sqrt2»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - Bounding.norm_M_sub_lt
  - Bounding.norm_X_sub_lt
- «lem:sqrt5»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Bounding.norm_RM_sub_RM_le
- «lem:symmetries»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (3)
- «lemma:nopert_point_symmetric»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Noperthedron.exactPoly_point_symmetric
- «lemma:nopert_verts_norm_le_one»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Noperthedron.exactVertex_norm_le_one
- «thm:exists_solution_table»(Theorem)
  
  Missing effort metadata.
- «thm:global_rational»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - RationalApprox.GlobalTheorem.rational_global
- «thm:global»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - GlobalTheorem.global_theorem
- «thm:local_rational»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - RationalApprox.LocalTheorem.rational_local
- «thm:no_nopert_matrix_pose»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Noperthedron.no_nopert_matrix_pose
- «thm:no_nopert_pose»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Noperthedron.no_nopert_pose
- «thm:no_nopert_rot_pose»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Noperthedron.no_nopert_rot_pose
- «thm:no_nopert_tight_pose»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Noperthedron.no_nopert_tight_pose
- «thm:nopertQ_approximate»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Noperthedron.KappaApprox.exact_κApprox_python
- «thm:nopert_not_rupert_set»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Noperthedron.nopert_not_rupert_set
- «thm:nopert_not_rupert»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Noperthedron.nopert_not_rupert
- «thm:polyhedron_radius_def»(Theorem)
  
  Missing effort metadata.
- «thm:pose_of_matrix_pose»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - pose_of_matrix_pose
  - converted_pose_rupert_iff
- «thm:row_valid_imp_not_rupert_ix»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - Noperthedron.Solution.Row.valid_imp_not_rupert_ix
  - Noperthedron.Solution.valid_split_imp_no_rupert
- «thm:row_valid_imp_not_rupert»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Noperthedron.Solution.Row.valid_imp_not_rupert
- «thm:rupert_iff_rupert_set»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - rupert_iff_rupert_set
- «thm:rupert_implies_rot_rupert»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - rupert_implies_rot_rupert
- «thm:solution_global»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Noperthedron.Solution.valid_global_imp_no_rupert
- «thm:solution_local»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Noperthedron.Solution.valid_local_imp_no_rupert

Untagged (67)

c1_c2_c3_norms(Lemma)

Missing tag metadata.
Associated lean decls (3)
«code:lem:MPgtr»(Theorem)

Missing tag metadata.
Associated lean decls (1)
- bp_norm_M_apply_gt
«code:lem:RaRalpha»(Theorem)

Missing tag metadata.
Associated lean decls (5)
«code:lem:RaRa»(Theorem)

Missing tag metadata.
Associated lean decls (4)
«code:lem:RxRy»(Theorem)

Missing tag metadata.
Associated lean decls (2)
- bp_lemma12
- bp_lemma12_lt_of_ne
«code:lem:XPgt0»(Theorem)

Missing tag metadata.
Associated lean decls (1)
- bp_XPgt0
«code:lem:sqrt2»(Theorem)

Missing tag metadata.
Associated lean decls (2)
- bp_norm_M_sub_lt
- bp_norm_X_sub_lt
«code:lem:sqrt5»(Theorem)

Missing tag metadata.
Associated lean decls (1)
- bp_norm_RM_sub_RM_le
«cor:rupert_tightening»(Corollary)

Missing tag metadata.
Associated lean decls (1)
- Noperthedron.Tightening.rupert_tightening
«corr:kappa1kappa»(Corollary)

Missing tag metadata.
Associated lean decls (17)
Show all 57 more untagged entries
- «def:LMD»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Local.LocallyMaximallyDistant
- «def:ekspanning»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Local.Triangle.κSpanning
- «def:nopertQ»(Definition)
  
  Missing tag metadata.
- «def:noperthedron»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Noperthedron.exactVertex
- «def:pointsymmetric»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - PointSym
- «def:spanp»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Local.Spanp
- «dfn:sin_cos_approx»(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - RationalApprox.sinℚ
  - RationalApprox.cosℚ
- «lem:A1AnB1Bn»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - RationalApprox.norm_sub_le_prod
- «lem:A_le_deltamn»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - RationalApprox.norm_le_delta_sqrt_dims
- «lem:LMD»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Local.inner_ge_implies_LMD
- «lem:MPgtr»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Bounding.norm_M_apply_gt
- «lem:RaRalpha»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (8)
- «lem:RaRa»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (4)
- «lem:RxRy»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - Bounding.lemma12
  - Bounding.lemma12_lt_of_ne
- «lem:XPgt0»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Bounding.XPgt0
- «lem:absscalar»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Local.abs_sub_inner_le
- «lem:boundskappa3»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - RationalApprox.bounds_kappa3_X
- «lem:boundskappa4»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (1)
  - RationalApprox.bounds_kappa4
- «lem:boundskappa»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (15)
- «lem:coss»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Local.coss
- «lem:dist_le_kappa»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - RationalApprox.norm_matrix_actual_approx_le_kappa
- «lem:ekspanningespanning»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - RationalApprox.ek_spanning_imp_e_spanning
- «lem:hullscalarprod»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - GlobalTheorem.hull_scalar_prod
- «lem:inCirc»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Local.inCirc
- «lem:kappa7»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - RationalApprox.sinℚ_approx'
  - RationalApprox.cosℚ_approx'
- «lem:langles»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Local.langles
- «lem:leq1»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - GlobalTheorem.rotation_third_partials_bounded
- «lem:n2»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - GlobalTheorem.bounded_partials_control_difference2
- «lem:origintriangle»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Local.origin_in_triangle
- «lem:pythagoras»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Local.pythagoras
- «lem:rotation_derivatives»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (7)
- «lem:scalarprodbars»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Local.abs_sub_inner_bars_le
- «lem:sin27cos26»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - RationalApprox.sinℚ_approx
  - RationalApprox.cosℚ_approx
- «lem:sqrt2»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - Bounding.norm_M_sub_lt
  - Bounding.norm_X_sub_lt
- «lem:sqrt5»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Bounding.norm_RM_sub_RM_le
- «lem:symmetries»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (3)
- «lemma:nopert_point_symmetric»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Noperthedron.exactPoly_point_symmetric
- «lemma:nopert_verts_norm_le_one»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Noperthedron.exactVertex_norm_le_one
- «thm:exists_solution_table»(Theorem)
  
  Missing tag metadata.
- «thm:global_rational»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - RationalApprox.GlobalTheorem.rational_global
- «thm:global»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - GlobalTheorem.global_theorem
- «thm:local_rational»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - RationalApprox.LocalTheorem.rational_local
- «thm:no_nopert_matrix_pose»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Noperthedron.no_nopert_matrix_pose
- «thm:no_nopert_pose»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Noperthedron.no_nopert_pose
- «thm:no_nopert_rot_pose»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Noperthedron.no_nopert_rot_pose
- «thm:no_nopert_tight_pose»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Noperthedron.no_nopert_tight_pose
- «thm:nopertQ_approximate»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Noperthedron.KappaApprox.exact_κApprox_python
- «thm:nopert_not_rupert_set»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Noperthedron.nopert_not_rupert_set
- «thm:nopert_not_rupert»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Noperthedron.nopert_not_rupert
- «thm:polyhedron_radius_def»(Theorem)
  
  Missing tag metadata.
- «thm:pose_of_matrix_pose»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - pose_of_matrix_pose
  - converted_pose_rupert_iff
- «thm:row_valid_imp_not_rupert_ix»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - Noperthedron.Solution.Row.valid_imp_not_rupert_ix
  - Noperthedron.Solution.valid_split_imp_no_rupert
- «thm:row_valid_imp_not_rupert»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Noperthedron.Solution.Row.valid_imp_not_rupert
- «thm:rupert_iff_rupert_set»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - rupert_iff_rupert_set
- «thm:rupert_implies_rot_rupert»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - rupert_implies_rot_rupert
- «thm:solution_global»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Noperthedron.Solution.valid_global_imp_no_rupert
- «thm:solution_local»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Noperthedron.Solution.valid_local_imp_no_rupert

Structure and coverage

Informal-only3Statements with no associated Lean code yet.

Ready to formalize2Entries with an actionable next formalization step.

Formalized, ancestors open11Local Lean work is done, but prerequisite closure is still open.

Fully closed57Local code and ancestor closure are both complete.

Blocked or incomplete1Entries not covered by the highlighted readiness buckets above.

Heaviest prerequisites (35)

«thm:local»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 8statement deps: 0proof deps: 8direct uses: 1downstream unlocks: 10
Associated lean decls (1)
- Local.local_theorem
«thm:solution_local»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 5statement deps: 0proof deps: 5direct uses: 1downstream unlocks: 8
Associated lean decls (1)
- Noperthedron.Solution.valid_local_imp_no_rupert
«thm:local_rational»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 5statement deps: 1proof deps: 4direct uses: 1downstream unlocks: 9
Associated lean decls (1)
- RationalApprox.LocalTheorem.rational_local
«lem:eps-spanning»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 5statement deps: 2proof deps: 3direct uses: 2downstream unlocks: 12
Associated lean decls (1)
- Local.vecX_spanning
«thm:global»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 0proof deps: 4direct uses: 1downstream unlocks: 10
Associated lean decls (1)
- GlobalTheorem.global_theorem
«lem:ekspanningespanning»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 1proof deps: 3direct uses: 1downstream unlocks: 10
Associated lean decls (1)
- RationalApprox.ek_spanning_imp_e_spanning
«thm:no_nopert_matrix_pose»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 0proof deps: 3direct uses: 1downstream unlocks: 2
Associated lean decls (1)
- Noperthedron.no_nopert_matrix_pose
«thm:no_nopert_tight_pose»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 1proof deps: 2direct uses: 1downstream unlocks: 5
Associated lean decls (1)
- Noperthedron.no_nopert_tight_pose
«thm:row_valid_imp_not_rupert_ix»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 1proof deps: 2direct uses: 1downstream unlocks: 7
Associated lean decls (2)
- Noperthedron.Solution.Row.valid_imp_not_rupert_ix
- Noperthedron.Solution.valid_split_imp_no_rupert
«corr:kappa1kappa»(Corollary)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 2statement deps: 0proof deps: 2direct uses: 2downstream unlocks: 14
Associated lean decls (17)
Show all 25 more heaviest-prerequisite entries
- «lem:boundskappa»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 10
  Associated lean decls (15)
- «lem:coss»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 11
  Associated lean decls (1)
  - Local.coss
- «lem:dist_le_kappa»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 15
  Associated lean decls (1)
  - RationalApprox.norm_matrix_actual_approx_le_kappa
- «lem:inCirc»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 11
  Associated lean decls (1)
  - Local.inCirc
- «thm:global_rational»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 9
  Associated lean decls (1)
  - RationalApprox.GlobalTheorem.rational_global
- «thm:no_nopert_pose»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 4
  Associated lean decls (1)
  - Noperthedron.no_nopert_pose
- «thm:no_nopert_rot_pose»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - Noperthedron.no_nopert_rot_pose
- «thm:nopert_not_rupert»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 0proof deps: 2direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - Noperthedron.nopert_not_rupert
- «thm:solution_global»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 8
  Associated lean decls (1)
  - Noperthedron.Solution.valid_global_imp_no_rupert
- «thm:nopert_not_rupert_set»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - Noperthedron.nopert_not_rupert_set
- «thm:row_valid_imp_not_rupert»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 6
  Associated lean decls (1)
  - Noperthedron.Solution.Row.valid_imp_not_rupert
- «lemma:nopert_point_symmetric»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - Noperthedron.exactPoly_point_symmetric
- «cor:rupert_tightening»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 5
  Associated lean decls (1)
  - Noperthedron.Tightening.rupert_tightening
- «lem:MPgtr»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 11
  Associated lean decls (1)
  - Bounding.norm_M_apply_gt
- «lem:XPgt0»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 11
  Associated lean decls (1)
  - Bounding.XPgt0
- «lem:boundskappa3»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 2downstream unlocks: 11
  Associated lean decls (1)
  - RationalApprox.bounds_kappa3_X
- «lem:boundskappa4»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 10
  Associated lean decls (1)
  - RationalApprox.bounds_kappa4
- «lem:kappa7»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 16
  Associated lean decls (2)
  - RationalApprox.sinℚ_approx'
  - RationalApprox.cosℚ_approx'
- «lem:sqrt2»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 5downstream unlocks: 17
  Associated lean decls (2)
  - Bounding.norm_M_sub_lt
  - Bounding.norm_X_sub_lt
- «lem:sqrt5»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 12
  Associated lean decls (1)
  - Bounding.norm_RM_sub_RM_le
- «thm:exists_solution_table»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 6
- «lem:LMD»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 11
  Associated lean decls (1)
  - Local.inner_ge_implies_LMD
- «lem:sin27cos26»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 17
  Associated lean decls (2)
  - RationalApprox.sinℚ_approx
  - RationalApprox.cosℚ_approx
- «thm:nopertQ_approximate»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 10
  Associated lean decls (1)
  - Noperthedron.KappaApprox.exact_κApprox_python
- «thm:polyhedron_radius_def»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0

No prerequisites (36)

«thm:pose_of_matrix_pose»(Theorem)
Associated lean decls (2)
- pose_of_matrix_pose
- converted_pose_rupert_iff
«lem:absscalar»(Lemma)
Associated lean decls (1)
- Local.abs_sub_inner_le
«code:lem:XPgt0»(Theorem)
Associated lean decls (1)
- bp_XPgt0
«code:lem:sqrt2»(Theorem)
Associated lean decls (2)
- bp_norm_M_sub_lt
- bp_norm_X_sub_lt
«lemma:nopert_verts_norm_le_one»(Lemma)
Associated lean decls (1)
- Noperthedron.exactVertex_norm_le_one
«lem:langles»(Lemma)
Associated lean decls (1)
- Local.langles
«code:lem:RxRy»(Theorem)
Associated lean decls (2)
- bp_lemma12
- bp_lemma12_lt_of_ne
«lem:RxRy»(Lemma)
Associated lean decls (2)
- Bounding.lemma12
- Bounding.lemma12_lt_of_ne
«def:pointsymmetric»(Definition)
Associated lean decls (1)
- PointSym
«thm:rupert_implies_rot_rupert»(Theorem)
Associated lean decls (1)
- rupert_implies_rot_rupert
Show all 26 more entries without prerequisites
- «code:lem:MPgtr»(Theorem)
  Associated lean decls (1)
  - bp_norm_M_apply_gt
- «lem:rotation_derivatives»(Lemma)
  Associated lean decls (7)
- «def:LMD»(Definition)
  Associated lean decls (1)
  - Local.LocallyMaximallyDistant
- «lem:A1AnB1Bn»(Lemma)
  Associated lean decls (1)
  - RationalApprox.norm_sub_le_prod
- «dfn:sin_cos_approx»(Definition)
  Associated lean decls (2)
  - RationalApprox.sinℚ
  - RationalApprox.cosℚ
- «lem:RaRalpha»(Lemma)
  Associated lean decls (8)
- «def:spanp»(Definition)
  Associated lean decls (1)
  - Local.Spanp
- «lem:A_le_deltamn»(Lemma)
  Associated lean decls (1)
  - RationalApprox.norm_le_delta_sqrt_dims
- «code:lem:RaRalpha»(Theorem)
  Associated lean decls (5)
- «lem:RaRa»(Lemma)
  Associated lean decls (4)
- «lem:leq1»(Lemma)
  Associated lean decls (1)
  - GlobalTheorem.rotation_third_partials_bounded
- «lem:hullscalarprod»(Lemma)
  Associated lean decls (1)
  - GlobalTheorem.hull_scalar_prod
- «def:ekspanning»(Definition)
  Associated lean decls (1)
  - Local.Triangle.κSpanning
- «lem:n2»(Lemma)
  Associated lean decls (1)
  - GlobalTheorem.bounded_partials_control_difference2
- «lem:origintriangle»(Lemma)
  Associated lean decls (1)
  - Local.origin_in_triangle
- «thm:rupert_iff_rupert_set»(Theorem)
  Associated lean decls (1)
  - rupert_iff_rupert_set
- c1_c2_c3_norms(Lemma)
  Associated lean decls (3)
- «lem:symmetries»(Lemma)
  Associated lean decls (3)
- «lem:pythagoras»(Lemma)
  Associated lean decls (1)
  - Local.pythagoras
- «def:noperthedron»(Definition)
  Associated lean decls (1)
  - Noperthedron.exactVertex
- «lem:scalarprodbars»(Lemma)
  Associated lean decls (1)
  - Local.abs_sub_inner_bars_le
- «def:nopertQ»(Definition)
- «code:lem:RaRa»(Theorem)
  Associated lean decls (4)
- «def:eps-spanning»(Definition)
  Associated lean decls (1)
  - Local.Triangle.Spanning
- «lem:congruent»(Lemma)
  Associated lean decls (1)
  - Local.congruent_iff_sym_matrix_eq
- «code:lem:sqrt5»(Theorem)
  Associated lean decls (1)
  - bp_norm_RM_sub_RM_le

No dependents (10)

«code:lem:XPgt0»(Theorem)
Associated lean decls (1)
- bp_XPgt0
«code:lem:MPgtr»(Theorem)
Associated lean decls (1)
- bp_norm_M_apply_gt
«thm:nopert_not_rupert»(Theorem)
Associated lean decls (1)
- Noperthedron.nopert_not_rupert
«code:lem:RaRalpha»(Theorem)
Associated lean decls (5)
«thm:polyhedron_radius_def»(Theorem)
«lem:RaRa»(Lemma)
Associated lean decls (4)
«code:lem:RxRy»(Theorem)
Associated lean decls (2)
- bp_lemma12
- bp_lemma12_lt_of_ne
«code:lem:sqrt2»(Theorem)
Associated lean decls (2)
- bp_norm_M_sub_lt
- bp_norm_X_sub_lt
«code:lem:RaRa»(Theorem)
Associated lean decls (4)
«code:lem:sqrt5»(Theorem)
Associated lean decls (1)
- bp_norm_RM_sub_RM_le