Two original families with independent conditioned totals
Abstract
Strict normalized bounds for full conditioned polygon families
Theorem 1.1 (Two nonempty cross-intersecting families have normalized sum below one).
Proof. Machine-checked in Lean as D5/S3/Geometry/Polygons/PolygonStrictNormalization.original_normalized_strict (✓ std3). ∎
Source. Repository-derived.
Commentary.
Fix an arbitrary natural n at least 14 and derive NeZero(n) from this inequality. The vertices are ZMod(n), ear(i) is the chord with endpoints i-1 and i+1, and EarCenters(T) is the complete set of centres of ears present in T. The arbitrary finite sets P,Q are disjoint, their union K has pairwise noncrossing ears, and their ordered cardinalities (p,q) are (2,2), (3,3), (2,4), or (4,2). There is no restriction on their cyclic placement.
WholeFiber(P,Q) is definitionally ConditionFiber(P,Q,empty,empty): every maximal noncrossing finite set T of actual internal diagonals with P contained in EarCenters(T) and Q disjoint from EarCenters(T). The empty observation imposes no further condition. Thus WholeFiber(Q,P) is a separate full conditioned type on the same polygon. A and B are arbitrary finite subfamilies of these respective types, and every T in A and U in B has a common ear in their full EarCenters sets. In the formula Natcard denotes Nat.card, card denotes Finset.card, and every division and addition in the conclusion takes place in Real.
For H contained in E_K, let w(R) be the real cast of Nat.card(ConditionFiber(P,Q,H,R)). When the ears centred in H are pairwise noncrossing, the actual conditioned trace flip injects the fibre with trace insert(h,R) into the fibre with trace R. Finite insertion induction gives w(S) at most w(R) whenever R is contained in S contained in H. This argument retains zero fibres and uses no positivity assumption on individual traces.
For every h in H, source_conditioned_witnesses supplies an actual member of the empty-trace fibre containing two distinct diagonals crossing ear(h). Every image of the singleton flip has at most one such chord, since all retained chords coexist with ear(h) in its input. That supplied fan lies outside the image, so w({h}) is strictly below w(empty). Integrality and antitonicity give w(R)+1 at most w(empty) for every nonempty R contained in H.
The complete fibres partition WholeFiber(P,Q) by T mapped to EarCenters(T) intersect H. Equiv.sigmaSubtypeFiberEquiv supplies the finite-fibre partition, with only the ConditionFiber subtype identification performed locally. Summing over every R contained in H gives exactly Nat.card(WholeFiber(P,Q)); the empty trace and every actual completion remain in this total.
On the finite distributive lattice of subsets of H, the proof applies the pinned Mathlib fkg inequality to the monotone functions w(bottom)-w and the indicator of a relatively upper family C. Subtracting one unit at bottom preserves antitonicity by the integer gap. Since C is nonempty and omits bottom, this yields mass(w,C)/sum(w) strictly below card(C)/card(powerset(H)). The positive whole-fibre total comes from source_conditioned_witnesses. The local signed-shift and bottom-subtraction helpers are consumed applications of fkg.
exists_original_terminal_compression supplies the same H for both original families and upper families C,D contained in powerset(H), with the original cardinalities bounded by the two respective weighted masses. Both upper families are nonempty and cross-intersecting. The complement map R mapped to H minus R injects D into a family disjoint from C, so card(C)+card(D) is at most card(powerset(H)). Apply the strict weighted comparison independently to P given Q and Q given P, add the bounds, and obtain the displayed strict inequality.
Application with the explicit Catalan denominators.
For the full B-37.2 application, retain all the hypotheses above but allow A or B to be empty. Define the integer function Npq as follows; Catalan(k) is the natural Catalan number, choose(q,j) is the binomial coefficient, and n-p-j-2 uses natural subtraction.
The pairwise noncrossing hypothesis on K is exactly PolygonEarContraction.Compatible(K). Apply PolygonConditionalCounts.conditional_card first to P,Q and then separately to Q,P, using disjointness in the corresponding orientation. WholeFiber is the complete fibre with empty observation, so these applications give the two integer identities below. They do not identify the two denominators.
Apply PolygonConditionedFan.source_conditioned_witnesses in each orientation, swapping the ordered cardinality case and rewriting union_comm for the second. Its nonempty whole-fibre witness and positive Nat.card give Npq(n,p,q)>0 and Npq(n,q,p)>0 in Int. Casting each integer identity to Real gives separately Nat.card(WholeFiber(P,Q))=Npq(n,p,q) and Nat.card(WholeFiber(Q,P))=Npq(n,q,p), with both right sides positive and nonzero in Real. These are casts of two actual counts, not assumptions or a symmetry assertion.
For every actual T in WholeFiber(P,Q) and U in WholeFiber(Q,P), PolygonSimultaneousCompression.common_ears_eq_trace_inter supplies the full common-ear identity below. E_K is the set of centres outside K whose ears are compatible with every ear in K. The identity transports the full-ear cross-intersection premise to the common observation carrier without requiring intersection inside a selected six-ear set.
Write S for the following expression in Real, with the integer Npq values cast individually.
If A and B are both nonempty, apply original_normalized_strict and rewrite its two whole-fibre denominators by their own cast count identities. This gives S<1. If A is empty, S=card(B)/Npq(n,q,p); Finset.card_le_univ bounds card(B) by Fintype.card(WholeFiber(Q,P))=Nat.card(WholeFiber(Q,P)). Dividing by its positive real total gives S<=1. If B is empty, use the separate bound for A and Npq(n,p,q). If both are empty, S=0.
Equality cannot occur with both families nonempty. With A empty, S=1 is equivalent, by positivity of Npq(n,q,p), to card(B)=Nat.card(WholeFiber(Q,P)); Fintype.card and Finset.eq_univ_of_card then give B=univ on its own whole fibre. Conversely B=univ has precisely that total, so S=1. With B empty the same reasoning uses Npq(n,p,q) and A=univ on WholeFiber(P,Q). Positive whole totals exclude the both-empty pair from equality. Thus the exact equality classification is:
This application includes all n at least 14, all four ordered size cases, arbitrary compatible placements, every actual completion, and separate counts in the two orientations. It is a consequence of the strict theorem, the original count and fan results, the common-ear identity, and finite-cardinality facts. No separate named upper-bound, equality, count, cast or final-application theorem is needed.
Six labelled complementary graphs.
Fix any n at least 14 and any labelled set D of polygon vertices. Let M indexed by Fin(3) be three pairwise disjoint matchings of ear centres, each of cardinality two, with M(0) union M(1) union M(2)=D. Assume the original ear chords centred in D are pairwise noncrossing. These hypotheses allow arbitrary compatible placements; there is no cyclic symmetry or position assumption. The labels form the dependent sum of the pairs (i,x) with i in Fin(3) and x in M(i). Its cardinality is 2+2+2=6. For each i, let j<k be the other two zero-based indices: (j,k)=(1,2),(0,2),(0,1) for i=0,1,2 respectively. This determines the indices uniquely and does not identify different polygon placements.
For the label (i,x), set P=M(j) union {x} and Q=M(k) union (M(i) minus {x}). Pairwise disjointness makes x absent from both M(j) and M(k), so card(P)=2+1=3 and card(Q)=2+(2-1)=3. The same hypotheses give Disjoint(P,Q), P union Q=D, card(D)=6, D minus P=Q and D minus Q=P. These are derived partition facts. For either orientation b, let S=P and S’=Q when b is false, and S=Q and S’=P when b is true. In particular S’=D minus S in both orientations.
Define Gamma_D(S) to be the subtype of all actual triangulations T with EarCenters(T) intersect D=S. A triangulation is its entire finite set of internal diagonals, with the maximal noncrossing predicate used by PolygonEarSlide.Carrier.IsTriangulation. No other ear or diagonal is restricted. Since S and S’ partition D, the displayed trace equality is equivalent to S being contained in EarCenters(T) and S’ being disjoint from EarCenters(T). Thus the identity on underlying chord sets is a bijection from Gamma_D(S) to PolygonSimultaneousCompression.WholeFiber(S,S’), and the analogous identity identifies Gamma_D(S’) with WholeFiber(S’,S). Both maps and inverses preserve every chord. The nonempty disjoint sets S,S’ also imply that vertices on opposite sides have distinct chord sets: equality would force their D-traces S and S’ to coincide.
Put X=Gamma_D(S) and Y=Gamma_D(S’). Join T in X to U in Y exactly when their chord sets differ and their complete EarCenters sets are disjoint. Under the two bijections this is exactly the full-ear disjointness relation on the respective WholeFiber types. It is not a relation merely on the D-traces. For every finite subset A of the entire X, define N_Y(A) to be all U in Y adjacent to some T in A. Mapping A and its neighborhood by the bijections gives exactly the corresponding WholeFiber subset and neighborhood; finite cardinalities, the empty subset and the full subset are preserved.
Apply PolygonConditionalCounts.conditional_card and PolygonConditionedFan.source_conditioned_witnesses separately in the two orientations, as above, now with ordered sizes (3,3). They give card(X)=card(Y)=Npq(n,3,3)>0, first as actual natural-cardinality identities in Int and then by positive casts in Real. The equal totals here follow from substituting the same ordered sizes into the two count identities. They impose no symmetry assertion for other size cases.
For any A contained in X, put B=Y minus N_Y(A). Every T in A and U in B has a common ear: otherwise their distinct chord sets and disjoint full ear sets would make them adjacent, contradicting U not in N_Y(A). Apply the preceding weak normalized bound to A,B and their equal positive totals. Since card(B)=card(Y)-card(N_Y(A)), it gives card(A)<=card(N_Y(A)). This is Hall’s inequality for every finite subset of the complete left carrier, without a restriction to subsets of some separately selected admissible family.
If A is nonempty and proper and B is nonempty, original_normalized_strict makes that inequality strict. If B is empty, N_Y(A)=Y, and properness gives card(A)<card(X)=card(Y), again strictly. The empty neighborhood of the empty subset follows directly from its definition. Applying Hall’s inequality to the full X gives card(Y)<=card(N_Y(X)); the reverse inequality follows from containment in Y, hence N_Y(X)=Y. Consequently equality in Hall’s inequality holds exactly for A empty or A=X. Full saturation uses the weak normalized bound; it requires no triangulation whose complete ear set is exactly S.
All signed integer deficits card(A)-card(N_Y(A)) are therefore at most zero, and the empty subset attains zero. Hence zero is the greatest element of the set of these deficits. Finiteness makes this the actual maximum over all subsets of X. Every count, adjacency identification, Hall inequality, strict proper expansion, empty/full neighborhood identity, equality classification and maximum-deficit assertion holds for each of the six dependent labels and independently in both orientations.
At the minimum allowed n=14, the matchings {0,2}, {4,6} and {8,10} in ZMod(14) satisfy the pair cardinalities, disjointness and actual ear compatibility. The same conclusion applies to all six of their labels in both orientations. The symbolic argument above covers arbitrary compatible labelled D for every n at least 14; this inhabited boundary example adds no position restriction. This graph application composes the canonical strict-normalization, conditioned-count, conditioned-fan and common-ear results with finite-set and bijection identities. It asserts neither the B-33.6 partition nor the complete-double-ear branch maximum L, the twelve-family classification or the global residual Kres.
Complementary path loss in one actual family.
Use six distinct labels f(i,b), with i in Fin(3) and b in Fin(2), on ZMod(n), for any n at least 14. The injective map f assigns f00,f01,f10,f11,f20,f21 to the abstract edges 12,34,13,24,14,23 respectively. Let D be its image and M_k={f(k,0),f(k,1)}. Then D has cardinality six and is the disjoint union of the three two-element matchings. Require pairwise noncrossing actual ears centred in D; shared chord endpoints are allowed. The abstract four-vertex edge labels specify incidence only and impose no order or symmetry on the polygon vertices.
The four complete stars are S_0={f00,f10,f20}, S_1={f00,f11,f21}, S_2={f01,f10,f21}, S_3={f01,f11,f20}. Fix any prescribed four witnesses W_a in one finite family F of actual triangulations, with full EarCenters(W_a)=S_a, for a in Fin(4). Require full-ear intersection only for distinct members T,U of this same F. For each k in Fin(3), require an actual U_k in F with EarCenters(U_k) intersect D=M_k. The active-core witnesses need not be chosen uniquely and their ears outside D are unrestricted. All statements below quantify over every such f,W,F, rather than selecting different families for different paths.
In finite-set notation define Gamma(D,R)={T : IsTriangulation(T) and EarCenters(T) intersect D=R}, where T ranges over all finite chord sets on the original polygon. This is the entire finite set of actual completions with that D-trace. Its subtype is the Gamma_D(R) used above. If P,Q partition D, the identity on underlying chord sets identifies its P subtype with WholeFiber(P,Q), and its Q subtype with WholeFiber(Q,P). The selections A=F intersect Gamma(D,P) and B=F intersect Gamma(D,Q) correspond respectively to all elements of those WholeFiber types whose underlying chord sets belong to F. These bijections preserve their cardinalities and all full-ear intersection statements; no completion or outside-D ear is discarded.
For any complementary three-element P,Q, conditional_card in the two orientations gives (card(Gamma(D,P)):Int)=Npq(n,3,3)=(card(Gamma(D,Q)):Int). Put w3(n)=toNat(Npq(n,3,3)). Thus card(Gamma(D,P))=Nat.card(WholeFiber(P,Q))=w3(n), and separately card(Gamma(D,Q))=Nat.card(WholeFiber(Q,P))=w3(n). The source_conditioned_witnesses positivity gives w3(n)>0, so its integer cast equals Npq(n,3,3) and its real cast is positive. Expanding the preceding inclusion-exclusion formula gives Npq(n,3,3)=Catalan(n-5)-3Catalan(n-6)+3Catalan(n-7)-Catalan(n-8), with each Catalan value cast to Int and natural subtraction in the indices. Equality of these two totals follows from their common ordered sizes (3,3).
First suppose A and B are both nonempty. Their distinct complementary D-traces make every cross-side pair different as actual chord sets. Hence the distinct-member full-ear intersection condition on F supplies exactly the cross-family hypothesis of original_normalized_strict after the identity transports above. Substitute the two positive whole-fibre totals to get card(A)/w3(n)+card(B)/w3(n)<1 in Real, hence card(A)+card(B)<w3(n). Integrality gives card(A)+card(B)<=w3(n)-1 in Nat and, after casting the counts separately, in Int. The pair inequality is a consequence of the actual family hypotheses, not an extra assumption.
The empty-side case uses an actual omitted completion. More generally, let R be a three-element subset of the compatible D and let M be an active two-element D-trace disjoint from R. Choose U in this same F with EarCenters(U) intersect D=M and h in M. PolygonCompressionTrace.independent_iff_noncrossing makes D cyclically independent, and earCenters_independent makes the full EarCenters(U) independent. Therefore h-1,h+1 lie outside both D and EarCenters(U), while h is outside R. Apply PolygonConditionedFan.fan_triangulation to the literal fan(R,h): it is an actual complete triangulation T, with R contained in EarCenters(T) contained in R union {h-1,h+1}. Consequently T belongs to Gamma(D,R). Any common ear with U would either lie in R intersect M, which is empty, or be h-1 or h+1, also excluded. Thus their full ear sets are disjoint. They are distinct since h belongs to EarCenters(U) and is absent from EarCenters(T). The distinct-member condition on F forces T not to belong to F. This construction uses no restriction on U’s other outside-D ears; the literal fan construction remains supplied by PolygonConditionedFan.
In the generic complementary case suppose an active two-element trace M is disjoint from P and an active two-element trace N is disjoint from Q, both witnessed in F. Apply the omitted-completion argument to (R,M)=(P,M) and (R,M)=(Q,N). Each selected side is a proper subset of its own entire fibre, so card(A)<=w3(n)-1 and card(B)<=w3(n)-1 individually. If A is empty use the latter bound; if B is empty use the former. If both are empty the pair sum is zero and w3(n)>0 still gives the same bound. Together with the nonempty argument this proves card(A)+card(B)<=w3(n)-1 over the full domain, both in Nat and in Int. No selected-side nonemptiness or saturation premise is needed.
For the original path correspondence, fix k and let i<j be the other two matching indices: (i,j)=(1,2),(0,2),(0,1) when k=0,1,2. For each x in M_k put P_x=M_i union {x} and Q_x=M_j union (M_k minus {x}). Under the abstract edge labels these are complementary three-edge paths. Injectivity of f gives card(P_x)=card(Q_x)=3, Disjoint(P_x,Q_x), and P_x union Q_x=D. Moreover P_x is disjoint from M_j, and Q_x is disjoint from M_i. The original active witnesses U_j,U_i therefore supply the two generic omission inputs, in the required orientations, within the same F. The four prescribed W_a retain their full-star equalities in this original domain; the pair estimate itself uses only the actualness, distinct-member intersection and active-core hypotheses.
Write a_x=card(F intersect Gamma(D,P_x)), b_x=card(F intersect Gamma(D,Q_x)), and t_k=sum over x in M_k of (a_x+b_x). There are exactly two complementary path pairs in this sum, because M_k has exactly two elements. Each satisfies a_x+b_x+1<=w3(n), including either or both empty selected sides. Summing these two inequalities gives t_k+2<=2w3(n). Define ell_k=2w3(n)-t_k in Nat; the preceding inequality justifies this subtraction and gives ell_k>=2. Casting the individual a_x,b_x to Int and taking the same two-term sum gives the same t_k+2<=2*w3(n) and ell_k>=2 with integer subtraction. This holds for every k in Fin(3), so all three losses are at least two simultaneously for the original single family.
A complete instance exists already at n=14. Take D={0,2,4,6,8,10} and (f00,f01,f10,f11,f20,f21)=(0,8,2,6,10,4). Use the four literal fans with (forced set,root) equal to ({0,2,10},1), ({0,4,6},5), ({2,4,8},3), ({6,8,10},7), in star order. Their forced sets are independent and their roots lie outside them. Both root neighbours lie in the corresponding forced star, so fan_triangulation gives full EarCenters equality with S_0,S_1,S_2,S_3 respectively.
For the three active cores in that instance use the literal fans ({0,8,12},2), ({2,6,12},0), ({4,10,12},0). Their exact D-traces are M_0={0,8}, M_1={2,6}, M_2={4,10}, since the possible additional ears are confined respectively to {1,3}, {13,1}, {13,1}, all outside D. All three contain the actual outside-D ear 12. Let F be exactly these seven fans. The seven D-traces are distinct, so F has seven distinct actual members. Every pair of forced sets intersects, giving full-ear intersection within this same F. Thus the four complete stars and all three active cores coexist in the original domain. Here w3(14)=1727, so for every k the conclusions are t_k+2<=3454 and ell_k>=2 in Nat and Int. This instance establishes nonvacuity without enumerating all triangulations or asserting path-count sharpness.
This application reuses the frozen normalized strict, conditioned-count, fan and ear-independence results. It requires no A>W, saturation, parity, polygon symmetry or fixed protection carrier for outside ears. It establishes the complementary-pair inequalities and all three stated path losses only; it does not establish the full B-37.7 partition or deficit and equality chains, a global maximum, n24 or Kres.
Quantitative native C20 pair bounds.
Specialize the original polygon to n=20. Take arbitrary P,Q:Finset(ZMod(20)) with Disjoint(P,Q), PolygonEarContraction.Compatible(P union Q), and card(P)=card(Q)=2. Retain arbitrary finite A:Finset(WholeFiber(P,Q)) and B:Finset(WholeFiber(Q,P)). Require every T in A and U in B to have intersecting full actual EarCenters sets. All completions and ears outside P union Q remain in scope. With Z=Npq(20,2,2)=18642420, the integer deficit Z-card(A)-card(B) is at least 2773974 if both sides are nonempty. If BOTH original cardinalities exceed 8502, that deficit is at least 3784063. The second bound has two separate cardinality hypotheses; positivity alone supplies only the first bound by this application.
Apply PolygonSimultaneousCompression.exists_original_terminal_compression once to this pair, keeping its one returned H,C,D. Here H is contained in PolygonCompressionTrace.E_K(P union Q), its ears are pairwise noncrossing, and C,D are relatively upper cross-intersecting subfamilies of powerset(H). Write w_P(X)=Nat.card(ConditionFiber(P,Q,H,X)) in Real and w_Q(X)=Nat.card(ConditionFiber(Q,P,H,X)) in Real. The original bounds are separately card(A)<=sum over X in C of w_P(X) and card(B)<=sum over X in D of w_Q(X). Nonempty A and B give nonempty C and D and nonempty H. Disjointness of P union Q from H and compatibility of their union follow from the returned E_K containment. PolygonEarContraction.compatible_card_bound gives 2*(4+card(H))<=20. Thus this same support has legal dimension 1<=d=card(H)<=6.
For every X contained in H, the identity on the actual chord set T is a bijection between ConditionFiber(P,Q,H,X) and WholeFiber(P union X,Q union (H minus X)). Its inverse recovers EarCenters(T) intersect H=X from forcing X and forbidding H minus X; it preserves the triangulation and every other ear. The two enlarged sides are disjoint and their union is compatible. PolygonConditionalCounts.conditional_card therefore gives (Nat.card(ConditionFiber(P,Q,H,X)):Int)=Npq(20,2+card(X),2+d-card(X)). Apply the same argument to Q,P separately. The reverse radial weight is identical here because p=q=2. This identifies full actual fibre counts, without assuming a radial table or a restricted collection of completions.
Define omega_d(r) in Real to be the cast of Npq(20,2+r,2+d-r) when r<=d, and zero when r>d. Npq is the signed Catalan sum defined above, including its natural subtractions and natural Catalan indices; sampled ranks always satisfy r<=d. For each legal d, omega_d(r)>=0 for every natural r, and omega_d is antitone on Iic(d). Passing from subsets X of H to finite subsets of the subtype H uses X mapped to X.subtype and the inverse image under the subtype embedding. These inverse maps preserve inclusion, intersection, complement relative to H, cardinality and rank. They turn C,D into upper cross-intersecting families on a d-element type and identify both separate original conditioned masses with m(C),m(D), where m(E)=sum over R in E of omega_d(card(R)).
The exact rows (omega_d(0),…,omega_d(d)) are (13553555,5088865) for d=1; (9861342,3692213,1396652) for d=2; (7180119,2681223,1010990,385662) for d=3; (5231460,1948659,732564,278426,107236) for d=4; (3814119,1417341,531318,201246,77180,30056) for d=5; and (2782476,1031643,385698,145620,55626,21554,8502) for d=6. In every row sum from r=0 to d of choose(d,r)*omega_d(r)=Z=18642420. The endpoint gains omega_d(0)-omega_d(d), in dimension order 1 through 6, are 8464690,8464690,6794457,5124224,3784063,2773974.
For an upper family E on this d-element type, put c_r(E)=card({R in E:card(R)=r}). The pinned Mathlib supplier Finset.local_lubell_yamamoto_meshalkin_inequality_div in Mathlib.Combinatorics.SetFamily.LYM, applied to the complemented r-slice, together with Finset.shadow_compls and inclusion of the upper shadow in the (r+1)-slice, gives c_r(E)/choose(d,r)<=c_(r+1)(E)/choose(d,r+1) for r<d. All denominators here are positive. Iteration and choose(d,r)=choose(d,d-r) give c_r(E)<=c_(d-r)(E) for 2*r<=d. This is the local LYM application on the actual support subtype, rather than a product-law assumption on triangulations.
Let flip(E)={H minus R:R in E}, interpreted on the support subtype. Rank decomposition gives m(E)=sum_r c_r(E)omega_d(r) and m(flip(E))=sum_r c_(d-r)(E)omega_d(r). For nonempty cross-intersecting upper C,D, C omits the empty set and contains the full support, so c_0(C)=0 and c_d(C)=1. Pairing ranks gives m(flip(C))-m(C)=sum over 2r<d of (c_(d-r)(C)-c_r(C))(omega_d(r)-omega_d(d-r)); the middle rank cancels. The rank cardinal gaps and antitone weights make every term nonnegative. The endpoint term yields m(flip(C))-m(C)>=omega_d(0)-omega_d(d). Cross-intersection makes flip(C) disjoint from D. Nonnegative weights then give m(flip(C))+m(D)<=Z, hence Z-m(C)-m(D)>=omega_d(0)-omega_d(d). The two original cardinal-to-mass inequalities now give the native basic deficit 2773974 over Int. This quantitative margin uses the radial counts and local LYM; original_normalized_strict alone does not supply it.
For d<=5 the endpoint gain is already at least 3784063. At d=6, the same rank pairing retains the more precise inequality m(flip(C))-m(C)>=2773974+1010089*(c_5(C)-c_1(C)), with 1010089=omega_6(1)-omega_6(5)=1031643-21554. Apply D5.S3.Combinatorics.SetFamily.CrossIntersectingLayerGap.weighted_cross_intersecting_layer_gap_of_binomial_threshold with k=0 and omega=omega_6. Its binomial threshold sum is omega_6(6)=8502. This invocation requires BOTH m(C)>8502 and m(D)>8502, and gives c_1(C)+1<=c_5(C), as well as the reverse-family gap. BOTH original inequalities card(A)>8502 and card(B)>8502 imply those respective mass hypotheses. Adding the extra 1010089 to 2773974 gives 3784063; casting back uses the original integer counts. No common support for different native pairs is required.
Conditional C20 composition in one actual family.
Keep one F:Finset(Tri20), where Tri20 is the subtype of entire finite chord sets T on ZMod(20) satisfying PolygonEarSlide.Carrier.IsTriangulation. Use the original six-edge labels E=Fin(3) times Fin(2), with (00,01,10,11,20,21) assigned to (12,34,13,24,14,23). Let f:E to ZMod(20) be any injective placement, D=image(f), m_i={(i,0),(i,1)}, M_i=image(f,m_i), q_i=E minus m_i and Q_i=D minus M_i=image(f,q_i). Require Compatible(D). Retain the original one-parity premise: there exists epsilon in Fin(2) such that (f(e)).val modulo 2=epsilon.val for every e in E. No order or symmetry of the six polygon positions is imposed.
The label stars are s_0={00,10,20}, s_1={00,11,21}, s_2={01,10,21}, s_3={01,11,20}. Take four arbitrary prescribed W_a in this same F with full EarCenters(W_a)=image(f,s_a). For all distinct T,U in F require their full EarCenters sets to intersect. Members equal to a prescribed witness are included, shared chord endpoints are allowed, and every outside-D ear of other members remains unrestricted. Define tau(T)={e in E:f(e) belongs to EarCenters(T)} and c(S)=card({T in F:tau(T)=S}). These are literal filters of this one actual F; the identity on T identifies each full trace fibre with WholeFiber(image(f,S),image(f,E minus S)).
Let Allowed={S contained in E: S meets each of s_0,s_1,s_2,s_3}. For T different from W_a, the original full-ear intersection and complete-star equality force tau(T) to meet s_a. If T=W_a, its own nonempty star gives the same conclusion directly. Exactly 41 label traces are allowed. They split into the three m_i, the three q_i, twelve paths, and U0. Here U0 consists of the four stars, the twelve four-element traces other than q_0,q_1,q_2, all six five-element traces, and E. Its rank counts for ranks zero through six are (0,0,0,4,12,6,1).
For i!=j and k the remaining matching index, define L_ij={m_i union {(k,0)},m_i union {(k,1)}}. Put a_i=card({T in F:tau(T)=m_i}), b_i=card({T in F:tau(T)=q_i}), v_ij=card({T in F:tau(T) belongs to L_ij}), and v_ii=0. For each k, let i<j be the other two indices and define G_k=L_ij union L_ji and t_k=card({T in F:tau(T) belongs to G_k}). Thus t_0=v_12+v_21, t_1=v_02+v_20, t_2=v_01+v_10. Finally u=card({T in F:tau(T) belongs to U0}). U0, the three matching traces, the three complementary traces and the three G_k are disjoint pieces partitioning Allowed, so card(F)=sum over S in Allowed of c(S)=u+sum_i a_i+sum_i b_i+sum_i t_i. In particular t_k, like the other counts, is a literal filter count of the original F, not an independent path budget.
For arbitrary forced and forbidden P,Q define Sel_F(P,Q) to contain exactly those elements of the entire native WholeFiber(P,Q) whose underlying actual triangulation belongs to F. Equivalently its cardinality is card({T in F:P contained in EarCenters(T) and Disjoint(Q,EarCenters(T))}). Set A_ij=Sel_F(M_i,M_j) and B_ij=Sel_F(M_j,M_i) for i!=j. Their label traces are exactly m_i,q_j,L_ij and m_j,q_i,L_ji respectively. Hence card(A_ij)=a_i+b_j+v_ij and card(B_ij)=a_j+b_i+v_ji. Set z_ij=card(A_ij)+card(B_ij)=a_i+a_j+b_i+b_j+v_ij+v_ji, and d_ij=18642420-z_ij in Int. These are the actual reverse-selection sums, with z_ij=z_ji. In particular z_01+z_02+z_12=2*sum_i(a_i+b_i)+sum_i t_i.
For every S contained in E, conditional_card and the identity on the full actual trace fibre give (c(S):Int)<=Npq(20,card(S),6-card(S)). Summing on U0 gives u<=4Npq(20,3,3)+12Npq(20,4,2)+6*Npq(20,5,1)+Npq(20,6,0)=34946016. Define eta=34946016-u in Int; thus eta>=0. This is a bound on the universal filters of F derived from complete conditional counts, with no fullness or saturation premise.
For the path groups use exactly the correspondence in Complementary path loss in one actual family above, specialized to n=20 and to this same f,F. For k=0,1,2, the other matching indices (i,j) are respectively (1,2),(0,2),(0,1). For b in Fin(2) let R_(k,b)=m_i union {(k,b)} and R’(k,b)=E minus R(k,b)=m_j union {(k,1-b)}. Their images P,Q partition D into compatible three-element sides. The four traces R_(k,0),R’(k,0),R(k,1),R’_(k,1) are exactly G_k. In each pair P avoids M_j and Q avoids M_i. A positive original core a_j therefore supplies an actual U in F with Disjoint(P,EarCenters(U)); a positive a_i supplies the reverse omission input. Ears of those witnesses outside D remain unrestricted.
The cited path-loss application gives card(Sel_F(P,Q))+card(Sel_F(Q,P))+1<=Npq(20,3,3)=3692213. With both sides nonempty it applies original_normalized_strict with the two equal positive complete-fibre totals. If a side is empty, retain the actual omitted completion supplied by the opposite-core witness. At n=20 this bridge can directly use PolygonPrescribedEars.prescribed_complete_ears for the compatible three-element side: a triangulation whose complete ear set is that side lies in the full fibre and is disjoint from the actual opposite-core member, so cannot belong to F. The full-ear intersection condition applies to distinct triangulations here, since the nonempty three-element complete ear set cannot equal a disjoint ear set. This is a consequence of the canonical supplier and the same-F witness, rather than an added exact-completion premise; the earlier fan/path-loss derivation need not be repeated. Either or both empty selected sides are included.
Assume all three original cores are positive: a_0,a_1,a_2>0. The two complementary path pairs for each k then have the required omission witnesses in both orientations. Their literal filter sums give t_k+2<=23692213. Define ell_k=23692213-t_k in Int. Thus ell_k>=2 simultaneously for all three k, under precisely these original core and intersection conditions. This use of path loss keeps the four arbitrary complete-star witnesses and the one-parity placement in the application domain without requiring them for the path estimate itself.
Each pair M_i,M_j is disjoint, compatible and of sizes (2,2). Every actual cross pair from A_ij,B_ij consists of distinct triangulations, since the nonempty M_i is forced on one side and forbidden on the reverse. Thus the distinct-member full-ear condition on F supplies the native pair intersection hypothesis. The inclusions of the original core filters give a_i<=card(A_ij), a_j<=card(B_ij). Therefore positive a_i,a_j imply d_ij>=2773974, and BOTH a_i>8502 and a_j>8502 imply d_ij>=3784063. Apply the native pair result separately to (0,1),(0,2),(1,2); their returned compression supports may differ. All six selections still come from the same unchanged F.
The literal partition and reverse-selection sum identity give, with all counts cast individually to Int, 2*(card(F)-69753940)=8464690-2eta-sum_i ell_i-(d_01+d_02+d_12). Indeed 2card(F)=2u+(z_01+z_02+z_12)+sum_i t_i; substitute u=34946016-eta, t_i=23692213-ell_i and z_ij=18642420-d_ij. This is a signed identity of the filters of the original F, not an assumed scalar upper bound.
Now retain an EXPLICIT actual pair i<j in Fin(3) with a_i>8502 and a_j>8502, in addition to all three a_k>0 and the original geometric, full-ear and four-complete-star hypotheses. The sum of its refined deficit and the other two basic deficits is at least 3784063+22773974=9332011. Since eta>=0 and sum_i ell_i>=6, the signed identity yields 2(card(F)-69753940)<=8464690-6-9332011=-867327. Hence 2*card(F)<=138640553; the left side is even, so it is at most 138640552 and card(F)<=69320276. This exact integer rounding is conditional on the stated actual pair and all three positive original cores.
Native omitted capacity conditionally supplies the actual large pair.
Retain exactly the same original f,D,F and four arbitrary actual complete-star witnesses W_a from Conditional C20 composition in one actual family above, its distinct-member full-ear intersection condition, its one-parity placement, and all three positive actual core counts. Also retain the original residual premise A=sum_i a_i>9861342. The only additional premise in the following implication is the explicit UNPROVED uniform omitted-capacity assumption stated below; it is a hypothesis, not a proved native fact or an axiom added to the library.
For every P contained in D with card(P)=2, define N(P)=image(p mapped to p+1,P) union image(p mapped to p-1,P), with arithmetic in ZMod(20), and B(D,P)=univ minus (D union N(P)). The parentheses exclude both D and the two neighbor images. Independent(K) means that no x in K has x+1 in K, as in PolygonConditionedFan.Independent. Let Gamma_D(P) be the entire finite set of U:Tri20 with EarCenters(U) intersect D=P, and O_D(P,J)={U in Gamma_D(P):Disjoint(EarCenters(U),J)}. These are sets of actual full triangulations, counting every different chord completion separately; ears outside D are retained without restriction except for the displayed avoidance of J.
The UNPROVED capacity premise is: for every such original P and every J inclusion-maximal among {K:K contained in B(D,P) and Independent(K)}, card(O_D(P,J))>=29205. Here J itself belongs to that finite independent-subset family, and no strict superset of J belongs to it. Maximum cardinality is not assumed, and the quantifier covers every inclusion-maximal J. Neither this premise nor the following argument assumes that Gamma_D(P) is contained in F.
For P=M_i, injectivity of the original six labels gives Q_i=image(f,E minus m_i)=D minus P, card(P)=2 and card(Q_i)=4. The identity on the actual chord set identifies Gamma_D(P) with WholeFiber(P,D minus P): its inverse recovers the exact D trace from forcing P and forbidding D minus P. Since P union (D minus P)=D is compatible, PolygonConditionalCounts.conditional_card gives card(Gamma_D(P))=Npq(20,2,4)=9861342. This application uses the compatible whole D only. It does not count by applying conditional_card to forbidden set (D minus P) union J; compatibility of that larger union is not supplied.
Fix any i. Choose j!=i and an actual V in F with tau(V)=m_j, using the positivity of that original other core, before constructing J. Thus EarCenters(V) intersect D=M_j. With P=M_i, define J0={x in EarCenters(V) minus D: for every p in P, not Cross(ear(x),ear(p))}. This is precisely all full ears of this same V outside D compatible with P. PolygonCompressionTrace.earCenters_independent makes J0 independent. PolygonCompressionTrace.cross_ear_iff_adjacent shows that its compatibility with P excludes both neighbor images N(P), so J0 is contained in B(D,P). Apply the pinned Mathlib Finset.exists_le_maximal to powerset(B(D,P)) filtered by Independent. It extends THIS J0 to an inclusion-maximal independent J inside B(D,P), with J0 contained in J. V remains the previously chosen actual member of the other core.
For any actual U in Gamma_D(P), every common full ear centre x of U and V lies in J0. Indeed x in D would lie in both P=M_i and M_j, which are disjoint. Otherwise x is an outside-D ear of V; every p in P is an ear of this same U, so its noncrossing triangulation makes ear(x) compatible with every ear(p). Separately, U!=V: equality would identify their D traces M_i and M_j, contradicting that these matching images are disjoint and nonempty. Thus distinctness holds before the distinct-member intersection condition on F is used.
Now let U belong to O_D(P,J). A common full ear of U and V would lie in J0 contained in J, contradicting Disjoint(EarCenters(U),J). Hence their full EarCenters sets are disjoint. If this actual U belonged to F, the original intersection condition applied to U!=V and the fixed V in F would contradict this disjointness. Every completion counted by O_D(P,J) is therefore omitted from this same F. The actual i-core F intersect Gamma_D(P) and O_D(P,J) are disjoint subsets of the SAME Gamma_D(P). Finite disjoint-union cardinality gives a_i+card(O_D(P,J))<=9861342. The explicit capacity premise then yields a_i<=9861342-29205=9832137, simultaneously for i=0,1,2.
If at most one of the three actual a_i exceeded 8502, their caps would give A<=9832137+2*8502=9849141<9861342, contrary to A>9861342. Consequently there are actual indices i<j in Fin(3) with both a_i>8502 and a_j>8502. This derives the pair from the original residual domain conditional on the UNPROVED capacity premise, rather than selecting independent numerical substitutes for the cores.
Insert this actual pair directly into the preceding one-family signed identity and deficit application, retaining the same F,f,W_a and three positive cores. The existing refined and basic deficits, the 41-trace partition and the complementary path losses already give 2*(card(F)-69753940)<=-867327 and card(F)<=69320276, with the integer rounding described there. Their pair-specific compression witnesses remain separate; no new common compression is required. The additional unproved assumption for this residual-to-large-pair and same-F bound is exactly the displayed native omitted-capacity bound.
Uniform native capacity remains UNPROVED, including any fixed-forest transport needed to establish it. The residual-only 69320276 target and the full original unconditional target remain open. No fullness, saturation, maximality of F, polygon symmetry, bound on other members’ complete ear-set sizes, protected E0, residual inhabitation, or common compression is assumed. These conditional mathematical consequences for native triangulations assert no stronger C0 equivalence, physical or native acquisition, readout, continuation, resource bound, literature novelty, or completion of the continuing research goal.
Original arbitrary-family maximum and unique literal-twelve equality.
Fix any n at least 14 and six distinct compatible actual ear chords e(i,b), indexed by Fin(3) times Fin(2), with the K4 edge assignment (0,0),(0,1),(1,0),(1,1),(2,0),(2,1) to 12,34,13,24,14,23. Require e to be injective, each e(i,b) to equal ear(f(i,b)) for some centre, and distinct labelled ears to be noncrossing. F is one arbitrary finite family of entire maximal noncrossing internal-chord triangulations. Only distinct members of F are required to share an ear in their complete actual ear sets. Four arbitrarily prescribed members w_j of this same F have complete ear sets exactly the images under e of the four K4 stars listed above; witness distinctness is not an additional premise. Derive NeZero(n) from n>=14. PolygonConditionedFan.ear_injective makes the centre f(i,b) unique and f injective. Set D=image(f) and M_i={f(i,0),f(i,1)}; applying ear recovers the original labelled chord sets. Complete ear sets, stars, D-traces and intersections transport by this injective image, preserving the same underlying T,F,w. Shared geometric endpoints and ears outside D are unrestricted, and no coordinate realization or exact-full-ear completion assumption is used.
For every R contained in D, Gamma_D(R) is the entire finite set of actual triangulations whose complete EarCenters set intersects D in exactly R. The corresponding chord trace is earChords(T) intersect image(e)=image(ear,R). The identity on T identifies this complete fibre first with ConditionFiber(empty,empty,D,R), then with WholeFiber(R,D minus R). Set a_i=card(F intersect Gamma_D(M_i)), A=sum_i a_i and active_count=card({i:a_i>0}). For every compatible trace R of rank r from two through six, PolygonConditionalCounts.conditional_card gives (card(Gamma_D(R)):Int)=Npq(n,r,6-r). Define w_r=toNat(Npq(n,r,6-r)); the nonnegative actual count justifies this natural conversion, so each such fibre has natural count w_r. Put W=w_2, V=w_4, H=w_3, U=4w_3+12w_4+6w_5+w_6 and L=U+W+2V+6H. Thus all sums defining L are natural counts of complete fibres. Expanding their integer casts gives L=Catalan(n-4)+6Catalan(n-5)-10Catalan(n-6)+4Catalan(n-7) in Int, with natural subtraction in the indices.
The four prescribed stars force each member of F into the same 41-trace covering table. When T equals a prescribed witness its complete star gives the required intersections directly; otherwise use the distinct-member hypothesis against that witness. The table partitions into the 23 universal traces, three matching traces, three complementary four-element traces and twelve paths. The universal traces are the four stars, all four-element subsets of D except Q_i=D minus M_i, all five-element subsets, and D itself. Let u be the selected universal count, b_i the selected count of Q_i, and t_k the total of its two prescribed complementary path pairs. Then card(F)=u+sum_i a_i+sum_i b_i+sum_i t_i, with u<=U, b_i<=V and t_i<=2H. Apply the normalized result to the actual selections from this same F in every relevant orientation. The (2,4) and (4,2) cases give a_i/W+b_i/V<=1, with equality exactly (a_i,b_i)=(W,0) or (0,V). The (3,3) cases give each complementary path-pair total at most H; equality means one complete side and the other empty. Empty selected sides retain the weak bound. Strictness is used only when both selected sides are nonempty. The (2,2) case for distinct i,j gives a_i+a_j+b_i+b_j+t_k<W+2H+V when a_i,a_j>0. The two ordered whole-fibre counts equal this last budget by the exact conditional counts, rather than by a selected-total substitution.
The count gap V<W follows from the existing conditioned trace-weight gap: force one matching, forbid another and observe the third. The empty observed trace has count W, and the full observed matching trace has count V. The nonempty-trace integer gap gives V+1<=W. Whole-fibre positivity in the source cases gives W,V,H>0; no positive-tail assumption is imposed on other trace ranks.
If A<=W, multiply and sum the three normalized inequalities to obtain VA+Wsum_i b_i<=3WV. Since W>V, this gives A+sum_i b_i<=W+2*V and therefore card(F)<=L. Equality forces A=W and equality in every normalized inequality. Their literal endpoints supply a full matching core Gamma_D(M_i) contained in F. If active_count<=2 and A>W, exactly two cores are active, and the remaining matching count is zero. The strict (2,2) budget together with the same-F partition gives card(F)<L. Thus every branch of active_count<=2 OR A<=W is included, also zero cores and three positive cores with A<=W.
A full matching core forces every original T in F to have a complete ear in that matching. This is the conditioned-fan consequence: the prescribed stars give a nonempty D-trace even when T is one of those witnesses; a disjoint completion of the matching trace would be a different member before the distinct-member intersection condition is applied. It does not require the completion to have complete ear set equal to the matching. The confined 41-trace table then excludes the other matching cores and Q_i. At card(F)=L the two complementary path pairs indexed by the elements x of M_i each have total H. The exact normalized endpoints and the actual subset/cardinality identities give one entire Gamma side and an empty opposite side for each x.
Explicitly, let j<k be the other two matching labels. The literal trace family B(i,E), for E:M_i to Bool, consists of all universal traces, M_i, Q_j,Q_k, the four traces M_i union {z} with z in D minus M_i, and for each x in M_i exactly one of M_j union {x} and M_k union (M_i minus {x}): choose the first when E(x) is true and the second when it is false. Write alpha=(i,epsilon) in Fin(3) times (Fin(2) to Bool), with E(f(i,b))=epsilon(b). Define the whole family F_alpha as the union of Gamma_D(R) over R in B(i,E); all completions and outside-D ears are retained. Under active_count<=2 OR A<=W, the confined table and the preceding equality argument give F contained in F_alpha at card(F)=L. Its natural count is L, so equality of cardinalities gives equality of the whole finite families. Every universal fibre is full, exactly one matching core is full, and the two prescribed path choices are complete. This proves the conditional equality implication on that domain; the complementary domain is handled below.
Cubic control of the same family closes the complementary domain. For disjoint compatible two-element forced sets P,Q, PolygonSimultaneousCompression.exists_original_terminal_compression supplies one common independent terminal carrier J and relatively upper cross-intersecting trace families C,D, with the original selected cardinalities bounded by their respective conditioned masses. PolygonSimultaneousCompression.common_ears_eq_trace_inter transports complete-ear cross-intersection to this carrier. Put d=card(J). The independent set P union Q union J has cardinality 4+d, hence 2*(4+d)<=n. For each X contained in J, the identity on chord sets identifies ConditionFiber(P,Q,J,X) with WholeFiber(P union X,Q union (J minus X)). Compatibility and disjointness of these enlarged sides follow from J contained in E_K(P union Q). Applying PolygonConditionalCounts.conditional_card gives the radial weight omega_r=Npq(n,r+2,d-r+2), r=card(X), in either orientation. The complete partition identity PolygonStrictNormalization.actual_partition_total, a private source lemma, sums every trace, including the empty trace, to the actual whole total s=Npq(n,2,2)>0. The passage between subsets of J and finite subsets of its subtype preserves cardinalities, order, cross-intersection and these exact masses.
Write M(l)=Catalan(l) in Real and Delta for its unit forward difference. The finite signed expansion identifies omega_r with Delta^(d-r+2) M(n-d-6). Apply CatalanDifferenceMoments.catalan_difference_ratio_envelope with L0=n-d-6 and k=d-r+1. For n>=15 and r<d, L0+k=n-r-5>=8; its lower ratio inequality gives omega_(r+1)<=5/12omega_r<=8/19omega_r. For n=14 the legal dimensions are d=0,1,2,3; the respective integer weight rows are (8502), (6071,2431), (4344,1727,704), (3114,1230,497,207), which give the same adjacent ratio inequality. Positivity follows from the same canonical difference envelope. This covers every legal terminal dimension and retains both empty selected sides and all original polygon placements.
Normalize these radial weights by their entire positive sum to a probability nu on subsets of J. Their adjacent ratio at most 8/19 makes w(r)/(8/19)^r antitone. With p=8/27, the odds p/(1-p)=8/19 turn this into the mixed lattice inequality required by the pinned Mathlib holley theorem in Mathlib.Combinatorics.SetFamily.FourFunctions. Applied to the increasing indicator of any upper event E, it gives nu(E)<=mu_p(E), where mu_p is the product Bernoulli law. The canonical Mathlib setBernoulli_eq_map and measurePreserving_arrowProdEquivProdArrow identify intersection of independent Bernoulli subsets of parameters t,u with parameter tu; measureReal_prod_prod then gives mu_(tu)(E)<=mu_t(E)*mu_u(E). Iterating at q=2/3, with q^3=p, gives mu_p(E)<=mu_q(E)^3. Reflection R mapped to J minus R, the same Holley comparison on the reflected complementary upper event, and q<=1-p give mu_q(E)<=nu(flip(E)). Cross-intersection makes C disjoint from flip(D) and D disjoint from flip(C), so nu(C)<=mu_p(C)<=mu_q(C)^3<=(1-nu(D))^3, and symmetrically for D. These are product-law and finite-sum applications of retained canonical results, with the radial and event correspondences just described; they assume no product structure for the actual triangulation law.
For each ordered i!=j let v_ij be the number of F members in the two path traces M_i union {f(k,b)}, b in Fin(2), where k is the third index. The same-F whole selection with M_i forced and M_j forbidden has cardinality a_i+b_j+v_ij; the reverse has a_j+b_i+v_ji. Their full-ear cross-intersection follows from the original distinct-member condition, since their different nonempty prescribed traces force different chord sets. Set x_ij=(a_i+b_j+v_ij)/s. The preceding cubic comparison and the terminal mass bounds give 0<=x_ij<=1 and x_ij<=(1-x_ji)^3 for all six ordered pairs. Each pair uses its own lawful terminal compression of these selections from the original F; it never substitutes an independently optimized family for F.
The exact count identity s=W+V+2H holds in Real after casting each actual count. Put uhat=W/s, bhat=V/s, khat=2H/s, abar_i=a_i/s, bbar_i=b_i/s and vbar_ij=v_ij/s. The same conditional counts and normalized endpoint bounds give 0<=abar_i<=uhat, 0<=bbar_i<=bhat, 0<=vbar_ij and vbar_ij+vbar_ji<=khat. Moreover uhat+bhat+khat=1 and bhat>0. The canonical CatalanDifferenceMoments.catalan_difference_ratio_envelope at L0=n-8 and orders two and three gives H<3V and W<3H, so uhat<9/16. All these caps belong to the same original family and the same natural counts.
Here is the scalar step using those six cubic inequalities. For nonnegative a,b,c,d,v,w with c<=a<=uhat, d<=bhat and v+w<=khat, put x=a+d+v, y=c+b+w and Z=a+b+2*(c+d+v+w). Assume x,y<=1 and x<=(1-y)^3, y<=(1-x)^3, as supplied by the two orientations above. Then x+y<=1 and Z=2*(x+y)-(a+b). If x+y<=1-uhat/2 this gives Z<=2-uhat. Otherwise, when y<=x set q0=1-x; the bounds give 0<=q0<=41/64 and Z<=2-uhat-q0*(1-2q0^2). When x<=y use q0=1-y and obtain Z<=2-uhat-bhat-q0(1-2q0^2)<2-uhat. The factor 1-2q0^2 is positive on this interval. Equality in the first low-sum case forces uhat=0 and x+y=1; the cubic constraint forces x=0 or x=1, and x=0 contradicts bhat>0 and v+w<=khat. In the remaining case equality forces q0=0, hence x=1,y=0. The caps and uhat+bhat+khat=1 then give exactly a=uhat,b=0,c=0,d=bhat,v=khat,w=0. Thus Z<=2-uhat, strictly if c>0. This scalar argument is polynomial and order normalization of the stated bounds.
Choose m with abar_m maximal and let j,k be the other two indices. Apply the scalar inequality to (a,b,c,d,v,w)=(abar_m,bbar_m,abar_j,bbar_j,vbar_mj,vbar_jm), then separately with j replaced by k. Their half-sum bounds the matching and complementary counts plus the four incident path counts by 2-uhat. The remaining pair satisfies vbar_jk+vbar_kj<=khat. Therefore the entire normalized nonuniversal count T=sum_i(abar_i+bbar_i)+sum_(i!=j)vbar_ij is at most 2-uhat+khat=uhat+2bhat+3khat. If all three a_i are positive, both incident scalar inequalities are strict, so this bound is strict. The exact 41-trace partition gives T=(card(F)-u)/s. Multiply by s>0 and use u<=U to obtain card(F)<=U+W+2V+6H=L without any activity or total-mass premise. If all three matching cores are nonempty, the same argument gives card(F)<L; integrality gives card(F)<=L-1, both in Nat and, after casting, in Int.
The cubic limit is the integer expression U_Z+Npq(n,2,4)+2Npq(n,4,2)+6Npq(n,3,3), where U_Z=4Npq(n,3,3)+12Npq(n,4,2)+6*Npq(n,5,1)+Npq(n,6,0). The actual-count casts for ranks two through six identify U_Z with the cast of U and this entire limit with the cast of L. Consequently its toNat is exactly L. Expanding the same integer expression yields the signed Catalan coefficients 1,6,-10,4 stated above. Thus the unconditional cubic bound, the natural literal-family count and the signed formula use identical labels and counts.
To classify equality, split locally on active_count<=2 OR A<=W. That branch is exactly the conditional derivation above. In its complement active_count>2; the positive-support filter is a subset of Fin(3), so its cardinality forces it to be the whole Fin(3). Each a_i>0 supplies an actual T in F intersect Gamma_D(M_i). Unfolding Gamma_D gives precisely a same-F member with earChords(T) intersect image(e)=image(e,M_i labels), so all three chord matching-core filters are nonempty. The strict cubic bound applies to this original F,e,w and contradicts card(F)=L. Core nonemptiness is derived inside this branch, not added to the original hypotheses. The strict-bound consequence itself retains its three-nonempty-cores antecedent.
Every literal F_alpha consists of valid whole triangulations, has every member meeting each prescribed star already in its D-trace, contains all four supplied w_j, and has full actual-ear intersection for all pairs. Its 32 trace rows have rank profile (1,10,14,6,1) in ranks two through six, so conditional_card and the disjoint complete-fibre union give its natural cardinality L. Its intersection with Gamma_D(M_j) is the entire matching fibre when j=alpha.1 and empty otherwise; hence exactly one core is active and its total matching count is W. Distinct indices with different matching labels differ on a rank-two fibre. For the same matching label, different Boolean choices differ on a rank-three path fibre. PolygonConditionedFan.source_conditioned_witnesses gives these separating rank-two and rank-three fibres positive cardinality through their WholeFiber correspondence. Thus alpha mapped to F_alpha is injective, and the 3*2^2=12 labelled families are distinct valid attainments containing the arbitrary prescribed witnesses. This uses no assumed saturation of an arbitrary F.
Combining forward classification, literal attainment and injectivity gives, under exactly the original hypotheses, card(F)<=L and card(F)=L if and only if there exists a unique alpha in Fin(3) times (Fin(2) to Bool) with F=F_alpha. The conclusion includes zero cores, three positive cores of either total mass, empty selected sides, shared geometric endpoints, outside-D ears and members equal to prescribed witnesses. The stronger D-trace intersection property is a conclusion for the constructed families; arbitrary F is assumed to intersect only in complete ear sets. This application is confined to maximal cyclic triangulations. It asserts no coordinate-convex C0 equivalence, stronger n20 or all-64 zero-core classification, exact-two-ear corollary, numerical capacity, physical realization, literature novelty or completion of the continuing research goal.
For arbitrary P, the strict-normalization theorem does not assert an exact completion with EarCenters(T)=P, the n-p-3 degree or rank formula, or the stronger intermediate trace and rank formula chains. The strict argument uses the two-crossing fan and FKG comparison. It gives no equality between Npq(n,p,q) and Npq(n,q,p), and no general classification outside the four ordered cases. The polygon gap and its composition are repository derivations; the generic FKG, finite-cardinality and reindexing steps are applications of pinned Mathlib results.