Ordered Cap Edges Determine Their Index Pairs
ProvedProblem97.CGN.edgeAt_injective_on_CapIndexPairscap-edgeconvex-geometryerdos-97-96-countinginjectivitylean-formalization
For an ordered cap L, two oriented index pairs r < s and u < v that determine the same unordered two-vertex edge must be the same ordered pair of indices.
Preamble
/- Generated theorem stub from Erdos9796Proof.P97.CGN.CGN by Stage 2 proof cut; source SHA-256 9f1ccd7df30637d7fbdf412fb40177dedb5193c45ec2993df86f137cbd34ffb7 -/
import Definitions.Def_Erdos9796Counting_Adapter
import Definitions.Def_Erdos9796Counting_CGN_CGN
import Definitions.Def_Erdos9796Counting_Foundation
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.Powerset
import Mathlib.Data.Fintype.BigOperators
import Mathlib.Order.Interval.Finset.Fin
open Problem97 Problem97.CGN
/-!
# CGN7: indexed cap-side witness matching scaffold
This file records the CGN7-local indexed witness relation requested by the
updated counterexample-card-ge-nine prose. The geometry that produces the
one-sided injectivity hypotheses lives in the CGN6 lemmas; this module only
packages the ordered-cap interface and the partial-matching counting shell.
-/
open scoped EuclideanGeometry
open scoped InnerProductSpace
open Finset
variable {m : ℕ}Formal statement
theorem Problem97.CGN.edgeAt_injective_on_CapIndexPairs {m : ℕ} {L : OrderedCap m}
{p q : Fin m × Fin m} (hp : p ∈ CapIndexPairs m) (hq : q ∈ CapIndexPairs m)
(heq : edgeAt L p.1 p.2 = edgeAt L q.1 q.2) :
p = q := by sorrySource