Rupert Counterexample

Blueprint Summary🔗

Overview
Total entries79completed: 53; deps incomplete: 15; sorries: 1; no proof: 9
Ready now10Entries with an actionable next formalization step.
Fully closed53Local code and prerequisite closure are both complete.
Actionable priorities9Entries ready now and already unlocking downstream work.
Current blockers1Missing external or incomplete Lean declarations.
Missing informal coverage10Entries with Lean code but missing an informal statement or proof block.
Actionable priorities (9)
  • «thm:polyhedron_radius_iff»(Theorem)
    Ready for proof work.
    stage: proofstatement: ready to formalizedirect uses: 2downstream unlocks: 12proof: ready to formalize
  • «lem:leq1»(Lemma)
    Ready for proof work.
    stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 11proof: ready to formalize
  • «lem:n2»(Lemma)
    Ready for proof work.
    stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 11proof: ready to formalize
  • «corr:deltakappa»(Corollary)
    Ready for proof work.
    stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 10proof: ready to formalize
  • «def:pointsymmetrize»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 10
  • «thm:pointsymmetrize_pres_radius»(Theorem)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 10proof: not ready
  • «lem:radius_noperthedron_one»(Lemma)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 9proof: not ready
  • «thm:exists_solution_table»(Theorem)
    Ready for proof work.
    stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 6proof: ready to formalize
  • «lemma:pointsymmetrization_is_pointsym»(Lemma)
    Ready for proof work.
    stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 4proof: ready to formalize
Current blockers (1)
  • «code:c1_c2_c3_norms»(Lemma)
    Declaration with sorry: NopertInline.c3_norm_bound [theorem/lemma; contains sorry; in proof; refs: 1]
Missing informal coverage (10)
Entry index (79)
Definitions9completed: 7; deps incomplete: 1; sorries: 0; no proof: 0
Lemmas45completed: 39; deps incomplete: 1; sorries: 1; no proof: 4
Theorems20completed: 4; deps incomplete: 12; sorries: 0; no proof: 4
Corollaries5completed: 3; deps incomplete: 1; sorries: 0; no proof: 1
Lean-only entries10
Informal-only entries10
Definition Index (9)
Theorem / Proposition / Lemma / Corollary Index (70)
By parent groups (16)
Rational trigonometric approximations. (2)
Radius and norm control for noperthedron vertices. (3)
Soundness of table rows and propagated non-Rupert certificates. (4)
Rotation and norm control inequalities. (2)
Pointsymmetry properties of the construction. (2)
Perturbation bounds for projected points. (4)
Reductions from general poses to certified subcases. (3)
Radius characterization and preservation tools. (2)
Distance and local-maximality sector estimates. (3)
Linear-algebra lemmas for local geometry. (5)
Rupert-tightening reduction lemmas. (2)
Matrix approximation error bounds. (5)
Derivative bounds and approximation control for rotated projections. (3)
Local theorem approximation bounds. (4)
Final non-Rupert conclusions for the noperthedron. (2)
Spanning criteria for projected triples. (1)
Dependency insights
Statement-used entries10Entries reused in statement dependencies.
Proof-used entries58Entries reused in proof-only dependencies.
Tracked parent groups17Grouped health rollups for parents with more than one child entry.
Most used in statements (10)
  • «def:noperthedron»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 9
    Associated lean decls (2)
  • «def:ekspanning»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 11
    Associated lean decls (1)
  • «dfn:sin_cos_approx»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 19
    Associated lean decls (2)
  • «def:eps-spanning»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 13
    Associated lean decls (1)
  • «def:spanp»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 13
    Associated lean decls (1)
  • «thm:polyhedron_radius_iff»(Theorem)
    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)
  • «def:C15»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 10
    Associated lean decls (1)
  • «def:pointsymmetrize»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 10
  • «def:pointsymmetric»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
    Associated lean decls (1)
Most used in proofs (58)
Group health (17)
  • Derivative bounds and approximation control for rotated projections.global_derivative_bounds
    Grouped view over entries sharing the same parent.
    total: 3closed: 1local-only: 0ready: 2blocked: 0incomplete Lean: 0unlock score: 33
    Next: «lem:leq1» stage: proofdownstream unlocks: 11
  • Radius characterization and preservation tools.prelims_radius_tools
    Grouped view over entries sharing the same parent.
    total: 2closed: 0local-only: 0ready: 2blocked: 0incomplete Lean: 0unlock score: 22
    Next: «thm:polyhedron_radius_iff» stage: proofdownstream unlocks: 12
  • Local theorem approximation bounds.rational_local_approx
    Grouped view over entries sharing the same parent.
    total: 5closed: 4local-only: 0ready: 1blocked: 0incomplete Lean: 0unlock score: 52
    Next: «corr:deltakappa» stage: proofdownstream unlocks: 10
  • Noperthedron construction and core definitions.nopert_construction
    Grouped view over entries sharing the same parent.
    total: 4closed: 2local-only: 1ready: 1blocked: 0incomplete Lean: 0unlock score: 33
    Next: «def:pointsymmetrize» stage: statementdownstream unlocks: 10
  • Radius and norm control for noperthedron vertices.nopert_radius
    Grouped view over entries sharing the same parent.
    total: 3closed: 2local-only: 0ready: 1blocked: 0incomplete Lean: 0unlock score: 29
    Next: «lem:radius_noperthedron_one» stage: statementdownstream unlocks: 9
  • Pointsymmetry properties of the construction.nopert_pointsymmetry
    Grouped view over entries sharing the same parent.
    total: 2closed: 0local-only: 1ready: 1blocked: 0incomplete Lean: 0unlock score: 7
    Next: «lemma:pointsymmetrization_is_pointsym» stage: proofdownstream unlocks: 4
  • 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: 74
    Next: no ready child currently unlocks downstream work.
  • 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.
  • Rational trigonometric approximations.rational_trig_approx
    Grouped view over entries sharing the same parent.
    total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 54
    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: 52
    Next: no ready child currently unlocks downstream work.
  • Show all 7 more groups
    • 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.
    • 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.
    • 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: 16
      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 owner75
Missing effort75
Untagged75
Missing owner (75)
Missing effort (75)
Untagged (75)
Structure and coverage
Informal-only10Statements with no associated Lean code yet.
Ready to formalize10Entries with an actionable next formalization step.
Formalized, ancestors open15Local Lean work is done, but prerequisite closure is still open.
Fully closed53Local code and ancestor closure are both complete.
Blocked or incomplete1Entries not covered by the highlighted readiness buckets above.
Heaviest prerequisites (37)
No prerequisites (42)
No dependents (12)