This record groups the data and proof fields needed for “core factorization”. A proposition-valued field is a requirement until a constructor supplies it. The physical bit/right-bond indexing is retained in the returned core.
structure CoreFactorization {l r : ℕ} (A : Core l r) where
R : _root_.Matrix (Fin l) (Fin (min l (2 * r))) ℝ
Q : Core (min l (2 * r)) r
factorization : A = R * Q
orthogonal : Q * Q.transpose = 1
/-- Relabel the deterministic matrix factors by the explicit product index. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “factor core”. Relabel the deterministic matrix factors by the explicit product index.
noncomputable def factorCore {l r : ℕ} (A : Core l r) : CoreFactorization A := by
commit-pinned source · Verso Blueprint panel
This record groups the data and proof fields needed for “result”. A proposition-valued field is a requirement until a constructor supplies it. Concrete canonical data, indexed by the precise original chain.
structure Result {n l r : ℕ} (C : Chain n l r) where
rank : ℕ
residual : _root_.Matrix (Fin l) (Fin rank) ℝ
canonical : Chain n rank r
rightCanonical : RightCanonical canonical
rankReduced : RankReduced C canonical
action : ∀ x, contract C x = residual * contract canonical x
/-- Structural recursion on the source chain; no factor or basis selection. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “canonicalize”. Structural recursion on the source chain; no factor or basis selection.
noncomputable def canonicalize : {n l r : ℕ} → (C : Chain n l r) → Result C
| _, _, _, .nil r =>
{ rank := r, residual := 1, canonical := .nil r,
rightCanonical := trivial, rankReduced := .nil r,
action := fun _ => by simp [contract] }
| _, l, _, .cons A C =>
let tailResult := canonicalize C
let headResult := factorCore (absorb A tailResult.residual)
{ rank := min l (2 * tailResult.rank), residual := headResult.R,
canonical := .cons headResult.Q tailResult.canonical,
rightCanonical := ⟨headResult.orthogonal, tailResult.rightCanonical⟩,
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “canonicalize right canonical”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem canonicalize_rightCanonical {n l r : ℕ} (C : Chain n l r) :
RightCanonical (canonicalize C).canonical := (canonicalize C).rightCanonical
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “canonicalize rank reduced”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem canonicalize_rankReduced {n l r : ℕ} (C : Chain n l r) :
RankReduced C (canonicalize C).canonical := (canonicalize C).rankReduced
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “canonicalize action”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem canonicalize_action {n l r : ℕ} (C : Chain n l r) (x : Word n) :
contract C x = (canonicalize C).residual * contract (canonicalize C).canonical x :=
(canonicalize C).action x
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “canonicalize max bond le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem canonicalize_maxBond_le {n l r : ℕ} (C : Chain n l r) :
maxBond (canonicalize C).canonical ≤ maxBond C :=
(canonicalize C).rankReduced.maxBond_le
/-- The returned residual converts an original boundary into its new boundary. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “boundary”. The returned residual converts an original boundary into its new boundary.
noncomputable def boundary {n l r : ℕ} (C : Chain n l r) (v : Fin l → ℝ) :
Fin (canonicalize C).rank → ℝ := _root_.Matrix.vecMul v (canonicalize C).residual
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “boundary action”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem boundary_action {n l r : ℕ} (C : Chain n l r) (v : Fin l → ℝ) (x : Word n) :
_root_.Matrix.vecMul v (contract C x) =
_root_.Matrix.vecMul (boundary C v) (contract (canonicalize C).canonical x) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “boundary mass”; the hypotheses and conclusion in the code panel fix its exact scope. Total source mass is obtained from the small returned residual boundary.
theorem boundary_mass {n l r : ℕ} (C : Chain n l r) (v : Fin l → ℝ) :
chainMass C v = mass (boundary C v) :=
residual_mass C (canonicalize C).canonical (canonicalize C).residual
(canonicalize C).rightCanonical (canonicalize C).action v
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “boundary normalized”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem boundary_normalized {n l r : ℕ} (C : Chain n l r) (v : Fin l → ℝ)
(normalized : chainMass C v = 1) : mass (boundary C v) = 1 :=
(boundary_mass C v).symm.trans normalized
/-- Concrete scalar-boundary state data, without requiring normalization. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “state boundary”. Concrete scalar-boundary state data, without requiring normalization.
noncomputable def stateBoundary {n : ℕ} (C : Chain n 1 1) :
Fin (canonicalize C).rank → ℝ := boundary C (fun _ => 1)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “state boundary action”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem stateBoundary_action {n : ℕ} (C : Chain n 1 1) (x : Word n) :
contract C x 0 0 = ∑ a, stateBoundary C a * contract (canonicalize C).canonical x a 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “state boundary normalized”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem stateBoundary_normalized {n : ℕ} (C : Chain n 1 1)
(normalized : (∑ x : Word n, (contract C x 0 0) ^ 2) = 1) :
mass (stateBoundary C) = 1 := by
commit-pinned source · Verso Blueprint panel