Open ears with two, three or four interior bodies

The steps of the induction on the general configuration at an open ear a − x 0 − ⋯ − x (k − 1) − b on V₁ with two, three or four interior bodies, whose ends may be adjacent (thm:pencil-x0-open-ear-two, thm:pencil-x0-open-ear-three, thm:pencil-x0-open-ear-four, sec:main-component-short). An ear is given as in MainComponent/Ear.lean. The steps follow the scheme of sec:main-component-cut (MainComponent/Cut.lean), with the ear rank formula (BodyHingeFramework.finrank_span_rigidityRows_ear_eq, lem:block-rank-ear) for the count: a configuration over a main picture of G, at which G[V₁] has its target, has rank at least the target of G once dim(ρ + Λ) ≥ k + 1 + def₃(G[V₁]) − def₃(G), the inequality (⋆) of the section, where ρ is the space of relative screws of a and b in G[V₁] and Λ the span of the joins of the ear.

With two interior bodies, given def₃(G[V₁]) ≤ def₃(G), three independent joins of the ear give (⋆). They are independent at one flat configuration, three joins of the closed hexagon of lem:pencil-chain-span-certificates, whose picture need not be admissible, and the heights 0 lie in every L_G(q): Graph.X0Attains.of_openEar_of_cert (MainComponent/Ear.lean) does the rest, as at five or more interior bodies.

With three or four interior bodies no bound on the deficiencies is assumed. The step also uses G″ = G.splitOff (x 1) (x 0) (x 2) (e 1), G with its second interior body suppressed and the label e 1 of x 0 − x 1 relinked to x 0 − x 2. It has the same G[V₁], an open ear on V₁ with one interior body fewer, and a deficiency at most that of G (Graph.splitOff_deficiency_le_of_eq_left, lem:splitoff-deficiency-reuse). The count is against G″. With W the span of ρ and the joins of the ear of G″, the ear rank formula at G″ bounds dim W below where G[V₁] and G″ have their targets, and (⋆) then asks for no more than min(dim W + 1, 6) (Graph.deficiency_induce_add_le_of_ear, lem:deficiency-ear). Putting x 1 back on a line through the point of x 0 or of x 2 gains the dimension, unless W already contains the star of that point, every line through it (lem:pencil-insertion, lem:pencil-two-stars). So it suffices that a W containing both stars be the whole screw space Λ²K⁴, and then x 1 goes to the point of x 0 (exists_insertion_four, exists_insertion_three, MainComponent/Lines.lean).

At four interior bodies a W containing both stars contains the six joins of the points of x 0, x 2, x 3 and b, which span Λ²K⁴ when the four points are independent (lem:pencil-tetrahedron, the case d = 3 of KT 2011 Lemma 2.1, pp. 651–652); the ear data are asked for the span, which holds at one ear datum (linearIndependent_tetra_witness). At three interior bodies the case split on ρ comes before the ear data. Either every relative screw pairs to zero with every line joining the planes of a and of b, and then W has dimension at most three and cannot contain both stars, which span at least five dimensions (lem:pencil-bilinear, lem:pencil-two-stars); or some c ∈ ρ does not, and the ear data are also asked for ⟨c, y₁ ∧ y₃⟩ ≠ 0, y₁ and y₃ the points of x 0 and x 2, written as the span bound dim(ker⟨c, ·⟩ + K (y₁ ∧ y₃)) ≥ 6 and met at a pair of affine points (exists_klein_liftPlane_affine_ne_zero). Then a W containing both stars contains c, which lies outside them, and is Λ²K⁴.

The configuration is chosen in two stages, the base data and then the ear data (def:pencil-ear-data, MainComponent/EarGen.lean). The base data are fixed first (Graph.exists_earBase_splitOff): a picture off the polynomials of the attainment at G[V₁] and at G″ and off the main-picture polynomial of G, and a height of G″ at which both have their targets, whose restriction to V₁ fixes ρ and the rank of G[V₁] at every ear datum. One space of ear data serves G and G″, and each condition the step asks of them holds off the zero set of a polynomial that is nonzero at one ear datum (lem:pencil-ear-data-picture, lem:pencil-ear-data-open). The ear data are taken twice (Graph.X0Attains.of_openEar_splitOff): for G″, where it has at least its target rank and an admissible picture and x 1 can be put back; then, with x 1 put back, for G, off the zero sets of the span bound so reached and of the main-picture polynomial of G. The span bound asks no nonzero hinge of the ear datum where it holds, unlike the rank bound (exists_mvPolynomial_le_finrank_sup_span_pointJoin, exists_mvPolynomial_le_finrank_ofNormals_bind): the point where x 1 is put back certifies dim(ρ + Λ), not the rank of G, and may be the point of x 0, with a zero join.

Main results

• Graph.X0Attains.of_openEar_two: thm:pencil-x0-open-ear-two, if G satisfies the standing hypotheses, with an open ear on V₁ with two interior bodies, its ends possibly adjacent, and def₃(G[V₁]) ≤ def₃(G), the general configuration of G attains when that of G[V₁] does.
• Graph.X0Attains.of_openEar_four and Graph.X0Attains.of_openEar_three: thm:pencil-x0-open-ear-four and thm:pencil-x0-open-ear-three, the same at four and at three interior bodies, with no bound on the deficiencies, when the general configurations of G[V₁] and of G″ attain.
• splitOff_ear_four and splitOff_ear_three: steps of the two, G″ has the open ear a − x 0 − x 2 − x 3 − b, resp. a − x 0 − x 2 − b, on V₁; induce_splitOff_ear, with the same G[V₁]. A selector of G, relinked at the freed label, records the links of the split-off (PanelHingeFramework.RecordsLinks.update_splitOff).
• Graph.exists_earBase_splitOff and Graph.X0Attains.of_openEar_splitOff: steps of the two, the base data, and the two choices of ear data and the count, given that x 1 can be put back off a polynomial in the ear data.
• linearIndependent_tetra_witness: a step of thm:pencil-x0-open-ear-four, the four independent points at the ear datum where the six joins of the points of x 0, x 2, x 3 and b span Λ²K⁴.

The open ear with two interior bodies (thm:pencil-x0-open-ear-two)

theorem Graph.X0Attains.of_openEar_two {K : Type u_1} [Field K] {α : Type u_2} {β : Type u_3} [Infinite K] [Finite α] [Finite β] {G : Graph α β} (hG : G.IsX0Graph) {V₁ : Set α} {x : Fin 2 → α} {a b : α} {e : Fin 3 → β} (hcover : G.vertexSet = V₁ ∪ Set.range x) (hinj : Function.Injective x) (hxV₁ : ∀ (i : Fin 2), x i ∉ V₁) (ha : a ∈ V₁) (hb : b ∈ V₁) (hab : a ≠ b) (hpath : ∀ (i : Fin 3), G.IsLink (e i) (CombinatorialRigidity.Molecular.pathVertex a x b i.castSucc) (CombinatorialRigidity.Molecular.pathVertex a x b i.succ)) (hsep : ∀ (f : β) (u w : α), G.IsLink f u w → (∀ (i : Fin 3), f ≠ e i) → u ∈ V₁ ∧ w ∈ V₁) (h₁ : X0Attains K G[V₁]) (hdef : G[V₁].deficiency 3 ≤ G.deficiency 3) : X0Attains K G

An open ear with two interior bodies (thm:pencil-x0-open-ear-two). Let G satisfy the standing hypotheses, with an open ear a − x 0 − x 1 − b on V₁ whose ends may be adjacent, and let def₃(G[V₁]) ≤ def₃(G); Graph.deficiency_induce_le_of_ear_of_merge (lem:deficiency-ear-merge) gives it when some partition of V₁ attaining def₃(G[V₁]) puts a and b in one part. If the general configuration of G[V₁] attains, so does that of G.

Proof. Graph.X0Attains.of_openEar_of_cert, with the three joins of the ear. The heights 0 lie in every L_G(q), and at them the joins are independent at one picture (certPicture), which puts the points of a, x 0, x 1 and b at Y₄, Y₅, Y₀ and Y₁, and every other body's at Y₄: three joins of the closed hexagon (linearIndependent_pointJoin_certHexagon). Independence is open in the picture, then in the heights, and the ear rank formula adds at least 5 · 3 + 3 − 6 = 12 to the rank, no less than the growth 12 − def₃(G) + def₃(G[V₁]) of the target.

Suppressing the second interior body

theorem CombinatorialRigidity.Molecular.splitOff_ear_four {α : Type u_2} {β : Type u_3} {G : Graph α β} {V₁ : Set α} {x : Fin 4 → α} {a b : α} {e : Fin 5 → β} (hcover : G.vertexSet = V₁ ∪ Set.range x) (hinj : Function.Injective x) (hxV₁ : ∀ (i : Fin 4), x i ∉ V₁) (ha : a ∈ V₁) (hb : b ∈ V₁) (hab : a ≠ b) (hpath : ∀ (i : Fin 5), G.IsLink (e i) (pathVertex a x b i.castSucc) (pathVertex a x b i.succ)) (hsep : ∀ (f : β) (u w : α), G.IsLink f u w → (∀ (i : Fin 5), f ≠ e i) → u ∈ V₁ ∧ w ∈ V₁) : (G.splitOff (x 1) (x 0) (x 2) (e 1)).vertexSet = V₁ ∪ Set.range ![x 0, x 2, x 3] ∧ Function.Injective ![x 0, x 2, x 3] ∧ (∀ (i : Fin (Nat.succ 0).succ.succ), ![x 0, x 2, x 3] i ∉ V₁) ∧ (∀ (i : Fin 4), (G.splitOff (x 1) (x 0) (x 2) (e 1)).IsLink (![e 0, e 1, e 3, e 4] i) (pathVertex a ![x 0, x 2, x 3] b i.castSucc) (pathVertex a ![x 0, x 2, x 3] b i.succ)) ∧ ∀ (f : β) (u w : α), (G.splitOff (x 1) (x 0) (x 2) (e 1)).IsLink f u w → (∀ (i : Fin (Nat.succ 0).succ.succ.succ), f ≠ ![e 0, e 1, e 3, e 4] i) → u ∈ V₁ ∧ w ∈ V₁

Suppressing the second interior body of a four-body ear (a step of thm:pencil-x0-open-ear-four): suppressing x 1 and relinking e 1 to x 0 − x 2 leaves the ear a − x 0 − x 2 − x 3 − b on V₁, with the labels e 0, e 1, e 3, e 4.

theorem CombinatorialRigidity.Molecular.splitOff_ear_three {α : Type u_2} {β : Type u_3} {G : Graph α β} {V₁ : Set α} {x : Fin 3 → α} {a b : α} {e : Fin 4 → β} (hcover : G.vertexSet = V₁ ∪ Set.range x) (hinj : Function.Injective x) (hxV₁ : ∀ (i : Fin 3), x i ∉ V₁) (ha : a ∈ V₁) (hb : b ∈ V₁) (hab : a ≠ b) (hpath : ∀ (i : Fin 4), G.IsLink (e i) (pathVertex a x b i.castSucc) (pathVertex a x b i.succ)) (hsep : ∀ (f : β) (u w : α), G.IsLink f u w → (∀ (i : Fin 4), f ≠ e i) → u ∈ V₁ ∧ w ∈ V₁) : (G.splitOff (x 1) (x 0) (x 2) (e 1)).vertexSet = V₁ ∪ Set.range ![x 0, x 2] ∧ Function.Injective ![x 0, x 2] ∧ (∀ (i : Fin (Nat.succ 0).succ), ![x 0, x 2] i ∉ V₁) ∧ (∀ (i : Fin 3), (G.splitOff (x 1) (x 0) (x 2) (e 1)).IsLink (![e 0, e 1, e 3] i) (pathVertex a ![x 0, x 2] b i.castSucc) (pathVertex a ![x 0, x 2] b i.succ)) ∧ ∀ (f : β) (u w : α), (G.splitOff (x 1) (x 0) (x 2) (e 1)).IsLink f u w → (∀ (i : Fin (Nat.succ 0).succ.succ), f ≠ ![e 0, e 1, e 3] i) → u ∈ V₁ ∧ w ∈ V₁

Suppressing the second interior body of a three-body ear (a step of thm:pencil-x0-open-ear-three): suppressing x 1 and relinking e 1 to x 0 − x 2 leaves the ear a − x 0 − x 2 − b on V₁, with the labels e 0, e 1, e 3.

theorem CombinatorialRigidity.Molecular.induce_splitOff_ear {α : Type u_2} {β : Type u_3} {G : Graph α β} {V₁ : Set α} {k : ℕ} {x : Fin k → α} (hcover : G.vertexSet = V₁ ∪ Set.range x) (hxV₁ : ∀ (i : Fin k), x i ∉ V₁) {v u w : α} {e₀ : β} (hv : v ∈ Set.range x) (hu : u ∉ V₁) (he₀ : ∀ (y y' : α), G.IsLink e₀ y y' → y ∉ V₁ ∨ y' ∉ V₁) : G[V₁] ≤ G.splitOff v u w e₀ ∧ (G.splitOff v u w e₀)[V₁] = G[V₁]

Splitting off an interior body keeps G[V₁] (a step of thm:pencil-x0-open-ear-four, thm:pencil-x0-open-ear-three and thm:pencil-x0-open-ear-two-orbit): if v is an interior body of the ear, u ∉ V₁, and e₀ links no two bodies of V₁ in G, then G[V₁] is a subgraph of G.splitOff v u w e₀, and is its subgraph induced on V₁.

Four independent points (thm:pencil-x0-open-ear-four)

theorem CombinatorialRigidity.Molecular.linearIndependent_tetra_witness {K : Type u_1} [Field K] (b₀ b₁ b₂ γ δ : K) : LinearIndependent K ![![b₀, b₁ + 1, γ, 1], ![b₀, b₁, b₂ + 1, 1], ![b₀ + 1, b₁, δ, 1], ![b₀, b₁, b₂, 1]]

Four independent points (a step of thm:pencil-x0-open-ear-four, the ear datum at which the six joins span Λ²K⁴): the points over the pictures (b₀, b₁ + 1), (b₀, b₁) and (b₀ + 1, b₁) at the heights γ, b₂ + 1 and δ, and (b₀, b₁, b₂, 1), are linearly independent for every γ and δ. In the step they are the points of x 0, x 2, x 3 and b, with (b₀, b₁) the picture of b and b₂ its height.

The base data of the steps at three and four interior bodies (def:pencil-ear-data)

theorem Graph.exists_earBase_splitOff {K : Type u_1} [Field K] {α : Type u_2} {β : Type u_3} [Infinite K] [Finite α] {G : Graph α β} {V₁ : Set α} {v u w : α} {e₀ : β} {k : ℕ} {y : Fin k → α} {a b : α} {e : Fin (k + 1) → β} (hk : 2 ≤ k) (hcover : (G.splitOff v u w e₀).vertexSet = V₁ ∪ Set.range y) (hinj : Function.Injective y) (hyV₁ : ∀ (i : Fin k), y i ∉ V₁) (ha : a ∈ V₁) (hb : b ∈ V₁) (hab : a ≠ b) (hpath : ∀ (i : Fin (k + 1)), (G.splitOff v u w e₀).IsLink (e i) (CombinatorialRigidity.Molecular.pathVertex a y b i.castSucc) (CombinatorialRigidity.Molecular.pathVertex a y b i.succ)) (hsep : ∀ (f : β) (p p' : α), (G.splitOff v u w e₀).IsLink f p p' → (∀ (i : Fin (k + 1)), f ≠ e i) → p ∈ V₁ ∧ p' ∈ V₁) (hl₀ : (G.splitOff v u w e₀).IsLink e₀ u w) (he₀ : ∀ (p p' : α), G.IsLink e₀ p p' → p ∉ V₁ ∨ p' ∉ V₁) (hind : (G.splitOff v u w e₀)[V₁] = G[V₁]) {ends : β → α × α} (hends : ∀ (f : β) (p p' : α), G.IsLink f p p' → G.IsLink f (ends f).1 (ends f).2) {xf xl : α} {X : Set α} (hxf : xf ∈ (G.splitOff v u w e₀).closedNbhd a) (hxl : xl ∈ (G.splitOff v u w e₀).closedNbhd b) (hX : Set.range y ⊆ X) (h₁ : X0Attains K G[V₁]) (h₂ : X0Attains K (G.splitOff v u w e₀)) {Pm : MvPolynomial (α × Fin 2) K} (hPm : Pm ≠ 0) : ∃ (q : α × Fin 2 → K) (z₁ : α → K) (la : Fin 3 → K) (lb : Fin 3 → K) (s₁ : α × Fin 2 ⊕ α → K) (ρ : Submodule K (CombinatorialRigidity.Molecular.ScrewSpace K 2)), (MvPolynomial.eval q) Pm ≠ 0 ∧ (G.splitOff v u w e₀).IsAdmissiblePicture q ∧ CombinatorialRigidity.Molecular.earPicture V₁ q s₁ = q ∧ ↑(Module.finrank K ↥(Submodule.span K (CombinatorialRigidity.Molecular.PanelHingeFramework.ofNormals (G.splitOff v u w e₀) (Function.update ends e₀ (u, w)) (CombinatorialRigidity.Molecular.earConfig V₁ q z₁ xf xl X la lb s₁) ⋯).toBodyHinge.rigidityRows)) = ↑(CombinatorialRigidity.Molecular.screwDim 2) * (↑(G.splitOff v u w e₀).vertexSet.ncard - 1) - (G.splitOff v u w e₀).deficiency 3 ∧ (∀ (f : β), (G.splitOff v u w e₀).IsLink f (Function.update ends e₀ (u, w) f).1 (Function.update ends e₀ (u, w) f).2 → (CombinatorialRigidity.Molecular.PanelHingeFramework.ofNormals (G.splitOff v u w e₀) (Function.update ends e₀ (u, w)) (CombinatorialRigidity.Molecular.earConfig V₁ q z₁ xf xl X la lb s₁) ⋯).toBodyHinge.supportExtensor f ≠ 0) ∧ (∀ (s : α × Fin 2 ⊕ α → K), z₁ ∈ G[V₁].liftingSpace (CombinatorialRigidity.Molecular.earPicture V₁ q s)) ∧ (∀ (s : α × Fin 2 ⊕ α → K), ∀ p ∈ G[V₁].closedNbhd a, z₁ p = la ⬝ᵥ CombinatorialRigidity.Molecular.pencilPicturePoint (CombinatorialRigidity.Molecular.earPicture V₁ q s) p) ∧ (∀ (s : α × Fin 2 ⊕ α → K), ∀ p ∈ G[V₁].closedNbhd b, z₁ p = lb ⬝ᵥ CombinatorialRigidity.Molecular.pencilPicturePoint (CombinatorialRigidity.Molecular.earPicture V₁ q s) p) ∧ (∀ (s : α × Fin 2 ⊕ α → K), { graph := G[V₁], supportExtensor := (CombinatorialRigidity.Molecular.PanelHingeFramework.ofNormals G ends (CombinatorialRigidity.Molecular.earConfig V₁ q z₁ xf xl X la lb s) ⋯).toBodyHinge.supportExtensor }.relScrews a b = ρ) ∧ (∀ (s : α × Fin 2 ⊕ α → K), { graph := (G.splitOff v u w e₀)[V₁], supportExtensor := (CombinatorialRigidity.Molecular.PanelHingeFramework.ofNormals (G.splitOff v u w e₀) (Function.update ends e₀ (u, w)) (CombinatorialRigidity.Molecular.earConfig V₁ q z₁ xf xl X la lb s) ⋯).toBodyHinge.supportExtensor }.relScrews a b = ρ) ∧ (∀ (s : α × Fin 2 ⊕ α → K), ↑(Module.finrank K ↥(Submodule.span K { graph := G[V₁], supportExtensor := (CombinatorialRigidity.Molecular.PanelHingeFramework.ofNormals G ends (CombinatorialRigidity.Molecular.earConfig V₁ q z₁ xf xl X la lb s) ⋯).toBodyHinge.supportExtensor }.rigidityRows)) = ↑(CombinatorialRigidity.Molecular.screwDim 2) * (↑V₁.ncard - 1) - G[V₁].deficiency 3) ∧ ∀ (s : α × Fin 2 ⊕ α → K), ↑(Module.finrank K ↥(Submodule.span K { graph := (G.splitOff v u w e₀)[V₁], supportExtensor := (CombinatorialRigidity.Molecular.PanelHingeFramework.ofNormals (G.splitOff v u w e₀) (Function.update ends e₀ (u, w)) (CombinatorialRigidity.Molecular.earConfig V₁ q z₁ xf xl X la lb s) ⋯).toBodyHinge.supportExtensor }.rigidityRows)) = ↑(CombinatorialRigidity.Molecular.screwDim 2) * (↑V₁.ncard - 1) - G[V₁].deficiency 3

The base data of the steps at three and four interior bodies (a step of thm:pencil-x0-open-ear-four and thm:pencil-x0-open-ear-three, their first stage). Let H = G.splitOff v u w e₀ have an open ear a − y − b on V₁ with at least two interior bodies, with the same subgraph on V₁ as G, and let the ear data read the planes at xf ∈ N_H[a] and xl ∈ N_H[b]. If G[V₁] and H attain, there are base data (q, z₁, la, lb) with:

• q off the given nonzero polynomial Pm and admissible for H;
• over the picture of every ear datum, z₁ a height of G[V₁] agreeing with the planes la, lb on the closed neighbourhoods of a, b;
• one ear datum s₁, with picture q, at which H, with the selector ends relinked at e₀, has nonzero hinges and its target rank;
• at every ear datum, the relative screws ρ of G[V₁] between a and b, and its target rank, in the frameworks of both G and H.

Three and four interior bodies, given that the suppressed body can be put back

theorem Graph.X0Attains.of_openEar_splitOff {K : Type u_1} [Field K] {α : Type u_2} {β : Type u_3} [Infinite K] [Finite α] [Finite β] {G : Graph α β} (hG : G.IsX0Graph) {V₁ : Set α} {m : ℕ} (hm : 2 ≤ m) {x : Fin (m + 1) → α} {a b : α} {e : Fin (m + 2) → β} (hcover : G.vertexSet = V₁ ∪ Set.range x) (hinj : Function.Injective x) (hxV₁ : ∀ (i : Fin (m + 1)), x i ∉ V₁) (ha : a ∈ V₁) (hb : b ∈ V₁) (hab : a ≠ b) (hpath : ∀ (i : Fin (m + 2)), G.IsLink (e i) (CombinatorialRigidity.Molecular.pathVertex a x b i.castSucc) (CombinatorialRigidity.Molecular.pathVertex a x b i.succ)) (hsep : ∀ (f : β) (u w : α), G.IsLink f u w → (∀ (i : Fin (m + 2)), f ≠ e i) → u ∈ V₁ ∧ w ∈ V₁) {v u w : α} {e₀ : β} {y : Fin m → α} {e'' : Fin (m + 1) → β} (hcover'' : (G.splitOff v u w e₀).vertexSet = V₁ ∪ Set.range y) (hinj'' : Function.Injective y) (hyV₁ : ∀ (i : Fin m), y i ∉ V₁) (hpath'' : ∀ (i : Fin (m + 1)), (G.splitOff v u w e₀).IsLink (e'' i) (CombinatorialRigidity.Molecular.pathVertex a y b i.castSucc) (CombinatorialRigidity.Molecular.pathVertex a y b i.succ)) (hsep'' : ∀ (f : β) (p p' : α), (G.splitOff v u w e₀).IsLink f p p' → (∀ (i : Fin (m + 1)), f ≠ e'' i) → p ∈ V₁ ∧ p' ∈ V₁) (hyx : Set.range y ⊆ Set.range x) (hv : v ∈ Set.range x) (hu : u ∉ V₁) (hl₀ : G.IsLink e₀ u v) (hl₀'' : (G.splitOff v u w e₀).IsLink e₀ u w) (hdef : (G.splitOff v u w e₀).deficiency 3 ≤ G.deficiency 3) {xf xl : α} (hxf : x ⟨0, ⋯⟩ = xf) (hxl : x ⟨m, ⋯⟩ = xl) (hvf : v ≠ xf) (hvl : v ≠ xl) (hins : ∀ (q : α × Fin 2 → K) (z : α → K) (la lb : Fin 3 → K) (ρ : Submodule K (CombinatorialRigidity.Molecular.ScrewSpace K 2)), z a = la ⬝ᵥ CombinatorialRigidity.Molecular.pencilPicturePoint q a → z b = lb ⬝ᵥ CombinatorialRigidity.Molecular.pencilPicturePoint q b → ∃ (Q : MvPolynomial (α × Fin 2 ⊕ α) K), Q ≠ 0 ∧ ∀ (s : α × Fin 2 ⊕ α → K), (MvPolynomial.eval s) Q ≠ 0 → (G.splitOff v u w e₀).IsAdmissiblePicture (CombinatorialRigidity.Molecular.earPicture V₁ q s) → ∃ (x₂ : Fin 4 → K), x₂ 3 = 1 ∧ ∀ (p : α → Fin 4 → K), p v = x₂ → (∀ (t : α), t ≠ v → p t = fun (j : Fin 4) => CombinatorialRigidity.Molecular.earConfig V₁ q z xf xl (Set.range x) la lb s (t, j)) → min (Module.finrank K ↥(ρ ⊔ Submodule.span K (Set.range fun (i : Fin (m + 1)) => CombinatorialRigidity.Molecular.pointJoin (fun (j : Fin 4) => CombinatorialRigidity.Molecular.earConfig V₁ q z xf xl (Set.range x) la lb s (CombinatorialRigidity.Molecular.pathVertex a y b i.castSucc, j)) fun (j : Fin 4) => CombinatorialRigidity.Molecular.earConfig V₁ q z xf xl (Set.range x) la lb s (CombinatorialRigidity.Molecular.pathVertex a y b i.succ, j))) + 1) 6 ≤ Module.finrank K ↥(ρ ⊔ Submodule.span K (Set.range fun (i : Fin (m + 2)) => CombinatorialRigidity.Molecular.pointJoin (p (CombinatorialRigidity.Molecular.pathVertex a x b i.castSucc)) (p (CombinatorialRigidity.Molecular.pathVertex a x b i.succ))))) (h₁ : X0Attains K G[V₁]) (h₂ : X0Attains K (G.splitOff v u w e₀)) : X0Attains K G

The steps at three and four interior bodies, given that v can be put back (a step of thm:pencil-x0-open-ear-four and thm:pencil-x0-open-ear-three). Let G satisfy the standing hypotheses, with an open ear a − x 0 − ⋯ − x m − b on V₁, m ≥ 2, and let G″ = G.splitOff v u w e₀, G with the interior body v suppressed and e₀ relinked from u − v to u − w, have the open ear a − y − b on V₁, with def₃(G″) ≤ def₃(G). Suppose that v can be put back off a polynomial: over any base data (q, z, la, lb), z on the plane la at a and on lb at b, and any subspace ρ, some nonzero polynomial in the ear data s has, at every s off it at which the picture is admissible for G″, an affine x₂ such that every point assignment that agrees with the configuration of s off v and puts x₂ at v gives dim(ρ + Λ_G) ≥ min(dim(ρ + Λ_{G″}) + 1, 6), where Λ_G and Λ_{G″} are the spans of the joins of the ears of G and G″. If the general configurations of G[V₁] and of G″ attain, so does that of G.

Proof. The base data are Graph.exists_earBase_splitOff's, at the main-picture polynomial of G, with ρ the relative screws of a and b in G[V₁]. Ear data off three polynomials give G″ at least its target rank and an admissible picture, and let v be put back; the ear rank formula at G″ bounds dim(ρ + Λ_{G″}), and with v put back the ear data of G meet (⋆) (Graph.deficiency_induce_add_le_of_ear for the bound 6). Ear data of G off the polynomial of that span bound and off the main-picture polynomial of G then give G its target. The four-body step puts v back by the tetrahedron (exists_insertion_four), the three-body step by the case split on ρ (exists_insertion_three).

The open ear with four interior bodies (thm:pencil-x0-open-ear-four)

theorem Graph.X0Attains.of_openEar_four {K : Type u_1} [Field K] {α : Type u_2} {β : Type u_3} [Infinite K] [Finite α] [Finite β] {G : Graph α β} (hG : G.IsX0Graph) {V₁ : Set α} {x : Fin 4 → α} {a b : α} {e : Fin 5 → β} (hcover : G.vertexSet = V₁ ∪ Set.range x) (hinj : Function.Injective x) (hxV₁ : ∀ (i : Fin 4), x i ∉ V₁) (ha : a ∈ V₁) (hb : b ∈ V₁) (hab : a ≠ b) (hpath : ∀ (i : Fin 5), G.IsLink (e i) (CombinatorialRigidity.Molecular.pathVertex a x b i.castSucc) (CombinatorialRigidity.Molecular.pathVertex a x b i.succ)) (hsep : ∀ (f : β) (u w : α), G.IsLink f u w → (∀ (i : Fin 5), f ≠ e i) → u ∈ V₁ ∧ w ∈ V₁) (h₁ : X0Attains K G[V₁]) (h₂ : X0Attains K (G.splitOff (x 1) (x 0) (x 2) (e 1))) : X0Attains K G

An open ear with four interior bodies (thm:pencil-x0-open-ear-four). Let G satisfy the standing hypotheses, with an open ear a − x 0 − x 1 − x 2 − x 3 − b on V₁ whose ends may be adjacent, and let G″ = G.splitOff (x 1) (x 0) (x 2) (e 1) be G with x 1 suppressed, the freed label e 1 relinked to x 0 − x 2. If the general configurations of G[V₁] and of G″ attain, so does that of G.

Proof. Graph.X0Attains.of_openEar_splitOff, with the ear a − x 0 − x 2 − x 3 − b of G″ (splitOff_ear_four) and def₃(G″) ≤ def₃(G) (Graph.splitOff_deficiency_le_of_eq_left). x 1 is put back at the point of exists_insertion_four once the six joins of the points of x 0, x 2, x 3 and b span Λ²K⁴: a condition on the ear data that holds off the zero set of a polynomial nonzero at the ear datum whose four points are those of linearIndependent_tetra_witness.

The open ear with three interior bodies (thm:pencil-x0-open-ear-three)

theorem Graph.X0Attains.of_openEar_three {K : Type u_1} [Field K] {α : Type u_2} {β : Type u_3} [Infinite K] [Finite α] [Finite β] {G : Graph α β} (hG : G.IsX0Graph) {V₁ : Set α} {x : Fin 3 → α} {a b : α} {e : Fin 4 → β} (hcover : G.vertexSet = V₁ ∪ Set.range x) (hinj : Function.Injective x) (hxV₁ : ∀ (i : Fin 3), x i ∉ V₁) (ha : a ∈ V₁) (hb : b ∈ V₁) (hab : a ≠ b) (hpath : ∀ (i : Fin 4), G.IsLink (e i) (CombinatorialRigidity.Molecular.pathVertex a x b i.castSucc) (CombinatorialRigidity.Molecular.pathVertex a x b i.succ)) (hsep : ∀ (f : β) (u w : α), G.IsLink f u w → (∀ (i : Fin 4), f ≠ e i) → u ∈ V₁ ∧ w ∈ V₁) (h₁ : X0Attains K G[V₁]) (h₂ : X0Attains K (G.splitOff (x 1) (x 0) (x 2) (e 1))) : X0Attains K G

An open ear with three interior bodies (thm:pencil-x0-open-ear-three). Let G satisfy the standing hypotheses, with an open ear a − x 0 − x 1 − x 2 − b on V₁ whose ends may be adjacent, and let G″ = G.splitOff (x 1) (x 0) (x 2) (e 1) be G with x 1 suppressed, the freed label e 1 relinked to x 0 − x 2. If the general configurations of G[V₁] and of G″ attain, so does that of G.

Proof. Graph.X0Attains.of_openEar_splitOff, with the ear a − x 0 − x 2 − b of G″ (splitOff_ear_three) and def₃(G″) ≤ def₃(G) (Graph.splitOff_deficiency_le_of_eq_left). x 1 is put back at the point of exists_insertion_three, which asks that the span W of ρ and the joins of the ear of G″ be Λ²K⁴ whenever it contains every line through the point y₁ of x 0 and every line through the point y₃ of x 2, the two stars. Over the base data, either every relative screw pairs to zero with every line joining the planes la at a and lb at b, and then W does not contain both stars (not_star_sup_star_le_of_klein); or some c ∈ ρ does not, and then ⟨c, y₁ ∧ y₃⟩ ≠ 0 is a further condition on the ear data, a span bound against the kernel of ⟨c, ·⟩ that holds at a pair of affine points (exists_klein_liftPlane_affine_ne_zero), under which a W containing both stars is Λ²K⁴ (eq_top_of_star_sup_star_le).