Complete exact traces and conditioned fibres

Abstract

Actual polygon condition preserving ear slide

Definition 1.1 (All ears of the actual chord set).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall T\in \mathrm{Finset}\left(Sym2\left(\mathrm{ZMod}\left(n\right)\right)\right),\forall i\in \mathrm{ZMod}\left(n\right),((i\in \mathrm{EarCenters}\left(T\right))⟺(\mathrm{ear}\left(i\right)\in T))$$

Formalization. D5/S3/Geometry/Polygons/PolygonEarSlide.EarCenters (✓ std3).

Source. Repository-derived.

Commentary.

Every ear of the complete finite chord set is observed.

Definition 1.2 (Common compatible ear carrier).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall K\in \mathrm{Finset}\left(\mathrm{ZMod}\left(n\right)\right),\forall i\in \mathrm{ZMod}\left(n\right),((i\in \mathrm{EK}\left(K\right))⟺(\neg ((i\in K))\wedge (\forall k\in \mathrm{ZMod}\left(n\right),((k\in K)⟹\neg (\mathrm{Cross}\left(\mathrm{ear}\left(i\right),\mathrm{ear}\left(k\right)\right))))))$$

Formalization. D5/S3/Geometry/Polygons/PolygonEarSlide.E_K (✓ std3).

Source. Repository-derived.

Commentary.

EK denotes E_K: centres outside K whose ears cross no ear of K.

Definition 1.3 (Complete conditioned exact-trace fibre).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall P\in \mathrm{Finset}\left(\mathrm{ZMod}\left(n\right)\right),\forall Q\in \mathrm{Finset}\left(\mathrm{ZMod}\left(n\right)\right),\forall J\in \mathrm{Finset}\left(\mathrm{ZMod}\left(n\right)\right),\forall X\in \mathrm{Finset}\left(\mathrm{ZMod}\left(n\right)\right),(\mathrm{ConditionFiber}\left(P,Q,J,X\right)=\{T:\mathrm{Finset}\left(Sym2\left(\mathrm{ZMod}\left(n\right)\right)\right)|(\mathrm{IsTriangulation}\left(T\right)\wedge ((P\subseteq \mathrm{EarCenters}\left(T\right))\wedge (\mathrm{Disjoint}\left(Q,\mathrm{EarCenters}\left(T\right)\right)\wedge (\mathrm{inter}\left(\mathrm{EarCenters}\left(T\right),J\right)=X))))\})$$

Formalization. D5/S3/Geometry/Polygons/PolygonEarSlide.ConditionFiber (✓ std3).

Source. Repository-derived.

Commentary.

P is forced, Q is forbidden, and the entire observed J trace equals X. The subtype includes infeasible empty fibres.

Theorem 1.4 (Cyclic translation of all triangulations).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall T\in \mathrm{Finset}\left(Sym2\left(\mathrm{ZMod}\left(n\right)\right)\right),\forall a\in \mathrm{ZMod}\left(n\right),(\mathrm{IsTriangulation}\left(T\right)⟹\mathrm{IsTriangulation}\left(\mathrm{shiftChords}\left(T,a\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/Geometry/Polygons/PolygonEarSlide.isTriangulation_map_add (✓ std3). ∎

Source. Repository-derived.

Commentary.

shiftChords(T,a) is the finite image of T under the chord map x -> x+a. Diagonal, noncrossing, and maximality conditions are preserved.

Theorem 1.5 (Forward exact observed-ear trace).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall T\in \mathrm{Finset}\left(Sym2\left(\mathrm{ZMod}\left(n\right)\right)\right),\forall J\in \mathrm{Finset}\left(\mathrm{ZMod}\left(n\right)\right),\forall R\in \mathrm{Finset}\left(\mathrm{ZMod}\left(n\right)\right),((14\le n)⟹(\mathrm{IsTriangulation}\left(T\right)⟹((\mathrm{ear}\left(2\right)\in T)⟹(\neg ((0\in J))⟹((1\in J)⟹((2\in J)⟹((R\subseteq \mathrm{erase}\left(\mathrm{erase}\left(\mathrm{erase}\left(J,1\right),2\right),3\right))⟹((\mathrm{inter}\left(\mathrm{EarCenters}\left(T\right),J\right)=\mathrm{insert}\left(2,R\right))⟹(\mathrm{inter}\left(\mathrm{EarCenters}\left(\mathrm{phi}\left(T\right)\right),\mathrm{erase}\left(\mathrm{erase}\left(J,2\right),3\right)\right)=\mathrm{insert}\left(1,R\right))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Geometry/Polygons/PolygonEarSlide.trace_phi (✓ std3). ∎

Source. Repository-derived.

Commentary.

J omits 0 and includes 1,2. R is supported on J with 1,2,3 erased. The output retains exactly R and centre 1 on J with 2,3 erased.

Theorem 1.6 (Inverse exact observed-ear trace).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall T\in \mathrm{Finset}\left(Sym2\left(\mathrm{ZMod}\left(n\right)\right)\right),\forall J\in \mathrm{Finset}\left(\mathrm{ZMod}\left(n\right)\right),\forall R\in \mathrm{Finset}\left(\mathrm{ZMod}\left(n\right)\right),((14\le n)⟹(\mathrm{IsTriangulation}\left(T\right)⟹((\mathrm{ear}\left(1\right)\in T)⟹(\neg ((0\in J))⟹((1\in J)⟹((2\in J)⟹((R\subseteq \mathrm{erase}\left(\mathrm{erase}\left(\mathrm{erase}\left(J,1\right),2\right),3\right))⟹((\mathrm{inter}\left(\mathrm{EarCenters}\left(T\right),\mathrm{erase}\left(\mathrm{erase}\left(J,2\right),3\right)\right)=\mathrm{insert}\left(1,R\right))⟹(\mathrm{inter}\left(\mathrm{EarCenters}\left(\mathrm{psi}\left(T\right)\right),J\right)=\mathrm{insert}\left(2,R\right))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Geometry/Polygons/PolygonEarSlide.trace_psi (✓ std3). ∎

Source. Repository-derived.

Commentary.

The same complete J-origin, membership and R-support hypotheses recover exactly R and centre 2 on the original J.

Theorem 1.7 (Normalized complete conditioned fibre equivalence).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall P\in \mathrm{Finset}\left(\mathrm{ZMod}\left(n\right)\right),\forall Q\in \mathrm{Finset}\left(\mathrm{ZMod}\left(n\right)\right),\forall J\in \mathrm{Finset}\left(\mathrm{ZMod}\left(n\right)\right),\forall R\in \mathrm{Finset}\left(\mathrm{ZMod}\left(n\right)\right),((14\le n)⟹((J\subseteq \mathrm{EK}\left((P\cup Q)\right))⟹(\neg ((0\in J))⟹((1\in J)⟹((2\in J)⟹((R\subseteq \mathrm{erase}\left(\mathrm{erase}\left(\mathrm{erase}\left(J,1\right),2\right),3\right))⟹\mathrm{Equiv}\left(\mathrm{ConditionFiber}\left(P,Q,J,\mathrm{insert}\left(2,R\right)\right),\mathrm{ConditionFiber}\left(P,Q,\mathrm{erase}\left(\mathrm{erase}\left(J,2\right),3\right),\mathrm{insert}\left(1,R\right)\right)\right)))))))$$

Proof. Machine-checked in Lean as D5/S3/Geometry/Polygons/PolygonEarSlide.condition_fibre_equiv (✓ std3). ∎

Source. Repository-derived.

Commentary.

J lies in E_K(P union Q), omits 0 and contains 1,2; R lies in J with 1,2,3 erased. All forced and forbidden conditions are preserved. No cardinality, P/Q disjointness or compatibility premise is needed for this local equivalence.

Theorem 1.8 (Complete fibre equivalence at every cyclic origin).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall P\in \mathrm{Finset}\left(\mathrm{ZMod}\left(n\right)\right),\forall Q\in \mathrm{Finset}\left(\mathrm{ZMod}\left(n\right)\right),\forall J\in \mathrm{Finset}\left(\mathrm{ZMod}\left(n\right)\right),\forall R\in \mathrm{Finset}\left(\mathrm{ZMod}\left(n\right)\right),\forall a\in \mathrm{ZMod}\left(n\right),((14\le n)⟹((J\subseteq \mathrm{EK}\left((P\cup Q)\right))⟹(\neg ((a\in J))⟹(((a+1)\in J)⟹(((a+2)\in J)⟹((R\subseteq \mathrm{erase}\left(\mathrm{erase}\left(\mathrm{erase}\left(J,(a+1)\right),(a+2)\right),(a+3)\right))⟹\mathrm{Equiv}\left(\mathrm{ConditionFiber}\left(P,Q,J,\mathrm{insert}\left((a+2),R\right)\right),\mathrm{ConditionFiber}\left(P,Q,\mathrm{erase}\left(\mathrm{erase}\left(J,(a+2)\right),(a+3)\right),\mathrm{insert}\left((a+1),R\right)\right)\right)))))))$$

Proof. Machine-checked in Lean as D5/S3/Geometry/Polygons/PolygonEarSlide.condition_fibre_equiv_at (✓ std3). ∎

Source. Repository-derived.

Commentary.

Conjugation by cyclic translation includes every origin a, the cyclic seam, and empty fibres. The cardinality theorem in PolygonEarSlideCardinality uses this equivalence to count the complete fibres.

References

• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlide.ConditionFiber
• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlide.E_K
• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlide.EarCenters
• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlide.condition_fibre_equiv
• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlide.condition_fibre_equiv_at
• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlide.isTriangulation_map_add
• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlide.trace_phi
• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlide.trace_psi
• Dependency: D5/S3/Geometry/Polygons/PolygonEarSlideMaps