IndisputableMonolith.Cosmology.RefineTrigger
Selective refinement of a coarsened recognition cell: expand internal postings only for blocks a decision predicate marks, while always keeping cross-block events. Cosmogenesis and equilibrium arguments cite it when a coarse ledger must be partially restored without full fine-grain cost. The module packages reconstruction, losslessness criteria, and a descent law tying refinement choices to J-cost.
claimGiven a coarsened cell and a blockwise decision $D$, reconstruct the fine cell by retaining every cross-block event and expanding a block's internal postings if and only if $D$ holds on that block; blocks left coarse contribute no internal postings. Losslessness holds precisely when reconstruction recovers the original fine data. A descent law relates admissible refinements to decrease (or non-increase) of the $J$-cost.
background
Scale-adaptive cosmogenesis works with rung-coarsened cells: fine postings are grouped into blocks so that sigma-structure and cost can be tracked at a coarser rung. The upstream RungCoarsen module is the Lean form of theorem T-1: rung-coarsening is sigma-exact and cost-exact (the "literal" theorem), matching the numerical round-trip on the voxel battery and idle cell.
This module sits one step finer. A decision predicate $D$ on blocks chooses which coarse blocks to reopen. Reconstruction keeps all cross-block events unconditionally; internal postings of a block appear only when $D$ selects that block. Sibling material includes the reconstruction map, a losslessness biconditional, demand and Boolean selectors, and the $J$-cost $J(x)=(x+x^{-1})/2-1$ with positivity and arbitrarily-small-positive facts used to compare refined versus coarse ledgers.
proof idea
Definition-heavy module with supporting lemmas rather than a single top theorem. Reconstruction is specified by cases on $D$: expand internals only on selected blocks, always retain cross-block structure. Losslessness is characterized by an iff relating full recovery of fine postings to the decision covering every block that carried internal mass. Descent and necessity lemmas connect admissible refinement choices to $J$-cost comparison, using positivity of $J$ and the Boolean block selectors. No single wrapper; the argument is the package of reconstruct-under-$D$, lossless criteria, and the descent law.
why it matters in Recognition Science
Feeds RecognitionEquilibrium, which discharges the Phase-7 forward-dynamics facts: a field of recognition levels on a coupling graph evolves by forced mean-resolutions (sigma = 0, $J$-minimal moves) and converges to the $J$-cost ground state. Selective refine-under-$D$ is the bookkeeping bridge between rung-coarsened ledgers (T-1 exactness) and those equilibrium dynamics: the engine can reopen only the blocks the decision demands without spoiling cost accounting.
In the broader RS spine this is cosmogenesis infrastructure, not a forcing-chain T0–T8 step. It keeps the eight-tick / rung ladder operational when the simulation alternates coarse and fine views while still measuring progress by $J$.
scope and limits
- Does not prove global cosmogenesis convergence; that lives in RecognitionEquilibrium.
- Does not re-prove rung-coarsening exactness; assumes RungCoarsen (T-1).
- Does not force a unique decision $D$; $D$ is an input predicate on blocks.
- Does not claim physical units or observational cosmology fits.
- Does not expand internals of blocks where $D$ fails; those stay coarse by design.
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