Regression checks for fuel-free ratio comparison

Internal higher-order composition computes its expected unit; independent scalar inputs remain distinct; β-equivalent open terms agree; unit binders and vector and matrix projections preserve results. At contexts containing an unknown function or unit family, the checks compare Tw.normEq with the bounded comparison Tw.scalarEq on Tw.norm forms, including a case where substitution creates another redex; no completeness claim is made there.

theorem LambdaS.RatioCompareExamples.open_composition_correct (ψ : Scaling LambdaS.RatioCompareExamples.B✝ 0) (ρ : TwEnv [LambdaS.RatioCompareExamples.S✝, LambdaS.RatioCompareExamples.S✝]) : Tw.eval ψ ((LambdaS.RatioCompareExamples.composed✝ 3).app LambdaS.RatioCompareExamples.x✝) ρ = Tw.eval ψ (LambdaS.RatioCompareExamples.x✝.mul (Tw.unit (Term.rpow LambdaS.RatioCompareExamples.u✝ 8))) ρ

A kernel-checked instance of Tw.normEq_sound at a first-order context, with internal higher-order syntax and arbitrary unknown scalar inputs.

Higher-order contexts, against the bounded comparison

theorem LambdaS.RatioCompareExamples.higherOrderBoundary_equal (ψ : Scaling LambdaS.RatioCompareExamples.B✝ 0) (ρ : TwEnv [LambdaS.RatioCompareExamples.F✝, LambdaS.RatioCompareExamples.S✝]) : Tw.eval ψ LambdaS.RatioCompareExamples.higherOrderBoundary✝ ρ = Tw.eval ψ LambdaS.RatioCompareExamples.higherOrderInput✝ ρ