Formalization: Generic Separation of Axis-Normalized Latent-Source Representations by Higher-Order Cumulants
The complete Lean development behind this paper — every definition, lemma, and theorem of its module, including helpers the paper text never cites. Identifiers link within this page, into the Causalean library, or out to the official Mathlib docs.
Basic.Cumulants 10 declarations The truncated-cumulant construction
The truncated-cumulant construction
Stacked joint-cumulant truncation T_L(P), coordinate (r, a) equal to κ_{r,a}(P) = Cum_P(X^{r-a}, Y^a) for 2 ≤ r ≤ L, 0 ≤ a ≤ r, and 0 outside the retained range. @realizes T_L(P),t(coordinatewise κ_{r,a}) @realizes kappa_{r,a}(P)(κ_{r,a} = Cum_P(X^{r-a}, Y^a))
Definition (Lean source)
Forward simultaneous binary-form map Φ^right_{m,L}, coordinate (r, a): Σ_j c_{jr} u_{j1}^{r-a} u_{j2}^a on the retained range, 0 outside. @realizes Phi^right_{m,L},Phi^left_{m,L}(forward binary-form map)
Definition (Lean source)
Reverse simultaneous binary-form map Φ^left_{m,L}, coordinate (r, a): Σ_j d_{jr} v_{j1}^{r-a} v_{j2}^a on the retained range, 0 outside. @realizes Phi^right_{m,L},Phi^left_{m,L}(reverse binary-form map)
Definition (Lean source)
The paper's finite retained-coordinate parameter space, represented inside the function-valued ParamSpace by pinning every off-band source weight to zero.
Definition (Lean source)
Generic retained-cumulant locus Θ^{b,∘}_{m,L}: the direct slope, all pairwise loading-slope differences, and all retained weights are nonzero inside the finite retained-band ambient Θ^b_{m,L}. The same predicate serves both arrows (forward (γ, ρ, c) and reverse (δ, σ, d)). @realizes Theta^{right,circ}_{m,L},Theta^{left,circ}_{m,L}(finite-band ambient and nonvanishing generic product)
Definition (Lean source)
A generic parameter lies in the paper's finite retained-band ambient: its source-weight coordinates vanish outside orders two through L.
Formal statement
Proof (Lean source)
At a generic parameter the defining product — direct slope, direct-to-latent slope gaps, pairwise latent slope gaps, and all retained source weights — is nonzero.
Formal statement
Proof (Lean source)
The paper's finite cumulant coordinate space ℂ^{q_L}, represented inside the ℕ-indexed CumVec by pinning every coordinate outside the retained range 2 ≤ r ≤ L, a ≤ r to zero.
Definition (Lean source)
Full complex fiber R^b_{m,L}(t) = { θ ∈ Θ^b_{m,L} : Φ^b_{m,L}(θ) = t }, parameterized by the arrow map Φ, restricted to the paper's finite retained-coordinate parameter space Θ^b_{m,L} and compared against t on the paper's retained cumulant coordinates 2 ≤ r ≤ L, a ≤ r (i.e. in ℂ^{q_L}).
Definition (Lean source)
Real moment-feasible region F^b_{m,L}: real loading-and-cumulant lists with nonzero direct slope, pairwise-distinct slopes, and every weight family c_{j·} (resp. d_{j·}) realized by a centered non-Gaussian real source law with finite L-th moment. The same predicate serves both arrows.
Definition (Lean source)
Basic.Swaps 7 declarations Admissible source swaps (the G_m action)
Admissible source swaps (the G_m action)
Relabel the middle block {1, …, m} of source indices by π, fixing 0 and m + 1.
Admissible source swap: π ∈ G_m = Equiv.Perm (Fin m) acts by relabeling the latent slopes ρ_i (resp. σ_i) and their weights c_{ir} (resp. d_{ir}) simultaneously, while fixing indices 0 and m + 1. The same map realizes both arrow actions. @realizes G_m,pi,b(π-relabeling of the middle source block)
Definition (Lean source)
Arrow index b ∈ {right, left}: the two-element type indexing the arrow parameterization on which the G_m action acts (right = forward, left = reverse). @realizes G_m,pi,b(arrow index b ∈ {right, left})
Definition (Lean source)
Provides a procedure that decides whether two arrow indices are equal, that is, whether two tags both name the forward orientation, both name the reverse one, or differ.
Definition (Lean source)
Arrow-tagged admissible source swap: the G_m action on arrow b. The same middle-block relabeling formula realizes both the forward (right) action on (ρ_i, c_{ir}) and the reverse (left) action on (σ_i, d_{ir}), so b is a tag; indices 0 and m + 1 are fixed in both cases. @realizes G_m,pi,b(π-relabeling tagged by arrow b; same formula for both)
Definition (Lean source)
The G_m action on the tagged space Arrow × ParamSpace: relabel the middle source block and preserve the arrow tag b. The swap fixes indices 0, m + 1, so it never converts a forward (right) axis pattern into a reverse (left) one; the tag component is carried unchanged. @realizes G_m,pi,b(tag-preserving G_m action on Arrow × ParamSpace)
Definition (Lean source)
Arrow-tagged G_m-orbit of (b, θ): its images under all admissible swaps, every member carrying the same tag b. Right-tagged and left-tagged orbits are therefore disjoint.
Definition (Lean source)
Basic.World 24 declarations The Gaussian-law predicate and the joint / univariate cumulants are general moment-problem objects; they were promoted to Causalean.Stat.MomentProblems and are re-exported here under the run's namespace so the run's stat
Cumulant coordinates (re-imported from Causalean)
The Gaussian-law predicate and the joint / univariate cumulants are general moment-problem
objects; they were promoted to Causalean.Stat.MomentProblems and are re-exported here under the
run's namespace so the run's statements read unchanged.
Number of independent sources n = m + 2. @realizes n(n = m+2 sources)
Definition (Lean source)
Candidate sufficient truncation order K = 2m + 2. @realizes K(K = 2m+2)
Definition (Lean source)
One-order-lower truncation K₋ = 2m + 1. @realizes K_-(K₋ = 2m+1)
Definition (Lean source)
Observable cumulant-coordinate dimension q_L = L(L+3)/2 - 2. @realizes q_L,p_L(q_L = L(L+3)/2 - 2)
Definition (Lean source)
Structural-parameter dimension p_L = (m+2)L - 1. @realizes q_L,p_L(p_L = (m+2)L - 1)
Definition (Lean source)
Space of the structural-complexity index m ∈ {1, 2, …}: at least one latent confounder. Every statement in this development is stated for m with this well-formedness clause. @realizes m(m ≥ 1, i.e. m ∈ {1,2,…})
Definition (Lean source)
Space of the truncation endpoint L ∈ {2, …, K} with K = 2m + 2: the order variable ranges over the retained cumulant orders. @realizes L(2 ≤ L ≤ 2m + 2)
Definition (Lean source)
Structural parameter space Θ^b_{m,L} = R^{m+1} × R^{n(L-1)}. The three components are the direct slope, the m latent-loading slopes, and the source-cumulant weight family (j, r) ↦ c_{jr}. @realizes Theta^right_{m,L},Theta^left_{m,L},theta,eta(coordinates (γ/δ, ρ/σ, c/d)) @realizes gamma(component .1) @realizes rho_i(component .2.1) @realizes delta(component .1) @realizes sigma_i(component .2.1) @realizes c_{jr},d_{jr}(component .2.2 j r)
Definition (Lean source)
Observable truncated-cumulant coordinate vector t ∈ R^{q_L}, indexed by (r, a) with 2 ≤ r ≤ L, 0 ≤ a ≤ r. @realizes T_L(P),t(coordinate family (r,a) ↦ t_{r,a}) @realizes kappa_{r,a}(P)(coordinate (r,a))
Definition (Lean source)
Forward source direction family u_j ∈ R²: u₀ = (1, γ), u_j = (1, ρ_j) for 1 ≤ j ≤ m, u_{m+1} = (0, 1). @realizes u_j(u₀=(1,γ), u_j=(1,ρ_j), u_{m+1}=(0,1))
Definition (Lean source)
Reverse source direction family v_j ∈ R²: v₀ = (1, 0), v_j = (σ_j, 1) for 1 ≤ j ≤ m, v_{m+1} = (δ, 1). @realizes v_j(v₀=(1,0), v_j=(σ_j,1), v_{m+1}=(δ,1))
Definition (Lean source)
Mutual independence of the m + 2 sources. @realizes S_j(source family S : Fin (m+2) → Ω → ℝ)
Definition (Lean source)
Finite K-th absolute moment E|S_j|^K < ∞ for every source.
Definition (Lean source)
Every source law is non-Gaussian.
Definition (Lean source)
Forward linear source-mixing structural equation (X, Y)ᵀ = Σ_j u_j S_j. @realizes X(X = Σ_j u_{j1} S_j) @realizes Y(Y = Σ_j u_{j2} S_j)
Definition (Lean source)
Reverse linear source-mixing structural equation (X, Y)ᵀ = Σ_j v_j S_j.
Definition (Lean source)
Distinct forward loading directions |{γ, ρ_i}| = m + 1.
Definition (Lean source)
Distinct reverse loading directions |{δ, σ_i}| = m + 1.
Definition (Lean source)
Nonzero forward direct edge γ ≠ 0. @realizes gamma(γ ≠ 0)
Definition (Lean source)
Nonzero reverse direct edge δ ≠ 0. @realizes delta(δ ≠ 0)
Definition (Lean source)
Forward bivariate LvLiNGAM class membership of an observational law P ∈ Laws(ℝ²): there exist a probability space (Ω, μ), centered independent non-Gaussian sources S with finite moments through K = 2m + 2, an observed pair (X, Y), and forward loadings (γ, ρ) realizing all six forward modeling assumptions, such that P is the pushforward law of (X, Y) under μ. This is the existential class of laws (not a witness bundle for fixed data): the witnesses are quantified, the sources are centered, and P is pinned as the pushforward law.
Definition (Lean source)
Reverse bivariate LvLiNGAM class membership of an observational law P ∈ Laws(ℝ²), reverse-parameterized: existential centered independent non-Gaussian sources and reverse loadings (δ, σ) whose pushforward law is P.
Definition (Lean source)
A forward LvLiNGAM representation of an observational law by a specified parameter consists of centered independent non-Gaussian sources whose stated loadings and cumulants generate that law.
Definition (Lean source)
A reverse LvLiNGAM representation of an observational law by a specified parameter consists of centered independent non-Gaussian sources whose stated loadings and cumulants generate that law.
Definition (Lean source)
Handles 150 declarations
Each causal direction has an effective numerical encoding and decoding.
Provides the stated computational structure for this data type.
Formal statement
Provides an effective numerical encoding for this finite data type.
Definition (Lean source)
Worked compatibility incidence systems A_m — the explicit complex full-fiber incidence equations at the two worked cases m = 1 (K = 4, the 12-equation system A_1) and m = 2 (K = 6, the 25-equation system A_2). A pair (θ, η) of complex loading-and-cumulant lists is in the system iff its forward and reverse simultaneous binary-form decompositions agree at every retained coordinate (r, a) through order K = 2m + 2 — the 12 scalar equations t_{r,a} = c_{0r}γ^a + c_{1r}ρ^a + c_{2r}1{a=r} = d_{0r}1{a=0} + d_{1r}σ^{r-a} + d_{2r}δ^{r-a} for m = 1, and the analogous 25 for m = 2 — and at least one of the two generic-locus inequations holds (θ ∈ Θ^{right,∘} or η ∈ Θ^{left,∘}), matching the paper's generic-locus disjunction. These are the explicit complex incidence equations the note requests (not a real-image complexification). The stated common-axis subfamily is workedCompatibilityCommonAxis below, which is a subset of this system (recorded in oeq:generic-exceptional-locus).
Definition (Lean source)
Common-axis subfamily of the worked incidence systems A_m (m ∈ {1, 2}). Shared across both worked cases: the first latent slope vanishes on both arrows (ρ_1 = 0, σ_1 = 0, read off the loading families at the first middle index), the direct edges are reciprocal (δγ = 1), and the weight relations d_{0r} = c_{1r}, d_{1r} = c_{m+1,r}, d_{m+1,r} = c_{0r}γ^r hold on the retained band (for m = 1 these are d_{1r} = c_{2r}, for m = 2 d_{1r} = c_{3r}; the m = 2-only relations σ₂ρ₂ = 1, d_{2r} = c_{2r}ρ₂^r specialise the same pattern).
Definition (Lean source)
Worked compatibility systems A_m (m ∈ {1, 2}) — the full object the paper's def:worked-compatibility-instances defines, bundled so the extracted definition carries both the explicit incidence system and its common-axis subfamily with all its explicit parameter relations (not only the incidence equations):
Definition (Lean source)
Compactly-supported real feasible region: like realFeasibleRegion but each source law is additionally required to be compactly supported (supported in a bounded set). This is strictly stronger than realFeasibleRegion, which allows arbitrary realizing non-Gaussian laws.
Definition (Lean source)
Real lower-order twin construction handle: existence of forward and reverse parameters whose source cumulant lists are realized by compactly supported non-Gaussian laws (obtained through the truncated-moment-matrix perturbation), and whose axis-conditioned simultaneous binary-form decompositions agree through the one-order-lower truncation K₋ = 2m + 1.
Definition (Lean source)
A cumulant vector has exactly the finite atlas coordinate band 2 ≤ r ≤ 2m+2, 0 ≤ a ≤ r; every other coordinate is zero.
Definition (Lean source)
Real exceptional-locus atlas handle, forward incidence set Γ_right = {(t, λ) : J_m(t) = 0, Φ^right(λ) = t, right-loading inequalities, Q_K(λ) for every source}, the project's own statable reduction. Here J_m(t) = 0 is realized as t ∈ \bar E_m(ℝ) (membership of the complexified observable in the compatibility closure), the right-loading inequalities are the nonzero direct slope and pairwise-distinct finite slopes, and Q_K is the finite atomic (Hankel-PSD) certificate on each source cumulant list. The reverse mirror is realAtlasHandleReverse. The simultaneous sign-invariant CAD stratification (interface I-3) and the atomic-certificate ↔ real-source equivalence (interface I-4) are external and not built here.
Definition (Lean source)
Real exceptional-locus atlas handle, reverse incidence set Γ_left = {(t, λ) : J_m(t) = 0, Φ^left(λ) = t, left-loading inequalities, Q_K(λ)} — the reverse mirror of realAtlasHandle, supplying the reverse incidence component the paper's atlas requires.
Definition (Lean source)
Forward atlas section over an observable t: the t-fiber of the forward incidence set Γ_right, i.e. the local description of R^right_{m,K}(t) ∩ F^right that the atlas outputs cellwise. (The section varies with t; the finite sign-invariant CAD t-cell stratification that makes it constant per cell is the external interface I-3.)
Definition (Lean source)
Reverse atlas section over t: the t-fiber of Γ_left (local description of R^left_{m,K}(t) ∩ F^left).
Definition (Lean source)
Forward atlas nonemptiness label ε^right(t): whether the forward incidence stack over t is nonempty — the cell label the CAD stratification attaches.
Definition (Lean source)
Reverse atlas nonemptiness label ε^left(t).
Definition (Lean source)
Coordinates of the full CAD incidence system: observable coordinates, loading/cumulant coordinates, and the atomic (w,z) witnesses.
Definition (Lean source)
Equality between indices of the atlas-incidence coordinate system can be decided.
Definition (Lean source)
Equality between real polynomials in the atlas-incidence coordinates can be decided.
Definition (Lean source)
Evaluation of a full incidence polynomial at (t, λ, w, z).
Definition (Lean source)
A finite polynomial sign presentation is generated from, and defines exactly, one of the two incidence sets Γ_b, including its atomic witnesses.
Definition (Lean source)
The block occupied by a concrete coordinate of the full incidence system.
Definition (Lean source)
Every coordinate occurring in an incidence polynomial occurs in the CAD list, and its actual list position obeys the recursive lifting/elimination order: atomic witnesses first, then λ, then the observable base t. The Lean CAD recursion peels and erases the head of this list, so this is the typed orientation of the paper's conventional base-first description t, then λ, then witnesses. Thus the prescribed block relation is a property of order itself, not a separately quantified relation unrelated to the incidence coordinates.
Definition (Lean source)
The projection family is generated stage-by-stage from the incidence presentation in an order containing all of its variables in the required blocks.
Definition (Lean source)
The real exceptional locus in the finite observable coordinate space used by the incidence handles: membership in bar E_m(ℝ) together with zero coordinates off the retained band 2 ≤ r ≤ 2m+2, 0 ≤ a ≤ r.
Definition (Lean source)
A retained-observable cell of the paper's finite cumulant coordinate space ℝ^{q_K}: after the off-band coordinates are pinned to zero (bandSupportedCumulants (2m+2)), it is cut out by finitely many real polynomial sign conditions.
Definition (Lean source)
A polynomial has constant sign on a cell.
Definition (Lean source)
A polynomial has the same sign at every pair of observable cumulant vectors in the cell.
Definition (Lean source)
Cylindricity of observable cells in lexicographic (r,a) order: whenever two cells meet over the same prefix, their projections to that prefix coincide.
Definition (Lean source)
A full point of the CAD incidence space, including the atomic witnesses.
Definition (Lean source)
An actual finite, simultaneous CAD atlas. All arrays are indexed by Fin, so finiteness is data rather than an existential proposition. Its selected cells live in the full (t, λ, w, z) coordinate space, arise by recursive lifting from the incidence-generated projection family, and project exactly to the two feasible fibers over every observable base cell.
Definition (Lean source)
Coordinates remaining after the atomic moment witnesses have been eliminated: the retained observable coordinates t, followed by the structural coordinates lambda.
Definition (Lean source)
A point of the witness-eliminated (t, lambda) coordinate space.
Definition (Lean source)
Coordinates of the complex generic two-arrow incidence used in Step 2: observable cumulants, forward parameters, reverse parameters, and one saturation coordinate for each arrow-genericity product. Atomic real moment witnesses do not occur in this coordinate type.
Definition (Lean source)
Evaluation of a witness-eliminated fiber polynomial at (t, lambda).
Definition (Lean source)
Equality on the witness-eliminated coordinate index.
Definition (Lean source)
The variable block occupied by a witness-eliminated fiber coordinate.
Definition (Lean source)
The recursive fiber CAD eliminates the structural lambda prefix before reaching the observable base. Since IsRecursivelyLiftedCADCell peels the head of its order, every displayed loading/cumulant coordinate must precede every displayed observable coordinate.
Definition (Lean source)
Equality on observable polynomials used by the finite sign-oracle program.
Definition (Lean source)
Provides a procedure that decides whether two coordinates of the complex generic two-arrow incidence space are equal.
Definition (Lean source)
Provides a procedure that decides whether two complex polynomials in the generic two-arrow incidence coordinates are equal.
Definition (Lean source)
Provides a procedure that decides whether two complex polynomials in the observable cumulant coordinates are equal.
Definition (Lean source)
One exhaustive row of the finite exact-real sign-oracle lookup program.
Definition (Lean source)
A finite sign-oracle program. Its only real-number primitive is exact sign evaluation of the displayed finite polynomial test list; no computable comparison operation on arbitrary real inputs is asserted.
Definition (Lean source)
The only non-discrete primitive used when an atlas program is evaluated: an exact sign query for a displayed observable polynomial.
Definition (Lean source)
An oracle answers each query by the mathematical sign of the corresponding real polynomial value. This is an exact-real oracle contract, not a claim that comparison of arbitrary real numbers is Turing computable.
Definition (Lean source)
Evaluate the finite lookup program relative to an exact-sign oracle. Once the finite sign answers are supplied, this is ordinary executable list lookup; no noncomputable comparison on ℝ occurs in this interpreter.
Definition (Lean source)
The canonical mathematical exact-sign oracle.
Definition (Lean source)
The canonical sign oracle is exact: for every displayed observable polynomial and every vector of observable cumulants it returns the mathematical sign of the real value that polynomial takes there.
Formal statement
Proof (Lean source)
Families carried between the full incidence, witness-eliminated fiber, and observable stages of the certified symbolic construction.
Definition (Lean source)
View an observable polynomial family inside the full incidence coordinate space. This is how the dependent intersection basis is supplied to the final simultaneous real CAD/QE job.
Definition (Lean source)
Operations appearing in the paper's finite elimination/projection/lifting construction trace.
Definition (Lean source)
Atlas trace operations have a decidable equality test: any two operations can be effectively determined to be the same or different.
Definition (Lean source)
Every atlas trace operation has an effective numerical encoding and decoding.
Definition (Lean source)
The three rational algebra jobs used by the paper-specific atlas. The general cited interface also supports Gaussian-rational jobs, but this atlas starts from rational incidence equations and casts their outputs to ℂ, so its Gaussian batch is empty.
Definition (Lean source)
The three rational algebra jobs of the paper-specific atlas have a decidable equality test: any two of them can be effectively determined to be the same or different.
Definition (Lean source)
Each of the three rational algebra jobs of the paper-specific atlas can be encoded as a natural number and decoded back, so the type is countable.
Definition (Lean source)
One primitive operation charged by the cited effective computations, with both its paper-side source job and its cited high-level trace stage retained. This is the bridge between the semantic atlas trace and the primitive cost model; it is deliberately unrelated to partial-recursive machine fuel.
Definition (Lean source)
The actual combined cited result consumed by one paper-specific atlas: exactly two rational incidence-elimination jobs, one rational observable-ideal intersection job, no Gaussian-rational job, and one rational CAD/QE job. The three machine codes are kept distinct, as in the cited combined interface.
Definition (Lean source)
The observable intersection job constructed by the dependent cited run.
Definition (Lean source)
The rational CAD job consuming the exact dependent intersection result.
Definition (Lean source)
The dependent execution, viewed as the three-result batch used by the generic combined cost bookkeeping.
Definition (Lean source)
The rational job list supplied to the combined cited bound.
Definition (Lean source)
The paper-specific Gaussian-rational job list is exactly empty.
Definition (Lean source)
Primitive charges of the specialized three-job rational batch, retaining which of the forward, reverse, or intersection results produced each charge.
Definition (Lean source)
Primitive charges of rational CAD source steps, indexed from a supplied offset so the paper-side slice can point back to the exact source step.
Definition (Lean source)
Primitive charges of the one rational real-CAD/QE result.
Definition (Lean source)
Charging a real-algebraic CAD trace bills exactly one primitive charge per primitive operation: the resulting charge list is as long as the total number of primitive operations recorded across the trace steps. The offset at which the source steps are indexed does not change the count.
Formal statement
Proof (Lean source)
Complete cited primitive stream for the paper-specific combined run. No Gaussian charges occur because gaussianResults is indexed by the empty job list.
Definition (Lean source)
The exact operation count on the left side of the cited combined bound.
Definition (Lean source)
The completed forward job stored in the specialized rational batch.
Definition (Lean source)
The completed reverse job stored in the specialized rational batch.
Definition (Lean source)
The completed observable-ideal intersection job stored in the specialized rational batch.
Definition (Lean source)
Rename a finite rational polynomial family into a displayed coordinate type and extend coefficients to ℂ. The embedding is explicit, so finite effective coordinates cannot be silently identified with unrelated paper coordinates.
Definition (Lean source)
Rename a finite rational polynomial family into a displayed coordinate type and extend coefficients to ℝ.
Definition (Lean source)
Rename a rational family after elimination, when only the variables that actually occur in the family must embed into the smaller retained coordinate space. This is the correct transport for (t, lambda) and observable outputs: the eliminated full-space coordinates need no image.
Definition (Lean source)
Real counterpart of the previous transport: rename a finite rational polynomial family into a displayed coordinate space and extend its coefficients to the reals, requiring only the variables that actually occur in the family to receive an image. This is the transport used for the (t, lambda) fiber and observable outputs, where the eliminated coordinates need no image.
Definition (Lean source)
Rename an already-real projected CAD family onto the displayed paper coordinate space. This is the transport used after the cited recursive prefix projection; it performs no additional elimination.
Definition (Lean source)
Transport one cited rational sign-test code to observable coordinates. The sign attached to the code is transported separately and unchanged.
Definition (Lean source)
Extend one finite cited CAD assignment along the exact incidence-coordinate embedding, using zero only outside the supplied finite coordinate image.
Definition (Lean source)
Observable component of a finite cited CAD assignment.
Definition (Lean source)
Witness-forgotten (t, lambda) component of a finite cited CAD assignment.
Definition (Lean source)
Erasing two consecutive lifting prefixes is the same geometric projection as erasing their concatenation. This is the compatibility used by the witness-to-fiber and fiber-to-observable transports.
Formal statement
Proof (Lean source)
A coordinate map is faithful on all variables that actually occur in a displayed polynomial family. It need not inject the already-eliminated ambient coordinates into the smaller output space.
Definition (Lean source)
Interpret one actual rational CAD trace code-family in a displayed real or complex atlas coordinate type, using an explicit finite-coordinate embedding. Every branch ends in an equality of polynomial families, not an opaque label.
Definition (Lean source)
A cited truth/retention query is exactly one of this paper's displayed full-incidence sign conditions after the fixed full-coordinate embedding.
Definition (Lean source)
A CAD-source primitive belongs to the indicated indexed cited trace step, including exact agreement of the source high-level operation.
Definition (Lean source)
The explicit primitive stream has exactly the combined cited count.
Formal statement
Proof (Lean source)
A cited primitive may be assigned only to the atlas operation consuming its source job. Rational algebra charges go to the corresponding forward, reverse, or intersection step; CAD charges stay on real projection/lifting or witness-retention steps. The real/imaginary coefficient reinterpretation is therefore necessarily an uncharged semantic step.
Definition (Lean source)
A declared input/output step of the finite symbolic atlas construction, together with its contiguous slice of the cited primitive stream.
Definition (Lean source)
Operation-specific linkage from one high-level atlas step to one actual step of the cited rational CAD result. Its inputs and output must be populated by the source step's decoded polynomial code families after explicit finite coordinate renaming.
Definition (Lean source)
Exactly the operations sourced from the rational CAD/QE result.
Definition (Lean source)
Real polynomial-family variants used by the rational CAD/QE branch.
Definition (Lean source)
Basic family shape for a cited CAD algebra/projection-closure step. Its full polynomial semantics comes from IsLinkedToCitedCADStep, which identifies the actual semantically certified source step and its decoded families.
Definition (Lean source)
The common real zero set of a finite observable polynomial family.
Definition (Lean source)
Evaluate the complex generic two-arrow incidence at (t, theta, eta, s).
A finite complex polynomial family presents the generic two-arrow incidence with the indicated arrow's genericity product saturated. This is the Step-2 incidence whose elimination produces observable equations for bar E_m; it is separate from the Step-3 real incidence with atomic moment witnesses.
Definition (Lean source)
The common complex zero set of a finite observable polynomial family.
Definition (Lean source)
Complex Zariski closure of the observable projection of the saturated generic two-arrow incidence. This is complex algebraic elimination only; it does not describe projection over real atomic witnesses.
Definition (Lean source)
A finite complex observable family cuts out exactly the complex projection closure of a saturated generic incidence.
Definition (Lean source)
Restriction of a full incidence assignment to the witness-eliminated (t, lambda) coordinates.
Definition (Lean source)
Zariski closure of a real projection, retained only as a diagnostic notion used by the counterexample module. It is deliberately not the semantics of any atlas construction-trace operation: complex Groebner elimination cannot compute this real witness projection.
Definition (Lean source)
Diagnostic predicate for exact real witness projection. The effective atlas does not require this predicate; Step 4 eliminates witnesses cellwise instead.
Definition (Lean source)
Operation-specific semantics for every symbolic trace step. Saturation and Groebner elimination act only on the complex generic two-arrow incidence and produce complex observable equations. Real atomic witnesses are removed later, cellwise, by witnessCellRetention; they are never assigned complex-elimination semantics.
Definition (Lean source)
Exact arithmetic/sign-operation charge for one certified atlas step: the length of its displayed slice of the cited primitive execution.
Definition (Lean source)
Complex-incidence families read or emitted by a trace step.
Definition (Lean source)
Complex-observable families read or emitted by a trace step.
Definition (Lean source)
Incidence-coordinate families read or emitted by a trace step.
Definition (Lean source)
Witness-eliminated fiber families read or emitted by a trace step.
Definition (Lean source)
Observable families read or emitted by a trace step.
Definition (Lean source)
An observable polynomial has constant mathematical sign on a base cell.
Definition (Lean source)
A trace step has the correct symbolic stage shape. In particular, the three CAD projection operations are not mere labels: their output family is definitionally the corresponding shared generic CAD operator applied to the declared input family. The remaining operations change or preserve stages as specified by the paper's elimination/lifting pipeline; their global correctness is certified by the endpoint, retained-cell, and exact-section fields of EffectiveRealAtlasOutput.
Definition (Lean source)
An observable polynomial family explicitly presents every base cell.
Definition (Lean source)
A finite construction trace starts Step 2 from the two complex generic incidences, produces their observable elimination ideals and their intersection, then runs real CAD and Step-4 witness-cell retention on the separately displayed real incidence and (t, lambda) families.
Definition (Lean source)
Exact accounting consequence of the slice certificate: the high-level atlas total is the combined cited primitive count.
Formal statement
Proof (Lean source)
Rational finite syntax for a polynomial. Coefficients and exponent lists are discrete data suitable for a genuine machine encoding.
Definition (Lean source)
Finite rational syntax for a polynomial — its list of coefficients with exponent lists — can be encoded as a natural number and decoded back, so the type of polynomial codes is countable whenever its variables are.
Definition (Lean source)
Finite syntax for one recursively lifted CAD cell. The six constructors record the zero-dimensional point and all five lifting cases of IsRecursivelyLiftedCADCell: a root-free whole fibre, a root section, and the three lower/bounded/upper sectors. Root indices are exact symbolic indices in the ordered real-root stack; evaluating signs or comparing arbitrary reals is not part of this discrete code.
Definition (Lean source)
Finite syntax for one recursively lifted CAD cell can be encoded as a natural number and decoded back, so the type of cell codes is countable.
Definition (Lean source)
Forget the effective cited certificate's rational root presentations and sign row while retaining its exact recursive CAD-cell shape and root indices.
Definition (Lean source)
Exact interpretation of finite cell syntax in the generic recursive CAD cell language. This ties every machine-emitted geometry code to the actual section/sector set it denotes, rather than merely recording a constructor tag.
Definition (Lean source)
Interpret rational polynomial syntax as an actual real multivariate polynomial.
Definition (Lean source)
Entire discrete symbolic payload emitted by the atlas construction machine. Every polynomial list is rational syntax; the fields of EffectiveRealAtlasOutput below identify its real interpretation with the actual incidence, fiber, base, and sign-test families.
Definition (Lean source)
Every encoded atlas construction, including its finite polynomial and trace data, has an effective numerical encoding and decoding.
Definition (Lean source)
A real polynomial family is exactly the interpretation of a displayed list of rational polynomial codes.
Definition (Lean source)
Interpret the same rational syntax as a complex polynomial.
Definition (Lean source)
A complex polynomial family is exactly the interpretation of rational polynomial codes.
Definition (Lean source)
Every intermediate family in a machine payload decodes, in order, to the corresponding family actually read or emitted by the certified trace.
Definition (Lean source)
Every complex intermediate family in the payload decodes to the family actually read or emitted by the certified Step-2 trace.
Definition (Lean source)
Encode the three-valued sign alphabet by natural numbers for the machine payload.
Definition (Lean source)
A concrete halting partial-recursive run producing the complete finite symbolic payload. Its output is required to be the Encodable code of the payload actually used by the atlas, so the effectivity witness cannot be an unrelated existence Prop. The existential evaln fuel witnesses halting only; it is not compared with the separate real-algebraic arithmetic/sign-operation count.
Definition (Lean source)
Observable-coordinate count q_K, for K = 2m+2.
Definition (Lean source)
Structural-coordinate count p_K = (m+2)K-1.
Definition (Lean source)
Number of real coordinates in the simultaneous two-arrow incidence input.
Definition (Lean source)
Explicit degree bound from the cumulant/moment equations and the two genericity-saturation products.
Definition (Lean source)
The concrete incidence presentation has a positive degree envelope. This is derived from the displayed formula, rather than assumed by the atlas theorem, and supplies the 1 ≤ D domain premise of the cited complexity interface.
Formal statement
Proof (Lean source)
The largest total degree in one finite polynomial family. This is a paper-side bookkeeping operation: it is evaluated only after the cited elimination output has been returned, so it does not pretend that the pre-elimination incidence bound also bounds a Gröbner basis.
Definition (Lean source)
The largest total degree charged by one supplied algebra job.
Definition (Lean source)
The largest total degree charged by one supplied CAD input. Generated CAD projection polynomials are outputs of the cited run and are deliberately not reclassified as inputs in this envelope.
Definition (Lean source)
The largest total degree occurring in a finite polynomial family is a valid uniform degree envelope for that family: every member has total degree at most that maximum.
Formal statement
Proof (Lean source)
The largest total degree charged by an algebra job is a valid uniform degree bound for it: both input families and the saturating polynomial have total degree at most that maximum.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of atlas CADJob degree Bounded By maximum.
Formal statement
Proof (Lean source)
Post-elimination degree envelope for the actual paper execution. In addition to the exact source-incidence degree, this finite maximum charges the two supplied elimination jobs, their returned saturated elimination bases, the dependent intersection job and its returned intersection basis, and the CAD input that consumes that basis.
Definition (Lean source)
Proves the stated mathematical property of atlas Source Degree Bound le charged.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of atlas Charged Degree Bound positive.
Formal statement
Proof (Lean source)
The finite maximum really bounds every input and returned basis charged by the dependent two-arrow elimination/intersection pipeline.
Formal statement
Proof (Lean source)
The same charged maximum bounds the exact CAD input. The generated CAD projection family is intentionally absent: it is an output, not an input to the universal complexity call.
Formal statement
Proof (Lean source)
Explicit size and complexity receipt for the finite symbolic construction. The source-incidence bound remains the displayed cumulant-equation formula; the distinct charged bound is chosen after the cited elimination pipeline and is the degree parameter used by the combined complexity theorem.
Definition (Lean source)
The paper-specific effective/evaluable real exceptional atlas output.
Definition (Lean source)
The output shape of the paper's atlas handle at complexity m: the engine returns a value of RealAtlasCADData m. This is a definition of what the handle emits, not an assertion that it exists. It is retained as an unasserted name for the weaker raw-CAD output shape. The proved paper-specific theorem concludes the strictly richer Nonempty (EffectiveRealAtlasOutput m), which also carries finite sign-table evaluators and their exactness certificates.
Definition (Lean source)
Real exceptional-locus atlas handle — the CITED external interface (I-3).
Definition (Lean source)
Helpers.AdmissibleSwaps 12 declarations
The admissible middle-block relabeling, as a permutation of all source indices.
Definition (Lean source)
Relabeling the middle source indices while keeping the two endpoint indices fixed does not change a finite sum.
Formal statement
Proof (Lean source)
After an admissible source relabeling, each forward loading equals the original loading at the correspondingly relabeled source.
Formal statement
Proof (Lean source)
After an admissible source relabeling, each reverse loading equals the original loading at the correspondingly relabeled source.
Formal statement
Proof (Lean source)
The forward cumulant map is unchanged by any admissible relabeling of the middle sources.
Formal statement
Proof (Lean source)
The reverse cumulant map is unchanged by any admissible relabeling of the middle sources.
Formal statement
Proof (Lean source)
Extend a permutation of the middle slopes by fixing the leading direct-slope index.
Definition (Lean source)
If the direct slope together with all latent slopes are distinct, they remain distinct after permuting the latent slopes.
Formal statement
Proof (Lean source)
The real feasible parameter region is closed under admissible relabeling of the middle sources.
Formal statement
Proof (Lean source)
A forward axis model remains a forward axis model when middle sources and their parameters are relabeled together.
Formal statement
Proof (Lean source)
A reverse axis model remains a reverse axis model when middle sources and their parameters are relabeled together.
Formal statement
Proof (Lean source)
The admissible-swap orbits tagged as forward and reverse are disjoint, regardless of their parameter values.
Formal statement
Proof (Lean source)
Helpers.ApolarDefs 3 declarations These realize the divided-power blocks f_r, the constant-coefficient differential operator q(∂), and the squarefree degree-n support annihilator Q_D = ∏_{ℓ ∈ D} ℓ^⊥ used in the common-contraction-kernel identity ker = ⟨Q
Divided-power binary forms, apolar contraction, and the support annihilator
These realize the divided-power blocks f_r, the constant-coefficient differential
operator q(∂), and the squarefree degree-n support annihilator
Q_D = ∏_{ℓ ∈ D} ℓ^⊥ used in the common-contraction-kernel identity ker = ⟨Q_D⟩.
Divided-power binary form of the order-r cumulant block: f_r(x, y) = Σ_{a=0}^r C(r,a) t_{r,a} x^{r-a} y^a (with x = X 0, y = X 1).
Definition (Lean source)
Apply the constant-coefficient differential operator q(∂) (with ∂ = (∂_x, ∂_y)) to a binary form f: q(∂) f = Σ_d (coeff_d q) ∂_x^{d 0} ∂_y^{d 1} f.
Definition (Lean source)
Squarefree degree-n support annihilator Q_D = ∏_{j} ℓ_j^⊥, the product over all n = m + 2 projective loading directions of the linear form perpendicular to u_j = (u_{j1}, u_{j2}), namely u_{j2} · X 0 - u_{j1} · X 1.
Definition (Lean source)
Helpers.ApolarKernel 6 declarations
Each linear factor C b * X0 - C a * X1 is nonzero when (a,b) ≠ (0,0).
Formal statement
Proof (Lean source)
For the forward loading family, the index-(m+1) factor equals X 0, so X 0 ∣ Q_D.
Formal statement
Proof (Lean source)
X 1 ∤ Q_D for the forward loading when its finite slopes are nonzero.
Formal statement
Proof (Lean source)
Mirror fixed-axis divisibility for the reverse loading family.
Formal statement
Proof (Lean source)
Mirror nondivisibility for the reverse loading family.
Formal statement
Proof (Lean source)
The support annihilator vanishes at every listed direction. This is the easy inclusion of the support-annihilator line in the apolar evaluation kernel.
Formal statement
Proof (Lean source)
Helpers.ApolarKernelAux 3 declarations
The support annihilator is a binary form of degree m + 2.
Formal statement
Proof (Lean source)
The reverse support-annihilator line lies in the common contraction kernel.
Formal statement
Proof (Lean source)
The roots of the default forward finite-slope polynomial are its slopes.
Formal statement
Proof (Lean source)
Helpers.ApolarKernelDiff 5 declarations Linear forms attached to loading directions
Linear forms attached to loading directions
The binary linear form associated with a loading direction.
Evaluation of a differential symbol at a loading direction.
Definition (Lean source)
A retained forward divided-power cumulant block is the corresponding sum of loading-direction powers.
Formal statement
Proof (Lean source)
The corresponding retained reverse divided-power cumulant block.
Formal statement
Proof (Lean source)
Applying a homogeneous differential symbol to a loading-direction power.
Formal statement
Proof (Lean source)
Helpers.ApolarKernelIdentity 9 declarations
Evaluation at a direction is the eval₂ used by the support-annihilator lemma, so the latter can be used directly in apolar calculations.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of diff Apply sum.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of diff Apply C mul.
Formal statement
Proof (Lean source)
The easy half of the apolar kernel calculation: a homogeneous form that vanishes on every loading direction annihilates every retained contraction.
Formal statement
Proof (Lean source)
The support-annihilator line is contained in the common contraction kernel. This is the backwards implication of the desired ker = ⟨Q_D⟩.
Formal statement
Proof (Lean source)
The genuine (un-charted) weighted block-contraction map. Its injectivity is exactly the rank-open condition needed in the forward implication.
Definition (Lean source)
Under injectivity of the actual weighted contraction map, the common contraction equations force every directional evaluation to vanish.
Formal statement
Proof (Lean source)
The binary interpolation step: a degree-m+2 homogeneous binary form vanishing on the m+1 finite forward directions and on the direction at infinity is a multiple of their support annihilator.
Formal statement
Proof (Lean source)
Forward apolar kernel identity. This is the actual common-kernel statement used by the flagship: among homogeneous degree-m+2 binary forms, the simultaneous contractions with orders m+2,…,2m+2 have exactly the support-annihilator line as their kernel.
Formal statement
Proof (Lean source)
Helpers.ApolarQD 8 declarations A default polynomial for a prescribed finite multiset of roots
A default polynomial for a prescribed finite multiset of roots
The monic polynomial with the given multiset of complex roots.
Definition (Lean source)
The default root polynomial is nonzero because every linear factor is nonzero.
Proof (Lean source)
The roots of qDefault have exactly the prescribed multiplicities.
Proof (Lean source)
Distinct prescribed roots make the default root polynomial squarefree.
Formal statement
Proof (Lean source)
If zero is absent from the prescribed roots, the default root polynomial is nonzero at zero.
Formal statement
Proof (Lean source)
The finite slopes in the forward parametrization: the direct slope followed by the latent slopes.
Definition (Lean source)
Genericity makes the direct and latent finite slopes pairwise distinct.
Formal statement
Proof (Lean source)
Under genericity and nonzero latent slopes, zero is absent from the forward slope multiset.
Formal statement
Proof (Lean source)
Helpers.ApolarRankBridge 10 declarations
Defines the mathematical object called the binary Dehom.
Definition (Lean source)
Proves the stated mathematical property of coeff binary Dehom lin Form pow.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of coeff binary Dehom lin Form pow'.
Formal statement
Proof (Lean source)
The selected weighted-contraction coefficient matrix, exposed independently of parameter polynomials so observable contraction minors can factor through it.
Definition (Lean source)
Explicit retained-band parameter at which the selected contraction matrix is nonsingular.
Definition (Lean source)
At the explicitly constructed witness parameter, and whenever there is at least one latent source slot, the selected forward weighted-contraction matrix has nonzero determinant. This exhibits a single point at which the contraction minor is nonsingular, which is what makes the corresponding minor polynomial not identically zero.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of forward Contraction Minor Witness loading cast Succ.
Formal statement
Proof (Lean source)
Proves that the map or coordinate assignment called the forward Contraction Minor Witness slope is injective.
Proof (Lean source)
Proves the stated mathematical property of forward Contraction Minor Witness loading last.
Formal statement
Proof (Lean source)
Injectivity of the genuine contraction holds on the principal open set cut out by the determinant of an explicit coefficient minor. The polynomial is nonzero at an explicit witness whose weights vanish outside the pinned degree band.
Formal statement
Proof (Lean source)
Helpers.ArrowPolynomialGeometry 15 declarations For a degree-m+2 differential operator divisible by X 1, use the monomial basis X 0 ^ (m+1-b) * X 1 ^ (b+1), 0 ≤ b < m+2.
An observable common-axis contraction minor
For a degree-m+2 differential operator divisible by X 1, use the monomial
basis X 0 ^ (m+1-b) * X 1 ^ (b+1), 0 ≤ b < m+2. We retain the scalar
contraction at order m+2 and every coefficient of the degree-m contraction
at order 2m+2. Up to nonzero row factors, the resulting observable matrix is
t_(m+2,b+1) in its first row and
choose(m,a) * t_(2m+2,a+b+1) in row a+1.
Every reverse loading list contains (1,0). The direction-evaluation factor
of this matrix therefore has a zero row, so its determinant vanishes on the
whole reverse arrow variety. On the forward common-axis family the same zero
row is supplied by the loading (1,ρ₀)=(1,0).
A cumulant-valued map whose scalar coordinates are polynomials in all structural parameter coordinates.
Definition (Lean source)
Proves that the map called the forward Cumulant Map is Polynomial is polynomial.
Formal statement
Proof (Lean source)
Proves that the map called the reverse Cumulant Map is Polynomial is polynomial.
Formal statement
Proof (Lean source)
The closure of the image of an affine polynomial map is irreducible.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of forward Cumulant Image Variety is Irreducible.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of reverse Cumulant Image Variety is Irreducible.
Formal statement
Proof (Lean source)
The explicit observable contraction matrix restricted to operators divisible by the horizontal-axis annihilator X 1.
Definition (Lean source)
The observable contraction-minor polynomial detecting the presence of the horizontal direction in a length-m+2 power decomposition.
Definition (Lean source)
Evaluating the horizontal contraction-minor polynomial at the retained cumulants of a cumulant vector returns the determinant of the explicit numerical contraction matrix built from those same cumulants. The polynomial is therefore just a symbolic name for that determinant.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of horizontal Contraction Minor Polynomial reverse vanishes.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of horizontal Contraction Minor Polynomial forward Common Axis vanishes.
Formal statement
Proof (Lean source)
The observable horizontal-axis contraction minor vanishes on the entire reverse arrow-image variety, not only on its parameterized range.
Formal statement
Proof (Lean source)
The same observable minor vanishes on the Zariski closure of the explicit forward common-axis image family.
Formal statement
Proof (Lean source)
Nonvanishing of the observable minor at the explicit forward block-Vandermonde witness.
Formal statement
Proof (Lean source)
The observable contraction minor is a nonzero polynomial.
Formal statement
Proof (Lean source)
Helpers.BandDimensionTransfer 4 declarations
Proves the stated closedness property for encode Band Param closed iff.
Formal statement
Proof (Lean source)
Proves the stated closedness property for decode Band Param closed.
Formal statement
Proof (Lean source)
Irreducibility is unchanged by passage to finite retained-band coordinates.
Formal statement
Proof (Lean source)
The paper's relative chain dimension is literally the affine chain dimension of the encoded finite-band set.
Formal statement
Proof (Lean source)
Helpers.BandParameterCoordinates 13 declarations
Coordinates of the finite retained-band parameter space. The last Fin (L-1) coordinate represents orders 2, ..., L.
Definition (Lean source)
Read retained coordinates from a function-valued parameter.
Definition (Lean source)
Put a finite coordinate vector back into the function-valued parameter space, setting every off-band weight to zero.
Definition (Lean source)
A parameter point read off from a finite vector of retained coordinates is always band supported: every source weight of an order below two or above L vanishes.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of encode decode Band Param.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of decode encode Band Param.
Formal statement
Proof (Lean source)
The actual retained-band subtype is equivalent to an ordinary finite complex affine space.
Definition (Lean source)
Embed a finite band coordinate among the original natural-number-indexed polynomial variables.
Definition (Lean source)
Distinct retained coordinates name distinct parameter variables: for a truncation order of at least two, the embedding of the finite band coordinates into the original parameter coordinates is injective.
Formal statement
Proof (Lean source)
Restrict an original parameter polynomial to the retained band by setting all off-band weight variables to zero.
Definition (Lean source)
Restricting a parameter polynomial to the retained band and evaluating it at a finite coordinate vector gives the same number as evaluating the original polynomial at the parameter point those coordinates decode to. Killing the off-band weight variables therefore loses no information, provided the truncation order is at least two.
Formal statement
Proof (Lean source)
Gives the stated evaluation formula for eval rename band Coord Embedding.
Formal statement
Proof (Lean source)
Relative closure in the paper's retained-band ambient becomes ordinary affine algebraic closure under finite-coordinate encoding.
Formal statement
Proof (Lean source)
Helpers.BandWeightKernelDimension 5 declarations
The tangent space obtained by fixing every loading slope and allowing each retained order's source weights to move in its synthesis kernel.
Definition (Lean source)
The retained-band kernel is the product of its independent order blocks.
Definition (Lean source)
Establishes the stated dimension formula for band Weight Kernel.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of retained kernel sum.
Formal statement
Proof (Lean source)
At the flagship retained order, the independent low-order weight kernels have total dimension m(m-1)/2.
Formal statement
Proof (Lean source)
Helpers.CAD.CADInterface 46 declarations Semialgebraic subsets of ℝ^r
Semialgebraic subsets of ℝ^r
The affine space ℝ^r the cited decomposition lives in.
A basic semialgebraic subset of ℝ^r: the common solution set of finitely many polynomial equations, finitely many non-strict polynomial inequalities and finitely many strict polynomial inequalities. These are the sets the cells are cut out by.
Definition (Lean source)
A semialgebraic subset of ℝ^r: a finite union of basic semialgebraic sets.
Definition (Lean source)
Regard a multivariate polynomial as a univariate polynomial in the selected CAD lifting variable, with all other variables retained in its coefficient ring.
Definition (Lean source)
Delete the current leading term when P is regarded as a polynomial in x. Iterating this operation gives BPR's successive truncations/reducta.
Definition (Lean source)
A coefficient lies in the real ground field, rather than depending on any remaining variable. Using empty variable support makes the predicate decidable for the finite projection algorithm; over MvPolynomial σ ℝ it is equivalent to being a constant polynomial.
Definition (Lean source)
A nonzero member of the real ground field.
Definition (Lean source)
The leading coefficient in the selected lifting variable.
Definition (Lean source)
Successive BPR truncations with their exact stopping rule. A nonzero current reductum is retained. Recursion continues only when its leading coefficient is not a nonzero ground-field constant; zero terminates immediately. The fuel is the original x-degree plus one.
Definition (Lean source)
Every relevant nonzero truncation/reductum of P in the selected variable, exactly stopping at a nonzero ground-field leading coefficient as in BPR's Tru(P).
Definition (Lean source)
The nonzero reducta of every polynomial in a finite stage family.
Definition (Lean source)
Every generated reductum is nonzero.
Formal statement
Proof (Lean source)
A nonzero polynomial occurs as the zeroth member of its own reducta family.
Formal statement
Proof (Lean source)
The zero polynomial contributes no reductum.
Formal statement
Proof (Lean source)
The empty stage has no reducta.
Formal statement
Proof (Lean source)
Focused zero-polynomial receipt: filtering is preserved after taking a family union.
Formal statement
Proof (Lean source)
The coefficient projection operation in variable x.
Definition (Lean source)
The discriminant projection operation in variable x.
Definition (Lean source)
The square leading block of the Sylvester--Habicht matrix at index j. Its rows are the coefficient vectors of X^(q-j-1) P, ..., P, Q, ..., X^(p-j-1) Q in the descending monomial basis; the first p+q-2j columns give the principal subresultant coefficient.
Definition (Lean source)
The unsigned principal subresultant coefficient at index j. BPR uses the signed normalization sRes_j; the two differ by a fixed unit ±1, so they have identical zero loci and constant-sign partitions. This determinant is the actual Sylvester--Habicht principal minor, not Polynomial.resultant with artificially reduced degree parameters.
Definition (Lean source)
In BPR's equal-degree branch, replace R by lcof(S) R - lcof(R) S, whose leading term cancels.
Definition (Lean source)
Derivative principal subresultants of every reductum, with BPR's exact range j = 0, ..., degree(R)-2.
Definition (Lean source)
Pair principal subresultants of all reducta. Unequal degrees put the larger-degree polynomial first and use indices below the smaller degree. Equal degrees use BPR's leading-term-cancelling combination before taking the principal subresultants.
Definition (Lean source)
The derivative and pair principal subresultant coefficients required by BPR Notation 5.15. Ground-field constants are omitted, since their signs are already globally constant.
Definition (Lean source)
One projection step (BPR Notation 5.15): coefficients and discriminants of every nonzero reductum, and all derivative/pair principal subresultants of those reducta.
Definition (Lean source)
The cylindrifying family generated along the supplied order (BPR §11.1): at every round, retain the family computed so far and adjoin its complete BPR elimination family. Thus the next round starts from fam ∪ cadProjectionStep x fam, and the final result contains the input, every nonzero truncation/reductum projection stage, and every later projection of the accumulated family. The foldl shape is load-bearing: replacing the family at each round would leave only the last constants and make lifting vacuous.
Definition (Lean source)
Erase the current lifting coordinate before consulting the recursively constructed base cell.
Definition (Lean source)
The specialization of P at the base point a, leaving only the lifting coordinate x, is not the zero univariate polynomial. This is deliberately stronger than the global condition P ≠ 0: a globally nonzero polynomial can nullify after the base coordinates are fixed.
Definition (Lean source)
The union of the real roots, in the current lifting coordinate, of every polynomial whose specialization at the current base point is nonzero. A polynomial that specializes identically to zero in the lifting variable is ignored, as in standard CAD lifting. This excludes both a globally zero input and a globally nonzero input nullified on the current base cell; without the latter guard, {X₁} lifted first in X₀ would contribute all of ℝ above the base X₁ = 0, contradicting the finiteness required of algebraic sections. Sections are selected from this whole ordered root stack, rather than being required to be the unique root of one polynomial.
Definition (Lean source)
If every member of the stage family specializes to the zero univariate polynomial over a base point, then that base point has no CAD lifting roots.
Formal statement
Proof (Lean source)
Nullified-specialization non-vacuity receipt. The globally nonzero polynomial X₁ specializes identically to zero in the first lifting coordinate over a base point with X₁ = 0, so it contributes no roots there. This is the two-variable counterexample that a merely global P ≠ 0 guard failed to exclude.
Formal statement
Proof (Lean source)
An indexed continuous real-algebraic section of the projection family. rootIndex is its zero-based position in the ordered set of real roots at every point of the recursively lifted base, so an ordinary selected root of a polynomial with several real roots is permitted; no uniqueness hypothesis is made.
Definition (Lean source)
The selected section is the greatest root in the complete ordered root stack — the boundary of the upper-unbounded sector.
Definition (Lean source)
Recursive cylindrical section/sector geometry in the declared variable order — the output of the section/sector lifting of BPR Def. 5.1 + Thm 5.16. Over a cell of the base decomposition the polynomials of the stage family have finitely many real roots ξ_1 < … < ξ_ℓ in the lifting coordinate, and the cells above it are exactly: the whole fibre when ℓ = 0; otherwise the graph of an indexed root (a section), the sector below the first root, a sector between two consecutive indexed roots, or the sector above the last root.
Definition (Lean source)
Non-vacuity receipt. With the empty family in one variable the cited theorem supplies the single cell ℝ, and the cell language now contains it: this is exactly the point at which the earlier encoding (no ℓ = 0 case, one fully projected family at every stage) was unsatisfiable, which would have made the cited Prop False.
Formal statement
Proof (Lean source)
Singleton-zero non-vacuity receipt. The identically zero polynomial contributes no section roots, so the one-variable CAD for the family {0} consists of the same root-free whole-fibre cell as the empty-family decomposition. This rules out the former counterexample in which {0} made the root stack equal to all of ℝ.
Formal statement
Proof (Lean source)
Project onto the coordinates still live at a given depth of the lifting order: every coordinate outside live is zeroed.
Definition (Lean source)
Cylindrical arrangement (the cylindricity condition of BPR Def. 5.1), relative to the lifting order. At every depth k of the order, the projections of any two cells onto the coordinates still live there (order.drop k) are either identical or disjoint — i.e. the cells are stacked in cylinders over the cells of the induced decomposition of every stage.
Definition (Lean source)
The polynomial P has constant sign on S.
Definition (Lean source)
The solution set of a finite system of polynomial sign conditions.
Definition (Lean source)
A cylindrical algebraic decomposition adapted to the finite family A in the variable order order (BPR Def. 5.1 + Def. 5.5): finitely many nonempty, pairwise disjoint, cylindrically arranged semialgebraic cells covering ℝ^r, obtained by recursive lifting of the generated projection family, on each of which every polynomial of A and of the projection family has constant sign, and which therefore decide every sign condition built from A.
Definition (Lean source)
Non-vacuity of the whole IsAdaptedCAD record. At the trivial instance the cited theorem supplies the single cell ℝ, and every field of the record is satisfied by it simultaneously.
Formal statement
Proof (Lean source)
Non-vacuity of the full adapted-CAD record for {0}. Ignoring an identically zero polynomial in the lifting root stack is compatible with every other field of IsAdaptedCAD: the single cell ℝ is semialgebraic, cylindrical, sign-invariant for the generated family, recursively root-free, and decides every sign condition built from {0}.
Formal statement
Proof (Lean source)
Cylindrical algebraic decomposition adapted to a finite polynomial family — BPR Thm 5.6 (with Def. 5.1, Def. 5.5, Notation 5.15, Thm 5.16); BCR §2.3.
Definition (Lean source)
Tarski–Seidenberg projection theorem — BCR Thm 2.2.1; BPR Ch. 2 (Projection Theorem for Semi-Algebraic Sets).
Definition (Lean source)
The cited external real-closed-field interface in full (cite:bcr-bpr-cad): the cylindrical algebraic decomposition adapted to an arbitrary finite real-polynomial family (BPR Thm 5.6; BCR §2.3), together with the Tarski–Seidenberg projection theorem (BCR Thm 2.2.1). Both conjuncts are general theorems about arbitrary finite real-polynomial families in arbitrary dimension; neither mentions this paper's objects, and neither asserts effectivity.
Definition (Lean source)
Helpers.CAD.EffectiveRationalGroebnerCADInterface 172 declarations
Provides a procedure that decides whether two values of this data type are equal.
Definition (Lean source)
Provides a procedure that decides whether two values of this data type are equal.
Definition (Lean source)
Finite rational syntax for a multivariate polynomial.
Definition (Lean source)
Every finite syntactic code for a multivariate polynomial with rational coefficients has an effective numerical encoding and decoding, so such codes can be listed one by one.
Definition (Lean source)
Interpretation of rational polynomial syntax.
Definition (Lean source)
Canonical code for the zero polynomial.
Definition (Lean source)
Canonical code for the constant polynomial one.
Definition (Lean source)
Canonical code for one coordinate variable.
Definition (Lean source)
The fixed finite machine substrate containing 0, 1, and every coordinate variable. These codes are available to primitive arithmetic, but are not registered as algorithm input families.
Definition (Lean source)
The canonical code for zero denotes the zero polynomial.
Formal statement
Proof (Lean source)
The canonical code for one denotes the constant polynomial one.
Formal statement
Proof (Lean source)
The canonical code for a coordinate variable denotes exactly that coordinate variable.
Formal statement
Proof (Lean source)
A displayed list of rational codes realizes exactly a finite polynomial family.
Definition (Lean source)
The Gaussian rational field ℚ(i), presented by the relation i² = -1.
Definition (Lean source)
No rational number satisfies the defining quadratic relation of the adjoined imaginary unit, that is, no rational number squares to minus one. Registering this fact is what makes the presented quadratic extension of the rationals a field.
Formal statement
The Gaussian rationals have an effective numerical encoding and decoding, obtained from the pair consisting of their rational real and imaginary parts.
Definition (Lean source)
Finite syntax for a polynomial over an arbitrary encodable coefficient field. This is used only by the paper-independent Gröbner interface; the real CAD specialization below remains over ℚ, as required by the cited algorithms.
Definition (Lean source)
Every finite syntactic code for a polynomial over an effectively encodable coefficient field has an effective numerical encoding and decoding, obtained from the encoding of the coefficients.
Definition (Lean source)
Interpretation of finite polynomial syntax over its coefficient field.
Definition (Lean source)
A displayed list of coefficient-field codes realizes exactly a finite polynomial family.
Definition (Lean source)
A finite, machine-readable presentation of a supplied semantic monomial order. The comparison program is part of the input to the uniform Buchberger machine; Realizes below prevents an arbitrary code from being passed off as the requested order.
Definition (Lean source)
Every finite machine presentation of a monomial order has an effective numerical encoding and decoding.
Definition (Lean source)
Exact total comparison semantics for a finite presentation of a monomial order. Terminating comparison is required on every pair of exponents, and the Boolean answer is exactly strict comparison in the supplied admissible Mathlib MonomialOrder.
Definition (Lean source)
A polynomial over K uses only the retained variables of an elimination block.
Definition (Lean source)
An admissible monomial order is an elimination order for keep when every monomial using an eliminated variable is strictly larger than every monomial supported on keep. This is a condition on the supplied order, not a claim that every MonomialOrder is an elimination order.
Definition (Lean source)
The standard finite block-elimination order is effectively presentable for every concrete retained coordinate block. This is an existence statement for the cited construction's canonical block order, not the false assertion that every abstract MonomialOrder is effectively presentable.
Definition (Lean source)
Exact Gröbner-basis semantics for an arbitrary admissible monomial order. Mathlib's MonomialOrder already packages well-foundedness, compatibility with addition, and 0 as the least monomial, so no lexicographic restriction is hidden in this interface.
Definition (Lean source)
Exact elimination-ideal output over an arbitrary coefficient field. Its use with the Gröbner output below is conditional on the supplied monomial order satisfying IsEffectiveEliminationMonomialOrder.
Definition (Lean source)
Exact ideal-intersection output over an arbitrary coefficient field.
Definition (Lean source)
Exact saturation output over an arbitrary coefficient field, characterized by membership after multiplication by a power of the saturating polynomial.
Definition (Lean source)
High-level stages in a coefficient-polymorphic exact algebra trace.
Definition (Lean source)
Provides a procedure that decides whether two high-level stages of a coefficient-polymorphic exact algebra trace are equal.
Definition (Lean source)
Every high-level stage of a coefficient-polymorphic exact algebra trace has an effective numerical encoding and decoding.
Definition (Lean source)
Primitive charged field operations used by the exact algebra trace.
Definition (Lean source)
Provides a procedure that decides whether two primitive charged field operations of the exact algebra trace are equal.
Definition (Lean source)
Every primitive charged field operation used by the exact algebra trace has an effective numerical encoding and decoding.
Definition (Lean source)
One state of a continuous coefficient-polymorphic symbolic execution.
Definition (Lean source)
Extensional availability of a coefficient-field polynomial code in the computed pool.
Definition (Lean source)
Exact transition semantics for one charged field operation.
Definition (Lean source)
Continuous execution of a list of charged coefficient-field operations.
Definition (Lean source)
One supplied-input high-level algebra step and its exact charged primitive program.
Definition (Lean source)
Every high-level algebra step, together with its supplied input families, its displayed output families, and its charged primitive program, has an effective numerical encoding and decoding.
Definition (Lean source)
Exact operation count of a coefficient-polymorphic trace step.
Definition (Lean source)
Extensional availability of a displayed family register.
Definition (Lean source)
A high-level algebra step consumes only registered families and computes every displayed output during this step's charged suffix, before registering those outputs for later steps.
Definition (Lean source)
The complete coefficient-polymorphic trace is one continuous execution; no step is reset with a fresh polynomial pool.
Definition (Lean source)
Canonical zero, one, negative one, and coordinate-variable codes available before every coefficient-polymorphic algebra run. The -1 code makes exact negation and subtraction expressible by the charged multiplication transition.
Definition (Lean source)
Finite machine output for one Gröbner computation over an encodable coefficient field. Its input presentation fields are required below to equal the presentations supplied before the output existential.
Definition (Lean source)
Every finite machine output of one Gröbner computation over an effectively encodable coefficient field — its input presentations, its computed bases, and its trace — has an effective numerical encoding and decoding.
Definition (Lean source)
The exact charged operation count is definitionally the length sum of the continuous coefficient-polymorphic execution.
Definition (Lean source)
A terminating exact Gröbner/elimination/intersection/saturation computation for one supplied finite presentation and one effectively supplied admissible monomial order.
Definition (Lean source)
Buchberger's terminating exact algorithm and its standard elimination, ideal-intersection, and saturation constructions over every effectively supplied admissible monomial order. One machine code is fixed before the dimension, order presentation, or any polynomial presentation; the input code lists are supplied and realized before the output existential.
Definition (Lean source)
One fully supplied coefficient-field algebra job. All semantic input, presentation, and monomial-order obligations are fixed before its output is chosen.
Definition (Lean source)
Input size charged to one coefficient-field algebra job.
Definition (Lean source)
A uniform degree bound for one coefficient-field algebra job.
Definition (Lean source)
A common degree envelope for a concrete finite polynomial family. Unlike EffectiveGroebnerJobOver.DegreeBoundedBy, this predicate can be applied to families produced by a completed exact computation, after those outputs have been chosen.
Definition (Lean source)
The exact output of one supplied algebra job, tied to a machine code fixed before every job in its batch.
Definition (Lean source)
Rename a finite rational polynomial family between two supplied finite coordinate presentations. The map is data: the dependent pipeline below does not silently identify the retained variables of two different jobs.
Definition (Lean source)
A source-matched dependent rational-algebra execution. The two supplied incidence jobs run first. Only after their exact elimination outputs exist is the intersection job supplied, and its two semantic inputs are exactly the renamed elimination outputs. The caller fixes which cross-source coordinates are shared before this pipeline is returned; the two coordinate maps realize exactly that relation while remaining injective within each source. Thus the third job cannot be an unrelated member of a preselected batch.
Definition (Lean source)
Exact charged operation count of the dependent two-eliminations-then- intersection execution.
Definition (Lean source)
A post-elimination degree envelope for one concrete dependent execution. It bounds the two supplied source jobs, their actual saturated elimination outputs, the dependent intersection job built from those outputs, and its actual intersection basis. In particular, this predicate is evaluated only after pipeline has been returned; it does not assert that elimination preserves a source-only degree bound.
Definition (Lean source)
Results for a finite batch of supplied algebra jobs over one coefficient field.
Definition (Lean source)
Sum of the exact charged symbolic traces in a coefficient-field batch.
Definition (Lean source)
Aggregate supplied input size of a finite algebra batch.
Definition (Lean source)
Every job in a finite batch lies in the common ambient-dimension and degree envelope used by the single combined complexity bound.
Definition (Lean source)
Coefficient extension of a rational family to the real closed field.
Definition (Lean source)
Coefficient extension of a rational family to the algebraically closed field used by the elimination-closure theorem.
Definition (Lean source)
Common complex zero set of a finite rational polynomial family.
Definition (Lean source)
Zariski closure in a finite complex affine space, written directly as the zero set of every complex polynomial vanishing on the supplied set.
Definition (Lean source)
Cylinder over the coordinate projection of a complex affine set onto a retained variable block.
The algebraically closed elimination-closure theorem for a displayed rational elimination basis. This is the exact geometric conclusion used after Groebner elimination: the output zero set is the Zariski closure of the input projection, not the projection itself.
Definition (Lean source)
A polynomial uses only the retained variables of an elimination block.
Definition (Lean source)
Lexicographic comparison of monomials in the explicitly supplied variable order.
The specified variable order is complete, duplicate-free, and is an elimination order for the retained block: every eliminated variable precedes every retained variable.
Definition (Lean source)
exponent is the leading exponent of P for the displayed lexicographic order.
Definition (Lean source)
An exact Gröbner-basis certificate for the specified monomial order. Besides ideal equality and exact normal-form division, every leading monomial in the input ideal is divisible by a leading monomial of the displayed basis, and the normal form contains no reducible monomial.
Definition (Lean source)
Exact elimination-ideal output on the retained variable block.
Definition (Lean source)
Exact ideal-intersection output.
Definition (Lean source)
Exact saturation output, characterized by membership after multiplication by a power.
Definition (Lean source)
The three-valued exact sign alphabet emitted by the effective CAD algorithm.
Definition (Lean source)
Provides a procedure that decides whether two exact signs from the three-valued alphabet (negative, zero, positive) are equal.
Definition (Lean source)
Every exact sign from the three-valued alphabet emitted by the effective CAD algorithm has an effective numerical encoding and decoding.
Definition (Lean source)
Exact interpretation of an encoded sign.
Definition (Lean source)
Iterated differentiation in one CAD lifting variable.
Definition (Lean source)
Finite exact algebraic-root data: a defining rational polynomial, its index in the complete ordered root stack, and its complete Thom-sign row.
Definition (Lean source)
Every finite exact algebraic-root certificate — its defining rational polynomial, its index in the ordered root stack, and its Thom-sign row — has an effective numerical encoding and decoding.
Definition (Lean source)
A root certificate denotes the indexed CAD root and gives the exact signs of every iterated derivative of its displayed defining polynomial along the section.
Definition (Lean source)
Finite syntax for recursive CAD lifting, enriched at every section/sector boundary by exact algebraic-root and Thom-sign certificates.
Definition (Lean source)
Every recursive finite syntax tree describing a lifted CAD cell geometry has an effective numerical encoding and decoding.
Definition (Lean source)
Exact interpretation of an algebraic-root-certified CAD cell.
Definition (Lean source)
Number of exact algebraic-sign answers explicitly stored in a recursive cell certificate.
Definition (Lean source)
A cell's encoded geometry together with an exhaustive exact sign row for the input and generated projection polynomials.
Definition (Lean source)
Every complete CAD cell certificate, consisting of its encoded geometry together with its exhaustive constant-sign row, has an effective numerical encoding and decoding.
Definition (Lean source)
The encoded cell certificate realizes both its recursive algebraic-root geometry and its complete constant-sign table.
Definition (Lean source)
Number of exact root/Thom/cell-sign answers carried by one complete cell certificate.
Definition (Lean source)
Every polynomial presentation contained in one exact algebraic-root certificate.
Definition (Lean source)
Recursive extraction of every defining polynomial used by a CAD cell certificate.
Definition (Lean source)
A recursive cell geometry requires an algebraic-root isolation stage exactly when it has a nontrivial lifting layer. A wholeFiber still requires certifying that the root stack is empty.
Definition (Lean source)
A recursive cell geometry contains a section-lifting layer.
Definition (Lean source)
A recursive cell geometry contains a sector-lifting layer.
Definition (Lean source)
Every polynomial presentation on which a certified CAD cell depends: recursive root-defining polynomials together with the complete displayed constant-sign family.
Definition (Lean source)
A finite encoded sign-condition query.
Definition (Lean source)
Every finite encoded sign-condition query — its equations together with its nonnegativity and positivity requirements — has an effective numerical encoding and decoding.
Definition (Lean source)
Every polynomial presentation read by a sign-condition query.
Definition (Lean source)
Exact decoding of a sign-condition query.
Definition (Lean source)
One exhaustive encoded cellwise truth row.
Definition (Lean source)
Every encoded cellwise truth row has an effective numerical encoding and decoding.
Definition (Lean source)
Every polynomial presentation read to produce a truth row.
Definition (Lean source)
One exhaustive encoded witness-retention row.
Definition (Lean source)
Every encoded witness-retention row has an effective numerical encoding and decoding.
Definition (Lean source)
Every polynomial presentation read to produce a witness-retention row.
Definition (Lean source)
Erase a supplied prefix of lifting coordinates. This is the geometric projection naturally paired with IsRecursivelyLiftedCADCell: the recursive cell language peels the head of the lifting order and applies cadEraseCoordinate at every dropped layer.
Definition (Lean source)
The recursion-varying BPR family after dropping a prefix of lifting layers. Unlike the public accumulated generatedCADProjectionFamily, this is the stage family consumed by the recursive cell certificate over the retained suffix.
Definition (Lean source)
Finite exact sign-vector syntax for one basic CAD cell presentation. Negative signs are kept explicitly, rather than encoding them by silently adjoining negated polynomials to the supplied family.
Definition (Lean source)
Every finite exact sign-vector presentation of a basic CAD cell has an effective numerical encoding and decoding.
Definition (Lean source)
The subset of the erased-prefix affine slice cut out by an encoded exact sign vector. The explicit zero-coordinate guard is part of the ambient representation: projected cells still use CADSpace r, so their eliminated coordinates must not be left as free cylindrical directions.
Definition (Lean source)
An encoded sign vector lists every polynomial in the displayed rational family, uses no polynomial outside that family, and cuts out exactly the displayed cell. The coverage direction is required by prefix-projected CAD consumers: soundness for the signs that happen to be listed does not by itself make the list an exact sign vector for the displayed family.
Definition (Lean source)
Every polynomial presentation read by a basic sign-condition certificate.
Definition (Lean source)
One fully encoded prefix-projected CAD cell certificate. The source-cell code and the exact truth/retention-row code lists link the projected cell back to all of the finite decision data emitted for its source cell.
Definition (Lean source)
Every fully encoded prefix-projected CAD cell certificate — its eliminated and retained variables, its source-cell links, its projected geometry, its basic sign presentation, and its truth- and retention-row links — has an effective numerical encoding and decoding.
Definition (Lean source)
Every polynomial presentation required by a prefix-projected cell artifact.
Definition (Lean source)
Exact root/Thom and basic-cell sign answers stored in one prefix projection artifact.
Definition (Lean source)
Exact finite data for one charged member of a BPR reducta family. The source code and iteration number are retained so the primitive trace records how the output code was obtained, rather than merely asserting that an extensionally equal polynomial eventually appeared.
Definition (Lean source)
Every finite certificate for one charged member of a reducta family — its source polynomial, the reduction variable and iteration number, and the output polynomial — has an effective numerical encoding and decoding.
Definition (Lean source)
A reductum certificate denotes exactly the displayed nonzero iterate, within the finite degree range used by cadReducta. Coefficient extension to ℝ is injective, so this equality also fixes the underlying rational output polynomial.
Definition (Lean source)
General symbolic operations supplied by the cited rational algebra and CAD algorithms.
Definition (Lean source)
General effective-algebra trace operations have a decidable equality test: any two operations can be effectively determined to be the same or different.
Definition (Lean source)
Every general effective-algebra trace operation has an effective numerical encoding and decoding.
Definition (Lean source)
Primitive operations in the real-algebraic cost model. Exact algebraic-sign queries are primitive here; this does not claim Turing-computable comparison of arbitrary real numbers.
Definition (Lean source)
Provides a procedure that decides whether two primitive operations of the real-algebraic cost model are equal.
Definition (Lean source)
Every primitive operation of the real-algebraic cost model has an effective numerical encoding and decoding.
Definition (Lean source)
One certified high-level trace step, including the polynomial families it reads and emits, the injective encodings of any CAD certificates/truth rows/retention rows it produces, and the complete list of primitive real-algebraic operations charged to that step. The artifact fields use Nat solely to avoid a circular datatype dependency; result-level equalities below identify them extensionally with the actual typed payload objects.
Definition (Lean source)
Every certified effective-algebra trace step, including its input, output, certificate, and primitive-operation data, has an effective numerical encoding and decoding.
Definition (Lean source)
Exact real-algebraic cost of one trace step.
Definition (Lean source)
Every typed output artifact attributed to a trace step consumes a charged exact-sign event. The stronger result-level bound below additionally charges every Thom/cell sign stored inside the produced cell certificates.
Definition (Lean source)
Artifact outputs occur only at the corresponding CAD/QE stages.
Definition (Lean source)
A trace step is tied to a particular high-level operation and its displayed input/output polynomial families.
Definition (Lean source)
The rational polynomial family decoded from one finite code list.
Definition (Lean source)
The real interpretation of one displayed rational code family.
Definition (Lean source)
The reductum-certificate code, when a primitive is a reductum-emission event.
Definition (Lean source)
The displayed reductum-certificate register is exactly the corresponding subsequence of the charged primitive program. Thus a reducta stage cannot list certificates beside an unrelated arithmetic trace.
Definition (Lean source)
A reducta-generation step charges one exact certificate for every displayed output code. Each certificate starts from a code in the declared input family, uses the declared active variable, and realizes the indicated finite reductum iterate.
Definition (Lean source)
One state of the primitive rational-arithmetic execution underlying a high-level trace step.
A required polynomial presentation is extensionally available in the computed register pool. The exact code need not be byte-identical, but it must denote the same rational polynomial.
Definition (Lean source)
Exact transition semantics for every charged primitive operation. Polynomial arithmetic adds the computed rational polynomial to the register pool; artifact-emission steps append the exact encoded object to the corresponding output register. Hence typed CAD/QE output is generated by, not merely listed beside, the bounded primitive execution.
Definition (Lean source)
Execution of the displayed primitive-operation list, with no hidden uncharged transitions.
Definition (Lean source)
A displayed polynomial family is already present, extensionally, in a family register created by the supplied input or by an earlier trace step.
Definition (Lean source)
Operation-specific mathematical semantics for the input and output families of a high-level trace step. This connects the encoded trace to the exact Gröbner, elimination, projection, and CAD operations whose primitive execution is charged.
Definition (Lean source)
One high-level trace step runs from the previous global state. No step can introduce a fresh input family: every input must already be registered extensionally. Its named semantic operation is correct, its primitive program starts from that same state, and every displayed output is available in the resulting pool. The pool may additionally retain charged intermediate results.
Definition (Lean source)
The whole symbolic trace is one continuous bounded execution. Each step consumes exactly the state produced by its predecessor; in particular no per-step polynomial pool is reset or supplied afresh.
Definition (Lean source)
A trace step at the displayed position has the exact operation, code-family boundary, and active CAD variable required by one projection round.
Definition (Lean source)
Exact ordered BPR projection rounds. Each round first registers all reducta of the current accumulated family, then computes coefficients, discriminants, and principal subresultants from that same registered reducta family, and finally registers the current family together with their union. The next round consumes that registered output directly, exactly matching the foldl defining generatedCADProjectionFamily; no fresh uncharged family is introduced between rounds.
Definition (Lean source)
Discrete output of one terminating general-purpose rational Gröbner/CAD run.
Definition (Lean source)
Every finite payload produced by the effective rational Gröbner/CAD computation has an effective numerical encoding and decoding.
Definition (Lean source)
The symbolic operation count is definitionally the sum of the primitive arithmetic/sign events recorded by the certified trace; it is not an independently chosen payload field.
Definition (Lean source)
Number of exact root/Thom/cell-sign answers explicitly certified by the payload.
Definition (Lean source)
Number of exact root/Thom/basic-cell signs stored in all prefix projection artifacts.
Definition (Lean source)
Two assignments agree on the coordinates retained after witness elimination.
Definition (Lean source)
Real sign-condition set associated with rational polynomial input.
Definition (Lean source)
A complete semantically certified output of the general effective algorithms. The machine halts with the exact encoding of the displayed finite payload. Its fuel is deliberately unrelated to payload.symbolicOperationCount, which counts the primitive rational-arithmetic and exact algebraic-sign events recorded in the symbolic trace.
Definition (Lean source)
One fully supplied rational real-CAD/QE job.
Definition (Lean source)
A rational CAD/QE job built from the exact ideal-intersection basis emitted by a completed dependent elimination pipeline. The CAD ambient may be larger than the observable-intersection ambient because later real source presentations can add witness and loading coordinates. intersectionToCAD is therefore an exact embedding, and input_from_intersection says that the first CAD input is precisely the computed basis after that injective rename, not an independently selected Groebner basis. The CAD job's secondInput remains available for the simultaneous real incidence and sign-query polynomials.
Definition (Lean source)
Input size charged to the rational CAD/QE job.
Definition (Lean source)
A uniform degree bound for the rational CAD/QE job.
Definition (Lean source)
Exact rational CAD/QE output tied to the uniform machine code.
Definition (Lean source)
The general Cox--Little--O'Shea Closure Theorem after scalar extension to the algebraically closed field ℂ. It is stated for arbitrary rational input and retained coordinate blocks and contains no paper-specific object.
Definition (Lean source)
Universal source-matched combined complexity certificate. The constants and all three uniform machine codes are fixed before every rational or Gaussian- rational algebra batch and before the rational CAD/QE input. In the dependent clause, the caller fixes the cross-source shared-coordinate relation before the two elimination results and their exact intersection result are returned; only then is a CAD/QE job consuming that pipeline's intersection basis quantified. The one displayed inequality charges the same returned pipeline and CAD/QE result together; partial-recursive fuel is deliberately absent from this cost statement.
Definition (Lean source)
Backward-compatible public name used by atlas complexity certificates. It now denotes the single combined algebra-plus-CAD batch bound, not a separate rational-CAD-only inequality.
Definition (Lean source)
The complete general effective interface: uniform exact Gröbner algorithms on supplied presentations over ℚ and ℚ(i) and a rational specialization carrying both the algebraically closed elimination-closure theorem and real CAD, whose actual finite certificate/truth/retention outputs are produced by its bounded trace.
Definition (Lean source)
Effective rational Gröbner/CAD interface — cited external tool. For every finite polynomial presentation over ℚ or ℚ(i) and every effectively supplied admissible MonomialOrder, the interface supplies a terminating exact Buchberger/Gröbner computation, exact elimination output whenever the supplied order has the encoded elimination property, and exact ideal-intersection and saturation output, including a charged saturation–Gröbner–elimination chain. It also supplies a computably realized standard finite block-elimination order for every concrete retained block. For rational input it supplies the standard Closure Theorem after coefficient extension to ℂ: the elimination-basis zero set is exactly the Zariski closure of the input zero set's retained-coordinate projection. Its rational real-polynomial specialization additionally supplies an effective sign-invariant recursively section/sector CAD for the union of both supplied real sign families, with exact algebraic-root indices, cellwise sign truth, quantifier elimination by witness-cell retention, and, for every lifting-order prefix and source cell, an exact erased-prefix cell with dropped-layer recursive geometry, a finite basic sign presentation, and exact truth/retention-row links. All of these data are emitted by a finite certified symbolic trace. Polynomial and order presentations are supplied before output selection; the algorithm codes are fixed uniformly before those inputs, the supplied order code is required to realize the semantic monomial order, and injective encodings tie the bounded trace extensionally to every emitted cell certificate, root/sign row, truth row, and retained-witness row. An artifact-emission transition is permitted only after every polynomial presentation recursively contained in that artifact has already been computed extensionally in the trace's polynomial register.
Definition (Lean source)
Helpers.CommonAxisImageGeometry 12 declarations General finite-affine image lemmas
General finite-affine image lemmas
Proves the stated mathematical property of Common Axis Band Coord.
Definition (Lean source)
Defines the mathematical object called the common Axis Band Insert.
Definition (Lean source)
Defines the mathematical object called the common Axis Param.
Definition (Lean source)
Defines the polynomial called the common Axis Polynomial.
Definition (Lean source)
Proves that the map called the eval common Axis Polynomial is polynomial.
Formal statement
Proof (Lean source)
Defines the mathematical object called the forward Common Axis Finite Map.
Definition (Lean source)
Proves that the map called the forward Common Axis Finite Map is Polynomial is polynomial.
Formal statement
Proof (Lean source)
Defines the mathematical object called the common Axis Source.
Definition (Lean source)
Proves the stated mathematical property of common Axis Source dense.
Formal statement
Proof (Lean source)
Proves the stated equality or equivalence for common Axis Finite Image eq.
Formal statement
Proof (Lean source)
Restriction to the retained band commutes with Zariski closure for a band-supported set.
Formal statement
Proof (Lean source)
The finite retained-coordinate closure of the explicit common-axis image is irreducible.
Formal statement
Proof (Lean source)
Helpers.CommonAxisPrincipalEquations 4 declarations
The horizontal contraction minor is an actual equation of the finite common-axis image closure.
Formal statement
Proof (Lean source)
The same equation is nontrivial modulo the forward arrow-image ideal.
Formal statement
Proof (Lean source)
Since the common-axis family lies in the exceptional locus and hence in the forward variety, the coordinate-reversed vertical minor is its second explicit principal equation.
Formal statement
Proof (Lean source)
The vertical equation is nontrivial modulo the reverse arrow-image ideal, witnessed by the coordinate reversal of the forward block-Vandermonde point.
Formal statement
Proof (Lean source)
Helpers.CommonAxisReversal 11 declarations
Observable coordinate reversal on the finite retained affine space.
Definition (Lean source)
Relabelling the retained cumulant coordinates by the observable coordinate exchange twice returns the original point of the retained affine space, so this relabelling is an involution there.
Formal statement
Proof (Lean source)
The observable coordinate exchange on the retained band is a polynomial map: each output coordinate is literally one of the input coordinates, hence a degree-one polynomial in them. This is what lets the exchange be pushed through Zariski closures.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of restrict Cum Band reverse Cum Coordinates.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of reverse Retained Coordinates image image.
Formal statement
Proof (Lean source)
A polynomial involution commutes with affine Zariski closure.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of reverse Cum Coordinates forward range.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of reverse Cum Coordinates common Axis raw.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of reverse Retained Coordinates forward Variety.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of reverse Retained Coordinates common Axis Closure.
Formal statement
Proof (Lean source)
Coordinate reversal transfers the reverse no-intermediate statement from the forward one.
Formal statement
Proof (Lean source)
Helpers.CommonAxisTwin 9 declarations
The generic forward parameter divisor on which the first latent direction is the horizontal axis.
Definition (Lean source)
Reverse parameters obtained by reciprocating every nonzero finite forward slope and cycling the two fixed axes with the zero latent direction.
Definition (Lean source)
If every source weight of a forward parameter point vanishes outside the retained orders two through 2m+2, the same holds for its common-axis reverse twin. The twin only relabels the sources and rescales each weight by a power of a slope, so it can create no weight outside the band.
Formal statement
Proof (Lean source)
The reciprocal common-axis twin stays in the generic retained-band locus. This is the parameter-level symmetry needed to transport the common-axis closure through observable coordinate reversal.
Formal statement
Proof (Lean source)
Proves the stated equality or equivalence for common Axis Reverse Twin map eq.
Formal statement
Proof (Lean source)
Proves the stated set-containment or membership property for forward Common Axis image mem exceptional.
Formal statement
Proof (Lean source)
Closure of the common-axis image divisor inside the forward arrow variety.
Definition (Lean source)
The closure of the observable image of the common-axis divisor lies inside the closure of the generic full-fiber compatibility locus. Every truncated cumulant vector generated by a generic forward parameter whose first latent direction is the horizontal axis is therefore also generated by some reverse-arrow parameter, so the arrow direction is not pinned down there.
Formal statement
Proof (Lean source)
The explicit common-axis image closure lies on the observable horizontal contraction-minor hypersurface.
Formal statement
Proof (Lean source)
Helpers.CoordinateReversalGeometry 19 declarations
Exchange the two observable coordinates in every cumulant block.
Definition (Lean source)
At a coordinate whose number of Y-copies does not exceed the cumulant order, the coordinate-reversed cumulant vector reproduces the original vector at the same order with the roles of the two observables interchanged: the entry of order r carrying a copies of Y is the original entry of order r carrying r − a copies.
Formal statement
Proof (Lean source)
Exchanging the two observable coordinates twice restores the original cumulant vector, so coordinate reversal is an involution of the cumulant space.
Formal statement
Proof (Lean source)
Reverse the source order at the two fixed axes.
Definition (Lean source)
The same slope coordinates and weights, with the two fixed-axis sources exchanged. Observable coordinate reversal turns this forward parameter into a reverse parameter.
Definition (Lean source)
Exchanging the two fixed-axis source labels twice returns the original source label, so the axis reversal is an involution of the source index set.
Formal statement
Proof (Lean source)
Applying the axis reversal twice returns the original parameter point: the direct and latent slopes are never touched, and the source-weight families attached to the two fixed axes are exchanged back into place.
Formal statement
Proof (Lean source)
Honest coordinate reversal identifies the two polynomial arrow maps.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of axis Reverse Parameter band Supported.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of axis Reverse Parameter generic.
Formal statement
Proof (Lean source)
Proves the stated set-containment or membership property for reverse Cum Coordinates mem band.
Formal statement
Proof (Lean source)
Coordinate reversal on finite retained cumulant coordinates.
Definition (Lean source)
Reversing a retained cumulant coordinate twice gives back the original coordinate: at a fixed order r the position carrying a copies of Y is sent to the one carrying r − a copies, and back again.
Formal statement
Proof (Lean source)
The coordinate-reversed observable contraction minor.
Definition (Lean source)
Evaluating the vertical contraction minor on the retained band of a cumulant vector gives the same number as evaluating the horizontal contraction minor on the retained band of the coordinate-reversed vector: the vertical minor is exactly the horizontal one read in the exchanged observable coordinates.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of vertical Contraction Minor Polynomial forward vanishes.
Formal statement
Proof (Lean source)
The vertical minor vanishes on the entire forward arrow-image variety.
Formal statement
Proof (Lean source)
The mirrored block-Vandermonde witness makes the vertical minor nonzero on the reverse arrow image.
Formal statement
Proof (Lean source)
With at least one latent confounder the vertical contraction-minor polynomial is not the zero polynomial: the mirrored block-Vandermonde reverse parameter produces an observable vector at which it does not vanish.
Formal statement
Proof (Lean source)
Helpers.DirectLatentSwaps 14 declarations
The source index i+1 belonging to the i-th latent loading.
Definition (Lean source)
θ' interchanges the complete forward direct-source pair with latent pair i.
Definition (Lean source)
η' interchanges the complete reverse direct-source pair with latent pair i.
Definition (Lean source)
The unordered finite-slope part of either arrow support.
Definition (Lean source)
The concrete forward direct/latent swap.
Definition (Lean source)
The concrete reverse direct/latent swap.
Definition (Lean source)
The explicitly constructed forward swap really does interchange the direct source with the i-th latent source: the new direct slope is the old i-th latent slope, the new i-th latent slope is the old direct slope, and the source-weight families of the two sources are exchanged.
Formal statement
Proof (Lean source)
The explicitly constructed reverse swap really does interchange the reverse arrow's direct source with the i-th latent source: the new direct slope is the old i-th latent slope, the new i-th latent slope is the old direct slope, and the source-weight families of the two sources are exchanged.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of forward Direct Latent Swap generic.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of reverse Direct Latent Swap generic.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of forward Cumulant Map direct Latent Swap.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of reverse Cumulant Map direct Latent Swap.
Formal statement
Proof (Lean source)
Proves the stated set-containment or membership property for forward Direct Latent Swap not mem admissible Orbit.
Formal statement
Proof (Lean source)
Proves the stated set-containment or membership property for reverse Direct Latent Swap not mem admissible Orbit.
Formal statement
Proof (Lean source)
Helpers.EmptyFiber 2 declarations
A point satisfying the forward apolar rank conditions has no reverse-arrow parameterization with the same truncated cumulants.
Formal statement
Proof (Lean source)
A point satisfying the reverse apolar rank conditions has no forward-arrow parameterization with the same truncated cumulants.
Formal statement
Proof (Lean source)
Helpers.ExceptionalCodimension 4 declarations
C is an irreducible component of the Zariski-closed set Z.
Definition (Lean source)
Exact minimum codimension of a closed set in an ambient irreducible variety, measured by strict irreducible chains from its components.
Definition (Lean source)
Exact codimension one excludes every claimed exact codimension d ≥ 2.
Formal statement
Proof (Lean source)
A proper closed subset of an irreducible ambient has codimension at least one; one component with no intermediate irreducible closed set makes the minimum codimension exactly one.
Formal statement
Proof (Lean source)
Helpers.ExceptionalCommonAxisJacobianTop 29 declarations Differentiating after pinning the common-axis variable
Differentiating after pinning the common-axis variable
Pinning one variable to zero commutes with partial differentiation in every retained variable.
Formal statement
Proof (Lean source)
Evaluation form of pderiv_commonAxisPolynomial.
Formal statement
Proof (Lean source)
The canonical common-axis coordinate is the pinned canonical full coordinate.
Formal statement
Proof (Lean source)
Partial derivatives of the canonical common-axis coordinate can be computed in the full coordinate family and then pinned.
Formal statement
Proof (Lean source)
Evaluation transfer from a common-axis Jacobian entry to the full Jacobian at the inserted parameter point.
Formal statement
Proof (Lean source)
Common-axis witness: the deleted latent slope is zero after insertion; the direct slope is one, all other latent slopes are i+1, and every retained weight is one.
Definition (Lean source)
The finite source permutation puts the pinned latent source first and the direct source second.
Definition (Lean source)
The permuted finite nodes are 0,1,...,m.
Definition (Lean source)
The permuted finite nodes carry pairwise distinct values, since node j is assigned the number j itself and the nodes are 0, 1, ..., m.
Formal statement
Proof (Lean source)
Reinstating the pinned latent-slope coordinate at the common-axis witness leaves the direct slope equal to one.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of common Axis Jacobian Witness insert latent.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of common Axis Jacobian Witness insert weight.
Formal statement
Proof (Lean source)
Loading evaluation at the inserted common-axis witness.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of common Axis Jacobian Witness weight.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of common Axis Jacobian Witness loading last.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of Common Axis Top Index.
Definition (Lean source)
Defines the mathematical object called the common Axis Top Row.
Definition (Lean source)
The slope associated with the derivative node i+1: the first is the direct slope; all later ones are their same-index latent slopes.
Definition (Lean source)
The slope differentiated at the i-th unpinned node — the direct slope when i is zero and the latent slope of the same index otherwise — is carried by exactly the source that the common-axis permutation places at node i + 1.
Formal statement
Proof (Lean source)
Defines the mathematical object called the common Axis Top Column.
Definition (Lean source)
Defines the Jacobian matrix, row, column, or indexing object called the canonical Common Axis Top Jacobian At Witness.
Definition (Lean source)
Proves the stated equality or equivalence for canonical Common Axis Top Jacobian At Witness equality pinned.
Formal statement
Proof (Lean source)
Proves that the quantity called the det canonical Common Axis Top Jacobian At Witness is nonzero.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of Common Axis Top Augmented Index.
Definition (Lean source)
Defines the mathematical object called the common Axis Top Augmented Row.
Definition (Lean source)
Defines the mathematical object called the common Axis Top Augmented Column.
Definition (Lean source)
Defines the Jacobian matrix, row, column, or indexing object called the canonical Common Axis Top Augmented Jacobian At Witness.
Definition (Lean source)
Proves the stated equality or equivalence for canonical Common Axis Top Augmented Jacobian At Witness eq.
Formal statement
Proof (Lean source)
Proves that the quantity called the det canonical Common Axis Top Augmented Jacobian At Witness is nonzero.
Formal statement
Proof (Lean source)
Helpers.ExceptionalCommonAxisOrdinary 6 declarations
Defines the Jacobian matrix, row, column, or indexing object called the canonical Common Axis Low Weight Jacobian At Witness.
Definition (Lean source)
Proves the stated equality or equivalence for canonical Common Axis Low Weight Jacobian At Witness eq.
Formal statement
Proof (Lean source)
Proves that the quantity called the det canonical Common Axis Low Weight Jacobian At Witness is nonzero.
Formal statement
Proof (Lean source)
Defines the Jacobian matrix, row, column, or indexing object called the canonical Common Axis High Weight Jacobian At Witness.
Definition (Lean source)
Proves the stated equality or equivalence for canonical Common Axis High Weight Jacobian At Witness eq.
Formal statement
Proof (Lean source)
Proves that the quantity called the det canonical Common Axis High Weight Jacobian At Witness is nonzero.
Formal statement
Proof (Lean source)
Helpers.ExceptionalGeometryBasic 8 declarations
Proves the stated set-containment or membership property for subset zariski Closure.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of zariski Closure mono.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of zariski Closure idem.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of zariski Closure is Closed.
Formal statement
Proof (Lean source)
Proves the stated set-containment or membership property for generic Full Fiber Compatibility subset forward range.
Formal statement
Proof (Lean source)
Proves the stated set-containment or membership property for generic Full Fiber Compatibility subset reverse range.
Formal statement
Proof (Lean source)
Proves the stated set-containment or membership property for generic Compatibility Closure subset forward Variety.
Formal statement
Proof (Lean source)
Proves the stated set-containment or membership property for generic Compatibility Closure subset reverse Variety.
Formal statement
Proof (Lean source)
Helpers.ExceptionalHeightReduction 20 declarations
Proves the stated set-containment or membership property for generic Compatibility Closure subset band.
Formal statement
Proof (Lean source)
Proves the stated set-containment or membership property for forward Cumulant Image Variety subset band.
Formal statement
Proof (Lean source)
Proves the stated set-containment or membership property for reverse Cumulant Image Variety subset band.
Formal statement
Proof (Lean source)
The exceptional closure is proper in the forward arrow variety. The separating equation is the explicit observable horizontal contraction minor: it vanishes on the reverse variety, while the block-Vandermonde forward witness has nonzero value.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of restrict generic Compatibility Closure ne forward Variety.
Formal statement
Proof (Lean source)
The coordinate-reversed observable minor gives the symmetric properness statement in the reverse ambient arrow variety.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of restrict generic Compatibility Closure ne reverse Variety.
Formal statement
Proof (Lean source)
The exact finite certificate still required for one arrow: properness of the exceptional closure and one of its affine irreducible components being a minimal prime over a single observable equation in the arrow coordinate ring.
Definition (Lean source)
The model-specific specialization demanded by the D0 proof: the component is the closure of the explicit common-axis opposite-arrow twin family.
Definition (Lean source)
For the forward ambient, observable-minor properness is compiled; only the common-axis component and its principal minimal-prime certificate remain.
Formal statement
Proof (Lean source)
Reverse-ambient assembly using the coordinate-reversed principal equation.
Formal statement
Proof (Lean source)
The exact residual after both observable properness arguments: one common irreducible-component proof and the two explicit principal minimal-prime certificates.
Formal statement
Proof (Lean source)
The principal certificates follow formally from the honest geometric height-one statement for the common-axis closure. This isolates the remaining model-specific work to irreducibility and the absence of an intermediate irreducible closed set in each arrow variety.
Formal statement
Proof (Lean source)
After proving polynomial-image irreducibility of the common-axis closure, the complete residual consists only of the two height-one (no-intermediate) statements.
Formal statement
Proof (Lean source)
Coordinate reversal supplies the reverse height-one statement, so the single remaining model-specific premise is the forward D - 1 versus D dimension gap.
Formal statement
Proof (Lean source)
The expected dimension of the common-axis image, namely D - 1 in the notation of the D0 Jacobian calculation. The forward arrow variety has the successor dimension.
Definition (Lean source)
Exact D - 1 and D image dimensions discharge the sole remaining height-one premise.
Formal statement
Proof (Lean source)
Once the explicit principal minimal-prime certificates are supplied, the frozen custom codimension-one claims follow exactly.
Formal statement
Proof (Lean source)
All non-geometric conjuncts of the flagship assemble from the compiled incidence helpers. Consequently the two explicit finite height certificates are the complete residual for exceptionalLocusCodimensionOne.
Formal statement
Proof (Lean source)
The explicit common-axis certificates alone imply the entire flagship conclusion.
Definition (Lean source)
Helpers.ExceptionalImageDimension 13 declarations
The forward cumulant map on the finite retained-band parameter space.
Definition (Lean source)
Every retained cumulant coordinate of the forward map is a polynomial in the finitely many retained parameter coordinates, so the forward map on the finite band is a polynomial map. The truncation order is assumed to be at least two.
Formal statement
Proof (Lean source)
A canonical coordinate-polynomial family for the finite forward map.
Definition (Lean source)
The chosen coordinate polynomial of a retained cumulant coordinate does what it is supposed to do: evaluated at any finite parameter coordinate vector it returns that coordinate of the forward band map.
Formal statement
Proof (Lean source)
Assembling the chosen coordinate polynomials into a single vector-valued map recovers exactly the forward map on the finite retained band.
Formal statement
Proof (Lean source)
Pinning the unused parameter coordinates does not change a truncated forward cumulant vector.
Formal statement
Proof (Lean source)
The set of retained cumulant vectors produced by the finite forward map is exactly the retained-band restriction of the set produced by the full forward cumulant map. Nothing is lost by pinning the off-band weights to zero, because cumulants of orders two through L never depend on them; the truncation order is assumed to be at least two.
Formal statement
Proof (Lean source)
The finite restriction of the forward arrow variety is exactly the polynomial-image closure to which the promoted dimension bridge applies.
Formal statement
Proof (Lean source)
A canonical coordinate-polynomial family for the common-axis map.
Definition (Lean source)
Assembling the chosen common-axis coordinate polynomials into a single vector-valued map recovers exactly the forward map on the common-axis band, where the first latent slope is pinned to zero. At least one latent source and a truncation order of at least two are assumed.
Formal statement
Proof (Lean source)
The finite common-axis closure is the corresponding polynomial-image closure; density removes the generic nonvanishing condition on the source.
Formal statement
Proof (Lean source)
The promoted Jacobian/transcendence bridge specialized to the full forward arrow image. The two hypotheses are precisely the model-specific lower and upper certificates still owed by the confluent-Vandermonde calculation and the low-order weight kernels.
Formal statement
Proof (Lean source)
The same promoted bridge specialized to the common-axis divisor image.
Formal statement
Proof (Lean source)
Helpers.ExceptionalImageDimensionUpper 9 declarations
The retained generators for the full forward image: all loading slopes, all cumulant coordinates through order m, and all source weights from order m+1 through order 2m+2.
Definition (Lean source)
Every forward coordinate polynomial factors through the retained generator family. This is the model-specific content of the upper dimension bound.
Formal statement
Proof (Lean source)
The full forward coordinate algebra is generated by the slopes, low-order outputs, and high-order weights retained above.
Formal statement
Proof (Lean source)
The common-axis generator family is obtained by deleting the pinned rho_0 slope from the full generator family.
Definition (Lean source)
Every common-axis coordinate polynomial factors through the generator family obtained by deleting the fixed slope.
Formal statement
Proof (Lean source)
The generator envelope has exactly the full expected image dimension.
Formal statement
Proof (Lean source)
Deleting the pinned common-axis slope removes exactly one generator.
Formal statement
Proof (Lean source)
Exact full-image transcendence upper bound supplied by the generator envelope, with no fiber-dimension interface.
Formal statement
Proof (Lean source)
Exact common-axis transcendence upper bound supplied by the generator envelope with the pinned slope deleted.
Formal statement
Proof (Lean source)
Helpers.ExceptionalIncidence 10 declarations
Proves the stated set-containment or membership property for forward Cumulant Map mem band Supported Cumulants.
Formal statement
Proof (Lean source)
Proves the stated set-containment or membership property for reverse Cumulant Map mem band Supported Cumulants.
Formal statement
Proof (Lean source)
Proves the stated set-containment or membership property for mem fiber Correspondence self.
Formal statement
Proof (Lean source)
Proves the stated set-containment or membership property for maps equality of mem fiber Correspondence.
Formal statement
Proof (Lean source)
Proves the stated set-containment or membership property for map equality target of mem fiber Correspondence.
Formal statement
Proof (Lean source)
Proves the stated set-containment or membership property for forward image mem generic Full Fiber Compatibility iff.
Formal statement
Proof (Lean source)
Proves the stated set-containment or membership property for reverse image mem generic Full Fiber Compatibility iff.
Formal statement
Proof (Lean source)
Proves the stated equality or equivalence for generic Compatibility Preimage Right iff.
Formal statement
Proof (Lean source)
Proves the stated equality or equivalence for generic Compatibility Preimage Left iff.
Formal statement
Proof (Lean source)
Proves the stated equality or equivalence for generic Full Fiber Compatibility equality worked projection.
Formal statement
Proof (Lean source)
Helpers.ExceptionalJacobianCoordinates 50 declarations Loading-slope derivatives
Loading-slope derivatives
Gives the stated evaluation formula for eval forward Band Loading Polynomial.
Formal statement
Proof (Lean source)
A definitionally explicit representative of the forward retained coordinate polynomial. Unlike the Classical.choose representative, its partial derivatives simplify directly.
Definition (Lean source)
The explicit representative computes the right thing: evaluated at any finite parameter coordinate vector it returns the corresponding retained cumulant coordinate of the forward band map, namely the sum over sources of that source's weight at the given order times the binary-form monomial in the source's loading direction.
Formal statement
Proof (Lean source)
The chosen coordinate family used by the promoted substrate is equal to the explicit coordinate polynomial above.
Formal statement
Proof (Lean source)
Partial derivatives of the canonical chosen coordinates may henceforth be computed from the explicit representative.
Formal statement
Proof (Lean source)
A weight derivative is the corresponding binary-form monomial. This is the ordinary Vandermonde block used at every retained order.
Formal statement
Proof (Lean source)
A weight coordinate belonging to a different retained order has zero derivative. This is the off-diagonal vanishing used by the block Jacobian.
Formal statement
Proof (Lean source)
Gives the stated evaluation formula for eval pderiv explicit Forward Band Coordinate Polynomial weight.
Formal statement
Proof (Lean source)
Weight derivatives at an arbitrary retained order. Distinct weight-order blocks do not interact; the matching block is the binary-form monomial.
Formal statement
Proof (Lean source)
Gives the stated evaluation formula for eval pderiv explicit Forward Band Coordinate Polynomial weight general.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of Forward Slope Index.
Definition (Lean source)
Defines the mathematical object called the forward Slope Band Coord.
Definition (Lean source)
Defines the index set used to select the forward Slope Source Index coordinates.
Definition (Lean source)
Proves that the map or coordinate assignment called the forward Slope Source Index is injective.
Formal statement
Proof (Lean source)
A loading-slope derivative is the derivative column of the corresponding finite node, multiplied by that source's weight.
Formal statement
Proof (Lean source)
Evaluation form of the slope derivative. This is the entry formula used to identify the selected top-order Jacobian block with a confluent Vandermonde matrix.
Formal statement
Proof (Lean source)
The loading-slope coordinate corresponding to a finite (non-infinity) source.
Definition (Lean source)
The slope coordinate attached to the j-th finite source — the direct slope when j is zero and the corresponding latent slope otherwise — is indeed carried by source j, viewed among the m + 1 finite sources, that is, all sources except the one at infinity.
Formal statement
Proof (Lean source)
Monomial rows of the top-order finite-source block.
Definition (Lean source)
Value columns are top-order weights; derivative columns are the finite source loading slopes.
Definition (Lean source)
A finite-coordinate witness tailored to the Jacobian calculation: the finite loading slopes are 1, ..., m+1 and every retained weight is one.
Definition (Lean source)
At the Jacobian witness parameter the loading direction of the j-th finite source is the vector with first entry one and second entry j + 1, so the finite loading slopes are the distinct numbers 1, ..., m + 1.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of forward Jacobian Witness top Weight cast Succ.
Formal statement
Proof (Lean source)
The selected finite-source part of the top-order Jacobian, evaluated at the explicit witness used elsewhere in the LiNGAM development.
Definition (Lean source)
The top-order finite-source block is exactly the standard doubled-node confluent Vandermonde matrix.
Formal statement
Proof (Lean source)
Proves that the quantity called the det forward Top Jacobian At Witness is nonzero.
Formal statement
Proof (Lean source)
The same selected block formed from the canonical coordinate family used by the polynomial-image dimension interface.
Definition (Lean source)
The selected top-order finite-source Jacobian block is the same matrix whether it is built from the canonical coordinate family used by the polynomial-image dimension interface or from the explicit representative.
Formal statement
Proof (Lean source)
Proves that the quantity called the det canonical Forward Top Jacobian At Witness is nonzero.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of Forward Top Augmented Index.
Definition (Lean source)
Defines the mathematical object called the forward Top Augmented Row.
Definition (Lean source)
Defines the mathematical object called the forward Top Augmented Column.
Definition (Lean source)
Defines the Jacobian matrix, row, column, or indexing object called the canonical Forward Top Augmented Jacobian At Witness.
Definition (Lean source)
Proves the stated mathematical property of forward Jacobian Witness loading last.
Formal statement
Proof (Lean source)
Proves the stated equality or equivalence for canonical Forward Top Augmented Jacobian At Witness eq.
Formal statement
Proof (Lean source)
Proves that the quantity called the det canonical Forward Top Augmented Jacobian At Witness is nonzero.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of Forward Low Weight Index.
Definition (Lean source)
Defines the mathematical object called the forward Low Weight Row.
Definition (Lean source)
Defines the mathematical object called the forward Low Weight Column.
Definition (Lean source)
Defines the Jacobian matrix, row, column, or indexing object called the canonical Forward Low Weight Jacobian At Witness.
Definition (Lean source)
Proves the stated equality or equivalence for canonical Forward Low Weight Jacobian At Witness eq.
Formal statement
Proof (Lean source)
Proves that the quantity called the det canonical Forward Low Weight Jacobian At Witness is nonzero.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of Forward High Weight Node.
Definition (Lean source)
Proves the stated mathematical property of Forward High Weight Index.
Definition (Lean source)
Defines the mathematical object called the forward High Weight Row.
Definition (Lean source)
Proves the stated mathematical property of forward High Weight Row order.
Formal statement
Proof (Lean source)
Defines the mathematical object called the forward High Weight Column.
Definition (Lean source)
Defines the Jacobian matrix, row, column, or indexing object called the canonical Forward High Weight Jacobian At Witness.
Definition (Lean source)
Proves the stated equality or equivalence for canonical Forward High Weight Jacobian At Witness eq.
Formal statement
Proof (Lean source)
Proves that the quantity called the det canonical Forward High Weight Jacobian At Witness is nonzero.
Formal statement
Proof (Lean source)
Helpers.ExceptionalJacobianMinor 31 declarations The ordinary-order block combines orders 2,...,m and m+1,...,2m+1.
The ordinary-order block combines orders 2,...,m and
m+1,...,2m+1. Only its lower-left block must vanish for the determinant
calculation; the upper-right block is kept explicitly.
Proves the stated mathematical property of Forward Ordinary Jacobian Index.
Definition (Lean source)
Defines the Jacobian matrix, row, column, or indexing object called the forward Ordinary Jacobian Row.
Definition (Lean source)
Defines the Jacobian matrix, row, column, or indexing object called the forward Ordinary Jacobian Column.
Definition (Lean source)
Defines the Jacobian matrix, row, column, or indexing object called the canonical Forward Ordinary Jacobian At Witness.
Definition (Lean source)
Proves the stated equality or equivalence for canonical Forward Ordinary Jacobian At Witness eq.
Formal statement
Proof (Lean source)
Proves that the quantity called the det canonical Forward Ordinary Jacobian At Witness is nonzero.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of Forward Full Jacobian Index.
Definition (Lean source)
Defines the Jacobian matrix, row, column, or indexing object called the forward Full Jacobian Row.
Definition (Lean source)
Defines the Jacobian matrix, row, column, or indexing object called the forward Full Jacobian Column.
Definition (Lean source)
Defines the Jacobian matrix, row, column, or indexing object called the canonical Forward Full Jacobian At Witness.
Definition (Lean source)
Proves the stated equality or equivalence for canonical Forward Full Jacobian At Witness eq.
Formal statement
Proof (Lean source)
Proves that the quantity called the det canonical Forward Full Jacobian At Witness is nonzero.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of card forward Full Jacobian Index.
Formal statement
Proof (Lean source)
Defines the Jacobian matrix, row, column, or indexing object called the forward Full Jacobian Equiv Fin.
Definition (Lean source)
Defines the Jacobian matrix, row, column, or indexing object called the forward Full Jacobian Fin Row.
Definition (Lean source)
Defines the Jacobian matrix, row, column, or indexing object called the forward Full Jacobian Fin Column.
Definition (Lean source)
Proves that the quantity called the forward Full Polynomial Jacobian Minor is nonzero.
Formal statement
Proof (Lean source)
The full forward retained-band image has the exact dimension certified by the global confluent/Vandermonde Jacobian minor and the independently proved generator-envelope upper bound.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of Common Axis Ordinary Jacobian Index.
Definition (Lean source)
Proves the stated mathematical property of Common Axis Full Jacobian Index.
Definition (Lean source)
Defines the Jacobian matrix, row, column, or indexing object called the common Axis Full Jacobian Row.
Definition (Lean source)
Defines the Jacobian matrix, row, column, or indexing object called the common Axis Full Jacobian Column.
Definition (Lean source)
Defines the Jacobian matrix, row, column, or indexing object called the canonical Common Axis Full Jacobian At Witness.
Definition (Lean source)
Proves the stated equality or equivalence for canonical Common Axis Full Jacobian At Witness eq.
Formal statement
Proof (Lean source)
Proves that the quantity called the det canonical Common Axis Full Jacobian At Witness is nonzero.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of card common Axis Full Jacobian Index.
Formal statement
Proof (Lean source)
Defines the Jacobian matrix, row, column, or indexing object called the common Axis Full Jacobian Equiv Fin.
Definition (Lean source)
Defines the Jacobian matrix, row, column, or indexing object called the common Axis Full Jacobian Fin Row.
Definition (Lean source)
Defines the Jacobian matrix, row, column, or indexing object called the common Axis Full Jacobian Fin Column.
Definition (Lean source)
Proves that the quantity called the forward Common Axis Polynomial Jacobian Minor is nonzero.
Formal statement
Proof (Lean source)
The common-axis retained-band image has the exact dimension certified by the pinned confluent-Vandermonde minor and the generator-envelope upper bound.
Formal statement
Proof (Lean source)
Helpers.FiberDimensionDefs 2 declarations
A relatively Zariski-closed parameter set is irreducible inside the retained finite-band ambient.
Definition (Lean source)
Exact relative Krull dimension, measured by strict chains of irreducible closed subsets inside the paper's retained-band parameter ambient.
Definition (Lean source)
Helpers.FiberSlopeComponents 2 declarations
Proves the stated set-containment or membership property for forward irreducible subset fixed Loading.
Formal statement
Proof (Lean source)
Proves the stated set-containment or membership property for reverse irreducible subset fixed Loading.
Formal statement
Proof (Lean source)
Helpers.FiniteCodimensionTransfer 2 declarations
Irreducible-component maximality is preserved by finite-band restriction.
Formal statement
Proof (Lean source)
Exact custom codimension in a band-supported CumVec set is equivalent to the same endpoint-fixed irreducible-chain statement in the finite retained affine space.
Formal statement
Proof (Lean source)
Helpers.FiniteCumBand 21 declarations
Finite coordinates (r,a) with 2 ≤ r ≤ L and a ≤ r.
Definition (Lean source)
Retained coordinates are a triangular family: at order k + 2 there are exactly k + 3 coordinate positions.
Definition (Lean source)
The finite retained band has the observable dimension q_L.
Formal statement
Proof (Lean source)
Restriction of an infinite cumulant vector to its retained coordinates.
Definition (Lean source)
Extend finite retained coordinates by zero.
Definition (Lean source)
Padding a finite list of retained cumulant coordinates with zeros produces a full cumulant vector that is supported on the band: every cumulant of order below two or above the truncation order is zero.
Formal statement
Proof (Lean source)
Reading the retained coordinates back off a zero-padded cumulant vector returns the original finite list of coordinates: padding then restricting changes nothing.
Formal statement
Proof (Lean source)
A cumulant vector that already vanishes outside the band loses nothing when it is cut down to its retained coordinates and padded back with zeros: the two operations recover the original vector exactly.
Formal statement
Proof (Lean source)
Substitute zero for every off-band observable variable.
Definition (Lean source)
Regard a finite-band polynomial as a polynomial in all cumulant variables.
Definition (Lean source)
Restricting a polynomial in all cumulant variables to the band does not change the value it takes at any cumulant vector supported on the band: substituting zero for the off-band variables and then evaluating on the retained coordinates gives the original value.
Formal statement
Proof (Lean source)
Gives the stated evaluation formula for eval extend Cum Polynomial.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of restrict extend Cum Polynomial.
Formal statement
Proof (Lean source)
On band-supported sets, ambient closure is exactly finite affine closure.
Formal statement
Proof (Lean source)
Proves the stated set-containment or membership property for zariski Closure subset band.
Formal statement
Proof (Lean source)
Proves that the map or coordinate assignment called the restrict Cum Band on band is injective.
Formal statement
Proof (Lean source)
Proves the stated set-containment or membership property for image restrict Cum Band subset iff.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of image restrict Cum Band inj.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of image restrict Cum Band union.
Formal statement
Proof (Lean source)
Closed band-supported sets correspond exactly to closed finite affine sets.
Formal statement
Proof (Lean source)
Irreducible closed band-supported sets correspond to irreducible closed sets in the finite retained affine space.
Formal statement
Proof (Lean source)
Helpers.FixedLoadingFiberDimension 8 declarations
The part of a forward fiber with the ordered loading coordinates fixed.
Definition (Lean source)
The part of a reverse fiber with the ordered loading coordinates fixed.
Definition (Lean source)
Every parameter point lying in a forward fiber with the loading coordinates held fixed is band-supported, meaning its source weights vanish at every cumulant order below two or above the truncation order.
Formal statement
Proof (Lean source)
Every parameter point lying in a reverse fiber with the loading coordinates held fixed is band-supported, meaning its source weights vanish at every cumulant order below two or above the truncation order.
Formal statement
Proof (Lean source)
Proves that the map or coordinate assignment called the forward fixed Loading Fiber dimension of is injective.
Formal statement
Proof (Lean source)
Proves that the map or coordinate assignment called the reverse fixed Loading Fiber dimension of is injective.
Formal statement
Proof (Lean source)
Establishes the stated dimension formula for forward fixed Loading Fiber.
Formal statement
Proof (Lean source)
Establishes the stated dimension formula for reverse fixed Loading Fiber.
Formal statement
Proof (Lean source)
Helpers.FullFiberSlopeRecovery 3 declarations
The displayed forward common-kernel identity determines the finite-slope multiset of every same-arrow representation, including nongeneric ones.
Formal statement
Proof (Lean source)
Reverse-arrow mirror of forward_slopes_determined_by_kernel_identity.
Formal statement
Proof (Lean source)
A root polynomial nonzero at zero certifies that every displayed latent slope is nonzero.
Formal statement
Proof (Lean source)
Helpers.GenericFiberDimension 2 declarations
Establishes the stated dimension formula for forward full fiber.
Formal statement
Proof (Lean source)
Establishes the stated dimension formula for reverse full fiber.
Formal statement
Proof (Lean source)
Helpers.GenericSlopes 7 declarations
On the generic locus the direct slope is nonzero.
Formal statement
Proof (Lean source)
On the generic locus the direct slope differs from every latent slope.
Formal statement
Proof (Lean source)
On the generic locus the latent slopes are pairwise distinct.
Formal statement
Proof (Lean source)
The forward loading slopes (u_j)₂ over j = 0,…,m (the direct slope γ followed by the latent slopes ρ_i) are pairwise distinct.
Formal statement
Proof (Lean source)
With nonzero latent slopes, the forward loading slopes (u_j)₂ over j = 0,…,m are all nonzero.
Formal statement
Proof (Lean source)
The reverse loading slopes (v_j)₁ over j = 1,…,m+1 (the latent slopes σ_i followed by the direct slope δ) are pairwise distinct.
Formal statement
Proof (Lean source)
With nonzero latent slopes, the reverse loading slopes (v_j)₁ over j = 1,…,m+1 are all nonzero.
Formal statement
Proof (Lean source)
Helpers.LoadingWeightKernelDimension 6 declarations
The linear weight-synthesis map attached to an arbitrary loading family.
Definition (Lean source)
Fixing the loading coordinates leaves the product of the orderwise loading-synthesis kernels.
Definition (Lean source)
Proves that the map or coordinate assignment called the forward loading Band Weight Kernel finrank of is injective.
Formal statement
Proof (Lean source)
Establishes the stated dimension formula for forward loading Band Weight Kernel.
Formal statement
Proof (Lean source)
Proves that the map or coordinate assignment called the reverse loading Band Weight Kernel finrank of is injective.
Formal statement
Proof (Lean source)
Establishes the stated dimension formula for reverse loading Band Weight Kernel.
Formal statement
Proof (Lean source)
Helpers.LowerOrderApolarKernel 6 declarations
Proves the stated mathematical property of lower Forward Evaluations Vanish.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of lower Reverse Evaluations Vanish.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of lower Forward Support Annihilator In Kernel.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of lower Reverse Support Annihilator In Kernel.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of lower Forward Apolar Kernel Identity.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of lower Reverse Apolar Kernel Identity.
Formal statement
Proof (Lean source)
Helpers.LowerOrderApolarRank 27 declarations
Defines the polynomial called the lower First Polynomial.
Definition (Lean source)
Defines the polynomial called the lower Slope Polynomial.
Definition (Lean source)
Defines the polynomial called the lower Reverse First Polynomial.
Definition (Lean source)
Defines the polynomial called the lower Reverse Second Polynomial.
Definition (Lean source)
Defines the polynomial called the lower Weight Polynomial.
Definition (Lean source)
Selected rows for the block partition J₀={axis}, J₁={direct} and J_{m-1}={latent sources}.
Definition (Lean source)
The coordinate-reversed selected minor. Its top block uses coefficients in reverse order so that the latent columns are an ordinary Vandermonde matrix.
Definition (Lean source)
Real rank witness for the forward arrow on the shorter apolar stack: the determinant of the selected forward contraction minor, read as a polynomial in the real structural parameters. Where this polynomial does not vanish, the selected rows of the forward contraction have full rank.
Definition (Lean source)
Defines the polynomial called the lower Reverse Real Rank Polynomial.
Definition (Lean source)
Defines the polynomial called the lower Forward Complex Rank Polynomial.
Definition (Lean source)
Defines the polynomial called the lower Reverse Complex Rank Polynomial.
Definition (Lean source)
Proves the stated mathematical property of lower Forward Rank Polynomial map of Real.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of lower Reverse Rank Polynomial map of Real.
Formal statement
Proof (Lean source)
Gives the stated evaluation formula for lower Forward Rank Polynomial complexify.
Formal statement
Proof (Lean source)
Gives the stated evaluation formula for lower Reverse Rank Polynomial complexify.
Formal statement
Proof (Lean source)
Defines the mathematical object called the lower Forward Minor.
Definition (Lean source)
Defines the mathematical object called the lower Reverse Minor.
Definition (Lean source)
The selected scalar rows of the contractions visible at order 2m+1. They are the k=0 constant coefficient, the k=1 first coefficient, and all coefficients of the k=m-1 block.
Definition (Lean source)
The coordinate-reversed selected contraction rows.
Definition (Lean source)
Gives the stated evaluation formula for lower Forward Minor.
Formal statement
Proof (Lean source)
Gives the stated evaluation formula for lower Reverse Minor.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of lower Forward Explicit Rank Data.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of lower Reverse Explicit Rank Data.
Formal statement
Proof (Lean source)
Proves that the quantity called the lower Forward Real Rank Polynomial is nonzero.
Formal statement
Proof (Lean source)
Proves that the quantity called the lower Reverse Real Rank Polynomial is nonzero.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of lower Forward Contraction Rank Witness.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of lower Reverse Contraction Rank Witness.
Formal statement
Proof (Lean source)
Helpers.LowerOrderApolarSeparation 15 declarations
Defines the polynomial called the lower Slope Product Polynomial.
Definition (Lean source)
Defines the polynomial called the lower Forward Real Exceptional Polynomial.
Definition (Lean source)
Defines the polynomial called the lower Reverse Real Exceptional Polynomial.
Definition (Lean source)
Defines the polynomial called the lower Forward Complex Exceptional Polynomial.
Definition (Lean source)
Defines the polynomial called the lower Reverse Complex Exceptional Polynomial.
Definition (Lean source)
Proves that the quantity called the lower Slope Product Polynomial is nonzero.
Formal statement
Proof (Lean source)
Proves that the quantity called the lower Forward Real Exceptional Polynomial is nonzero.
Formal statement
Proof (Lean source)
Proves that the quantity called the lower Reverse Real Exceptional Polynomial is nonzero.
Formal statement
Proof (Lean source)
Gives the stated evaluation formula for lower Forward Exceptional complexify.
Formal statement
Proof (Lean source)
Gives the stated evaluation formula for lower Reverse Exceptional complexify.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of forward Slopes Injective of real Feasible.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of reverse Slopes Injective of real Feasible.
Formal statement
Proof (Lean source)
Proves the stated compatibility of forward Cumulant Map with complexification.
Formal statement
Proof (Lean source)
Proves the stated compatibility of reverse Cumulant Map with complexification.
Formal statement
Proof (Lean source)
At m ≥ 3, the complete cumulant truncation through order 2m+1 generically separates the two real arrows.
Formal statement
Proof (Lean source)
Helpers.LowerOrderEmptyFiber 2 declarations
Proves the stated mathematical property of lower Forward Reverse Impossible.
Formal statement
Proof (Lean source)
Proves the stated mathematical property of lower Reverse Forward Impossible.
Formal statement
Proof (Lean source)
Helpers.MomentGate 3 declarations
The real parameter points at which a fixed complex polynomial does not vanish after complexification form a Euclidean-open set.
Formal statement
Proof (Lean source)
The generic-parameter polynomial stays nonzero after pinning: it is witnessed at the pinned parameter point whose direct slope is one, whose latent slopes are 2, 3, …, m+1, and whose in-band weights are all one.
Formal statement
Proof (Lean source)
If the truncated-moment interior gate holds, every polynomial whose pinned form is nonzero has a nonvanishing point in the real feasible parameter region.
Formal statement
Proof (Lean source)
Helpers.PinSubst 7 declarations
Pinning substitutes zero for every weight coordinate outside orders two through L, while leaving all loading coordinates and retained weight coordinates fixed.
Definition (Lean source)
A polynomial remains nonzero after pinning whenever it is nonzero at one point whose out-of-band weight coordinates are already zero.
Formal statement
Proof (Lean source)
Pinning fixes every loading coordinate, so a latent slope variable remains the same variable.
Formal statement
Proof (Lean source)
A coordinate assignment determines a structural parameter with its loading coordinates and retained source weights unchanged and all off-band weights set to zero.
Definition (Lean source)
Every parameter obtained by pinning a coordinate assignment belongs to the paper's finite retained-band parameter space.
Formal statement
Proof (Lean source)
Evaluating a pinned polynomial at a coordinate assignment equals evaluating the original polynomial at the corresponding pinned parameter.
Formal statement
Proof (Lean source)
At a parameter in the paper's retained band, pinning a polynomial does not change its value.
Formal statement
Proof (Lean source)
Helpers.PolynomialRetractDimension 2 declarations The polynomial-map and retract proofs are implemented in neutral substrate; this file retains the paper namespace and method-style API.
Compatibility reexports for polynomial retract dimension
The polynomial-map and retract proofs are implemented in neutral substrate; this file retains the paper namespace and method-style API.
Proves the stated mathematical property of comp.
Formal statement
Proof (Lean source)
Gives the stated evaluation formula for eval comp.
Formal statement
Proof (Lean source)
Helpers.ReverseApolarKernel 5 declarations
The genuine weighted contraction map for the reverse loading family.
Definition (Lean source)
Common reverse contractions force all directional evaluations to vanish.
Formal statement
Proof (Lean source)
Reverse interpolation in the affine chart X₁ = 1, with the omitted axis direction supplying the vanishing top coefficient.
Formal statement
Proof (Lean source)
The common reverse apolar kernel is the reverse support-annihilator line.
Formal statement
Proof (Lean source)
Reverse contraction injectivity holds on the principal open set cut out by a genuine coefficient-minor determinant. The polynomial is nonzero at an explicit witness whose weights vanish outside the pinned degree band.
Formal statement
Proof (Lean source)
Helpers.SlopeUniqueness 2 declarations This file recovers, with multiplicity, the finite forward and reverse loading slopes from the one-dimensional common apolar-contraction kernel.
This file recovers, with multiplicity, the finite forward and reverse loading slopes from the one-dimensional common apolar-contraction kernel.
At a forward parameter where the common apolar-contraction kernel is the support-annihilator line, cumulants through order 2m+2 determine the multiset of the direct and latent finite loading slopes.
Formal statement
Proof (Lean source)
At a reverse parameter where the common apolar-contraction kernel is the support-annihilator line, cumulants through order 2m+2 determine the multiset of the direct and latent finite loading slopes.
Formal statement
Proof (Lean source)
Helpers.Varieties 27 declarations Quotient fibers modulo admissible swaps and Jacobian ranks
Quotient fibers modulo admissible swaps and Jacobian ranks
Zariski closure of a set A ⊆ ℂ^{q_L} of cumulant vectors: the common zero set of every polynomial (in the coordinate ring ℂ[t_{r,a}]) that vanishes on A. Coordinates are indexed by (r, a) ∈ ℕ × ℕ.
Definition (Lean source)
Coordinate index of the structural parameter space: the direct slope, the m latent slopes, and the weight family (j, r).
Definition (Lean source)
Evaluate the parameter coordinates of θ at a coordinate index.
Definition (Lean source)
Zariski closure of a set of structural parameters.
Definition (Lean source)
A Zariski-open subset of the parameter space (complement of a proper Zariski closed set).
Definition (Lean source)
A Zariski-dense subset of the parameter space.
Definition (Lean source)
The relative Zariski closure consists of the retained-band parameters at which every polynomial vanishing on the original set also vanishes.
Definition (Lean source)
A relatively Zariski-open set is the complement, within the retained-band parameter space, of a proper relatively closed set.
Definition (Lean source)
A relatively Zariski-dense set has the whole retained-band parameter space as its relative Zariski closure.
Definition (Lean source)
An irreducible Zariski-closed subset of the cumulant coordinate space: nonempty, Zariski-closed, and not the union of two proper Zariski-closed subsets. A strictly increasing chain of such sets is a chain of irreducible subvarieties (a prime chain in the coordinate ring), which is the dimension/codimension notion — Krull dimension via irreducible-component chains — that a codimension statement requires, as opposed to a chain of arbitrary Zariski-closed sets.
Definition (Lean source)
Complexification of a real structural parameter, coordinatewise.
Definition (Lean source)
Complexification of a real cumulant coordinate vector, coordinatewise.
Definition (Lean source)
Axis-conditioned cumulant-image variety C^b_{m,L}, the Zariski closure of the image of the arrow map Φ over the whole complex parameter space. The same construction gives C^right (with forwardCumulantMap) and C^left (with reverseCumulantMap). @realizes C^right_{m,L},C^left_{m,L}(Zariski closure of the arrow-map image)
Definition (Lean source)
Generic full-fiber opposite-arrow compatibility locus E_m ⊆ ℂ^{q_K} (K = 2m + 2): observable vectors t whose one arrow has a generic full fiber and whose opposite arrow has a (possibly non-generic) full fiber. This is the first of the four components of def:generic-full-fiber-compatibility (bundled in genericFullFiberCompatibilityLocus). @realizes E_m,barE_m,H^right_m,H^left_m(compatibility locus E_m)
Definition (Lean source)
Zariski closure \bar E_m of the compatibility locus — the second component of the compatibility-locus construction def:generic-full-fiber-compatibility (E_m, \bar E_m, H^right_m, H^left_m). @realizes E_m,barE_m,H^right_m,H^left_m(Zariski closure \bar E_m)
Definition (Lean source)
Parameter-level preimage H^b_m = Θ^{b,∘}_{m,K} ∩ (Φ^b)^{-1}(E_m) — the third and fourth components of def:generic-full-fiber-compatibility (H^right_m with Φ = forwardCumulantMap, H^left_m with Φ = reverseCumulantMap).
Definition (Lean source)
Right generic-locus preimage H^right_m = Θ^{right,∘}_{m,K} ∩ (Φ^right)^{-1}(E_m) — the third component of def:generic-full-fiber-compatibility.
Definition (Lean source)
Left generic-locus preimage H^left_m = Θ^{left,∘}_{m,K} ∩ (Φ^left)^{-1}(E_m) — the fourth component of def:generic-full-fiber-compatibility.
Definition (Lean source)
Generic full-fiber compatibility construction — the full four-component object the paper's def:generic-full-fiber-compatibility defines, bundled so the extracted definition carries all of its parts (not only E_m):
Definition (Lean source)
Orbit of θ under the admissible source-swap G_m action (the admissible relabelings of the middle latent block).
Definition (Lean source)
Same-arrow quotient fiber of Φ over t: the set of G_m-orbits (admissible-source-swap classes) contained in the full fiber Φ⁻¹(t). This is the quotient of the same-arrow fiber by the admissible-swap action, not an assertion that the fiber is a single orbit.
Definition (Lean source)
Update the coordinate k of a complex structural parameter θ to the value s.
Definition (Lean source)
Finite active parameter coordinates through retained order L: the direct slope, the m latent slopes, and the weights c_{jr} for r ≤ L.
Definition (Lean source)
The active parameter coordinate as a full parameter coordinate.
Definition (Lean source)
The Jacobian matrix of an arrow map Φ at θ over the retained finite coordinate band up to order L: the partial derivative of each retained output coordinate (r, a) with respect to each active parameter coordinate, taken with Mathlib's deriv (each Φ-coordinate is polynomial in one substituted scalar).
Definition (Lean source)
The Jacobian rank of the same-arrow fiber equation of Φ at θ (through retained order L): the rank of jacobianMatrix. The quantitative value of this rank is the deferred content (interfaces I-1/I-2).
Definition (Lean source)
Separation handle: the data used to compare the two axis-conditioned decompositions after quotienting each same-arrow fiber by G_m. It records the shared-observable equation, the two complete quotient fibers, and the two Jacobian ranks at the displayed representatives. The fixed vertical/horizontal axes are already built into forwardCumulantMap and reverseCumulantMap.
Definition (Lean source)
Helpers.ZariskiLocus 8 declarations
Every assignment of the structural coordinates is represented by a parameter.
Formal statement
The complement of the vanishing set of a nonzero polynomial is Zariski-open and dense.
Formal statement
Proof (Lean source)
The polynomial whose nonvanishing defines the generic parameter locus.
Definition (Lean source)
The polynomial defining the generic parameter restrictions is not identically zero.
Formal statement
Proof (Lean source)
At any complex parameter value, the genericity polynomial equals the product of the direct slope, all slope-separation factors, and all retained cumulant coordinates.
Formal statement
Proof (Lean source)
The generic parameter locus is the band-supported parameter space with the genericity polynomial nonzero.
Formal statement
Proof (Lean source)
Within the paper's finite retained-band parameter space, the nonvanishing locus of any polynomial whose pinned form is nonzero is relatively Zariski-open and dense.
Formal statement
Proof (Lean source)
The generic retained-band parameter locus is relatively Zariski-open and dense in the paper's finite structural parameter space.
Formal statement
Proof (Lean source)
Selector 39 declarations The note defines the arrow decision on the rank-open locus by *"factoring the recovered degree-n support annihilator Q_D from the contractions of the divided-power forms f_{n+k}"* (def:global-feasible-fiber-decision; wri
The apolar route: divided-power blocks and their contractions
The note defines the arrow decision on the rank-open locus by "factoring the recovered degree-n
support annihilator Q_D from the contractions of the divided-power forms f_{n+k}"
(def:global-feasible-fiber-decision; writeup.tex §thm:generic-apolar-arrow-recovery). Q_D is
therefore not just some squarefree product over a recovered support — it is the generator of the
common contraction kernel. These three primitives let the certificate say exactly that, so the
definition carries the note's own characterization of Q_D rather than a downstream consequence of
it. (They mirror dividedPowerBlock / diffApply / supportAnnihilator of
Helpers/ApolarDefs.lean, which are stated over ℂ; the certificate lives over ℝ.)
Coordinate index of the real structural parameter space (direct slope, the m latent slopes, and the weight family (j, r)).
Definition (Lean source)
Evaluate the real parameter coordinates of θ at a coordinate index.
Definition (Lean source)
A proper real algebraic subset of the parameter space: the (real) zero locus of a nonzero real polynomial in the parameter coordinates. Nonzeroness of the polynomial makes it a proper subset (its complement is Zariski-dense), which is the paper's genericity notion — deletion of a proper real algebraic subset.
Definition (Lean source)
Causal direction value.
Definition (Lean source)
Provides a procedure that decides whether two causal directions are equal.
Definition (Lean source)
Raw moments μ_r = B_r(0, k_2, …, k_r) from a centered cumulant list k (with k 1 = 0 supplied by the caller), via the exponential/Bell set-partition formula μ_r = Σ_{π} ∏_{B∈π} k_{|B|}.
Definition (Lean source)
Finite atomic (Hankel-PSD / truncated Hamburger) certificate Q_K(k): the raw moments μ_r(k) (1 ≤ r ≤ K) are the moments of an n-atom probability law with μ_2 > 0. Its equivalence with real non-Gaussian finite-K source realizability is the external interface I-4.
Definition (Lean source)
Global feasible-fiber feasibility formula FeasFiber^b_m(t) at order K = 2m + 2 (the existential-atomic-feasibility component of the bundled def:global-feasible-fiber-decision, feasibleFiberDecision below). Its truth value is exactly the nonemptiness of R^b_{m,K}(t) ∩ F^b_{m,K}: there exist b-loading and source-cumulant coordinates λ that are real moment-feasible (λ ∈ F^b_{m,K}, which already carries the nonzero direct slope, the pairwise-distinct finite slopes, the finite-band cumulant coordinates, and the real non-Gaussian source realizability whose finite atomic Q_K reformulation is interface I-4) with Φ^b(λ) = t. By construction this def is the exact feasible-fiber equivalence; the atomic Q_K reformulation is atomicCertificate below.
Definition (Lean source)
Signs used by a finite polynomial sign table.
Definition (Lean source)
Provides a procedure that decides whether two polynomial signs are equal.
Definition (Lean source)
Sign of a real number.
Definition (Lean source)
A function on cumulant vectors is given by a finite semialgebraic sign table: finitely many observable-coordinate polynomials are evaluated and their signs are looked up in a finite table.
Definition (Lean source)
The three variable blocks in the prescribed CAD order.
Definition (Lean source)
Provides a procedure that decides whether two variable blocks of the fiber decision problem are equal.
Definition (Lean source)
The prescribed elimination order is t, then λ, then atomic witnesses.
Definition (Lean source)
A stacked cumulant vector is band-supported when it vanishes off the retained range 2 ≤ r ≤ 2m + 2, a ≤ r — the only coordinates the order-(2m+2) truncation records. Every cumulant map Φ^b_{m,2m+2} lands here (it is defined to be 0 off the band), so this is exactly the observable coordinate space the paper's decision procedure ranges over.
Definition (Lean source)
A finite sign-table decision obtained by CAD using the paper's prescribed t, then λ, then atomic-witness variable-block order, and deciding the stated feasible-fiber formula on the band-supported observable coordinates. Keeping the order as an argument of the certificate ties it to this CAD decision rather than recording an unrelated order witness.
Definition (Lean source)
The fixed projective axis belonging to an arrow parameterization.
The direction-specific cumulant map used by the arrow certificate.
Definition (Lean source)
A genuine polynomial rank-open locus: a nonempty principal open set cut out by nonvanishing of a nonzero observable-coordinate minor.
Definition (Lean source)
The retained divided-power cumulant blocks of t admit the displayed m+2-direction support with order-specific source weights.
Definition (Lean source)
Two nonzero affine representatives determine the same projective direction.
Definition (Lean source)
A support list has pairwise distinct projective directions.
Definition (Lean source)
Equality of unordered supports in projective space, allowing an independent nonzero rescaling of every displayed affine representative.
Definition (Lean source)
On the rank-open locus the support is recovered from the simultaneous divided-power blocks: every other projectively distinct m+2-direction decomposition has the same unordered projective support.
Definition (Lean source)
Real divided-power binary form of the order-r cumulant block: f_r(x, y) = Σ_{a=0}^r C(r,a) t_{r,a} x^{r-a} y^a (with x = X 0, y = X 1).
Definition (Lean source)
The apolar contraction q(∂) f of a binary form f by the constant-coefficient differential operator with symbol q.
Definition (Lean source)
The squarefree degree-n support annihilator Q_D = ∏_{ℓ ∈ D} ℓ^⊥ as a real binary form, in the same sign convention as the evaluation-form product used by the certificate below.
Definition (Lean source)
The recovered squarefree support-annihilator certificate on the apolar rank-open locus. Q_D is characterized exactly as the note characterizes it — as the generator of the common kernel of the contractions q ↦ (q(∂) f_{n+k})_{0 ≤ k ≤ n-2} of the divided-power blocks, n = m + 2 — and it is then factored into the m+2 support directions, from which the decision is read off membership of the arrow's fixed axis.
Definition (Lean source)
Operational structure required by the paper: a finite semialgebraic real-QE/CAD decision, with the prescribed variable-block order, and its apolar support-annihilator implementation on the rank-open locus.
Definition (Lean source)
Global feasible-fiber decision FeasFiber^b_m — the full object the paper's def:global-feasible-fiber-decision defines, bundled as a pair so the extracted definition carries both the existential atomic feasibility formula and the paper's operational decision structure (not only the existential Prop, which alone under-records the paper):
Definition (Lean source)
Separate-fiber direction selector S_m(t) (the two-branch relational component of the bundled def:direction-selector, directionSelectorWithDecision below): forward when the forward feasible-fiber formula holds and the reverse fails, reverse in the mirror case, and undefined (none) otherwise. The Option-valued map encodes only the two-branch relation; any claim that S_m is an evaluable finite semialgebraic decision procedure rests on the external interface I-3 and is not encoded (the definition is noncomputable, decided classically). @realizes S_m(two-branch partial direction map)
Definition (Lean source)
The separated observable domain on which exactly one feasible arrow remains.
Definition (Lean source)
Operational selector structure: one finite semialgebraic procedure on the declared separated domain, together with the two arrow-specific apolar support-annihilator factorizations implementing its generic branches.
Definition (Lean source)
Separate-fiber direction selector S_m — the full object the paper's def:direction-selector defines, bundled so the extracted definition carries both the two-branch selection map and the paper's operational decision structure (not only the weaker noncomputable classical two-branch relation):
Definition (Lean source)
Structural-model witness M: a bivariate LvLiNGAM structural model carrying its observational law P_M = law, its directed edge D(M) = edge, and a direction-specific real moment-feasible parameter list param ∈ F^b_{m,K} (with b = edge) that realizes the truncated cumulant observation T_K(P_M) through order K, together with the corresponding LvLiNGAM class membership. This carries the model / representation identity (P_M and its feasible parameters) that a bare observational measure would lose. @realizes M,P_M,D(M),M^{sep}_{m,K}(model M: law P_M, edge D(M), feasible param)
Definition (Lean source)
Separated nonzero-edge structural-model domain M^{sep}_{m,K}, a K-explicit set of structural models M : StructuralModel m K (each carrying its law P_M, edge D(M), and direction-specific feasible parameters). Membership imposes opposite-arrow fiber emptiness at T_K(P_M): a forward model whose reverse feasible fiber over T_K(P_M) is empty, or a reverse model whose forward feasible fiber over T_K(P_M) is empty. The domain retains the model / representation identity and the explicit truncation order K. @realizes M,P_M,D(M),M^{sep}_{m,K}(models M with empty opposite fiber at T_K(P_M))
Definition (Lean source)
Generic arrow separation at order L: off a proper real algebraic subset of each real feasible region, no arrow value admits an opposite-region representation. The excluded set is constrained to be a proper real algebraic subset (the zero locus of a nonzero real polynomial), matching the paper's genericity notion; an arbitrary excluded set is not permitted. Helper for def:information-order.
Definition (Lean source)
Generic real information order K^star(m): the least L ≥ 2 at which the arrow is generically separated over both real feasible regions, and ⊤ = ∞ if no such L exists. @realizes K^star(m)(least separating truncation order)
Definition (Lean source)
TAdmissibleSwaps 1 declarations In-scope crux: admissible swaps preserve the arrow
In-scope crux: admissible swaps preserve the arrow
Admissible swaps preserve direction. For each π ∈ G_m:
Formal statement
Proof (Lean source)
TApolar 1 declarations
Generic apolar arrow recovery. With n = m + 2 and K = 2n - 2 = 2m + 2, there are Zariski-open dense parameter loci U^right ⊆ Θ^{right,∘}_{m,K} and U^left ⊆ Θ^{left,∘}_{m,K}, each meeting its real feasible region, on which the full opposite-arrow fiber is empty: for every θ ∈ U^right the reverse fiber over Φ^right_{m,K}(θ) is empty, and dually for U^left. Recovery is by factoring the degree-n support annihilator Q_D and reading its fixed axis.
Formal statement
Proof (Lean source)
TExceptionalLocus 1 declarations
Exceptional-locus codimension one. For every m ≥ 1, the complex exceptional closure has codimension exactly one in both arrow-image varieties; for m ≥ 2 it therefore does not have the formerly conjectured codimension m. The two generic parameter preimages are exactly the band-supported generic points retaining a complete opposite-arrow fiber, and the m=1 and m=2 incidence systems project exactly to E_m.
Formal statement
Proof (Lean source)
TGenericSeparation 1 declarations
Generic arrow recovery and fiber obstruction. At K = 2m+2, relative Zariski-open dense loci meet the real feasible regions in nonempty relatively Euclidean-open sets. On them the unordered loading directions are recovered and the full opposite-arrow fiber is empty. Nevertheless a direct/latent source-pair swap lies in the same-arrow fiber but outside the admissible G_m-orbit; for m ≥ 2 the complete same-arrow fiber has exact relative Zariski dimension m(m-1)/2 from the independent low-order weight kernels.
Formal statement
Proof (Lean source)
TInfoOrder 1 declarations
Improved real information order. For every m ≥ 3, generic real opposite-arrow separation already holds at order 2m+1. Hence K^star(m) ≤ 2m+1, and in particular it is not equal to 2m+2.