ForestGeometry.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The independent-direction obstruction to an incidence cycle

A hypothetical simple cycle of line and point vertices uses each line once. Its successive point differences lie along distinct independent directions. Telescoping around the cycle forces every difference to vanish, contradicting distinct adjacent points. This is the algebraic acyclicity step in q:forest-code.

theorem OAI.TwoPointCorrelations.independent_directions_closed_chain line 20

theorem OAI.TwoPointCorrelations.independent_lines_cycle_degenerate line 31

Source documentation

Distinct independent line directions cannot support a nontrivial closed polygon, regardless of where the affine lines are based.

theorem independent_lines_cycle_degenerate {K ι V : Type*} [Field K]
    [Fintype ι] [AddCommGroup V] [Module K V]
    (d : ι → V) (hd : LinearIndependent K d) (anchor p : ι → V)
    (next : Equiv.Perm ι)
    (hincidence : ∀ i, ∃ s t : K,
      p i = anchor i + s • d i ∧ p (next i) = anchor i + t • d i) :
    ∀ i, p (next i) = p i := by
…