Flat pi graph and actual face components
Abstract
The complete native flat-component counting and endpoint theorem, with loops and parallel edges retained.
The source telescope is CFMP_GEOMETRIC_REALIZATION.md Sections 1 and 61-62. Fix the actual finite ideal tetrahedron face pairing of the stated compact connected orientable 3-manifold whose nonempty boundary components have genus at least two. Regard its whole-face pairing as p:EdgeStarTransitions.RawFacePairing(T). Its global edges are exactly p.GlobalEdge, the quotient of T times Fin(6) by the equivalence relation generated by the actual paired-face edge steps. P(t,q)=p.edgeLabel(t,q), and d(e) counts the entire P fiber. Source self-gluings and repeated edge labels remain in scope. The theorem below holds for every finite raw pairing, so its application to this source pairing uses no additional topological premise.
One common positive length ell:E->Real gives x(t,q)=cosh(ell(P(t,q))) and the original raw cosine, square-root, clip and arccos angle alpha(t,q). The slots are (12,13,14,34,24,23). Every global occurrence angle sum is 2*pi and every d(e)>=6. F is derived from the unique native closed flat sector in PositiveFlatClassification.positive_classification; it is exactly the set of nongenuine blocks. It is assumed nonempty. The local and component logarithmic inequalities, including their positive corrections, and saturated actual quotient support are derived in FlatComponentBudget from these same coordinates.
The pi multigraph has one edge for each actual t in F and the two global labels of its uniquely selected opposite pi slots as its ends. Its vertex set Vpi is the labels with positive global pi multiplicity m(e). The carrier uses the actual edge index t and two distinct local darts, so repeated labels, loops and parallel edges are retained. Its canonical subdivision has vertices Vpi disjoint-union (F times Fin(2)); each original edge is the three-edge path from its first global end to its first dart, its second dart, and its second global end. A loop becomes a triangle and two parallel edges become a six-cycle. The dart-fiber bijection proves that each global vertex degree is exactly m(e), with a loop contributing two, and every internal dart has degree two.
PathComponent is an actual connected component of this faithful subdivision with a simple walk covering every vertex, distinct endpoints, and degree one at both endpoints. Thus pathCount is the number of actual path components; it is not defined by an Euler deficit or by dividing the number of leaves. The graph proof establishes that a finite connected graph of degrees one or two has such a covering path exactly when it has a leaf. A maximal simple path starting at a leaf is closed under adjacency: an unvisited neighbor at an internal vertex would create three neighbors, and an unvisited neighbor at its terminal vertex would extend the path. Connectivity then forces it to cover the component. The handshake identity and connected edge lower bound give exactly two leaves in each such component. Components with no leaves retain their cycle contribution.
cF=faceComponentCount is the cardinality of the quotient of F by the relation generated by actual flat/flat face pairing. It is a separate relation from pi graph connectivity. Saturated support ensures that two distinct pi darts with the same global label belong to one actual face component. Therefore each pi graph component maps to a unique actual face component. The positive coefficient witness of FlatComponentBudget.component_exposed_label supplies a leaf in each face component, making the map from path components onto face components surjective.
The information-escape audit of complete_flat_counting remains unfinished under https://github.com/the-omega-institute/trureturing/issues/17994. Its full source law and equivalence bridge compile, but complete variation, sensitivity, observational-dependence and admissible source-selection evidence remain missing. No zero-curvature flat instance is assumed to supply an audit witness; the issue supplies neither mathematical proof nor validated registration status.
Theorem 1.1 (Complete original component counting conclusion).
Proof. Machine-checked in Lean as D5/S3/Geometry/Hyperideal/FlatPathAllocation.complete_flat_counting (✓ std3). ∎
Source. Repository-derived.
Commentary.
Write f=flatCount=card(F), v=piVertexCount=card(Vpi), p=pathCount and c=faceComponentCount. The subdivision has v+2f vertices and degree sum 6f. Its degree deficit is the number of leaves, which the proved path-component classification identifies as 2*p. Hence v=f+p. Surjective path allocation gives c<=p; F nonempty gives c>=1. The stated natural-number subtraction inequalities follow with their required size inequalities already proved. For every actual flat face component the endpoint theorem gives two distinct labels with pi occurrences there, global multiplicity one and genuine occurrences. No local n<=2 assertion is made for both endpoints.
This is Theorem 62.1 on the original common length and quotient carrier. It permits cycle components and proves neither that every pi component is a path nor a full CFMP realization or length existence theorem. Its source consumers are the Section 62 exclusion requiring 3<=4-2 for three flat blocks in at least two face components when card(E)=4, and the Section 64 restriction card(F)<=vpi-cF. Those consumers are prose applications, not additional Lean theorems or an independent admission witness.