signed_log_flow
plain-language theorem explainer
Placeholder for the signed logarithmic flow of a single bond in a recognition ledger state. It currently returns the constant zero for every state and bond index. Anyone wiring bond-level dynamics or cost gradients into the recognition operator will hit this symbol. The body is a pure stub, not a derived identity.
Claim. For every ledger state $s$ and bond index $b$, the signed log-flow is defined by $\mathrm{signed\_log\_flow}(s,b) := 0 \in \mathbb{R}$.
background
In this module a ledger state is identified with an eight-component signal (Signal8), the discrete carrier of the eight-tick octave. Bonds are bare natural-number identifiers. Elsewhere in the monolith, ledger states appear with richer structure: positive real bond multipliers, active-bond finsets, and a total recognition cost summed over bonds.
Signed log-flow is the natural bond-wise quantity one would extract from those multipliers: something like $\pm\log m_b$, measuring directed stretch or compression of a bond ratio. The recognition operator is meant to evolve the ledger by such bond-level updates, consistent with the J-cost and the Recognition Composition Law.
No non-trivial formula is supplied yet. The definition ignores both arguments and returns zero, so it does not yet connect to bond multipliers, Z-patterns, or global phase.
proof idea
There is no proof. The declaration is a definitional stub: both parameters are unused, and the right-hand side is the real constant $0$. No lemmas are applied.
why it matters
The recognition operator needs a bond-resolved flow to drive ledger evolution and to interface with variational dynamics and information-cost thermodynamics. A signed log of bond multipliers is the obvious candidate once the operator is non-trivial.
At present nothing downstream depends on this symbol (used_by is empty). It is scaffolding for a future non-zero flow that should respect eight-tick structure, conserved total log-ratio (charge), and the J-cost geometry forced in the T5–T8 chain. Until the body is replaced, it contributes no dynamical content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.