Left-Side Bound for Cap Edges Witnessed at One Vertex
ProvedProblem97.CGN.card_witnessedPairsAt_le_leftcap-witnessconvex-geometryerdos-97-96-countinglean-formalizationpartial-matching
Fix a vertex j of an ordered cap with m vertices. If, for every earlier endpoint r, two witnessed cap edges from r through j must have the same later endpoint, then the number of cap-index pairs witnessed at j is at most the index value of j.
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.card_witnessedPairsAt_le_left {m : ℕ} (L : OrderedCap m) (j : Fin m)
(hleft : ∀ {r s t : Fin m}, WitnessesCapEdgeAt L j r s →
WitnessesCapEdgeAt L j r t → s = t) :
(WitnessedPairsAt L j).card ≤ j.val := by sorrySource