Universal fixed-lag certificate search

Abstract

A finite algorithm decides original numbered certificates at each fixed positive lag.

The orders n and k and lag m are arbitrary natural numbers. A and B are natural count matrices of orders n and k. The input requires positive orders, positive lag, and a nonzero entry in every row and every column of both matrices. The selector aligned chooses either the two original aligned laws or the two original compatibility sweep laws. All equalities retain the numbered edges and the whole output paths.

Definition 1.1 (The four actual maps).

$$\forall n\in Nat,k\in Nat,A\in \mathrm{CountMat}\left(n,n\right),B\in \mathrm{CountMat}\left(k,k\right),m\in Nat,\forall R\in \mathrm{CountMat}\left(n,k\right),S\in \mathrm{CountMat}\left(k,n\right),\mathrm{Maps}\left(A,B,R,S,m\right)=\mathrm{FourEquivalenceFamilies}\left(A,B,R,S,m\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.Maps (✓ std3).

Source. Repository-derived.

Commentary.

FourEquivalenceFamilies is the product of the endpoint-indexed families EdgePair(A,R,i,z) ≃ EdgePair(R,B,i,z), EdgePair(B,S,t,w) ≃ EdgePair(S,A,t,w), EdgePair(R,S,i,w) ≃ FinitePath(A,m,i,w), and EdgePair(S,R,t,v) ≃ FinitePath(B,m,t,v). Each equivalence stores its forward and inverse tables and both inverse laws.

Definition 1.2 (Both sweep laws).

$$\forall n\in Nat,k\in Nat,A\in \mathrm{CountMat}\left(n,n\right),B\in \mathrm{CountMat}\left(k,k\right),m\in Nat,\forall R\in \mathrm{CountMat}\left(n,k\right),S\in \mathrm{CountMat}\left(k,n\right),\forall d\in \mathrm{Maps}\left(A,B,R,S,m\right),\mathrm{Compatible}\left(d\right)=\left(\mathrm{ForwardSweepLaw}\left(d\right)\wedge \mathrm{BackwardSweepLaw}\left(d\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.Compatible (✓ std3).

Source. Repository-derived.

Commentary.

For every length-m A path alpha from i to j and every numbered R edge r from j to z, write psiA(i,j) inverse(alpha)=(u,r0,s0). ForwardSweepLaw says sweep(phiR,alpha,r)=(u,r0,psiB(u,z)(j,s0,r)). BackwardSweepLaw is the literal swapped equation: for a B path beta from t to z and S edge s from z to w, write psiB(t,z) inverse(beta)=(u,s0,r0); sweep(phiS,beta,s)=(u,s0,psiA(u,w)(z,r0,s)). Both quantify over every original path and numbered edge.

Definition 1.3 (Both alignment laws).

$$\forall n\in Nat,k\in Nat,A\in \mathrm{CountMat}\left(n,n\right),B\in \mathrm{CountMat}\left(k,k\right),m\in Nat,\forall R\in \mathrm{CountMat}\left(n,k\right),S\in \mathrm{CountMat}\left(k,n\right),\forall d\in \mathrm{Maps}\left(A,B,R,S,m\right),\mathrm{Aligned}\left(d\right)=\left(\mathrm{AlignedA}\left(\mathrm{phiR}\left(d\right),\mathrm{phiS}\left(d\right),\mathrm{psiA}\left(d\right)\right)\wedge \mathrm{AlignedB}\left(\mathrm{phiR}\left(d\right),\mathrm{phiS}\left(d\right),\mathrm{psiB}\left(d\right)\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.Aligned (✓ std3).

Source. Repository-derived.

Commentary.

AlignedA and AlignedB are the original predicates from OriginalAlignedBalanced, applied to these same four equivalences.

Definition 1.4 (Selecting the law pair).

$$\forall n\in Nat,k\in Nat,A\in \mathrm{CountMat}\left(n,n\right),B\in \mathrm{CountMat}\left(k,k\right),m\in Nat,\forall R\in \mathrm{CountMat}\left(n,k\right),S\in \mathrm{CountMat}\left(k,n\right),\forall d\in \mathrm{Maps}\left(A,B,R,S,m\right),\forall aligned\in Bool,\mathrm{Valid}\left(aligned,d\right)=\mathrm{ifThenElse}\left(aligned,\mathrm{Aligned}\left(d\right),\mathrm{Compatible}\left(d\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.Valid (✓ std3).

Source. Repository-derived.

Commentary.

The true selector requires Aligned and the false selector requires Compatible. No maps are replaced when selecting the laws.

Definition 1.5 (Essential count matrices).

$$\forall r\in Nat,X\in \mathrm{CountMat}\left(r,r\right),\mathrm{Essential}\left(X\right)=\left(\left(\forall i\in \mathrm{Fin}\left(r\right),\exists j\in \mathrm{Fin}\left(r\right),\mathrm{entry}\left(X,i,j\right)\ne 0\right)\wedge \left(\forall j\in \mathrm{Fin}\left(r\right),\exists i\in \mathrm{Fin}\left(r\right),\mathrm{entry}\left(X,i,j\right)\ne 0\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.Essential (✓ std3).

Source. Repository-derived.

Commentary.

Every row and every column has a nonzero entry. The two clauses are separate, including at order zero.

Definition 1.6 (The original input boundary).

$$\forall n\in Nat,k\in Nat,A\in \mathrm{CountMat}\left(n,n\right),B\in \mathrm{CountMat}\left(k,k\right),m\in Nat,\mathrm{Input}\left(A,B,m\right)=\left(1\le n\wedge \left(1\le k\wedge \left(1\le m\wedge \left(\mathrm{Essential}\left(A\right)\wedge \mathrm{Essential}\left(B\right)\right)\right)\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.Input (✓ std3).

Source. Repository-derived.

Commentary.

Input consists exactly of 0<n, 0<k, 0<m and essentiality of A and B. Lag zero, an empty order, and a zero row or column are rejected.

Definition 1.7 (Unrestricted original existence).

$$\forall n\in Nat,k\in Nat,A\in \mathrm{CountMat}\left(n,n\right),B\in \mathrm{CountMat}\left(k,k\right),m\in Nat,\forall aligned\in Bool,\mathrm{OriginalExists}\left(A,B,m,aligned\right)=\left(\mathrm{Input}\left(A,B,m\right)\wedge \left(\exists R\in \mathrm{CountMat}\left(n,k\right),S\in \mathrm{CountMat}\left(k,n\right),d\in \mathrm{Maps}\left(A,B,R,S,m\right),\mathrm{Valid}\left(aligned,d\right)\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.OriginalExists (✓ std3).

Source. Repository-derived.

Commentary.

R and S range over all natural matrices of the displayed shapes. There is no entry bound in this existence predicate. The witness includes all four equivalences and both selected laws.

Definition 1.8 (The four matrix products).

$$\forall n\in Nat,k\in Nat,A\in \mathrm{CountMat}\left(n,n\right),B\in \mathrm{CountMat}\left(k,k\right),m\in Nat,\forall R\in \mathrm{CountMat}\left(n,k\right),S\in \mathrm{CountMat}\left(k,n\right),\mathrm{MatrixLaws}\left(A,B,R,S,m\right)=\left(A\cdot R=R\cdot B\wedge \left(B\cdot S=S\cdot A\wedge \left(R\cdot S=\mathrm{power}\left(A,m\right)\wedge S\cdot R=\mathrm{power}\left(B,m\right)\right)\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.MatrixLaws (✓ std3).

Source. Repository-derived.

Commentary.

The four products follow from cardinalities of the four equivalences. The RS and SR equations use the corresponding A and B path counts separately.

Definition 1.9 (A finite matrix carrier).

$$\forall r\in Nat,s\in Nat,bound\in Nat,\mathrm{BoundedMatrix}\left(r,s,bound\right)=\mathrm{FiniteMatrixFunctions}\left(r,s,\mathrm{succ}\left(bound\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.BoundedMatrix (✓ std3).

Source. Repository-derived.

Commentary.

BoundedMatrix(r,s,bound) is Fin r → Fin s → Fin(bound+1), including entries zero through bound.

Definition 1.10 (Recovering natural entries).

$$\forall r\in Nat,s\in Nat,bound\in Nat,X\in \mathrm{BoundedMatrix}\left(r,s,bound\right),i\in \mathrm{Fin}\left(r\right),j\in \mathrm{Fin}\left(s\right),\mathrm{entry}\left(\mathrm{entries}\left(X\right),i,j\right)=\mathrm{val}\left(\mathrm{entry}\left(X,i,j\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.entries (✓ std3).

Source. Repository-derived.

Commentary.

The decoding takes each Fin value’s natural-number value without changing a row, column or edge number.

Definition 1.11 (All bounded matrices and all maps).

$$\forall n\in Nat,k\in Nat,A\in \mathrm{CountMat}\left(n,n\right),B\in \mathrm{CountMat}\left(k,k\right),m\in Nat,\mathrm{Candidate}\left(A,B,m\right)=\mathrm{BoundedMatrixAndMapTuples}\left(A,B,m\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.Candidate (✓ std3).

Source. Repository-derived.

Commentary.

The dependent sum first enumerates R in BoundedMatrix(n,k,powerMaximum(A,m)), then S in BoundedMatrix(k,n,powerMaximum(B,m)), then all Maps(A,B,entries(R),entries(S),m). Path types are encoded recursively. Equivalences are encoded by their actual forward and inverse finite tables with inverse-law tests. Thus the enumeration includes whole maps rather than cardinality surrogates.

Definition 1.12 (Checking a candidate).

$$\forall n\in Nat,k\in Nat,A\in \mathrm{CountMat}\left(n,n\right),B\in \mathrm{CountMat}\left(k,k\right),m\in Nat,\forall aligned\in Bool,\forall c\in \mathrm{Candidate}\left(A,B,m\right),\mathrm{candidateCheck}\left(A,B,m,aligned,c\right)=\mathrm{decide}\left(\mathrm{Input}\left(A,B,m\right)\wedge \left(\mathrm{CandidateMatrixLaws}\left(A,B,m,c\right)\wedge \mathrm{Valid}\left(aligned,\mathrm{maps}\left(c\right)\right)\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.candidateCheck (✓ std3).

Source. Repository-derived.

Commentary.

CandidateMatrixLaws abbreviates MatrixLaws(A,B,entries(c.R),entries(c.S),m). The final conjunction tests both laws of the selected kind on c’s four actual maps.

Definition 1.13 (Executable finite search).

$$\forall n\in Nat,k\in Nat,A\in \mathrm{CountMat}\left(n,n\right),B\in \mathrm{CountMat}\left(k,k\right),m\in Nat,\forall aligned\in Bool,\mathrm{search}\left(A,B,m,aligned\right)=\mathrm{GuardedFirstAcceptedCandidate}\left(A,B,m,aligned\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.search (✓ std3).

Source. Repository-derived.

Commentary.

If Input is false, search returns none. Otherwise it runs List.find? with candidateCheck on Encodable.sortedUniv(Candidate(A,B,m)). A successful result returns the actual bounded matrices and all four equivalences. Both Fintype and Encodable are constructed, so this is executable exhaustive search.

Definition 1.14 (The decision Boolean).

$$\forall n\in Nat,k\in Nat,A\in \mathrm{CountMat}\left(n,n\right),B\in \mathrm{CountMat}\left(k,k\right),m\in Nat,\forall aligned\in Bool,\mathrm{existsBool}\left(A,B,m,aligned\right)=\mathrm{isSome}\left(\mathrm{search}\left(A,B,m,aligned\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.existsBool (✓ std3).

Source. Repository-derived.

Commentary.

existsBool observes whether the search returned an actual candidate.

Theorem 1.15 (Soundness of the returned maps).

$$\forall n\in Nat,k\in Nat,A\in \mathrm{CountMat}\left(n,n\right),B\in \mathrm{CountMat}\left(k,k\right),m\in Nat,\forall aligned\in Bool,\forall c\in \mathrm{Candidate}\left(A,B,m\right),\mathrm{search}\left(A,B,m,aligned\right)=\mathrm{some}\left(c\right)\Rightarrow \left(\mathrm{Input}\left(A,B,m\right)\wedge \mathrm{Valid}\left(aligned,\mathrm{maps}\left(c\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.search_sound (✓ std3). ∎

Source. Repository-derived.

Commentary.

List.find? supplies a true candidateCheck. Eliminating its decidable conjunction gives the original input and both selected laws for precisely the returned maps.

Theorem 1.16 (Universal correctness).

$$\forall n\in Nat,k\in Nat,A\in \mathrm{CountMat}\left(n,n\right),B\in \mathrm{CountMat}\left(k,k\right),m\in Nat,\forall aligned\in Bool,\mathrm{existsBool}\left(A,B,m,aligned\right)=true\iff \mathrm{OriginalExists}\left(A,B,m,aligned\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.search_correct (✓ std3). ∎

Source. Repository-derived.

Commentary.

Soundness recovers the unrestricted witness from the returned candidate. For completeness, start with arbitrary natural R and S and the original four equivalences. Essentiality and the inverse path bijections bound every R entry by powerMaximum(A,m) and every S entry by powerMaximum(B,m). Encode each entry in the corresponding Fin type and retain the same four equivalences. This constructs an actual Candidate whose check is true; membership in sortedUniv makes the search succeed. The construction occurs directly in the universal theorem and adds no bounded-input hypothesis.

The executable examples use command-local CountMat(1,1) inputs with every entry equal to one, evaluate both selectors, and reject lag zero and a nonessential input. The utility instance names the already existing private unitCountMatrix in CompatibleResponseForgettingBound, which is the same closed one-matrix input. A separate example enumerates all four map tables for the one-vertex two-loop input. Examples provide computational observations, not additional mathematical results.

References

• Truth anchor: D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.Aligned
• Truth anchor: D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.BoundedMatrix
• Truth anchor: D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.Candidate
• Truth anchor: D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.Compatible
• Truth anchor: D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.Essential
• Truth anchor: D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.Input
• Truth anchor: D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.Maps
• Truth anchor: D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.MatrixLaws
• Truth anchor: D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.OriginalExists
• Truth anchor: D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.Valid
• Truth anchor: D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.candidateCheck
• Truth anchor: D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.entries
• Truth anchor: D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.existsBool
• Truth anchor: D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.search
• Truth anchor: D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.search_correct
• Truth anchor: D5/S3/ConceptDynamics/Coding/ResponseRealization/FixedLagCertificateSearch.search_sound
• Dependency: D5/S3/ConceptDynamics/Coding/OriginalResponseControls