Boundary checks for the strengthened Pi theorem

These kernel-checked examples test three predictions recorded before running: coherent factorization covers addMixed despite its diagnostic decline; internal dimension/unit abstraction is accepted by the coherent bridge; and rank-zero/full-rank matrices require no extra nonempty hypotheses. The caster's derivation is constructed from typing rules and substitution lemmas, without compiler-evaluated decision procedures.

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.

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.

def LambdaS.Examples.instantiatedCasterDeriv : HasTy Δ₀ (scalarCtx [m]) instantiatedCaster (Ty.Q ft)

Equations

• One or more equations did not get rendered due to their size.

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)

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.

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.