Documentation

LeanPool.BrillNoetherGraphs.Utilities.Subdivision.AffinePosition

Affine-described positions on a subdivided slot #

This is the small bridge between a passive affine certificate and the dependent PathPosition type of a concrete subdivision. A code names a slot, an affine offset measured from one of its endpoints, and a direction. The certificate contains no proofs: the two rows asserting that the offset lies in its slot are required literally in its local cone. Cone soundness then supplies the bounds needed to construct a typed path position.

source
structure MarkedGraphs.Certificate.AffinePosition.Code (m p : ℕ) :
Type

Passive name for a point on a slot. fromHead = true reads offset from the head, so its tail-oriented coordinate is length - offset.

  • edge : Fin p

    The core slot containing the affine-coded position.

  • fromHead : Bool

    Whether the offset is measured from the slot's head; otherwise it is measured from the tail.

  • offset : Utilities.Certificate.ExplicitPotential.AffineForm m

    The affine expression for the distance from the selected endpoint, with bounds checked separately.

Instances For
    source
    def MarkedGraphs.Certificate.AffinePosition.Code.lowerRow {m p : ℕ} (code : Code m p) :
    Utilities.Certificate.ExplicitPotential.AffineForm m

    The lower-bound row for a position code.

    Equations
    Instances For
      source
      def MarkedGraphs.Certificate.AffinePosition.Code.upperRow {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) :
      Utilities.Certificate.ExplicitPotential.AffineForm m

      The upper-bound row for a position code on a particular certificate.

      Equations
      Instances For
        source
        def MarkedGraphs.Certificate.AffinePosition.Code.BoundsCertified {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) :
        Prop

        The local cone explicitly contains the two rows which say that the offset is between zero and the length of its named slot.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def MarkedGraphs.Certificate.AffinePosition.Code.checkRow {m : ℕ} (form : Utilities.Certificate.ExplicitPotential.AffineForm m) (cone : List (Utilities.Certificate.ExplicitPotential.AffineForm m)) :
          Bool

          Proof-free check that one required bound row is either identically zero or literally present in the local cone.

          Equations
          Instances For
            source
            @[simp]
            theorem MarkedGraphs.Certificate.AffinePosition.Code.checkRow_eq_true_iff {m : ℕ} (form : Utilities.Certificate.ExplicitPotential.AffineForm m) (cone : List (Utilities.Certificate.ExplicitPotential.AffineForm m)) :
            checkRow form cone = true ↔ form = 0 ∨ form ∈ cone
            source
            def MarkedGraphs.Certificate.AffinePosition.Code.checkBounds {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) :
            Bool

            Executable fail-closed bounds check for an affine position code.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem MarkedGraphs.Certificate.AffinePosition.Code.checkBounds_eq_true_iff {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) :
              checkBounds certificate code = true ↔ BoundsCertified certificate code
              source
              def MarkedGraphs.Certificate.AffinePosition.Code.rawOffset {m p : ℕ} (code : Code m p) (point : Fin m → ℤ) :
              ℕ

              The raw natural offset recovered from an integral affine evaluation.

              Equations
              Instances For
                source
                theorem MarkedGraphs.Certificate.AffinePosition.Code.offset_nonneg {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) :
                0 ≤ Utilities.Certificate.AffineCover.AffineForm.eval code.offset point

                Cone-certified offsets evaluate nonnegatively.

                source
                theorem MarkedGraphs.Certificate.AffinePosition.Code.offset_le_segment_eval {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) :
                Utilities.Certificate.AffineCover.AffineForm.eval code.offset point ≤ Utilities.Certificate.AffineCover.AffineForm.eval (certificate.segment code.edge) point

                Cone-certified offsets do not exceed their named segment length.

                source
                theorem MarkedGraphs.Certificate.AffinePosition.Code.rawOffset_cast {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) :
                ↑(code.rawOffset point) = Utilities.Certificate.AffineCover.AffineForm.eval code.offset point

                At a certified point, coercing the raw offset back to ℤ recovers its affine value exactly.

                source
                theorem MarkedGraphs.Certificate.AffinePosition.Code.rawOffset_le_segmentNat {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) {degree : ℤ} (hValid : certificate.Valid degree) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) :
                code.rawOffset point ≤ certificate.segmentNat point code.edge

                The raw natural offset is bounded by the concrete subdivision length.

                source
                def MarkedGraphs.Certificate.AffinePosition.Code.coordinate {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) :
                ℕ

                Tail-oriented numerical coordinate of a code in the concrete subdivision.

                Equations
                Instances For
                  source
                  theorem MarkedGraphs.Certificate.AffinePosition.Code.coordinate_le_segmentNat {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) {degree : ℤ} (hValid : certificate.Valid degree) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) :
                  coordinate certificate code point ≤ certificate.segmentNat point code.edge

                  The orientation-normalized coordinate lies on its named slot.

                  source
                  def MarkedGraphs.Certificate.AffinePosition.Code.decodePosition {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) (core_nonempty : 0 < n) {degree : ℤ} (hValid : certificate.Valid degree) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) :
                  (certificate.subdivisionSpec point core_nonempty hValid hCone).PathPosition code.edge

                  Typed path position decoded from a cone-certified affine position.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def MarkedGraphs.Certificate.AffinePosition.Code.decodeVertex {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) (core_nonempty : 0 < n) {degree : ℤ} (hValid : certificate.Valid degree) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) :
                    (certificate.subdivisionSpec point core_nonempty hValid hCone).Vertex

                    The actual subdivision vertex named by an affine position code.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[simp]
                      theorem MarkedGraphs.Certificate.AffinePosition.Code.decodePosition_val {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) (core_nonempty : 0 < n) {degree : ℤ} (hValid : certificate.Valid degree) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) :
                      ↑(decodePosition certificate code point core_nonempty hValid hBounds hCone) = coordinate certificate code point
                      source
                      theorem MarkedGraphs.Certificate.AffinePosition.Code.decodePosition_val_of_fromHead_false {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) (core_nonempty : 0 < n) {degree : ℤ} (hValid : certificate.Valid degree) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) (hDirection : code.fromHead = false) :
                      ↑(decodePosition certificate code point core_nonempty hValid hBounds hCone) = code.rawOffset point

                      Tail-oriented codes retain their raw coordinate.

                      source
                      theorem MarkedGraphs.Certificate.AffinePosition.Code.decodePosition_val_of_fromHead_true {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) (core_nonempty : 0 < n) {degree : ℤ} (hValid : certificate.Valid degree) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) (hDirection : code.fromHead = true) :
                      ↑(decodePosition certificate code point core_nonempty hValid hBounds hCone) = certificate.segmentNat point code.edge - code.rawOffset point

                      Head-oriented codes use the complementary tail coordinate.

                      source
                      theorem MarkedGraphs.Certificate.AffinePosition.Code.decodePosition_eq_pathPosition_of_fromHead_false {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) (core_nonempty : 0 < n) {degree : ℤ} (hValid : certificate.Valid degree) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) (hDirection : code.fromHead = false) :
                      decodePosition certificate code point core_nonempty hValid hBounds hCone = (certificate.subdivisionSpec point core_nonempty hValid hCone).pathPosition code.edge (code.rawOffset point) ⋯

                      Tail-oriented decoding is definitionally the ordinary bounded path position constructor.

                      source
                      theorem MarkedGraphs.Certificate.AffinePosition.Code.decodePosition_isInterior {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) (core_nonempty : 0 < n) {degree : ℤ} (hValid : certificate.Valid degree) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) (hPositive : 0 < coordinate certificate code point) (hStrict : coordinate certificate code point < certificate.segmentNat point code.edge) :
                      (certificate.subdivisionSpec point core_nonempty hValid hCone).IsInteriorPosition code.edge (decodePosition certificate code point core_nonempty hValid hBounds hCone)

                      A decoded position is interior whenever its normalized coordinate is strictly between the two endpoints.

                      source
                      theorem MarkedGraphs.Certificate.AffinePosition.Code.decodeVertex_eq_tail_of_coordinate_eq_zero {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) (core_nonempty : 0 < n) {degree : ℤ} (hValid : certificate.Valid degree) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) (hZero : coordinate certificate code point = 0) :
                      decodeVertex certificate code point core_nonempty hValid hBounds hCone = (certificate.subdivisionSpec point core_nonempty hValid hCone).coreVertex (certificate.core.tail code.edge)

                      Coordinate zero decodes to the tail core vertex.

                      source
                      theorem MarkedGraphs.Certificate.AffinePosition.Code.decodeVertex_eq_head_of_coordinate_eq_length {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) (core_nonempty : 0 < n) {degree : ℤ} (hValid : certificate.Valid degree) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) (hLength : coordinate certificate code point = certificate.segmentNat point code.edge) :
                      decodeVertex certificate code point core_nonempty hValid hBounds hCone = (certificate.subdivisionSpec point core_nonempty hValid hCone).coreVertex (certificate.core.head code.edge)

                      Coordinate equal to the slot length decodes to the head core vertex.