Body-Pin Rigidity

Blueprint Summary🔗

Overview
Total entries62completed: 57; deps incomplete: 0; sorries: 0; no proof: 4
Ready now0Entries whose next formalization step is currently unblocked.
Fully closed57Local code and prerequisite closure are both complete.
Actionable priorities1Entries ready now and already unlocking downstream work.
Missing informal coverage19Entries with Lean code but missing an informal statement or proof block.
Ready next (1)
  • direction_complex(Definition)
    Ready for statement work.
    tag: informal-onlystage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
Missing informal coverage (19)
Entry index (62)
Definitions20completed: 19; deps incomplete: 0; sorries: 0; no proof: 0
Lemmas31completed: 31; deps incomplete: 0; sorries: 0; no proof: 0
Theorems10completed: 7; deps incomplete: 0; sorries: 0; no proof: 3
Corollaries1completed: 0; deps incomplete: 0; sorries: 0; no proof: 1
Informal-only entries5
Definition Index (20)
Theorem / Lemma / Corollary Index (42)
By parent groups (11)
The Euclidean statements the formalization proves in place of that citation: local rigidity on an open dense set of placements, rigidity against continuous motions, and the vocabulary both are stated in. (3)
Twists, the pin compatibility equation, and the counting argument. (3)
Combinatorics with no paper counterpart. (2)
The paper's algebraic argument: the form, the ideal, the shear, the dimension formula, and the height theorem. (4)
What Section 4 claims, and which part of it the formalization uses. (2)
The passage from a maximum-rank graph placement to a rigid twist system. (2)
The direction matrix over a coefficient field, the exact sequence, the ledger, and the local classification at a low-degree vertex. (4)
The theorem itself, in both of the paper's formulations, together with the one literature citation standing between them. (3)
The paper's sparsity vocabulary: the counting condition, tight sets, and the two facts about them that the vertex-deletion induction uses. (3)
The paper's flag vocabulary and the results of Section 3: definitions, overlap counting, selection, pivot, classification, augmentation, and the stress–codimension theorem. (8)
The paper's assembly argument: the partition, the selection lemma, the orbit drop, the properness of the exceptional locus, and the final assembly. (4)
Dependency insights
Statement-used entries35Entries reused in statement dependencies.
Proof-used entries29Entries reused in proof-only dependencies.
Tracked parent groups12Grouped health rollups for parents with more than one child entry.
Most used in statements (35)
Most used in proofs (29)
Group health (12)
  • The theorem itself, in both of the paper's formulations, together with the one literature citation standing between them.statement_theorem
    Grouped view over entries sharing the same parent.
    total: 3closed: 1local-only: 0ready: 2blocked: 0incomplete Lean: 0unlock score: 3
    Next: no ready child currently unlocks downstream work.
  • The paper's algebraic argument: the form, the ideal, the shear, the dimension formula, and the height theorem.splitklein_spine
    Grouped view over entries sharing the same parent.
    total: 6closed: 5local-only: 0ready: 1blocked: 0incomplete Lean: 0unlock score: 49
    Next: no ready child currently unlocks downstream work.
  • What Section 4 claims, and which part of it the formalization uses.strata_comparison
    Grouped view over entries sharing the same parent.
    total: 3closed: 1local-only: 0ready: 1blocked: 1incomplete Lean: 0unlock score: 10
    Next: direction_complex stage: statementdownstream unlocks: 1
  • The paper's flag vocabulary and the results of Section 3: definitions, overlap counting, selection, pivot, classification, augmentation, and the stress–codimension theorem.flags_spine
    Grouped view over entries sharing the same parent.
    total: 11closed: 11local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 153
    Next: no ready child currently unlocks downstream work.
  • The direction matrix over a coefficient field, the exact sequence, the ledger, and the local classification at a low-degree vertex.deletion_spine
    Grouped view over entries sharing the same parent.
    total: 8closed: 8local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 123
    Next: no ready child currently unlocks downstream work.
  • The paper's sparsity vocabulary: the counting condition, tight sets, and the two facts about them that the vertex-deletion induction uses.sparsity_spine
    Grouped view over entries sharing the same parent.
    total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 73
    Next: no ready child currently unlocks downstream work.
  • The combinatorial data of a body–pin framework, the rigidity operator, and the two sides of the equivalence.statement_data
    Grouped view over entries sharing the same parent.
    total: 6closed: 6local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 62
    Next: no ready child currently unlocks downstream work.
  • Twists, the pin compatibility equation, and the counting argument.necessity_spine
    Grouped view over entries sharing the same parent.
    total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 30
    Next: no ready child currently unlocks downstream work.
  • The paper's assembly argument: the partition, the selection lemma, the orbit drop, the properness of the exceptional locus, and the final assembly.bodypin_spine
    Grouped view over entries sharing the same parent.
    total: 5closed: 5local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 29
    Next: no ready child currently unlocks downstream work.
  • The Euclidean statements the formalization proves in place of that citation: local rigidity on an open dense set of placements, rigidity against continuous motions, and the vocabulary both are stated in.statement_geometric
    Grouped view over entries sharing the same parent.
    total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 8
    Next: no ready child currently unlocks downstream work.
  • Show all 2 more groups
    • Combinatorics with no paper counterpart.sparsity_infrastructure
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 1
      Next: no ready child currently unlocks downstream work.
    • The passage from a maximum-rank graph placement to a rigid twist system.necessity_infrastructure
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
      Next: no ready child currently unlocks downstream work.
Metadata
Tags in use4Distinct tags currently attached to blueprint entries.
Tag rollups (4)
  • tag: informal-only
    entries: 3actionable: 1quick wins: 0linked PRs: 0
  • tag: paper
    entries: 47actionable: 0quick wins: 0linked PRs: 0
  • tag: deviation
    entries: 15actionable: 0quick wins: 0linked PRs: 0
  • tag: lean-only
    entries: 10actionable: 0quick wins: 0linked PRs: 0
Metadata audit
Missing owner62
Missing effort62
Missing owner (62)
Missing effort (62)
Structure and coverage
Informal-only5Statements with no associated Lean code yet.
Fully closed57Local code and ancestor closure are both complete.
Heaviest prerequisites (49)
No prerequisites (13)
No dependents (12)