The literal standard second closed star attains 25/48
Abstract
Sharpness of the literal second-star coordinate bound
For each original vertex, the equal-weight barycenter of the four parent-flag vertices lies in the corresponding literal closed star and has coordinate exactly 25/48.
Theorem 1.1 (The 25/48 lower bound is attained).
Lean statement: D5/S3/Geometry/Gluing/LiteralSecondStarCoordinateBoundSharpness.literal_standard_closed_star_coordinate_bound_sharp
Proof. Machine-checked in Lean as D5/S3/Geometry/Gluing/LiteralSecondStarCoordinateBoundSharpness.literal_standard_closed_star_coordinate_bound_sharp (✓ std3). ∎
Source. Repository-derived.
Commentary.
The equal-weight barycenter of the four parent-flag vertices is a closed-star point, and its distinguished coordinate is exactly the average 1, 1/2, 1/3, 1/4.