Actual flat face components

Abstract

Native logarithmic budgets, saturated actual quotient support and genuine endpoints.

T is any finite tetrahedron type and p:EdgeStarTransitions.RawFacePairing(T) is one actual whole-face pairing. Occ=T times Fin(6), E=p.GlobalEdge is exactly the quotient by the equivalence relation generated by p.edgeStep, and P(t,q)=p.edgeLabel(t,q). The local order is (12,13,14,34,24,23), with opposite pairs (0,3),(1,4),(2,5). No coloring, face normal orientation, injectivity of local labels or exclusion of self-gluing is assumed. In the original source, p is the fixed ideal triangulation of the compact connected orientable 3-manifold with nonempty boundary of genus at least two. The conclusions here hold for every finite raw pairing, so no additional manifold property is used.

One function ell:E->Real supplies all block coordinates x(t,q)=cosh(ell(P(t,q))) and angles alpha(t,q)=TwoLengthAngleSum.extendedAngle(x(t),q). Flat(t) means that x(t) is in one of the three closed native sectors from PositiveFlatClassification.positive_classification. Thus F=flats(p,ell) is derived from the original formula, with its unique opposite pi pair and four zero angles. Outside F every angle is strictly between zero and pi when ell is positive. The source global angle equation AngleSums is sum over all occurrences in each P fiber equals 2*pi. Degree d(e) is the full fiber cardinality.

For any finite C subset T, n(C,e) counts all occurrences with block in C and global label e; m(C,e) counts those same occurrences whose actual angle is pi. Repeated labels retain their multiplicity. FaceStep(t,u) means both blocks are flat and some actual p.facePair sends a face of t to a face of u. SameFlatComponent includes flatness at both ends and the generated equivalence relation. component(t) is its finite class. These face components are not defined using the pi graph.

RestrictedFlatEdgeChain(p,ell,i,j) abbreviates EqvGen of the relation p.edgeStep(u,v) together with Flat(p,ell,u.fst) and Flat(p,ell,v.fst), from i to j. Endpoint(p,ell,C,e) means that some occurrence i has i.fst in C, P(i)=e and alpha(i)=pi, that the global m(F,e)=1, and that some occurrence j has P(j)=e with j.fst outside Flat. The classifier makes that last block genuine. All weighted coefficients and cardinalities in real sums use their real casts.

The information-escape audits for m_le_two, saturated_support, native_component_budget, genuine_of_single_pi, component_exposed_label and component_endpoints remain unfinished under https://github.com/the-omega-institute/trureturing/issues/17994. The universal native_component_budget family has compiled proof evidence, but its source registration remains blocked by the rigid-universe decoder. The other five audits lack complete variation, sensitivity, observational-dependence and admissible source-selection evidence. The issue supplies neither mathematical proof nor validated registration status.

Theorem 1.1 (At most two flat pi contributions).

$\forall T \in T y p e, [F in t y p e (T)], \forall p \in R a wF a ce P ai r in g (T), e ll \in F u n c t i o n (Gl o ba lE d g e (p), R e a l), C \in F in se t (T), e \in Gl o ba lE d g e (p), A n g l e S u m s (p, e ll) \Rightarrow m (p, e ll, C, e) \leq 2$

Proof. Machine-checked in Lean as D5/S3/Geometry/Hyperideal/FlatComponentBudget.m_le_two (✓ std3). ∎

Source. Repository-derived.

Commentary.

Nonnegative native angles and the actual global 2*pi sum bound the sum on the pi occurrence subset. That subset sum is exactly m(C,e)*pi.

Theorem 1.2 (Saturation restricts actual quotient support).

$\forall T \in T y p e, [F in t y p e (T)], \forall p \in R a wF a ce P ai r in g (T), e ll \in F u n c t i o n (Gl o ba lE d g e (p), R e a l), e \in Gl o ba lE d g e (p), i \in P ro d u c t (T, F in (6)), j \in P ro d u c t (T, F in (6)), (((((\forall e \in Gl o ba lE d g e (p), 0 < v a l u e (e ll, e)) \land A n g l e S u m s (p, e ll)) \land m (p, e ll, f l a t s (p, e ll), e) = 2) \land l ab e l (p, i) = e) \land l ab e l (p, j) = e) \Rightarrow (R es t r i c t e d Fl a tE d g e C hain (p, e ll, i, j) \land S am e Fl a tC o m p o n e n t (p, e ll, f s t (i), f s t (j)))$

Proof. Machine-checked in Lean as D5/S3/Geometry/Hyperideal/FlatComponentBudget.saturated_support (✓ std3). ∎

Source. Repository-derived.

Commentary.

If the global flat pi multiplicity is two, these two pi contributions exhaust the actual 2*pi sum. A genuine occurrence would contribute a strictly positive angle, so every occurrence in the entire quotient fiber is flat. Equality in the actual quotient supplies an EqvGen edgeStep chain. Induction retains its common global label, hence every intermediate block is flat. Projecting each paired-face edge step gives the actual flat face chain. This derives restricted support; it is not a saturation certificate premise.

Theorem 1.3 (Native budget on every nonempty flat subset).

$\forall T \in T y p e, [F in t y p e (T)], \forall p \in R a wF a ce P ai r in g (T), e ll \in F u n c t i o n (Gl o ba lE d g e (p), R e a l), C \in F in se t (T), (((\forall e \in Gl o ba lE d g e (p), 0 < v a l u e (e ll, e)) \land (\forall t \in T, m e mb er (t, C) \Rightarrow Fl a t (p, e ll, t))) \land N o n e m pt y (C)) \Rightarrow c a r d (C) \cdot l o g (16) + 2 \cdot e \in Gl o ba lE d g e (p) \sum m (p, e ll, C, e) \cdot correc t i o n (p, e ll, e) \leq e \in Gl o ba lE d g e (p) \sum (3 \cdot m (p, e ll, C, e) - n (p, e ll, C, e)) \cdot w e i g h t (p, e ll, e) \land c a r d (C) \cdot l o g (16) < e \in Gl o ba lE d g e (p) \sum (3 \cdot m (p, e ll, C, e) - n (p, e ll, C, e)) \cdot w e i g h t (p, e ll, e)$

Proof. Machine-checked in Lean as D5/S3/Geometry/Hyperideal/FlatComponentBudget.native_component_budget (✓ std3). ∎

Source. Repository-derived.

Commentary.

Set w(e)=log(cosh(ell(e))) and h(e)=log(cosh(ell(e))/(cosh(ell(e))-1)). Sum PositiveFlatClassification.native_flat_budget after the actual six-slot frame permutation on each block in C. Fiberwise finite sum regrouping gives the coefficient 3*m(C,e)-n(C,e) and retains both positive pi correction contributions per block. The inequality is strict above card(C)*log(16). No supplied local or component budget is used.

Theorem 1.4 (A single flat pi label touches a genuine block).

$\forall T \in T y p e, [F in t y p e (T)], \forall p \in R a wF a ce P ai r in g (T), e ll \in F u n c t i o n (Gl o ba lE d g e (p), R e a l), e \in Gl o ba lE d g e (p), (((\forall e \in Gl o ba lE d g e (p), 0 < v a l u e (e ll, e)) \land A n g l e S u m s (p, e ll)) \land m (p, e ll, f l a t s (p, e ll), e) = 1) \Rightarrow (\exists i \in P ro d u c t (T, F in (6)), l ab e l (p, i) = e \land (\neg Fl a t (p, e ll, f s t (i))))$

Proof. Machine-checked in Lean as D5/S3/Geometry/Hyperideal/FlatComponentBudget.genuine_of_single_pi (✓ std3). ∎

Source. Repository-derived.

Commentary.

If every occurrence were flat, the native pi/zero classification would make the global angle sum exactly onepi. This contradicts 2pi. The occurrence outside Flat is genuine by the full positive-domain classifier.

Theorem 1.5 (One coefficient witness in each actual component).

$\forall T \in T y p e, [F in t y p e (T)], \forall p \in R a wF a ce P ai r in g (T), e ll \in F u n c t i o n (Gl o ba lE d g e (p), R e a l), t \in T, ((((\forall e \in Gl o ba lE d g e (p), 0 < v a l u e (e ll, e)) \land A n g l e S u m s (p, e ll)) \land (\forall e \in Gl o ba lE d g e (p), 6 \leq d e g ree (p, e))) \land Fl a t (p, e ll, t)) \Rightarrow (\exists e \in Gl o ba lE d g e (p), ((m (p, e ll, f l a t s (p, e ll), e) = 1 \land m (p, e ll, co m p o n e n t (p, e ll, t), e) = 1) \land n (p, e ll, co m p o n e n t (p, e ll, t), e) \leq 2) \land (\exists i \in P ro d u c t (T, F in (6)), l ab e l (p, i) = e \land (\neg Fl a t (p, e ll, f s t (i)))))$

Proof. Machine-checked in Lean as D5/S3/Geometry/Hyperideal/FlatComponentBudget.component_exposed_label (✓ std3). ∎

Source. Repository-derived.

Commentary.

The strictly positive component budget gives a positive coefficient. If its global m were two, saturated support would put the entire fiber in this actual component, giving n=d>=6 and coefficient 3*2-d<=0. Hence its global and local m are one, and its local n is at most two. The single-pi result gives a genuine occurrence. The n<=2 assertion concerns this coefficient witness only.

Theorem 1.6 (Two distinct globally single pi labels per component).

$\forall T \in T y p e, [F in t y p e (T)], \forall p \in R a wF a ce P ai r in g (T), e ll \in F u n c t i o n (Gl o ba lE d g e (p), R e a l), t \in T, ((((\forall e \in Gl o ba lE d g e (p), 0 < v a l u e (e ll, e)) \land A n g l e S u m s (p, e ll)) \land (\forall e \in Gl o ba lE d g e (p), 6 \leq d e g ree (p, e))) \land Fl a t (p, e ll, t)) \Rightarrow (\exists a \in Gl o ba lE d g e (p), \exists b \in Gl o ba lE d g e (p), (a \neq = b \land E n d p o in t (p, e ll, co m p o n e n t (p, e ll, t), a)) \land E n d p o in t (p, e ll, co m p o n e n t (p, e ll, t), b))$

Proof. Machine-checked in Lean as D5/S3/Geometry/Hyperideal/FlatComponentBudget.component_endpoints (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every flat block contributes precisely two pi occurrences. In a component, sum_e m(C,e)=2*card(C). Saturated support shows that any local m=1 is globally one. Splitting local multiplicities into zero, one and two makes the number of labels with local m=1 even. The coefficient witness makes this number positive, hence at least two. Both labels have actual pi occurrences in C and genuine occurrences globally. No n<=2 claim is made for both labels, and this parity argument does not assert that all pi graph components are paths.

References

Truth anchor: D5/S3/Geometry/Hyperideal/FlatComponentBudget.component_endpoints
Truth anchor: D5/S3/Geometry/Hyperideal/FlatComponentBudget.component_exposed_label
Truth anchor: D5/S3/Geometry/Hyperideal/FlatComponentBudget.genuine_of_single_pi
Truth anchor: D5/S3/Geometry/Hyperideal/FlatComponentBudget.m_le_two
Truth anchor: D5/S3/Geometry/Hyperideal/FlatComponentBudget.native_component_budget
Truth anchor: D5/S3/Geometry/Hyperideal/FlatComponentBudget.saturated_support
Dependency: D5/S3/Geometry/Hyperideal/EdgeStarTransitions
Dependency: D5/S3/Geometry/Hyperideal/PositiveFlatClassification

Keyboard shortcuts

trureturing — Discovering truth

Actual flat face components

Abstract

References