OAI/Combinatorics/HoneycombChords/ChordRemoval.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

Chord removal and finite partition identities

Formalized from Critical honeycomb chords with prescribed boundary endpoints (OpenAI, September 26, 2026).

  1. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.three_slots_excludes_third line 16
  2. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.isolated line 27

    Source documentation

    In a contributing center configuration, the two sides of a selected simple path occupy the full local degree. Thus all detached components are genuinely disjoint from every center on that path.

    lemma CenterPath.isolated {n : ℕ} (p : CenterPath n) (σ : Wire → Fin 3)
    (he : ∀ i, σ (p.edge i)≠1) (hn : ∀ i, centerTensor σ (p.center i)≠0)
    (i : Fin n) (k : Fin 3) (hk : incidentWire (p.center i) k∉Set.range p.edge) :
    σ (incidentWire (p.center i) k)=1 := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath, OAI.CriticalHoneycomb.Wire, OAI.CriticalHoneycomb.incidentWire

  3. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.factor_of_isolated line 45
  4. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.selected_orientation_unique line 60
  5. def OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.erase line 72
  6. def OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.fill line 75
  7. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.erased_center line 78
  8. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.erased_off line 91
  9. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.tensor_selected line 99
  10. theorem OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.remove_product line 112

    Source documentation

    Removing a forced directed chord factors its exact physical weight from the remaining center product. No independence or loop cancellation is assumed here.

    theorem CenterPath.remove_product {n : ℕ} (p : CenterPath n) (D : Finset Center)
    (σ : Wire → Fin 3) (h0 : p.point 0∉D) (hl : p.point (Fin.last (n+1))∉D)
    (he : ∀ i, σ (p.edge i)≠1) (hn : ∀ i, centerTensor σ (p.center i)≠0)
    (hroot : σ (p.edge 0)=outSpin (p.point 0) (p.side 0)) :
    centerProduct D σ=centerProduct D p.spins * centerProduct D (p.erase σ) := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath, OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.Wire, OAI.CriticalHoneycomb.Transfer.ChordOrientations.outSpin

  11. def OAI.CriticalHoneycomb.Transfer.ChordOrientations.vertexCenter line 133
  12. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.selected_to_actual line 137
  13. theorem OAI.CriticalHoneycomb.Transfer.ChordOrientations.chord_edges_of_selected_path line 164

    Source documentation

    Chord extraction remembers the literal occupied wires, so removal is not an abstraction to a different path model.

    theorem chord_edges_of_selected_path {D : Finset Center} {a b : Port (D : Set Center)}
    (γ : Chord (D : Set Center) a b) (hab : a.outside≠b.outside) (s : Wire → Bool)
    (xs : List (Interior D))
    (p : (selectedGraph a b s).Walk (.inr false) (.inr true))
    (hm : xs.map Subtype.val=γ.val)
    (hs : p.support=Sum.inr false :: (xs.map Sum.inl ++ [Sum.inr true])) :
    ∀ i, s ((ofChord γ hab).edge i)=true := by
…

    Mentions: OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Port, OAI.CriticalHoneycomb.Chord, OAI.CriticalHoneycomb.Wire, OAI.CriticalHoneycomb.Transfer.ChordOrientations.ofChord

  14. theorem OAI.CriticalHoneycomb.Transfer.ChordOrientations.nonzero_contains_selected_chord line 192

    Source documentation

    A contributing physical configuration contains an actual source chord all of whose center tensors use an isolated two-side passage.

    theorem nonzero_contains_selected_chord {D : Finset Center}
    (a b : Port (D : Set Center)) (hab : a.outside≠b.outside) (σ : Wire → Fin 3)
    (hboundary : BoundarySelection a b (selected σ)) (h : centerProduct D σ≠0) :
    ∃ γ : Chord (D : Set Center) a b,
      ∀ i, σ ((ofChord γ hab).edge i)≠1 := by
…

    Mentions: OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Port, OAI.CriticalHoneycomb.Wire, OAI.CriticalHoneycomb.Transfer.h, OAI.CriticalHoneycomb.Chord, OAI.CriticalHoneycomb.Transfer.ChordOrientations.ofChord

  15. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.fill_tensor line 210
  16. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.fill_off line 221
  17. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.tensor_empty line 229
  18. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.fill_product line 235
  19. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.erase_fill line 249
  20. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.fill_erase line 257
  21. abbrev OAI.CriticalHoneycomb.Transfer.RasterGrid.Assignment line 271
  22. def OAI.CriticalHoneycomb.Transfer.RasterGrid.assignmentSpins line 273
  23. def OAI.CriticalHoneycomb.Transfer.RasterGrid.restrictAssignment line 275
  24. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.restrictAssignment_spins line 278
  25. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.assignmentSpins_injective line 284
  26. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.assignmentSpins_supported line 289
  27. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.assignmentSpins_restrict line 293
  28. def OAI.CriticalHoneycomb.Transfer.RasterGrid.eraseAssignment line 303
  29. def OAI.CriticalHoneycomb.Transfer.RasterGrid.fillAssignment line 306
  30. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.eraseAssignment_spins line 309
  31. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.fillAssignment_spins line 316
  32. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.matches_of_occupied_eq line 324
  33. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.selected_erase_congr line 336
  34. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.selected_fill_erase line 343
  35. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.erase_eq_one line 357
  36. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.fill_eq_spins line 364
  37. def OAI.CriticalHoneycomb.Transfer.RasterGrid.HasBoundary line 378

    Source documentation

    All four literal cuts, with the prescribed boundary spin at each wire.

    def HasBoundary {W H : ℕ} (west east : Column H) (south north : Fin W → Fin 3)
    (σ : GridWire W H → Fin 3) : Prop :=
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.Column, OAI.CriticalHoneycomb.Transfer.RasterGrid.GridWire

  38. instance OAI.CriticalHoneycomb.Transfer.RasterGrid.(instance at line 383) line 383
  39. def OAI.CriticalHoneycomb.Transfer.RasterGrid.maskedTerm line 387
  40. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.maskedTerm_ne_zero line 392
  41. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.sum_subtype_indicator line 400
  42. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.sum_maskedTerm line 407

    Source documentation

    Unrestricted wires with explicit indicators. This form is suitable for an actual chord erasure bijection of nonzero tensor terms.

    theorem sum_maskedTerm {W H : ℕ} (cfg : Cell W H → Shape)
    (west east : Column H) (south north : Fin W → Fin 3) :
    (∑ x : Assignment W H, maskedTerm cfg west east south north x)=
      (kappa:ℂ)^(∑ t, (cfg t).visits) * chosenPartition cfg west east south north := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.Cell, OAI.CriticalHoneycomb.Transfer.RasterGrid.Column, OAI.CriticalHoneycomb.Transfer.RasterGrid.Assignment, OAI.CriticalHoneycomb.Transfer.RasterGrid.maskedTerm, OAI.CriticalHoneycomb.kappa, OAI.CriticalHoneycomb.Transfer.RasterGrid.chosenPartition

  43. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.boundary_erase line 437
  44. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.boundary_fill line 453
  45. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.selected_fill_congr line 475
  46. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.actual_path_factorization line 486

    Source documentation

    Factorization by removal of the actual boundary chord. cfgR is the occupancy left on deleting that chord; it has empty boundary, and is not assumed to have zero coefficient. The next step applies the already proved vacuum cancellation to it.

    theorem actual_path_factorization {W H n : ℕ} (hW : 0<W) (hH : 0<H)
    (cfg cfgR : Cell W H → Shape) (west east : Column H) (south north : Fin W → Fin 3)
    (p : CenterPath n) (x₀ : Assignment W H)
    (hx₀ : maskedTerm cfg west east south north x₀≠0)
    (hc : ∀ i, p.center i∈domain W H)
    (h0 : p.point 0∉domain W H) (hl : p.point (Fin.last (n+1))∉domain W H)
    (hcover : ∀ i, p.edge i∈Set.range (wireEmbedding (W:=W) (H:=H)))
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.Cell, OAI.CriticalHoneycomb.Transfer.RasterGrid.Column, OAI.CriticalHoneycomb.Transfer.RasterGrid.Assignment, OAI.CriticalHoneycomb.Transfer.RasterGrid.maskedTerm, OAI.CriticalHoneycomb.Transfer.RasterGrid.domain, OAI.CriticalHoneycomb.Transfer.RasterGrid.wireEmbedding

  47. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.mem_domain_iff line 586
  48. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.boundary_wire_exhaustive line 598
  49. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.assignment_boundary_selection line 654
  50. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.matches_unique line 692
  51. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.matches_empty line 700
  52. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.assignment_empty line 705
  53. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.rectanglePath_boundary line 717
  54. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.rectangle_root line 722
  55. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.nonzero_shape_is_chord line 736

    Source documentation

    The actual one-strand tensor has no contribution from detached polygons: every nonzero resolved shape is exactly one literal prescribed-port chord.

    theorem nonzero_shape_is_chord {W H : ℕ} (j k : Fin (H+1))
    (cfg : Cell (W+1) (H+1) → Shape)
    (hn : chosenPartition cfg (singleColumn j) (singleColumn k) (fun _=>1) (fun _=>1)≠0) :
    ∃ γ : RectChord W H j k, cfg=rectangleShape γ := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.Cell, OAI.CriticalHoneycomb.Transfer.RasterGrid.chosenPartition, OAI.CriticalHoneycomb.Transfer.RasterGrid.singleColumn, OAI.CriticalHoneycomb.Transfer.RasterGrid.RectChord, OAI.CriticalHoneycomb.Transfer.RasterGrid.rectangleShape

  56. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.actual_chord_sum_eq_transfer line 810

    Source documentation

    Exact finite original-source path partition. Each occupied center has weight κ; the two prescribed boundary ports are unweighted. Detached cycles cancel in the tensor contraction rather than being dropped by fiat.

    theorem actual_chord_sum_eq_transfer {W H : ℕ} (j k : Fin (H+1)) :
    (prescribedPartition (W+1) (H+1) (singleColumn j) (singleColumn k) (fun _=>1) (fun _=>1)) =
      ∑ γ : RectChord W H j k, (kappa:ℂ)^γ.val.length := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.prescribedPartition, OAI.CriticalHoneycomb.Transfer.RasterGrid.singleColumn, OAI.CriticalHoneycomb.Transfer.RasterGrid.RectChord, OAI.CriticalHoneycomb.kappa

  57. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.actual_chordMass_eq_transfer line 839

    Source documentation

    The ENNReal mass defined directly from the literal path subtype agrees with the finite physical transfer entry. This is finite identification only; no uniform bound in width or infinite-strip asymptotic is assumed.

    theorem actual_chordMass_eq_transfer {W H : ℕ} (j k : Fin (H+1)) :
    chordMass (domain (W+1) (H+1) : Set Center) (westPort W H j) (eastPort W H k) =
      ENNReal.ofReal (prescribedPartition (W+1) (H+1)
        (singleColumn j) (singleColumn k) (fun _=>1) (fun _=>1)).re := by
…

    Mentions: OAI.CriticalHoneycomb.chordMass, OAI.CriticalHoneycomb.Transfer.RasterGrid.domain, OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.Transfer.RasterGrid.westPort, OAI.CriticalHoneycomb.Transfer.RasterGrid.eastPort, OAI.CriticalHoneycomb.Transfer.RasterGrid.prescribedPartition, OAI.CriticalHoneycomb.Transfer.RasterGrid.singleColumn