IndisputableMonolith.Cosmology.RefineTrigger
Selective reconstruction of a fine cell from a coarse partition: only blocks chosen by a decision predicate D are expanded, while cross-block events are always kept. Cosmogenesis and equilibrium arguments cite it when a rung-coarsened ledger must be refined without reopening every block. The module packages the reconstruction map, lossless criteria, and a descent law tying refinement to J-cost.
claimGiven a coarse partition of a fine cell and a decision predicate $D$ on blocks, reconstruct the fine ledger by retaining every cross-block event and expanding internal postings of a block if and only if $D$ holds on that block. Blocks left coarse contribute no internal postings. The module also records when this reconstruction is lossless and when refinement descends in $J$-cost.
background
Scale-adaptive cosmogenesis works with rung-coarsened ledgers: fine recognition events are grouped into blocks so that sigma and cost can be tracked exactly at coarser rungs. The upstream module RungCoarsen discharges theorem T-1: rung-coarsening is sigma-exact and cost-exact (the "literal" theorem of the Cosmogenesis north-star plan).
This module sits one step above that exact coarsening. A decision predicate $D$ marks which coarse blocks should be opened again. Reconstruction keeps the global cross-block skeleton fixed and only re-expands internal postings inside selected blocks; unselected blocks stay coarse and contribute nothing internal.
Sibling material introduces the reconstruction map, a losslessness criterion (round-trip fidelity under $D$), a descent law relating refinement to the Recognition Science $J$-cost $J(x)=(x+x^{-1})/2-1$, positivity and smallness facts for that cost, and a simple demand/bit interface used to drive which blocks open.
proof idea
Definition-heavy module with supporting lemmas rather than a single deep theorem. It defines the selective reconstruction operator from a coarse cell and predicate $D$, then proves characterizations of lossless reconstruction (when expanding exactly the $D$-selected blocks recovers the fine postings of interest). Descent and necessity lemmas connect the decision to monotone decrease of $J$-cost, using positivity of $J$ on the positive reals and the fact that $J$ can be arbitrarily small yet positive. Bit-level helpers package the open/closed choice per block.
why it matters in Recognition Science
Recognition equilibrium (the downstream consumer) needs a controlled way to refine a coarsened field while the forward dynamics posts forced mean-resolving events toward the $J$-minimal ground state. Without selective refine-under-$D$, every descent step would have to reopen the full fine ledger, breaking the T-1 coarsening discipline.
The module therefore supplies the refine trigger that lets Phase-7 forward dynamics stay on the coarse spine until a block's demand forces expansion. It links the literal coarsening theorem T-1 to the equilibrium convergence facts: dynamics may descend in $J$ at coarse grain and only pay the fine internal postings where $D$ fires. That is the bridge between rung-exact bookkeeping and the claim that recognition levels flow to the $J$-cost ground state on the coupling graph.
scope and limits
- Does not prove global convergence of forward dynamics; that lives in RecognitionEquilibrium.
- Does not re-prove sigma- or cost-exactness of coarsening; those are imported from RungCoarsen T-1.
- Does not choose a unique physical predicate D; D is an input decision interface.
- Does not fix cosmological parameters, expansion history, or observational constraints.
- Does not assert losslessness for arbitrary D; losslessness is characterized, not automatic.
used by (1)
depends on (1)
declarations in this module (17)
-
def
reconstructUnder -
theorem
lossless_iff -
def
descendLaw -
theorem
lossless_law -
theorem
descendLaw_necessary -
def
Jcost -
theorem
jcost_pos -
theorem
jcost_arbitrarily_small_positive -
def
demand -
def
b01 -
theorem
b01_zero -
theorem
b01_one -
theorem
cost_singleton -
theorem
epsilon_unsafe -
structure
LawGivenTrigger -
theorem
lawGivenTrigger -
theorem
t3_law_derived_refinement