Documentation

LambdaS.PiExamples

Boundary checks for the coherent Pi theorem #

These kernel-checked examples test three boundaries: the dimension-level scaling law covers addMixed, which the drift diagnostic declines (addMixed_coherent); the coherent bridge accepts internal dimension and unit abstraction (instantiatedCaster_coherent); and descent needs no extra nonempty hypotheses at rank zero or full rank. The caster's derivation is constructed from typing rules and substitution lemmas, without compiler-evaluated decision procedures.

source
theorem LambdaS.Examples.addMixed_coherent (V : Scaling Base 0) {m' : ℕ} (eqv : Fin m' ≃ Dim ⊕ Fin 0) :
Pi.MulScaleLaw (Pi.dimensionMatrix eqv [m, ft]) (Pi.dimensionExponents eqv ft) fun (x : Fin [m, ft].length → ℝ) => den V addMixedDeriv (Pi.envOf [m, ft] x)

Coherent scaling covers a program the drift diagnostic declines.

source
def LambdaS.Examples.instantiatedCaster :
Term₀

Internal dimension and unit abstraction, instantiated at meter and foot.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def LambdaS.Examples.instantiatedCasterDeriv :
    HasTy Δ₀ (scalarCtx [m]) instantiatedCaster (Ty.Q ft)

    The typing derivation of instantiatedCaster at Q ft over one meter input, built from HasTy.dapp, HasTy.uapp, and substitution lemmas.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem LambdaS.Examples.instantiatedCaster_coherent (V : Scaling Base 0) {m' : ℕ} (eqv : Fin m' ≃ Dim ⊕ Fin 0) :
      Pi.MulScaleLaw (Pi.dimensionMatrix eqv [m]) (Pi.dimensionExponents eqv ft) fun (x : Fin [m].length → ℝ) => den V instantiatedCasterDeriv (Pi.envOf [m] x)

      The dimension-level scaling law holds for instantiatedCaster, which binds a dimension and two units internally and converts meters to feet.

      source
      theorem LambdaS.Pi.fullRank_descends {H : (Fin 1 → ℝ) → ℝ} (hH : Invariant 1 H) :
      ∃ (G : (Fin 0 → ℝ) → ℝ), ∀ (ξ : Fin 1 → ℝ), H ξ = G fun (i : Fin 0) => i.elim0

      Full rank really produces a function of zero arguments.

      source
      theorem LambdaS.Pi.zeroRank_descends {n : ℕ} {H : (Fin n → ℝ) → ℝ} :
      Matrix.rank 0 = 0 ∧ ∃ (G : (Fin (n - Matrix.rank 0) → ℝ) → ℝ), ∀ (ξ : Fin n → ℝ), H ξ = G (piCoordinates 0 ξ)

      Zero rank retains all coordinates, with no nonempty-row assumption.