A.6.0:5.4 - Formal work: length-indexed zero-vector operation

An engineer declares the reusable operation zeroVector(n) in ordinary language: give it a natural number n; it returns a vector of n real-valued entries, every one zero. In the A.6.1 OperationDeclaration, argument lengthIndex means the requested component count and has ValueKind NaturalNumber. Result zeroVectorResult means the returned zero vector and has the indexed result family FiniteVector(RealScalar, n). The application predicate says that one application binds one n and returns that vector. The dependency law states length(zeroVector(n)) = n, and the zero law states that every indexed entry equals scalar zero. Applicability limits this declaration to finite vectors over the declared RealScalar field.

The declaration imports the exact type-former FiniteVector(RealScalar, n) and its length-index law from FormalSubstrate signature FiniteVectorSubstrate_v2. Remove that provider and neither the result declaration can be interpreted nor the length law replayed, so this is a declaration dependency rather than a background citation. The operation argument and result remain A.6.1 declarations; they are not A.6.5 relation SlotSpecs.

A Lean representation may write the result as Vector Real n. A proof-carrying record representation may write entries: List Real together with lengthProof: entries.length = n. Because both represent the same operation declaration and no mathematical lens changes the next comparison action, A.6.3.RT alone governs this representation-scheme transition. It preserves the result-length index and the all-zero law. Lean binder order, implicit elaboration, record field order, and the location of the length proof are representation-local and need not survive. Stop here: no C.29 result is needed. If a later comparison uses a named free-module lens to decide algebraic reuse, that changed lens use opens C.29 and must separately state the preserved addition and scalar action and the lost coordinate or layout detail. State a blocked inference only when it passes F.19:4’s full guard test.

Practical payoff: formal-methods engineers can fill and inspect the dependent A.6.1 declaration, test its actual FormalSubstrate dependency, and compare representations.