Add Mayer K_n edge-count split and inside-connected crux (GJ §18.4)

[phasetr]

Part of #1499 (Mayer expansion general-t identity, Phase B).

Summary

Toward the root-component bijection D_n = ∑_{C∋0} c_{|C|} D_{n-|C|}, including
the hardest ingredient — that the within-component edges form a connected
spanning subgraph on C.

Declarations (in MayerRootComponent.lean)

• rootComponent_edge_card_split: #(S∩C.sym2) + #(S∩Cᶜ.sym2) = #S via
  Finset.sym2 + Finset.card_filter_add_card_filter_not + crossing-free.
• coe_rootComponentFinset: ↑(rootComponentFinset S r) = the support of r's
  connected component in fromEdgeSet ↑S.
• induce_fromEdgeSet_inside_eq: the within-C edges S∩C.sym2 induce the same
  graph on C as all of S (outside/crossing edges give no inside adjacency).
• induce_fromEdgeSet_inside_connected (crux): the within-C edges induce a
  connected graph on C. Since ↑C is r's component support, the induced
  graph is the component's toSimpleGraph, connected by
  SimpleGraph.ConnectedComponent.connected_toSimpleGraph.

The fiber sum (reindex S_in to K_C, S_out to K_complement; sum = c(K_C)·D(K_compl))
and the recurrence c_n + (n-1)c_{n-1} = 0 follow.

Verification

• Targeted lake build: clean, zero warnings, no sorry.
• lake exe GKSTest: all passed.
• latexmk: 263 pages, no undefined refs; Japanese grep clean.

References

• Glimm–Jaffe, Quantum Physics, §18.4; Friedli–Velenik §5.7.