Documentation

LeanMlir.Proofs.Foundation.OpaquePrefix

The opaque running activations of a layered net — one def per slot #

opaqueA k stem b1 … bk x is the activation after the k-th stage of a chain whose stages are all still VARIABLES. Every whole-net certified backward tie states its apex over these: the tie keeps its blocks opaque, and a *_eq_slots shape check says the concrete stages ARE the committed forward. They are plain defs so the closing rfl of a tie can unfold them.

Net-agnostic and generic in every dimension, with enough slots for the deepest chain in the suite.

source
noncomputable def Proofs.opaqueA0 {s0 s1 : ℕ} (stem : Vec s0 → Vec s1) (x : Vec s0) :
Vec s1

The first stage's output.

Equations
Instances For
    source
    noncomputable def Proofs.opaqueA1 {s0 s1 s2 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (x : Vec s0) :
    Vec s2

    The activation after stage 1.

    Equations
    Instances For
      source
      noncomputable def Proofs.opaqueA2 {s0 s1 s2 s3 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (b2 : Vec s2 → Vec s3) (x : Vec s0) :
      Vec s3

      The activation after stage 2.

      Equations
      Instances For
        source
        noncomputable def Proofs.opaqueA3 {s0 s1 s2 s3 s4 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (b2 : Vec s2 → Vec s3) (b3 : Vec s3 → Vec s4) (x : Vec s0) :
        Vec s4

        The activation after stage 3.

        Equations
        Instances For
          source
          noncomputable def Proofs.opaqueA4 {s0 s1 s2 s3 s4 s5 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (b2 : Vec s2 → Vec s3) (b3 : Vec s3 → Vec s4) (b4 : Vec s4 → Vec s5) (x : Vec s0) :
          Vec s5

          The activation after stage 4.

          Equations
          Instances For
            source
            noncomputable def Proofs.opaqueA5 {s0 s1 s2 s3 s4 s5 s6 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (b2 : Vec s2 → Vec s3) (b3 : Vec s3 → Vec s4) (b4 : Vec s4 → Vec s5) (b5 : Vec s5 → Vec s6) (x : Vec s0) :
            Vec s6

            The activation after stage 5.

            Equations
            Instances For
              source
              noncomputable def Proofs.opaqueA6 {s0 s1 s2 s3 s4 s5 s6 s7 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (b2 : Vec s2 → Vec s3) (b3 : Vec s3 → Vec s4) (b4 : Vec s4 → Vec s5) (b5 : Vec s5 → Vec s6) (b6 : Vec s6 → Vec s7) (x : Vec s0) :
              Vec s7

              The activation after stage 6.

              Equations
              Instances For
                source
                noncomputable def Proofs.opaqueA7 {s0 s1 s2 s3 s4 s5 s6 s7 s8 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (b2 : Vec s2 → Vec s3) (b3 : Vec s3 → Vec s4) (b4 : Vec s4 → Vec s5) (b5 : Vec s5 → Vec s6) (b6 : Vec s6 → Vec s7) (b7 : Vec s7 → Vec s8) (x : Vec s0) :
                Vec s8

                The activation after stage 7.

                Equations
                Instances For
                  source
                  noncomputable def Proofs.opaqueA8 {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (b2 : Vec s2 → Vec s3) (b3 : Vec s3 → Vec s4) (b4 : Vec s4 → Vec s5) (b5 : Vec s5 → Vec s6) (b6 : Vec s6 → Vec s7) (b7 : Vec s7 → Vec s8) (b8 : Vec s8 → Vec s9) (x : Vec s0) :
                  Vec s9

                  The activation after stage 8.

                  Equations
                  Instances For
                    source
                    noncomputable def Proofs.opaqueA9 {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (b2 : Vec s2 → Vec s3) (b3 : Vec s3 → Vec s4) (b4 : Vec s4 → Vec s5) (b5 : Vec s5 → Vec s6) (b6 : Vec s6 → Vec s7) (b7 : Vec s7 → Vec s8) (b8 : Vec s8 → Vec s9) (b9 : Vec s9 → Vec s10) (x : Vec s0) :
                    Vec s10

                    The activation after stage 9.

                    Equations
                    Instances For
                      source
                      noncomputable def Proofs.opaqueA10 {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (b2 : Vec s2 → Vec s3) (b3 : Vec s3 → Vec s4) (b4 : Vec s4 → Vec s5) (b5 : Vec s5 → Vec s6) (b6 : Vec s6 → Vec s7) (b7 : Vec s7 → Vec s8) (b8 : Vec s8 → Vec s9) (b9 : Vec s9 → Vec s10) (b10 : Vec s10 → Vec s11) (x : Vec s0) :
                      Vec s11

                      The activation after stage 10.

                      Equations
                      Instances For
                        source
                        noncomputable def Proofs.opaqueA11 {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (b2 : Vec s2 → Vec s3) (b3 : Vec s3 → Vec s4) (b4 : Vec s4 → Vec s5) (b5 : Vec s5 → Vec s6) (b6 : Vec s6 → Vec s7) (b7 : Vec s7 → Vec s8) (b8 : Vec s8 → Vec s9) (b9 : Vec s9 → Vec s10) (b10 : Vec s10 → Vec s11) (b11 : Vec s11 → Vec s12) (x : Vec s0) :
                        Vec s12

                        The activation after stage 11.

                        Equations
                        Instances For
                          source
                          noncomputable def Proofs.opaqueA12 {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (b2 : Vec s2 → Vec s3) (b3 : Vec s3 → Vec s4) (b4 : Vec s4 → Vec s5) (b5 : Vec s5 → Vec s6) (b6 : Vec s6 → Vec s7) (b7 : Vec s7 → Vec s8) (b8 : Vec s8 → Vec s9) (b9 : Vec s9 → Vec s10) (b10 : Vec s10 → Vec s11) (b11 : Vec s11 → Vec s12) (b12 : Vec s12 → Vec s13) (x : Vec s0) :
                          Vec s13

                          The activation after stage 12.

                          Equations
                          Instances For
                            source
                            noncomputable def Proofs.opaqueA13 {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (b2 : Vec s2 → Vec s3) (b3 : Vec s3 → Vec s4) (b4 : Vec s4 → Vec s5) (b5 : Vec s5 → Vec s6) (b6 : Vec s6 → Vec s7) (b7 : Vec s7 → Vec s8) (b8 : Vec s8 → Vec s9) (b9 : Vec s9 → Vec s10) (b10 : Vec s10 → Vec s11) (b11 : Vec s11 → Vec s12) (b12 : Vec s12 → Vec s13) (b13 : Vec s13 → Vec s14) (x : Vec s0) :
                            Vec s14

                            The activation after stage 13.

                            Equations
                            Instances For
                              source
                              noncomputable def Proofs.opaqueA14 {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (b2 : Vec s2 → Vec s3) (b3 : Vec s3 → Vec s4) (b4 : Vec s4 → Vec s5) (b5 : Vec s5 → Vec s6) (b6 : Vec s6 → Vec s7) (b7 : Vec s7 → Vec s8) (b8 : Vec s8 → Vec s9) (b9 : Vec s9 → Vec s10) (b10 : Vec s10 → Vec s11) (b11 : Vec s11 → Vec s12) (b12 : Vec s12 → Vec s13) (b13 : Vec s13 → Vec s14) (b14 : Vec s14 → Vec s15) (x : Vec s0) :
                              Vec s15

                              The activation after stage 14.

                              Equations
                              Instances For
                                source
                                noncomputable def Proofs.opaqueA15 {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (b2 : Vec s2 → Vec s3) (b3 : Vec s3 → Vec s4) (b4 : Vec s4 → Vec s5) (b5 : Vec s5 → Vec s6) (b6 : Vec s6 → Vec s7) (b7 : Vec s7 → Vec s8) (b8 : Vec s8 → Vec s9) (b9 : Vec s9 → Vec s10) (b10 : Vec s10 → Vec s11) (b11 : Vec s11 → Vec s12) (b12 : Vec s12 → Vec s13) (b13 : Vec s13 → Vec s14) (b14 : Vec s14 → Vec s15) (b15 : Vec s15 → Vec s16) (x : Vec s0) :
                                Vec s16

                                The activation after stage 15.

                                Equations
                                Instances For
                                  source
                                  noncomputable def Proofs.opaqueA16 {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 s17 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (b2 : Vec s2 → Vec s3) (b3 : Vec s3 → Vec s4) (b4 : Vec s4 → Vec s5) (b5 : Vec s5 → Vec s6) (b6 : Vec s6 → Vec s7) (b7 : Vec s7 → Vec s8) (b8 : Vec s8 → Vec s9) (b9 : Vec s9 → Vec s10) (b10 : Vec s10 → Vec s11) (b11 : Vec s11 → Vec s12) (b12 : Vec s12 → Vec s13) (b13 : Vec s13 → Vec s14) (b14 : Vec s14 → Vec s15) (b15 : Vec s15 → Vec s16) (b16 : Vec s16 → Vec s17) (x : Vec s0) :
                                  Vec s17

                                  The activation after stage 16.

                                  Equations
                                  Instances For
                                    source
                                    noncomputable def Proofs.opaqueA17 {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 s17 s18 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (b2 : Vec s2 → Vec s3) (b3 : Vec s3 → Vec s4) (b4 : Vec s4 → Vec s5) (b5 : Vec s5 → Vec s6) (b6 : Vec s6 → Vec s7) (b7 : Vec s7 → Vec s8) (b8 : Vec s8 → Vec s9) (b9 : Vec s9 → Vec s10) (b10 : Vec s10 → Vec s11) (b11 : Vec s11 → Vec s12) (b12 : Vec s12 → Vec s13) (b13 : Vec s13 → Vec s14) (b14 : Vec s14 → Vec s15) (b15 : Vec s15 → Vec s16) (b16 : Vec s16 → Vec s17) (b17 : Vec s17 → Vec s18) (x : Vec s0) :
                                    Vec s18

                                    The activation after stage 17.

                                    Equations
                                    • Proofs.opaqueA17 stem b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 x = b17 (Proofs.opaqueA16 stem b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 x)
                                    Instances For
                                      source
                                      noncomputable def Proofs.opaqueA18 {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 s17 s18 s19 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (b2 : Vec s2 → Vec s3) (b3 : Vec s3 → Vec s4) (b4 : Vec s4 → Vec s5) (b5 : Vec s5 → Vec s6) (b6 : Vec s6 → Vec s7) (b7 : Vec s7 → Vec s8) (b8 : Vec s8 → Vec s9) (b9 : Vec s9 → Vec s10) (b10 : Vec s10 → Vec s11) (b11 : Vec s11 → Vec s12) (b12 : Vec s12 → Vec s13) (b13 : Vec s13 → Vec s14) (b14 : Vec s14 → Vec s15) (b15 : Vec s15 → Vec s16) (b16 : Vec s16 → Vec s17) (b17 : Vec s17 → Vec s18) (b18 : Vec s18 → Vec s19) (x : Vec s0) :
                                      Vec s19

                                      The activation after stage 18.

                                      Equations
                                      • Proofs.opaqueA18 stem b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 x = b18 (Proofs.opaqueA17 stem b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 x)
                                      Instances For
                                        source
                                        noncomputable def Proofs.opaqueA19 {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 s17 s18 s19 s20 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (b2 : Vec s2 → Vec s3) (b3 : Vec s3 → Vec s4) (b4 : Vec s4 → Vec s5) (b5 : Vec s5 → Vec s6) (b6 : Vec s6 → Vec s7) (b7 : Vec s7 → Vec s8) (b8 : Vec s8 → Vec s9) (b9 : Vec s9 → Vec s10) (b10 : Vec s10 → Vec s11) (b11 : Vec s11 → Vec s12) (b12 : Vec s12 → Vec s13) (b13 : Vec s13 → Vec s14) (b14 : Vec s14 → Vec s15) (b15 : Vec s15 → Vec s16) (b16 : Vec s16 → Vec s17) (b17 : Vec s17 → Vec s18) (b18 : Vec s18 → Vec s19) (b19 : Vec s19 → Vec s20) (x : Vec s0) :
                                        Vec s20

                                        The activation after stage 19.

                                        Equations
                                        • Proofs.opaqueA19 stem b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 x = b19 (Proofs.opaqueA18 stem b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 x)
                                        Instances For
                                          source
                                          noncomputable def Proofs.opaqueA20 {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 s17 s18 s19 s20 s21 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (b2 : Vec s2 → Vec s3) (b3 : Vec s3 → Vec s4) (b4 : Vec s4 → Vec s5) (b5 : Vec s5 → Vec s6) (b6 : Vec s6 → Vec s7) (b7 : Vec s7 → Vec s8) (b8 : Vec s8 → Vec s9) (b9 : Vec s9 → Vec s10) (b10 : Vec s10 → Vec s11) (b11 : Vec s11 → Vec s12) (b12 : Vec s12 → Vec s13) (b13 : Vec s13 → Vec s14) (b14 : Vec s14 → Vec s15) (b15 : Vec s15 → Vec s16) (b16 : Vec s16 → Vec s17) (b17 : Vec s17 → Vec s18) (b18 : Vec s18 → Vec s19) (b19 : Vec s19 → Vec s20) (b20 : Vec s20 → Vec s21) (x : Vec s0) :
                                          Vec s21

                                          The activation after stage 20.

                                          Equations
                                          • Proofs.opaqueA20 stem b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 x = b20 (Proofs.opaqueA19 stem b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 x)
                                          Instances For
                                            source
                                            noncomputable def Proofs.opaqueA21 {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 s17 s18 s19 s20 s21 s22 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (b2 : Vec s2 → Vec s3) (b3 : Vec s3 → Vec s4) (b4 : Vec s4 → Vec s5) (b5 : Vec s5 → Vec s6) (b6 : Vec s6 → Vec s7) (b7 : Vec s7 → Vec s8) (b8 : Vec s8 → Vec s9) (b9 : Vec s9 → Vec s10) (b10 : Vec s10 → Vec s11) (b11 : Vec s11 → Vec s12) (b12 : Vec s12 → Vec s13) (b13 : Vec s13 → Vec s14) (b14 : Vec s14 → Vec s15) (b15 : Vec s15 → Vec s16) (b16 : Vec s16 → Vec s17) (b17 : Vec s17 → Vec s18) (b18 : Vec s18 → Vec s19) (b19 : Vec s19 → Vec s20) (b20 : Vec s20 → Vec s21) (b21 : Vec s21 → Vec s22) (x : Vec s0) :
                                            Vec s22

                                            The activation after stage 21.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              source
                                              noncomputable def Proofs.opaqueA22 {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 s17 s18 s19 s20 s21 s22 s23 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (b2 : Vec s2 → Vec s3) (b3 : Vec s3 → Vec s4) (b4 : Vec s4 → Vec s5) (b5 : Vec s5 → Vec s6) (b6 : Vec s6 → Vec s7) (b7 : Vec s7 → Vec s8) (b8 : Vec s8 → Vec s9) (b9 : Vec s9 → Vec s10) (b10 : Vec s10 → Vec s11) (b11 : Vec s11 → Vec s12) (b12 : Vec s12 → Vec s13) (b13 : Vec s13 → Vec s14) (b14 : Vec s14 → Vec s15) (b15 : Vec s15 → Vec s16) (b16 : Vec s16 → Vec s17) (b17 : Vec s17 → Vec s18) (b18 : Vec s18 → Vec s19) (b19 : Vec s19 → Vec s20) (b20 : Vec s20 → Vec s21) (b21 : Vec s21 → Vec s22) (b22 : Vec s22 → Vec s23) (x : Vec s0) :
                                              Vec s23

                                              The activation after stage 22.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                source
                                                noncomputable def Proofs.opaqueA23 {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 s17 s18 s19 s20 s21 s22 s23 s24 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (b2 : Vec s2 → Vec s3) (b3 : Vec s3 → Vec s4) (b4 : Vec s4 → Vec s5) (b5 : Vec s5 → Vec s6) (b6 : Vec s6 → Vec s7) (b7 : Vec s7 → Vec s8) (b8 : Vec s8 → Vec s9) (b9 : Vec s9 → Vec s10) (b10 : Vec s10 → Vec s11) (b11 : Vec s11 → Vec s12) (b12 : Vec s12 → Vec s13) (b13 : Vec s13 → Vec s14) (b14 : Vec s14 → Vec s15) (b15 : Vec s15 → Vec s16) (b16 : Vec s16 → Vec s17) (b17 : Vec s17 → Vec s18) (b18 : Vec s18 → Vec s19) (b19 : Vec s19 → Vec s20) (b20 : Vec s20 → Vec s21) (b21 : Vec s21 → Vec s22) (b22 : Vec s22 → Vec s23) (b23 : Vec s23 → Vec s24) (x : Vec s0) :
                                                Vec s24

                                                The activation after stage 23.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  source
                                                  noncomputable def Proofs.opaqueA24 {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 s17 s18 s19 s20 s21 s22 s23 s24 s25 : ℕ} (stem : Vec s0 → Vec s1) (b1 : Vec s1 → Vec s2) (b2 : Vec s2 → Vec s3) (b3 : Vec s3 → Vec s4) (b4 : Vec s4 → Vec s5) (b5 : Vec s5 → Vec s6) (b6 : Vec s6 → Vec s7) (b7 : Vec s7 → Vec s8) (b8 : Vec s8 → Vec s9) (b9 : Vec s9 → Vec s10) (b10 : Vec s10 → Vec s11) (b11 : Vec s11 → Vec s12) (b12 : Vec s12 → Vec s13) (b13 : Vec s13 → Vec s14) (b14 : Vec s14 → Vec s15) (b15 : Vec s15 → Vec s16) (b16 : Vec s16 → Vec s17) (b17 : Vec s17 → Vec s18) (b18 : Vec s18 → Vec s19) (b19 : Vec s19 → Vec s20) (b20 : Vec s20 → Vec s21) (b21 : Vec s21 → Vec s22) (b22 : Vec s22 → Vec s23) (b23 : Vec s23 → Vec s24) (b24 : Vec s24 → Vec s25) (x : Vec s0) :
                                                  Vec s25

                                                  The activation after stage 24.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    source
                                                    theorem Proofs.HasVJPAt.correct_of_backward_eq {m n : ℕ} {f : Vec m → Vec n} {x : Vec m} (hf : HasVJPAt f x) {B : Vec n → Vec m} (h : B = hf.backward) (dy : Vec n) (i : Fin m) :
                                                    B dy i = ∑ j : Fin n, pdiv f x i j * dy j

                                                    correct through a named backward. A whole-net tie states B = hf.backward for its apex witness hf; this turns that equation into B's correctness without spelling hf out again (unification reads it off h).