pith. machine review for the scientific record. sign in
def definition def or abbrev high

trivialFlow

show as:
view Lean formalization →

Any defect-bounded sub-ledger admits a constant coarse-graining flow that keeps the apparent defect fixed at every scale. Researchers formalizing the RS version of the Hodge conjecture cite this as the baseline flow that satisfies the monotonicity and non-negativity axioms without additional structure. The definition populates the flow fields directly from the ledger's defect value together with reflexivity of the order and the non-negativity theorem for defect.

claimFor any finite set of recognition events with bounded total J-cost, the constant function returning that total J-cost defines a coarse-graining flow on the set.

background

In the RS translation of the Hodge conjecture a defect-bounded sub-ledger is a finite collection of recognition events whose total J-cost (defect) is finite and bounded above by phi^44. A coarse-graining flow on such a ledger consists of a function from natural numbers to reals giving the apparent defect after n successive coarse-grainings, required to equal the ledger defect at scale zero, to be monotone non-increasing, and to remain non-negative at every scale. The local setting is the module that maps classical Hodge classes to coarse-graining-stable classes and algebraic cycles to J-cost-minimal cycles.

proof idea

The definition directly instantiates the four fields of the coarse-graining flow structure. The coarsened defect is set to the constant function returning the ledger defect. The zero-scale equality holds by reflexivity. Monotonicity follows from the reflexive property of the order relation on the naturals. Non-negativity is supplied by the defect non-negativity theorem.

why it matters in Recognition Science

The construction supplies the simplest explicit flow inside the module that translates the Hodge conjecture into Recognition Science terms. It anchors the proved direction that every J-cost-minimal cycle is coarse-graining stable by providing a canonical flow for every sub-ledger. The module leaves open the converse direction of the conjecture; this definition does not close that gap but supplies the baseline object against which stability can be tested.

scope and limits

formal statement (Lean)

 199def trivialFlow (L : DefectBoundedSubLedger) : CoarseGrainingFlow L where
 200  coarsened_defect := fun _ => L.defect

proof body

Definition body.

 201  at_zero := rfl
 202  monotone_decrease := fun _ => le_refl _
 203  nonneg := fun _ => L.defect_nonneg
 204
 205/-- The limit of a coarse-graining flow is the asymptotic defect. -/

depends on (16)

Lean names referenced from this declaration's body.